let n, k be Nat; :: thesis: n ! divides (n + k) !
defpred S₁[ Nat] means n ! divides (n + $1) ! ;
A1: S₁[ 0 ] ;
A2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume B1: n ! divides (n + m) ! ; :: thesis: S₁[m + 1]
((n + m) + 1) ! = ((n + m) !) * ((n + m) + 1) by NEWTON:15;
then (n + m) ! divides ((n + m) + 1) ! ;
hence S₁[m + 1] by B1, INT_2:9; :: thesis: verum

end;

for c being Nat holds S₁[c] from NAT_1:sch 2(A1, A2);
hence n ! divides (n + k) ! ; :: thesis: verum