:: deftheorem Def13 defines product-like CARD_3:def 13 :
for S being set holds
( S is product-like iff ex f being Function st S = product f );