for a being Real
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n st x in L & a <> 1 & a * x in L holds
0* n in L