theorem :: NORMSP_3:51

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