let f, g be Function; ( f tolerates g iff ex h being Function st f \/ g = h )
( ( for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x ) iff ex h being Function st f \/ g = h )
by Th2, Th3;
hence
( f tolerates g iff ex h being Function st f \/ g = h )
by Def4; verum