let f, g 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 object st [x,y] in (rng g) |` f holds
[x,y] in g

proof

let x, y be object ; :: 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 object st [x1,y] in g by XTUPLE_0:def 13;
[x,y] in f by A3, RELAT_1:def 12;
hence [x,y] in g by A1, A2, A4, Th9; :: thesis: verum

end;

then A5: (rng g) |` f c= g ;
(rng g) |` g c= (rng g) |` f by A1, RELAT_1:101;
then g c= (rng g) |` f ;
hence (rng g) |` f = g by A5; :: thesis: verum