set FC = F_Complex ;
let f be FinSequence of F_Complex; :: thesis: ( ( for i being Element of NAT st i in dom f holds
f . i is integer ) implies Sum f is integer )
assume A1: for i being Element of NAT st i in dom f holds
f . i is integer ; :: thesis: Sum f is integer
defpred S₁[ Nat] means for f being FinSequence of F_Complex st len f = $1 & ( for i being Element of NAT st i in dom f holds
f . i is integer ) holds
Sum f is integer ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
let f be FinSequence of F_Complex; :: thesis: ( len f = n + 1 & ( for i being Element of NAT st i in dom f holds
f . i is integer ) implies Sum f is integer )
assume that
A4: len f = n + 1 and
A5: for i being Element of NAT st i in dom f holds
f . i is integer ; :: thesis: Sum f is integer
consider g being FinSequence of F_Complex, c being Element of F_Complex such that
A6: f = g ^ <*c*> by A4, FINSEQ_2:19;

A7: now :: thesis: for i being Element of NAT st i in dom g holds
g . i is integer

let i be Element of NAT ; :: thesis: ( i in dom g implies g . i is integer )
A8: dom g c= dom f by A6, FINSEQ_1:26;
assume A9: i in dom g ; :: thesis: g . i is integer
then f . i = g . i by A6, FINSEQ_1:def 7;
hence g . i is integer by A5, A9, A8; :: thesis: verum

end;

0 + 1 <= len f by A4, NAT_1:13;
then len f in dom f by FINSEQ_3:25;
then A10: f . (len f) is integer by A5;
reconsider Sgc = Sum g, cc = c as Element of COMPLEX by COMPLFLD:def 1;
len f = (len g) + (len <*c*>) by A6, FINSEQ_1:22
.= (len g) + 1 by FINSEQ_1:40 ;
then reconsider Sgi = Sgc, ci = cc as Integer by A3, A4, A6, A7, A10, FINSEQ_1:42;
Sum f = (Sum g) + (Sum <*c*>) by A6, RLVECT_1:41
.= Sgi + ci by RLVECT_1:44 ;
hence Sum f is integer ; :: thesis: verum

end;

A11: len f is Element of NAT ;
A12: S₁[ 0 ]

proof

let f be FinSequence of F_Complex; :: thesis: ( len f = 0 & ( for i being Element of NAT st i in dom f holds
f . i is integer ) implies Sum f is integer )
assume len f = 0 ; :: thesis: ( ex i being Element of NAT st
( i in dom f & not f . i is integer ) or Sum f is integer )
then f = <*> the carrier of F_Complex ;
hence ( ex i being Element of NAT st
( i in dom f & not f . i is integer ) or Sum f is integer ) by COMPLFLD:7, RLVECT_1:43; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A12, A2);
hence Sum f is integer by A1, A11; :: thesis: verum