for n being Nat
for x being Element of REAL n holds |(x,(0* n))| = 0