let f, g, h be Function; :: thesis: ( f tolerates g & g tolerates h & h tolerates f implies f +* g tolerates h )
assume that
A1: f tolerates g and
A2: g tolerates h and
A3: h tolerates f ; :: thesis: f +* g tolerates h
let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (dom (f +* g)) /\ (dom h) or (f +* g) . x = h . x )
assume A4: x in (dom (f +* g)) /\ (dom h) ; :: thesis: (f +* g) . x = h . x
then x in dom (f +* g) by XBOOLE_0:def 4;
then A5: ( x in dom f or x in dom g ) by Th12;
x in dom h by A4, XBOOLE_0:def 4;
then ( ( x in (dom h) /\ (dom f) & (f +* g) . x = f . x ) or ( x in (dom g) /\ (dom h) & (f +* g) . x = g . x ) ) by A1, A5, Th13, Th15, XBOOLE_0:def 4;
hence (f +* g) . x = h . x by A2, A3; :: thesis: verum