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

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