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 Z: X c= dom f ; :: thesis: ( not f | X is uniformly_continuous or (- f) | X is uniformly_continuous )
assume A1: f | X is uniformly_continuous ; :: thesis: (- f) | X is uniformly_continuous
- f = (- 1) (#) f ;
hence (- f) | X is uniformly_continuous by A1, Th5, Z; :: thesis: verum