let X be set ; :: thesis: for f being PartFunc of REAL,REAL st f | X is Lipschitzian holds

( - (f | X) is Lipschitzian & (abs f) | X is Lipschitzian )

let f be PartFunc of REAL,REAL; :: thesis: ( f | X is Lipschitzian implies ( - (f | X) is Lipschitzian & (abs f) | X is Lipschitzian ) )

assume A1: f | X is Lipschitzian ; :: thesis: ( - (f | X) is Lipschitzian & (abs f) | X is Lipschitzian )

hence - (f | X) is Lipschitzian ; :: thesis: (abs f) | X is Lipschitzian

(abs f) | X = abs (f | X) by RFUNCT_1:46;

hence (abs f) | X is Lipschitzian by A1; :: thesis: verum

( - (f | X) is Lipschitzian & (abs f) | X is Lipschitzian )

let f be PartFunc of REAL,REAL; :: thesis: ( f | X is Lipschitzian implies ( - (f | X) is Lipschitzian & (abs f) | X is Lipschitzian ) )

assume A1: f | X is Lipschitzian ; :: thesis: ( - (f | X) is Lipschitzian & (abs f) | X is Lipschitzian )

hence - (f | X) is Lipschitzian ; :: thesis: (abs f) | X is Lipschitzian

(abs f) | X = abs (f | X) by RFUNCT_1:46;

hence (abs f) | X is Lipschitzian by A1; :: thesis: verum