let X1, X2, Y1, Y2 be set ; :: thesis: ( X1,Y1 are_equipotent & X2,Y2 are_equipotent implies ( [:X1,X2:],[:Y1,Y2:] are_equipotent & card [:X1,X2:] = card [:Y1,Y2:] ) )
assume ( X1,Y1 are_equipotent & X2,Y2 are_equipotent ) ; :: thesis: ( [:X1,X2:],[:Y1,Y2:] are_equipotent & card [:X1,X2:] = card [:Y1,Y2:] )
then A1: ( card X1 = card Y1 & card X2 = card Y2 ) by CARD_1:5;
( [:X1,X2:],[:(card X1),(card X2):] are_equipotent & [:Y1,Y2:],[:(card Y1),(card Y2):] are_equipotent ) by Th6;
hence [:X1,X2:],[:Y1,Y2:] are_equipotent by A1, WELLORD2:15; :: thesis: card [:X1,X2:] = card [:Y1,Y2:]
hence card [:X1,X2:] = card [:Y1,Y2:] by CARD_1:5; :: thesis: verum