theorem Th88: :: NCFCONT1:88

for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS st dom f <> {} & dom f is compact & f is_continuous_on dom f holds
ex x1, x2 being Point of CNS st
( x1 in dom f & x2 in dom f & ||.f.|| /. x1 = upper_bound (rng ||.f.||) & ||.f.|| /. x2 = lower_bound (rng ||.f.||) )