for q being Point of (TOP-REAL 2)
for r being Real holds dist (|[0,0]|,(r * q)) = |.r.| * (dist (|[0,0]|,q))