theorem Th5: :: AOFA_000:5

for f, g being Function
for x, X being set st x nin X & x in dom g holds
((f,X) +* g) . x = g . x