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;
hence rng g c= dom f by FUNCT_1:15; :: thesis: verum