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: A = the carrier of (Closed-Interval-TSpace a,b) by A1, TOPMETR:25;
A6: dom (f | A) = the carrier of (Closed-Interval-TSpace a,b)

proof

A7: A = the carrier of X /\ A by XBOOLE_1:28;
( dom f = the carrier of X & dom (f | A) = (dom f) /\ A ) by FUNCT_2:def 1, RELAT_1:90;
hence dom (f | A) = the carrier of (Closed-Interval-TSpace a,b) by A1, A7, TOPMETR:25; :: thesis: verum

end;

rng (f | A) c= the carrier of (Closed-Interval-TSpace a,b) by A4, A5, RELAT_1:148;
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:11;
reconsider Z = Closed-Interval-TSpace a,b as SubSpace of X by A5, TSEP_1:4;
A8: Z is SubSpace of Y by A3, A5, 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 A5, 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 ) )
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
A9: G0 is open and
A10: G0 /\ ([#] (Closed-Interval-TSpace a,b)) = G by A8, TOPS_2:32;
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 A5, FUNCT_1:72;
then ( f . w in G0 & f is_continuous_at w ) by A10, TMAP_1:49, XBOOLE_0:def 4;
then consider H0 being Subset of X such that
A11: H0 is open and
A12: w in H0 and
A13: f .: H0 c= G0 by A9, TMAP_1:48;

now

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 A11, TOPS_2:32; :: thesis: ( s in H & g .: H c= G )
thus s in H by A12, XBOOLE_0:def 4; :: thesis: g .: H c= G
thus g .: H c= G :: thesis: verum

proof

let t be set ; :: 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 set such that
r in dom g and
A14: r in H and
A15: t = g . r by FUNCT_1:def 12;
A16: r in the carrier of Z by A14;
reconsider r = r as Point of (Closed-Interval-TSpace a,b) by A14;
reconsider p = r as Point of X by A5, TARSKI:def 3;
p in [#] X ;
then ( t = f . p & p in H0 & p in dom f ) by A5, A14, A15, FUNCT_1:72, FUNCT_2:def 1, XBOOLE_0:def 4;
then A17: t in f .: H0 by FUNCT_1:def 12;
r in dom g by A16, FUNCT_2:def 1;
then t in g .: the carrier of Z by A15, FUNCT_1:def 12;
hence t in G by A10, A13, A17, 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:48; :: thesis: verum

end;

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

now

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

end;

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