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

A4: now :: thesis: for x being object st x in rng f holds
(f * g) . x = (id (rng f)) . x

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

end;

take g ; :: thesis: ( dom g = rng f & f * g = id (rng f) )
thus dom g = rng f by A2; :: thesis: f * g = id (rng f)
dom (f * g) = rng f by A2, RELAT_1:27;
hence f * g = id (rng f) by A4; :: thesis: verum