let X, Y be set ; :: thesis: ( not X is finite & Y is finite implies ( X \/ Y,X are_equipotent & card (X \/ Y) = card X ) )
assume that
A1: not X is finite and
A2: Y is finite ; :: thesis: ( X \/ Y,X are_equipotent & card (X \/ Y) = card X )
card Y in card X by A1, A2, CARD_3:86;
then A3: (card X) +` (card Y) = card X by A1, Th118;
A4: card (X \/ Y) c= (card X) +` (card Y) by Th47;
card X c= card (X \/ Y) by CARD_1:11, XBOOLE_1:7;
then card X = card (X \/ Y) by A3, A4, XBOOLE_0:def 10;
hence ( X \/ Y,X are_equipotent & card (X \/ Y) = card X ) by CARD_1:5; :: thesis: verum