let f, g, h be Function; :: thesis: ( f tolerates g +* h implies f tolerates h )
assume A1: f tolerates g +* h ; :: thesis: f tolerates h
let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( not x in (dom f) /\ (dom h) or f . x = h . x )
assume x in (dom f) /\ (dom h) ; :: thesis: f . x = h . x
then ( x in dom f & x in dom h ) by XBOOLE_0:def 4;
then ( x in dom f & x in dom (g +* h) & (g +* h) . x = h . x ) by Th13, Th14;
then ( x in (dom f) /\ (dom (g +* h)) & (g +* h) . x = h . x ) by XBOOLE_0:def 4;
hence f . x = h . x by A1, PARTFUN1:def 6; :: thesis: verum