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