for X being non empty TopSpace holds CLSStruct(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))) #) is Subspace of ComplexVectSpace the carrier of X by Th40;