let f, g, h be Function; :: thesis: ( f | (dom g) = g & rng h c= dom g & rng h c= dom f implies f * h = g * h )
assume AS: ( f | (dom g) = g & rng h c= dom g & rng h c= dom f ) ; :: thesis: f * h = g * h
P1: dom (f * h) = dom h by AS, RELAT_1:27;
P2: dom (g * h) = dom h by AS, RELAT_1:27;
for x being object st x in dom (f * h) holds
(f * h) . x = (g * h) . x
proof
let x be object ; :: thesis: ( x in dom (f * h) implies (f * h) . x = (g * h) . x )
assume AS1: x in dom (f * h) ; :: thesis: (f * h) . x = (g * h) . x
then x in dom h by AS, RELAT_1:27;
then P3: h . x in rng h by FUNCT_1:3;
thus (f * h) . x = f . (h . x) by FUNCT_1:12, AS1
.= (f | (dom g)) . (h . x) by AS, P3, FUNCT_1:49
.= (g * h) . x by AS, AS1, P1, P2, FUNCT_1:12 ; :: thesis: verum
end;
hence f * h = g * h by AS, P1, RELAT_1:27; :: thesis: verum