:: deftheorem defines (Omega). CONVEX4:def 21 :
for V being ComplexLinearSpace holds (Omega). V = CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);