theorem Th123: :: FUNCT_4:123

for f, g, h being Function st f c= g holds
f +* h c= g +* h