let X, Y be finite set ; :: thesis: card [:X,Y:] = (card X) * (card Y)
card (card [:X,Y:]) = (card (card X)) *` (card (card Y)) by Th14
.= card ((card X) * (card Y)) by Th52 ;
hence card [:X,Y:] = (card X) * (card Y) by CARD_1:40; :: thesis: verum