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 Th20;
A2:
L c= f .: K
proof
let x be
object ;
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:22;
then
z is
Tuple of 2,
REAL
by FINSEQ_2:131;
then consider x1,
y1 being
Element of
REAL such that A5:
z = <*x1,y1*>
by FINSEQ_2:100;
z `1 = x1
by A5, EUCLID:52;
then A6:
y1 <= (2 * x1) - 1
by A4, A5, EUCLID:52;
set Y =
[x1,y1];
A7:
[x1,y1] in [: the carrier of R^1, the carrier of R^1:]
by TOPMETR:17, ZFMISC_1:87;
then A8:
[x1,y1] in the
carrier of
[:R^1,R^1:]
by BORSUK_1:def 2;
reconsider Y =
[x1,y1] as
Point of
[:R^1,R^1:] by A7, BORSUK_1:def 2;
A9:
Y in dom f
by A8, FUNCT_2:def 1;
(
Y `1 = x1 &
Y `2 = y1 )
;
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 6;
verum
end;
A11:
f is being_homeomorphism
by A1, TOPREAL6:76;
f .: K c= L
proof
let x be
object ;
TARSKI:def 3 ( not x in f .: K or x in L )
assume
x in f .: K
;
x in L
then consider y being
object such that
y in dom f
and A12:
y in K
and A13:
x = f . y
by FUNCT_1:def 6;
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 2;
then consider x1,
y1 being
object 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;
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;
(
x9 `1 = x1 &
x9 `2 = y1 )
by A18, FINSEQ_1:44;
hence
x in L
by A15, A19;
verum
end;
then
f .: K = L
by A2;
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, Th15, TOPS_2:58; verum