let X be RealUnitarySpace; :: thesis:
let x be Point of X; :: thesis:
let S be non empty finite Subset of X; :: thesis:
let F be Function of the carrier of X,the carrier of X; :: thesis:
assume A1: S c= dom F ; :: thesis:
let H be Function of the carrier of X,REAL ; :: thesis:
assume A2: ( S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [x,(F . y)] ) ) ; :: thesis:
let p be FinSequence of the carrier of X; :: thesis:
assume A3: ( p is one-to-one & rng p = S ) ; :: thesis:
set p1 = Func_Seq F,p;
set q1 = Func_Seq H,p;

let xd be set ; :: thesis:
( 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, A3, FUNCT_1:21; :: thesis:

end;

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

let xd be set ; :: thesis:
( 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, A3, FUNCT_1:21; :: thesis:

end;

then A5: dom (Func_Seq H,p) = dom p by TARSKI:2;
A6: 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)]

let i be Element of NAT ; :: thesis:
assume A7: i in dom (Func_Seq F,p) ; :: thesis:
A8: p . i in S by A3, A4, A7, FUNCT_1:12;
(Func_Seq H,p) . i = H . (p . i) by A4, A7, FUNCT_1:23
.= the scalar of X . [x,(F . (p . i))] by A2, A8
.= the scalar of X . [x,((Func_Seq F,p) . i)] by A4, A7, FUNCT_1:23 ;
hence (Func_Seq H,p) . i = the scalar of X . [x,((Func_Seq F,p) . i)] ; :: thesis:

end;

len (Func_Seq F,p) >= 1

A9: 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 ;
A10: 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 len (Func_Seq F,p) >= 1 by A9, A10, FINSEQ_1:8; :: thesis:

end;

then x .|. (the addF of X "**" (Func_Seq F,p)) = addreal "**" (Func_Seq H,p) by A4, A5, A6, 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: