defpred S₁[ Element of NAT ] means for n being Element of NAT st n <= $1 holds
n ! <= $1 ! ;
A1: S₁[ 0 ] ;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: for n being Element of NAT st n <= k holds
n ! <= k ! ; :: thesis: S₁[k + 1]
let n be Element of NAT ; :: thesis: ( n <= k + 1 implies n ! <= (k + 1) ! )
assume A4: n <= k + 1 ; :: thesis: n ! <= (k + 1) !

per cases ( n <= k or n = k + 1 ) by A4, NAT_1:8;

suppose n <= k ; :: thesis: n ! <= (k + 1) !

then A5: n ! <= k ! by A3;
k + 1 >= 0 + 1 by XREAL_1:8;
then (k + 1) * (k ! ) >= 1 * (k ! ) by XREAL_1:66;
then (k + 1) ! >= k ! by NEWTON:21;
hence n ! <= (k + 1) ! by A5, XXREAL_0:2; :: thesis: verum

end;

suppose n = k + 1 ; :: thesis: n ! <= (k + 1) !

hence n ! <= (k + 1) ! ; :: thesis: verum

end;

end;

end;

for n1 being Element of NAT holds S₁[n1] from NAT_1:sch 1(A1, A2);
hence for n1, n being Element of NAT st n <= n1 holds
n ! <= n1 ! ; :: thesis: verum