theorem Th74: :: CSSPACE:79

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