let f, g, h be Function; :: thesis: for A being set st A c= dom f & A c= dom g & rng h c= A & ( for x being set st x in A holds
f . x = g . x ) holds
f * h = g * h
let A be set ; :: thesis: ( A c= dom f & A c= dom g & rng h c= A & ( for x being set st x in A holds
f . x = g . x ) implies f * h = g * h )
assume that
A1: A c= dom f and
A2: A c= dom g and
A3: rng h c= A and
A4: for x being set st x in A holds
f . x = g . x ; :: thesis: f * h = g * h
A5: dom (f * h) = dom h by A1, A3, RELAT_1:46, XBOOLE_1:1;
A6: dom (g * h) = dom h by A2, A3, RELAT_1:46, XBOOLE_1:1;

now

let x be set ; :: thesis: ( x in dom h implies (f * h) . x = (g * h) . x )
assume A7: x in dom h ; :: thesis: (f * h) . x = (g * h) . x
then A8: (f * h) . x = f . (h . x) by FUNCT_1:23;
A9: (g * h) . x = g . (h . x) by A7, FUNCT_1:23;
h . x in rng h by A7, FUNCT_1:12;
hence (f * h) . x = (g * h) . x by A3, A4, A8, A9; :: thesis: verum

end;

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