let X be set ; :: thesis: for f, g being Function st dom f = X & dom g = X & rng g c= X & f is one-to-one & f * g = f holds
g = id X
let f, g be Function; :: thesis: ( dom f = X & dom g = X & rng g c= X & f is one-to-one & f * g = f implies g = id X )
assume that
A1: dom f = X and
A2: dom g = X and
A3: ( rng g c= X & f is one-to-one ) and
A4: f * g = f ; :: thesis: g = id X
for x being object st x in X holds
g . x = x

proof

let x be object ; :: thesis: ( x in X implies g . x = x )
assume A5: x in X ; :: thesis: g . x = x
then ( g . x in rng g & f . x = f . (g . x) ) by A2, A4, Def3, Th13;
hence g . x = x by A1, A3, A5; :: thesis: verum

end;

hence g = id X by A2, Th17; :: thesis: verum