let CNS1, CNS2 be ComplexNormSpace; for f being PartFunc of CNS1,CNS2
for Y being Subset of CNS1 st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y holds
ex x1, x2 being Point of CNS1 st
( x1 in Y & x2 in Y & ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) )
let f be PartFunc of CNS1,CNS2; for Y being Subset of CNS1 st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y holds
ex x1, x2 being Point of CNS1 st
( x1 in Y & x2 in Y & ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) )
let Y be Subset of CNS1; ( Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y implies ex x1, x2 being Point of CNS1 st
( x1 in Y & x2 in Y & ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) ) )
assume that
A1:
Y <> {}
and
A2:
Y c= dom f
and
A3:
Y is compact
and
A4:
f is_continuous_on Y
; ex x1, x2 being Point of CNS1 st
( x1 in Y & x2 in Y & ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) )
A5: dom (f | Y) =
(dom f) /\ Y
by RELAT_1:61
.=
Y
by A2, XBOOLE_1:28
;
f | Y is_continuous_on Y
then consider x1, x2 being Point of CNS1 such that
A6:
x1 in dom (f | Y)
and
A7:
x2 in dom (f | Y)
and
A8:
( ||.(f | Y).|| /. x1 = upper_bound (rng ||.(f | Y).||) & ||.(f | Y).|| /. x2 = lower_bound (rng ||.(f | Y).||) )
by A1, A3, A5, Th87;
A9:
dom f = dom ||.f.||
by NORMSP_0:def 3;
take
x1
; ex x2 being Point of CNS1 st
( x1 in Y & x2 in Y & ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) )
take
x2
; ( x1 in Y & x2 in Y & ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) )
thus
( x1 in Y & x2 in Y )
by A5, A6, A7; ( ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) )
A10: ||.f.|| .: Y =
rng (||.f.|| | Y)
by RELAT_1:115
.=
rng ||.(f | Y).||
by Th90
;
A11:
x2 in dom ||.(f | Y).||
by A7, NORMSP_0:def 3;
then A12: ||.(f | Y).|| /. x2 =
||.(f | Y).|| . x2
by PARTFUN1:def 6
.=
||.((f | Y) /. x2).||
by A11, NORMSP_0:def 3
.=
||.(f /. x2).||
by A7, PARTFUN2:15
.=
||.f.|| . x2
by A2, A5, A7, A9, NORMSP_0:def 3
.=
||.f.|| /. x2
by A2, A5, A7, A9, PARTFUN1:def 6
;
A13:
x1 in dom ||.(f | Y).||
by A6, NORMSP_0:def 3;
then ||.(f | Y).|| /. x1 =
||.(f | Y).|| . x1
by PARTFUN1:def 6
.=
||.((f | Y) /. x1).||
by A13, NORMSP_0:def 3
.=
||.(f /. x1).||
by A6, PARTFUN2:15
.=
||.f.|| . x1
by A2, A5, A6, A9, NORMSP_0:def 3
.=
||.f.|| /. x1
by A2, A5, A6, A9, PARTFUN1:def 6
;
hence
( ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) )
by A8, A12, A10; verum