let M, N be Cardinal; :: thesis: ( not M is finite & 0 in N & ( N c= M or N in M ) implies ( M *` N = M & N *` M = M ) )
A1: 1 *` M = M by CARD_2:21;
assume not M is finite ; :: thesis: ( not 0 in N or ( not N c= M & not N in M ) or ( M *` N = M & N *` M = M ) )
then A2: M *` M = M by Th15;
assume 0 in N ; :: thesis: ( ( not N c= M & not N in M ) or ( M *` N = M & N *` M = M ) )
then 1 c= N by CARD_2:68;
then A3: 1 *` M c= N *` M by CARD_2:90;
assume ( N c= M or N in M ) ; :: thesis: ( M *` N = M & N *` M = M )
then N *` M c= M *` M by CARD_2:90;
hence ( M *` N = M & N *` M = M ) by A2, A3, A1; :: thesis: verum