theorem :: TOPREAL6:25

for p, q being Point of (Euclid 2)
for z being Point of (TOP-REAL 2) st p = 0.REAL 2 & q = z holds
dist (p,q) = |.z.|