let e be FinSequence of REAL ; :: thesis: for f being FinSequence of F_Real st e = f holds
Sum e = Sum f
let f be FinSequence of F_Real; :: thesis: ( e = f implies Sum e = Sum f )
assume A1: e = f ; :: thesis: Sum e = Sum f
consider e1 being sequence of REAL such that
A2: e1 . 0 = 0 and
A3: for i being Nat st i < len e holds
e1 . (i + 1) = (e1 . i) + (e . (i + 1)) and
A4: Sum e = e1 . (len e) by Th7;
consider f1 being sequence of the carrier of F_Real such that
A5: Sum f = f1 . (len f) and
A6: f1 . 0 = 0. F_Real and
A7: for j being Nat
for v being Element of F_Real st j < len f & v = f . (j + 1) holds
f1 . (j + 1) = (f1 . j) + v by RLVECT_1:def 12;
for n being Nat st n <= len e holds
e1 . n = f1 . n

proof

defpred S₁[ Nat] means ( $1 <= len e implies e1 . $1 = f1 . $1 );
let n be Nat; :: thesis: ( n <= len e implies e1 . n = f1 . n )

A8: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: ( k + 1 <= len e implies e1 . (k + 1) = f1 . (k + 1) )

reconsider k9 = k as Element of NAT by ORDINAL1:def 12;
e . (k + 1) in REAL by XREAL_0:def 1;
then reconsider a = e . (k + 1) as Element of F_Real by VECTSP_1:def 5;
assume k + 1 <= len e ; :: thesis: e1 . (k + 1) = f1 . (k + 1)
then A10: k < len e by NAT_1:13;
then e1 . (k + 1) = (f1 . k9) + a by A3, A9
.= f1 . (k + 1) by A1, A7, A10 ;
hence e1 . (k + 1) = f1 . (k + 1) ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A11: S₁[ 0 ] by A2, A6, STRUCT_0:def 6, VECTSP_1:def 5;
for n being Nat holds S₁[n] from NAT_1:sch 2(A11, A8);
hence ( n <= len e implies e1 . n = f1 . n ) ; :: thesis: verum

end;

hence Sum e = Sum f by A1, A4, A5; :: thesis: verum