theorem :: CSSPACE3:2

for l being CNORMSTR st CLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is ComplexLinearSpace holds
l is ComplexLinearSpace by CSSPACE:79;