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