defpred S₁[ Nat] means ex n being Element of NAT st
( n ! <= $1 & $1 < (n + 1) ! & ( for m being Element of NAT st m ! <= $1 & $1 < (m + 1) ! holds
m = n ) );
A1: for k being Nat st k >= 1 & S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume that
k >= 1 and
A2: ex n being Element of NAT st
( n ! <= k & k < (n + 1) ! & ( for m being Element of NAT st m ! <= k & k < (m + 1) ! holds
m = n ) ) ; :: thesis:
consider n being Element of NAT such that
A3: n ! <= k and
A4: k < (n + 1) ! and
for m being Element of NAT st m ! <= k & k < (m + 1) ! holds
m = n by A2;
A5: k + 1 <= (n + 1) ! by A4, INT_1:7;

per cases by A5, XXREAL_0:1;

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

take n ; :: thesis:
k + 0 <= k + 1 by XREAL_1:6;
hence n ! <= k + 1 by A3, XXREAL_0:2; :: thesis:
thus k + 1 < (n + 1) ! by A6; :: thesis:
let m be Element of NAT ; :: thesis:
assume that
A7: m ! <= k + 1 and
A8: k + 1 < (m + 1) ! ; :: thesis:

now :: thesis:

assume A9: m <> n ; :: thesis:
thus contradiction :: thesis:

proof

per cases by A9, XXREAL_0:1;

suppose m > n ; :: thesis:

then m >= n + 1 by NAT_1:13;
then m ! >= (n + 1) ! by Lm51;
hence contradiction by A6, A7, XXREAL_0:2; :: thesis:

end;

suppose m < n ; :: thesis:

then m + 1 <= n by NAT_1:13;
then (m + 1) ! <= n ! by Lm51;
then A10: (m + 1) ! <= k by A3, XXREAL_0:2;
k <= k + 1 by NAT_1:11;
hence contradiction by A8, A10, XXREAL_0:2; :: thesis:

end;

hence m = n ; :: thesis:

end;

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

take N = n + 1; :: thesis:
thus N ! <= k + 1 by A11; :: thesis:
A12: N ! > 0 by NEWTON:17;
N + 1 > 0 + 1 by XREAL_1:6;
then (N + 1) * (N !) > 1 * (N !) by A12, XREAL_1:68;
hence k + 1 < (N + 1) ! by A11, NEWTON:15; :: thesis:
let m be Element of NAT ; :: thesis:
assume that
A13: m ! <= k + 1 and
A14: k + 1 < (m + 1) ! ; :: thesis:

now :: thesis:

assume A15: m <> N ; :: thesis:
thus contradiction :: thesis:

proof

per cases by A15, XXREAL_0:1;

suppose m > N ; :: thesis:

then m >= N + 1 by NAT_1:13;
then m ! >= (N + 1) ! by Lm51;
then A16: k + 1 >= (N + 1) ! by A13, XXREAL_0:2;
n + 2 >= 0 + 2 by XREAL_1:6;
then A17: N + 1 > 1 by XXREAL_0:2;
N ! > 0 by NEWTON:17;
then (N + 1) * (N !) > 1 * (N !) by A17, XREAL_1:68;
hence contradiction by A11, A16, NEWTON:15; :: thesis:

end;

suppose m < N ; :: thesis:

then m + 1 <= N by NAT_1:13;
hence contradiction by A11, A14, Lm51; :: thesis:

end;

hence m = N ; :: thesis:

end;

A18: S₁[1]

proof

take 1 ; :: thesis:
thus ( 1 ! <= 1 & 1 < (1 + 1) ! ) by NEWTON:13, NEWTON:14; :: thesis:
let m be Element of NAT ; :: thesis:
assume that
A19: m ! <= 1 and
A20: 1 < (m + 1) ! ; :: thesis:

A21: now :: thesis:

assume m > 1 ; :: thesis:
then m >= 1 + 1 by NAT_1:13;
hence contradiction by A19, Lm50; :: thesis:

end;

m <> 0 by A20, NEWTON:13;
then m >= 0 + 1 by NAT_1:13;
hence m = 1 by A21, XXREAL_0:1; :: thesis:

end;

for k being Nat st k >= 1 holds
S₁[k] from NAT_1:sch 8(A18, A1);
hence for k being Element of NAT st k >= 1 holds
ex n being Element of NAT st
( n ! <= k & k < (n + 1) ! & ( for m being Element of NAT st m ! <= k & k < (m + 1) ! holds
m = n ) ) ; :: thesis: