let X be set ; :: thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
let RNS be RealNormSpace; :: thesis: for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
let CNS be ComplexNormSpace; :: thesis: for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
let f be PartFunc of RNS,CNS; :: thesis: ( f is_uniformly_continuous_on X implies - f is_uniformly_continuous_on X )
assume A1: f is_uniformly_continuous_on X ; :: thesis: - f is_uniformly_continuous_on X
- f = (- 1r ) (#) f by VFUNCT_2:23;
hence - f is_uniformly_continuous_on X by A1, Th12; :: thesis: verum