let n be Nat; :: thesis:
set T = TOP-REAL n;
set V = n -VectSp_over F_Real;
let F be FinSequence of (TOP-REAL n); :: thesis:
let Fv be FinSequence of (n -VectSp_over F_Real); :: thesis:
assume A1: Fv = F ; :: thesis:
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 (n -VectSp_over F_Real) such that
A5: Sum Fv = fv . (len Fv) and
A6: fv . 0 = 0. (n -VectSp_over F_Real) and
A7: for j being Nat
for v being Element of (n -VectSp_over F_Real) st j < len Fv & v = Fv . (j + 1) holds
fv . (j + 1) = (fv . j) + v by RLVECT_1:def 12;
defpred S₁[ Nat] means ( $1 <= len F implies f . $1 = fv . $1 );
A8: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis:
assume A9: S₁[i] ; :: thesis:
set i1 = i + 1;
reconsider Fvi1 = Fv /. (i + 1), fvi = fv . i as Element of n -tuples_on the carrier of F_Real by MATRIX13:102;
A10: ( @ (@ Fvi1) = Fvi1 & @ (@ fvi) = fvi ) ;
reconsider Fi1 = F /. (i + 1) as Element of T ;
assume A11: i + 1 <= len F ; :: thesis:
then A12: i < len F by NAT_1:13;
1 <= i + 1 by NAT_1:11;
then A13: i + 1 in dom F by A11, FINSEQ_3:25;
then F . (i + 1) = F /. (i + 1) by PARTFUN1:def 6;
then A14: f . (i + 1) = (f . i) + Fi1 by A4, A12;
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) = (@ fvi) + (@ Fvi1) by A9, A11, A14, EUCLID:64, NAT_1:13
.= fvi + Fvi1 by A10, MATRTOP1:1
.= (fv . i) + (Fv /. (i + 1)) by MATRIX13:102
.= fv . (i + 1) by A1, A7, A12, A15 ;
:: thesis:

end;