theorem Th39: :: FUNCT_6:44

for f, g, h being Function st dom f = dom h & dom g = rng h & h is one-to-one & ( for x being object st x in dom h holds
f . x,g . (h . x) are_equipotent ) holds
product f, product g are_equipotent