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 S_{1}[ Nat] means ( $1 <= len Z implies Sum (Z | $1) = f . $1 );

A4: S_{1}[ 0 ]
by A2, RVSUM_2:29, COMPLFLD:7;

A5: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A4, A5);

then ( S_{1}[ len Z] & Z | (len Z) = Z )
;

hence Sum Z = Sum E by A2, A1; :: thesis: verum

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 S

A4: S

A5: for n being Nat st S

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

set n1 = n + 1;

assume A6: ( S_{1}[n] & n + 1 <= len Z )
; :: thesis: 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; :: thesis: verum

end;set n1 = n + 1;

assume A6: ( S

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; :: thesis: verum

then ( S

hence Sum Z = Sum E by A2, A1; :: thesis: verum