let f, g be Function; :: thesis: ( f is idempotent & rng g c= rng f & rng g c= dom f implies f * g = g )
assume f is idempotent ; :: thesis: ( not rng g c= rng f or not rng g c= dom f or f * g = g )
then A1: f * f = f by QUANTAL1:def 9;
assume A2: rng g c= rng f ; :: thesis: ( not rng g c= dom f or f * g = g )

A3: now :: thesis: for x being object st x in dom g holds
(f * g) . x = g . x

let x be object ; :: thesis: ( x in dom g implies (f * g) . x = g . x )
assume A4: x in dom g ; :: thesis: (f * g) . x = g . x
then g . x in rng g by FUNCT_1:def 3;
then A5: ex a being object st
( a in dom f & g . x = f . a ) by A2, FUNCT_1:def 3;
(f * g) . x = f . (g . x) by A4, FUNCT_1:13;
hence (f * g) . x = g . x by A1, A5, FUNCT_1:13; :: thesis: verum

end;

assume rng g c= dom f ; :: thesis: f * g = g
then dom (f * g) = dom g by RELAT_1:27;
hence f * g = g by A3, FUNCT_1:2; :: thesis: verum