let f, g, h be Function; :: thesis: ( f tolerates g +* h implies f | ((dom f) \ (dom h)) tolerates g )
assume A1: f tolerates g +* h ; :: thesis: f | ((dom f) \ (dom h)) tolerates g
let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (dom (f | ((dom f) \ (dom h)))) /\ (dom g) or (f | ((dom f) \ (dom h))) . x = g . x )
assume A2: x in (dom (f | ((dom f) \ (dom h)))) /\ (dom g) ; :: thesis: (f | ((dom f) \ (dom h))) . x = g . x
then A3: x in dom (f | ((dom f) \ (dom h))) by XBOOLE_0:def 4;
x in dom g by A2, XBOOLE_0:def 4;
then A4: x in dom (g +* h) by Th12;
A5: dom (f | ((dom f) \ (dom h))) c= (dom f) \ (dom h) by RELAT_1:58;
then x in dom f by A3, XBOOLE_0:def 5;
then A6: x in (dom f) /\ (dom (g +* h)) by A4, XBOOLE_0:def 4;
not x in dom h by A3, A5, XBOOLE_0:def 5;
then (g +* h) . x = g . x by Th11;
then f . x = g . x by A1, A6;
hence (f | ((dom f) \ (dom h))) . x = g . x by A3, A5, FUNCT_1:49; :: thesis: verum