for f being FinSequence of REAL
for p being Point of (TOP-REAL 2) st len f = 2 & p = f holds
|.p.| = |.f.| ;