for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for v being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for g being PartFunc of REAL,Y st g = v holds
for t being Real st t in X holds
||.(g /. t).|| <= ||.v.||