let X be non empty closed_interval Subset of REAL; :: thesis: for Y being RealNormSpace holds R_NormSpace_of_ContinuousFunctions (X,Y) is RealNormSpace
let Y be RealNormSpace; :: thesis: R_NormSpace_of_ContinuousFunctions (X,Y) is RealNormSpace
RLSStruct(# (ContinuousFunctions (X,Y)),(Zero_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),(Add_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),(Mult_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))) #) is RealLinearSpace by RSSPACE:11;
hence R_NormSpace_of_ContinuousFunctions (X,Y) is RealNormSpace by Lm3, RSSPACE3:2; :: thesis: verum