let f, g, h be Function; :: thesis: ( f c= g & (rng h) /\ (dom g) c= dom f implies g * h = f * h )
assume A1: ( f c= g & (rng h) /\ (dom g) c= dom f ) ; :: thesis: g * h = f * h
A2: dom (f * h) = dom (g * h)

proof

f * h c= g * h by A1, RELAT_1:48;
hence dom (f * h) c= dom (g * h) by RELAT_1:25; :: according to XBOOLE_0:def 10 :: thesis: dom (g * h) c= dom (f * h)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (g * h) or x in dom (f * h) )
assume x in dom (g * h) ; :: thesis: x in dom (f * h)
then A3: ( x in dom h & h . x in dom g ) by FUNCT_1:21;
then h . x in rng h by FUNCT_1:def 5;
then h . x in (rng h) /\ (dom g) by A3, XBOOLE_0:def 4;
hence x in dom (f * h) by A1, A3, FUNCT_1:21; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in dom (f * h) implies (g * h) . x = (f * h) . x )
assume x in dom (f * h) ; :: thesis: (g * h) . x = (f * h) . x
then A4: ( x in dom h & h . x in dom f & h . x in dom g ) by A2, FUNCT_1:21;
then ( h . x in rng h & (g * h) . x = g . (h . x) & (f * h) . x = f . (h . x) ) by FUNCT_1:23, FUNCT_1:def 5;
hence (g * h) . x = (f * h) . x by A1, A4, GRFUNC_1:8; :: thesis: verum

end;

hence g * h = f * h by A2, FUNCT_1:9; :: thesis: verum