defpred S₁[ 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: S₁[ 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: i divides Sum f
Sum f = 0 by A2, RVSUM_1:72;
hence i divides Sum f by NAT_D:6; :: thesis: verum

end;

A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[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: i divides Sum f
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 A7, FINSEQ_1:36;
reconsider f2 = <*x*> as FinSequence of NAT by A7, FINSEQ_1:36;
k + 1 = (len f1) + (len f2) by A5, A7, FINSEQ_1:22;
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 A7, FINSEQ_1:26;
then f /. j = f . j by A9, PARTFUN1:def 6
.= f1 . j by A7, A9, FINSEQ_1:def 7
.= f1 /. j by A9, PARTFUN1:def 6 ;
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 A5, A7, A8, FINSEQ_1:42;
len f in Seg (len f) by A5, FINSEQ_1:3;
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 A7, RVSUM_1:74;
hence i divides Sum f by A11, A14, NAT_D:8; :: thesis: verum

end;

A15: for k being Nat holds S₁[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: i divides Sum f
len f = len f ;
hence i divides Sum f by A15, A16; :: thesis: verum