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

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:12;
hence ( z in dom (Func_Seq F,p) iff z in dom p ) by A1, A6, FUNCT_1:21; :: 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:77;
0 < card S by NAT_1:3;
then 0 + 1 <= card S by INT_1:20;
then A10: 1 <= len (Func_Seq F,p) by A8, A9, FINSEQ_1:8;
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:12;
A16: p . j in S by A6, A7, A13, FUNCT_1:12;
A17: (Func_Seq F,p) . i = F . (p . i) by A12, FUNCT_1:22;
A18: (Func_Seq F,p) . j = F . (p . j) by A13, FUNCT_1:22;
p . i <> p . j by A5, A7, A12, A13, A14, FUNCT_1:def 8;
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

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:12;
hence ( z in dom (Func_Seq H,p) iff z in dom p ) by A3, A6, FUNCT_1:21; :: thesis: verum

end;

then A19: dom (Func_Seq H,p) = dom p by TARSKI:2;
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:12;
(Func_Seq H,p) . i = H . (p . i) by A19, A21, FUNCT_1:23
.= 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:23
.= the scalar of X . [((Func_Seq F,p) . i),((Func_Seq F,p) . i)] by A19, A21, FUNCT_1:23 ;
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