let CNS1, CNS2 be ComplexNormSpace; :: thesis: for X, X1 being set
for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds
f1 + f2 is_Lipschitzian_on X /\ X1
let X, X1 be set ; :: thesis: for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds
f1 + f2 is_Lipschitzian_on X /\ X1
let f1, f2 be PartFunc of CNS1,CNS2; :: thesis: ( f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 implies f1 + f2 is_Lipschitzian_on X /\ X1 )
assume A1: ( f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 ) ; :: thesis: f1 + f2 is_Lipschitzian_on X /\ X1
then A2: f1 is_Lipschitzian_on X /\ X1 by Th118, XBOOLE_1:17;
then A3: X /\ X1 c= dom f1 by Def27;
A4: f2 is_Lipschitzian_on X /\ X1 by A1, Th118, XBOOLE_1:17;
then X /\ X1 c= dom f2 by Def27;
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 1; :: according to NCFCONT1:def 27 :: thesis: ex r being Real st
( 0 < r & ( for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= r * ||.(x1 - x2).|| ) )
consider s being Real such that
A6: ( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 holds
||.((f1 /. x1) - (f1 /. x2)).|| <= s * ||.(x1 - x2).|| ) ) by A2, Def27;
consider g being Real such that
A7: ( 0 < g & ( for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 holds
||.((f2 /. x1) - (f2 /. x2)).|| <= g * ||.(x1 - x2).|| ) ) by A4, Def27;
take p = s + g; :: thesis: ( 0 < p & ( for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= p * ||.(x1 - x2).|| ) )
0 + 0 < s + g by A6, A7, XREAL_1:10;
hence 0 < p ; :: thesis: for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= p * ||.(x1 - x2).||
let x1, x2 be Point of CNS1; :: thesis: ( x1 in X /\ X1 & x2 in X /\ X1 implies ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= p * ||.(x1 - x2).|| )
assume A8: ( x1 in X /\ X1 & x2 in X /\ X1 ) ; :: thesis: ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= p * ||.(x1 - x2).||
then ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| = ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 + f2) /. x2)).|| by A5, VFUNCT_2:def 1
.= ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 /. x2) + (f2 /. x2))).|| by A5, A8, VFUNCT_2:def 1
.= ||.((f1 /. x1) + ((f2 /. x1) - ((f1 /. x2) + (f2 /. x2)))).|| by RLVECT_1:42
.= ||.((f1 /. x1) + (((f2 /. x1) - (f1 /. x2)) - (f2 /. x2))).|| by RLVECT_1:41
.= ||.((f1 /. x1) + (((- (f1 /. x2)) + (f2 /. x1)) - (f2 /. x2))).|| by RLVECT_1:def 12
.= ||.((f1 /. x1) + ((- (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:42
.= ||.(((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 12 ;
then A9: ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| by CLVECT_1:def 11;
A10: ||.((f1 /. x1) - (f1 /. x2)).|| <= s * ||.(x1 - x2).|| by A6, A8;
||.((f2 /. x1) - (f2 /. x2)).|| <= g * ||.(x1 - x2).|| by A7, A8;
then ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| <= (s * ||.(x1 - x2).||) + (g * ||.(x1 - x2).||) by A10, XREAL_1:9;
hence ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= p * ||.(x1 - x2).|| by A9, XXREAL_0:2; :: thesis: verum