let n be Element of NAT ; :: thesis: for g being Function of I[01] ,(TOP-REAL n)
for a being Real st g is continuous & |.(pi g,0 ).| <= a & a <= |.(pi g,1).| holds
ex s being Point of I[01] st |.(pi g,s).| = a
let g be Function of I[01] ,(TOP-REAL n); :: thesis: for a being Real st g is continuous & |.(pi g,0 ).| <= a & a <= |.(pi g,1).| holds
ex s being Point of I[01] st |.(pi g,s).| = a
let a be Real; :: thesis: ( g is continuous & |.(pi g,0 ).| <= a & a <= |.(pi g,1).| implies ex s being Point of I[01] st |.(pi g,s).| = a )
assume A1:
( g is continuous & |.(pi g,0 ).| <= a & a <= |.(pi g,1).| )
; :: thesis: ex s being Point of I[01] st |.(pi g,s).| = a
then consider f being Function of I[01] ,R^1 such that
A2:
( ( for t being Point of I[01] holds f . t = |.(g . t).| ) & f is continuous )
by Th93;
A3:
0 in [.0 ,1.]
by XXREAL_1:1;
reconsider o = 0 as Point of I[01] by BORSUK_1:83, XXREAL_1:1;
A4: f . 0 =
|.(g . o).|
by A2
.=
|.(pi g,0 ).|
by Def10
;
A5:
1 in the carrier of I[01]
by BORSUK_1:83, XXREAL_1:1;
reconsider I = 1 as Point of I[01] by BORSUK_1:83, XXREAL_1:1;
A6: f . 1 =
|.(g . I).|
by A2
.=
|.(pi g,1).|
by Def10
;
set c = |.(pi g,0 ).|;
set b = |.(pi g,1).|;
per cases
( ( |.(pi g,0 ).| < a & a < |.(pi g,1).| ) or |.(pi g,0 ).| = a or a = |.(pi g,1).| )
by A1, XXREAL_0:1;
suppose
(
|.(pi g,0 ).| < a &
a < |.(pi g,1).| )
;
:: thesis: ex s being Point of I[01] st |.(pi g,s).| = athen consider rc being
Real such that A7:
(
f . rc = a &
0 < rc &
rc < 1 )
by A2, A4, A6, TOPMETR:27, TOPREAL5:12;
A8:
rc in the
carrier of
I[01]
by A7, BORSUK_1:83, XXREAL_1:1;
reconsider rc1 =
rc as
Point of
I[01] by A7, BORSUK_1:83, XXREAL_1:1;
|.(pi g,rc).| =
|.(g . rc1).|
by Def10
.=
a
by A2, A7
;
hence
ex
s being
Point of
I[01] st
|.(pi g,s).| = a
by A8;
:: thesis: verum end;