theorem :: CARD_3:59

for A, B being non empty set
for f being Function of A,B holds sproduct f = sproduct (f | { x where x is Element of A : f . x <> {} } )