theorem Th9: :: LOPBAN_6:9

for X being RealNormSpace
for V being Subset of X
for a being Real
for V1 being Subset of (LinearTopSpaceNorm X) st V = V1 holds
a * V = a * V1