let n1, n2 be Element of NAT ; :: thesis: ( ( x <> 0 & ex n being Element of NAT st
( n ! <= x & x < (n + 1) ! & n1 = n ! ) & ex n being Element of NAT st
( n ! <= x & x < (n + 1) ! & n2 = n ! ) implies n1 = n2 ) & ( not x <> 0 & n1 = 0 & n2 = 0 implies n1 = n2 ) )

now

assume that
A4: ex n being Element of NAT st
( n ! <= x & x < (n + 1) ! & n1 = n ! ) and
A5: ex n being Element of NAT st
( n ! <= x & x < (n + 1) ! & n2 = n ! ) ; :: thesis: n1 = n2
consider n being Element of NAT such that
A6: n ! <= x and
A7: x < (n + 1) ! and
A8: n1 = n ! by A4;
consider m being Element of NAT such that
A9: m ! <= x and
A10: x < (m + 1) ! and
A11: n2 = m ! by A5;

now

assume A12: m <> n ; :: thesis: contradiction
thus contradiction :: thesis: verum

proof

per cases ( m > n or m < n ) by A12, XXREAL_0:1;

suppose m > n ; :: thesis: contradiction

then m >= n + 1 by INT_1:7;
then m ! >= (n + 1) ! by Lm51;
hence contradiction by A7, A9, XXREAL_0:2; :: thesis: verum

end;

suppose m < n ; :: thesis: contradiction

then m + 1 <= n by INT_1:7;
then (m + 1) ! <= n ! by Lm51;
hence contradiction by A6, A10, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

hence n1 = n2 by A8, A11; :: thesis: verum

end;

hence ( ( x <> 0 & ex n being Element of NAT st
( n ! <= x & x < (n + 1) ! & n1 = n ! ) & ex n being Element of NAT st
( n ! <= x & x < (n + 1) ! & n2 = n ! ) implies n1 = n2 ) & ( not x <> 0 & n1 = 0 & n2 = 0 implies n1 = n2 ) ) ; :: thesis: verum