theorem :: NCFCONT1:94

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