theorem :: RUSUB_3:30

for V being RealUnitarySpace
for v being VECTOR of V holds v in Lin {v}