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 Th7
.= card ((card X) * (card Y)) by Th39 ;
hence card [:X,Y:] = (card X) * (card Y) by CARD_1:40; :: thesis: verum