:: deftheorem defines Product CARD_3:def 8 :
for F being Cardinal-Function holds Product F = card (product F);