:: BHSP_5 semantic presentation

begin


theorem Th1: :: BHSP_5:1
for D being set
for p1, p2 being FinSequence of D st p1 is one-to-one & p2 is one-to-one & rng p1 = rng p2 holds
( dom p1 = dom p2 & ex P being Permutation of (dom p1) st
( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) )
proof
let D be set ; ::_thesis: for p1, p2 being FinSequence of D st p1 is one-to-one & p2 is one-to-one & rng p1 = rng p2 holds
( dom p1 = dom p2 & ex P being Permutation of (dom p1) st
( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) )
let p1, p2 be FinSequence of D; ::_thesis: ( p1 is one-to-one & p2 is one-to-one & rng p1 = rng p2 implies ( dom p1 = dom p2 & ex P being Permutation of (dom p1) st
( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) ) )
assume that
A1: p1 is one-to-one and
A2: p2 is one-to-one and
A3: rng p1 = rng p2 ; ::_thesis: ( dom p1 = dom p2 & ex P being Permutation of (dom p1) st
( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) )
set P = (p1 ") * p2;
len p1 = card (rng p2) by A1, A3, FINSEQ_4:62
.= len p2 by A2, FINSEQ_4:62 ;
then A4: dom p1 = Seg (len p2) by FINSEQ_1:def_3
.= dom p2 by FINSEQ_1:def_3 ;
A5: now__::_thesis:_for_xd_being_set_holds_
(_xd_in_dom_((p1_")_*_p2)_iff_xd_in_dom_p2_)
let xd be set ; ::_thesis: ( xd in dom ((p1 ") * p2) iff xd in dom p2 )
 dom (p1 ") = rng p1 by A1, FUNCT_1:33;
then  ( xd in dom p2 implies p2 . xd in dom (p1 ") ) by A3, FUNCT_1:3;
hence  ( xd in dom ((p1 ") * p2) iff xd in dom p2 ) by FUNCT_1:11; ::_thesis: verum
end;
then A6: dom ((p1 ") * p2) = dom p2 by TARSKI:1;
A7: rng (p1 ") = dom p1 by A1, FUNCT_1:33;
A8: rng ((p1 ") * p2) c= dom p1
proof
let xd be set ; :: according to TARSKI:def_3 ::_thesis: ( not xd in rng ((p1 ") * p2) or xd in dom p1 )
assume  xd in rng ((p1 ") * p2) ; ::_thesis: xd in dom p1
hence  xd in dom p1 by A7, FUNCT_1:14; ::_thesis: verum
end;
A9: dom p1 c= rng ((p1 ") * p2)
proof
let xd be set ; :: according to TARSKI:def_3 ::_thesis: ( not xd in dom p1 or xd in rng ((p1 ") * p2) )
assume  xd in dom p1 ; ::_thesis: xd in rng ((p1 ") * p2)
then  xd in rng (p1 ") by A1, FUNCT_1:33;
then consider yd being set  such that
A10: yd in dom (p1 ") and
A11: xd = (p1 ") . yd by FUNCT_1:def_3;
 yd in rng p2 by A1, A3, A10, FUNCT_1:33;
then consider z being set  such that
A12: z in dom p2 and
A13: yd = p2 . z by FUNCT_1:def_3;
 xd = ((p1 ") * p2) . z by A11, A12, A13, FUNCT_1:13;
hence  xd in rng ((p1 ") * p2) by A6, A12, FUNCT_1:def_3; ::_thesis: verum
end;
A14: dom ((p1 ") * p2) = dom p1 by A4, A5, TARSKI:1;
A15: rng ((p1 ") * p2) = dom p1 by A8, A9, XBOOLE_0:def_10;
then  (p1 ") * p2 is Function of (dom p1),(dom p1) by A14, FUNCT_2:1;
then A16: (p1 ") * p2 is Permutation of (dom p1) by A1, A2, A15, FUNCT_2:57;
now__::_thesis:_for_xd_being_set_holds_
(_xd_in_dom_(p1_*_((p1_")_*_p2))_iff_xd_in_dom_p1_)
let xd be set ; ::_thesis: ( xd in dom (p1 * ((p1 ") * p2)) iff xd in dom p1 )
 ( xd in dom ((p1 ") * p2) implies ((p1 ") * p2) . xd in dom p1 ) by A15, FUNCT_1:3;
hence  ( xd in dom (p1 * ((p1 ") * p2)) iff xd in dom p1 ) by A14, FUNCT_1:11; ::_thesis: verum
end;
then A17: dom p2 = dom (p1 * ((p1 ") * p2)) by A4, TARSKI:1;
 for xd being set st xd in dom p2 holds
p2 . xd = (p1 * ((p1 ") * p2)) . xd
proof
let xd be set ; ::_thesis: ( xd in dom p2 implies p2 . xd = (p1 * ((p1 ") * p2)) . xd )
assume A18: xd in dom p2 ; ::_thesis: p2 . xd = (p1 * ((p1 ") * p2)) . xd
then A19: p2 . xd in rng p1 by A3, FUNCT_1:3;
(p1 * ((p1 ") * p2)) . xd = p1 . (((p1 ") * p2) . xd) by A4, A14, A18, FUNCT_1:13
.= p1 . ((p1 ") . (p2 . xd)) by A18, FUNCT_1:13
.= p2 . xd by A1, A19, FUNCT_1:35 ;
hence  p2 . xd = (p1 * ((p1 ") * p2)) . xd ; ::_thesis: verum
end;
hence  ( dom p1 = dom p2 & ex P being Permutation of (dom p1) st
( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) ) by A4, A14, A15, A16, A17, FUNCT_1:2; ::_thesis: verum
end;

definition
let DX be non empty set ;
let f be BinOp of DX;
assume that
A1: ( f is commutative & f is associative ) and
A2: f is having_a_unity ;
let Y be finite Subset of DX;
funcf ++ Y ->  Element of DX means :: BHSP_5:def 1
 ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & it = f "**" p );
existence
 ex b1 being Element of DX ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b1 = f "**" p )
proof
consider p being FinSequence such that
A1: rng p = Y and
A2: p is one-to-one by FINSEQ_4:58;
reconsider q = p as FinSequence of DX by A1, FINSEQ_1:def_4;
 ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & f "**" q = f "**" p ) by A1, A2;
hence  ex b1 being Element of DX ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b1 = f "**" p ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of DX st ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b1 = f "**" p ) & ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b2 = f "**" p ) holds
b1 = b2
proof
let X1, X2 be Element of DX; ::_thesis: ( ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & X1 = f "**" p ) & ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & X2 = f "**" p ) implies X1 = X2 )
assume that
A3: ex p1 being FinSequence of DX st
( p1 is one-to-one & rng p1 = Y & X1 = f "**" p1 ) and
A4: ex p2 being FinSequence of DX st
( p2 is one-to-one & rng p2 = Y & X2 = f "**" p2 ) ; ::_thesis: X1 = X2
consider p1 being FinSequence of DX such that
A5: p1 is one-to-one and
A6: rng p1 = Y and
A7: X1 = f "**" p1 by A3;
consider p2 being FinSequence of DX such that
A8: p2 is one-to-one and
A9: rng p2 = Y and
A10: X2 = f "**" p2 by A4;
 ex P being Permutation of (dom p1) st
( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) by A5, A6, A8, A9, Th1;
hence  X1 = X2 by A1, A2, A7, A10, FINSOP_1:7; ::_thesis: verum
end;
end;

:: deftheorem  defines ++ BHSP_5:def_1_:_
 for DX being non empty set
for f being BinOp of DX st f is commutative & f is associative & f is having_a_unity holds
for Y being finite Subset of DX
for b4 being Element of DX holds
( b4 = f ++ Y iff ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b4 = f "**" p ) );

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

:: deftheorem  defines setop_SUM BHSP_5:def_2_:_
 for X being RealUnitarySpace
for Y being finite Subset of X holds
( ( Y <> {} implies setop_SUM (Y,X) = the addF of X ++ Y ) & ( not Y <> {} implies setop_SUM (Y,X) = 0. X ) );

definition
let X be RealUnitarySpace;
let x be Point of X;
let p be FinSequence;
let i be Nat;
func PO (i,p,x) ->  set  equals :: BHSP_5:def 3
 the scalar of X . [x,(p . i)];
correctness
coherence
the scalar of X . [x,(p . i)] is set ;
;
end;

:: deftheorem  defines PO BHSP_5:def_3_:_
 for X being RealUnitarySpace
for x being Point of X
for p being FinSequence
for i being Nat holds PO (i,p,x) = the scalar of X . [x,(p . i)];

definition
let DK, DX be non empty set ;
let F be Function of DX,DK;
let p be FinSequence of DX;
func Func_Seq (F,p) ->  FinSequence of DK equals :: BHSP_5:def 4
F * p;
correctness
coherence
F * p is FinSequence of DK;
by FINSEQ_2:32;
end;

:: deftheorem  defines Func_Seq BHSP_5:def_4_:_
 for DK, DX being non empty set
for F being Function of DX,DK
for p being FinSequence of DX holds Func_Seq (F,p) = F * p;

definition
let DK, DX be non empty set ;
let f be BinOp of DK;
assume that
A1: ( f is commutative & f is associative ) and
A2: f is having_a_unity ;
let Y be finite Subset of DX;
let F be Function of DX,DK;
assume B3: Y c= dom F ;
func setopfunc (Y,DX,DK,F,f) ->  Element of DK means :Def5: :: BHSP_5:def 5
 ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & it = f "**" (Func_Seq (F,p)) );
existence
 ex b1 being Element of DK ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b1 = f "**" (Func_Seq (F,p)) )
proof
consider p being FinSequence such that
A1: rng p = Y and
A2: p is one-to-one by FINSEQ_4:58;
reconsider q = p as FinSequence of DX by A1, FINSEQ_1:def_4;
 ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & f "**" (Func_Seq (F,q)) = f "**" (Func_Seq (F,p)) ) by A1, A2;
hence  ex b1 being Element of DK ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b1 = f "**" (Func_Seq (F,p)) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of DK st ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b1 = f "**" (Func_Seq (F,p)) ) & ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b2 = f "**" (Func_Seq (F,p)) ) holds
b1 = b2
proof
let X1, X2 be Element of DK; ::_thesis: ( ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & X1 = f "**" (Func_Seq (F,p)) ) & ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & X2 = f "**" (Func_Seq (F,p)) ) implies X1 = X2 )
assume that
A3: ex p1 being FinSequence of DX st
( p1 is one-to-one & rng p1 = Y & X1 = f "**" (Func_Seq (F,p1)) ) and
A4: ex p2 being FinSequence of DX st
( p2 is one-to-one & rng p2 = Y & X2 = f "**" (Func_Seq (F,p2)) ) ; ::_thesis: X1 = X2
consider p1 being FinSequence of DX such that
A5: p1 is one-to-one and
A6: rng p1 = Y and
A7: X1 = f "**" (Func_Seq (F,p1)) by A3;
consider p2 being FinSequence of DX such that
A8: p2 is one-to-one and
A9: rng p2 = Y and
A10: X2 = f "**" (Func_Seq (F,p2)) by A4;
A11: dom p1 = dom p2 by A5, A6, A8, A9, Th1;
consider P being Permutation of (dom p1) such that
A12: p2 = p1 * P and
 dom P = dom p1 and
 rng P = dom p1 by A5, A6, A8, A9, Th1;
now__::_thesis:_for_xd_being_set_holds_
(_xd_in_dom_(Func_Seq_(F,p1))_iff_xd_in_dom_p1_)
let xd be set ; ::_thesis: ( xd in dom (Func_Seq (F,p1)) iff xd in dom p1 )
 ( xd in dom p1 implies p1 . xd in rng p1 ) by FUNCT_1:3;
hence  ( xd in dom (Func_Seq (F,p1)) iff xd in dom p1 ) by B3, A6, FUNCT_1:11; ::_thesis: verum
end;
then A13: dom (Func_Seq (F,p1)) = dom p1 by TARSKI:1;
now__::_thesis:_for_xd_being_set_holds_
(_xd_in_dom_(Func_Seq_(F,p2))_iff_xd_in_dom_p2_)
let xd be set ; ::_thesis: ( xd in dom (Func_Seq (F,p2)) iff xd in dom p2 )
 ( xd in dom p2 implies p2 . xd in rng p2 ) by FUNCT_1:3;
hence  ( xd in dom (Func_Seq (F,p2)) iff xd in dom p2 ) by B3, A9, FUNCT_1:11; ::_thesis: verum
end;
then A14: dom (Func_Seq (F,p2)) = dom p2 by TARSKI:1;
A15: rng P = dom (Func_Seq (F,p1)) by A13, FUNCT_2:def_3;
now__::_thesis:_for_xd_being_set_holds_
(_xd_in_dom_((Func_Seq_(F,p1))_*_P)_iff_xd_in_dom_(Func_Seq_(F,p2))_)
let xd be set ; ::_thesis: ( xd in dom ((Func_Seq (F,p1)) * P) iff xd in dom (Func_Seq (F,p2)) )
 ( xd in dom P implies P . xd in dom (Func_Seq (F,p1)) ) by A15, FUNCT_1:3;
then  ( xd in dom ((Func_Seq (F,p1)) * P) iff xd in dom P ) by FUNCT_1:11;
hence  ( xd in dom ((Func_Seq (F,p1)) * P) iff xd in dom (Func_Seq (F,p2)) ) by A11, A14, FUNCT_2:52; ::_thesis: verum
end;
then A16: dom (Func_Seq (F,p2)) = dom ((Func_Seq (F,p1)) * P) by TARSKI:1;
now__::_thesis:_for_s_being_set_st_s_in_dom_(Func_Seq_(F,p2))_holds_
(Func_Seq_(F,p2))_._s_=_((Func_Seq_(F,p1))_*_P)_._s
let s be set ; ::_thesis: ( s in dom (Func_Seq (F,p2)) implies (Func_Seq (F,p2)) . s = ((Func_Seq (F,p1)) * P) . s )
assume A17: s in dom (Func_Seq (F,p2)) ; ::_thesis: (Func_Seq (F,p2)) . s = ((Func_Seq (F,p1)) * P) . s
then reconsider i = s as Element of NAT ;
 i in dom P by A11, A14, A17, FUNCT_2:52;
then A18: P . i in rng P by FUNCT_1:3;
then  P . i in dom (Func_Seq (F,p2)) by A11, A14, FUNCT_2:def_3;
then reconsider j = P . i as Element of NAT ;
A19: j in dom p1 by A18, FUNCT_2:def_3;
A20: s in dom P by A11, A14, A17, FUNCT_2:52;
(Func_Seq (F,p2)) . s = F . (p2 . i) by A14, A17, FUNCT_1:13
.= F . (p1 . (P . i)) by A12, A20, FUNCT_1:13
.= (Func_Seq (F,p1)) . j by A19, FUNCT_1:13
.= ((Func_Seq (F,p1)) * P) . s by A20, FUNCT_1:13 ;
hence  (Func_Seq (F,p2)) . s = ((Func_Seq (F,p1)) * P) . s ; ::_thesis: verum
end;
then  Func_Seq (F,p2) = (Func_Seq (F,p1)) * P by A16, FUNCT_1:2;
hence  X1 = X2 by A1, A2, A7, A10, A13, FINSOP_1:7; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines setopfunc BHSP_5:def_5_:_
 for DK, DX being non empty set
for f being BinOp of DK st f is commutative & f is associative & f is having_a_unity holds
for Y being finite Subset of DX
for F being Function of DX,DK st Y c= dom F holds
for b6 being Element of DK holds
( b6 = setopfunc (Y,DX,DK,F,f) iff ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b6 = f "**" (Func_Seq (F,p)) ) );

definition
let X be RealUnitarySpace;
let x be Point of X;
let Y be finite Subset of X;
func setop_xPre_PROD (x,Y,X) ->  Real means :: BHSP_5:def 6
 ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Element of NAT st i in dom q holds
q . i = PO (i,p,x) ) & it = addreal "**" q ) );
existence
 ex b1 being Real ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Element of NAT st i in dom q holds
q . i = PO (i,p,x) ) & b1 = addreal "**" q ) )
proof
consider p0 being FinSequence such that
A1: rng p0 = Y and
A2: p0 is one-to-one by FINSEQ_4:58;
reconsider p = p0 as FinSequence of the carrier of X by A1, FINSEQ_1:def_4;
set ll = len p;
deffunc H1( Nat) ->  set = PO ($1,p,x);
consider q0 being FinSequence such that
A3: ( len q0 = len p & ( for i being Nat st i in dom q0 holds
q0 . i = H1(i) ) ) from FINSEQ_1:sch_2();
A4: dom q0 = Seg (len p) by A3, FINSEQ_1:def_3;
A5: dom q0 = dom p by A3, FINSEQ_3:29;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_q0_holds_
q0_._i_in_REAL
let i be Nat; ::_thesis: ( i in dom q0 implies q0 . i in REAL )
assume A6: i in dom q0 ; ::_thesis: q0 . i in REAL
then A7: q0 . i = PO (i,p,x) by A3
.= the scalar of X . [x,(p . i)] ;
reconsider y = p . i as Point of X by A5, A6, FINSEQ_2:11;
 the scalar of X . [x,(p . i)] = x .|. y by BHSP_1:def_1;
hence  q0 . i in REAL by A7; ::_thesis: verum
end;
then reconsider q = q0 as FinSequence of REAL by FINSEQ_2:12;
take  addreal "**" q ; ::_thesis: ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Element of NAT st i in dom q holds
q . i = PO (i,p,x) ) & addreal "**" q = addreal "**" q ) )
take  p ; ::_thesis: ( p is one-to-one & rng p = Y & ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Element of NAT st i in dom q holds
q . i = PO (i,p,x) ) & addreal "**" q = addreal "**" q ) )
thus  ( p is one-to-one & rng p = Y ) by A1, A2; ::_thesis: ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Element of NAT st i in dom q holds
q . i = PO (i,p,x) ) & addreal "**" q = addreal "**" q )
take  q ; ::_thesis: ( dom q = dom p & ( for i being Element of NAT st i in dom q holds
q . i = PO (i,p,x) ) & addreal "**" q = addreal "**" q )
thus  ( dom q = dom p & ( for i being Element of NAT st i in dom q holds
q . i = PO (i,p,x) ) & addreal "**" q = addreal "**" q ) by A3, A4, FINSEQ_1:def_3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real st ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Element of NAT st i in dom q holds
q . i = PO (i,p,x) ) & b1 = addreal "**" q ) ) & ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Element of NAT st i in dom q holds
q . i = PO (i,p,x) ) & b2 = addreal "**" q ) ) holds
b1 = b2
proof
let X1, X2 be Element of REAL ; ::_thesis: ( ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Element of NAT st i in dom q holds
q . i = PO (i,p,x) ) & X1 = addreal "**" q ) ) & ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Element of NAT st i in dom q holds
q . i = PO (i,p,x) ) & X2 = addreal "**" q ) ) implies X1 = X2 )
assume that
A8: ex p1 being FinSequence of the carrier of X st
( p1 is one-to-one & rng p1 = Y & ex q1 being FinSequence of REAL st
( dom q1 = dom p1 & ( for i being Element of NAT st i in dom q1 holds
q1 . i = PO (i,p1,x) ) & X1 = addreal "**" q1 ) ) and
A9: ex p2 being FinSequence of the carrier of X st
( p2 is one-to-one & rng p2 = Y & ex q2 being FinSequence of REAL st
( dom q2 = dom p2 & ( for i being Element of NAT st i in dom q2 holds
q2 . i = PO (i,p2,x) ) & X2 = addreal "**" q2 ) ) ; ::_thesis: X1 = X2
consider p1 being FinSequence of the carrier of X such that
A10: p1 is one-to-one and
A11: rng p1 = Y and
A12: ex q1 being FinSequence of REAL st
( dom q1 = dom p1 & ( for i being Element of NAT st i in dom q1 holds
q1 . i = PO (i,p1,x) ) & X1 = addreal "**" q1 ) by A8;
consider p2 being FinSequence of the carrier of X such that
A13: p2 is one-to-one and
A14: rng p2 = Y and
A15: ex q2 being FinSequence of REAL st
( dom q2 = dom p2 & ( for i being Element of NAT st i in dom q2 holds
q2 . i = PO (i,p2,x) ) & X2 = addreal "**" q2 ) by A9;
consider q1 being FinSequence of REAL  such that
A16: dom q1 = dom p1 and
A17: for i being Element of NAT st i in dom q1 holds
q1 . i = PO (i,p1,x) and
A18: X1 = addreal "**" q1 by A12;
consider q2 being FinSequence of REAL  such that
A19: dom q2 = dom p2 and
A20: for i being Element of NAT st i in dom q2 holds
q2 . i = PO (i,p2,x) and
A21: X2 = addreal "**" q2 by A15;
A22: dom p1 = dom p2 by A10, A11, A13, A14, Th1;
consider P being Permutation of (dom p1) such that
A23: p2 = p1 * P and
 dom P = dom p1 and
 rng P = dom p1 by A10, A11, A13, A14, Th1;
A24: rng P = dom q1 by A16, FUNCT_2:def_3;
A25: dom P = dom q2 by A19, A22, FUNCT_2:52;
A26: rng P = dom q2 by A19, A22, FUNCT_2:def_3;
A27: dom p1 = dom q2 by A10, A11, A13, A14, A19, Th1;
now__::_thesis:_for_xd_being_set_holds_
(_xd_in_dom_(q1_*_P)_iff_xd_in_dom_q2_)
let xd be set ; ::_thesis: ( xd in dom (q1 * P) iff xd in dom q2 )
 ( xd in dom P implies P . xd in dom q1 ) by A24, FUNCT_1:3;
hence  ( xd in dom (q1 * P) iff xd in dom q2 ) by A25, FUNCT_1:11; ::_thesis: verum
end;
then A28: dom q2 = dom (q1 * P) by TARSKI:1;
now__::_thesis:_for_s_being_set_st_s_in_dom_q2_holds_
q2_._s_=_(q1_*_P)_._s
let s be set ; ::_thesis: ( s in dom q2 implies q2 . s = (q1 * P) . s )
assume A29: s in dom q2 ; ::_thesis: q2 . s = (q1 * P) . s
then reconsider i = s as Element of NAT ;
 P . i in dom q2 by A25, A26, A29, FUNCT_1:3;
then reconsider j = P . i as Element of NAT ;
A30: s in dom P by A19, A22, A29, FUNCT_2:52;
q2 . s = PO (i,p2,x) by A20, A29
.= PO (j,p1,x) by A23, A30, FUNCT_1:13
.= q1 . (P . i) by A16, A17, A25, A26, A27, A29, FUNCT_1:3
.= (q1 * P) . s by A30, FUNCT_1:13 ;
hence  q2 . s = (q1 * P) . s ; ::_thesis: verum
end;
then  q2 = q1 * P by A28, FUNCT_1:2;
hence  X1 = X2 by A16, A18, A21, FINSOP_1:7; ::_thesis: verum
end;
end;

:: deftheorem  defines setop_xPre_PROD BHSP_5:def_6_:_
 for X being RealUnitarySpace
for x being Point of X
for Y being finite Subset of X
for b4 being Real holds
( b4 = setop_xPre_PROD (x,Y,X) iff ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Element of NAT st i in dom q holds
q . i = PO (i,p,x) ) & b4 = addreal "**" q ) ) );

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

:: deftheorem  defines setop_xPROD BHSP_5:def_7_:_
 for X being RealUnitarySpace
for x being Point of X
for Y being finite Subset of X holds
( ( Y <> {} implies setop_xPROD (x,Y,X) = setop_xPre_PROD (x,Y,X) ) & ( not Y <> {} implies setop_xPROD (x,Y,X) = 0 ) );

begin

definition
let X be RealUnitarySpace;
mode OrthogonalFamily of X ->  Subset of X means :Def8: :: BHSP_5:def 8
 for x, y being Point of X st x in it & y in it & x <> y holds
x .|. y = 0 ;
existence
 ex b1 being Subset of X st
for x, y being Point of X st x in b1 & y in b1 & x <> y holds
x .|. y = 0
proof
take  {} ; ::_thesis: ( {} is Subset of X & ( for x, y being Point of X st x in {} & y in {} & x <> y holds
x .|. y = 0 ) )
thus  ( {} is Subset of X & ( for x, y being Point of X st x in {} & y in {} & x <> y holds
x .|. y = 0 ) ) by SUBSET_1:1; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines OrthogonalFamily BHSP_5:def_8_:_
 for X being RealUnitarySpace
for b2 being Subset of X holds
( b2 is OrthogonalFamily of X iff for x, y being Point of X st x in b2 & y in b2 & x <> y holds
x .|. y = 0 );

theorem Th2: :: BHSP_5:2
for X being RealUnitarySpace holds {} is OrthogonalFamily of X
proof
let X be RealUnitarySpace; ::_thesis: {} is OrthogonalFamily of X
A1: {} is Subset of X by SUBSET_1:1;
 for x, y being Point of X st x in {} & y in {} & x <> y holds
x .|. y = 0 ;
hence  {} is OrthogonalFamily of X by A1, Def8; ::_thesis: verum
end;

registration
let X be RealUnitarySpace;
cluster finite for OrthogonalFamily of X;
existence
 ex b1 being OrthogonalFamily of X st b1 is finite
proof
take  {} ; ::_thesis: ( {} is Subset of X & {} is OrthogonalFamily of X & {} is finite )
thus  ( {} is Subset of X & {} is OrthogonalFamily of X & {} is finite ) by Th2; ::_thesis: verum
end;
end;

definition
let X be RealUnitarySpace;
mode OrthonormalFamily of X ->  Subset of X means :Def9: :: BHSP_5:def 9
( it is OrthogonalFamily of X & ( for x being Point of X st x in it holds
x .|. x = 1 ) );
existence
 ex b1 being Subset of X st
( b1 is OrthogonalFamily of X & ( for x being Point of X st x in b1 holds
x .|. x = 1 ) )
proof
take  {} ; ::_thesis: ( {} is Subset of X & {} is OrthogonalFamily of X & ( for x being Point of X st x in {} holds
x .|. x = 1 ) )
thus  ( {} is Subset of X & {} is OrthogonalFamily of X & ( for x being Point of X st x in {} holds
x .|. x = 1 ) ) by Th2; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines OrthonormalFamily BHSP_5:def_9_:_
 for X being RealUnitarySpace
for b2 being Subset of X holds
( b2 is OrthonormalFamily of X iff ( b2 is OrthogonalFamily of X & ( for x being Point of X st x in b2 holds
x .|. x = 1 ) ) );

theorem Th3: :: BHSP_5:3
for X being RealUnitarySpace holds {} is OrthonormalFamily of X
proof
let X be RealUnitarySpace; ::_thesis: {} is OrthonormalFamily of X
A1: {} is OrthogonalFamily of X by Th2;
 for x being Point of X st x in {} holds
x .|. x = 1 ;
hence  {} is OrthonormalFamily of X by A1, Def9; ::_thesis: verum
end;

registration
let X be RealUnitarySpace;
cluster finite for OrthonormalFamily of X;
existence
 ex b1 being OrthonormalFamily of X st b1 is finite
proof
take  {} ; ::_thesis: ( {} is Subset of X & {} is OrthonormalFamily of X & {} is finite )
thus  ( {} is Subset of X & {} is OrthonormalFamily of X & {} is finite ) by Th3; ::_thesis: verum
end;
end;

theorem :: BHSP_5:4
for X being RealUnitarySpace
for x being Point of X holds
( x = 0. X iff for y being Point of X holds x .|. y = 0 )
proof
let X be RealUnitarySpace; ::_thesis: for x being Point of X holds
( x = 0. X iff for y being Point of X holds x .|. y = 0 )
let x be Point of X; ::_thesis: ( x = 0. X iff for y being Point of X holds x .|. y = 0 )
now__::_thesis:_(_(_for_y_being_Point_of_X_holds_x_.|._y_=_0_)_implies_x_=_0._X_)
assume  for y being Point of X holds x .|. y = 0 ; ::_thesis: x = 0. X
then  x .|. x = 0 ;
hence  x = 0. X by BHSP_1:def_2; ::_thesis: verum
end;
hence  ( x = 0. X iff for y being Point of X holds x .|. y = 0 ) by BHSP_1:14; ::_thesis: verum
end;

begin

theorem :: BHSP_5:5
for X being RealUnitarySpace
for x, y being Point of X holds (||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2))
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X holds (||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2))
let x, y be Point of X; ::_thesis: (||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2))
A1: (x + y) .|. (x + y) >= 0 by BHSP_1:def_2;
A2: (x - y) .|. (x - y) >= 0 by BHSP_1:def_2;
A3: x .|. x >= 0 by BHSP_1:def_2;
A4: y .|. y >= 0 by BHSP_1:def_2;
(||.(x + y).|| ^2) + (||.(x - y).|| ^2) = ((sqrt ((x + y) .|. (x + y))) ^2) + (||.(x - y).|| ^2) by BHSP_1:def_4
.= ((x + y) .|. (x + y)) + (||.(x - y).|| ^2) by A1, SQUARE_1:def_2
.= ((x + y) .|. (x + y)) + ((sqrt ((x - y) .|. (x - y))) ^2) by BHSP_1:def_4
.= ((x + y) .|. (x + y)) + ((x - y) .|. (x - y)) by A2, SQUARE_1:def_2
.= (((x .|. x) + (2 * (x .|. y))) + (y .|. y)) + ((x - y) .|. (x - y)) by BHSP_1:16
.= (((x .|. x) + (2 * (x .|. y))) + (y .|. y)) + (((x .|. x) - (2 * (x .|. y))) + (y .|. y)) by BHSP_1:18
.= (2 * (x .|. x)) + (2 * (y .|. y))
.= (2 * ((sqrt (x .|. x)) ^2)) + (2 * (y .|. y)) by A3, SQUARE_1:def_2
.= (2 * ((sqrt (x .|. x)) ^2)) + (2 * ((sqrt (y .|. y)) ^2)) by A4, SQUARE_1:def_2
.= (2 * (||.x.|| ^2)) + (2 * ((sqrt (y .|. y)) ^2)) by BHSP_1:def_4
.= (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2)) by BHSP_1:def_4 ;
hence  (||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2)) ; ::_thesis: verum
end;

theorem :: BHSP_5:6
for X being RealUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2)
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X st x,y are_orthogonal holds
||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2)
let x, y be Point of X; ::_thesis: ( x,y are_orthogonal implies ||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2) )
assume  x,y are_orthogonal ; ::_thesis: ||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2)
then A1: x .|. y = 0 by BHSP_1:def_3;
A2: (x + y) .|. (x + y) >= 0 by BHSP_1:def_2;
A3: x .|. x >= 0 by BHSP_1:def_2;
A4: y .|. y >= 0 by BHSP_1:def_2;
||.(x + y).|| ^2 = (sqrt ((x + y) .|. (x + y))) ^2 by BHSP_1:def_4
.= (x + y) .|. (x + y) by A2, SQUARE_1:def_2
.= ((x .|. x) + (2 * (x .|. y))) + (y .|. y) by BHSP_1:16
.= ((sqrt (x .|. x)) ^2) + (y .|. y) by A1, A3, SQUARE_1:def_2
.= ((sqrt (x .|. x)) ^2) + ((sqrt (y .|. y)) ^2) by A4, SQUARE_1:def_2
.= (||.x.|| ^2) + ((sqrt (y .|. y)) ^2) by BHSP_1:def_4
.= (||.x.|| ^2) + (||.y.|| ^2) by BHSP_1:def_4 ;
hence  ||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2) ; ::_thesis: verum
end;

theorem Th7: :: BHSP_5:7
for X being RealUnitarySpace
for p being FinSequence of the carrier of X st len p >= 1 & ( for i, j being Element of NAT st i in dom p & j in dom p & i <> j holds
the scalar of X . [(p . i),(p . j)] = 0 ) holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = the scalar of X . [(p . i),(p . i)] ) holds
( the addF of X "**" p) .|. ( the addF of X "**" p) = addreal "**" q
proof
let X be RealUnitarySpace; ::_thesis: for p being FinSequence of the carrier of X st len p >= 1 & ( for i, j being Element of NAT st i in dom p & j in dom p & i <> j holds
the scalar of X . [(p . i),(p . j)] = 0 ) holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = the scalar of X . [(p . i),(p . i)] ) holds
( the addF of X "**" p) .|. ( the addF of X "**" p) = addreal "**" q
let p be FinSequence of the carrier of X; ::_thesis: ( len p >= 1 & ( for i, j being Element of NAT st i in dom p & j in dom p & i <> j holds
the scalar of X . [(p . i),(p . j)] = 0 ) implies for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = the scalar of X . [(p . i),(p . i)] ) holds
( the addF of X "**" p) .|. ( the addF of X "**" p) = addreal "**" q )
assume that
A1: len p >= 1 and
A2: for i, j being Element of NAT st i in dom p & j in dom p & i <> j holds
the scalar of X . [(p . i),(p . j)] = 0 ; ::_thesis: for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = the scalar of X . [(p . i),(p . i)] ) holds
( the addF of X "**" p) .|. ( the addF of X "**" p) = addreal "**" q
A3: 1 in dom p by A1, FINSEQ_3:25;
let q be FinSequence of REAL ; ::_thesis: ( dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = the scalar of X . [(p . i),(p . i)] ) implies ( the addF of X "**" p) .|. ( the addF of X "**" p) = addreal "**" q )
assume that
A4: dom p = dom q and
A5: for i being Element of NAT st i in dom q holds
q . i = the scalar of X . [(p . i),(p . i)] ; ::_thesis: ( the addF of X "**" p) .|. ( the addF of X "**" p) = addreal "**" q
consider f being Function of NAT, the carrier of X such that
A6: f . 1 = p . 1 and
A7: for n being Element of NAT st 0 <> n & n < len p holds
f . (n + 1) = the addF of X . ((f . n),(p . (n + 1))) and
A8: the addF of X "**" p = f . (len p) by A1, FINSOP_1:1;
A9: ( the addF of X "**" p) .|. ( the addF of X "**" p) = the scalar of X . [(f . (len p)),(f . (len p))] by A8, BHSP_1:def_1;
A10: Seg (len q) = dom p by A4, FINSEQ_1:def_3
.= Seg (len p) by FINSEQ_1:def_3 ;
then A11: len q = len p by FINSEQ_1:6;
 len q >= 1 by A1, A10, FINSEQ_1:6;
then consider g being Function of NAT,REAL such that
A12: g . 1 = q . 1 and
A13: for n being Element of NAT st 0 <> n & n < len q holds
g . (n + 1) = addreal . ((g . n),(q . (n + 1))) and
A14: addreal "**" q = g . (len q) by FINSOP_1:1;
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= len q implies g . $1 = the scalar of X . [(f . $1),(f . $1)] );
A15: S1[ 0 ] ;
now__::_thesis:_for_n_being_Element_of_NAT_st_(_1_<=_n_&_n_<=_len_q_implies_g_._n_=_the_scalar_of_X_._[(f_._n),(f_._n)]_)_&_1_<=_n_+_1_&_n_+_1_<=_len_q_holds_
g_._(n_+_1)_=_the_scalar_of_X_._[(f_._(n_+_1)),(f_._(n_+_1))]
let n be Element of NAT ; ::_thesis: ( ( 1 <= n & n <= len q implies g . n = the scalar of X . [(f . n),(f . n)] ) & 1 <= n + 1 & n + 1 <= len q implies g . (n + 1) = the scalar of X . [(f . (n + 1)),(f . (n + 1))] )
assume A16: ( 1 <= n & n <= len q implies g . n = the scalar of X . [(f . n),(f . n)] ) ; ::_thesis: ( 1 <= n + 1 & n + 1 <= len q implies g . (n + 1) = the scalar of X . [(f . (n + 1)),(f . (n + 1))] )
now__::_thesis:_(_1_<=_n_+_1_&_n_+_1_<=_len_q_implies_g_._(n_+_1)_=_the_scalar_of_X_._[(f_._(n_+_1)),(f_._(n_+_1))]_)
assume that
A17: 1 <= n + 1 and
A18: n + 1 <= len q ; ::_thesis: g . (n + 1) = the scalar of X . [(f . (n + 1)),(f . (n + 1))]
A19: n <= n + 1 by NAT_1:11;
percases ( n = 0 or n <> 0 ) ;
supposeA20: n = 0 ; ::_thesis: g . (n + 1) = the scalar of X . [(f . (n + 1)),(f . (n + 1))]
 1 in Seg (len p) by A1, FINSEQ_1:1;
then  1 in dom q by A4, FINSEQ_1:def_3;
hence  g . (n + 1) = the scalar of X . [(f . (n + 1)),(f . (n + 1))] by A5, A6, A12, A20; ::_thesis: verum
end;
supposeA21: n <> 0 ; ::_thesis: g . (n + 1) = the scalar of X . [(f . (n + 1)),(f . (n + 1))]
then  0 < n by NAT_1:3;
then A22: 0 + 1 <= n by INT_1:7;
A23: n <= len p by A11, A18, A19, XXREAL_0:2;
A24: (n + 1) - 1 < (len q) - 0 by A18, XREAL_1:15;
then A25: n < len p by A10, FINSEQ_1:6;
A26: n + 1 in Seg (len q) by A17, A18, FINSEQ_1:1;
then A27: n + 1 in dom q by FINSEQ_1:def_3;
A28: n + 1 in dom p by A4, A26, FINSEQ_1:def_3;
A29: dom f = NAT by FUNCT_2:def_1;
then A30: f . n in rng f by FUNCT_1:3;
 rng f c= the carrier of X by RELAT_1:def_19;
then reconsider z = f . n as Element of X by A30;
A31: p . (n + 1) in rng p by A28, FUNCT_1:3;
 rng p c= the carrier of X by RELAT_1:def_19;
then reconsider y = p . (n + 1) as Element of X by A31;
 for i being Element of NAT st 1 <= i & i <= n holds
the scalar of X . [(f . i),y] = 0
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies the scalar of X . [(f . i),y] = 0 )
defpred S2[ Element of NAT ] means ( 1 <= $1 & $1 <= n implies the scalar of X . [(f . $1),y] = 0 );
A32: S2[ 0 ] ;
A33: for i being Element of NAT st S2[i] holds
S2[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S2[i] implies S2[i + 1] )
assume A34: S2[i] ; ::_thesis: S2[i + 1]
A35: 1 <> n + 1 by A21;
assume that
A36: 1 <= i + 1 and
A37: i + 1 <= n ; ::_thesis: the scalar of X . [(f . (i + 1)),y] = 0
 i + 1 <= len p by A23, A37, XXREAL_0:2;
then A38: i + 1 in dom p by A36, FINSEQ_3:25;
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: the scalar of X . [(f . (i + 1)),y] = 0
hence  the scalar of X . [(f . (i + 1)),y] = 0 by A2, A3, A6, A28, A35; ::_thesis: verum
end;
supposeA39: i <> 0 ; ::_thesis: the scalar of X . [(f . (i + 1)),y] = 0
A40: f . i in rng f by A29, FUNCT_1:3;
 rng f c= the carrier of X by RELAT_1:def_19;
then reconsider s = f . i as Element of X by A40;
A41: i + 1 <= len p by A23, A37, XXREAL_0:2;
then  i + 1 in dom p by A36, FINSEQ_3:25;
then A42: p . (i + 1) in rng p by FUNCT_1:3;
 rng p c= the carrier of X by RELAT_1:def_19;
then reconsider t = p . (i + 1) as Element of X by A42;
A43: (i + 1) - 1 < (len p) - 0 by A41, XREAL_1:15;
 0 < i by A39, NAT_1:3;
then A44: 0 + 1 <= i by INT_1:7;
 i < i + 1 by XREAL_1:29;
then A45: s .|. y = 0 by A34, A37, A44, BHSP_1:def_1, XXREAL_0:2;
A46: (i + 1) + 0 < n + 1 by A37, XREAL_1:8;
the scalar of X . [(f . (i + 1)),y] = the scalar of X . [(s + t),y] by A7, A39, A43
.= (s + t) .|. y by BHSP_1:def_1
.= 0 + (t .|. y) by A45, BHSP_1:2
.= the scalar of X . [t,y] by BHSP_1:def_1
.= 0 by A2, A28, A38, A46 ;
hence  the scalar of X . [(f . (i + 1)),y] = 0 ; ::_thesis: verum
end;
end;
end;
 for i being Element of NAT holds S2[i] from NAT_1:sch_1(A32, A33);
hence  ( 1 <= i & i <= n implies the scalar of X . [(f . i),y] = 0 ) ; ::_thesis: verum
end;
then A47: 0 = the scalar of X . [z,y] by A22
.= z .|. y by BHSP_1:def_1 ;
thus g . (n + 1) = addreal . (( the scalar of X . [(f . n),(f . n)]),(q . (n + 1))) by A13, A16, A21, A22, A24
.= addreal . (( the scalar of X . [(f . n),(f . n)]),( the scalar of X . [(p . (n + 1)),(p . (n + 1))])) by A5, A27
.= addreal . (( the scalar of X . [(f . n),(f . n)]),(y .|. y)) by BHSP_1:def_1
.= addreal . ((z .|. z),(y .|. y)) by BHSP_1:def_1
.= (((z .|. z) + (z .|. y)) + (y .|. z)) + (y .|. y) by A47, BINOP_2:def_9
.= ((z .|. (z + y)) + (y .|. z)) + (y .|. y) by BHSP_1:2
.= (z .|. (z + y)) + ((y .|. z) + (y .|. y))
.= (z .|. (z + y)) + (y .|. (z + y)) by BHSP_1:2
.= (z + y) .|. (z + y) by BHSP_1:2
.= the scalar of X . [( the addF of X . ((f . n),(p . (n + 1)))),(z + y)] by BHSP_1:def_1
.= the scalar of X . [( the addF of X . ((f . n),(p . (n + 1)))),(f . (n + 1))] by A7, A21, A25
.= the scalar of X . [(f . (n + 1)),(f . (n + 1))] by A7, A21, A25 ; ::_thesis: verum
end;
end;
end;
hence  ( 1 <= n + 1 & n + 1 <= len q implies g . (n + 1) = the scalar of X . [(f . (n + 1)),(f . (n + 1))] ) ; ::_thesis: verum
end;
then A48: for n being Element of NAT st S1[n] holds
S1[n + 1] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A15, A48);
hence  ( the addF of X "**" p) .|. ( the addF of X "**" p) = addreal "**" q by A1, A9, A11, A14; ::_thesis: verum
end;

theorem Th8: :: BHSP_5:8
for X being RealUnitarySpace
for x being Point of X
for p being FinSequence of the carrier of X st len p >= 1 holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = the scalar of X . [x,(p . i)] ) holds
x .|. ( the addF of X "**" p) = addreal "**" q
proof
let X be RealUnitarySpace; ::_thesis: for x being Point of X
for p being FinSequence of the carrier of X st len p >= 1 holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = the scalar of X . [x,(p . i)] ) holds
x .|. ( the addF of X "**" p) = addreal "**" q
let x be Point of X; ::_thesis: for p being FinSequence of the carrier of X st len p >= 1 holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = the scalar of X . [x,(p . i)] ) holds
x .|. ( the addF of X "**" p) = addreal "**" q
let p be FinSequence of the carrier of X; ::_thesis: ( len p >= 1 implies for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = the scalar of X . [x,(p . i)] ) holds
x .|. ( the addF of X "**" p) = addreal "**" q )
assume A1: len p >= 1 ; ::_thesis: for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = the scalar of X . [x,(p . i)] ) holds
x .|. ( the addF of X "**" p) = addreal "**" q
let q be FinSequence of REAL ; ::_thesis: ( dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = the scalar of X . [x,(p . i)] ) implies x .|. ( the addF of X "**" p) = addreal "**" q )
assume that
A2: dom p = dom q and
A3: for i being Element of NAT st i in dom q holds
q . i = the scalar of X . [x,(p . i)] ; ::_thesis: x .|. ( the addF of X "**" p) = addreal "**" q
consider f being Function of NAT, the carrier of X such that
A4: f . 1 = p . 1 and
A5: for n being Element of NAT st 0 <> n & n < len p holds
f . (n + 1) = the addF of X . ((f . n),(p . (n + 1))) and
A6: the addF of X "**" p = f . (len p) by A1, FINSOP_1:1;
A7: Seg (len q) = dom p by A2, FINSEQ_1:def_3
.= Seg (len p) by FINSEQ_1:def_3 ;
then A8: len q = len p by FINSEQ_1:6;
 len q >= 1 by A1, A7, FINSEQ_1:6;
then consider g being Function of NAT,REAL such that
A9: g . 1 = q . 1 and
A10: for n being Element of NAT st 0 <> n & n < len q holds
g . (n + 1) = addreal . ((g . n),(q . (n + 1))) and
A11: addreal "**" q = g . (len q) by FINSOP_1:1;
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= len q implies g . $1 = the scalar of X . [x,(f . $1)] );
A12: S1[ 0 ] ;
now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_&_1_<=_n_+_1_&_n_+_1_<=_len_q_holds_
g_._(n_+_1)_=_the_scalar_of_X_._[x,(f_._(n_+_1))]
let n be Element of NAT ; ::_thesis: ( S1[n] & 1 <= n + 1 & n + 1 <= len q implies g . (n + 1) = the scalar of X . [x,(f . (n + 1))] )
assume A13: S1[n] ; ::_thesis: ( 1 <= n + 1 & n + 1 <= len q implies g . (n + 1) = the scalar of X . [x,(f . (n + 1))] )
now__::_thesis:_(_1_<=_n_+_1_&_n_+_1_<=_len_q_implies_g_._(n_+_1)_=_the_scalar_of_X_._[x,(f_._(n_+_1))]_)
assume that
A14: 1 <= n + 1 and
A15: n + 1 <= len q ; ::_thesis: g . (n + 1) = the scalar of X . [x,(f . (n + 1))]
percases ( n = 0 or n <> 0 ) ;
supposeA16: n = 0 ; ::_thesis: g . (n + 1) = the scalar of X . [x,(f . (n + 1))]
 1 in Seg (len p) by A1, FINSEQ_1:1;
then  1 in dom q by A2, FINSEQ_1:def_3;
hence  g . (n + 1) = the scalar of X . [x,(f . (n + 1))] by A3, A4, A9, A16; ::_thesis: verum
end;
supposeA17: n <> 0 ; ::_thesis: g . (n + 1) = the scalar of X . [x,(f . (n + 1))]
then  0 < n by NAT_1:3;
then A18: 0 + 1 <= n by INT_1:7;
A19: (n + 1) - 1 < (len q) - 0 by A15, XREAL_1:15;
A20: n + 1 in Seg (len q) by A14, A15, FINSEQ_1:1;
then A21: n + 1 in dom q by FINSEQ_1:def_3;
A22: n + 1 in dom p by A2, A20, FINSEQ_1:def_3;
 dom f = NAT by FUNCT_2:def_1;
then A23: f . n in rng f by FUNCT_1:3;
 rng f c= the carrier of X by RELAT_1:def_19;
then reconsider z = f . n as Element of X by A23;
A24: p . (n + 1) in rng p by A22, FUNCT_1:3;
 rng p c= the carrier of X by RELAT_1:def_19;
then reconsider y = p . (n + 1) as Element of X by A24;
thus g . (n + 1) = addreal . (( the scalar of X . [x,(f . n)]),(q . (n + 1))) by A10, A13, A17, A18, A19
.= addreal . (( the scalar of X . [x,(f . n)]),( the scalar of X . [x,(p . (n + 1))])) by A3, A21
.= addreal . (( the scalar of X . [x,(f . n)]),(x .|. y)) by BHSP_1:def_1
.= addreal . ((x .|. z),(x .|. y)) by BHSP_1:def_1
.= (x .|. z) + (x .|. y) by BINOP_2:def_9
.= x .|. (z + y) by BHSP_1:2
.= the scalar of X . [x,( the addF of X . ((f . n),(p . (n + 1))))] by BHSP_1:def_1
.= the scalar of X . [x,(f . (n + 1))] by A5, A8, A17, A19 ; ::_thesis: verum
end;
end;
end;
hence  ( 1 <= n + 1 & n + 1 <= len q implies g . (n + 1) = the scalar of X . [x,(f . (n + 1))] ) ; ::_thesis: verum
end;
then A25: for n being Element of NAT st S1[n] holds
S1[n + 1] ;
A26: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A12, A25);
 1 <= len q by A1, A7, FINSEQ_1:6;
then g . (len q) = the scalar of X . [x,(f . (len q))] by A26
.= the scalar of X . [x,(f . (len p))] by A7, FINSEQ_1:6 ;
hence  x .|. ( the addF of X "**" p) = addreal "**" q by A6, A11, BHSP_1:def_1; ::_thesis: verum
end;

theorem Th9: :: BHSP_5:9
for X being RealUnitarySpace
for S being non empty finite Subset of X
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y1, y2 being Point of X st y1 in S & y2 in S & y1 <> y2 holds
the scalar of X . [(F . y1),(F . y2)] = 0 ) holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [(F . y),(F . y)] ) holds
for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [( the addF of X "**" (Func_Seq (F,p))),( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))
proof
let X be RealUnitarySpace; ::_thesis: for S being non empty finite Subset of X
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y1, y2 being Point of X st y1 in S & y2 in S & y1 <> y2 holds
the scalar of X . [(F . y1),(F . y2)] = 0 ) holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [(F . y),(F . y)] ) holds
for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [( the addF of X "**" (Func_Seq (F,p))),( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))
let S be non empty finite Subset of X; ::_thesis: for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y1, y2 being Point of X st y1 in S & y2 in S & y1 <> y2 holds
the scalar of X . [(F . y1),(F . y2)] = 0 ) holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [(F . y),(F . y)] ) holds
for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [( the addF of X "**" (Func_Seq (F,p))),( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))
let F be Function of the carrier of X, the carrier of X; ::_thesis: ( S c= dom F & ( for y1, y2 being Point of X st y1 in S & y2 in S & y1 <> y2 holds
the scalar of X . [(F . y1),(F . y2)] = 0 ) implies for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [(F . y),(F . y)] ) holds
for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [( the addF of X "**" (Func_Seq (F,p))),( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p)) )
assume that
A1: S c= dom F and
A2: for y1, y2 being Point of X st y1 in S & y2 in S & y1 <> y2 holds
the scalar of X . [(F . y1),(F . y2)] = 0 ; ::_thesis: for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [(F . y),(F . y)] ) holds
for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [( the addF of X "**" (Func_Seq (F,p))),( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))
let H be Function of the carrier of X,REAL; ::_thesis: ( S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [(F . y),(F . y)] ) implies for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [( the addF of X "**" (Func_Seq (F,p))),( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p)) )
assume that
A3: S c= dom H and
A4: for y being Point of X st y in S holds
H . y = the scalar of X . [(F . y),(F . y)] ; ::_thesis: for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [( the addF of X "**" (Func_Seq (F,p))),( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))
let p be FinSequence of the carrier of X; ::_thesis: ( p is one-to-one & rng p = S implies the scalar of X . [( the addF of X "**" (Func_Seq (F,p))),( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p)) )
assume that
A5: p is one-to-one and
A6: rng p = S ; ::_thesis: the scalar of X . [( the addF of X "**" (Func_Seq (F,p))),( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))
set fp = Func_Seq (F,p);
set hp = Func_Seq (H,p);
now__::_thesis:_for_z_being_set_holds_
(_z_in_dom_(Func_Seq_(F,p))_iff_z_in_dom_p_)
let z be set ; ::_thesis: ( z in dom (Func_Seq (F,p)) iff z in dom p )
 ( z in dom p implies p . z in rng p ) by FUNCT_1:3;
