let f be Function of (TOP-REAL 1),R^1; ( ( for p being Element of (TOP-REAL 1) holds f . p = p /. 1 ) implies f is being_homeomorphism )
assume A1:
for p being Element of (TOP-REAL 1) holds f . p = p /. 1
; f is being_homeomorphism
A2:
dom f = the carrier of (TOP-REAL 1)
by FUNCT_2:def 1;
REAL c= rng f
then A4:
( [#] (TOP-REAL 1) = the carrier of (TOP-REAL 1) & rng f = [#] R^1 )
by TOPMETR:17, XBOOLE_0:def 10;
A5:
TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1)
by EUCLID:def 8;
then reconsider ff = f /" as Function of R^1,(TopSpaceMetr (Euclid 1)) ;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
then A13:
f is one-to-one
by FUNCT_1:def 4;
A14:
f /" is continuous
proof
TopStruct(# the
carrier of
(TOP-REAL 1), the
topology of
(TOP-REAL 1) #)
= TopSpaceMetr (Euclid 1)
by EUCLID:def 8;
then reconsider g =
f /" as
Function of
R^1,
(TopSpaceMetr (Euclid 1)) ;
reconsider g1 =
g as
Function of the
carrier of
R^1, the
carrier of
(TOP-REAL 1) ;
the
carrier of
R^1 c= rng f
then A15:
rng f = the
carrier of
R^1
by XBOOLE_0:def 10;
for
r being
Real for
u being
Element of
(Euclid 1) for
P being
Subset of the
carrier of
(TopSpaceMetr (Euclid 1)) st
r > 0 &
P = Ball (
u,
r) holds
g " P is
open
proof
reconsider f1 =
f as
Function of the
carrier of
(TOP-REAL 1), the
carrier of
R^1 ;
let r be
Real;
for u being Element of (Euclid 1)
for P being Subset of the carrier of (TopSpaceMetr (Euclid 1)) st r > 0 & P = Ball (u,r) holds
g " P is open let u be
Element of
(Euclid 1);
for P being Subset of the carrier of (TopSpaceMetr (Euclid 1)) st r > 0 & P = Ball (u,r) holds
g " P is open let P be
Subset of the
carrier of
(TopSpaceMetr (Euclid 1));
( r > 0 & P = Ball (u,r) implies g " P is open )
assume that
r > 0
and A16:
P = Ball (
u,
r)
;
g " P is open
u is
Tuple of 1,
REAL
by FINSEQ_2:131;
then consider s1 being
Element of
REAL such that A17:
u = <*s1*>
by FINSEQ_2:97;
dom f1 = the
carrier of
(TOP-REAL 1)
by FUNCT_2:def 1;
then A18:
dom f1 = REAL 1
by EUCLID:22;
A19:
Ball (
u,
r)
= { <*s*> where s is Real : ( s1 - r < s & s < s1 + r ) }
by A17, Th27;
A20:
f1 .: (Ball (u,r)) = { w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r ) }
f1 is
onto
by A15, FUNCT_2:def 3;
then
g1 = f1 "
by A13, TOPS_2:def 4;
then
g1 " (Ball (u,r)) = { w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r ) }
by A13, A20, FUNCT_1:84;
hence
g " P is
open
by A16, Th26;
verum
end;
then
ff is
continuous
by Th16;
hence
f /" is
continuous
by A5, PRE_TOPC:33;
verum
end;
1 in Seg 1
by FINSEQ_1:1;
then
f is continuous
by A1, Th18;
hence
f is being_homeomorphism
by A2, A4, A13, A14, TOPS_2:def 5; verum