proof

let c₁ be set ;
let c₂, c₃ be FinSequence of c₁;
assume that E2: c₂ is one-to-one
and E3: c₃ is one-to-one
and E4: rng c₂ = rng c₃ ;
set c₄ = c₃ * (c₂ " );
E5: dom c₃ = dom c₂

proof

len c₂ = card (rng c₃) by E2, E4, FINSEQ_4:77
.= len c₃ by E3, FINSEQ_4:77 ;
then dom c₂ = Seg (len c₃) by FINSEQ_1:def 3
.= dom c₃ by FINSEQ_1:def 3 ;
hence dom c₃ = dom c₂ ;

end;

E6: ( dom (c₃ * (c₂ " )) = dom c₂ & rng (c₃ * (c₂ " )) = dom c₂ )

proof

E7: now

let c₅ be set ;
( dom (c₂ " ) = rng c₂ & rng (c₂ " ) = dom c₂ ) by E2, FUNCT_1:55;
then ( c₅ in dom c₃ implies c₃ . c₅ in dom (c₂ " ) ) by E4, FUNCT_1:12;
hence ( c₅ in dom (c₃ * (c₂ " )) iff c₅ in dom c₃ ) by FUNCT_1:21;

end;

then E8: dom (c₃ * (c₂ " )) = dom c₃ by TARSKI:2;
E9: ( dom (c₂ " ) = rng c₂ & rng (c₂ " ) = dom c₂ ) by E2, FUNCT_1:55;
E10: rng (c₃ * (c₂ " )) c= dom c₂

proof

let c₅ be set ; :: uses TARSKI:def 3
assume c₅ in rng (c₃ * (c₂ " )) ;
hence c₅ in dom c₂ by E9, FUNCT_1:25;

end;

dom c₂ c= rng (c₃ * (c₂ " ))

proof

let c₅ be set ; :: uses TARSKI:def 3
assume c₅ in dom c₂ ;
then c₅ in rng (c₂ " ) by E2, FUNCT_1:55;
then consider c₆ being set such that
E11: c₆ in dom (c₂ " )
and E12: c₅ = (c₂ " ) . c₆ by FUNCT_1:def 5;
c₆ in rng c₃ by E2, E4, E11, FUNCT_1:55;
then consider c₇ being set such that
E13: c₇ in dom c₃
and E14: c₆ = c₃ . c₇ by FUNCT_1:def 5;
c₅ = (c₃ * (c₂ " )) . c₇ by E12, E13, E14, FUNCT_1:23;
hence c₅ in rng (c₃ * (c₂ " )) by E8, E13, FUNCT_1:def 5;

end;

hence ( dom (c₃ * (c₂ " )) = dom c₂ & rng (c₃ * (c₂ " )) = dom c₂ ) by E5, E7, E10, TARSKI:2, XBOOLE_0:def 10;

end;

c₂ " is one-to-one by E2, FUNCT_1:62;
then ( c₃ * (c₂ " ) is one-to-one & rng (c₃ * (c₂ " )) = dom c₂ ) by E3, E6, FUNCT_1:46;
then E7: c₃ * (c₂ " ) is Permutation of dom c₂ by E6, FUNCT_2:3, FUNCT_2:83;

now

let c₅ be set ;
( c₅ in dom (c₃ * (c₂ " )) implies (c₃ * (c₂ " )) . c₅ in dom c₂ ) by E6, FUNCT_1:12;
hence ( c₅ in dom ((c₃ * (c₂ " )) * c₂) iff c₅ in dom c₂ ) by E6, FUNCT_1:21;

end;

then E8: dom c₃ = dom ((c₃ * (c₂ " )) * c₂) by E5, TARSKI:2;
for b₁ being set holds
( b₁ in dom c₃ implies c₃ . b₁ = ((c₃ * (c₂ " )) * c₂) . b₁ )

proof

let c₅ be set ;
assume E9: c₅ in dom c₃ ;
then E10: c₃ . c₅ in rng c₂ by E4, FUNCT_1:12;
((c₃ * (c₂ " )) * c₂) . c₅ = c₂ . ((c₃ * (c₂ " )) . c₅) by E5, E6, E9, FUNCT_1:23
.= c₂ . ((c₂ " ) . (c₃ . c₅)) by E9, FUNCT_1:23
.= c₃ . c₅ by E2, E10, FUNCT_1:57 ;
hence c₃ . c₅ = ((c₃ * (c₂ " )) * c₂) . c₅ ;

end;

then c₃ = (c₃ * (c₂ " )) * c₂ by E8, FUNCT_1:9;
hence ( dom c₂ = dom c₃ & ex b₁ being Permutation of dom c₂ st
( c₃ = b₁ * c₂ & dom b₁ = dom c₂ & rng b₁ = dom c₂ ) ) by E5, E6, E7;

end;

definition

let c₁ be non empty set ;
let c₂ be BinOp of c₁;
assume E2: ( c₂ is commutative & c₂ is associative & c₂ is has_a_unity ) ;
let c₃ be finite Subset of c₁;
func a₂ ++ a₃ -> Element of a₁ means :: BHSP_5:def 1
ex b₁ being FinSequence of a₁ st
( b₁ is one-to-one & rng b₁ = a₃ & a₄ = a₂ "**" b₁ );
existence

proof

consider c₄ being FinSequence such that
E3: rng c₄ = c₃
and E4: c₄ is one-to-one by FINSEQ_4:73;
reconsider c₅ = c₄ as FinSequence of c₁ by E3, FINSEQ_1:def 4;
ex b₁ being FinSequence of c₁ st
( b₁ is one-to-one & rng b₁ = c₃ & c₂ "**" c₅ = c₂ "**" b₁ ) by E3, E4;
hence ex b₁ being Element of c₁ex b₂ being FinSequence of c₁ st
( b₂ is one-to-one & rng b₂ = c₃ & b₁ = c₂ "**" b₂ ) ;

end;

uniqueness

proof

let c₄, c₅ be Element of c₁;
assume that E3: ex b₁ being FinSequence of c₁ st
( b₁ is one-to-one & rng b₁ = c₃ & c₄ = c₂ "**" b₁ )
and E4: ex b₁ being FinSequence of c₁ st
( b₁ is one-to-one & rng b₁ = c₃ & c₅ = c₂ "**" b₁ ) ;
consider c₆ being FinSequence of c₁ such that
E5: c₆ is one-to-one
and E6: rng c₆ = c₃
and E7: c₄ = c₂ "**" c₆ by E3;
consider c₇ being FinSequence of c₁ such that
E8: c₇ is one-to-one
and E9: rng c₇ = c₃
and E10: c₅ = c₂ "**" c₇ by E4;
( dom c₆ = dom c₇ & ex b₁ being Permutation of dom c₆ st
( c₇ = b₁ * c₆ & dom b₁ = dom c₆ & rng b₁ = dom c₆ ) ) by E5, E6, E8, E9, E1;
then consider c₈ being Permutation of dom c₆ such that
E11: c₇ = c₈ * c₆ ;
thus c₄ = c₅ by E2, E7, E10, E11, FINSOP_1:8;

end;

definition

let c₁ be RealUnitarySpace;
let c₂ be finite Subset of c₁;
func setop_SUM a₂,a₁ -> set equals :: BHSP_5:def 2
the add of a₁ ++ a₂ if a₂ <> {}
otherwise 0. a₁;
correctness ;

end;

definition

let c₁ be RealUnitarySpace;
let c₂ be Point of c₁;
let c₃ be FinSequence;
let c₄ be Nat;
func PO a₄,a₃,a₂ -> set equals :: BHSP_5:def 3
the scalar of a₁ . [a₂,(a₃ . a₄)];
correctness ;

end;

definition

let c₁, c₂ be non empty set ;
let c₃ be Function of c₂,c₁;
let c₄ be FinSequence of c₂;
func Func_Seq a₃,a₄ -> FinSequence of a₁ equals :: BHSP_5:def 4
a₄ * a₃;
correctness by FINSEQ_2:36;

end;

definition

let c₁, c₂ be non empty set ;
let c₃ be BinOp of c₁;
assume E2: ( c₃ is commutative & c₃ is associative & c₃ is has_a_unity ) ;
let c₄ be finite Subset of c₂;
let c₅ be Function of c₂,c₁;
assume E3: c₄ c= dom c₅ ;
func setopfunc a₄,a₂,a₁,a₅,a₃ -> Element of a₁ means :E2: :: BHSP_5:def 5
ex b₁ being FinSequence of a₂ st
( b₁ is one-to-one & rng b₁ = a₄ & a₆ = a₃ "**" (Func_Seq a₅,b₁) );
existence

proof

consider c₆ being FinSequence such that
E4: rng c₆ = c₄
and E5: c₆ is one-to-one by FINSEQ_4:73;
reconsider c₇ = c₆ as FinSequence of c₂ by E4, FINSEQ_1:def 4;
ex b₁ being FinSequence of c₂ st
( b₁ is one-to-one & rng b₁ = c₄ & c₃ "**" (Func_Seq c₅,c₇) = c₃ "**" (Func_Seq c₅,b₁) ) by E4, E5;
hence ex b₁ being Element of c₁ex b₂ being FinSequence of c₂ st
( b₂ is one-to-one & rng b₂ = c₄ & b₁ = c₃ "**" (Func_Seq c₅,b₂) ) ;

end;

uniqueness

proof

let c₆, c₇ be Element of c₁;
assume that E4: ex b₁ being FinSequence of c₂ st
( b₁ is one-to-one & rng b₁ = c₄ & c₆ = c₃ "**" (Func_Seq c₅,b₁) )
and E5: ex b₁ being FinSequence of c₂ st
( b₁ is one-to-one & rng b₁ = c₄ & c₇ = c₃ "**" (Func_Seq c₅,b₁) ) ;
consider c₈ being FinSequence of c₂ such that
E6: c₈ is one-to-one
and E7: rng c₈ = c₄
and E8: c₆ = c₃ "**" (Func_Seq c₅,c₈) by E4;
consider c₉ being FinSequence of c₂ such that
E9: c₉ is one-to-one
and E10: rng c₉ = c₄
and E11: c₇ = c₃ "**" (Func_Seq c₅,c₉) by E5;
E12: ( dom c₈ = dom c₉ & ex b₁ being Permutation of dom c₈ st
( c₉ = b₁ * c₈ & dom b₁ = dom c₈ & rng b₁ = dom c₈ ) ) by E6, E7, E9, E10, E1;
consider c₁₀ being Permutation of dom c₈ such that
E13: c₉ = c₁₀ * c₈
and dom c₁₀ = dom c₈
and rng c₁₀ = dom c₈ by E6, E7, E9, E10, E1;

now

let c₁₁ be set ;
( c₁₁ in dom c₈ implies c₈ . c₁₁ in rng c₈ ) by FUNCT_1:12;
hence ( c₁₁ in dom (Func_Seq c₅,c₈) iff c₁₁ in dom c₈ ) by E3, E7, FUNCT_1:21;

end;

then E14: dom (Func_Seq c₅,c₈) = dom c₈ by TARSKI:2;

now

let c₁₁ be set ;
( c₁₁ in dom c₉ implies c₉ . c₁₁ in rng c₉ ) by FUNCT_1:12;
hence ( c₁₁ in dom (Func_Seq c₅,c₉) iff c₁₁ in dom c₉ ) by E3, E10, FUNCT_1:21;

end;

then E15: dom (Func_Seq c₅,c₉) = dom c₉ by TARSKI:2;
E16: ( dom c₁₀ = dom (Func_Seq c₅,c₈) & rng c₁₀ = dom (Func_Seq c₅,c₈) ) by E14, FUNCT_2:67, FUNCT_2:def 3;
Func_Seq c₅,c₉ = c₁₀ * (Func_Seq c₅,c₈)

proof

now

let c₁₁ be set ;
( c₁₁ in dom c₁₀ implies c₁₀ . c₁₁ in dom (Func_Seq c₅,c₈) ) by E16, FUNCT_1:12;
then ( c₁₁ in dom (c₁₀ * (Func_Seq c₅,c₈)) iff c₁₁ in dom c₁₀ ) by FUNCT_1:21;
hence ( c₁₁ in dom (c₁₀ * (Func_Seq c₅,c₈)) iff c₁₁ in dom (Func_Seq c₅,c₉) ) by E12, E15, FUNCT_2:67;

end;

then E17: dom (Func_Seq c₅,c₉) = dom (c₁₀ * (Func_Seq c₅,c₈)) by TARSKI:2;

now

let c₁₁ be set ;
assume E18: c₁₁ in dom (Func_Seq c₅,c₉) ;
E19: dom (Func_Seq c₅,c₉) is Subset of NAT by RELSET_1:12;
then reconsider c₁₂ = c₁₁ as Nat by E18;
c₁₂ in dom c₁₀ by E12, E15, E18, FUNCT_2:67;
then E20: c₁₀ . c₁₂ in rng c₁₀ by FUNCT_1:12;
then c₁₀ . c₁₂ in dom (Func_Seq c₅,c₉) by E12, E15, FUNCT_2:def 3;
then reconsider c₁₃ = c₁₀ . c₁₂ as Nat by E19;
E21: c₁₃ in dom c₈ by E20, FUNCT_2:def 3;
E22: c₁₁ in dom c₁₀ by E12, E15, E18, FUNCT_2:67;
(Func_Seq c₅,c₉) . c₁₁ = (c₉ * c₅) . c₁₂
.= c₅ . (c₉ . c₁₂) by E15, E18, FUNCT_1:23
.= c₅ . (c₈ . (c₁₀ . c₁₂)) by E13, E22, FUNCT_1:23
.= (c₈ * c₅) . c₁₃ by E21, FUNCT_1:23
.= (Func_Seq c₅,c₈) . c₁₃
.= (c₁₀ * (Func_Seq c₅,c₈)) . c₁₁ by E22, FUNCT_1:23 ;
hence (Func_Seq c₅,c₉) . c₁₁ = (c₁₀ * (Func_Seq c₅,c₈)) . c₁₁ ;

end;

hence Func_Seq c₅,c₉ = c₁₀ * (Func_Seq c₅,c₈) by E17, FUNCT_1:9;

end;

hence c₆ = c₇ by E2, E8, E11, E14, FINSOP_1:8;

end;

definition

let c₁ be RealUnitarySpace;
let c₂ be Point of c₁;
let c₃ be finite Subset of c₁;
func setop_xPre_PROD a₂,a₃,a₁ -> Real means :: BHSP_5:def 6
ex b₁ being FinSequence of the carrier of a₁ st
( b₁ is one-to-one & rng b₁ = a₃ & ex b₂ being FinSequence of REAL st
( dom b₂ = dom b₁ & for b₃ being Nat holds
( b₃ in dom b₂ implies b₂ . b₃ = PO b₃,b₁,a₂ ) & a₄ = addreal "**" b₂ ) );
existence

proof

consider c₄ being FinSequence such that
E3: rng c₄ = c₃
and E4: c₄ is one-to-one by FINSEQ_4:73;
reconsider c₅ = c₄ as FinSequence of the carrier of c₁ by E3, FINSEQ_1:def 4;
set c₆ = len c₅;
deffunc H₁( Nat) -> set = PO a₁,c₅,c₂;
ex b₁ being FinSequence st
( len b₁ = len c₅ & for b₂ being Nat holds
( b₂ in Seg (len c₅) implies b₁ . b₂ = H₁(b₂) ) ) from FINSEQ_1:sch 2();
then consider c₇ being FinSequence such that
E5: ( len c₇ = len c₅ & for b₁ being Nat holds
( b₁ in Seg (len c₅) implies c₇ . b₁ = PO b₁,c₅,c₂ ) ) ;
E6: dom c₇ = Seg (len c₅) by E5, FINSEQ_1:def 3;
then E7: dom c₇ = dom c₅ by FINSEQ_1:def 3;

now

let c₈ be Nat;
assume E8: c₈ in dom c₇ ;
then E9: c₇ . c₈ = PO c₈,c₅,c₂ by E5, E6
.= the scalar of c₁ . [c₂,(c₅ . c₈)] ;
reconsider c₉ = c₅ . c₈ as Point of c₁ by E7, E8, FINSEQ_2:13;
the scalar of c₁ . [c₂,(c₅ . c₈)] = c₂ .|. c₉ by BHSP_1:def 1;
hence c₇ . c₈ in REAL by E9;

end;

then reconsider c₈ = c₇ as FinSequence of REAL by FINSEQ_2:14;
take addreal "**" c₈ ;
thus ex b₁ being FinSequence of the carrier of c₁ st
( b₁ is one-to-one & rng b₁ = c₃ & ex b₂ being FinSequence of REAL st
( dom b₂ = dom b₁ & for b₃ being Nat holds
( b₃ in dom b₂ implies b₂ . b₃ = PO b₃,b₁,c₂ ) & addreal "**" c₈ = addreal "**" b₂ ) ) by E3, E4, E5, E6, E7;

end;

uniqueness

proof

let c₄, c₅ be Element of REAL ;
assume that E3: ex b₁ being FinSequence of the carrier of c₁ st
( b₁ is one-to-one & rng b₁ = c₃ & ex b₂ being FinSequence of REAL st
( dom b₂ = dom b₁ & for b₃ being Nat holds
( b₃ in dom b₂ implies b₂ . b₃ = PO b₃,b₁,c₂ ) & c₄ = addreal "**" b₂ ) )
and E4: ex b₁ being FinSequence of the carrier of c₁ st
( b₁ is one-to-one & rng b₁ = c₃ & ex b₂ being FinSequence of REAL st
( dom b₂ = dom b₁ & for b₃ being Nat holds
( b₃ in dom b₂ implies b₂ . b₃ = PO b₃,b₁,c₂ ) & c₅ = addreal "**" b₂ ) ) ;
consider c₆ being FinSequence of the carrier of c₁ such that
E5: c₆ is one-to-one
and E6: rng c₆ = c₃
and E7: ex b₁ being FinSequence of REAL st
( dom b₁ = dom c₆ & for b₂ being Nat holds
( b₂ in dom b₁ implies b₁ . b₂ = PO b₂,c₆,c₂ ) & c₄ = addreal "**" b₁ ) by E3;
consider c₇ being FinSequence of the carrier of c₁ such that
E8: c₇ is one-to-one
and E9: rng c₇ = c₃
and E10: ex b₁ being FinSequence of REAL st
( dom b₁ = dom c₇ & for b₂ being Nat holds
( b₂ in dom b₁ implies b₁ . b₂ = PO b₂,c₇,c₂ ) & c₅ = addreal "**" b₁ ) by E4;
consider c₈ being FinSequence of REAL such that
E11: dom c₈ = dom c₆
and E12: for b₁ being Nat holds
( b₁ in dom c₈ implies c₈ . b₁ = PO b₁,c₆,c₂ )
and E13: c₄ = addreal "**" c₈ by E7;
consider c₉ being FinSequence of REAL such that
E14: dom c₉ = dom c₇
and E15: for b₁ being Nat holds
( b₁ in dom c₉ implies c₉ . b₁ = PO b₁,c₇,c₂ )
and E16: c₅ = addreal "**" c₉ by E10;
E17: ( dom c₆ = dom c₇ & ex b₁ being Permutation of dom c₆ st
( c₇ = b₁ * c₆ & dom b₁ = dom c₆ & rng b₁ = dom c₆ ) ) by E5, E6, E8, E9, E1;
consider c₁₀ being Permutation of dom c₆ such that
E18: c₇ = c₁₀ * c₆
and dom c₁₀ = dom c₆
and rng c₁₀ = dom c₆ by E5, E6, E8, E9, E1;
E19: ( dom c₁₀ = dom c₈ & rng c₁₀ = dom c₈ ) by E11, FUNCT_2:67, FUNCT_2:def 3;
E20: ( dom c₁₀ = dom c₉ & rng c₁₀ = dom c₉ ) by E14, E17, FUNCT_2:67, FUNCT_2:def 3;
E21: dom c₆ = dom c₉ by E5, E6, E8, E9, E14, E1;

now

let c₁₁ be set ;
( c₁₁ in dom c₁₀ implies c₁₀ . c₁₁ in dom c₈ ) by E19, FUNCT_1:12;
hence ( c₁₁ in dom (c₁₀ * c₈) iff c₁₁ in dom c₉ ) by E20, FUNCT_1:21;

end;

then E22: dom c₉ = dom (c₁₀ * c₈) by TARSKI:2;
c₉ = c₁₀ * c₈

proof

E23: dom c₉ is Subset of NAT by RELSET_1:12;

now

let c₁₁ be set ;
assume E24: c₁₁ in dom c₉ ;
then reconsider c₁₂ = c₁₁ as Nat by E23;
c₁₀ . c₁₂ in dom c₉ by E20, E24, FUNCT_1:12;
then reconsider c₁₃ = c₁₀ . c₁₂ as Nat by E23;
E25: c₁₃ in dom c₈ by E11, E20, E21, E24, FUNCT_1:12;
E26: c₁₁ in dom c₁₀ by E14, E17, E24, FUNCT_2:67;
c₉ . c₁₁ = PO c₁₂,c₇,c₂ by E15, E24
.= the scalar of c₁ . [c₂,((c₁₀ * c₆) . c₁₂)] by E18
.= the scalar of c₁ . [c₂,(c₆ . c₁₃)] by E26, FUNCT_1:23
.= PO c₁₃,c₆,c₂
.= c₈ . (c₁₀ . c₁₂) by E12, E25
.= (c₁₀ * c₈) . c₁₁ by E26, FUNCT_1:23 ;
hence c₉ . c₁₁ = (c₁₀ * c₈) . c₁₁ ;

end;

hence c₉ = c₁₀ * c₈ by E22, FUNCT_1:9;

end;

hence c₄ = c₅ by E11, E13, E16, FINSOP_1:8;

end;

definition

let c₁ be RealUnitarySpace;
let c₂ be Point of c₁;
let c₃ be finite Subset of c₁;
func setop_xPROD a₂,a₃,a₁ -> Real equals :: BHSP_5:def 7
setop_xPre_PROD a₂,a₃,a₁ if a₃ <> {}
otherwise 0;
correctness ;

end;

definition

let c₁ be RealUnitarySpace;
mode OrthogonalFamily of a₁ -> Subset of a₁ means :E3: :: BHSP_5:def 8
for b₁, b₂ being Point of a₁ holds
( ( b₁ in a₂ & b₂ in a₂ ) implies ( not b₁ <> b₂ or b₁ .|. b₂ = 0 ) );
existence

proof

take {} ;
thus ( {} is Subset of c₁ & for b₁, b₂ being Point of c₁ holds
( ( b₁ in {} & b₂ in {} ) implies ( not b₁ <> b₂ or b₁ .|. b₂ = 0 ) ) ) by SUBSET_1:4;

end;

proof

let c₁ be RealUnitarySpace;
E5: {} is Subset of c₁ by SUBSET_1:4;
for b₁, b₂ being Point of c₁ holds
( ( b₁ in {} & b₂ in {} ) implies ( not b₁ <> b₂ or b₁ .|. b₂ = 0 ) ) ;
hence {} is OrthogonalFamily of c₁ by E5, E3;

end;

registration

let c₁ be RealUnitarySpace;
cluster finite OrthogonalFamily of a₁;
existence

proof

take {} ;
thus ( {} is Subset of c₁ & {} is OrthogonalFamily of c₁ & {} is finite ) by E4;

end;

definition

let c₁ be RealUnitarySpace;
mode OrthonormalFamily of a₁ -> Subset of a₁ means :E5: :: BHSP_5:def 9
( a₂ is OrthogonalFamily of a₁ & for b₁ being Point of a₁ holds
( b₁ in a₂ implies b₁ .|. b₁ = 1 ) );
existence

proof

take {} ;
thus ( {} is Subset of c₁ & {} is OrthogonalFamily of c₁ & for b₁ being Point of c₁ holds
( b₁ in {} implies b₁ .|. b₁ = 1 ) ) by E4;

end;

proof

let c₁ be RealUnitarySpace;
E7: {} is OrthogonalFamily of c₁ by E4;
for b₁ being Point of c₁ holds
( b₁ in {} implies b₁ .|. b₁ = 1 ) ;
hence {} is OrthonormalFamily of c₁ by E7, E5;

end;

registration

let c₁ be RealUnitarySpace;
cluster finite OrthonormalFamily of a₁;
existence

proof

take {} ;
thus ( {} is Subset of c₁ & {} is OrthonormalFamily of c₁ & {} is finite ) by E6;

end;

proof

let c₁ be RealUnitarySpace;
let c₂ be Point of c₁;
( for b₁ being Point of c₁ holds c₂ .|. b₁ = 0 implies c₂ = 0. c₁ )

proof

now

assume for b₁ being Point of c₁ holds c₂ .|. b₁ = 0 ;
then c₂ .|. c₂ = 0 ;
hence c₂ = 0. c₁ by BHSP_1:def 2;

end;

hence ( for b₁ being Point of c₁ holds c₂ .|. b₁ = 0 implies c₂ = 0. c₁ ) ;

end;

hence ( c₂ = 0. c₁ iff for b₁ being Point of c₁ holds c₂ .|. b₁ = 0 ) by BHSP_1:19;

end;

proof

let c₁ be RealUnitarySpace;
let c₂, c₃ be Point of c₁;
E7: (c₂ + c₃) .|. (c₂ + c₃) >= 0 by BHSP_1:def 2;
E8: (c₂ - c₃) .|. (c₂ - c₃) >= 0 by BHSP_1:def 2;
E9: c₂ .|. c₂ >= 0 by BHSP_1:def 2;
E10: c₃ .|. c₃ >= 0 by BHSP_1:def 2;
(||.(c₂ + c₃).|| ^2 ) + (||.(c₂ - c₃).|| ^2 ) = ((sqrt ((c₂ + c₃) .|. (c₂ + c₃))) ^2 ) + (||.(c₂ - c₃).|| ^2 ) by BHSP_1:def 4
.= ((c₂ + c₃) .|. (c₂ + c₃)) + (||.(c₂ - c₃).|| ^2 ) by E7, SQUARE_1:def 4
.= ((c₂ + c₃) .|. (c₂ + c₃)) + ((sqrt ((c₂ - c₃) .|. (c₂ - c₃))) ^2 ) by BHSP_1:def 4
.= ((c₂ + c₃) .|. (c₂ + c₃)) + ((c₂ - c₃) .|. (c₂ - c₃)) by E8, SQUARE_1:def 4
.= (((c₂ .|. c₂) + (2 * (c₂ .|. c₃))) + (c₃ .|. c₃)) + ((c₂ - c₃) .|. (c₂ - c₃)) by BHSP_1:21
.= (((c₂ .|. c₂) + (2 * (c₂ .|. c₃))) + (c₃ .|. c₃)) + (((c₂ .|. c₂) - (2 * (c₂ .|. c₃))) + (c₃ .|. c₃)) by BHSP_1:23
.= (2 * (c₂ .|. c₂)) + (2 * (c₃ .|. c₃))
.= (2 * ((sqrt (c₂ .|. c₂)) ^2 )) + (2 * (c₃ .|. c₃)) by E9, SQUARE_1:def 4
.= (2 * ((sqrt (c₂ .|. c₂)) ^2 )) + (2 * ((sqrt (c₃ .|. c₃)) ^2 )) by E10, SQUARE_1:def 4
.= (2 * (||.c₂.|| ^2 )) + (2 * ((sqrt (c₃ .|. c₃)) ^2 )) by BHSP_1:def 4
.= (2 * (||.c₂.|| ^2 )) + (2 * (||.c₃.|| ^2 )) by BHSP_1:def 4 ;
hence (||.(c₂ + c₃).|| ^2 ) + (||.(c₂ - c₃).|| ^2 ) = (2 * (||.c₂.|| ^2 )) + (2 * (||.c₃.|| ^2 )) ;

end;

proof

let c₁ be RealUnitarySpace;
let c₂, c₃ be Point of c₁;
assume c₂,c₃ are_orthogonal ;
then E7: c₂ .|. c₃ = 0 by BHSP_1:def 3;
E8: (c₂ + c₃) .|. (c₂ + c₃) >= 0 by BHSP_1:def 2;
E9: c₂ .|. c₂ >= 0 by BHSP_1:def 2;
E10: c₃ .|. c₃ >= 0 by BHSP_1:def 2;
||.(c₂ + c₃).|| ^2 = (sqrt ((c₂ + c₃) .|. (c₂ + c₃))) ^2 by BHSP_1:def 4
.= (c₂ + c₃) .|. (c₂ + c₃) by E8, SQUARE_1:def 4
.= ((c₂ .|. c₂) + (2 * (c₂ .|. c₃))) + (c₃ .|. c₃) by BHSP_1:21
.= ((sqrt (c₂ .|. c₂)) ^2 ) + (c₃ .|. c₃) by E7, E9, SQUARE_1:def 4
.= ((sqrt (c₂ .|. c₂)) ^2 ) + ((sqrt (c₃ .|. c₃)) ^2 ) by E10, SQUARE_1:def 4
.= (||.c₂.|| ^2 ) + ((sqrt (c₃ .|. c₃)) ^2 ) by BHSP_1:def 4
.= (||.c₂.|| ^2 ) + (||.c₃.|| ^2 ) by BHSP_1:def 4 ;
hence ||.(c₂ + c₃).|| ^2 = (||.c₂.|| ^2 ) + (||.c₃.|| ^2 ) ;

end;

proof

let c₁ be RealUnitarySpace;
let c₂ be FinSequence of the carrier of c₁;
assume E8: ( len c₂ >= 1 & for b₁, b₂ being Nat holds
( ( b₁ in dom c₂ & b₂ in dom c₂ ) implies ( not b₁ <> b₂ or the scalar of c₁ . [(c₂ . b₁),(c₂ . b₂)] = 0 ) ) ) ;
then E9: 1 in dom c₂ by FINSEQ_3:27;
let c₃ be FinSequence of REAL ;
assume E10: ( dom c₂ = dom c₃ & for b₁ being Nat holds
( b₁ in dom c₃ implies c₃ . b₁ = the scalar of c₁ . [(c₂ . b₁),(c₂ . b₁)] ) ) ;
consider c₄ being Function of NAT ,the carrier of c₁ such that
E11: c₄ . 1 = c₂ . 1
and E12: for b₁ being