for r being Real
for f, g being ExtReal st r <> 0 & r * f = r * g holds
f = g