:: deftheorem defines *` CARD_2:def 2 :
for M, N being Cardinal holds M *` N = card [:M,N:];