defpred S1[ Nat] means for F being FinSequence of COMPLEX
for Fr being FinSequence of REAL st len F = \$1 & Fr = Re F holds
Sum Fr = Re (Sum F);
A1: S1[ 0 ]
proof
let F be FinSequence of COMPLEX ; :: thesis: for Fr being FinSequence of REAL st len F = 0 & Fr = Re F holds
Sum Fr = Re (Sum F)

let Fr be FinSequence of REAL ; :: thesis: ( len F = 0 & Fr = Re F implies Sum Fr = Re (Sum F) )
assume A2: ( len F = 0 & Fr = Re F ) ; :: thesis: Sum Fr = Re (Sum F)
then dom Fr = dom F by COMSEQ_3:def 3
.= Seg (len F) by FINSEQ_1:def 3 ;
then A3: len Fr = 0 by ;
thus Re (Sum F) = Re 0 by
.= Sum Fr by ; :: thesis: verum
end;
A4: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for F being FinSequence of COMPLEX
for Fr being FinSequence of REAL st len F = k + 1 & Fr = Re F holds
Re (Sum F) = Sum Fr
let F be FinSequence of COMPLEX ; :: thesis: for Fr being FinSequence of REAL st len F = k + 1 & Fr = Re F holds
Re (Sum F) = Sum Fr

let Fr be FinSequence of REAL ; :: thesis: ( len F = k + 1 & Fr = Re F implies Re (Sum F) = Sum Fr )
assume A6: ( len F = k + 1 & Fr = Re F ) ; :: thesis: Re (Sum F) = Sum Fr
reconsider F1 = F | k as FinSequence of COMPLEX ;
A7: len F1 = k by ;
reconsider F1r = Re F1 as FinSequence of REAL ;
reconsider x = F . (k + 1) as Element of COMPLEX by XCMPLX_0:def 2;
A8: F = F1 ^ <*x*> by ;
hence Re (Sum F) = Re ((Sum F1) + x) by Lm3
.= (Re (Sum F1)) + (Re x) by COMPLEX1:8
.= (Sum F1r) + (Re x) by A5, A7
.= Sum (F1r ^ <*(Re x)*>) by RVSUM_1:74
.= Sum Fr by A6, A8, Th5 ;
:: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A9: for k being Nat holds S1[k] from NAT_1:sch 2(A1, A4);
let F be FinSequence of COMPLEX ; :: thesis: for Fr being FinSequence of REAL st Fr = Re F holds
Sum Fr = Re (Sum F)

let Fr be FinSequence of REAL ; :: thesis: ( Fr = Re F implies Sum Fr = Re (Sum F) )
assume A10: Fr = Re F ; :: thesis: Sum Fr = Re (Sum F)
len F is Element of NAT ;
hence Sum Fr = Re (Sum F) by ; :: thesis: verum