for A, B being Ordinal holds
( A *^ B,[:A,B:] are_equipotent & card (A *^ B) = card [:A,B:] )