let f, g be Function; :: thesis: ( g is rng-retract of f implies rng g c= dom f )
assume ( dom g = rng f & f * g = id (rng f) ) ; :: according to ALGSPEC1:def 2 :: thesis: rng g c= dom f
then dom g = dom (f * g) by RELAT_1:71;
hence rng g c= dom f by FUNCT_1:27; :: thesis: verum