:: deftheorem defines = FUNCT_1:def 11 :
for f, g being Function holds
( f = g iff ( dom f = dom g & ( for x being object st x in dom f holds
f . x = g . x ) ) );