theorem Th25: :: ORDEQ_01:25

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