theorem Th23: :: FUNCT_1:23

for f, g being Function st rng f = dom g & g * f = f holds
g = id (dom g)