let k, n be Nat; :: thesis: ( k <= n implies (n !) / (k !) is integer )
defpred S₁[ Nat] means (($1 + k) !) / (k !) is integer ;
assume k <= n ; :: thesis: (n !) / (k !) is integer
then reconsider m = n - k as Element of NAT by INT_1:5;
A1: n = m + k ;

now :: thesis: for m being Nat st ((m + k) !) / (k !) is integer holds
(((m + 1) + k) !) / (k !) is integer

let m be Nat; :: thesis: ( ((m + k) !) / (k !) is integer implies (((m + 1) + k) !) / (k !) is integer )
A2: (((m + 1) + k) !) / (k !) = (((m + k) + 1) * ((m + k) !)) * ((k !) ") by NEWTON:15
.= ((m + k) + 1) * (((m + k) !) * ((k !) "))
.= ((m + k) + 1) * (((m + k) !) / (k !)) ;
assume ((m + k) !) / (k !) is integer ; :: thesis: (((m + 1) + k) !) / (k !) is integer
then reconsider i = ((m + k) !) / (k !) as Integer ;
((m + k) + 1) * i is Integer ;
hence (((m + 1) + k) !) / (k !) is integer by A2; :: thesis: verum

end;

then A3: for n being Nat st S₁[n] holds
S₁[n + 1] ;
A4: S₁[ 0 ] by XCMPLX_1:60;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A3);
hence (n !) / (k !) is integer by A1; :: thesis: verum