let X, Y be non empty SubSpace of R^1 ; :: thesis: for f being continuous Function of X,Y st ex a, b being Real st
( a <= b & [.a,b.] c= the carrier of X & f .: [.a,b.] c= [.a,b.] ) holds
ex x being Point of X st f . x = x
let f be continuous Function of X,Y; :: thesis: ( ex a, b being Real st
( a <= b & [.a,b.] c= the carrier of X & f .: [.a,b.] c= [.a,b.] ) implies ex x being Point of X st f . x = x )
given a, b being Real such that A1: a <= b and
A2: [.a,b.] c= the carrier of X and
A3: f .: [.a,b.] c= [.a,b.] ; :: thesis: ex x being Point of X st f . x = x
set g = (Y incl R^1 ) * f;
Y incl R^1 is continuous Function of Y,R^1 by TMAP_1:98;
then A4: (Y incl R^1 ) * f is continuous ;
A5: R^1 is SubSpace of R^1 by TSEP_1:2;
the carrier of X c= the carrier of R^1 by BORSUK_1:35;
then A6: [.a,b.] c= the carrier of R^1 by A2, XBOOLE_1:1;
( f .: [.a,b.] c= the carrier of Y & the carrier of Y c= the carrier of R^1 ) by BORSUK_1:35;
then reconsider B = f .: [.a,b.] as Subset of R^1 by XBOOLE_1:1;
((Y incl R^1 ) * f) .: [.a,b.] = (Y incl R^1 ) .: (f .: [.a,b.]) by RELAT_1:159;
then ((Y incl R^1 ) * f) .: [.a,b.] = ((id R^1 ) | Y) .: B by TMAP_1:def 6;
then ((Y incl R^1 ) * f) .: [.a,b.] = (id R^1 ) .: B by TMAP_1:61;
then A7: ((Y incl R^1 ) * f) .: [.a,b.] c= [.a,b.] by A3, FUNCT_1:162;

now

consider x being Point of X such that
A8: ((Y incl R^1 ) * f) . x = x by A1, A2, A4, A5, A6, A7, Th26;
take x = x; :: thesis: f . x = x
the carrier of Y c= the carrier of R^1 by BORSUK_1:35;
then reconsider y = f . x as Point of R^1 by TARSKI:def 3;
thus f . x = (Y incl R^1 ) . y by TMAP_1:95
.= x by A8, FUNCT_2:21 ; :: thesis: verum

end;

hence ex x being Point of X st f . x = x ; :: thesis: verum