let n be Nat; :: thesis: for g being Function of I[01],(TOP-REAL n)
for a being Real st g is continuous & |.(g /. 0).| <= a & a <= |.(g /. 1).| holds
ex s being Point of I[01] st |.(g /. s).| = a
reconsider I = 1 as Point of I[01] by BORSUK_1:40, XXREAL_1:1;
A1: 0 in [.0,1.] by XXREAL_1:1;
reconsider o = 0 as Point of I[01] by BORSUK_1:40, XXREAL_1:1;
let g be Function of I[01],(TOP-REAL n); :: thesis: for a being Real st g is continuous & |.(g /. 0).| <= a & a <= |.(g /. 1).| holds
ex s being Point of I[01] st |.(g /. s).| = a
let a be Real; :: thesis: ( g is continuous & |.(g /. 0).| <= a & a <= |.(g /. 1).| implies ex s being Point of I[01] st |.(g /. s).| = a )
assume that
A2: g is continuous and
A3: ( |.(g /. 0).| <= a & a <= |.(g /. 1).| ) ; :: thesis: ex s being Point of I[01] st |.(g /. s).| = a
consider f being Function of I[01],R^1 such that
A4: for t being Point of I[01] holds f . t = |.(g . t).| and
A5: f is continuous by A2, Th69;
A6: f . 0 = |.(g . o).| by A4
.= |.(g /. 0).| by FUNCT_2:def 13 ;
set c = |.(g /. 0).|;
set b = |.(g /. 1).|;
A7: 1 in the carrier of I[01] by BORSUK_1:40, XXREAL_1:1;
A8: f . 1 = |.(g . I).| by A4
.= |.(g /. 1).| by FUNCT_2:def 13 ;

per cases ( ( |.(g /. 0).| < a & a < |.(g /. 1).| ) or |.(g /. 0).| = a or a = |.(g /. 1).| ) by A3, XXREAL_0:1;

suppose ( |.(g /. 0).| < a & a < |.(g /. 1).| ) ; :: thesis: ex s being Point of I[01] st |.(g /. s).| = a

then consider rc being Real such that
A9: f . rc = a and
A10: ( 0 < rc & rc < 1 ) by A5, A6, A8, TOPMETR:20, TOPREAL5:6;
reconsider rc1 = rc as Point of I[01] by A10, BORSUK_1:40, XXREAL_1:1;
A11: rc in the carrier of I[01] by A10, BORSUK_1:40, XXREAL_1:1;
|.(g /. rc).| = |.(g . rc1).| by FUNCT_2:def 13
.= a by A4, A9 ;
hence ex s being Point of I[01] st |.(g /. s).| = a by A11; :: thesis: verum

end;

suppose |.(g /. 0).| = a ; :: thesis: ex s being Point of I[01] st |.(g /. s).| = a

hence ex s being Point of I[01] st |.(g /. s).| = a by A1, BORSUK_1:40; :: thesis: verum

end;

suppose a = |.(g /. 1).| ; :: thesis: ex s being Point of I[01] st |.(g /. s).| = a

hence ex s being Point of I[01] st |.(g /. s).| = a by A7; :: thesis: verum

end;

end;