theorem :: NORMSP_3:50

for X being RealLinearSpace
for v being Element of X
for a being Real
for v1 being Element of (RLSp2RVSp X)
for a1 being Element of F_Real st v = v1 & a = a1 holds
a * v = a1 * v1 ;