theorem Th70: :: FUNCT_4:70

for f being Function
for A, B being set st dom f c= A \/ B holds
(f | A) +* (f | B) = f