theorem Th1: :: SUBLEMMA:1
for f, g, h, h1, h2 being Function st dom h1 c= dom h & dom h2 c= dom h holds
(f +* g) +* h = ((f +* h1) +* (g +* h2)) +* h