theorem Th40: :: RUSUB_1:40

for V being RealUnitarySpace
for v being VECTOR of V holds v + ((Omega). V) = the carrier of V by STRUCT_0:def 5, Lm3;