let a, b be real number ; :: 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

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 (#) );
set g = ((P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) * f) * (L[01] ((#) a,b),(a,b (#) ));
A3: id (Closed-Interval-TSpace a,b) = (L[01] ((#) a,b),(a,b (#) )) * (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) by A2, Th18;
A4: id (Closed-Interval-TSpace 0 ,1) = (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) * (L[01] ((#) a,b),(a,b (#) )) by A2, Th18;
A5: f = ((L[01] ((#) a,b),(a,b (#) )) * (P[01] a,b,((#) 0 ,1),(0 ,1 (#) ))) * f by A3, TMAP_1:93
.= (L[01] ((#) a,b),(a,b (#) )) * ((P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) * f) by RELAT_1:55
.= (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 A3, TMAP_1:93
.= (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:55
.= ((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:55 ;
A6: L[01] ((#) a,b),(a,b (#) ) is continuous Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace a,b) by A1, Th11;
P[01] a,b,((#) 0 ,1),(0 ,1 (#) ) is continuous Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace 0 ,1) by A2, Th15;
then (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) * f is continuous ;
then ((P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) * f) * (L[01] ((#) a,b),(a,b (#) )) is continuous by A6;
then consider y being Point of (Closed-Interval-TSpace 0 ,1) such that
A7: (((P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) * f) * (L[01] ((#) a,b),(a,b (#) ))) . y = y by Th24, TOPMETR:27;

now

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:21
.= (((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 A4, RELAT_1:55
.= ((L[01] ((#) a,b),(a,b (#) )) * (((P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) * f) * (L[01] ((#) a,b),(a,b (#) )))) . y by TMAP_1:93
.= x by A7, FUNCT_2:21 ; :: 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:25;

now

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