let X be non empty closed_interval Subset of REAL; :: thesis: 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).||
let Y be RealNormSpace; :: thesis: 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).||
let v1, v2 be Point of (R_NormSpace_of_ContinuousFunctions (X,Y)); :: thesis: 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).||
let g1, g2 be PartFunc of REAL,Y; :: thesis: ( g1 = v1 & g2 = v2 implies for t being Real st t in X holds
||.((g1 /. t) - (g2 /. t)).|| <= ||.(v1 - v2).|| )
assume A1: ( g1 = v1 & g2 = v2 ) ; :: thesis: for t being Real st t in X holds
||.((g1 /. t) - (g2 /. t)).|| <= ||.(v1 - v2).||
consider f1 being continuous PartFunc of REAL,Y such that
A2: ( v1 = f1 & dom f1 = X ) by Def2;
consider f2 being continuous PartFunc of REAL,Y such that
A3: ( v2 = f2 & dom f2 = X ) by Def2;
consider f12 being continuous PartFunc of REAL,Y such that
A4: ( v1 - v2 = f12 & dom f12 = X ) by Def2;
let t be Real; :: thesis: ( t in X implies ||.((g1 /. t) - (g2 /. t)).|| <= ||.(v1 - v2).|| )
assume t in X ; :: thesis: ||.((g1 /. t) - (g2 /. t)).|| <= ||.(v1 - v2).||
then reconsider t1 = t as Element of X ;
f12 /. t1 = (f1 /. t1) - (f2 /. t1) by A2, A3, A4, Th20;
hence ||.((g1 /. t) - (g2 /. t)).|| <= ||.(v1 - v2).|| by A1, A2, A3, A4, Th24; :: thesis: verum