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_{1}[ Nat] means ( 1 <= $1 & $1 <= len q implies g . $1 = L . (f . $1) );

_{1}[ 0 ]
;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A22, A11);

hence L . ( the addF of X "**" p) = addreal "**" q by A1, A4, A7, A10; :: thesis: verum

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

A11: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

A22:
SS

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

A12: n in NAT by ORDINAL1:def 12;

assume A13: S_{1}[n]
; :: thesis: S_{1}[n + 1]

_{1}[n + 1]
; :: thesis: verum

end;A12: n in NAT by ORDINAL1:def 12;

assume A13: S

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

hence
SA14:
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))

end;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 )
;

end;

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;hence g . (n + 1) = L . (f . (n + 1)) by A5, A6, A2, A8, A17; :: thesis: verum

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;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

for n being Nat holds S

hence L . ( the addF of X "**" p) = addreal "**" q by A1, A4, A7, A10; :: thesis: verum