defpred S₁[ 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);
P0: S₁[ 0 ]

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 P01: ( 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 P02: len Fi = 0 by P01, FINSEQ_1:def 3;
thus Im (Sum F) = Im 0 by P01, FINSEQ_1:28, RVSUM1102
.= Sum Fi by P02, FINSEQ_1:28, RVSUM_1:102, COMPLEX1:12 ; :: thesis: verum

end;

P1: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A1: S₁[k] ; :: thesis: S₁[k + 1]

now

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 P10: ( len F = k + 1 & Fi = Im F ) ; :: thesis: Im (Sum F) = Sum Fi
reconsider F1 = F | k as FinSequence of COMPLEX ;
P11: len F1 = k by P10, NAT_1:11, FINSEQ_1:80;
reconsider F1i = Im F1 as FinSequence of REAL ;
reconsider x = F . (k + 1) as Element of COMPLEX by XCMPLX_0:def 2;
P12: F = F1 ^ <*x*> by FINSEQ_3:61, P10;
hence Im (Sum F) = Im ((Sum F1) + x) by RVSUM1104
.= (Im (Sum F1)) + (Im x) by COMPLEX1:19
.= (Sum F1i) + (Im x) by A1, P11
.= Sum (F1i ^ <*(Im x)*>) by RVSUM_1:104
.= Sum Fi by P10, P12, RVSUM2105 ;
:: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

P2: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(P0, P1);
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 P3: Fi = Im F ; :: thesis: Sum Fi = Im (Sum F)
len F is Element of NAT ;
hence Sum Fi = Im (Sum F) by P2, P3; :: thesis: verum