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