let X be set ; :: thesis: for S, T being RealNormSpace
for f being PartFunc of S,T st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
let f be PartFunc of S,T; :: thesis: ( f is_uniformly_continuous_on X implies - f is_uniformly_continuous_on X )
A1: - f = (- 1) (#) f by VFUNCT_1:23;
assume f is_uniformly_continuous_on X ; :: thesis: - f is_uniformly_continuous_on X
hence - f is_uniformly_continuous_on X by A1, Th4; :: thesis: verum