let a, b be Real; :: thesis: ( a <= b implies for f being continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)) ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x )
assume A1: a <= b ; :: thesis: for f being continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)) ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x
let f be continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)); :: thesis: ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x

now :: thesis: ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x

per cases ( a < b or a = b ) by A1, XXREAL_0:1;

suppose A2: a < b ; :: thesis: ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x

set L = L[01] (((#) (a,b)),((a,b) (#)));
set P = P[01] (a,b,((#) (0,1)),((0,1) (#)));
A3: P[01] (a,b,((#) (0,1)),((0,1) (#))) is continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) by A2, Th12;
set g = ((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#))));
A4: id (Closed-Interval-TSpace (a,b)) = (L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) by A2, Th15;
then A5: f = ((L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))))) * f by FUNCT_2:17
.= (L[01] (((#) (a,b)),((a,b) (#)))) * ((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) by RELAT_1:36
.= (L[01] (((#) (a,b)),((a,b) (#)))) * (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * ((L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))))) by A4, FUNCT_2:17
.= (L[01] (((#) (a,b)),((a,b) (#)))) * ((((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#))))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))))) by RELAT_1:36
.= ((L[01] (((#) (a,b)),((a,b) (#)))) * (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#)))))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) by RELAT_1:36 ;
L[01] (((#) (a,b)),((a,b) (#))) is continuous Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) by A1, Th8;
then consider y being Point of (Closed-Interval-TSpace (0,1)) such that
A6: (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#))))) . y = y by A3, Th21, TOPMETR:20;
A7: id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#)))) by A2, Th15;

now :: thesis: ex x being Element of the carrier of (Closed-Interval-TSpace (a,b)) st f . x = x

take x = (L[01] (((#) (a,b)),((a,b) (#)))) . y; :: thesis: f . x = x
thus f . x = ((((L[01] (((#) (a,b)),((a,b) (#)))) * (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#)))))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))))) * (L[01] (((#) (a,b)),((a,b) (#))))) . y by A5, FUNCT_2:15
.= (((L[01] (((#) (a,b)),((a,b) (#)))) * (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#)))))) * (id (Closed-Interval-TSpace (0,1)))) . y by A7, RELAT_1:36
.= ((L[01] (((#) (a,b)),((a,b) (#)))) * (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#)))))) . y by FUNCT_2:17
.= x by A6, FUNCT_2:15 ; :: thesis: verum

end;

hence ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x ; :: thesis: verum

end;

suppose A8: a = b ; :: thesis: ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x

then ( [.a,b.] = {a} & a = (#) (a,b) ) by Def1, XXREAL_1:17;
then A9: the carrier of (Closed-Interval-TSpace (a,b)) = {((#) (a,b))} by A8, TOPMETR:18;

now :: thesis: ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x

take x = (#) (a,b); :: thesis: f . x = x
thus f . x = x by A9, TARSKI:def 1; :: thesis: verum

end;

hence ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x ; :: thesis: verum

end;

end;

end;

hence ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x ; :: thesis: verum