theorem Th9: :: CARD_3:9

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