theorem Th12: :: FUNCT_2:12

for X, Y being set
for f1, f2 being Function of X,Y st ( for x being object st x in X holds
f1 . x = f2 . x ) holds
f1 = f2