hence  ( z in dom (Func_Seq (F,p)) iff z in dom p ) by A1, A6, FUNCT_1:11; ::_thesis: verum
end;
then A7: dom (Func_Seq (F,p)) = dom p by TARSKI:1;
then A8: Seg (len p) = dom (Func_Seq (F,p)) by FINSEQ_1:def_3
.= Seg (len (Func_Seq (F,p))) by FINSEQ_1:def_3 ;
A9: len p = card S by A5, A6, FINSEQ_4:62;
 0 < card S by NAT_1:3;
then  0 + 1 <= card S by INT_1:7;
then A10: 1 <= len (Func_Seq (F,p)) by A8, A9, FINSEQ_1:6;
A11: for i, j being Element of NAT st i in dom (Func_Seq (F,p)) & j in dom (Func_Seq (F,p)) & i <> j holds
the scalar of X . [((Func_Seq (F,p)) . i),((Func_Seq (F,p)) . j)] = 0
proof
let i, j be Element of NAT ; ::_thesis: ( i in dom (Func_Seq (F,p)) & j in dom (Func_Seq (F,p)) & i <> j implies the scalar of X . [((Func_Seq (F,p)) . i),((Func_Seq (F,p)) . j)] = 0 )
assume that
A12: i in dom (Func_Seq (F,p)) and
A13: j in dom (Func_Seq (F,p)) and
A14: i <> j ; ::_thesis: the scalar of X . [((Func_Seq (F,p)) . i),((Func_Seq (F,p)) . j)] = 0
A15: p . i in S by A6, A7, A12, FUNCT_1:3;
A16: p . j in S by A6, A7, A13, FUNCT_1:3;
A17: (Func_Seq (F,p)) . i = F . (p . i) by A12, FUNCT_1:12;
A18: (Func_Seq (F,p)) . j = F . (p . j) by A13, FUNCT_1:12;
 p . i <> p . j by A5, A7, A12, A13, A14, FUNCT_1:def_4;
