theorem Th26: :: ORDEQ_01:26

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
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 holds
for t being Real st t in X holds
||.((g1 /. t) - (g2 /. t)).|| <= ||.(v1 - v2).||