for X being set
for f, g being Function of X,X holds f +* g = g by Th37;