hence  the scalar of X . [((Func_Seq (F,p)) . i),((Func_Seq (F,p)) . j)] = 0 by A2, A15, A16, A17, A18; ::_thesis: verum
end;
now__::_thesis:_for_z_being_set_holds_
(_z_in_dom_(Func_Seq_(H,p))_iff_z_in_dom_p_)
let z be set ; ::_thesis: ( z in dom (Func_Seq (H,p)) iff z in dom p )
 ( z in dom p implies p . z in rng p ) by FUNCT_1:3;
hence  ( z in dom (Func_Seq (H,p)) iff z in dom p ) by A3, A6, FUNCT_1:11; ::_thesis: verum
end;
then A19: dom (Func_Seq (H,p)) = dom p by TARSKI:1;
A20: for i being Element of NAT st i in dom (Func_Seq (H,p)) holds
(Func_Seq (H,p)) . i = the scalar of X . [((Func_Seq (F,p)) . i),((Func_Seq (F,p)) . i)]
proof
let i be Element of NAT ; ::_thesis: ( i in dom (Func_Seq (H,p)) implies (Func_Seq (H,p)) . i = the scalar of X . [((Func_Seq (F,p)) . i),((Func_Seq (F,p)) . i)] )
assume A21: i in dom (Func_Seq (H,p)) ; ::_thesis: (Func_Seq (H,p)) . i = the scalar of X . [((Func_Seq (F,p)) . i),((Func_Seq (F,p)) . i)]
A22: p . i in S by A6, A19, A21, FUNCT_1:3;
(Func_Seq (H,p)) . i = H . (p . i) by A19, A21, FUNCT_1:13
.= the scalar of X . [(F . (p . i)),(F . (p . i))] by A4, A22
.= the scalar of X . [((F * p) . i),(F . (p . i))] by A19, A21, FUNCT_1:13
.= the scalar of X . [((Func_Seq (F,p)) . i),((Func_Seq (F,p)) . i)] by A19, A21, FUNCT_1:13 ;
hence  (Func_Seq (H,p)) . i = the scalar of X . [((Func_Seq (F,p)) . i),((Func_Seq (F,p)) . i)] ; ::_thesis: verum
end;
the scalar of X . [( the addF of X "**" (Func_Seq (F,p))),( the addF of X "**" (Func_Seq (F,p)))] = ( the addF of X "**" (Func_Seq (F,p))) .|. ( the addF of X "**" (Func_Seq (F,p))) by BHSP_1:def_1
.= addreal "**" (Func_Seq (H,p)) by A7, A10, A11, A19, A20, Th7 ;
hence  the scalar of X . [( the addF of X "**" (Func_Seq (F,p))),( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p)) ; ::_thesis: verum
end;

