theorem Th49: :: CARD_3:49

for f, g being Function st g in sproduct f holds
( dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) )