per cases ( N is Nat or N = +infty ) by Th3;

suppose N is Nat ; :: thesis: N + M is ext-natural

then reconsider n = N as Nat ;

per cases ( M is Nat or M = +infty ) by Th3;

suppose M is Nat ; :: thesis: N + M is ext-natural

then reconsider k = M as Nat ;
n + k is Nat ;
hence N + M is ext-natural ; :: thesis: verum

end;

suppose M = +infty ; :: thesis: N + M is ext-natural

hence N + M is ext-natural by XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

suppose N = +infty ; :: thesis: N + M is ext-natural

hence N + M is ext-natural by XXREAL_3:def 2; :: thesis: verum

end;

end;