theorem Th10: :: BHSP_5:10
for X being RealUnitarySpace
for x being Point of X
for S being non empty finite Subset of X
for F being Function of the carrier of X, the carrier of X st S c= dom F holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [x,(F . y)] ) holds
for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [x,( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))
proof
let X be RealUnitarySpace; ::_thesis: for x being Point of X
for S being non empty finite Subset of X
for F being Function of the carrier of X, the carrier of X st S c= dom F holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [x,(F . y)] ) holds
for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [x,( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))
let x be Point of X; ::_thesis: for S being non empty finite Subset of X
for F being Function of the carrier of X, the carrier of X st S c= dom F holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [x,(F . y)] ) holds
for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [x,( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))
let S be non empty finite Subset of X; ::_thesis: for F being Function of the carrier of X, the carrier of X st S c= dom F holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [x,(F . y)] ) holds
for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [x,( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))
let F be Function of the carrier of X, the carrier of X; ::_thesis: ( S c= dom F implies for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [x,(F . y)] ) holds
for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [x,( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p)) )
assume A1: S c= dom F ; ::_thesis: for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [x,(F . y)] ) holds
for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [x,( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))
let H be Function of the carrier of X,REAL; ::_thesis: ( S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [x,(F . y)] ) implies for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [x,( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p)) )
assume that
A2: S c= dom H and
A3: for y being Point of X st y in S holds
H . y = the scalar of X . [x,(F . y)] ; ::_thesis: for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [x,( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))
let p be FinSequence of the carrier of X; ::_thesis: ( p is one-to-one & rng p = S implies the scalar of X . [x,( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p)) )
assume that
A4: p is one-to-one and
A5: rng p = S ; ::_thesis: the scalar of X . [x,( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))
set p1 = Func_Seq (F,p);
set q1 = Func_Seq (H,p);
now__::_thesis:_for_xd_being_set_holds_
(_xd_in_dom_(Func_Seq_(F,p))_iff_xd_in_dom_p_)
let xd be set ; ::_thesis: ( xd in dom (Func_Seq (F,p)) iff xd in dom p )
 ( xd in dom p implies p . xd in rng p ) by FUNCT_1:3;
