defpred S₁[ set , set ] means f . $2 = $1;
A1: dom (id (rng f)) = rng f by RELAT_1:45;
A2: for o being set st o in rng f holds
ex y being set st
( y in dom f & S₁[o,y] ) by FUNCT_1:def 3;
consider g being Function such that
A3: ( dom g = rng f & rng g c= dom f ) and
A4: for o being set st o in rng f holds
S₁[o,g . o] from FUNCT_1:sch 5(A2);

A5: now

let x be set ; :: thesis: ( x in rng f implies (f * g) . x = (id (rng f)) . x )
assume A6: x in rng f ; :: thesis: (f * g) . x = (id (rng f)) . x
then A7: (f * g) . x = f . (g . x) by A3, FUNCT_1:13;
f . (g . x) = x by A4, A6;
hence (f * g) . x = (id (rng f)) . x by A6, A7, FUNCT_1:18; :: thesis: verum

end;

take g ; :: thesis: ( dom g = rng f & f * g = id (rng f) )
thus dom g = rng f by A3; :: thesis: f * g = id (rng f)
dom (f * g) = rng f by A3, RELAT_1:27;
hence f * g = id (rng f) by A1, A5, FUNCT_1:2; :: thesis: verum