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

let xd be object ; :: 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:2;

now :: thesis: for xd being object holds
( xd in dom (Func_Seq (H,p)) iff xd in dom p )

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