for r being Real
for f, g being ExtReal st r + f = r + g holds
f = g