let x, y be Nat; :: thesis:
thus ( y = x ! implies ex n, y1, y2, y3 being Nat st
( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] ) ) :: thesis:

proof

assume A1: y = x ! ; :: thesis:

per cases ;

suppose A2: x = 0 ; :: thesis:

take n = 1; :: thesis:
take y1 = 0 ; :: thesis:
take y2 = 1; :: thesis:
take y3 = 1; :: thesis:
thus ( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 ) by A2, NEWTON:19; :: thesis:
thus y = [\(y2 / y3)/] by INT_1:25, NEWTON:12, A2, A1; :: thesis:

end;

suppose A3: x > 0 ; :: thesis:

take n = ((2 * x) |^ (x + 1)) + 1; :: thesis:
take y1 = (2 * x) |^ (x + 1); :: thesis:
take y2 = n |^ x; :: thesis:
take y3 = n choose x; :: thesis:
n > y1 by NAT_1:13;
hence ( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] ) by A1, A3, Th17; :: thesis:

end;

end;

end;

given n, y1, y2, y3 being Nat such that A4: ( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 ) and
A5: y = [\(y2 / y3)/] ; :: thesis:

per cases ;

suppose A6: x = 0 ; :: thesis:

then ( y1 = 0 & y2 = 1 & y3 = 1 ) by A4, NEWTON:4, NEWTON:19;
hence y = x ! by NEWTON:12, A6, A5, INT_1:25; :: thesis:

end;

suppose x > 0 ; :: thesis:

hence y = x ! by A4, A5, Th17; :: thesis:

end;

end;