theorem Th52: :: CARD_3:52

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