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 A1: ( dom h1 c= dom h & dom h2 c= dom h ) ; :: thesis: (f +* g) +* h = ((f +* h1) +* (g +* h2)) +* h
dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
then A2: dom ((f +* g) +* h) = ((dom f) \/ (dom g)) \/ (dom h) by FUNCT_4:def 1;
( 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 A1, 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 dom (((f +* h1) +* (g +* h2)) +* h) = ((dom f) \/ (dom h)) \/ (dom g) by A1, XBOOLE_1:12;
then A3: dom (((f +* h1) +* (g +* h2)) +* h) = dom ((f +* g) +* h) by A2, XBOOLE_1:4;
for b being set st b in dom ((f +* g) +* h) holds
((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b

proof

let b be set ; :: 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

A4: now

assume A5: not b in dom h ; :: thesis: ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b
then A6: ( ((f +* g) +* h) . b = (f +* g) . b & (((f +* h1) +* (g +* h2)) +* h) . b = ((f +* h1) +* (g +* h2)) . b ) by FUNCT_4:12;

A7: now

assume A8: not b in dom g ; :: thesis: ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b
then A9: ((f +* g) +* h) . b = f . b by A6, FUNCT_4:12;
not b in dom h2 by A1, A5;
then not b in (dom g) \/ (dom h2) by A8, XBOOLE_0:def 3;
then not b in dom (g +* h2) by FUNCT_4:def 1;
then A10: (((f +* h1) +* (g +* h2)) +* h) . b = (f +* h1) . b by A6, FUNCT_4:12;
not b in dom h1 by A1, A5;
hence ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b by A9, A10, FUNCT_4:12; :: thesis: verum

end;

now

assume A11: b in dom g ; :: thesis: ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b
then A12: ((f +* g) +* h) . b = g . b by A6, FUNCT_4:14;
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 A13: (((f +* h1) +* (g +* h2)) +* h) . b = (g +* h2) . b by A6, FUNCT_4:14;
not b in dom h2 by A1, A5;
hence ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b by A12, A13, FUNCT_4:12; :: thesis: verum

end;

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

end;

now

assume A14: 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:14;
hence ((f +* g) +* h) . b = (((f +* h1) +* (g +* h2)) +* h) . b by A14, FUNCT_4:14; :: thesis: verum

end;

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

end;

hence (f +* g) +* h = ((f +* h1) +* (g +* h2)) +* h by A3, FUNCT_1:9; :: thesis: verum