let iC be infinite Cardinal; :: thesis: omega *` iC = iC
omega c= iC by CARD_3:102;
then A1: omega *` iC c= iC *` iC by CARD_3:136;
( iC *` iC = iC & iC c= omega *` iC ) by CARD_3:141, CARD_4:77;
hence omega *` iC = iC by A1, XBOOLE_0:def 10; :: thesis: verum