per cases by Th3;

suppose N is Nat ; :: thesis:

then reconsider n = N as Nat ;

per cases by Th3;

suppose M is Nat ; :: thesis:

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

end;

suppose M = +infty ; :: thesis:

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

end;

end;

end;

suppose N = +infty ; :: thesis:

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

end;

end;