let f, g be Function; :: thesis: f tolerates g +* f
let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (dom f) /\ (dom (g +* f)) or f . x = (g +* f) . x )
assume x in (dom f) /\ (dom (g +* f)) ; :: thesis: f . x = (g +* f) . x
then ( x in (dom f) /\ ((dom g) \/ (dom f)) & (dom f) /\ ((dom g) \/ (dom f)) = dom f ) by FUNCT_4:def 1, XBOOLE_1:21;
hence (g +* f) . x = f . x by FUNCT_4:13; :: thesis: verum