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 A1: ( rng g c= dom f1 & rng g c= dom f2 & f1 tolerates f2 ) ; :: thesis: f1 * g = f2 * g
then A2: ( dom (f1 * g) = dom g & dom (f2 * g) = dom g ) by RELAT_1:46;

now

let x be set ; :: thesis: ( x in dom g implies (f1 * g) . x = (f2 * g) . x )
assume x in dom g ; :: thesis: (f1 * g) . x = (f2 * g) . x
then A3: ( g . x in rng g & (f1 * g) . x = f1 . (g . x) & (f2 * g) . x = f2 . (g . x) ) by A2, FUNCT_1:22, FUNCT_1:def 5;
then g . x in (dom f1) /\ (dom f2) by A1, XBOOLE_0:def 4;
hence (f1 * g) . x = (f2 * g) . x by A1, A3, PARTFUN1:def 6; :: thesis: verum

end;

hence f1 * g = f2 * g by A2, FUNCT_1:9; :: thesis: verum