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;
the carrier of Y c= the carrier of R^1 by BORSUK_1:1;
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:126;
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:55;
then A4: ((Y incl R^1) * f) .: [.a,b.] c= [.a,b.] by A3, FUNCT_1:92;
A5: ( Y incl R^1 is continuous Function of Y,R^1 & R^1 is SubSpace of R^1 ) by TMAP_1:87, TSEP_1:2;
the carrier of X c= the carrier of R^1 by BORSUK_1:1;
then A6: [.a,b.] c= the carrier of R^1 by A2;

now :: thesis: ex x being Point of X st f . x = x

consider x being Point of X such that
A7: ((Y incl R^1) * f) . x = x by A1, A2, A5, A6, A4, Th23;
the carrier of Y c= the carrier of R^1 by BORSUK_1:1;
then reconsider y = f . x as Point of R^1 ;
take x = x; :: thesis: f . x = x
thus f . x = (Y incl R^1) . y by TMAP_1:84
.= x by A7, FUNCT_2:15 ; :: thesis: verum

end;

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