theorem :: FUNCT_7:27
for f, g, h being Function
for A being set st f,g equal_outside A & g,h equal_outside A holds
f,h equal_outside A ;