theorem Th55: :: CARD_3:55

for f being Function holds sproduct f c= PFuncs ((dom f),(union (rng f)))