let n, i be Nat; :: thesis: ( n > 1 & i > 1 implies (n + i) ! >= (n !) + i )
assume A1: ( n > 1 & i > 1 ) ; :: thesis: (n + i) ! >= (n !) + i
then A2: i >= 1 + 1 by NAT_1:13;
A3: (n + i) ! >= (n !) * (i !) by NEWTON04:70;
n >= 1 + 1 by A1, NAT_1:13;
then ( n ! > 1 & i ! > 1 ) by A2, ASYMPT_1:55;
then A5: (n !) * (i !) >= (n !) + (i !) by Th1;

per cases ( i = 2 or i > 2 ) by A2, XXREAL_0:1;

suppose i = 2 ; :: thesis: (n + i) ! >= (n !) + i

hence (n + i) ! >= (n !) + i by A1, Th6; :: thesis: verum

end;

suppose i > 2 ; :: thesis: (n + i) ! >= (n !) + i

then A6: i >= 2 + 1 by NAT_1:13;
i ! > i by ASYMPT_1:59, A6;
then (n !) + (i !) > (n !) + i by XREAL_1:6;
then (n !) * (i !) > (n !) + i by A5, XXREAL_0:2;
hence (n + i) ! >= (n !) + i by A3, XXREAL_0:2; :: thesis: verum

end;

end;