let g, f be Function; :: thesis: ( g c= f & f is one-to-one implies (rng g) | f = g )
assume A1: g c= f ; :: thesis: ( not f is one-to-one or (rng g) | f = g )
assume A2: f is one-to-one ; :: thesis: (rng g) | f = g
for x, y being set st [x,y] in (rng g) | f holds
[x,y] in g

proof

let x, y be set ; :: thesis: ( [x,y] in (rng g) | f implies [x,y] in g )
assume A3: [x,y] in (rng g) | f ; :: thesis: [x,y] in g
then y in rng g by RELAT_1:def 12;
then A4: ex x1 being set st [x1,y] in g by RELAT_1:def 5;
[x,y] in f by A3, RELAT_1:def 12;
hence [x,y] in g by A1, A2, A4, Th25; :: thesis: verum

end;

then A5: (rng g) | f c= g by RELAT_1:def 3;
(rng g) | g c= (rng g) | f by A1, RELAT_1:101;
then g c= (rng g) | f by RELAT_1:94;
hence (rng g) | f = g by A5, XBOOLE_0:def 10; :: thesis: verum