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;
let G be FinSequence of F_Complex; :: thesis: ( ( for i being Element of NAT st i in dom G holds
G . i is Integer ) implies Sum G is Integer )

assume A1: for i being Element of NAT st i in dom G holds
G . i is Integer ; :: thesis: Sum G is Integer
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[k + 1]
let F be FinSequence of F_Complex; :: thesis: ( len F = k + 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 = k + 1 and
A5: for i being Element of NAT st i in dom F holds
F . i is Integer ; :: thesis: Sum F is Integer
F <> {} by A4;
then consider G being FinSequence, x being object such that
A6: F = G ^ <*x*> by FINSEQ_1:46;
len F in Seg (len F) by ;
then A7: len F in dom F by FINSEQ_1:def 3;
reconsider f2 = <*x*> as FinSequence of F_Complex by ;
reconsider f1 = G as FinSequence of F_Complex by ;
rng f2 c= the carrier of F_Complex by FINSEQ_1:def 4;
then {x} c= the carrier of F_Complex by FINSEQ_1:38;
then reconsider m = x as Element of F_Complex by ZFMISC_1:31;
k + 1 = (len f1) + (len f2) by ;
then A8: k + 1 = (len f1) + 1 by FINSEQ_1:39;
then F . (len F) = m by ;
then reconsider i2 = m as Integer by A5, A7;
for j being Element of NAT st j in dom f1 holds
f1 . j is Integer
proof
A9: dom f1 c= dom F by ;
let j be Element of NAT ; :: thesis: ( j in dom f1 implies f1 . j is Integer )
assume A10: j in dom f1 ; :: thesis: f1 . j is Integer
F . j = f1 . j by ;
hence f1 . j is Integer by A5, A10, A9; :: thesis: verum
end;
then reconsider i1 = Sum f1 as Integer by A3, A8;
Sum F = (Sum f1) + m by ;
then Sum F = i1 + i2 ;
hence Sum F is Integer ; :: thesis: verum
end;
A11: 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 that
A12: len F = 0 and
for i being Element of NAT st i in dom F holds
F . i is Integer ; :: thesis: Sum F is Integer
( 0 -tuples_on the carrier of F_Complex = & F = {} ) by ;
then F is Element of 0 -tuples_on the carrier of F_Complex by TARSKI:def 1;
hence Sum F is Integer by ; :: thesis: verum
end;
A13: for k being Nat holds S1[k] from NAT_1:sch 2(A11, A2);
len G = len G ;
hence Sum G is Integer by ; :: thesis: verum