theorem Th23: :: ALGSPEC1:23

for f being Function
for g being rng-retract of f holds rng g c= dom f