let X, Y be non empty SubSpace of R^1 ; 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; ( 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.]
; 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));
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));
( 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
;
( 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
;
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 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;
( H is open & s in H & g .: H c= G )thus
H is
open
by A12, TOPS_2:24;
( s in H & g .: H c= G )thus
s in H
by A13, XBOOLE_0:def 4;
g .: H c= Gthus
g .: H c= G
verumproof
let t be
object ;
TARSKI:def 3 ( not t in g .: H or t in G )
assume
t in g .: H
;
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;
verum
end; end;
hence
ex
H being
Subset of
Z st
(
H is
open &
s in H &
g .: H c= G )
;
verum
end;
hence
g is_continuous_at s
by TMAP_1:43;
verum
end;
then reconsider h = g as continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)) by TMAP_1:44;
hence
ex x being Point of X st f . x = x
; verum