theorem Th17: :: ORDEQ_01:17
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for g being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f = g holds
||.f.|| = ||.g.|| by FUNCT_1:49;