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 ;
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
.= 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 ;
defpred S1[ Nat] means ( 1 <= \$1 & \$1 <= len q implies g . \$1 = L . (f . \$1) );
A11: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
A12: n in NAT by ORDINAL1:def 12;
assume A13: S1[n] ; :: thesis: S1[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 ;
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 ;
reconsider z = f . n as Element of X ;
reconsider z1 = z as VECTOR of X ;
A20: n + 1 in dom q by ;
then p . (n + 1) in rng p by ;
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 ;
hence g . (n + 1) = addreal . ((g . n),(q . (n + 1))) by
.= addreal . ((L . (f . n)),(L . y)) by
.= (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 S1[n + 1] ; :: thesis: verum
end;
A22: S1[ 0 ] ;
for n being Nat holds S1[n] from hence L . ( the addF of X "**" p) = addreal "**" q by A1, A4, A7, A10; :: thesis: verum