hence  ( xd in dom (Func_Seq (F,p)) iff xd in dom p ) by A1, A5, FUNCT_1:11; ::_thesis: verum
end;
then A6: dom (Func_Seq (F,p)) = dom p by TARSKI:1;
now__::_thesis:_for_xd_being_set_holds_
(_xd_in_dom_(Func_Seq_(H,p))_iff_xd_in_dom_p_)
let xd be set ; ::_thesis: ( xd in dom (Func_Seq (H,p)) iff xd in dom p )
 ( xd in dom p implies p . xd in rng p ) by FUNCT_1:3;
hence  ( xd in dom (Func_Seq (H,p)) iff xd in dom p ) by A2, A5, FUNCT_1:11; ::_thesis: verum
end;
then A7: dom (Func_Seq (H,p)) = dom p by TARSKI:1;
A8: for i being Element of NAT st i in dom (Func_Seq (F,p)) holds
(Func_Seq (H,p)) . i = the scalar of X . [x,((Func_Seq (F,p)) . i)]
proof
let i be Element of NAT ; ::_thesis: ( i in dom (Func_Seq (F,p)) implies (Func_Seq (H,p)) . i = the scalar of X . [x,((Func_Seq (F,p)) . i)] )
assume A9: i in dom (Func_Seq (F,p)) ; ::_thesis: (Func_Seq (H,p)) . i = the scalar of X . [x,((Func_Seq (F,p)) . i)]
A10: p . i in S by A5, A6, A9, FUNCT_1:3;
(Func_Seq (H,p)) . i = H . (p . i) by A6, A9, FUNCT_1:13
.= the scalar of X . [x,(F . (p . i))] by A3, A10
.= the scalar of X . [x,((Func_Seq (F,p)) . i)] by A6, A9, FUNCT_1:13 ;
hence  (Func_Seq (H,p)) . i = the scalar of X . [x,((Func_Seq (F,p)) . i)] ; ::_thesis: verum
end;
A11: Seg (len p) = dom (Func_Seq (F,p)) by A6, FINSEQ_1:def_3
.= Seg (len (Func_Seq (F,p))) by FINSEQ_1:def_3 ;
A12: len p = card S by A4, A5, FINSEQ_4:62;
 0 < card S by NAT_1:3;
