let n, i be Nat; :: thesis: ( n >= 1 & i >= 1 implies (n + i) ! >= (n !) + i )
assume ( n >= 1 & i >= 1 ) ; :: thesis: (n + i) ! >= (n !) + i

per cases then ( ( n >= 1 & i > 1 ) or ( n >= 1 & i = 1 ) ) by XXREAL_0:1;

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

per cases then ( ( n > 1 & i > 1 ) or ( n = 1 & i > 1 ) ) by XXREAL_0:1;

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

hence (n + i) ! >= (n !) + i by Th7; :: thesis: verum

end;

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

hence (n + i) ! >= (n !) + i by NEWTON:13, NEWTON:38; :: thesis: verum

end;

end;

end;

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

hence (n + i) ! >= (n !) + i by Th4; :: thesis: verum

end;

end;