let f, g, h be Function; :: thesis: ( rng h c= dom f implies f * (g +* h) = (f * g) +* (f * h) )
assume A1: rng h c= dom f ; :: thesis: f * (g +* h) = (f * g) +* (f * h)
A2: dom h c= dom (g +* h) by FUNCT_4:10;
A3: dom g c= dom (g +* h) by FUNCT_4:10;
A4: dom (f * (g +* h)) = (dom (f * g)) \/ (dom (f * h))

proof

thus dom (f * (g +* h)) c= (dom (f * g)) \/ (dom (f * h)) :: according to XBOOLE_0:def 10 :: thesis: (dom (f * g)) \/ (dom (f * h)) c= dom (f * (g +* h))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (f * (g +* h)) or x in (dom (f * g)) \/ (dom (f * h)) )
assume A5: x in dom (f * (g +* h)) ; :: thesis: x in (dom (f * g)) \/ (dom (f * h))
then A6: (g +* h) . x in dom f by FUNCT_1:11;
x in dom (g +* h) by A5, FUNCT_1:11;
then A7: x in (dom g) \/ (dom h) by FUNCT_4:def 1;

per cases ( x in dom h or not x in dom h ) ;

suppose A8: x in dom h ; :: thesis: x in (dom (f * g)) \/ (dom (f * h))

then h . x in dom f by A6, FUNCT_4:13;
then x in dom (f * h) by A8, FUNCT_1:11;
hence x in (dom (f * g)) \/ (dom (f * h)) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose not x in dom h ; :: thesis: x in (dom (f * g)) \/ (dom (f * h))

then ( g . x in dom f & x in dom g ) by A7, A6, FUNCT_4:11, XBOOLE_0:def 3;
then x in dom (f * g) by FUNCT_1:11;
hence x in (dom (f * g)) \/ (dom (f * h)) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (dom (f * g)) \/ (dom (f * h)) or x in dom (f * (g +* h)) )
assume A9: x in (dom (f * g)) \/ (dom (f * h)) ; :: thesis: x in dom (f * (g +* h))

per cases ( x in dom (f * h) or not x in dom (f * h) ) ;

suppose A10: x in dom (f * h) ; :: thesis: x in dom (f * (g +* h))

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

end;

suppose A13: not x in dom (f * h) ; :: thesis: x in dom (f * (g +* h))

( x in dom h implies h . x in dom f )

proof

assume x in dom h ; :: thesis: h . x in dom f
then h . x in rng h by FUNCT_1:3;
hence h . x in dom f by A1; :: thesis: verum

end;

then not x in dom h by A13, FUNCT_1:11;
then A14: (g +* h) . x = g . x by FUNCT_4:11;
x in dom (f * g) by A9, A13, XBOOLE_0:def 3;
then ( g . x in dom f & x in dom g ) by FUNCT_1:11;
hence x in dom (f * (g +* h)) by A3, A14, FUNCT_1:11; :: thesis: verum

end;

end;

end;

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

let x be object ; :: thesis: ( x in (dom (f * g)) \/ (dom (f * h)) implies ( ( x in dom (f * h) implies (f * (g +* h)) . x = (f * h) . x ) & ( not x in dom (f * h) implies (f * (g +* h)) . x = (f * g) . x ) ) )
assume A15: x in (dom (f * g)) \/ (dom (f * h)) ; :: thesis: ( ( x in dom (f * h) implies (f * (g +* h)) . x = (f * h) . x ) & ( not x in dom (f * h) implies (f * (g +* h)) . x = (f * g) . x ) )
thus ( x in dom (f * h) implies (f * (g +* h)) . x = (f * h) . x ) :: thesis: ( not x in dom (f * h) implies (f * (g +* h)) . x = (f * g) . x )

proof

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

end;

assume A17: not x in dom (f * h) ; :: thesis: (f * (g +* h)) . x = (f * g) . x
( x in dom h implies h . x in dom f )

proof

assume x in dom h ; :: thesis: h . x in dom f
then h . x in rng h by FUNCT_1:3;
hence h . x in dom f by A1; :: thesis: verum

end;

then A18: not x in dom h by A17, FUNCT_1:11;
x in dom (f * g) by A15, A17, XBOOLE_0:def 3;
then A19: x in dom g by FUNCT_1:11;
hence (f * (g +* h)) . x = f . ((g +* h) . x) by A3, FUNCT_1:13
.= f . (g . x) by A18, FUNCT_4:11
.= (f * g) . x by A19, FUNCT_1:13 ;
:: thesis: verum

end;

hence f * (g +* h) = (f * g) +* (f * h) by A4, FUNCT_4:def 1; :: thesis: verum