let f, g, h, h1, h2 be Function; :: thesis: ( dom h1 c= dom h & dom h2 c= dom h implies (f +* g) +* h = ((f +* h1) +* (g +* h2)) +* h )
assume that
A1: dom h1 c= dom h and
A2: dom h2 c= dom h ; :: thesis: (f +* g) +* h = ((f +* h1) +* (g +* h2)) +* h
( dom (f +* h1) = (dom f) \/ (dom h1) & dom (g +* h2) = (dom g) \/ (dom h2) ) by FUNCT_4:def 1;
then dom ((f +* h1) +* (g +* h2)) = ((dom f) \/ (dom h1)) \/ ((dom g) \/ (dom h2)) by FUNCT_4:def 1;
then dom (((f +* h1) +* (g +* h2)) +* h) = (((dom f) \/ (dom h1)) \/ ((dom g) \/ (dom h2))) \/ (dom h) by FUNCT_4:def 1;
then dom (((f +* h1) +* (g +* h2)) +* h) = ((dom f) \/ (dom h1)) \/ (((dom g) \/ (dom h2)) \/ (dom h)) by XBOOLE_1:4;
then dom (((f +* h1) +* (g +* h2)) +* h) = ((dom f) \/ (dom h1)) \/ ((dom g) \/ ((dom h2) \/ (dom h))) by XBOOLE_1:4;
then dom (((f +* h1) +* (g +* h2)) +* h) = ((dom f) \/ (dom h1)) \/ ((dom g) \/ (dom h)) by A2, XBOOLE_1:12;
then dom (((f +* h1) +* (g +* h2)) +* h) = (((dom f) \/ (dom h1)) \/ (dom h)) \/ (dom g) by XBOOLE_1:4;
then dom (((f +* h1) +* (g +* h2)) +* h) = ((dom f) \/ ((dom h1) \/ (dom h))) \/ (dom g) by XBOOLE_1:4;
then A3: dom (((f +* h1) +* (g +* h2)) +* h) = ((dom f) \/ (dom h)) \/ (dom g) by A1, XBOOLE_1:12;
A4: for b being object st b in dom ((f +* g) +* h) holds
((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b

proof

let b be object ; :: thesis: ( b in dom ((f +* g) +* h) implies ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b )
assume b in dom ((f +* g) +* h) ; :: thesis: ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b

A5: now :: thesis: ( not b in dom h implies ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b )

assume A6: not b in dom h ; :: thesis: ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b
then A7: (((f +* h1) +* (g +* h2)) +* h) . b = ((f +* h1) +* (g +* h2)) . b by FUNCT_4:11;
A8: ((f +* g) +* h) . b = (f +* g) . b by A6, FUNCT_4:11;

A9: now :: thesis: ( b in dom g implies ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b )

A10: not b in dom h2 by A2, A6;
assume A11: b in dom g ; :: thesis: ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b
dom g c= (dom g) \/ (dom h2) by XBOOLE_1:7;
then b in (dom g) \/ (dom h2) by A11;
then b in dom (g +* h2) by FUNCT_4:def 1;
then A12: (((f +* h1) +* (g +* h2)) +* h) . b = (g +* h2) . b by A7, FUNCT_4:13;
((f +* g) +* h) . b = g . b by A8, A11, FUNCT_4:13;
hence ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b by A12, A10, FUNCT_4:11; :: thesis: verum

end;

now :: thesis: ( not b in dom g implies ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b )

A13: not b in dom h1 by A1, A6;
assume A14: not b in dom g ; :: thesis: ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b
not b in dom h2 by A2, A6;
then not b in (dom g) \/ (dom h2) by A14, XBOOLE_0:def 3;
then not b in dom (g +* h2) by FUNCT_4:def 1;
then A15: (((f +* h1) +* (g +* h2)) +* h) . b = (f +* h1) . b by A7, FUNCT_4:11;
((f +* g) +* h) . b = f . b by A8, A14, FUNCT_4:11;
hence ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b by A15, A13, FUNCT_4:11; :: thesis: verum

end;

hence ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b by A9; :: thesis: verum

end;

now :: thesis: ( b in dom h implies ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b )

assume A16: b in dom h ; :: thesis: ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b
then ((f +* g) +* h) . b = h . b by FUNCT_4:13;
hence ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b by A16, FUNCT_4:13; :: thesis: verum

end;

hence ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b by A5; :: thesis: verum

end;

dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
then dom ((f +* g) +* h) = ((dom f) \/ (dom g)) \/ (dom h) by FUNCT_4:def 1;
hence (f +* g) +* h = ((f +* h1) +* (g +* h2)) +* h by A3, A4, FUNCT_1:2, XBOOLE_1:4; :: thesis: verum