theorem :: CARD_3:61

for f being Function holds
( sproduct f = {{}} iff for x being object st x in dom f holds
f . x = {} )