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 (proj1 f) /\ (proj1 h) or f . x = h . x )
assume A2: x in (dom f) /\ (dom h) ; :: thesis: f . x = h . x
then A3: x in dom f by XBOOLE_0:def 4;
A4: x in dom h by A2, XBOOLE_0:def 4;
then x in dom (g +* h) by Th13;
then A5: x in (dom f) /\ (dom (g +* h)) by A3, XBOOLE_0:def 4;
(g +* h) . x = h . x by A4, Th14;
hence f . x = h . x by A1, A5, PARTFUN1:def 6; :: thesis: verum