let f, g be Function; :: thesis: ( dom f = dom g & f tolerates g implies f = g )
assume that
A1: dom f = dom g and
A2: f tolerates g ; :: thesis: f = g
for x being set st x in dom f holds
f . x = g . x by A1, A2, Th132;
hence f = g by A1, FUNCT_1:2; :: thesis: verum