theorem Th57: :: FOMODEL0:57

for X being set
for f, g being Function holds (f | X) +* g = (f | (X \ (dom g))) \/ g