let n be Element of NAT ; :: thesis: for X, X1 being set
for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 + f2) | (X /\ X1) is Lipschitzian
let X, X1 be set ; :: thesis: for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 + f2) | (X /\ X1) is Lipschitzian
let f1, f2 be PartFunc of REAL,(REAL n); :: thesis: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian implies (f1 + f2) | (X /\ X1) is Lipschitzian )
assume A1: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian ) ; :: thesis: (f1 + f2) | (X /\ X1) is Lipschitzian
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
( g1 | X is Lipschitzian & g2 | X1 is Lipschitzian ) by A1;
then A2: (g1 + g2) | (X /\ X1) is Lipschitzian by NFCONT_3:28;
g1 + g2 = f1 + f2 by Th5;
hence (f1 + f2) | (X /\ X1) is Lipschitzian by A2; :: thesis: verum