:: deftheorem Def5 defines product CARD_3:def 5 :
for f being Function
for b₂ being set holds
( b₂ = product f iff for x being object holds
( x in b₂ iff ex g being Function st
( x = g & dom g = dom f & ( for y being object st y in dom f holds
g . y in f . y ) ) ) );