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 Function of NAT ,REAL such that
A2: ( e1 . 0 = 0 & ( for i being Nat st i < len e holds
e1 . (i + 1) = (e1 . i) + (e . (i + 1)) ) & Sum e = e1 . (len e) ) by Th7;
consider f1 being Function of NAT ,the carrier of F_Real such that
A3: ( Sum f = f1 . (len f) & f1 . 0 = 0. F_Real & ( for j being Element of 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 13;
for n being Nat st n <= len e holds
e1 . n = f1 . n

proof

let n be Nat; :: thesis: ( n <= len e implies e1 . n = f1 . n )
defpred S₁[ Nat] means ( $1 <= len e implies e1 . $1 = f1 . $1 );
A4: S₁[ 0 ] by A2, A3, STRUCT_0:def 6, VECTSP_1:def 15;

A5: now

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

now

assume k + 1 <= len e ; :: thesis: e1 . (k + 1) = f1 . (k + 1)
then A7: k < len e by NAT_1:13;
reconsider a = e . (k + 1) as Element of F_Real by VECTSP_1:def 15;
reconsider k' = k as Element of NAT by ORDINAL1:def 13;
e1 . (k + 1) = (f1 . k') + a by A2, A6, A7
.= f1 . (k + 1) by A1, A3, A7 ;
hence e1 . (k + 1) = f1 . (k + 1) ; :: thesis: verum

end;

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

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A5);
hence ( n <= len e implies e1 . n = f1 . n ) ; :: thesis: verum

end;

hence Sum e = Sum f by A1, A2, A3; :: thesis: verum