let f1, f2, g be Function; :: thesis: ( rng g c= dom f1 & rng g c= dom f2 & f1 tolerates f2 implies f1 * g = f2 * g )
assume that
A1: rng g c= dom f1 and
A2: rng g c= dom f2 and
A3: f1 tolerates f2 ; :: thesis: f1 * g = f2 * g
A4: dom (f2 * g) = dom g by A2, RELAT_1:27;
A5: dom (f1 * g) = dom g by A1, RELAT_1:27;
now :: thesis: for x being object st x in dom g holds
(f1 * g) . x = (f2 * g) . x
let x be object ; :: thesis: ( x in dom g implies (f1 * g) . x = (f2 * g) . x )
assume A6: x in dom g ; :: thesis: (f1 * g) . x = (f2 * g) . x
then A7: (f2 * g) . x = f2 . (g . x) by A4, FUNCT_1:12;
g . x in rng g by A6, FUNCT_1:def 3;
then A8: g . x in (dom f1) /\ (dom f2) by A1, A2, XBOOLE_0:def 4;
(f1 * g) . x = f1 . (g . x) by A5, A6, FUNCT_1:12;
hence (f1 * g) . x = (f2 * g) . x by A3, A7, A8; :: thesis: verum
end;
hence f1 * g = f2 * g by A5, A4; :: thesis: verum