let X, X1 be set ; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 + f2) | (X /\ X1) is Lipschitzian
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian implies (f1 + f2) | (X /\ X1) is Lipschitzian )
A1: ( f1 | (X /\ X1) = (f1 | X) | (X /\ X1) & f2 | (X /\ X1) = (f2 | X1) | (X /\ X1) ) by RELAT_1:74, XBOOLE_1:17;
A2: (f1 + f2) | (X /\ X1) = (f1 | (X /\ X1)) + (f2 | (X /\ X1)) by RFUNCT_1:44;
assume ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian ) ; :: thesis: (f1 + f2) | (X /\ X1) is Lipschitzian
hence (f1 + f2) | (X /\ X1) is Lipschitzian by A1, A2; :: thesis: verum