let X, Y be set ; :: thesis: ( not X is finite & Y is finite & Y <> {} implies ( [:X,Y:],X are_equipotent & card [:X,Y:] = card X ) )
assume Z: ( not X is finite & Y is finite & Y <> {} ) ; :: thesis: ( [:X,Y:],X are_equipotent & card [:X,Y:] = card X )
( card Y c= card X & 0 in card Y ) by Z, ORDINAL3:10;
then (card X) *` (card Y) = card X by Z, Th78;
then card [:(card X),(card Y):] = card X by CARD_2:def 2;
then card [:X,Y:] = card X by CARD_2:14;
hence ( [:X,Y:],X are_equipotent & card [:X,Y:] = card X ) by CARD_1:21; :: thesis: verum