let n be Nat; :: thesis: for F being FinSequence of (TOP-REAL n)

for Fv being FinSequence of (RealVectSpace (Seg n)) st Fv = F holds

Sum F = Sum Fv

set T = TOP-REAL n;

set V = RealVectSpace (Seg n);

let F be FinSequence of (TOP-REAL n); :: thesis: for Fv being FinSequence of (RealVectSpace (Seg n)) st Fv = F holds

Sum F = Sum Fv

let Fv be FinSequence of (RealVectSpace (Seg n)); :: thesis: ( Fv = F implies Sum F = Sum Fv )

assume A1: Fv = F ; :: thesis: Sum F = Sum Fv

reconsider T = TOP-REAL n as RealLinearSpace ;

consider f being sequence of the carrier of T such that

A2: Sum F = f . (len F) and

A3: f . 0 = 0. T and

A4: for j being Nat

for v being Element of T st j < len F & v = F . (j + 1) holds

f . (j + 1) = (f . j) + v by RLVECT_1:def 12;

consider fv being sequence of the carrier of (RealVectSpace (Seg n)) such that

A5: Sum Fv = fv . (len Fv) and

A6: fv . 0 = 0. (RealVectSpace (Seg n)) and

A7: for j being Nat

for v being Element of (RealVectSpace (Seg n)) st j < len Fv & v = Fv . (j + 1) holds

fv . (j + 1) = (fv . j) + v by RLVECT_1:def 12;

defpred S_{1}[ Nat] means ( $1 <= len F implies f . $1 = fv . $1 );

A8: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[ 0 ]
by A3, A6, Lm2;

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

hence Sum F = Sum Fv by A1, A2, A5; :: thesis: verum

for Fv being FinSequence of (RealVectSpace (Seg n)) st Fv = F holds

Sum F = Sum Fv

set T = TOP-REAL n;

set V = RealVectSpace (Seg n);

let F be FinSequence of (TOP-REAL n); :: thesis: for Fv being FinSequence of (RealVectSpace (Seg n)) st Fv = F holds

Sum F = Sum Fv

let Fv be FinSequence of (RealVectSpace (Seg n)); :: thesis: ( Fv = F implies Sum F = Sum Fv )

assume A1: Fv = F ; :: thesis: Sum F = Sum Fv

reconsider T = TOP-REAL n as RealLinearSpace ;

consider f being sequence of the carrier of T such that

A2: Sum F = f . (len F) and

A3: f . 0 = 0. T and

A4: for j being Nat

for v being Element of T st j < len F & v = F . (j + 1) holds

f . (j + 1) = (f . j) + v by RLVECT_1:def 12;

consider fv being sequence of the carrier of (RealVectSpace (Seg n)) such that

A5: Sum Fv = fv . (len Fv) and

A6: fv . 0 = 0. (RealVectSpace (Seg n)) and

A7: for j being Nat

for v being Element of (RealVectSpace (Seg n)) st j < len Fv & v = Fv . (j + 1) holds

fv . (j + 1) = (fv . j) + v by RLVECT_1:def 12;

defpred S

A8: for i being Nat st S

S

proof

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

assume A9: S_{1}[i]
; :: thesis: S_{1}[i + 1]

set i1 = i + 1;

A10: the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)

then reconsider Fvi1 = Fv /. (i + 1), fvi = fv . i as Element of n -tuples_on the carrier of F_Real by A10, Lm1;

reconsider Fi1 = F /. (i + 1) as Element of T ;

assume A11: i + 1 <= len F ; :: thesis: f . (i + 1) = fv . (i + 1)

A13: i + 1 in dom F by A11, NAT_1:11, FINSEQ_3:25;

then F . (i + 1) = F /. (i + 1) by PARTFUN1:def 6;

then A14: f . (i + 1) = (f . i) + Fi1 by A4, A11, NAT_1:13;

A15: Fv /. (i + 1) = Fv . (i + 1) by A1, A13, PARTFUN1:def 6;

then Fvi1 = F /. (i + 1) by A1, A13, PARTFUN1:def 6;

hence f . (i + 1) = (fv . i) + (Fv /. (i + 1)) by A9, A11, A14, EUCLID:64, NAT_1:13

.= fv . (i + 1) by A1, A7, A11, NAT_1:13, A15 ;

:: thesis: verum

end;assume A9: S

set i1 = i + 1;

A10: the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)

proof

the carrier of (n -VectSp_over F_Real) = n -tuples_on the carrier of F_Real
by MATRIX13:102;
thus the carrier of (n -VectSp_over F_Real) =
REAL n
by MATRIX13:102

.= the carrier of (TOP-REAL n) by EUCLID:22 ; :: thesis: verum

end;.= the carrier of (TOP-REAL n) by EUCLID:22 ; :: thesis: verum

then reconsider Fvi1 = Fv /. (i + 1), fvi = fv . i as Element of n -tuples_on the carrier of F_Real by A10, Lm1;

reconsider Fi1 = F /. (i + 1) as Element of T ;

assume A11: i + 1 <= len F ; :: thesis: f . (i + 1) = fv . (i + 1)

A13: i + 1 in dom F by A11, NAT_1:11, FINSEQ_3:25;

then F . (i + 1) = F /. (i + 1) by PARTFUN1:def 6;

then A14: f . (i + 1) = (f . i) + Fi1 by A4, A11, NAT_1:13;

A15: Fv /. (i + 1) = Fv . (i + 1) by A1, A13, PARTFUN1:def 6;

then Fvi1 = F /. (i + 1) by A1, A13, PARTFUN1:def 6;

hence f . (i + 1) = (fv . i) + (Fv /. (i + 1)) by A9, A11, A14, EUCLID:64, NAT_1:13

.= fv . (i + 1) by A1, A7, A11, NAT_1:13, A15 ;

:: thesis: verum

for n being Nat holds S

hence Sum F = Sum Fv by A1, A2, A5; :: thesis: verum