for N being Nat
for r being Real
for w being Point of (TOP-REAL N) holds |.r.| * |.w.| = |.(r * w).| by EUCLID:11;