for X being RealNormSpace
for f being PartFunc of REAL, the carrier of X
for Z being Subset of REAL st Z c= dom f & Z is compact & f | Z is continuous holds
f | Z is uniformly_continuous