let f, g, h be Function; :: thesis: ( f tolerates g & g tolerates h & h tolerates f implies f +* g tolerates h )
assume A1: ( f tolerates g & g tolerates h & h tolerates f ) ; :: thesis: f +* g tolerates h
let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( not x in (dom (f +* g)) /\ (dom h) or (f +* g) . x = h . x )
assume x in (dom (f +* g)) /\ (dom h) ; :: thesis: (f +* g) . x = h . x
then ( x in dom (f +* g) & x in dom h ) by XBOOLE_0:def 4;
then ( ( x in dom f or x in dom g ) & x in dom h ) by FUNCT_4:13;
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, FUNCT_4:14, FUNCT_4:16, XBOOLE_0:def 4;
hence (f +* g) . x = h . x by A1, PARTFUN1:def 6; :: thesis: verum