let X, Y be set ; ( 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 <> {} )
; ( [: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; verum