let f, g be Function; :: thesis: ( dom f c= dom g implies ( f tolerates g iff for x being set st x in dom f holds
f . x = g . x ) )
assume dom f c= dom g ; :: thesis: ( f tolerates g iff for x being set st x in dom f holds
f . x = g . x )
then (dom f) /\ (dom g) = dom f by XBOOLE_1:28;
hence ( f tolerates g iff for x being set st x in dom f holds
f . x = g . x ) by Def4; :: thesis: verum