theorem :: C0SP3:12

for S, T being RealNormSpace holds RLSStruct(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))) #) is Subspace of RealVectSpace ( the carrier of S,T) by Th11, RSSPACE:11;