let X be non empty closed_interval Subset of REAL; for Y being RealNormSpace holds R_NormSpace_of_ContinuousFunctions (X,Y) is RealNormSpace
let Y be RealNormSpace; 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; verum