let N be Element of NAT ; :: thesis: for r being Real
for w being Point of (TOP-REAL N) holds (abs r) * |.w.| = |.(r * w).|
let r be Real; :: thesis: for w being Point of (TOP-REAL N) holds (abs r) * |.w.| = |.(r * w).|
let w be Point of (TOP-REAL N); :: thesis: (abs r) * |.w.| = |.(r * w).|
reconsider w2 = w as Element of REAL N by EUCLID:22;
thus (abs r) * |.w.| = |.(r * w2).| by EUCLID:11
.= |.(r * w).| ; :: thesis: verum