let X be set ; :: thesis: for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st f | X is Lipschitzian holds
( - (f | X) is Lipschitzian & (- f) | X is Lipschitzian & ||.f.|| | X is Lipschitzian )
let S be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of S st f | X is Lipschitzian holds
( - (f | X) is Lipschitzian & (- f) | X is Lipschitzian & ||.f.|| | X is Lipschitzian )
let f be PartFunc of REAL, the carrier of S; :: thesis: ( f | X is Lipschitzian implies ( - (f | X) is Lipschitzian & (- f) | X is Lipschitzian & ||.f.|| | X is Lipschitzian ) )
assume A1: f | X is Lipschitzian ; :: thesis: ( - (f | X) is Lipschitzian & (- f) | X is Lipschitzian & ||.f.|| | X is Lipschitzian )
A2: - (f | X) = (- 1) (#) (f | X) by VFUNCT_1:23;
hence - (f | X) is Lipschitzian by A1; :: thesis: ( (- f) | X is Lipschitzian & ||.f.|| | X is Lipschitzian )
thus (- f) | X is Lipschitzian by A1, A2, VFUNCT_1:29; :: thesis: ||.f.|| | X is Lipschitzian
||.f.|| | X = ||.(f | X).|| by VFUNCT_1:29;
hence ||.f.|| | X is Lipschitzian by A1; :: thesis: verum