theorem Th34: :: NFCONT_1:34

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