let k, n be Nat; :: thesis: for x being Real st x = 1 / (n + 1) holds
(n !) / (((n + k) + 1) !) <= x ^ (k + 1)
let x be Real; :: thesis: ( x = 1 / (n + 1) implies (n !) / (((n + k) + 1) !) <= x ^ (k + 1) )
defpred S₁[ Nat] means (n !) / (((n + $1) + 1) !) <= x ^ ($1 + 1);
assume A1: x = 1 / (n + 1) ; :: thesis: (n !) / (((n + k) + 1) !) <= x ^ (k + 1)

A2: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
A4: (n !) / (((n + (k + 1)) + 1) !) = (n !) * ((((n + (k + 1)) + 1) !) ")
.= (n !) * ((((n + (k + 1)) + 1) * (((n + k) + 1) !)) ") by NEWTON:15
.= (n !) * ((((n + (k + 1)) + 1) ") * ((((n + k) + 1) !) ")) by XCMPLX_1:204
.= ((n !) * ((((n + k) + 1) !) ")) * (((n + (k + 1)) + 1) ")
.= ((n !) / (((n + k) + 1) !)) * (((n + (k + 1)) + 1) ") ;
n + (k + 1) >= n + 0 by XREAL_1:6;
then (n + (k + 1)) + 1 >= n + 1 by XREAL_1:6;
then A5: ((n + (k + 1)) + 1) " <= 1 / (n + 1) by XREAL_1:85;
(x ^ (k + 1)) * x = (x ^ (k + 1)) * (x ^ 1)
.= x ^ ((k + 1) + 1) by A1, POWER:27 ;
hence S₁[k + 1] by A1, A3, A5, A4, XREAL_1:66; :: thesis: verum

end;

(n !) / ((n + 1) !) = (n !) / ((n + 1) * (n !)) by NEWTON:15
.= (n !) * (((n + 1) * (n !)) ")
.= (n !) * (((n + 1) ") * ((n !) ")) by XCMPLX_1:204
.= ((n !) * ((n !) ")) * ((n + 1) ")
.= 1 * ((n + 1) ") by XCMPLX_0:def 7
.= x by A1 ;
then A6: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A2);
hence (n !) / (((n + k) + 1) !) <= x ^ (k + 1) ; :: thesis: verum