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 object holds
( z in dom (Func_Seq (F,p)) iff z in dom p )

let z be object ; :: 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:2;
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 ;
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 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 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 object holds
( z in dom (Func_Seq (H,p)) iff z in dom p )

let z be object ; :: 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:2;
A20: for i being 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 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