let n be Nat; for Ft being FinSequence of (TOP-REAL n)
for Fr being FinSequence of (REAL-NS n) st Ft = Fr holds
Sum Ft = Sum Fr
let F be FinSequence of (TOP-REAL n); for Fr being FinSequence of (REAL-NS n) st F = Fr holds
Sum F = Sum Fr
let Fv be FinSequence of (REAL-NS n); ( F = Fv implies Sum F = Sum Fv )
assume A1:
F = Fv
; Sum F = Sum Fv
set T = TOP-REAL n;
set V = REAL-NS n;
consider f being sequence of the carrier of (TOP-REAL n) such that
A2:
Sum F = f . (len F)
and
A3:
f . 0 = 0. (TOP-REAL n)
and
A4:
for j being Nat
for v being Element of (TOP-REAL n) 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 (REAL-NS n) such that
A5:
Sum Fv = fv . (len Fv)
and
A6:
fv . 0 = 0. (REAL-NS n)
and
A7:
for j being Nat
for v being Element of (REAL-NS 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;
( S1[i] implies S1[i + 1] )
assume A9:
S1[
i]
;
S1[i + 1]
assume A10:
i + 1
<= len F
;
f . (i + 1) = fv . (i + 1)
then A11:
i + 1
in dom F
by NAT_1:11, FINSEQ_3:25;
then
F . (i + 1) = F /. (i + 1)
by PARTFUN1:def 6;
then A12:
f . (i + 1) = (f . i) + (F /. (i + 1))
by A4, A10, NAT_1:13;
A13:
Fv /. (i + 1) = Fv . (i + 1)
by A1, A11, PARTFUN1:def 6;
then
Fv /. (i + 1) = F /. (i + 1)
by A1, A11, PARTFUN1:def 6;
hence f . (i + 1) =
(fv . i) + (Fv /. (i + 1))
by A9, A10, A12, Th7, NAT_1:13
.=
fv . (i + 1)
by A1, A7, A10, A13, NAT_1:13
;
verum
end;
A14:
S1[ 0 ]
by A3, A6, Th6;
for n being Nat holds S1[n]
from NAT_1:sch 2(A14, A8);
hence
Sum F = Sum Fv
by A1, A2, A5; verum