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 object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (dom f) /\ (dom 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 Th12;
then A5: x in (dom f) /\ (dom (g +* h)) by A3, XBOOLE_0:def 4;
(g +* h) . x = h . x by A4, Th13;
hence f . x = h . x by A1, A5; :: thesis: verum