let n be Nat; :: thesis: for F being FinSequence of ()
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 (); :: 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 S1[ Nat] means ( \$1 <= len F implies f . \$1 = fv . \$1 );
A8: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A9: S1[i] ; :: thesis: S1[i + 1]
set i1 = i + 1;
A10: the carrier of () = the carrier of ()
proof
thus the carrier of () = REAL n by MATRIX13:102
.= the carrier of () by EUCLID:22 ; :: thesis: verum
end;
the carrier of () = n -tuples_on the carrier of F_Real by MATRIX13:102;
then reconsider Fvi1 = Fv /. (i + 1), fvi = fv . i as Element of n -tuples_on the carrier of F_Real by ;
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 ;
then F . (i + 1) = F /. (i + 1) by PARTFUN1:def 6;
then A14: f . (i + 1) = (f . i) + Fi1 by ;
A15: Fv /. (i + 1) = Fv . (i + 1) by ;
then Fvi1 = F /. (i + 1) by ;
hence f . (i + 1) = (fv . i) + (Fv /. (i + 1)) by
.= fv . (i + 1) by ;
:: thesis: verum
end;
A16: S1[ 0 ] by A3, A6, Lm2;
for n being Nat holds S1[n] from NAT_1:sch 2(A16, A8);
hence Sum F = Sum Fv by A1, A2, A5; :: thesis: verum