:: deftheorem Def9 defines sproduct CARD_3:def 9 :
for f being Function
for b₂ being set holds
( b₂ = sproduct f iff for x being object holds
( x in b₂ iff ex g being Function st
( x = g & dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) ) ) );