let X, X1 be set ; :: thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f1, f2 being PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
let RNS be RealNormSpace; :: thesis: for CNS being ComplexNormSpace
for f1, f2 being PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
let CNS be ComplexNormSpace; :: thesis: for f1, f2 being PartFunc of RNS,CNS 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 RNS,CNS; :: thesis: ( f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 implies f1 - f2 is_uniformly_continuous_on X /\ X1 )
assume A1: ( f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 ) ; :: thesis: f1 - f2 is_uniformly_continuous_on X /\ X1
then A2: f1 is_uniformly_continuous_on X /\ X1 by Th3, XBOOLE_1:17;
then A3: X /\ X1 c= dom f1 by Def3;
A4: f2 is_uniformly_continuous_on X /\ X1 by A1, Th3, XBOOLE_1:17;
then X /\ X1 c= dom f2 by Def3;
then X /\ X1 c= (dom f1) /\ (dom f2) by A3, XBOOLE_1:19;
hence A5: X /\ X1 c= dom (f1 - f2) by VFUNCT_2:def 2; :: according to NCFCONT2:def 3 :: thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS 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 RNS 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 RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) )
then A6: 0 < r / 2 by XREAL_1:217;
then consider s being Real such that
A7: ( 0 < s & ( for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 ) ) by A2, Def3;
consider g being Real such that
A8: ( 0 < g & ( for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < g holds
||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 ) ) by A4, A6, Def3;
take p = min s,g; :: thesis: ( 0 < p & ( for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) )
thus 0 < p by A7, A8, XXREAL_0:15; :: thesis: for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r
A9: ( p <= s & p <= g ) by XXREAL_0:17;
let x1, x2 be Point of RNS; :: thesis: ( x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p implies ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r )
assume A10: ( x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p ) ; :: thesis: ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r
then ( x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s ) by A9, XXREAL_0:2;
then A11: ||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A7;
( x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < g ) by A9, A10, XXREAL_0:2;
then ||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A8;
then A12: ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| < (r / 2) + (r / 2) by A11, XREAL_1:10;
A13: ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| = ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 - f2) /. x2)).|| by A5, A10, VFUNCT_2:def 2
.= ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 /. x2) - (f2 /. x2))).|| by A5, A10, VFUNCT_2:def 2
.= ||.((f1 /. x1) - ((f2 /. x1) + ((f1 /. x2) - (f2 /. x2)))).|| by RLVECT_1:41
.= ||.((f1 /. x1) - (((f1 /. x2) + (f2 /. x1)) - (f2 /. x2))).|| by RLVECT_1:def 6
.= ||.((f1 /. x1) - ((f1 /. x2) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:def 6
.= ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:41 ;
||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| by CLVECT_1:105;
hence ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r by A12, A13, XXREAL_0:2; :: thesis: verum