let Z be complex-valued FinSequence; :: thesis: for E being FinSequence of F_Complex st E = Z holds
Sum Z = Sum E

let E be FinSequence of F_Complex; :: thesis: ( E = Z implies Sum Z = Sum E )
assume A1: E = Z ; :: thesis: 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 ;
A5: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
set n1 = n + 1;
assume A6: ( S1[n] & n + 1 <= len Z ) ; :: thesis: Sum (Z | (n + 1)) = f . (n + 1)
A7: n + 1 in dom Z by ;
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 ;
then reconsider E1n1 = E1 . (n + 1) as Element of F_Complex ;
f . (n + 1) = (f . n) + E1n1 by ;
hence Sum (Z | (n + 1)) = f . (n + 1) by ; :: thesis: 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; :: thesis: verum