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) = |.r.| * (Norm v)

let r be Real; :: thesis: for v being Element of V holds Norm (r * v) = |.r.| * (Norm v)

let v be Element of V; :: thesis: Norm (r * v) = |.r.| * (Norm v)

thus Norm (r * v) = dist ((r * (0. V)),(r * v)) by RLVECT_1:10

.= |.r.| * (Norm v) by Def5 ; :: thesis: verum

for v being Element of V holds Norm (r * v) = |.r.| * (Norm v)

let r be Real; :: thesis: for v being Element of V holds Norm (r * v) = |.r.| * (Norm v)

let v be Element of V; :: thesis: Norm (r * v) = |.r.| * (Norm v)

thus Norm (r * v) = dist ((r * (0. V)),(r * v)) by RLVECT_1:10

.= |.r.| * (Norm v) by Def5 ; :: thesis: verum