theorem Th2: :: GRFUNC_1:2

for f, g being Function holds
( f c= g iff ( dom f c= dom g & ( for x being object st x in dom f holds
f . x = g . x ) ) )