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;
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 S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[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 A4, FINSEQ_1:3;
then A7: len F in dom F by FINSEQ_1:def 3;
reconsider f2 = <*x*> as FinSequence of F_Complex by A6, FINSEQ_1:36;
reconsider f1 = G as FinSequence of F_Complex by A6, FINSEQ_1:36;
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 A4, A6, FINSEQ_1:22;
then A8: k + 1 = (len f1) + 1 by FINSEQ_1:39;
then F . (len F) = m by A4, A6, FINSEQ_1:42;
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 A6, FINSEQ_1:26;
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 A6, A10, FINSEQ_1:def 7;
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 A6, FVSUM_1:71;
then Sum F = i1 + i2 ;
hence Sum F is Integer ; :: thesis: verum

end;

A11: 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 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 A12, COMPUT_1:5;
then F is Element of 0 -tuples_on the carrier of F_Complex by TARSKI:def 1;
hence Sum F is Integer by COMPLFLD:7, FVSUM_1:74; :: thesis: verum

end;

A13: for k being Nat holds S₁[k] from NAT_1:sch 2(A11, A2);
len G = len G ;
hence Sum G is Integer by A1, A13; :: thesis: verum