theorem Th65: :: CLVECT_1:65

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