theorem Th23: :: FUNCOP_1:23

for f, g, h being Function
for A being set
for F being Function st f | A = g | A holds
(F .: (f,h)) | A = (F .: (g,h)) | A