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

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:12;
hence ( xd in dom (Func_Seq F,p) iff xd in dom p ) by A1, A5, FUNCT_1:21; :: thesis: verum

end;

then A6: dom (Func_Seq F,p) = dom p by TARSKI:2;

now

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

end;

then A7: dom (Func_Seq H,p) = dom p by TARSKI:2;
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:12;
(Func_Seq H,p) . i = H . (p . i) by A6, A9, FUNCT_1:23
.= 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:23 ;
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:77;
0 < card S by NAT_1:3;
then 0 + 1 <= card S by INT_1:20;
then len (Func_Seq F,p) >= 1 by A11, A12, FINSEQ_1:8;
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