let CNS be ComplexNormSpace; :: thesis: for f being PartFunc of the carrier of CNS,REAL 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) )
let f be PartFunc of the carrier of CNS,REAL ; :: thesis: ( dom f <> {} & dom f is compact & f is_continuous_on dom f implies 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) ) )
assume that
A1: dom f <> {} and
A2: dom f is compact and
A3: f is_continuous_on dom f ; :: thesis: 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) )
A4: rng f <> {} by A1, RELAT_1:65;
rng f is compact by A2, A3, Th102;
then A5: ( upper_bound (rng f) in rng f & lower_bound (rng f) in rng f ) by A4, RCOMP_1:32;
then consider x being Element of CNS such that
A6: ( x in dom f & upper_bound (rng f) = f . x ) by PARTFUN1:26;
consider y being Element of CNS such that
A7: ( y in dom f & lower_bound (rng f) = f . y ) by A5, PARTFUN1:26;
take x ; :: thesis: ex x2 being Point of CNS st
( x in dom f & x2 in dom f & f /. x = upper_bound (rng f) & f /. x2 = lower_bound (rng f) )
take y ; :: thesis: ( x in dom f & y in dom f & f /. x = upper_bound (rng f) & f /. y = lower_bound (rng f) )
thus ( x in dom f & y in dom f & f /. x = upper_bound (rng f) & f /. y = lower_bound (rng f) ) by A6, A7, PARTFUN1:def 8; :: thesis: verum