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