let k, n be Element of NAT ; :: thesis: ( k <= n implies (n ! ) / (k ! ) is integer )
defpred S₁[ Element of 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:18;
A1: n = m + k ;

now

let m be Element of 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:21
.= ((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 Element of NAT st S₁[n] holds
S₁[n + 1] ;
A4: S₁[ 0 ] by XCMPLX_1:60;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A3);
hence (n ! ) / (k ! ) is integer by A1; :: thesis: verum