let f1, f2, g be Function; :: thesis: ( rng g c= dom f2 implies (f1 +* f2) * g = f2 * g )
assume Z0: rng g c= dom f2 ; :: thesis: (f1 +* f2) * g = f2 * g
dom (f1 +* f2) = (dom f1) \/ (dom f2) by FUNCT_4:def 1;
then Z2: ( dom ((f1 +* f2) * g) = dom g & dom (f2 * g) = dom g ) by Z0, RELAT_1:46, XBOOLE_1:10;

now

let x be set ; :: thesis: ( x in dom g implies ((f1 +* f2) * g) . x = (f2 * g) . x )
assume x in dom g ; :: thesis: ((f1 +* f2) * g) . x = (f2 * g) . x
then ( ((f1 +* f2) * g) . x = (f1 +* f2) . (g . x) & (f2 * g) . x = f2 . (g . x) & g . x in rng g ) by FUNCT_1:12, FUNCT_1:23;
hence ((f1 +* f2) * g) . x = (f2 * g) . x by Z0, FUNCT_4:14; :: thesis: verum

end;

hence (f1 +* f2) * g = f2 * g by Z2, FUNCT_1:9; :: thesis: verum