then  0 + 1 <= card S by INT_1:7;
then  len (Func_Seq (F,p)) >= 1 by A11, A12, FINSEQ_1:6;
then  x .|. ( the addF of X "**" (Func_Seq (F,p))) = addreal "**" (Func_Seq (H,p)) by A6, A7, A8, Th8;
hence  the scalar of X . [x,( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p)) by BHSP_1:def_1; ::_thesis: verum
end;

theorem Th11: :: BHSP_5:11
for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
x .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)
proof
let X be RealUnitarySpace; ::_thesis: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity implies for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
x .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal) )
assume that
A1: ( the addF of X is commutative & the addF of X is associative ) and
A2: the addF of X is having_a_unity ; ::_thesis: for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
x .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)
let x be Point of X; ::_thesis: for S being finite OrthonormalFamily of X st not S is empty holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
x .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)
let S be finite OrthonormalFamily of X; ::_thesis: ( not S is empty implies for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
x .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal) )
assume A3: not S is empty ; ::_thesis: for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
x .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)
let H be Function of the carrier of X,REAL; ::_thesis: ( S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) implies for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
x .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal) )
assume that
A4: S c= dom H and
A5: for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ; ::_thesis: for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
x .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)
let F be Function of the carrier of X, the carrier of X; ::_thesis: ( S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) implies x .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal) )
assume that
A6: S c= dom F and
A7: for y being Point of X st y in S holds
F . y = (x .|. y) * y ; ::_thesis: x .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)
consider p being FinSequence of the carrier of X such that
A8: p is one-to-one and
A9: rng p = S and
A10: setopfunc (S, the carrier of X, the carrier of X,F, the addF of X) = the addF of X "**" (Func_Seq (F,p)) by A1, A2, A6, Def5;
A11: for y being Point of X st y in S holds
H . y = the scalar of X . [x,(F . y)]
proof
let y be Point of X; ::_thesis: ( y in S implies H . y = the scalar of X . [x,(F . y)] )
assume A12: y in S ; ::_thesis: H . y = the scalar of X . [x,(F . y)]
set a = x .|. y;
H . y = (x .|. y) ^2 by A5, A12
.= x .|. ((x .|. y) * y) by BHSP_1:3
.= the scalar of X . [x,((x .|. y) * y)] by BHSP_1:def_1
.= the scalar of X . [x,(F . y)] by A7, A12 ;
hence  H . y = the scalar of X . [x,(F . y)] ; ::_thesis: verum
end;
A13: setopfunc (S, the carrier of X,REAL,H,addreal) = addreal "**" (Func_Seq (H,p)) by A4, A8, A9, Def5;
 x .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = the scalar of X . [x,( the addF of X "**" (Func_Seq (F,p)))] by A10, BHSP_1:def_1;
