theorem Th4: :: AOFA_000:4

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