theorem Th46: :: RLSUB_1:46

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