theorem :: FUNCT_2:125

for x, A being set
for f, g being Function of {x},A st f . x = g . x holds
f = g