let M, N be Cardinal; :: thesis: ( not M is finite implies ( not M +` N is finite & not N +` M is finite ) )
assume A1: not M is finite ; :: thesis: ( not M +` N is finite & not N +` M is finite )
( M c= N or N c= M ) ;
then ( ( M c= N & not N is finite ) or ( M +` N = M & N +` M = M ) ) by A1, Th75;
hence ( not M +` N is finite & not N +` M is finite ) by A1, Th75; :: thesis: verum