:: deftheorem Def8 defines Toler NAGATA_1:def 8 :
for A, B being non empty set
for F being Function of A,(Funcs (A,B))
for b₄ being Function of A,B holds
( b₄ = F Toler iff for p being Element of A holds b₄ . p = (F . p) . p );