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

proof

let x be object ; :: thesis: ( x in dom g implies g . x = x )
assume x in dom g ; :: thesis: g . x = x
then ex y being object st
( y in dom f & f . y = x ) by A1, Def3;
hence g . x = x by A2, Th13; :: thesis: verum

end;

hence g = id (dom g) by Th17; :: thesis: verum