theorem Th89: :: NCFCONT1:89

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