let X, X1 be set ; :: thesis: for S, T being RealNormSpace
for f1, f2 being PartFunc of S,T st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
let S, T be RealNormSpace; :: thesis: for f1, f2 being PartFunc of S,T st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
let f1, f2 be PartFunc of S,T; :: thesis: ( f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 implies f1 - f2 is_uniformly_continuous_on X /\ X1 )
assume that
A1: f1 is_uniformly_continuous_on X and
A2: f2 is_uniformly_continuous_on X1 ; :: thesis: f1 - f2 is_uniformly_continuous_on X /\ X1
A3: f2 is_uniformly_continuous_on X /\ X1 by A2, Th1, XBOOLE_1:17;
then A4: X /\ X1 c= dom f2 ;
A5: f1 is_uniformly_continuous_on X /\ X1 by A1, Th1, XBOOLE_1:17;
then X /\ X1 c= dom f1 ;
then X /\ X1 c= (dom f1) /\ (dom f2) by A4, XBOOLE_1:19;
hence A6: X /\ X1 c= dom (f1 - f2) by VFUNCT_1:def 2; :: according to NFCONT_2:def 1 :: thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) )
let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) )
then A7: 0 < r / 2 by XREAL_1:215;
then consider s being Real such that
A8: 0 < s and
A9: for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A5;
consider g being Real such that
A10: 0 < g and
A11: for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < g holds
||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A3, A7;
take p = min (s,g); :: thesis: ( 0 < p & ( for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) )
thus 0 < p by A8, A10, XXREAL_0:15; :: thesis: for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r
let x1, x2 be Point of S; :: thesis: ( x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p implies ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r )
assume that
A12: x1 in X /\ X1 and
A13: x2 in X /\ X1 and
A14: ||.(x1 - x2).|| < p ; :: thesis: ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r
p <= g by XXREAL_0:17;
then ||.(x1 - x2).|| < g by A14, XXREAL_0:2;
then A15: ||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A11, A12, A13;
p <= s by XXREAL_0:17;
then ||.(x1 - x2).|| < s by A14, XXREAL_0:2;
then ||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A9, A12, A13;
then A16: ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| < (r / 2) + (r / 2) by A15, XREAL_1:8;
A17: ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| by NORMSP_1:3;
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| = ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 - f2) /. x2)).|| by A6, A12, VFUNCT_1:def 2
.= ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 /. x2) - (f2 /. x2))).|| by A6, A13, VFUNCT_1:def 2
.= ||.((f1 /. x1) - ((f2 /. x1) + ((f1 /. x2) - (f2 /. x2)))).|| by RLVECT_1:27
.= ||.((f1 /. x1) - (((f1 /. x2) + (f2 /. x1)) - (f2 /. x2))).|| by RLVECT_1:def 3
.= ||.((f1 /. x1) - ((f1 /. x2) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:def 3
.= ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:27 ;
hence ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r by A16, A17, XXREAL_0:2; :: thesis: verum