let X, X1 be set ; for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f1, f2 being PartFunc of CNS,RNS 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; for CNS being ComplexNormSpace
for f1, f2 being PartFunc of CNS,RNS 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; for f1, f2 being PartFunc of CNS,RNS 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 CNS,RNS; ( 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
; f1 + f2 is_uniformly_continuous_on X /\ X1
A3:
f2 is_uniformly_continuous_on X /\ X1
by A2, Th2, XBOOLE_1:17;
then A4:
X /\ X1 c= dom f2
;
A5:
f1 is_uniformly_continuous_on X /\ X1
by A1, Th2, 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 1; NCFCONT2:def 2 for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) )
let r be Real; ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) ) )
assume
0 < r
; ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS 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
;
then consider s being Real such that
A8:
0 < s
and
A9:
for x1, x2 being Point of CNS 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 CNS 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); ( 0 < p & ( for x1, x2 being Point of CNS 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; for x1, x2 being Point of CNS 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 CNS; ( 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
; ||.(((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:def 1;
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| =
||.(((f1 /. x1) + (f2 /. x1)) - ((f1 + f2) /. x2)).||
by A6, A12, VFUNCT_1:def 1
.=
||.(((f1 /. x1) + (f2 /. x1)) - ((f1 /. x2) + (f2 /. x2))).||
by A6, A13, VFUNCT_1:def 1
.=
||.((f1 /. x1) + ((f2 /. x1) - ((f1 /. x2) + (f2 /. x2)))).||
by RLVECT_1:def 3
.=
||.((f1 /. x1) + (((f2 /. x1) - (f1 /. x2)) - (f2 /. x2))).||
by RLVECT_1:27
.=
||.((f1 /. x1) + (((- (f1 /. x2)) + (f2 /. x1)) - (f2 /. x2))).||
.=
||.((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
;
hence
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r
by A16, A17, XXREAL_0:2; verum