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

proof

f * h c= g * h by A1, RELAT_1:29;
hence dom (f * h) c= dom (g * h) by RELAT_1:11; :: according to XBOOLE_0:def 10 :: thesis: dom (g * h) c= dom (f * h)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (g * h) or x in dom (f * h) )
assume A4: x in dom (g * h) ; :: thesis: x in dom (f * h)
then A5: h . x in dom g by FUNCT_1:11;
A6: x in dom h by A4, FUNCT_1:11;
then h . x in rng h by FUNCT_1:def 3;
then h . x in (rng h) /\ (dom g) by A5, XBOOLE_0:def 4;
hence x in dom (f * h) by A2, A6, FUNCT_1:11; :: thesis: verum

end;

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

let x be object ; :: thesis: ( x in dom (f * h) implies (g * h) . x = (f * h) . x )
assume A7: x in dom (f * h) ; :: thesis: (g * h) . x = (f * h) . x
then A8: x in dom h by FUNCT_1:11;
then A9: (g * h) . x = g . (h . x) by FUNCT_1:13;
A10: (f * h) . x = f . (h . x) by A8, FUNCT_1:13;
h . x in dom f by A7, FUNCT_1:11;
hence (g * h) . x = (f * h) . x by A1, A9, A10, GRFUNC_1:2; :: thesis: verum

end;

hence g * h = f * h by A3; :: thesis: verum