let S, T be 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.||) )
let f be PartFunc of S,T; ( dom f <> {} & dom f is compact & f is_continuous_on dom f implies 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.||) ) )
assume that
A1:
dom f <> {}
and
A2:
dom f is compact
and
A3:
f is_continuous_on dom f
; 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.||) )
A4:
dom f = dom ||.f.||
by NORMSP_0:def 3;
dom ||.f.|| is compact
by A2, NORMSP_0:def 3;
then A5:
rng ||.f.|| is compact
by A3, A4, Th28, Th31;
A6:
rng ||.f.|| <> {}
by A1, A4, RELAT_1:42;
then consider x being Element of S such that
A7:
( x in dom ||.f.|| & upper_bound (rng ||.f.||) = ||.f.|| . x )
by A5, PARTFUN1:3, RCOMP_1:14;
consider y being Element of S such that
A8:
( y in dom ||.f.|| & lower_bound (rng ||.f.||) = ||.f.|| . y )
by A6, A5, PARTFUN1:3, RCOMP_1:14;
take
x
; ex x2 being Point of S st
( x in dom f & x2 in dom f & ||.f.|| /. x = upper_bound (rng ||.f.||) & ||.f.|| /. x2 = lower_bound (rng ||.f.||) )
take
y
; ( 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 A7, A8, NORMSP_0:def 3, PARTFUN1:def 6; verum