let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital homogeneous RLSMetrStruct ; :: thesis: for r being Real
for v being Element of V holds Norm (r * v) = (abs r) * (Norm v)
let r be Real; :: thesis: for v being Element of V holds Norm (r * v) = (abs r) * (Norm v)
let v be Element of V; :: thesis: Norm (r * v) = (abs r) * (Norm v)
thus Norm (r * v) = dist ((r * (0. V)),(r * v)) by RLVECT_1:23
.= (abs r) * (Norm v) by Def5 ; :: thesis: verum