:: deftheorem Def2 defines rng-retract ALGSPEC1:def 2 :
for f, b₂ being Function holds
( b₂ is rng-retract of f iff ( dom b₂ = rng f & f * b₂ = id (rng f) ) );