let X be RealUnitarySpace; :: thesis: for L being linear-Functional of X
for p being FinSequence of the carrier of X st len p >= 1 holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Nat st i in dom q holds
q . i = L . (p . i) ) holds
L . ( the addF of X "**" p) = addreal "**" q
let L be linear-Functional of X; :: thesis: for p being FinSequence of the carrier of X st len p >= 1 holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Nat st i in dom q holds
q . i = L . (p . i) ) holds
L . ( the addF of X "**" p) = addreal "**" q
let p be FinSequence of the carrier of X; :: thesis: ( len p >= 1 implies for q being FinSequence of REAL st dom p = dom q & ( for i being Nat st i in dom q holds
q . i = L . (p . i) ) holds
L . ( the addF of X "**" p) = addreal "**" q )
assume A1: len p >= 1 ; :: thesis: for q being FinSequence of REAL st dom p = dom q & ( for i being Nat st i in dom q holds
q . i = L . (p . i) ) holds
L . ( the addF of X "**" p) = addreal "**" q
consider f being sequence of the carrier of X such that
A2: f . 1 = p . 1 and
A3: for n being Nat st 0 <> n & n < len p holds
f . (n + 1) = the addF of X . ((f . n),(p . (n + 1))) and
A4: the addF of X "**" p = f . (len p) by A1, FINSOP_1:1;
let q be FinSequence of REAL ; :: thesis: ( dom p = dom q & ( for i being Nat st i in dom q holds
q . i = L . (p . i) ) implies L . ( the addF of X "**" p) = addreal "**" q )
assume that
A5: dom p = dom q and
A6: for i being Nat st i in dom q holds
q . i = L . (p . i) ; :: thesis: L . ( the addF of X "**" p) = addreal "**" q
Seg (len q) = dom p by A5, FINSEQ_1:def 3
.= Seg (len p) by FINSEQ_1:def 3 ;
then A7: len q = len p by FINSEQ_1:6;
then consider g being sequence of REAL such that
A8: g . 1 = q . 1 and
A9: for n being Nat st 0 <> n & n < len q holds
g . (n + 1) = addreal . ((g . n),(q . (n + 1))) and
A10: addreal "**" q = g . (len q) by A1, FINSOP_1:1;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len q implies g . $1 = L . (f . $1) );

A11: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
A12: n in NAT by ORDINAL1:def 12;
assume A13: S₁[n] ; :: thesis: S₁[n + 1]

now :: thesis: ( 1 <= n + 1 & n + 1 <= len q implies g . (n + 1) = L . (f . (n + 1)) )

A14: n <= n + 1 by NAT_1:11;
assume that
A15: 1 <= n + 1 and
A16: n + 1 <= len q ; :: thesis: g . (n + 1) = L . (f . (n + 1))

per cases ( n = 0 or n <> 0 ) ;

suppose A17: n = 0 ; :: thesis: g . (n + 1) = L . (f . (n + 1))

1 in dom p by A1, FINSEQ_3:25;
hence g . (n + 1) = L . (f . (n + 1)) by A5, A6, A2, A8, A17; :: thesis: verum

end;

suppose A18: n <> 0 ; :: thesis: g . (n + 1) = L . (f . (n + 1))

then A19: 0 + 1 <= n by INT_1:7, A12;
reconsider z = f . n as Element of X ;
reconsider z1 = z as VECTOR of X ;
A20: n + 1 in dom q by A15, A16, FINSEQ_3:25;
then p . (n + 1) in rng p by A5, FUNCT_1:3;
then reconsider y = p . (n + 1) as Element of X ;
reconsider y1 = y as VECTOR of X ;
set Lz = L . z1;
set Ly = L . y1;
A21: (n + 1) - 1 < (len q) - 0 by A16, XREAL_1:15;
hence g . (n + 1) = addreal . ((g . n),(q . (n + 1))) by A9, A18
.= addreal . ((L . (f . n)),(L . y)) by A6, A13, A16, A14, A19, A20, XXREAL_0:2
.= (L . z1) + (L . y1) by BINOP_2:def 9
.= L . (z1 + y1) by HAHNBAN:def 2
.= L . (f . (n + 1)) by A3, A7, A18, A21 ;
:: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A22: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A22, A11);
hence L . ( the addF of X "**" p) = addreal "**" q by A1, A4, A7, A10; :: thesis: verum