let X be non empty closed_interval Subset of REAL; :: thesis: for Y being RealNormSpace holds X --> (0. Y) = 0. (R_NormSpace_of_ContinuousFunctions (X,Y))
let Y be RealNormSpace; :: thesis: X --> (0. Y) = 0. (R_NormSpace_of_ContinuousFunctions (X,Y))
X --> (0. Y) = 0. (R_VectorSpace_of_ContinuousFunctions (X,Y)) by Th12
.= 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) ;
hence X --> (0. Y) = 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) ; :: thesis: verum