defpred S1[ Nat] means for f being FinSequence of NAT st len f = \$1 holds
for i being Element of NAT st ( for j being Element of NAT st j in dom f holds
i divides f /. j ) holds
i divides Sum f;
A1: S1[ 0 ]
proof
let f be FinSequence of NAT ; :: thesis: ( len f = 0 implies for i being Element of NAT st ( for j being Element of NAT st j in dom f holds
i divides f /. j ) holds
i divides Sum f )

assume len f = 0 ; :: thesis: for i being Element of NAT st ( for j being Element of NAT st j in dom f holds
i divides f /. j ) holds
i divides Sum f

then A2: f = <*> NAT ;
let i be Element of NAT ; :: thesis: ( ( for j being Element of NAT st j in dom f holds
i divides f /. j ) implies i divides Sum f )

assume for j being Element of NAT st j in dom f holds
i divides f /. j ; :: thesis:
Sum f = 0 by ;
hence i divides Sum f by NAT_D:6; :: thesis: verum
end;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
let f be FinSequence of NAT ; :: thesis: ( len f = k + 1 implies for i being Element of NAT st ( for j being Element of NAT st j in dom f holds
i divides f /. j ) holds
i divides Sum f )

assume A5: len f = k + 1 ; :: thesis: for i being Element of NAT st ( for j being Element of NAT st j in dom f holds
i divides f /. j ) holds
i divides Sum f

let i be Element of NAT ; :: thesis: ( ( for j being Element of NAT st j in dom f holds
i divides f /. j ) implies i divides Sum f )

assume A6: for j being Element of NAT st j in dom f holds
i divides f /. j ; :: thesis:
f <> {} by A5;
then consider q being FinSequence, x being object such that
A7: f = q ^ <*x*> by FINSEQ_1:46;
reconsider f1 = q as FinSequence of NAT by ;
reconsider f2 = <*x*> as FinSequence of NAT by ;
k + 1 = (len f1) + (len f2) by ;
then A8: k + 1 = (len f1) + 1 by FINSEQ_1:39;
for j being Element of NAT st j in dom f1 holds
i divides f1 /. j
proof
let j be Element of NAT ; :: thesis: ( j in dom f1 implies i divides f1 /. j )
assume A9: j in dom f1 ; :: thesis: i divides f1 /. j
A10: dom f1 c= dom f by ;
then f /. j = f . j by
.= f1 . j by
.= f1 /. j by ;
hence i divides f1 /. j by A6, A9, A10; :: thesis: verum
end;
then A11: i divides Sum f1 by A4, A8;
rng f2 c= NAT by FINSEQ_1:def 4;
then {x} c= NAT by FINSEQ_1:38;
then reconsider m = x as Element of NAT by ZFMISC_1:31;
A12: f . (len f) = m by ;
len f in Seg (len f) by ;
then A13: len f in dom f by FINSEQ_1:def 3;
then f /. (len f) = f . (len f) by PARTFUN1:def 6;
then A14: i divides m by A6, A12, A13;
Sum f = (Sum f1) + m by ;
hence i divides Sum f by ; :: thesis: verum
end;
A15: for k being Nat holds S1[k] from NAT_1:sch 2(A1, A3);
let f be FinSequence of NAT ; :: thesis: for i being Element of NAT st ( for j being Element of NAT st j in dom f holds
i divides f /. j ) holds
i divides Sum f

let i be Element of NAT ; :: thesis: ( ( for j being Element of NAT st j in dom f holds
i divides f /. j ) implies i divides Sum f )

assume A16: for j being Element of NAT st j in dom f holds
i divides f /. j ; :: thesis:
len f = len f ;
hence i divides Sum f by ; :: thesis: verum