let Z be complex-valued FinSequence; for E being FinSequence of F_Complex st E = Z holds
Sum Z = Sum E
let E be FinSequence of F_Complex; ( E = Z implies Sum Z = Sum E )
assume A1:
E = Z
; Sum Z = Sum E
consider f being sequence of F_Complex such that
A2:
( Sum E = f . (len E) & f . 0 = 0. F_Complex )
and
A3:
for j being Nat
for v being Element of F_Complex st j < len E & v = E . (j + 1) holds
f . (j + 1) = (f . j) + v
by RLVECT_1:def 12;
reconsider E1 = E as FinSequence of F_Complex ;
defpred S1[ Nat] means ( $1 <= len Z implies Sum (Z | $1) = f . $1 );
A4:
S1[ 0 ]
by A2, RVSUM_2:29, COMPLFLD:7;
A5:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
set n1 =
n + 1;
assume A6:
(
S1[
n] &
n + 1
<= len Z )
;
Sum (Z | (n + 1)) = f . (n + 1)
A7:
n + 1
in dom Z
by A6, NAT_1:11, FINSEQ_3:25;
then A8:
Z | (n + 1) = (Z | n) ^ <*(Z . (n + 1))*>
by FINSEQ_5:10;
(
E1 . (n + 1) in rng E1 &
rng E1 c= the
carrier of
F_Complex )
by A7, A1, FUNCT_1:def 3;
then reconsider E1n1 =
E1 . (n + 1) as
Element of
F_Complex ;
f . (n + 1) = (f . n) + E1n1
by A1, A3, A6, NAT_1:13;
hence
Sum (Z | (n + 1)) = f . (n + 1)
by A8, A1, NAT_1:13, A6, RVSUM_2:31;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A4, A5);
then
( S1[ len Z] & Z | (len Z) = Z )
;
hence
Sum Z = Sum E
by A2, A1; verum