for x being object
for f being Function st x in sproduct f holds
x is PartFunc of (dom f),(union (rng f))