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_{1}[ 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_{1}[n] holds

S_{1}[n + 1]

A12: S_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A12, A2);

hence Sum f is integer by A1, A11; :: thesis: verum

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

f . i is integer ) holds

Sum f is integer ;

A2: for n being Nat st S

S

proof

A11:
len f is Element of NAT
;
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[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;

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;assume A3: S

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

0 + 1 <= len f
by A4, NAT_1:13;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;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

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

A12: S

proof

for n being Nat holds S
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;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

hence Sum f is integer by A1, A11; :: thesis: verum