for a being Real
for n being Nat
for x1, x2 being Element of REAL n holds
( not a * x1 = a * x2 or a = 0 or x1 = x2 )