for X, Y being set holds
( product <*X,Y*>,[:X,Y:] are_equipotent & card (product <*X,Y*>) = (card X) *` (card Y) )