let f, g, h be Function; :: thesis: (g +* h) * f = (g * f) +* (h * f)
A1: dom ((g +* h) * f) = (dom (g * f)) \/ (dom (h * f))

proof

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

proof

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

end;

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

end;

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

let x be object ; :: thesis: ( x in (dom (g * f)) \/ (dom (h * f)) implies ( ( x in dom (h * f) implies ((g +* h) * f) . x = (h * f) . x ) & ( not x in dom (h * f) implies ((g +* h) * f) . x = (g * f) . x ) ) )
assume x in (dom (g * f)) \/ (dom (h * f)) ; :: thesis: ( ( x in dom (h * f) implies ((g +* h) * f) . x = (h * f) . x ) & ( not x in dom (h * f) implies ((g +* h) * f) . x = (g * f) . x ) )
then ( x in dom (g * f) or x in dom (h * f) ) by XBOOLE_0:def 3;
then A6: x in dom f by FUNCT_1:11;

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

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

end;

assume not x in dom (h * f) ; :: thesis: ((g +* h) * f) . x = (g * f) . x
then A9: not f . x in dom h by A6, FUNCT_1:11;
thus ((g +* h) * f) . x = (g +* h) . (f . x) by A6, FUNCT_1:13
.= g . (f . x) by A9, FUNCT_4:11
.= (g * f) . x by A6, FUNCT_1:13 ; :: thesis: verum

end;

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