let f, g be Function; :: thesis: ( dom f c= dom g implies ( f tolerates g iff for x being object st x in dom f holds
f . x = g . x ) )
assume dom f c= dom g ; :: thesis: ( f tolerates g iff for x being object 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 object st x in dom f holds
f . x = g . x ) ; :: thesis: verum