let f, g, h be Function; :: thesis: (f +* g) +* h = f +* (g +* h)
A1: now :: thesis: for x being object st x in (dom f) \/ (dom (g +* h)) holds
( ( 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 ) )
let x be object ; :: 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, Th12;
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 Th11
.= g . x by A3, Th13
.= (g +* h) . x by A3, Th11 ;
:: 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 Th13
.= (g +* h) . x by A4, Th13 ;
:: 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 Th12;
not x in dom h by A5, Th12;
hence ((f +* g) +* h) . x = (f +* g) . x by Th11
.= f . x by A6, Th11 ;
:: 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