:: BHSP_5 semantic presentation

theorem E1: :: BHSP_5:1
for b1 being set
for b2, b3 being FinSequence of b1 holds
( ( b2 is one-to-one & b3 is one-to-one & rng b2 = rng b3 ) implies ( ( dom b2 = dom b3 & ex b4 being Permutation of dom b2 st
( b3 = b2 * b4 & dom b4 = dom b2 & rng b4 = dom b2 ) ) ) )
proof
let c1 be set ;
let c2, c3 be FinSequence of c1;
assume that
E2: c2 is one-to-one and
E3: c3 is one-to-one and
E4: rng c2 = rng c3 ;
set c4 = (c2 " ) * c3;
E5: dom c3 = dom c2
proof
len c2 = card (rng c3) by E2, E4, FINSEQ_4:77
.= len c3 by E3, FINSEQ_4:77 ;
then dom c2 = Seg (len c3) by FINSEQ_1:def 3
.= dom c3 by FINSEQ_1:def 3 ;
hence dom c3 = dom c2 ;
end;
E6: ( dom ((c2 " ) * c3) = dom c2 & rng ((c2 " ) * c3) = dom c2 )
proof
E7: now
let c5 be set ;
( dom (c2 " ) = rng c2 & rng (c2 " ) = dom c2 ) by E2, FUNCT_1:55;
then ( c5 in dom c3 implies c3 . c5 in dom (c2 " ) ) by E4, FUNCT_1:12;
hence ( c5 in dom ((c2 " ) * c3) iff c5 in dom c3 ) by FUNCT_1:21;
end;
then E8: dom ((c2 " ) * c3) = dom c3 by TARSKI:2;
E9: ( dom (c2 " ) = rng c2 & rng (c2 " ) = dom c2 ) by E2, FUNCT_1:55;
E10: rng ((c2 " ) * c3) c= dom c2
proof
let c5 be set ; :: according to TARSKI:def 3
assume c5 in rng ((c2 " ) * c3) ;
hence c5 in dom c2 by E9, FUNCT_1:25;
end;
dom c2 c= rng ((c2 " ) * c3)
proof
let c5 be set ; :: according to TARSKI:def 3
assume c5 in dom c2 ;
then c5 in rng (c2 " ) by E2, FUNCT_1:55;
then consider c6 being set such that
E11: c6 in dom (c2 " ) and
E12: c5 = (c2 " ) . c6 by FUNCT_1:def 5;
c6 in rng c3 by E2, E4, E11, FUNCT_1:55;
then consider c7 being set such that
E13: c7 in dom c3 and
E14: c6 = c3 . c7 by FUNCT_1:def 5;
c5 = ((c2 " ) * c3) . c7 by E12, E13, E14, FUNCT_1:23;
hence c5 in rng ((c2 " ) * c3) by E8, E13, FUNCT_1:def 5;
end;
hence ( dom ((c2 " ) * c3) = dom c2 & rng ((c2 " ) * c3) = dom c2 ) by E5, E7, E10, TARSKI:2, XBOOLE_0:def 10;
end;
c2 " is one-to-one by E2, FUNCT_1:62;
then ( (c2 " ) * c3 is one-to-one & rng ((c2 " ) * c3) = dom c2 ) by E3, E6, FUNCT_1:46;
then E7: (c2 " ) * c3 is Permutation of dom c2 by E6, FUNCT_2:3, FUNCT_2:83;
now
let c5 be set ;
( c5 in dom ((c2 " ) * c3) implies ((c2 " ) * c3) . c5 in dom c2 ) by E6, FUNCT_1:12;
hence ( c5 in dom (c2 * ((c2 " ) * c3)) iff c5 in dom c2 ) by E6, FUNCT_1:21;
end;
then E8: dom c3 = dom (c2 * ((c2 " ) * c3)) by E5, TARSKI:2;
for b1 being set holds
( b1 in dom c3 implies c3 . b1 = (c2 * ((c2 " ) * c3)) . b1 )
proof
let c5 be set ;
assume E9: c5 in dom c3 ;
then E10: c3 . c5 in rng c2 by E4, FUNCT_1:12;
(c2 * ((c2 " ) * c3)) . c5 = c2 . (((c2 " ) * c3) . c5) by E5, E6, E9, FUNCT_1:23
.= c2 . ((c2 " ) . (c3 . c5)) by E9, FUNCT_1:23
.= c3 . c5 by E2, E10, FUNCT_1:57 ;
hence c3 . c5 = (c2 * ((c2 " ) * c3)) . c5 ;
end;
then c3 = c2 * ((c2 " ) * c3) by E8, FUNCT_1:9;
hence ( dom c2 = dom c3 & ex b1 being Permutation of dom c2 st
( c3 = c2 * b1 & dom b1 = dom c2 & rng b1 = dom c2 ) ) by E5, E6, E7;
end;

definition
let c1 be non empty set ;
let c2 be BinOp of c1;
assume E2: ( c2 is commutative & c2 is associative & c2 has_a_unity ) ;
let c3 be finite Subset of c1;
func c2 ++ c3 -> Element of a1 means :: BHSP_5:def 1
ex b1 being FinSequence of a1 st
( b1 is one-to-one & rng b1 = a3 & a4 = a2 "**" b1 );
existence
ex b1 being Element of c1ex b2 being FinSequence of c1 st
( b2 is one-to-one & rng b2 = c3 & b1 = c2 "**" b2 )
proof
consider c4 being FinSequence such that
E3: rng c4 = c3 and
E4: c4 is one-to-one by FINSEQ_4:73;
reconsider c5 = c4 as FinSequence of c1 by E3, FINSEQ_1:def 4;
ex b1 being FinSequence of c1 st
( b1 is one-to-one & rng b1 = c3 & c2 "**" c5 = c2 "**" b1 ) by E3, E4;
hence ex b1 being Element of c1ex b2 being FinSequence of c1 st
( b2 is one-to-one & rng b2 = c3 & b1 = c2 "**" b2 ) ;
end;
uniqueness
for b1, b2 being Element of c1 holds
( ( ) implies ( ( for b3 being FinSequence of c1 holds
not ( b3 is one-to-one & rng b3 = c3 & b1 = c2 "**" b3 ) ) or ( for b3 being FinSequence of c1 holds
not ( b3 is one-to-one & rng b3 = c3 & b2 = c2 "**" b3 ) ) or b1 = b2 ) )
proof
let c4, c5 be Element of c1;
assume that
E3: ex b1 being FinSequence of c1 st
( b1 is one-to-one & rng b1 = c3 & c4 = c2 "**" b1 ) and
E4: ex b1 being FinSequence of c1 st
( b1 is one-to-one & rng b1 = c3 & c5 = c2 "**" b1 ) ;
consider c6 being FinSequence of c1 such that
E5: c6 is one-to-one and
E6: rng c6 = c3 and
E7: c4 = c2 "**" c6 by E3;
consider c7 being FinSequence of c1 such that
E8: c7 is one-to-one and
E9: rng c7 = c3 and
E10: c5 = c2 "**" c7 by E4;
( dom c6 = dom c7 & ex b1 being Permutation of dom c6 st
( c7 = c6 * b1 & dom b1 = dom c6 & rng b1 = dom c6 ) ) by E5, E6, E8, E9, E1;
then consider c8 being Permutation of dom c6 such that
E11: c7 = c6 * c8 ;
thus c4 = c5 by E2, E7, E10, E11, FINSOP_1:8;
end;
end;

:: deftheorem defines ++ BHSP_5:def 1 :
for b1 being non empty set
for b2 being BinOp of b1 holds
( ( b2 is commutative & b2 is associative & b2 has_a_unity ) implies ( ( for b3 being finite Subset of b1
for b4 being Element of b1 holds
( b4 = b2 ++ b3 iff ex b5 being FinSequence of b1 st
( b5 is one-to-one & rng b5 = b3 & b4 = b2 "**" b5 ) ) ) ) );

definition
let c1 be RealUnitarySpace;
let c2 be finite Subset of c1;
func setop_SUM c2,c1 -> set equals :: BHSP_5:def 2
the add of a1 ++ a2 if a2 <> {}
otherwise 0. a1;
correctness
coherence
( ( c2 <> {} implies the add of c1 ++ c2 is set ) & ( not c2 <> {} implies 0. c1 is set ) );
consistency
for b1 being set holds
verum;
;
end;

:: deftheorem defines setop_SUM BHSP_5:def 2 :
for b1 being RealUnitarySpace
for b2 being finite Subset of b1 holds
( ( b2 <> {} implies setop_SUM b2,b1 = the add of b1 ++ b2 ) & ( not b2 <> {} implies setop_SUM b2,b1 = 0. b1 ) );

definition
let c1 be RealUnitarySpace;
let c2 be Point of c1;
let c3 be FinSequence;
let c4 be Nat;
func PO c4,c3,c2 -> set equals :: BHSP_5:def 3
the scalar of a1 . [a2,(a3 . a4)];
correctness
coherence
the scalar of c1 . [c2,(c3 . c4)] is set ;
;
end;

:: deftheorem defines PO BHSP_5:def 3 :
for b1 being RealUnitarySpace
for b2 being Point of b1
for b3 being FinSequence
for b4 being Nat holds PO b4,b3,b2 = the scalar of b1 . [b2,(b3 . b4)];

definition
let c1, c2 be non empty set ;
let c3 be Function of c2,c1;
let c4 be FinSequence of c2;
func Func_Seq c3,c4 -> FinSequence of a1 equals :: BHSP_5:def 4
a3 * a4;
correctness
coherence
c3 * c4 is FinSequence of c1;
by FINSEQ_2:36;
end;

:: deftheorem defines Func_Seq BHSP_5:def 4 :
for b1, b2 being non empty set
for b3 being Function of b2,b1
for b4 being FinSequence of b2 holds Func_Seq b3,b4 = b3 * b4;

definition
let c1, c2 be non empty set ;
let c3 be BinOp of c1;
assume E2: ( c3 is commutative & c3 is associative & c3 has_a_unity ) ;
let c4 be finite Subset of c2;
let c5 be Function of c2,c1;
assume E3: c4 c= dom c5 ;
func setopfunc c4,c2,c1,c5,c3 -> Element of a1 means :E2: :: BHSP_5:def 5
ex b1 being FinSequence of a2 st
( b1 is one-to-one & rng b1 = a4 & a6 = a3 "**" (Func_Seq a5,b1) );
existence
ex b1 being Element of c1ex b2 being FinSequence of c2 st
( b2 is one-to-one & rng b2 = c4 & b1 = c3 "**" (Func_Seq c5,b2) )
proof
consider c6 being FinSequence such that
E4: rng c6 = c4 and
E5: c6 is one-to-one by FINSEQ_4:73;
reconsider c7 = c6 as FinSequence of c2 by E4, FINSEQ_1:def 4;
ex b1 being FinSequence of c2 st
( b1 is one-to-one & rng b1 = c4 & c3 "**" (Func_Seq c5,c7) = c3 "**" (Func_Seq c5,b1) ) by E4, E5;
hence ex b1 being Element of c1ex b2 being FinSequence of c2 st
( b2 is one-to-one & rng b2 = c4 & b1 = c3 "**" (Func_Seq c5,b2) ) ;
end;
uniqueness
for b1, b2 being Element of c1 holds
( ( ) implies ( ( for b3 being FinSequence of c2 holds
not ( b3 is one-to-one & rng b3 = c4 & b1 = c3 "**" (Func_Seq c5,b3) ) ) or ( for b3 being FinSequence of c2 holds
not ( b3 is one-to-one & rng b3 = c4 & b2 = c3 "**" (Func_Seq c5,b3) ) ) or b1 = b2 ) )
proof
let c6, c7 be Element of c1;
assume that
E4: ex b1 being FinSequence of c2 st
( b1 is one-to-one & rng b1 = c4 & c6 = c3 "**" (Func_Seq c5,b1) ) and
E5: ex b1 being FinSequence of c2 st
( b1 is one-to-one & rng b1 = c4 & c7 = c3 "**" (Func_Seq c5,b1) ) ;
consider c8 being FinSequence of c2 such that
E6: c8 is one-to-one and
E7: rng c8 = c4 and
E8: c6 = c3 "**" (Func_Seq c5,c8) by E4;
consider c9 being FinSequence of c2 such that
E9: c9 is one-to-one and
E10: rng c9 = c4 and
E11: c7 = c3 "**" (Func_Seq c5,c9) by E5;
E12: ( dom c8 = dom c9 & ex b1 being Permutation of dom c8 st
( c9 = c8 * b1 & dom b1 = dom c8 & rng b1 = dom c8 ) ) by E6, E7, E9, E10, E1;
consider c10 being Permutation of dom c8 such that
E13: c9 = c8 * c10 and
dom c10 = dom c8 and
rng c10 = dom c8 by E6, E7, E9, E10, E1;
now
let c11 be set ;
( c11 in dom c8 implies c8 . c11 in rng c8 ) by FUNCT_1:12;
hence ( c11 in dom (Func_Seq c5,c8) iff c11 in dom c8 ) by E3, E7, FUNCT_1:21;
end;
then E14: dom (Func_Seq c5,c8) = dom c8 by TARSKI:2;
now
let c11 be set ;
( c11 in dom c9 implies c9 . c11 in rng c9 ) by FUNCT_1:12;
hence ( c11 in dom (Func_Seq c5,c9) iff c11 in dom c9 ) by E3, E10, FUNCT_1:21;
end;
then E15: dom (Func_Seq c5,c9) = dom c9 by TARSKI:2;
E16: ( dom c10 = dom (Func_Seq c5,c8) & rng c10 = dom (Func_Seq c5,c8) ) by E14, FUNCT_2:67, FUNCT_2:def 3;
Func_Seq c5,c9 = (Func_Seq c5,c8) * c10
proof
now
let c11 be set ;
( c11 in dom c10 implies c10 . c11 in dom (Func_Seq c5,c8) ) by E16, FUNCT_1:12;
then ( c11 in dom ((Func_Seq c5,c8) * c10) iff c11 in dom c10 ) by FUNCT_1:21;
hence ( c11 in dom ((Func_Seq c5,c8) * c10) iff c11 in dom (Func_Seq c5,c9) ) by E12, E15, FUNCT_2:67;
end;
then E17: dom (Func_Seq c5,c9) = dom ((Func_Seq c5,c8) * c10) by TARSKI:2;
now
let c11 be set ;
assume E18: c11 in dom (Func_Seq c5,c9) ;
E19: dom (Func_Seq c5,c9) is Subset of NAT by RELSET_1:12;
then reconsider c12 = c11 as Nat by E18;
c12 in dom c10 by E12, E15, E18, FUNCT_2:67;
then E20: c10 . c12 in rng c10 by FUNCT_1:12;
then c10 . c12 in dom (Func_Seq c5,c9) by E12, E15, FUNCT_2:def 3;
then reconsider c13 = c10 . c12 as Nat by E19;
E21: c13 in dom c8 by E20, FUNCT_2:def 3;
E22: c11 in dom c10 by E12, E15, E18, FUNCT_2:67;
(Func_Seq c5,c9) . c11 = (c5 * c9) . c12
.= c5 . (c9 . c12) by E15, E18, FUNCT_1:23
.= c5 . (c8 . (c10 . c12)) by E13, E22, FUNCT_1:23
.= (c5 * c8) . c13 by E21, FUNCT_1:23
.= (Func_Seq c5,c8) . c13
.= ((Func_Seq c5,c8) * c10) . c11 by E22, FUNCT_1:23 ;
hence (Func_Seq c5,c9) . c11 = ((Func_Seq c5,c8) * c10) . c11 ;
end;
hence Func_Seq c5,c9 = (Func_Seq c5,c8) * c10 by E17, FUNCT_1:9;
end;
hence c6 = c7 by E2, E8, E11, E14, FINSOP_1:8;
end;
end;

:: deftheorem E2 defines setopfunc BHSP_5:def 5 :
for b1, b2 being non empty set
for b3 being BinOp of b1 holds
( ( b3 is commutative & b3 is associative & b3 has_a_unity ) implies ( ( for b4 being finite Subset of b2
for b5 being Function of b2,b1 holds
( b4 c= dom b5 implies for b6 being Element of b1 holds
( b6 = setopfunc b4,b2,b1,b5,b3 iff ex b7 being FinSequence of b2 st
( b7 is one-to-one & rng b7 = b4 & b6 = b3 "**" (Func_Seq b5,b7) ) ) ) ) ) );

definition
let c1 be RealUnitarySpace;
let c2 be Point of c1;
let c3 be finite Subset of c1;
func setop_xPre_PROD c2,c3,c1 -> Real means :: BHSP_5:def 6
ex b1 being FinSequence of the carrier of a1 st
( b1 is one-to-one & rng b1 = a3 & ex b2 being FinSequence of REAL st
( dom b2 = dom b1 & ( for b3 being Nat holds
( b3 in dom b2 implies b2 . b3 = PO b3,b1,a2 ) ) & a4 = addreal "**" b2 ) );
existence
ex b1 being Realex b2 being FinSequence of the carrier of c1 st
( b2 is one-to-one & rng b2 = c3 & ex b3 being FinSequence of REAL st
( dom b3 = dom b2 & ( for b4 being Nat holds
( b4 in dom b3 implies b3 . b4 = PO b4,b2,c2 ) ) & b1 = addreal "**" b3 ) )
proof
consider c4 being FinSequence such that
E3: rng c4 = c3 and
E4: c4 is one-to-one by FINSEQ_4:73;
reconsider c5 = c4 as FinSequence of the carrier of c1 by E3, FINSEQ_1:def 4;
set c6 = len c5;
deffunc H1( Nat) -> set = PO a1,c5,c2;
ex b1 being FinSequence st
( len b1 = len c5 & ( for b2 being Nat holds
( b2 in Seg (len c5) implies b1 . b2 = H1(b2) ) ) ) from FINSEQ_1:sch 2();
 then consider c7 being FinSequence such that
E5: ( len c7 = len c5 & ( for b1 being Nat holds
( b1 in Seg (len c5) implies c7 . b1 = PO b1,c5,c2 ) ) ) ;
E6: dom c7 = Seg (len c5) by E5, FINSEQ_1:def 3;
then E7: dom c7 = dom c5 by FINSEQ_1:def 3;
now
let c8 be Nat;
assume E8: c8 in dom c7 ;
then E9: c7 . c8 = PO c8,c5,c2 by E5, E6
.= the scalar of c1 . [c2,(c5 . c8)] ;
reconsider c9 = c5 . c8 as Point of c1 by E7, E8, FINSEQ_2:13;
the scalar of c1 . [c2,(c5 . c8)] = c2 .|. c9 by BHSP_1:def 1;
hence c7 . c8 in REAL by E9;
end;
then reconsider c8 = c7 as FinSequence of REAL by FINSEQ_2:14;
take addreal "**" c8 ;
thus ex b1 being FinSequence of the carrier of c1 st
( b1 is one-to-one & rng b1 = c3 & ex b2 being FinSequence of REAL st
( dom b2 = dom b1 & ( for b3 being Nat holds
( b3 in dom b2 implies b2 . b3 = PO b3,b1,c2 ) ) & addreal "**" c8 = addreal "**" b2 ) ) by E3, E4, E5, E6, E7;
end;
uniqueness
for b1, b2 being Real holds
( ( ) implies ( ( for b3 being FinSequence of the carrier of c1 holds
not ( b3 is one-to-one & rng b3 = c3 & ex b4 being FinSequence of REAL st
( dom b4 = dom b3 & ( for b5 being Nat holds
( b5 in dom b4 implies b4 . b5 = PO b5,b3,c2 ) ) & b1 = addreal "**" b4 ) ) ) or ( for b3 being FinSequence of the carrier of c1 holds
not ( b3 is one-to-one & rng b3 = c3 & ex b4 being FinSequence of REAL st
( dom b4 = dom b3 & ( for b5 being Nat holds
( b5 in dom b4 implies b4 . b5 = PO b5,b3,c2 ) ) & b2 = addreal "**" b4 ) ) ) or b1 = b2 ) )
proof
let c4, c5 be Element of REAL ;
assume that
E3: ex b1 being FinSequence of the carrier of c1 st
( b1 is one-to-one & rng b1 = c3 & ex b2 being FinSequence of REAL st
( dom b2 = dom b1 & ( for b3 being Nat holds
( b3 in dom b2 implies b2 . b3 = PO b3,b1,c2 ) ) & c4 = addreal "**" b2 ) ) and
E4: ex b1 being FinSequence of the carrier of c1 st
( b1 is one-to-one & rng b1 = c3 & ex b2 being FinSequence of REAL st
( dom b2 = dom b1 & ( for b3 being Nat holds
( b3 in dom b2 implies b2 . b3 = PO b3,b1,c2 ) ) & c5 = addreal "**" b2 ) ) ;
consider c6 being FinSequence of the carrier of c1 such that
E5: c6 is one-to-one and
E6: rng c6 = c3 and
E7: ex b1 being FinSequence of REAL st
( dom b1 = dom c6 & ( for b2 being Nat holds
( b2 in dom b1 implies b1 . b2 = PO b2,c6,c2 ) ) & c4 = addreal "**" b1 ) by E3;
consider c7 being FinSequence of the carrier of c1 such that
E8: c7 is one-to-one and
E9: rng c7 = c3 and
E10: ex b1 being FinSequence of REAL st
( dom b1 = dom c7 & ( for b2 being Nat holds
( b2 in dom b1 implies b1 . b2 = PO b2,c7,c2 ) ) & c5 = addreal "**" b1 ) by E4;
consider c8 being FinSequence of REAL such that
E11: dom c8 = dom c6 and
E12: for b1 being Nat holds
( b1 in dom c8 implies c8 . b1 = PO b1,c6,c2 ) and
E13: c4 = addreal "**" c8 by E7;
consider c9 being FinSequence of REAL such that
E14: dom c9 = dom c7 and
E15: for b1 being Nat holds
( b1 in dom c9 implies c9 . b1 = PO b1,c7,c2 ) and
E16: c5 = addreal "**" c9 by E10;
E17: ( dom c6 = dom c7 & ex b1 being Permutation of dom c6 st
( c7 = c6 * b1 & dom b1 = dom c6 & rng b1 = dom c6 ) ) by E5, E6, E8, E9, E1;
consider c10 being Permutation of dom c6 such that
E18: c7 = c6 * c10 and
dom c10 = dom c6 and
rng c10 = dom c6 by E5, E6, E8, E9, E1;
E19: ( dom c10 = dom c8 & rng c10 = dom c8 ) by E11, FUNCT_2:67, FUNCT_2:def 3;
E20: ( dom c10 = dom c9 & rng c10 = dom c9 ) by E14, E17, FUNCT_2:67, FUNCT_2:def 3;
E21: dom c6 = dom c9 by E5, E6, E8, E9, E14, E1;
now
let c11 be set ;
( c11 in dom c10 implies c10 . c11 in dom c8 ) by E19, FUNCT_1:12;
hence ( c11 in dom (c8 * c10) iff c11 in dom c9 ) by E20, FUNCT_1:21;
end;
then E22: dom c9 = dom (c8 * c10) by TARSKI:2;
c9 = c8 * c10
proof
E23: dom c9 is Subset of NAT by RELSET_1:12;
now
let c11 be set ;
assume E24: c11 in dom c9 ;
then reconsider c12 = c11 as Nat by E23;
c10 . c12 in dom c9 by E20, E24, FUNCT_1:12;
then reconsider c13 = c10 . c12 as Nat by E23;
E25: c13 in dom c8 by E11, E20, E21, E24, FUNCT_1:12;
E26: c11 in dom c10 by E14, E17, E24, FUNCT_2:67;
c9 . c11 = PO c12,c7,c2 by E15, E24
.= the scalar of c1 . [c2,((c6 * c10) . c12)] by E18
.= the scalar of c1 . [c2,(c6 . c13)] by E26, FUNCT_1:23
.= PO c13,c6,c2
.= c8 . (c10 . c12) by E12, E25
.= (c8 * c10) . c11 by E26, FUNCT_1:23 ;
hence c9 . c11 = (c8 * c10) . c11 ;
end;
hence c9 = c8 * c10 by E22, FUNCT_1:9;
end;
hence c4 = c5 by E11, E13, E16, FINSOP_1:8;
end;
end;

:: deftheorem defines setop_xPre_PROD BHSP_5:def 6 :
for b1 being RealUnitarySpace
for b2 being Point of b1
for b3 being finite Subset of b1
for b4 being Real holds
( b4 = setop_xPre_PROD b2,b3,b1 iff ex b5 being FinSequence of the carrier of b1 st
( b5 is one-to-one & rng b5 = b3 & ex b6 being FinSequence of REAL st
( dom b6 = dom b5 & ( for b7 being Nat holds
( b7 in dom b6 implies b6 . b7 = PO b7,b5,b2 ) ) & b4 = addreal "**" b6 ) ) );

definition
let c1 be RealUnitarySpace;
let c2 be Point of c1;
let c3 be finite Subset of c1;
func setop_xPROD c2,c3,c1 -> Real equals :: BHSP_5:def 7
 setop_xPre_PROD a2,a3,a1 if a3 <> {}
otherwise 0;
correctness
coherence
( ( c3 <> {} implies setop_xPre_PROD c2,c3,c1 is Real ) & ( not c3 <> {} implies 0 is Real ) );
consistency
for b1 being Real holds
verum;
;
end;

:: deftheorem defines setop_xPROD BHSP_5:def 7 :
for b1 being RealUnitarySpace
for b2 being Point of b1
for b3 being finite Subset of b1 holds
( ( b3 <> {} implies setop_xPROD b2,b3,b1 = setop_xPre_PROD b2,b3,b1 ) & ( not b3 <> {} implies setop_xPROD b2,b3,b1 = 0 ) );

definition
let c1 be RealUnitarySpace;
mode OrthogonalFamily of c1 -> Subset of a1 means :E3: :: BHSP_5:def 8
for b1, b2 being Point of a1 holds
( ( b1 in a2 & b2 in a2 ) implies ( not b1 <> b2 or b1 .|. b2 = 0 ) );
existence
ex b1 being Subset of c1 st
for b2, b3 being Point of c1 holds
( ( b2 in b1 & b3 in b1 ) implies ( not b2 <> b3 or b2 .|. b3 = 0 ) )
proof
take {} ;
thus ( {} is Subset of c1 & ( for b1, b2 being Point of c1 holds
( ( b1 in {} & b2 in {} ) implies ( not b1 <> b2 or b1 .|. b2 = 0 ) ) ) ) by SUBSET_1:4;
end;
end;

:: deftheorem E3 defines OrthogonalFamily BHSP_5:def 8 :
for b1 being RealUnitarySpace
for b2 being Subset of b1 holds
( b2 is OrthogonalFamily of b1 iff for b3, b4 being Point of b1 holds
( ( b3 in b2 & b4 in b2 ) implies ( not b3 <> b4 or b3 .|. b4 = 0 ) ) );

theorem E4: :: BHSP_5:2
for b1 being RealUnitarySpace holds
{} is OrthogonalFamily of b1
proof
let c1 be RealUnitarySpace;
E5: {} is Subset of c1 by SUBSET_1:4;
for b1, b2 being Point of c1 holds
( ( b1 in {} & b2 in {} ) implies ( not b1 <> b2 or b1 .|. b2 = 0 ) ) ;
hence {} is OrthogonalFamily of c1 by E5, E3;
end;

registration
let c1 be RealUnitarySpace;
cluster finite OrthogonalFamily of a1;
existence
ex b1 being OrthogonalFamily of c1 st b1 is finite
proof
take {} ;
thus ( {} is Subset of c1 & {} is OrthogonalFamily of c1 & {} is finite ) by E4;
end;
end;

definition
let c1 be RealUnitarySpace;
mode OrthonormalFamily of c1 -> Subset of a1 means :E5: :: BHSP_5:def 9
( a2 is OrthogonalFamily of a1 & ( for b1 being Point of a1 holds
( b1 in a2 implies b1 .|. b1 = 1 ) ) );
existence
ex b1 being Subset of c1 st
( b1 is OrthogonalFamily of c1 & ( for b2 being Point of c1 holds
( b2 in b1 implies b2 .|. b2 = 1 ) ) )
proof
take {} ;
thus ( {} is Subset of c1 & {} is OrthogonalFamily of c1 & ( for b1 being Point of c1 holds
( b1 in {} implies b1 .|. b1 = 1 ) ) ) by E4;
end;
end;

:: deftheorem E5 defines OrthonormalFamily BHSP_5:def 9 :
for b1 being RealUnitarySpace
for b2 being Subset of b1 holds
( b2 is OrthonormalFamily of b1 iff ( b2 is OrthogonalFamily of b1 & ( for b3 being Point of b1 holds
( b3 in b2 implies b3 .|. b3 = 1 ) ) ) );

theorem E6: :: BHSP_5:3
for b1 being RealUnitarySpace holds
{} is OrthonormalFamily of b1
proof
let c1 be RealUnitarySpace;
E7: {} is OrthogonalFamily of c1 by E4;
for b1 being Point of c1 holds
( b1 in {} implies b1 .|. b1 = 1 ) ;
hence {} is OrthonormalFamily of c1 by E7, E5;
end;

registration
let c1 be RealUnitarySpace;
cluster finite OrthonormalFamily of a1;
existence
ex b1 being OrthonormalFamily of c1 st b1 is finite
proof
take {} ;
thus ( {} is Subset of c1 & {} is OrthonormalFamily of c1 & {} is finite ) by E6;
end;
end;

theorem :: BHSP_5:4
for b1 being RealUnitarySpace
for b2 being Point of b1 holds
( b2 = 0. b1 iff for b3 being Point of b1 holds b2 .|. b3 = 0 )
proof
let c1 be RealUnitarySpace;
let c2 be Point of c1;
( ( for b1 being Point of c1 holds c2 .|. b1 = 0 ) implies c2 = 0. c1 )
proof
now
assume for b1 being Point of c1 holds c2 .|. b1 = 0 ;
then c2 .|. c2 = 0 ;
hence c2 = 0. c1 by BHSP_1:def 2;
end;
hence ( ( for b1 being Point of c1 holds c2 .|. b1 = 0 ) implies c2 = 0. c1 ) ;
end;
hence ( c2 = 0. c1 iff for b1 being Point of c1 holds c2 .|. b1 = 0 ) by BHSP_1:19;
end;

theorem :: BHSP_5:5
for b1 being RealUnitarySpace
for b2, b3 being Point of b1 holds (||.(b2 + b3).|| ^2 ) + (||.(b2 - b3).|| ^2 ) = (2 * (||.b2.|| ^2 )) + (2 * (||.b3.|| ^2 ))
proof
let c1 be RealUnitarySpace;
let c2, c3 be Point of c1;
E7: (c2 + c3) .|. (c2 + c3) >= 0 by BHSP_1:def 2;
E8: (c2 - c3) .|. (c2 - c3) >= 0 by BHSP_1:def 2;
E9: c2 .|. c2 >= 0 by BHSP_1:def 2;
E10: c3 .|. c3 >= 0 by BHSP_1:def 2;
(||.(c2 + c3).|| ^2 ) + (||.(c2 - c3).|| ^2 ) = ((sqrt ((c2 + c3) .|. (c2 + c3))) ^2 ) + (||.(c2 - c3).|| ^2 ) by BHSP_1:def 4
.= ((c2 + c3) .|. (c2 + c3)) + (||.(c2 - c3).|| ^2 ) by E7, SQUARE_1:def 4
.= ((c2 + c3) .|. (c2 + c3)) + ((sqrt ((c2 - c3) .|. (c2 - c3))) ^2 ) by BHSP_1:def 4
.= ((c2 + c3) .|. (c2 + c3)) + ((c2 - c3) .|. (c2 - c3)) by E8, SQUARE_1:def 4
.= (((c2 .|. c2) + (2 * (c2 .|. c3))) + (c3 .|. c3)) + ((c2 - c3) .|. (c2 - c3)) by BHSP_1:21
.= (((c2 .|. c2) + (2 * (c2 .|. c3))) + (c3 .|. c3)) + (((c2 .|. c2) - (2 * (c2 .|. c3))) + (c3 .|. c3)) by BHSP_1:23
.= (2 * (c2 .|. c2)) + (2 * (c3 .|. c3))
.= (2 * ((sqrt (c2 .|. c2)) ^2 )) + (2 * (c3 .|. c3)) by E9, SQUARE_1:def 4
.= (2 * ((sqrt (c2 .|. c2)) ^2 )) + (2 * ((sqrt (c3 .|. c3)) ^2 )) by E10, SQUARE_1:def 4
.= (2 * (||.c2.|| ^2 )) + (2 * ((sqrt (c3 .|. c3)) ^2 )) by BHSP_1:def 4
.= (2 * (||.c2.|| ^2 )) + (2 * (||.c3.|| ^2 )) by BHSP_1:def 4 ;
hence (||.(c2 + c3).|| ^2 ) + (||.(c2 - c3).|| ^2 ) = (2 * (||.c2.|| ^2 )) + (2 * (||.c3.|| ^2 )) ;
end;

theorem :: BHSP_5:6
for b1 being RealUnitarySpace
for b2, b3 being Point of b1 holds
( b2,b3 are_orthogonal implies ||.(b2 + b3).|| ^2 = (||.b2.|| ^2 ) + (||.b3.|| ^2 ) )
proof
let c1 be RealUnitarySpace;
let c2, c3 be Point of c1;
assume c2,c3 are_orthogonal ;
then E7: c2 .|. c3 = 0 by BHSP_1:def 3;
E8: (c2 + c3) .|. (c2 + c3) >= 0 by BHSP_1:def 2;
E9: c2 .|. c2 >= 0 by BHSP_1:def 2;
E10: c3 .|. c3 >= 0 by BHSP_1:def 2;
||.(c2 + c3).|| ^2 = (sqrt ((c2 + c3) .|. (c2 + c3))) ^2 by BHSP_1:def 4
.= (c2 + c3) .|. (c2 + c3) by E8, SQUARE_1:def 4
.= ((c2 .|. c2) + (2 * (c2 .|. c3))) + (c3 .|. c3) by BHSP_1:21
.= ((sqrt (c2 .|. c2)) ^2 ) + (c3 .|. c3) by E7, E9, SQUARE_1:def 4
.= ((sqrt (c2 .|. c2)) ^2 ) + ((sqrt (c3 .|. c3)) ^2 ) by E10, SQUARE_1:def 4
.= (||.c2.|| ^2 ) + ((sqrt (c3 .|. c3)) ^2 ) by BHSP_1:def 4
.= (||.c2.|| ^2 ) + (||.c3.|| ^2 ) by BHSP_1:def 4 ;
hence ||.(c2 + c3).|| ^2 = (||.c2.|| ^2 ) + (||.c3.|| ^2 ) ;
end;

theorem E7: :: BHSP_5:7
for b1 being RealUnitarySpace
for b2 being FinSequence of the carrier of b1 holds
( ( len b2 >= 1 & ( for b3, b4 being Nat holds
( ( b3 in dom b2 & b4 in dom b2 ) implies ( not b3 <> b4 or the scalar of b1 . [(b2 . b3),(b2 . b4)] = 0 ) ) ) ) implies ( ( for b3 being FinSequence of REAL holds
( ( dom b2 = dom b3 & ( for b4 being Nat holds
( b4 in dom b3 implies b3 . b4 = the scalar of b1 . [(b2 . b4),(b2 . b4)] ) ) ) implies ( (the add of b1 "**" b2) .|. (the add of b1 "**" b2) = addreal "**" b3 ) ) ) ) )
proof
let c1 be RealUnitarySpace;
let c2 be FinSequence of the carrier of c1;
assume E8: ( len c2 >= 1 & ( for b1, b2 being Nat holds
( ( b1 in dom c2 & b2 in dom c2 ) implies ( not b1 <> b2 or the scalar of c1 .