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