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