set GG = [:R^1 ,R^1 :];
set SS = TOP-REAL 2;
defpred S1[ Point of [:R^1 ,R^1 :]] means $1 `2 <= (2 * ($1 `1 )) - 1;
defpred S2[ Point of (TOP-REAL 2)] means $1 `2 <= (2 * ($1 `1 )) - 1;
reconsider K = { p where p is Point of [:R^1 ,R^1 :] : S1[p] } as Subset of [:R^1 ,R^1 :] from DOMAIN_1:sch 7();
reconsider L = { p where p is Point of (TOP-REAL 2) : S2[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
consider f being Function of [:R^1 ,R^1 :],(TOP-REAL 2) such that
A1:
for x, y being Real holds f . [x,y] = <*x,y*>
by Th24;
A2:
L c= f .: K
proof
let x be
set ;
TARSKI:def 3 ( not x in L or x in f .: K )
assume
x in L
;
x in f .: K
then consider z being
Point of
(TOP-REAL 2) such that A3:
z = x
and A4:
S2[
z]
;
the
carrier of
(TOP-REAL 2) = REAL 2
by EUCLID:25;
then
z is
Tuple of 2,
REAL
by FINSEQ_2:151;
then consider x1,
y1 being
Real such that A5:
z = <*x1,y1*>
by FINSEQ_2:120;
z `1 = x1
by A5, EUCLID:56;
then A6:
y1 <= (2 * x1) - 1
by A4, A5, EUCLID:56;
set Y =
[x1,y1];
A7:
[x1,y1] in [:the carrier of R^1 ,the carrier of R^1 :]
by TOPMETR:24, ZFMISC_1:106;
then A8:
[x1,y1] in the
carrier of
[:R^1 ,R^1 :]
by BORSUK_1:def 5;
reconsider Y =
[x1,y1] as
Point of
[:R^1 ,R^1 :] by A7, BORSUK_1:def 5;
A9:
Y in dom f
by A8, FUNCT_2:def 1;
(
Y `1 = x1 &
Y `2 = y1 )
by MCART_1:7;
then A10:
Y in K
by A6;
x = f . Y
by A1, A3, A5;
hence
x in f .: K
by A10, A9, FUNCT_1:def 12;
verum
end;
A11:
f is being_homeomorphism
by A1, TOPREAL6:85;
f .: K c= L
proof
let x be
set ;
TARSKI:def 3 ( not x in f .: K or x in L )
assume
x in f .: K
;
x in L
then consider y being
set such that
y in dom f
and A12:
y in K
and A13:
x = f . y
by FUNCT_1:def 12;
consider z being
Point of
[:R^1 ,R^1 :] such that A14:
z = y
and A15:
S1[
z]
by A12;
z in the
carrier of
[:R^1 ,R^1 :]
;
then
z in [:the carrier of R^1 ,the carrier of R^1 :]
by BORSUK_1:def 5;
then consider x1,
y1 being
set such that A16:
(
x1 in the
carrier of
R^1 &
y1 in the
carrier of
R^1 )
and A17:
z = [x1,y1]
by ZFMISC_1:def 2;
reconsider x1 =
x1,
y1 =
y1 as
Real by A16, TOPMETR:24;
A18:
x = |[x1,y1]|
by A1, A13, A14, A17;
then reconsider x9 =
x as
Point of
(TOP-REAL 2) ;
A19:
(
z `1 = x1 &
z `2 = y1 )
by A17, MCART_1:7;
(
x9 `1 = x1 &
x9 `2 = y1 )
by A18, FINSEQ_1:61;
hence
x in L
by A15, A19;
verum
end;
then
f .: K = L
by A2, XBOOLE_0:def 10;
hence
{ p where p is Point of [:R^1 ,R^1 :] : p `2 <= (2 * (p `1 )) - 1 } is closed Subset of [:R^1 ,R^1 :]
by A11, Th19, TOPS_2:72; verum