hence  x .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal) by A3, A4, A6, A8, A9, A11, A13, Th10; ::_thesis: verum
end;

theorem Th12: :: BHSP_5:12
for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty holds
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
(setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)
proof
let X be RealUnitarySpace; ::_thesis: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity implies for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty holds
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
(setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal) )
assume that
A1: ( the addF of X is commutative & the addF of X is associative ) and
A2: the addF of X is having_a_unity ; ::_thesis: for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty holds
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
(setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)
let x be Point of X; ::_thesis: for S being finite OrthonormalFamily of X st not S is empty holds
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
(setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)
let S be finite OrthonormalFamily of X; ::_thesis: ( not S is empty implies for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
(setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal) )
assume A3: not S is empty ; ::_thesis: for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
(setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)
let F be Function of the carrier of X, the carrier of X; ::_thesis: ( S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) implies for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
(setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal) )
assume that
A4: S c= dom F and
A5: for y being Point of X st y in S holds
F . y = (x .|. y) * y ; ::_thesis: for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
(setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)
let H be Function of the carrier of X,REAL; ::_thesis: ( S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) implies (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal) )
assume that
A6: S c= dom H and
A7: for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ; ::_thesis: (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)
consider p being FinSequence of the carrier of X such that
A8: p is one-to-one and
A9: rng p = S and
A10: setopfunc (S, the carrier of X, the carrier of X,F, the addF of X) = the addF of X "**" (Func_Seq (F,p)) by A1, A2, A4, Def5;
A11: for y1, y2 being Point of X st y1 in S & y2 in S & y1 <> y2 holds
the scalar of X . [(F . y1),(F . y2)] = 0
proof
let y1, y2 be Point of X; ::_thesis: ( y1 in S & y2 in S & y1 <> y2 implies the scalar of X . [(F . y1),(F . y2)] = 0 )
assume that
A12: y1 in S and
A13: y2 in S and
A14: y1 <> y2 ; ::_thesis: the scalar of X . [(F . y1),(F . y2)] = 0
set z1 = x .|. y1;
set z2 = x .|. y2;
 S is OrthogonalFamily of X by Def9;
