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

now

let x be set ; :: thesis: ( x in ((dom f) \/ (dom g)) \/ (dom h) implies ((f +* g) +* h) . b₁ = ((g +* f) +* h) . b₁ )
assume A5: x in ((dom f) \/ (dom g)) \/ (dom h) ; :: thesis: ((f +* g) +* h) . b₁ = ((g +* f) +* h) . b₁

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

suppose x in dom h ; :: thesis: ((f +* g) +* h) . b₁ = ((g +* f) +* h) . b₁

then ( ((f +* g) +* h) . x = h . x & ((g +* f) +* h) . x = h . x ) by FUNCT_4:14;
hence ((f +* g) +* h) . x = ((g +* f) +* h) . x ; :: thesis: verum

end;

suppose A6: not x in dom h ; :: thesis: ((f +* g) +* h) . b₁ = ((g +* f) +* h) . b₁

then A7: ( x in (dom g) \/ (dom f) & not x in (dom f) /\ (dom g) ) by A4, A5, XBOOLE_0:def 3;
A8: ( ((f +* g) +* h) . x = (f +* g) . x & ((g +* f) +* h) . x = (g +* f) . x ) by A6, FUNCT_4:12;
( ( x in dom f or x in dom g ) & ( not x in dom f or not x in dom g ) ) by A7, XBOOLE_0:def 3, XBOOLE_0:def 4;
then ( ( (f +* g) . x = f . x & (g +* f) . x = f . x ) or ( (f +* g) . x = g . x & (g +* f) . x = g . x ) ) by FUNCT_4:12, FUNCT_4:14;
hence ((f +* g) +* h) . x = ((g +* f) +* h) . x by A8; :: thesis: verum

end;

end;

end;

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