defpred S_{1}[ Nat] means for F being FinSequence of COMPLEX

for Fi being FinSequence of REAL st len F = $1 & Fi = Im F holds

Sum Fi = Im (Sum F);

A1: S_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A1, A4);

let F be FinSequence of COMPLEX ; :: thesis: for Fi being FinSequence of REAL st Fi = Im F holds

Sum Fi = Im (Sum F)

let Fi be FinSequence of REAL ; :: thesis: ( Fi = Im F implies Sum Fi = Im (Sum F) )

assume A10: Fi = Im F ; :: thesis: Sum Fi = Im (Sum F)

len F is Element of NAT ;

hence Sum Fi = Im (Sum F) by A9, A10; :: thesis: verum

for Fi being FinSequence of REAL st len F = $1 & Fi = Im F holds

Sum Fi = Im (Sum F);

A1: S

proof

let F be FinSequence of COMPLEX ; :: thesis: for Fi being FinSequence of REAL st len F = 0 & Fi = Im F holds

Sum Fi = Im (Sum F)

let Fi be FinSequence of REAL ; :: thesis: ( len F = 0 & Fi = Im F implies Sum Fi = Im (Sum F) )

assume A2: ( len F = 0 & Fi = Im F ) ; :: thesis: Sum Fi = Im (Sum F)

then dom Fi = dom F by COMSEQ_3:def 4

.= Seg (len F) by FINSEQ_1:def 3 ;

then A3: len Fi = 0 by A2, FINSEQ_1:def 3;

thus Im (Sum F) = Im 0 by A2, Lm2, FINSEQ_1:20

.= Sum Fi by A3, COMPLEX1:4, FINSEQ_1:20, RVSUM_1:72 ; :: thesis: verum

end;Sum Fi = Im (Sum F)

let Fi be FinSequence of REAL ; :: thesis: ( len F = 0 & Fi = Im F implies Sum Fi = Im (Sum F) )

assume A2: ( len F = 0 & Fi = Im F ) ; :: thesis: Sum Fi = Im (Sum F)

then dom Fi = dom F by COMSEQ_3:def 4

.= Seg (len F) by FINSEQ_1:def 3 ;

then A3: len Fi = 0 by A2, FINSEQ_1:def 3;

thus Im (Sum F) = Im 0 by A2, Lm2, FINSEQ_1:20

.= Sum Fi by A3, COMPLEX1:4, FINSEQ_1:20, RVSUM_1:72 ; :: thesis: verum

A4: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A9:
for k being Nat holds SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A5: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A5: S

now :: thesis: for F being FinSequence of COMPLEX

for Fi being FinSequence of REAL st len F = k + 1 & Fi = Im F holds

Im (Sum F) = Sum Fi

hence
Sfor Fi being FinSequence of REAL st len F = k + 1 & Fi = Im F holds

Im (Sum F) = Sum Fi

let F be FinSequence of COMPLEX ; :: thesis: for Fi being FinSequence of REAL st len F = k + 1 & Fi = Im F holds

Im (Sum F) = Sum Fi

let Fi be FinSequence of REAL ; :: thesis: ( len F = k + 1 & Fi = Im F implies Im (Sum F) = Sum Fi )

assume A6: ( len F = k + 1 & Fi = Im F ) ; :: thesis: Im (Sum F) = Sum Fi

reconsider F1 = F | k as FinSequence of COMPLEX ;

A7: len F1 = k by A6, FINSEQ_1:59, NAT_1:11;

reconsider F1i = Im F1 as FinSequence of REAL ;

reconsider x = F . (k + 1) as Element of COMPLEX by XCMPLX_0:def 2;

A8: F = F1 ^ <*x*> by A6, FINSEQ_3:55;

hence Im (Sum F) = Im ((Sum F1) + x) by Lm3

.= (Im (Sum F1)) + (Im x) by COMPLEX1:8

.= (Sum F1i) + (Im x) by A5, A7

.= Sum (F1i ^ <*(Im x)*>) by RVSUM_1:74

.= Sum Fi by A6, A8, Th6 ;

:: thesis: verum

end;Im (Sum F) = Sum Fi

let Fi be FinSequence of REAL ; :: thesis: ( len F = k + 1 & Fi = Im F implies Im (Sum F) = Sum Fi )

assume A6: ( len F = k + 1 & Fi = Im F ) ; :: thesis: Im (Sum F) = Sum Fi

reconsider F1 = F | k as FinSequence of COMPLEX ;

A7: len F1 = k by A6, FINSEQ_1:59, NAT_1:11;

reconsider F1i = Im F1 as FinSequence of REAL ;

reconsider x = F . (k + 1) as Element of COMPLEX by XCMPLX_0:def 2;

A8: F = F1 ^ <*x*> by A6, FINSEQ_3:55;

hence Im (Sum F) = Im ((Sum F1) + x) by Lm3

.= (Im (Sum F1)) + (Im x) by COMPLEX1:8

.= (Sum F1i) + (Im x) by A5, A7

.= Sum (F1i ^ <*(Im x)*>) by RVSUM_1:74

.= Sum Fi by A6, A8, Th6 ;

:: thesis: verum

let F be FinSequence of COMPLEX ; :: thesis: for Fi being FinSequence of REAL st Fi = Im F holds

Sum Fi = Im (Sum F)

let Fi be FinSequence of REAL ; :: thesis: ( Fi = Im F implies Sum Fi = Im (Sum F) )

assume A10: Fi = Im F ; :: thesis: Sum Fi = Im (Sum F)

len F is Element of NAT ;

hence Sum Fi = Im (Sum F) by A9, A10; :: thesis: verum