let X be set ; :: thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is uniformly_continuous holds
(- f) | X is uniformly_continuous
let f be PartFunc of REAL,REAL; :: thesis: ( X c= dom f & f | X is uniformly_continuous implies (- f) | X is uniformly_continuous )
assume A1: X c= dom f ; :: thesis: ( not f | X is uniformly_continuous or (- f) | X is uniformly_continuous )
A2: - f = (- 1) (#) f ;
assume f | X is uniformly_continuous ; :: thesis: (- f) | X is uniformly_continuous
hence (- f) | X is uniformly_continuous by A1, A2, Th5; :: thesis: verum