then A15: y1 .|. y2 = 0 by A12, A13, A14, Def8;
the scalar of X . [(F . y1),(F . y2)] = the scalar of X . [((x .|. y1) * y1),(F . y2)] by A5, A12
.= the scalar of X . [((x .|. y1) * y1),((x .|. y2) * y2)] by A5, A13
.= ((x .|. y1) * y1) .|. ((x .|. y2) * y2) by BHSP_1:def_1
.= (x .|. y2) * (y2 .|. ((x .|. y1) * y1)) by BHSP_1:3
.= (x .|. y2) * ((x .|. y1) * (y2 .|. y1)) by BHSP_1:3
.= 0 by A15 ;
hence  the scalar of X . [(F . y1),(F . y2)] = 0 ; ::_thesis: verum
end;
A16: for y being Point of X st y in S holds
H . y = the scalar of X . [(F . y),(F . y)]
proof
let y be Point of X; ::_thesis: ( y in S implies H . y = the scalar of X . [(F . y),(F . y)] )
assume A17: y in S ; ::_thesis: H . y = the scalar of X . [(F . y),(F . y)]
then A18: F . y = (x .|. y) * y by A5;
H . y = (x .|. y) ^2 by A7, A17
.= ((x .|. y) * (x .|. y)) * 1
.= ((x .|. y) * (x .|. y)) * (y .|. y) by A17, Def9
.= (x .|. y) * ((x .|. y) * (y .|. y))
.= (x .|. y) * (((x .|. y) * y) .|. y) by BHSP_1:3
.= ((x .|. y) * y) .|. ((x .|. y) * y) by BHSP_1:3
.= the scalar of X . [(F . y),(F . y)] by A18, BHSP_1:def_1 ;
hence  H . y = the scalar of X . [(F . y),(F . y)] ; ::_thesis: verum
end;
(setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = the scalar of X . [( the addF of X "**" (Func_Seq (F,p))),( the addF of X "**" (Func_Seq (F,p)))] by A10, BHSP_1:def_1
.= addreal "**" (Func_Seq (H,p)) by A3, A4, A6, A8, A9, A11, A16, Th9
.= setopfunc (S, the carrier of X,REAL,H,addreal) by A6, A8, A9, Def5 ;
hence  (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal) ; ::_thesis: verum
end;

theorem :: BHSP_5:13
for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2
proof
let X be RealUnitarySpace; ::_thesis: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity implies for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2 )
assume that
A1: ( the addF of X is commutative & the addF of X is associative ) and
A2: the addF of X is having_a_unity ; ::_thesis: for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2
let x be Point of X; ::_thesis: for S being finite OrthonormalFamily of X st not S is empty holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2
let S be finite OrthonormalFamily of X; ::_thesis: ( not S is empty implies for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2 )
assume A3: not S is empty ; ::_thesis: for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2
let H be Function of the carrier of X,REAL; ::_thesis: ( S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) implies setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2 )
assume that
A4: S c= dom H and
A5: for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ; ::_thesis: setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2
now__::_thesis:_0_<=_(x_.|._x)_-_(setopfunc_(S,_the_carrier_of_X,REAL,H,addreal))
deffunc H1( set ) ->  set = the Mult of X . [( the scalar of X . [x,$1]),$1];
A6: for y being set st y in the carrier of X holds
H1(y) in the carrier of X
proof
let y be set ; ::_thesis: ( y in the carrier of X implies H1(y) in the carrier of X )
assume A7: y in the carrier of X ; ::_thesis: H1(y) in the carrier of X
reconsider y1 = y as Point of X by A7;
set x1 = x;
 the scalar of X . [x,y] = x .|. y1 by BHSP_1:def_1;
then reconsider a = the scalar of X . [x,y] as Real ;
reconsider y2 = y as VECTOR of X by A7;
 the Mult of X . (( the scalar of X . [x,y]),y) = a * y2 ;
hence  H1(y) in the carrier of X ; ::_thesis: verum
end;
 ex F0 being Function of the carrier of X, the carrier of X st
for y being set st y in the carrier of X holds
F0 . y = H1(y) from FUNCT_2:sch_2(A6);
then consider F0 being Function of the carrier of X, the carrier of X such that
A8: for y being set st y in the carrier of X holds
F0 . y = the Mult of X . [( the scalar of X . [x,y]),y] ;
A9: dom F0 = the carrier of X by FUNCT_2:def_1;
now__::_thesis:_for_y_being_Point_of_X_st_y_in_S_holds_
F0_._y_=_(x_.|._y)_*_y
let y be Point of X; ::_thesis: ( y in S implies F0 . y = (x .|. y) * y )
assume  y in S ; ::_thesis: F0 . y = (x .|. y) * y
thus F0 . y = the Mult of X . [( the scalar of X . [x,y]),y] by A8
.= (x .|. y) * y by BHSP_1:def_1 ; ::_thesis: verum
end;
then consider F being Function of the carrier of X, the carrier of X such that
A10: S c= dom F and
A11: for y being Point of X st y in S holds
F . y = (x .|. y) * y by A9;
set z = setopfunc (S, the carrier of X, the carrier of X,F, the addF of X);
 (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. x = setopfunc (S, the carrier of X,REAL,H,addreal) by A1, A2, A3, A4, A5, A10, A11, Th11;
then  x .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) by A1, A2, A3, A4, A5, A10, A11, Th12;
then (x - (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X))) .|. (x - (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X))) = (((x .|. x) - ((setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)))) - ((setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)))) + ((setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X))) by BHSP_1:13
.= (x .|. x) - (setopfunc (S, the carrier of X,REAL,H,addreal)) by A1, A2, A3, A4, A5, A10, A11, Th12 ;
hence  0 <= (x .|. x) - (setopfunc (S, the carrier of X,REAL,H,addreal)) by BHSP_1:def_2; ::_thesis: verum
end;
then A12: 0 + (setopfunc (S, the carrier of X,REAL,H,addreal)) <= x .|. x by XREAL_1:19;
 0 <= x .|. x by BHSP_1:def_2;
then  setopfunc (S, the carrier of X,REAL,H,addreal) <= (sqrt (x .|. x)) ^2 by A12, SQUARE_1:def_2;
hence  setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2 by BHSP_1:def_4; ::_thesis: verum
end;

theorem :: BHSP_5:14
for DK, DX being non empty set
for f being BinOp of DK st f is commutative & f is associative & f is having_a_unity holds
for Y1, Y2 being finite Subset of DX st Y1 misses Y2 holds
for F being Function of DX,DK st Y1 c= dom F & Y2 c= dom F holds
for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f)))
proof
let DK, DX be non empty set ; ::_thesis: for f being BinOp of DK st f is commutative & f is associative & f is having_a_unity holds
for Y1, Y2 being finite Subset of DX st Y1 misses Y2 holds
for F being Function of DX,DK st Y1 c= dom F & Y2 c= dom F holds
for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f)))
let f be BinOp of DK; ::_thesis: ( f is commutative & f is associative & f is having_a_unity implies for Y1, Y2 being finite Subset of DX st Y1 misses Y2 holds
for F being Function of DX,DK st Y1 c= dom F & Y2 c= dom F holds
for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f))) )
assume that
A1: ( f is commutative & f is associative ) and
A2: f is having_a_unity ; ::_thesis: for Y1, Y2 being finite Subset of DX st Y1 misses Y2 holds
for F being Function of DX,DK st Y1 c= dom F & Y2 c= dom F holds
for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f)))
let Y1, Y2 be finite Subset of DX; ::_thesis: ( Y1 misses Y2 implies for F being Function of DX,DK st Y1 c= dom F & Y2 c= dom F holds
for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f))) )
assume A3: Y1 misses Y2 ; ::_thesis: for F being Function of DX,DK st Y1 c= dom F & Y2 c= dom F holds
for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f)))
let F be Function of DX,DK; ::_thesis: ( Y1 c= dom F & Y2 c= dom F implies for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f))) )
assume that
A4: Y1 c= dom F and
A5: Y2 c= dom F ; ::_thesis: for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f)))
let Z be finite Subset of DX; ::_thesis: ( Z = Y1 \/ Y2 implies setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f))) )
assume A6: Z = Y1 \/ Y2 ; ::_thesis: setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f)))
then A7: Z c= dom F by A4, A5, XBOOLE_1:8;
consider p1 being FinSequence of DX such that
A8: p1 is one-to-one and
A9: rng p1 = Y1 and
A10: setopfunc (Y1,DX,DK,F,f) = f "**" (Func_Seq (F,p1)) by A1, A2, A4, Def5;
consider p2 being FinSequence of DX such that
A11: p2 is one-to-one and
A12: rng p2 = Y2 and
A13: setopfunc (Y2,DX,DK,F,f) = f "**" (Func_Seq (F,p2)) by A1, A2, A5, Def5;
set q = p1 ^ p2;
A14: p1 ^ p2 is one-to-one by A3, A8, A9, A11, A12, FINSEQ_3:91;
 rng (p1 ^ p2) = Z by A6, A9, A12, FINSEQ_1:31;
then A15: setopfunc (Z,DX,DK,F,f) = f "**" (Func_Seq (F,(p1 ^ p2))) by A1, A2, A7, A14, Def5;
 ex fp1, fp2 being FinSequence st
( fp1 = F * p1 & fp2 = F * p2 & F * (p1 ^ p2) = fp1 ^ fp2 ) by A4, A5, A6, A9, A12, HILBASIS:1, XBOOLE_1:8;
hence  setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f))) by A1, A2, A10, A13, A15, FINSOP_1:5; ::_thesis: verum
end;