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 that
A1: not X is finite and
A2: ( 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 A1, A2, ORDINAL3:8;
then (card X) *` (card Y) = card X by A1, Th16;
then card [:(card X),(card Y):] = card X by CARD_2:def 2;
then card [:X,Y:] = card X by CARD_2:7;
hence ( [:X,Y:],X are_equipotent & card [:X,Y:] = card X ) by CARD_1:5; :: thesis: verum