theorem Th1: :: ALGSPEC1:1

for f, g, h being Function st (dom f) /\ (dom g) c= dom h holds
(f +* g) +* h = (g +* f) +* h