:: deftheorem Def10 defines constant FUNCT_1:def 10 :
for f being Function holds
( f is constant iff for x, y being object st x in dom f & y in dom f holds
f . x = f . y );