let f, g, h be Function; :: thesis: ( rng h c= dom f implies f * (g +* h) = (f * g) +* (f * h) )
assume ZZ: rng h c= dom f ; :: thesis: f * (g +* h) = (f * g) +* (f * h)
M: dom g c= dom (g +* h) by FUNCT_4:11;
U: dom h c= dom (g +* h) by FUNCT_4:11;
A1: 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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (f * (g +* h)) or x in (dom (f * g)) \/ (dom (f * h)) )
assume Z: x in dom (f * (g +* h)) ; :: thesis: x in (dom (f * g)) \/ (dom (f * h))
then x in dom (g +* h) by FUNCT_1:21;
then B: x in (dom g) \/ (dom h) by FUNCT_4:def 1;
A: (g +* h) . x in dom f by Z, FUNCT_1:21;

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

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

then h . x in dom f by A, FUNCT_4:14;
then x in dom (f * h) by S, FUNCT_1:21;
hence x in (dom (f * g)) \/ (dom (f * h)) by XBOOLE_0:def 3; :: thesis: verum

end;

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

then T: g . x in dom f by A, FUNCT_4:12;
x in dom g by S, B, XBOOLE_0:def 3;
then x in dom (f * g) by T, FUNCT_1:21;
hence x in (dom (f * g)) \/ (dom (f * h)) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (dom (f * g)) \/ (dom (f * h)) or x in dom (f * (g +* h)) )
assume Z: 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 S: x in dom (f * h) ; :: thesis: x in dom (f * (g +* h))

then T: x in dom h by FUNCT_1:21;
then X: (g +* h) . x = h . x by FUNCT_4:14;
h . x in dom f by S, FUNCT_1:21;
hence x in dom (f * (g +* h)) by X, U, T, FUNCT_1:21; :: thesis: verum

end;

suppose S: 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:12;
hence h . x in dom f by ZZ; :: thesis: verum

end;

then not x in dom h by S, FUNCT_1:21;
then V: (g +* h) . x = g . x by FUNCT_4:12;
K: x in dom (f * g) by S, Z, XBOOLE_0:def 3;
then L: g . x in dom f by FUNCT_1:21;
x in dom g by K, FUNCT_1:21;
hence x in dom (f * (g +* h)) by V, L, M, FUNCT_1:21; :: thesis: verum

end;

end;

end;

now

let x be set ; :: 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 Z1: 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 A: x in dom h by FUNCT_1:21;
hence (f * (g +* h)) . x = f . ((g +* h) . x) by U, FUNCT_1:23
.= f . (h . x) by A, FUNCT_4:14
.= (f * h) . x by A, FUNCT_1:23 ;
:: thesis: verum

end;

assume S: 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:12;
hence h . x in dom f by ZZ; :: thesis: verum

end;

then X: not x in dom h by S, FUNCT_1:21;
x in dom (f * g) by S, Z1, XBOOLE_0:def 3;
then V: x in dom g by FUNCT_1:21;
hence (f * (g +* h)) . x = f . ((g +* h) . x) by M, FUNCT_1:23
.= f . (g . x) by X, FUNCT_4:12
.= (f * g) . x by V, FUNCT_1:23 ;
:: thesis: verum

end;

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