for x being object
for n being Nat
for r being Real st x in Seg n holds
|.((0* n) +* (x,r)).| = |.r.|