let CNS1, CNS2 be ComplexNormSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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

proof

thus Y c= dom (f | Y) by A5; :: according to NCFCONT1:def 11 :: thesis: for x0 being Point of CNS1 st x0 in Y holds
(f | Y) | Y is_continuous_in x0
let r be Point of CNS1; :: thesis: ( r in Y implies (f | Y) | Y is_continuous_in r )
assume r in Y ; :: thesis: (f | Y) | Y is_continuous_in r
then f | Y is_continuous_in r by A4;
hence (f | Y) | Y is_continuous_in r by RELAT_1:72; :: thesis: verum

end;

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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( ||.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; :: thesis: verum