let n be Element of NAT ; :: thesis: for X being set
for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian holds
( - (f | X) is Lipschitzian & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian )
let X be set ; :: thesis: for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian holds
( - (f | X) is Lipschitzian & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian )
let f be PartFunc of REAL,(REAL n); :: 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 )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
g | X is Lipschitzian by A1;
then A2: ( - (g | X) is Lipschitzian & ||.g.|| | X is Lipschitzian & (- g) | X is Lipschitzian ) by NFCONT_3:31;
- (g | X) = - (f | X) by Th8;
hence - (f | X) is Lipschitzian by A2; :: thesis: ( |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian )
thus |.f.| | X is Lipschitzian by A2, Th9; :: thesis: (- f) | X is Lipschitzian
- g = - f by Th8;
hence (- f) | X is Lipschitzian by A2; :: thesis: verum