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 A1: ( 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 ) ) ; :: 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 A2: ( 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)] ) ) ; :: 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 A3: ( p is one-to-one & 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, A3, FUNCT_1:21; :: thesis: verum

end;

then A4: dom (Func_Seq F,p) = dom p by TARSKI:2;
A5: 1 <= len (Func_Seq F,p)

proof

A6: Seg (len p) = dom (Func_Seq F,p) by A4, FINSEQ_1:def 3
.= Seg (len (Func_Seq F,p)) by FINSEQ_1:def 3 ;
A7: len p = card S by A3, FINSEQ_4:77;
0 < card S by NAT_1:3;
then 0 + 1 <= card S by INT_1:20;
hence 1 <= len (Func_Seq F,p) by A6, A7, FINSEQ_1:8; :: thesis: verum

end;

A8: 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 A9: ( i in dom (Func_Seq F,p) & j in dom (Func_Seq F,p) & i <> j ) ; :: thesis: the scalar of X . [((Func_Seq F,p) . i),((Func_Seq F,p) . j)] = 0
then A10: p . i in S by A3, A4, FUNCT_1:12;
A11: p . j in S by A3, A4, A9, FUNCT_1:12;
A12: ( (Func_Seq F,p) . i = F . (p . i) & (Func_Seq F,p) . j = F . (p . j) ) by A9, FUNCT_1:22;
p . i <> p . j by A3, A4, A9, FUNCT_1:def 8;
hence the scalar of X . [((Func_Seq F,p) . i),((Func_Seq F,p) . j)] = 0 by A1, A10, A11, A12; :: 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 A2, A3, FUNCT_1:21; :: thesis: verum

end;

then A13: dom (Func_Seq H,p) = dom p by TARSKI:2;
A14: 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 A15: 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)]
A16: p . i in S by A3, A13, A15, FUNCT_1:12;
(Func_Seq H,p) . i = H . (p . i) by A13, A15, FUNCT_1:23
.= the scalar of X . [(F . (p . i)),(F . (p . i))] by A2, A16
.= the scalar of X . [((F * p) . i),(F . (p . i))] by A13, A15, FUNCT_1:23
.= the scalar of X . [((Func_Seq F,p) . i),((Func_Seq F,p) . i)] by A13, A15, 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 A4, A5, A8, A13, A14, 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