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 & [.a,b.] c= the carrier of Y & 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 & [.a,b.] c= the carrier of Y & 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: [.a,b.] c= the carrier of Y and
A4: f .: [.a,b.] c= [.a,b.] ; :: thesis: ex x being Point of X st f . x = x
reconsider A = [.a,b.] as non empty Subset of X by A1, A2, XXREAL_1:1;
A5: dom (f | A) = (dom f) /\ A by RELAT_1:61;
( A = the carrier of X /\ A & dom f = the carrier of X ) by FUNCT_2:def 1, XBOOLE_1:28;
then A6: dom (f | A) = the carrier of (Closed-Interval-TSpace (a,b)) by A1, A5, TOPMETR:18;
A7: A = the carrier of (Closed-Interval-TSpace (a,b)) by A1, TOPMETR:18;
then reconsider Z = Closed-Interval-TSpace (a,b) as SubSpace of X by TSEP_1:4;
rng (f | A) c= the carrier of (Closed-Interval-TSpace (a,b)) by A4, A7, RELAT_1:115;
then reconsider g = f | A as Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)) by A6, FUNCT_2:def 1, RELSET_1:4;
A8: Z is SubSpace of Y by A3, A7, TSEP_1:4;
for s being Point of (Closed-Interval-TSpace (a,b)) holds g is_continuous_at s

proof

let s be Point of (Closed-Interval-TSpace (a,b)); :: thesis: g is_continuous_at s
reconsider w = s as Point of X by A7, TARSKI:def 3;
for G being Subset of (Closed-Interval-TSpace (a,b)) st G is open & g . s in G holds
ex H being Subset of Z st
( H is open & s in H & g .: H c= G )

proof

let G be Subset of (Closed-Interval-TSpace (a,b)); :: thesis: ( G is open & g . s in G implies ex H being Subset of Z st
( H is open & s in H & g .: H c= G ) )
A9: f is_continuous_at w by TMAP_1:44;
assume G is open ; :: thesis: ( not g . s in G or ex H being Subset of Z st
( H is open & s in H & g .: H c= G ) )
then consider G0 being Subset of Y such that
A10: G0 is open and
A11: G0 /\ ([#] (Closed-Interval-TSpace (a,b))) = G by A8, TOPS_2:24;
assume g . s in G ; :: thesis: ex H being Subset of Z st
( H is open & s in H & g .: H c= G )
then f . w in G by A7, FUNCT_1:49;
then f . w in G0 by A11, XBOOLE_0:def 4;
then consider H0 being Subset of X such that
A12: H0 is open and
A13: w in H0 and
A14: f .: H0 c= G0 by A10, A9, TMAP_1:43;

now :: thesis: ex H being Subset of Z st
( H is open & s in H & g .: H c= G )

reconsider H = H0 /\ ([#] (Closed-Interval-TSpace (a,b))) as Subset of Z ;
take H = H; :: thesis: ( H is open & s in H & g .: H c= G )
thus H is open by A12, TOPS_2:24; :: thesis: ( s in H & g .: H c= G )
thus s in H by A13, XBOOLE_0:def 4; :: thesis: g .: H c= G
thus g .: H c= G :: thesis: verum

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in g .: H or t in G )
assume t in g .: H ; :: thesis: t in G
then consider r being object such that
r in dom g and
A15: r in H and
A16: t = g . r by FUNCT_1:def 6;
A17: r in the carrier of Z by A15;
reconsider r = r as Point of (Closed-Interval-TSpace (a,b)) by A15;
r in dom g by A17, FUNCT_2:def 1;
then A18: t in g .: the carrier of Z by A16, FUNCT_1:def 6;
reconsider p = r as Point of X by A7, TARSKI:def 3;
p in [#] X ;
then A19: p in dom f by FUNCT_2:def 1;
( t = f . p & p in H0 ) by A7, A15, A16, FUNCT_1:49, XBOOLE_0:def 4;
then t in f .: H0 by A19, FUNCT_1:def 6;
hence t in G by A11, A14, A18, XBOOLE_0:def 4; :: thesis: verum

end;

end;

hence ex H being Subset of Z st
( H is open & s in H & g .: H c= G ) ; :: thesis: verum

end;

hence g is_continuous_at s by TMAP_1:43; :: thesis: verum

end;

then reconsider h = g as continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)) by TMAP_1:44;

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

consider y being Point of (Closed-Interval-TSpace (a,b)) such that
A20: h . y = y by A1, Th22;
reconsider x = y as Point of X by A7, TARSKI:def 3;
take x = x; :: thesis: f . x = x
thus f . x = x by A7, A20, FUNCT_1:49; :: thesis: verum

end;

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