let f1, f2, g be Function; :: thesis: ( rng g c= dom f2 implies (f1 +* f2) * g = f2 * g )
assume A1: rng g c= dom f2 ; :: thesis: (f1 +* f2) * g = f2 * g

A2: now :: thesis: for x being object st x in dom g holds
((f1 +* f2) * g) . x = (f2 * g) . x

let x be object ; :: thesis: ( x in dom g implies ((f1 +* f2) * g) . x = (f2 * g) . x )
assume A3: x in dom g ; :: thesis: ((f1 +* f2) * g) . x = (f2 * g) . x
then A4: (f2 * g) . x = f2 . (g . x) by FUNCT_1:13;
A5: g . x in rng g by A3, FUNCT_1:3;
((f1 +* f2) * g) . x = (f1 +* f2) . (g . x) by A3, FUNCT_1:13;
hence ((f1 +* f2) * g) . x = (f2 * g) . x by A1, A4, A5, FUNCT_4:13; :: thesis: verum

end;

dom (f1 +* f2) = (dom f1) \/ (dom f2) by FUNCT_4:def 1;
then A6: dom ((f1 +* f2) * g) = dom g by A1, RELAT_1:27, XBOOLE_1:10;
dom (f2 * g) = dom g by A1, RELAT_1:27;
hence (f1 +* f2) * g = f2 * g by A6, A2; :: thesis: verum