theorem Th27: :: ORDEQ_01:27

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