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

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