for l being CLSStruct st CLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is ComplexLinearSpace holds
l is ComplexLinearSpace