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:27, XBOOLE_1:1;
A6: dom (g * h) = dom h by A2, A3, RELAT_1:27, XBOOLE_1:1;

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

let x be object ; :: 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:13;
A9: (g * h) . x = g . (h . x) by A7, FUNCT_1:13;
h . x in rng h by A7, FUNCT_1:3;
hence (f * h) . x = (g * h) . x by A3, A4, A8, A9; :: thesis: verum

end;

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