theorem Th2: :: FUNCT_1:2

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