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 S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; :: thesis: S1[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 ;
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 ;
assume A9: i in dom g ; :: thesis: g . i is integer
then f . i = g . i by ;
hence g . i is integer by A5, A9, A8; :: thesis: verum
end;
0 + 1 <= len f by ;
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) + () by
.= (len g) + 1 by FINSEQ_1:40 ;
then reconsider Sgi = Sgc, ci = cc as Integer by ;
Sum f = (Sum g) + () by
.= Sgi + ci by RLVECT_1:44 ;
hence Sum f is integer ; :: thesis: verum
end;
A11: len f is Element of NAT ;
A12: S1[ 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 ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A12, A2);
hence Sum f is integer by ; :: thesis: verum