let X, X1 be set ; :: thesis: for S being RealNormSpace

for f1, f2 being PartFunc of REAL, the carrier of S st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds

(f1 - f2) | (X /\ X1) is Lipschitzian

let S be RealNormSpace; :: thesis: for f1, f2 being PartFunc of REAL, the carrier of S st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds

(f1 - f2) | (X /\ X1) is Lipschitzian

let f1, f2 be PartFunc of REAL, the carrier of S; :: 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 VFUNCT_1:30;

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

for f1, f2 being PartFunc of REAL, the carrier of S st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds

(f1 - f2) | (X /\ X1) is Lipschitzian

let S be RealNormSpace; :: thesis: for f1, f2 being PartFunc of REAL, the carrier of S st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds

(f1 - f2) | (X /\ X1) is Lipschitzian

let f1, f2 be PartFunc of REAL, the carrier of S; :: 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 VFUNCT_1:30;

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