:: deftheorem Def2 defines dist NAGATA_2:def 2 :
for X being set
for f being Function of [:X,X:],REAL
for x being Element of X
for b₄ being Function of X,REAL holds
( b₄ = dist (f,x) iff for y being Element of X holds b₄ . y = f . (x,y) );