let f, g, h be Function; :: thesis: ( dom f misses rng h & g .: (dom h) misses dom f implies f * (g +* h) = f * g )
assume that
A1: dom f misses rng h and
A2: g .: (dom h) misses dom f ; :: thesis: f * (g +* h) = f * g
A3: dom (f * g) = dom (f * (g +* h))

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: dom (f * (g +* h)) c= dom (f * g)

let x be object ; :: thesis: ( x in dom (f * g) implies x in dom (f * (g +* h)) )
assume A4: x in dom (f * g) ; :: thesis: x in dom (f * (g +* h))
then A5: x in dom g by FUNCT_1:11;
A6: g . x in dom f by A4, FUNCT_1:11;

now :: thesis: not x in dom h

assume x in dom h ; :: thesis: contradiction
then g . x in g .: (dom h) by A5, FUNCT_1:def 6;
hence contradiction by A2, A6, XBOOLE_0:3; :: thesis: verum

end;

then A7: g . x = (g +* h) . x by FUNCT_4:11;
x in dom (g +* h) by A5, FUNCT_4:12;
hence x in dom (f * (g +* h)) by A6, A7, FUNCT_1:11; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (f * (g +* h)) or x in dom (f * g) )
assume A8: x in dom (f * (g +* h)) ; :: thesis: x in dom (f * g)
then x in dom (g +* h) by FUNCT_1:11;
then ( ( x in dom g & not x in dom h ) or x in dom h ) by FUNCT_4:12;
then A9: ( ( x in dom g & (g +* h) . x = g . x ) or ( (g +* h) . x = h . x & h . x in rng h ) ) by FUNCT_1:def 3, FUNCT_4:11, FUNCT_4:13;
(g +* h) . x in dom f by A8, FUNCT_1:11;
hence x in dom (f * g) by A1, A9, FUNCT_1:11, XBOOLE_0:3; :: thesis: verum

end;

now :: thesis: for x being object st x in dom (f * g) holds
(f * (g +* h)) . x = (f * g) . x

let x be object ; :: thesis: ( x in dom (f * g) implies (f * (g +* h)) . x = (f * g) . x )
assume A10: x in dom (f * g) ; :: thesis: (f * (g +* h)) . x = (f * g) . x
then A11: x in dom g by FUNCT_1:11;
A12: g . x in dom f by A10, FUNCT_1:11;

now :: thesis: not x in dom h

assume x in dom h ; :: thesis: contradiction
then g . x in g .: (dom h) by A11, FUNCT_1:def 6;
hence contradiction by A2, A12, XBOOLE_0:3; :: thesis: verum

end;

then A13: g . x = (g +* h) . x by FUNCT_4:11;
x in dom (g +* h) by A11, FUNCT_4:12;
hence (f * (g +* h)) . x = f . (g . x) by A13, FUNCT_1:13
.= (f * g) . x by A11, FUNCT_1:13 ;
:: thesis: verum

end;

hence f * (g +* h) = f * g by A3; :: thesis: verum