let X be non empty closed_interval Subset of REAL; :: thesis: 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
let Y be RealNormSpace; :: thesis: 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
let K be Real; :: 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 & ( for t being Real st t in X holds
||.((g1 /. t) - (g2 /. t)).|| <= K ) holds
||.(v1 - v2).|| <= K
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 & ( for t being Real st t in X holds
||.((g1 /. t) - (g2 /. t)).|| <= K ) holds
||.(v1 - v2).|| <= K
let g1, g2 be PartFunc of REAL,Y; :: thesis: ( g1 = v1 & g2 = v2 & ( for t being Real st t in X holds
||.((g1 /. t) - (g2 /. t)).|| <= K ) implies ||.(v1 - v2).|| <= K )
assume A1: ( g1 = v1 & g2 = v2 & ( for t being Real st t in X holds
||.((g1 /. t) - (g2 /. t)).|| <= K ) ) ; :: thesis: ||.(v1 - v2).|| <= K
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;
for t being Real st t in X holds
||.(f12 /. t).|| <= K

proof

let t be Real; :: thesis: ( t in X implies ||.(f12 /. t).|| <= K )
assume t in X ; :: thesis: ||.(f12 /. t).|| <= K
then reconsider t1 = t as Element of X ;
f12 /. t1 = (g1 /. t) - (g2 /. t) by A1, A2, A3, A4, Th20;
hence ||.(f12 /. t).|| <= K by A1; :: thesis: verum

end;

hence ||.(v1 - v2).|| <= K by Th25, A4; :: thesis: verum