theorem
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;