let f, g, h be Function; :: thesis: (f +* g) +* h = f +* (g +* h)

A1: now

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

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

assume A2: x in dom (g +* h) ; :: thesis: ((f +* g) +* h) . x = (g +* h) . x

per cases ( ( x in dom g & not x in dom h ) or x in dom h ) by A2, Th13;

suppose A3: ( x in dom g & not x in dom h ) ; :: thesis: ((f +* g) +* h) . x = (g +* h) . x

hence ((f +* g) +* h) . x = (f +* g) . x by Th12
.= g . x by A3, Th14
.= (g +* h) . x by A3, Th12 ;
:: thesis: verum

end;

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

hence ((f +* g) +* h) . x = h . x by Th14
.= (g +* h) . x by A4, Th14 ;
:: thesis: verum

end;

end;

end;

assume A5: not x in dom (g +* h) ; :: thesis: ((f +* g) +* h) . x = f . x
then A6: not x in dom g by Th13;
not x in dom h by A5, Th13;
hence ((f +* g) +* h) . x = (f +* g) . x by Th12
.= f . x by A6, Th12 ;
:: thesis: verum

end;

dom ((f +* g) +* h) = (dom (f +* g)) \/ (dom h) by Def1
.= ((dom f) \/ (dom g)) \/ (dom h) by Def1
.= (dom f) \/ ((dom g) \/ (dom h)) by XBOOLE_1:4
.= (dom f) \/ (dom (g +* h)) by Def1 ;
hence (f +* g) +* h = f +* (g +* h) by A1, Def1; :: thesis: verum