:: TOPREALA semantic presentation

begin

set R = the carrier of R^1;

Lm1:  the carrier of [:R^1,R^1:] = [: the carrier of R^1, the carrier of R^1:]
by BORSUK_1:def_2;


registration
let r be real number ;
let s be real positive number ;
clusterK148(r,(r + s)) ->  non empty ;
coherence
 not ].r,(r + s).[ is empty
proof
 r + 0 < r + s by XREAL_1:6;
then  ( r < (r + (r + s)) / 2 & (r + (r + s)) / 2 < r + s ) by XREAL_1:226;
hence  not ].r,(r + s).[ is empty by XXREAL_1:4; ::_thesis: verum
end;
clusterK146(r,(r + s)) ->  non empty ;
coherence
 not [.r,(r + s).[ is empty
proof
 r + 0 < r + s by XREAL_1:6;
hence  not [.r,(r + s).[ is empty by XXREAL_1:3; ::_thesis: verum
end;
clusterK147(r,(r + s)) ->  non empty ;
coherence
 not ].r,(r + s).] is empty
proof
 r + 0 < r + s by XREAL_1:6;
hence  not ].r,(r + s).] is empty by XXREAL_1:2; ::_thesis: verum
end;
clusterK145(r,(r + s)) ->  non empty ;
coherence
 not [.r,(r + s).] is empty
proof
 r + 0 < r + s by XREAL_1:6;
hence  not [.r,(r + s).] is empty by XXREAL_1:1; ::_thesis: verum
end;
clusterK148((r - s),r) ->  non empty ;
coherence
 not ].(r - s),r.[ is empty
proof
 r - s < r - 0 by XREAL_1:15;
then  ( r - s < ((r - s) + r) / 2 & ((r - s) + r) / 2 < r ) by XREAL_1:226;
hence  not ].(r - s),r.[ is empty by XXREAL_1:4; ::_thesis: verum
end;
clusterK146((r - s),r) ->  non empty ;
coherence
 not [.(r - s),r.[ is empty
proof
 r - s < r - 0 by XREAL_1:15;
hence  not [.(r - s),r.[ is empty by XXREAL_1:3; ::_thesis: verum
end;
clusterK147((r - s),r) ->  non empty ;
coherence
 not ].(r - s),r.] is empty
proof
 r - s < r - 0 by XREAL_1:15;
hence  not ].(r - s),r.] is empty by XXREAL_1:32; ::_thesis: verum
end;
clusterK145((r - s),r) ->  non empty ;
coherence
 not [.(r - s),r.] is empty
proof
 r - s < r - 0 by XREAL_1:15;
hence  not [.(r - s),r.] is empty by XXREAL_1:1; ::_thesis: verum
end;
end;

registration
let r be real non positive number ;
let s be real positive number ;
clusterK148(r,s) ->  non empty ;
coherence
 not ].r,s.[ is empty
proof
 ( r < (r + s) / 2 & (r + s) / 2 < s ) by XREAL_1:226;
hence  not ].r,s.[ is empty by XXREAL_1:4; ::_thesis: verum
end;
clusterK146(r,s) ->  non empty ;
coherence
 not [.r,s.[ is empty by XXREAL_1:3;
clusterK147(r,s) ->  non empty ;
coherence
 not ].r,s.] is empty by XXREAL_1:2;
clusterK145(r,s) ->  non empty ;
coherence
 not [.r,s.] is empty by XXREAL_1:1;
end;

registration
let r be real negative number ;
let s be real non negative number ;
clusterK148(r,s) ->  non empty ;
coherence
 not ].r,s.[ is empty
proof
 ( r < (r + s) / 2 & (r + s) / 2 < s ) by XREAL_1:226;
hence  not ].r,s.[ is empty by XXREAL_1:4; ::_thesis: verum
end;
clusterK146(r,s) ->  non empty ;
coherence
 not [.r,s.[ is empty by XXREAL_1:3;
clusterK147(r,s) ->  non empty ;
coherence
 not ].r,s.] is empty by XXREAL_1:2;
clusterK145(r,s) ->  non empty ;
coherence
 not [.r,s.] is empty by XXREAL_1:1;
end;

begin

theorem :: TOPREALA:1
for f being Function
for x, X being set st x in dom f & f . x in f .: X & f is one-to-one holds
x in X
proof
let f be Function; ::_thesis: for x, X being set st x in dom f & f . x in f .: X & f is one-to-one holds
x in X
let x, X be set ; ::_thesis: ( x in dom f & f . x in f .: X & f is one-to-one implies x in X )
assume A1: x in dom f ; ::_thesis: ( not f . x in f .: X or not f is one-to-one or x in X )
assume  f . x in f .: X ; ::_thesis: ( not f is one-to-one or x in X )
then A2: ex a being set st
( a in dom f & a in X & f . x = f . a ) by FUNCT_1:def_6;
assume  f is one-to-one ; ::_thesis: x in X
hence  x in X by A1, A2, FUNCT_1:def_4; ::_thesis: verum
end;

theorem :: TOPREALA:2
for f being FinSequence
for i being Nat holds
( not i + 1 in dom f or i in dom f or i = 0 )
proof
let f be FinSequence; ::_thesis: for i being Nat holds
( not i + 1 in dom f or i in dom f or i = 0 )
let i be Nat; ::_thesis: ( not i + 1 in dom f or i in dom f or i = 0 )
assume A1: i + 1 in dom f ; ::_thesis: ( i in dom f or i = 0 )
then  1 <= i + 1 by FINSEQ_3:25;
then A2: ( 1 < i + 1 or 1 + 0 = i + 1 ) by XXREAL_0:1;
percases ( i = 0 or 1 <= i ) by A2, NAT_1:13;
suppose i = 0 ; ::_thesis: ( i in dom f or i = 0 )
hence  ( i in dom f or i = 0 ) ; ::_thesis: verum
end;
supposeA3: 1 <= i ; ::_thesis: ( i in dom f or i = 0 )
 i + 1 <= len f by A1, FINSEQ_3:25;
then  i <= len f by NAT_1:13;
hence  ( i in dom f or i = 0 ) by A3, FINSEQ_3:25; ::_thesis: verum
end;
end;
end;

theorem Th3: :: TOPREALA:3
for x, y, X, Y being set
for f being Function st x <> y & f in product ((x,y) --> (X,Y)) holds
( f . x in X & f . y in Y )
proof
let x, y, X, Y be set ; ::_thesis: for f being Function st x <> y & f in product ((x,y) --> (X,Y)) holds
( f . x in X & f . y in Y )
let f be Function; ::_thesis: ( x <> y & f in product ((x,y) --> (X,Y)) implies ( f . x in X & f . y in Y ) )
assume that
A1: x <> y and
A2: f in product ((x,y) --> (X,Y)) ; ::_thesis: ( f . x in X & f . y in Y )
set g = (x,y) --> (X,Y);
A3: dom ((x,y) --> (X,Y)) = {x,y} by FUNCT_4:62;
then  y in dom ((x,y) --> (X,Y)) by TARSKI:def_2;
then A4: f . y in ((x,y) --> (X,Y)) . y by A2, CARD_3:9;
 x in dom ((x,y) --> (X,Y)) by A3, TARSKI:def_2;
then  f . x in ((x,y) --> (X,Y)) . x by A2, CARD_3:9;
hence  ( f . x in X & f . y in Y ) by A1, A4, FUNCT_4:63; ::_thesis: verum
end;

theorem Th4: :: TOPREALA:4
for a, b being set holds <*a,b*> = (1,2) --> (a,b)
proof
let a, b be set ; ::_thesis: <*a,b*> = (1,2) --> (a,b)
set f = (1,2) --> (a,b);
set g = <*a,b*>;
A1: dom ((1,2) --> (a,b)) = {1,2} by FUNCT_4:62;
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_((1,2)_-->_(a,b))_holds_
((1,2)_-->_(a,b))_._x_=_<*a,b*>_._x
let x be set ; ::_thesis: ( x in dom ((1,2) --> (a,b)) implies ((1,2) --> (a,b)) . b1 = <*a,b*> . b1 )
assume A3: x in dom ((1,2) --> (a,b)) ; ::_thesis: ((1,2) --> (a,b)) . b1 = <*a,b*> . b1
percases ( x = 1 or x = 2 ) by A1, A3, TARSKI:def_2;
supposeA4: x = 1 ; ::_thesis: ((1,2) --> (a,b)) . b1 = <*a,b*> . b1
hence ((1,2) --> (a,b)) . x = a by FUNCT_4:63
.= <*a,b*> . x by A4, FINSEQ_1:44 ;
::_thesis: verum
end;
supposeA5: x = 2 ; ::_thesis: ((1,2) --> (a,b)) . b1 = <*a,b*> . b1
hence ((1,2) --> (a,b)) . x = b by FUNCT_4:63
.= <*a,b*> . x by A5, FINSEQ_1:44 ;
::_thesis: verum
end;
end;
end;
 dom <*a,b*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
hence  <*a,b*> = (1,2) --> (a,b) by A2, FUNCT_1:2, FUNCT_4:62; ::_thesis: verum
end;

begin

registration
cluster non empty strict TopSpace-like constituted-FinSeqs for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is constituted-FinSeqs & not b1 is empty & b1 is strict )
proof
take T = TopSpaceMetr (Euclid 1); ::_thesis: ( T is constituted-FinSeqs & not T is empty & T is strict )
thus  for a being Element of T holds a is FinSequence :: according to MONOID_0:def_2 ::_thesis: ( not T is empty & T is strict )
proof
let a be Element of T; ::_thesis: a is FinSequence
 T = TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) by EUCLID:def_8;
hence  a is FinSequence ; ::_thesis: verum
end;
thus  ( not T is empty & T is strict ) ; ::_thesis: verum
end;
end;

registration
let T be constituted-FinSeqs TopSpace;
cluster  ->  constituted-FinSeqs for SubSpace of T;
coherence
 for b1 being SubSpace of T holds b1 is constituted-FinSeqs
proof
let X be SubSpace of T; ::_thesis: X is constituted-FinSeqs
let p be Element of X; :: according to MONOID_0:def_2 ::_thesis: p is set
A1: the carrier of X is Subset of T by TSEP_1:1;
percases ( not the carrier of X is empty or the carrier of X is empty ) ;
suppose not the carrier of X is empty ; ::_thesis: p is set
then  p in the carrier of X ;
then reconsider p = p as Point of T by A1;
 p is FinSequence ;
hence  p is set ; ::_thesis: verum
end;
suppose the carrier of X is empty ; ::_thesis: p is set
hence  p is set ; ::_thesis: verum
end;
end;
end;
end;

theorem Th5: :: TOPREALA:5
for T being non empty TopSpace
for Z being non empty SubSpace of T
for t being Point of T
for z being Point of Z
for N being open a_neighborhood of t
for M being Subset of Z st t = z & M = N /\ ([#] Z) holds
M is open a_neighborhood of z
proof
let T be non empty TopSpace; ::_thesis: for Z being non empty SubSpace of T
for t being Point of T
for z being Point of Z
for N being open a_neighborhood of t
for M being Subset of Z st t = z & M = N /\ ([#] Z) holds
M is open a_neighborhood of z
let Z be non empty SubSpace of T; ::_thesis: for t being Point of T
for z being Point of Z
for N being open a_neighborhood of t
for M being Subset of Z st t = z & M = N /\ ([#] Z) holds
M is open a_neighborhood of z
let t be Point of T; ::_thesis: for z being Point of Z
for N being open a_neighborhood of t
for M being Subset of Z st t = z & M = N /\ ([#] Z) holds
M is open a_neighborhood of z
let z be Point of Z; ::_thesis: for N being open a_neighborhood of t
for M being Subset of Z st t = z & M = N /\ ([#] Z) holds
M is open a_neighborhood of z
let N be open a_neighborhood of t; ::_thesis: for M being Subset of Z st t = z & M = N /\ ([#] Z) holds
M is open a_neighborhood of z
let M be Subset of Z; ::_thesis: ( t = z & M = N /\ ([#] Z) implies M is open a_neighborhood of z )
assume that
A1: t = z and
A2: M = N /\ ([#] Z) ; ::_thesis: M is open a_neighborhood of z
 M is open by A2, TOPS_2:24;
then A3: Int M = M by TOPS_1:23;
 ( t in Int N & Int N c= N ) by CONNSP_2:def_1, TOPS_1:16;
then  z in Int M by A1, A2, A3, XBOOLE_0:def_4;
hence  M is open a_neighborhood of z by A2, CONNSP_2:def_1, TOPS_2:24; ::_thesis: verum
end;

registration
cluster empty TopSpace-like  ->  discrete anti-discrete for TopStruct ;
coherence
 for b1 being TopSpace st b1 is empty holds
( b1 is discrete & b1 is anti-discrete )
proof
let T be TopSpace; ::_thesis: ( T is empty implies ( T is discrete & T is anti-discrete ) )
assume  T is empty ; ::_thesis: ( T is discrete & T is anti-discrete )
then  the carrier of T = {} ;
then  bool the carrier of T = {{}, the carrier of T} by ENUMSET1:29, ZFMISC_1:1;
hence  ( T is discrete & T is anti-discrete ) by TDLAT_3:14; ::_thesis: verum
end;
end;

registration
let X be discrete TopSpace;
let Y be TopSpace;
cluster Function-like quasi_total  ->  continuous for Element of bool [: the carrier of X, the carrier of Y:];
coherence
 for b1 being Function of X,Y holds b1 is continuous by TEX_2:62;
end;

theorem Th6: :: TOPREALA:6
for X being TopSpace
for Y being TopStruct
for f being Function of X,Y st f is empty holds
f is continuous
proof
let X be TopSpace; ::_thesis: for Y being TopStruct
for f being Function of X,Y st f is empty holds
f is continuous
let Y be TopStruct ; ::_thesis: for f being Function of X,Y st f is empty holds
f is continuous
let f be Function of X,Y; ::_thesis: ( f is empty implies f is continuous )
assume A1: f is empty ; ::_thesis: f is continuous
let P be Subset of Y; :: according to PRE_TOPC:def_6 ::_thesis: ( not P is closed or f " P is closed )
assume  P is closed ; ::_thesis: f " P is closed
 f " P = {} X by A1;
hence  f " P is closed ; ::_thesis: verum
end;

registration
let X be TopSpace;
let Y be TopStruct ;
cluster Function-like empty quasi_total  ->  continuous for Element of bool [: the carrier of X, the carrier of Y:];
coherence
 for b1 being Function of X,Y st b1 is empty holds
b1 is continuous by Th6;
end;

theorem :: TOPREALA:7
for X being TopStruct
for Y being non empty TopStruct
for Z being non empty SubSpace of Y
for f being Function of X,Z holds f is Function of X,Y
proof
let X be TopStruct ; ::_thesis: for Y being non empty TopStruct
for Z being non empty SubSpace of Y
for f being Function of X,Z holds f is Function of X,Y
let Y be non empty TopStruct ; ::_thesis: for Z being non empty SubSpace of Y
for f being Function of X,Z holds f is Function of X,Y
let Z be non empty SubSpace of Y; ::_thesis: for f being Function of X,Z holds f is Function of X,Y
let f be Function of X,Z; ::_thesis: f is Function of X,Y
 the carrier of Z is Subset of Y by TSEP_1:1;
then A1: rng f c= the carrier of Y by XBOOLE_1:1;
 dom f = the carrier of X by FUNCT_2:def_1;
hence  f is Function of X,Y by A1, FUNCT_2:2; ::_thesis: verum
end;

theorem :: TOPREALA:8
for S, T being non empty TopSpace
for X being Subset of S
for Y being Subset of T
for f being continuous Function of S,T
for g being Function of (S | X),(T | Y) st g = f | X holds
g is continuous
proof
let S, T be non empty TopSpace; ::_thesis: for X being Subset of S
for Y being Subset of T
for f being continuous Function of S,T
for g being Function of (S | X),(T | Y) st g = f | X holds
g is continuous
let X be Subset of S; ::_thesis: for Y being Subset of T
for f being continuous Function of S,T
for g being Function of (S | X),(T | Y) st g = f | X holds
g is continuous
let Y be Subset of T; ::_thesis: for f being continuous Function of S,T
for g being Function of (S | X),(T | Y) st g = f | X holds
g is continuous
let f be continuous Function of S,T; ::_thesis: for g being Function of (S | X),(T | Y) st g = f | X holds
g is continuous
let g be Function of (S | X),(T | Y); ::_thesis: ( g = f | X implies g is continuous )
assume A1: g = f | X ; ::_thesis: g is continuous
set h = f | X;
A2: ( the carrier of (S | X) = X & rng (f | X) c= the carrier of T ) by PRE_TOPC:8;
 dom f = the carrier of S by FUNCT_2:def_1;
then  dom (f | X) = X by RELAT_1:62;
then reconsider h = f | X as Function of (S | X),T by A2, FUNCT_2:2;
 h is continuous by TOPMETR:7;
hence  g is continuous by A1, TOPMETR:6; ::_thesis: verum
end;

theorem :: TOPREALA:9
for S, T being non empty TopSpace
for Z being non empty SubSpace of T
for f being Function of S,T
for g being Function of S,Z st f = g & f is open holds
g is open
proof
let S, T be non empty TopSpace; ::_thesis: for Z being non empty SubSpace of T
for f being Function of S,T
for g being Function of S,Z st f = g & f is open holds
g is open
let Z be non empty SubSpace of T; ::_thesis: for f being Function of S,T
for g being Function of S,Z st f = g & f is open holds
g is open
let f be Function of S,T; ::_thesis: for g being Function of S,Z st f = g & f is open holds
g is open
let g be Function of S,Z; ::_thesis: ( f = g & f is open implies g is open )
assume that
A1: f = g and
A2: f is open ; ::_thesis: g is open
 for p being Point of S
for P being open a_neighborhood of p ex R being a_neighborhood of g . p st R c= g .: P
proof
let p be Point of S; ::_thesis: for P being open a_neighborhood of p ex R being a_neighborhood of g . p st R c= g .: P
let P be open a_neighborhood of p; ::_thesis: ex R being a_neighborhood of g . p st R c= g .: P
consider R being open a_neighborhood of f . p such that
A3: R c= f .: P by A2, TOPGRP_1:22;
reconsider R2 = R /\ ([#] Z) as Subset of Z ;
reconsider R2 = R2 as a_neighborhood of g . p by A1, Th5;
take  R2 ; ::_thesis: R2 c= g .: P
 R2 c= R by XBOOLE_1:17;
hence  R2 c= g .: P by A1, A3, XBOOLE_1:1; ::_thesis: verum
end;
hence  g is open by TOPGRP_1:23; ::_thesis: verum
end;

theorem :: TOPREALA:10
for S, T being non empty TopSpace
for S1 being Subset of S
for T1 being Subset of T
for f being Function of S,T
for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds
g is open
proof
let S, T be non empty TopSpace; ::_thesis: for S1 being Subset of S
for T1 being Subset of T
for f being Function of S,T
for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds
g is open
let S1 be Subset of S; ::_thesis: for T1 being Subset of T
for f being Function of S,T
for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds
g is open
let T1 be Subset of T; ::_thesis: for f being Function of S,T
for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds
g is open
let f be Function of S,T; ::_thesis: for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds
g is open
let g be Function of (S | S1),(T | T1); ::_thesis: ( g = f | S1 & g is onto & f is open & f is one-to-one implies g is open )
assume that
A1: g = f | S1 and
A2: rng g = the carrier of (T | T1) and
A3: f is open and
A4: f is one-to-one ; :: according to FUNCT_2:def_3 ::_thesis: g is open
let A be Subset of (S | S1); :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or g .: A is open )
A5: [#] (T | T1) = T1 by PRE_TOPC:def_5;
assume  A is open ; ::_thesis: g .: A is open
then consider C being Subset of S such that
A6: C is open and
A7: C /\ ([#] (S | S1)) = A by TOPS_2:24;
A8: ( [#] (S | S1) = S1 & g .: (C /\ S1) c= (g .: C) /\ (g .: S1) ) by PRE_TOPC:def_5, RELAT_1:121;
A9: g .: A = (f .: C) /\ T1
proof
 g .: C c= f .: C by A1, RELAT_1:128;
then  (g .: C) /\ (g .: S1) c= (f .: C) /\ T1 by A5, XBOOLE_1:27;
hence  g .: A c= (f .: C) /\ T1 by A7, A8, XBOOLE_1:1; :: according to XBOOLE_0:def_10 ::_thesis: (f .: C) /\ T1 c= g .: A
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (f .: C) /\ T1 or y in g .: A )
A10: ( dom g c= dom f & dom f = the carrier of S ) by A1, FUNCT_2:def_1, RELAT_1:60;
assume A11: y in (f .: C) /\ T1 ; ::_thesis: y in g .: A
then  y in f .: C by XBOOLE_0:def_4;
then consider x being Element of S such that
A12: x in C and
A13: y = f . x by FUNCT_2:65;
 y in T1 by A11, XBOOLE_0:def_4;
then consider a being set  such that
A14: a in dom g and
A15: g . a = y by A2, A5, FUNCT_1:def_3;
 f . a = g . a by A1, A14, FUNCT_1:47;
then  a = x by A4, A13, A14, A15, A10, FUNCT_1:def_4;
then  a in A by A7, A12, A14, XBOOLE_0:def_4;
hence  y in g .: A by A14, A15, FUNCT_1:def_6; ::_thesis: verum
end;
 f .: C is open by A3, A6, T_0TOPSP:def_2;
hence  g .: A is open by A5, A9, TOPS_2:24; ::_thesis: verum
end;

theorem :: TOPREALA:11
for X, Y, Z being non empty TopSpace
for f being Function of X,Y
for g being Function of Y,Z st f is open & g is open holds
g * f is open
proof
let X, Y, Z be non empty TopSpace; ::_thesis: for f being Function of X,Y
for g being Function of Y,Z st f is open & g is open holds
g * f is open
let f be Function of X,Y; ::_thesis: for g being Function of Y,Z st f is open & g is open holds
g * f is open
let g be Function of Y,Z; ::_thesis: ( f is open & g is open implies g * f is open )
assume that
A1: f is open and
A2: g is open ; ::_thesis: g * f is open
let A be Subset of X; :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or (g * f) .: A is open )
assume  A is open ; ::_thesis: (g * f) .: A is open
then A3: f .: A is open by A1, T_0TOPSP:def_2;
 (g * f) .: A = g .: (f .: A) by RELAT_1:126;
hence  (g * f) .: A is open by A2, A3, T_0TOPSP:def_2; ::_thesis: verum
end;

theorem :: TOPREALA:12
for X, Y being TopSpace
for Z being open SubSpace of Y
for f being Function of X,Y
for g being Function of X,Z st f = g & g is open holds
f is open
proof
let X, Y be TopSpace; ::_thesis: for Z being open SubSpace of Y
for f being Function of X,Y
for g being Function of X,Z st f = g & g is open holds
f is open
let Z be open SubSpace of Y; ::_thesis: for f being Function of X,Y
for g being Function of X,Z st f = g & g is open holds
f is open
let f be Function of X,Y; ::_thesis: for g being Function of X,Z st f = g & g is open holds
f is open
let g be Function of X,Z; ::_thesis: ( f = g & g is open implies f is open )
assume that
A1: f = g and
A2: g is open ; ::_thesis: f is open
let A be Subset of X; :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or f .: A is open )
assume  A is open ; ::_thesis: f .: A is open
then  g .: A is open by A2, T_0TOPSP:def_2;
hence  f .: A is open by A1, TSEP_1:17; ::_thesis: verum
end;

theorem Th13: :: TOPREALA:13
for S, T being non empty TopSpace
for f being Function of S,T st f is one-to-one & f is onto holds
( f is continuous iff f " is open )
proof
let S, T be non empty TopSpace; ::_thesis: for f being Function of S,T st f is one-to-one & f is onto holds
( f is continuous iff f " is open )
let f be Function of S,T; ::_thesis: ( f is one-to-one & f is onto implies ( f is continuous iff f " is open ) )
assume A1: f is one-to-one ; ::_thesis: ( not f is onto or ( f is continuous iff f " is open ) )
assume  f is onto ; ::_thesis: ( f is continuous iff f " is open )
then A2: f " = f " by A1, TOPS_2:def_4;
A3: [#] T <> {} ;
thus  ( f is continuous implies f " is open ) ::_thesis: ( f " is open implies f is continuous )
proof
assume A4: f is continuous ; ::_thesis: f " is open
let A be Subset of T; :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or (f ") .: A is open )
assume  A is open ; ::_thesis: (f ") .: A is open
then  f " A is open by A3, A4, TOPS_2:43;
hence  (f ") .: A is open by A1, A2, FUNCT_1:85; ::_thesis: verum
end;
assume A5: f " is open ; ::_thesis: f is continuous
now__::_thesis:_for_A_being_Subset_of_T_st_A_is_open_holds_
f_"_A_is_open
let A be Subset of T; ::_thesis: ( A is open implies f " A is open )
assume  A is open ; ::_thesis: f " A is open
then  (f ") .: A is open by A5, T_0TOPSP:def_2;
hence  f " A is open by A1, A2, FUNCT_1:85; ::_thesis: verum
end;
hence  f is continuous by A3, TOPS_2:43; ::_thesis: verum
end;

theorem :: TOPREALA:14
for S, T being non empty TopSpace
for f being Function of S,T st f is one-to-one & f is onto holds
( f is open iff f " is continuous )
proof
let S, T be non empty TopSpace; ::_thesis: for f being Function of S,T st f is one-to-one & f is onto holds
( f is open iff f " is continuous )
let f be Function of S,T; ::_thesis: ( f is one-to-one & f is onto implies ( f is open iff f " is continuous ) )
assume A1: f is one-to-one ; ::_thesis: ( not f is onto or ( f is open iff f " is continuous ) )
assume  f is onto ; ::_thesis: ( f is open iff f " is continuous )
then A2: rng f = [#] T by FUNCT_2:def_3;
then  rng (f ") = [#] S by A1, TOPS_2:49;
then A3: f " is onto by FUNCT_2:def_3;
 ( f " is one-to-one & (f ") " = f ) by A1, A2, TOPS_2:50, TOPS_2:51;
hence  ( f is open iff f " is continuous ) by A3, Th13; ::_thesis: verum
end;

theorem :: TOPREALA:15
for S being TopSpace
for T being non empty TopSpace holds
( S,T are_homeomorphic iff TopStruct(# the carrier of S, the topology of S #), TopStruct(# the carrier of T, the topology of T #) are_homeomorphic )
proof
let S be TopSpace; ::_thesis: for T being non empty TopSpace holds
( S,T are_homeomorphic iff TopStruct(# the carrier of S, the topology of S #), TopStruct(# the carrier of T, the topology of T #) are_homeomorphic )
let T be non empty TopSpace; ::_thesis: ( S,T are_homeomorphic iff TopStruct(# the carrier of S, the topology of S #), TopStruct(# the carrier of T, the topology of T #) are_homeomorphic )
set SS = TopStruct(# the carrier of S, the topology of S #);
set TT = TopStruct(# the carrier of T, the topology of T #);
A1: ( [#] S = [#] TopStruct(# the carrier of S, the topology of S #) & [#] T = [#] TopStruct(# the carrier of T, the topology of T #) ) ;
thus  ( S,T are_homeomorphic implies TopStruct(# the carrier of S, the topology of S #), TopStruct(# the carrier of T, the topology of T #) are_homeomorphic ) ::_thesis: ( TopStruct(# the carrier of S, the topology of S #), TopStruct(# the carrier of T, the topology of T #) are_homeomorphic implies S,T are_homeomorphic )
proof
given f being Function of S,T such that A2: f is being_homeomorphism ; :: according to T_0TOPSP:def_1 ::_thesis: TopStruct(# the carrier of S, the topology of S #), TopStruct(# the carrier of T, the topology of T #) are_homeomorphic
reconsider g = f as Function of TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #) ;
A3: now__::_thesis:_for_P_being_Subset_of_TopStruct(#_the_carrier_of_S,_the_topology_of_S_#)_holds_g_.:_(Cl_P)_=_Cl_(g_.:_P)
let P be Subset of TopStruct(# the carrier of S, the topology of S #); ::_thesis: g .: (Cl P) = Cl (g .: P)
reconsider R = P as Subset of S ;
thus g .: (Cl P) = f .: (Cl R) by TOPS_3:80
.= Cl (f .: R) by A2, TOPS_2:60
.= Cl (g .: P) by TOPS_3:80 ; ::_thesis: verum
end;
take  g ; :: according to T_0TOPSP:def_1 ::_thesis: g is being_homeomorphism
 ( dom f = [#] S & rng f = [#] T ) by A2, TOPS_2:60;
hence  g is being_homeomorphism by A1, A2, A3, TOPS_2:60; ::_thesis: verum
end;
given f being Function of TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #) such that A4: f is being_homeomorphism ; :: according to T_0TOPSP:def_1 ::_thesis: S,T are_homeomorphic
reconsider g = f as Function of S,T ;
A5: now__::_thesis:_for_P_being_Subset_of_S_holds_g_.:_(Cl_P)_=_Cl_(g_.:_P)
let P be Subset of S; ::_thesis: g .: (Cl P) = Cl (g .: P)
reconsider R = P as Subset of TopStruct(# the carrier of S, the topology of S #) ;
thus g .: (Cl P) = f .: (Cl R) by TOPS_3:80
.= Cl (f .: R) by A4, TOPS_2:60
.= Cl (g .: P) by TOPS_3:80 ; ::_thesis: verum
end;
take  g ; :: according to T_0TOPSP:def_1 ::_thesis: g is being_homeomorphism
 ( dom f = [#] TopStruct(# the carrier of S, the topology of S #) & rng f = [#] TopStruct(# the carrier of T, the topology of T #) ) by A4, TOPS_2:60;
hence  g is being_homeomorphism by A1, A4, A5, TOPS_2:60; ::_thesis: verum
end;

theorem :: TOPREALA:16
for S, T being non empty TopSpace
for f being Function of S,T st f is one-to-one & f is onto & f is continuous & f is open holds
f is being_homeomorphism
proof
let S, T be non empty TopSpace; ::_thesis: for f being Function of S,T st f is one-to-one & f is onto & f is continuous & f is open holds
f is being_homeomorphism
let f be Function of S,T; ::_thesis: ( f is one-to-one & f is onto & f is continuous & f is open implies f is being_homeomorphism )
assume that
A1: f is one-to-one and
A2: f is onto and
A3: f is continuous and
A4: f is open ; ::_thesis: f is being_homeomorphism
A5: [#] T <> {} ;
A6: dom f = the carrier of S by FUNCT_2:def_1;
A7: for P being Subset of S holds
( P is open iff f .: P is open )
proof
let P be Subset of S; ::_thesis: ( P is open iff f .: P is open )
thus  ( P is open implies f .: P is open ) by A4, T_0TOPSP:def_2; ::_thesis: ( f .: P is open implies P is open )
assume  f .: P is open ; ::_thesis: P is open
then  f " (f .: P) is open by A3, A5, TOPS_2:43;
hence  P is open by A1, A6, FUNCT_1:94; ::_thesis: verum
end;
 ( dom f = [#] S & rng f = [#] T ) by A2, FUNCT_2:def_1, FUNCT_2:def_3;
hence  f is being_homeomorphism by A1, A7, TOPGRP_1:25; ::_thesis: verum
end;

begin

theorem :: TOPREALA:17
for r being real number
for f being PartFunc of REAL,REAL st f = REAL --> r holds
f | REAL is continuous
proof
let r be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f = REAL --> r holds
f | REAL is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( f = REAL --> r implies f | REAL is continuous )
assume A1: f = REAL --> r ; ::_thesis: f | REAL is continuous
 f | REAL is constant
proof
reconsider r = r as Real by XREAL_0:def_1;
take  r ; :: according to PARTFUN2:def_1 ::_thesis: for b1 being Element of REAL holds
( not b1 in dom (f | REAL) or (f | REAL) . b1 = r )
let c be Element of REAL ; ::_thesis: ( not c in dom (f | REAL) or (f | REAL) . c = r )
assume  c in dom (f | REAL) ; ::_thesis: (f | REAL) . c = r
thus (f | REAL) . c = f . c
.= r by A1, FUNCOP_1:7 ; ::_thesis: verum
end;
hence  f | REAL is continuous ; ::_thesis: verum
end;

theorem :: TOPREALA:18
for f, f1, f2 being PartFunc of REAL,REAL st dom f = (dom f1) \/ (dom f2) & dom f1 is open & dom f2 is open & f1 | (dom f1) is continuous & f2 | (dom f2) is continuous & ( for z being set st z in dom f1 holds
f . z = f1 . z ) & ( for z being set st z in dom f2 holds
f . z = f2 . z ) holds
f | (dom f) is continuous
proof
let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( dom f = (dom f1) \/ (dom f2) & dom f1 is open & dom f2 is open & f1 | (dom f1) is continuous & f2 | (dom f2) is continuous & ( for z being set st z in dom f1 holds
f . z = f1 . z ) & ( for z being set st z in dom f2 holds
f . z = f2 . z ) implies f | (dom f) is continuous )
set X1 = dom f1;
set X2 = dom f2;
assume that
A1: dom f = (dom f1) \/ (dom f2) and
A2: dom f1 is open and
A3: dom f2 is open and
A4: f1 | (dom f1) is continuous and
A5: f2 | (dom f2) is continuous and
A6: for z being set st z in dom f1 holds
f . z = f1 . z and
A7: for z being set st z in dom f2 holds
f . z = f2 . z ; ::_thesis: f | (dom f) is continuous
A8: (dom f) /\ (dom f1) = dom f1 by A1, XBOOLE_1:7, XBOOLE_1:28;
A9: dom (f | (dom f2)) = (dom f) /\ (dom f2) by RELAT_1:61;
let x be real number ; :: according to FCONT_1:def_2 ::_thesis: ( not x in dom (f | (dom f)) or f | (dom f) is_continuous_in x )
assume  x in dom (f | (dom f)) ; ::_thesis: f | (dom f) is_continuous_in x
then A10: x in dom f ;
then A11: (f | ((dom f1) \/ (dom f2))) . x = f . x by A1, FUNCT_1:49;
A12: (dom f) /\ (dom f2) = dom f2 by A1, XBOOLE_1:7, XBOOLE_1:28;
A13: dom (f | (dom f1)) = (dom f) /\ (dom f1) by RELAT_1:61;
percases ( x in dom f1 or x in dom f2 ) by A1, A10, XBOOLE_0:def_3;
supposeA14: x in dom f1 ; ::_thesis: f | (dom f) is_continuous_in x
then A15: (f | ((dom f1) \/ (dom f2))) . x = f1 . x by A6, A11
.= (f1 | (dom f1)) . x ;
 for N1 being Neighbourhood of (f | ((dom f1) \/ (dom f2))) . x ex N being Neighbourhood of x st
for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N holds
(f | ((dom f1) \/ (dom f2))) . x1 in N1
proof
let N1 be Neighbourhood of (f | ((dom f1) \/ (dom f2))) . x; ::_thesis: ex N being Neighbourhood of x st
for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N holds
(f | ((dom f1) \/ (dom f2))) . x1 in N1
consider N2 being Neighbourhood of x such that
A16: N2 c= dom f1 by A2, A14, RCOMP_1:18;
 x in dom (f1 | (dom f1)) by A14;
then  f1 | (dom f1) is_continuous_in x by A4, FCONT_1:def_2;
then consider N being Neighbourhood of x such that
A17: for x1 being real number st x1 in dom (f1 | (dom f1)) & x1 in N holds
(f1 | (dom f1)) . x1 in N1 by A15, FCONT_1:4;
consider N3 being Neighbourhood of x such that
A18: N3 c= N and
A19: N3 c= N2 by RCOMP_1:17;
take  N3 ; ::_thesis: for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N3 holds
(f | ((dom f1) \/ (dom f2))) . x1 in N1
let x1 be real number ; ::_thesis: ( x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N3 implies (f | ((dom f1) \/ (dom f2))) . x1 in N1 )
assume that
A20: x1 in dom (f | ((dom f1) \/ (dom f2))) and
A21: x1 in N3 ; ::_thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1
percases ( x1 in dom (f | (dom f1)) or not x1 in dom (f | (dom f1)) ) ;
supposeA22: x1 in dom (f | (dom f1)) ; ::_thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1
A23: dom (f | (dom f1)) = (dom f1) /\ (dom f1) by A1, A13, XBOOLE_1:7, XBOOLE_1:28
.= dom (f1 | (dom f1)) ;
A24: x1 in dom f1 by A13, A22, XBOOLE_0:def_4;
(f | ((dom f1) \/ (dom f2))) . x1 = f . x1 by A20, FUNCT_1:47
.= f1 . x1 by A6, A24
.= (f1 | (dom f1)) . x1 ;
hence  (f | ((dom f1) \/ (dom f2))) . x1 in N1 by A17, A18, A21, A22, A23; ::_thesis: verum
end;
supposeA25: not x1 in dom (f | (dom f1)) ; ::_thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1
 x1 in N2 by A19, A21;
hence  (f | ((dom f1) \/ (dom f2))) . x1 in N1 by A13, A8, A16, A25; ::_thesis: verum
end;
end;
end;
hence  f | (dom f) is_continuous_in x by A1, FCONT_1:4; ::_thesis: verum
end;
supposeA26: x in dom f2 ; ::_thesis: f | (dom f) is_continuous_in x
then A27: (f | ((dom f1) \/ (dom f2))) . x = f2 . x by A7, A11
.= (f2 | (dom f2)) . x ;
 for N1 being Neighbourhood of (f | ((dom f1) \/ (dom f2))) . x ex N being Neighbourhood of x st
for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N holds
(f | ((dom f1) \/ (dom f2))) . x1 in N1
proof
let N1 be Neighbourhood of (f | ((dom f1) \/ (dom f2))) . x; ::_thesis: ex N being Neighbourhood of x st
for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N holds
(f | ((dom f1) \/ (dom f2))) . x1 in N1
consider N2 being Neighbourhood of x such that
A28: N2 c= dom f2 by A3, A26, RCOMP_1:18;
 x in dom (f2 | (dom f2)) by A26;
then  f2 | (dom f2) is_continuous_in x by A5, FCONT_1:def_2;
then consider N being Neighbourhood of x such that
A29: for x1 being real number st x1 in dom (f2 | (dom f2)) & x1 in N holds
(f2 | (dom f2)) . x1 in N1 by A27, FCONT_1:4;
consider N3 being Neighbourhood of x such that
A30: N3 c= N and
A31: N3 c= N2 by RCOMP_1:17;
take  N3 ; ::_thesis: for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N3 holds
(f | ((dom f1) \/ (dom f2))) . x1 in N1
let x1 be real number ; ::_thesis: ( x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N3 implies (f | ((dom f1) \/ (dom f2))) . x1 in N1 )
assume that
A32: x1 in dom (f | ((dom f1) \/ (dom f2))) and
A33: x1 in N3 ; ::_thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1
percases ( x1 in dom (f | (dom f2)) or not x1 in dom (f | (dom f2)) ) ;
supposeA34: x1 in dom (f | (dom f2)) ; ::_thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1
A35: dom (f | (dom f2)) = (dom f2) /\ (dom f2) by A1, A9, XBOOLE_1:7, XBOOLE_1:28
.= dom (f2 | (dom f2)) ;
A36: x1 in dom f2 by A9, A34, XBOOLE_0:def_4;
(f | ((dom f1) \/ (dom f2))) . x1 = f . x1 by A32, FUNCT_1:47
.= f2 . x1 by A7, A36
.= (f2 | (dom f2)) . x1 ;
hence  (f | ((dom f1) \/ (dom f2))) . x1 in N1 by A29, A30, A33, A34, A35; ::_thesis: verum
end;
supposeA37: not x1 in dom (f | (dom f2)) ; ::_thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1
 x1 in N2 by A31, A33;
hence  (f | ((dom f1) \/ (dom f2))) . x1 in N1 by A9, A12, A28, A37; ::_thesis: verum
end;
end;
end;
hence  f | (dom f) is_continuous_in x by A1, FCONT_1:4; ::_thesis: verum
end;
end;
end;

theorem Th19: :: TOPREALA:19
for x being Point of R^1
for N being Subset of REAL
for M being Subset of R^1 st M = N & N is Neighbourhood of x holds
M is a_neighborhood of x
proof
let x be Point of R^1; ::_thesis: for N being Subset of REAL
for M being Subset of R^1 st M = N & N is Neighbourhood of x holds
M is a_neighborhood of x
let N be Subset of REAL; ::_thesis: for M being Subset of R^1 st M = N & N is Neighbourhood of x holds
M is a_neighborhood of x
let M be Subset of R^1; ::_thesis: ( M = N & N is Neighbourhood of x implies M is a_neighborhood of x )
assume A1: M = N ; ::_thesis: ( not N is Neighbourhood of x or M is a_neighborhood of x )
given r being real number  such that A2: 0 < r and
A3: N = ].(x - r),(x + r).[ ; :: according to RCOMP_1:def_6 ::_thesis: M is a_neighborhood of x
 M is open by A1, A3, JORDAN6:35;
hence  M is a_neighborhood of x by A1, A2, A3, CONNSP_2:3, TOPREAL6:15; ::_thesis: verum
end;

theorem Th20: :: TOPREALA:20
for x being Point of R^1
for M being a_neighborhood of x ex N being Neighbourhood of x st N c= M
proof
let x be Point of R^1; ::_thesis: for M being a_neighborhood of x ex N being Neighbourhood of x st N c= M
let M be a_neighborhood of x; ::_thesis: ex N being Neighbourhood of x st N c= M
consider V being Subset of R^1 such that
A1: V is open and
A2: V c= M and
A3: x in V by CONNSP_2:6;
 x is Real by XREAL_0:def_1;
then consider r being Real such that
A4: r > 0 and
A5: ].(x - r),(x + r).[ c= V by A1, A3, FRECHET:8;
reconsider N = ].(x - r),(x + r).[ as Neighbourhood of x by A4, RCOMP_1:def_6;
take  N ; ::_thesis: N c= M
thus  N c= M by A2, A5, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th21: :: TOPREALA:21
for f being Function of R^1,R^1
for g being PartFunc of REAL,REAL
for x being Point of R^1 st f = g & g is_continuous_in x holds
f is_continuous_at x
proof
let f be Function of R^1,R^1; ::_thesis: for g being PartFunc of REAL,REAL
for x being Point of R^1 st f = g & g is_continuous_in x holds
f is_continuous_at x
let g be PartFunc of REAL,REAL; ::_thesis: for x being Point of R^1 st f = g & g is_continuous_in x holds
f is_continuous_at x
let x be Point of R^1; ::_thesis: ( f = g & g is_continuous_in x implies f is_continuous_at x )
assume that
A1: f = g and
A2: g is_continuous_in x ; ::_thesis: f is_continuous_at x
let G be a_neighborhood of f . x; :: according to TMAP_1:def_2 ::_thesis: ex b1 being a_neighborhood of x st f .: b1 c= G
consider Z being Neighbourhood of g . x such that
A3: Z c= G by A1, Th20;
consider N being Neighbourhood of x such that
A4: g .: N c= Z by A2, FCONT_1:5;
reconsider H = N as a_neighborhood of x by Th19, TOPMETR:17;
take  H ; ::_thesis: f .: H c= G
thus  f .: H c= G by A1, A3, A4, XBOOLE_1:1; ::_thesis: verum
end;

theorem :: TOPREALA:22
for f being Function of R^1,R^1
for g being Function of REAL,REAL st f = g & g is continuous holds
f is continuous
proof
let f be Function of R^1,R^1; ::_thesis: for g being Function of REAL,REAL st f = g & g is continuous holds
f is continuous
let g be Function of REAL,REAL; ::_thesis: ( f = g & g is continuous implies f is continuous )
assume that
A1: f = g and
A2: g is continuous ; ::_thesis: f is continuous
 for x being Point of R^1 holds f is_continuous_at x
proof
let x be Point of R^1; ::_thesis: f is_continuous_at x
 dom f = REAL by A1, FUNCT_2:def_1;
then  x in dom g by A1, XREAL_0:def_1;
then  g is_continuous_in x by A2, FCONT_1:def_2;
hence  f is_continuous_at x by A1, Th21; ::_thesis: verum
end;
hence  f is continuous by TMAP_1:44; ::_thesis: verum
end;

theorem :: TOPREALA:23
for a, r, s, b being real number st a <= r & s <= b holds
[.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b))
proof
let a, r, s, b be real number ; ::_thesis: ( a <= r & s <= b implies [.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b)) )
set T = Closed-Interval-TSpace (a,b);
set A = [.r,s.];
assume that
A1: a <= r and
A2: s <= b ; ::_thesis: [.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b))
percases ( r > s or r <= s ) ;
suppose r > s ; ::_thesis: [.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b))
then  [.r,s.] = {} (Closed-Interval-TSpace (a,b)) by XXREAL_1:29;
hence  [.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b)) ; ::_thesis: verum
end;
suppose r <= s ; ::_thesis: [.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b))
then  a <= s by A1, XXREAL_0:2;
then  the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by A2, TOPMETR:18, XXREAL_0:2;
then reconsider A = [.r,s.] as Subset of (Closed-Interval-TSpace (a,b)) by A1, A2, XXREAL_1:34;
reconsider C = A as Subset of R^1 by TOPMETR:17;
 ( C is closed & C /\ ([#] (Closed-Interval-TSpace (a,b))) = A ) by TREAL_1:1, XBOOLE_1:28;
hence  [.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b)) by PRE_TOPC:13; ::_thesis: verum
end;
end;
end;

theorem :: TOPREALA:24
for a, r, s, b being real number st a <= r & s <= b holds
].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b))
proof
let a, r, s, b be real number ; ::_thesis: ( a <= r & s <= b implies ].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b)) )
set T = Closed-Interval-TSpace (a,b);
set A = ].r,s.[;
assume that
A1: a <= r and
A2: s <= b ; ::_thesis: ].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b))
percases ( r >= s or r < s ) ;
suppose r >= s ; ::_thesis: ].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b))
then  ].r,s.[ = {} (Closed-Interval-TSpace (a,b)) by XXREAL_1:28;
hence  ].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b)) ; ::_thesis: verum
end;
suppose r < s ; ::_thesis: ].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b))
then  a < s by A1, XXREAL_0:2;
then  the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by A2, TOPMETR:18, XXREAL_0:2;
then reconsider A = ].r,s.[ as Subset of (Closed-Interval-TSpace (a,b)) by A1, A2, XXREAL_1:37;
reconsider C = A as Subset of R^1 by TOPMETR:17;
 ( C is open & C /\ ([#] (Closed-Interval-TSpace (a,b))) = A ) by JORDAN6:35, XBOOLE_1:28;
hence  ].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b)) by TOPS_2:24; ::_thesis: verum
end;
end;
end;

theorem :: TOPREALA:25
for a, b, r being real number st a <= b & a <= r holds
].r,b.] is open Subset of (Closed-Interval-TSpace (a,b))
proof
let a, b, r be real number ; ::_thesis: ( a <= b & a <= r implies ].r,b.] is open Subset of (Closed-Interval-TSpace (a,b)) )
set T = Closed-Interval-TSpace (a,b);
assume that
A1: a <= b and
A2: a <= r ; ::_thesis: ].r,b.] is open Subset of (Closed-Interval-TSpace (a,b))
A3: the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by A1, TOPMETR:18;
then reconsider A = ].r,b.] as Subset of (Closed-Interval-TSpace (a,b)) by A2, XXREAL_1:36;
reconsider C = ].r,(b + 1).[ as Subset of R^1 by TOPMETR:17;
A4: C /\ ([#] (Closed-Interval-TSpace (a,b))) c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C /\ ([#] (Closed-Interval-TSpace (a,b))) or x in A )
assume A5: x in C /\ ([#] (Closed-Interval-TSpace (a,b))) ; ::_thesis: x in A
then A6: x in C by XBOOLE_0:def_4;
then reconsider x = x as Real ;
A7: r < x by A6, XXREAL_1:4;
 x <= b by A3, A5, XXREAL_1:1;
hence  x in A by A7; ::_thesis: verum
end;
 b + 0 < b + 1 by XREAL_1:6;
then  A c= C by XXREAL_1:49;
then  A c= C /\ ([#] (Closed-Interval-TSpace (a,b))) by XBOOLE_1:19;
then  ( C is open & C /\ ([#] (Closed-Interval-TSpace (a,b))) = A ) by A4, JORDAN6:35, XBOOLE_0:def_10;
hence  ].r,b.] is open Subset of (Closed-Interval-TSpace (a,b)) by TOPS_2:24; ::_thesis: verum
end;

theorem :: TOPREALA:26
for a, b, r being real number st a <= b & r <= b holds
[.a,r.[ is open Subset of (Closed-Interval-TSpace (a,b))
proof
let a, b, r be real number ; ::_thesis: ( a <= b & r <= b implies [.a,r.[ is open Subset of (Closed-Interval-TSpace (a,b)) )
set T = Closed-Interval-TSpace (a,b);
assume that
A1: a <= b and
A2: r <= b ; ::_thesis: [.a,r.[ is open Subset of (Closed-Interval-TSpace (a,b))
A3: the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by A1, TOPMETR:18;
then reconsider A = [.a,r.[ as Subset of (Closed-Interval-TSpace (a,b)) by A2, XXREAL_1:35;
reconsider C = ].(a - 1),r.[ as Subset of R^1 by TOPMETR:17;
A4: C /\ ([#] (Closed-Interval-TSpace (a,b))) c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C /\ ([#] (Closed-Interval-TSpace (a,b))) or x in A )
assume A5: x in C /\ ([#] (Closed-Interval-TSpace (a,b))) ; ::_thesis: x in A
then A6: x in C by XBOOLE_0:def_4;
then reconsider x = x as Real ;
A7: x < r by A6, XXREAL_1:4;
 a <= x by A3, A5, XXREAL_1:1;
hence  x in A by A7; ::_thesis: verum
end;
 a - 1 < a - 0 by XREAL_1:15;
then  A c= C by XXREAL_1:48;
then  A c= C /\ ([#] (Closed-Interval-TSpace (a,b))) by XBOOLE_1:19;
then  ( C is open & C /\ ([#] (Closed-Interval-TSpace (a,b))) = A ) by A4, JORDAN6:35, XBOOLE_0:def_10;
hence  [.a,r.[ is open Subset of (Closed-Interval-TSpace (a,b)) by TOPS_2:24; ::_thesis: verum
end;

theorem Th27: :: TOPREALA:27
for a, b, r, s being real number st a <= b & r <= s holds
the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] = [:[.a,b.],[.r,s.]:]
proof
let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] = [:[.a,b.],[.r,s.]:] )
set C1 = Closed-Interval-TSpace (a,b);
set C2 = Closed-Interval-TSpace (r,s);
assume  ( a <= b & r <= s ) ; ::_thesis: the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] = [:[.a,b.],[.r,s.]:]
then  ( the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] & the carrier of (Closed-Interval-TSpace (r,s)) = [.r,s.] ) by TOPMETR:18;
hence  the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] = [:[.a,b.],[.r,s.]:] by BORSUK_1:def_2; ::_thesis: verum
end;

begin

theorem :: TOPREALA:28
for a, b being real number holds |[a,b]| = (1,2) --> (a,b) by Th4;

theorem :: TOPREALA:29
for a, b being real number holds
( |[a,b]| . 1 = a & |[a,b]| . 2 = b )
proof
let a, b be real number ; ::_thesis: ( |[a,b]| . 1 = a & |[a,b]| . 2 = b )
thus |[a,b]| . 1 = ((1,2) --> (a,b)) . 1 by Th4
.= a by FUNCT_4:63 ; ::_thesis: |[a,b]| . 2 = b
thus |[a,b]| . 2 = ((1,2) --> (a,b)) . 2 by Th4
.= b by FUNCT_4:63 ; ::_thesis: verum
end;

theorem Th30: :: TOPREALA:30
for a, b, r, s being real number holds closed_inside_of_rectangle (a,b,r,s) = product ((1,2) --> ([.a,b.],[.r,s.]))
proof
let a, b, r, s be real number ; ::_thesis: closed_inside_of_rectangle (a,b,r,s) = product ((1,2) --> ([.a,b.],[.r,s.]))
set A = [.a,b.];
set B = [.r,s.];
set f = (1,2) --> ([.a,b.],[.r,s.]);
set R = closed_inside_of_rectangle (a,b,r,s);
A1: closed_inside_of_rectangle (a,b,r,s) =  {  p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s )  }  by JGRAPH_6:def_2;
thus  closed_inside_of_rectangle (a,b,r,s) c= product ((1,2) --> ([.a,b.],[.r,s.])) :: according to XBOOLE_0:def_10 ::_thesis: product ((1,2) --> ([.a,b.],[.r,s.])) c= closed_inside_of_rectangle (a,b,r,s)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in closed_inside_of_rectangle (a,b,r,s) or x in product ((1,2) --> ([.a,b.],[.r,s.])) )
assume  x in closed_inside_of_rectangle (a,b,r,s) ; ::_thesis: x in product ((1,2) --> ([.a,b.],[.r,s.]))
then consider p being Point of (TOP-REAL 2) such that
A2: x = p and
A3: ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s ) by A1;
 |[(p `1),(p `2)]| = (1,2) --> ((p `1),(p `2)) by Th4;
then A4: p = (1,2) --> ((p `1),(p `2)) by EUCLID:53;
 ( p `1 in [.a,b.] & p `2 in [.r,s.] ) by A3;
hence  x in product ((1,2) --> ([.a,b.],[.r,s.])) by A2, A4, HILBERT3:11; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product ((1,2) --> ([.a,b.],[.r,s.])) or x in closed_inside_of_rectangle (a,b,r,s) )
assume A5: x in product ((1,2) --> ([.a,b.],[.r,s.])) ; ::_thesis: x in closed_inside_of_rectangle (a,b,r,s)
then consider g being Function such that
A6: x = g and
A7: dom g = dom ((1,2) --> ([.a,b.],[.r,s.])) and
 for y being set st y in dom ((1,2) --> ([.a,b.],[.r,s.])) holds
g . y in ((1,2) --> ([.a,b.],[.r,s.])) . y by CARD_3:def_5;
A8: g . 2 in [.r,s.] by A5, A6, Th3;
A9: g . 1 in [.a,b.] by A5, A6, Th3;
then reconsider g1 = g . 1, g2 = g . 2 as Real by A8;
A10: dom ((1,2) --> ([.a,b.],[.r,s.])) = {1,2} by FUNCT_4:62;
then reconsider g = g as FinSequence by A7, FINSEQ_1:2, FINSEQ_1:def_2;
A11: len g = 2 by A7, A10, FINSEQ_1:2, FINSEQ_1:def_3;
 |[g1,g2]| = (1,2) --> (g1,g2) by Th4;
then reconsider g = g as Point of (TOP-REAL 2) by A11, FINSEQ_1:44;
A12: ( r <= g `2 & g `2 <= s ) by A8, XXREAL_1:1;
 ( a <= g `1 & g `1 <= b ) by A9, XXREAL_1:1;
hence  x in closed_inside_of_rectangle (a,b,r,s) by A1, A6, A12; ::_thesis: verum
end;

theorem Th31: :: TOPREALA:31
for a, b, r, s being real number st a <= b & r <= s holds
|[a,r]| in closed_inside_of_rectangle (a,b,r,s)
proof
let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies |[a,r]| in closed_inside_of_rectangle (a,b,r,s) )
set o = |[a,r]|;
A1: ( closed_inside_of_rectangle (a,b,r,s) =  {  p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s )  }  & |[a,r]| `1 = a ) by EUCLID:52, JGRAPH_6:def_2;
A2: |[a,r]| `2 = r by EUCLID:52;
assume  ( a <= b & r <= s ) ; ::_thesis: |[a,r]| in closed_inside_of_rectangle (a,b,r,s)
hence  |[a,r]| in closed_inside_of_rectangle (a,b,r,s) by A1, A2; ::_thesis: verum
end;

definition
let a, b, c, d be real number ;
func Trectangle (a,b,c,d) ->  SubSpace of TOP-REAL 2 equals :: TOPREALA:def 1
(TOP-REAL 2) | (closed_inside_of_rectangle (a,b,c,d));
coherence
 (TOP-REAL 2) | (closed_inside_of_rectangle (a,b,c,d)) is SubSpace of TOP-REAL 2 ;
end;

:: deftheorem  defines Trectangle TOPREALA:def_1_:_
 for a, b, c, d being real number holds Trectangle (a,b,c,d) = (TOP-REAL 2) | (closed_inside_of_rectangle (a,b,c,d));

theorem Th32: :: TOPREALA:32
for a, b, r, s being real number st a <= b & r <= s holds
not Trectangle (a,b,r,s) is empty
proof
let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies not Trectangle (a,b,r,s) is empty )
assume  ( a <= b & r <= s ) ; ::_thesis: not Trectangle (a,b,r,s) is empty
then  |[a,r]| in closed_inside_of_rectangle (a,b,r,s) by Th31;
hence  not the carrier of (Trectangle (a,b,r,s)) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;

registration
let a, c be real non positive number ;
let b, d be real non negative number ;
cluster Trectangle (a,b,c,d) ->  non empty ;
coherence
 not Trectangle (a,b,c,d) is empty by Th32;
end;

definition
func R2Homeomorphism  ->  Function of [:R^1,R^1:],(TOP-REAL 2) means :Def2: :: TOPREALA:def 2
 for x, y being real number holds it . [x,y] = <*x,y*>;
existence
 ex b1 being Function of [:R^1,R^1:],(TOP-REAL 2) st
for x, y being real number holds b1 . [x,y] = <*x,y*>
proof
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 BORSUK_6:20;
take  f ; ::_thesis: for x, y being real number holds f . [x,y] = <*x,y*>
let x, y be real number ; ::_thesis: f . [x,y] = <*x,y*>
 ( x is Real & y is Real ) by XREAL_0:def_1;
hence  f . [x,y] = <*x,y*> by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:R^1,R^1:],(TOP-REAL 2) st ( for x, y being real number holds b1 . [x,y] = <*x,y*> ) & ( for x, y being real number holds b2 . [x,y] = <*x,y*> ) holds
b1 = b2
proof
let f, g be Function of [:R^1,R^1:],(TOP-REAL 2); ::_thesis: ( ( for x, y being real number holds f . [x,y] = <*x,y*> ) & ( for x, y being real number holds g . [x,y] = <*x,y*> ) implies f = g )
assume that
A2: for x, y being real number holds f . [x,y] = <*x,y*> and
A3: for x, y being real number holds g . [x,y] = <*x,y*> ; ::_thesis: f = g
let a be Point of [:R^1,R^1:]; :: according to FUNCT_2:def_8 ::_thesis: f . a = g . a
consider x, y being Element of the carrier of R^1 such that
A4: a = [x,y] by Lm1, DOMAIN_1:1;
thus f . a = <*x,y*> by A2, A4
.= g . a by A3, A4 ; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines R2Homeomorphism TOPREALA:def_2_:_
 for b1 being Function of [:R^1,R^1:],(TOP-REAL 2) holds
( b1 = R2Homeomorphism iff for x, y being real number holds b1 . [x,y] = <*x,y*> );

theorem Th33: :: TOPREALA:33
for A, B being Subset of REAL holds R2Homeomorphism .: [:A,B:] = product ((1,2) --> (A,B))
proof
 for x, y being Real holds R2Homeomorphism . [x,y] = <*x,y*> by Def2;
hence  for A, B being Subset of REAL holds R2Homeomorphism .: [:A,B:] = product ((1,2) --> (A,B)) by TOPREAL6:75; ::_thesis: verum
end;

theorem Th34: :: TOPREALA:34
R2Homeomorphism is being_homeomorphism
proof
 for x, y being Real holds R2Homeomorphism . [x,y] = <*x,y*> by Def2;
hence  R2Homeomorphism is being_homeomorphism by TOPREAL6:76; ::_thesis: verum
end;

theorem Th35: :: TOPREALA:35
for a, b, r, s being real number st a <= b & r <= s holds
R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is Function of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],(Trectangle (a,b,r,s))
proof
let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is Function of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],(Trectangle (a,b,r,s)) )
set C1 = Closed-Interval-TSpace (a,b);
set C2 = Closed-Interval-TSpace (r,s);
set TR = Trectangle (a,b,r,s);
set h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):];
assume  ( a <= b & r <= s ) ; ::_thesis: R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is Function of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],(Trectangle (a,b,r,s))
then A1: the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] = [:[.a,b.],[.r,s.]:] by Th27;
 dom R2Homeomorphism = [: the carrier of R^1, the carrier of R^1:] by Lm1, FUNCT_2:def_1;
then A2: dom (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) = the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] by A1, RELAT_1:62, TOPMETR:17, ZFMISC_1:96;
 rng (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) c= the carrier of (Trectangle (a,b,r,s))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) or y in the carrier of (Trectangle (a,b,r,s)) )
A3: ( the carrier of (Trectangle (a,b,r,s)) = closed_inside_of_rectangle (a,b,r,s) & closed_inside_of_rectangle (a,b,r,s) =  {  p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s )  }  ) by JGRAPH_6:def_2, PRE_TOPC:8;
assume  y in rng (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) ; ::_thesis: y in the carrier of (Trectangle (a,b,r,s))
then consider x being set  such that
A4: x in dom (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) and
A5: (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) . x = y by FUNCT_1:def_3;
reconsider x = x as Point of [:R^1,R^1:] by A4;
 dom (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) c= [: the carrier of R^1, the carrier of R^1:] by A1, A2, TOPMETR:17, ZFMISC_1:96;
then consider x1, x2 being Element of the carrier of R^1 such that
A6: x = [x1,x2] by A4, DOMAIN_1:1;
A7: x2 in [.r,s.] by A1, A2, A4, A6, ZFMISC_1:87;
A8: (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) . x = R2Homeomorphism . x by A4, FUNCT_1:47;
then reconsider p = (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) . x as Point of (TOP-REAL 2) ;
A9: (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) . x = <*x1,x2*> by A8, A6, Def2;
then  x2 = p `2 by FINSEQ_1:44;
then A10: ( r <= p `2 & p `2 <= s ) by A7, XXREAL_1:1;
A11: x1 in [.a,b.] by A1, A2, A4, A6, ZFMISC_1:87;
 x1 = p `1 by A9, FINSEQ_1:44;
then  ( a <= p `1 & p `1 <= b ) by A11, XXREAL_1:1;
hence  y in the carrier of (Trectangle (a,b,r,s)) by A5, A3, A10; ::_thesis: verum
end;
hence  R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is Function of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],(Trectangle (a,b,r,s)) by A2, FUNCT_2:2; ::_thesis: verum
end;

theorem Th36: :: TOPREALA:36
for a, b, r, s being real number st a <= b & r <= s holds
for h being Function of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],(Trectangle (a,b,r,s)) st h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] holds
h is being_homeomorphism
proof
let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies for h being Function of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],(Trectangle (a,b,r,s)) st h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] holds
h is being_homeomorphism )
assume A1: ( a <= b & r <= s ) ; ::_thesis: for h being Function of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],(Trectangle (a,b,r,s)) st h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] holds
h is being_homeomorphism
set TR = Trectangle (a,b,r,s);
A2: closed_inside_of_rectangle (a,b,r,s) =  {  p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s )  }  by JGRAPH_6:def_2;
set p = |[a,r]|;
 ( |[a,r]| `1 = a & |[a,r]| `2 = r ) by EUCLID:52;
then  |[a,r]| in closed_inside_of_rectangle (a,b,r,s) by A1, A2;
then reconsider T0 = Trectangle (a,b,r,s) as non empty SubSpace of TOP-REAL 2 ;
set C2 = Closed-Interval-TSpace (r,s);
set C1 = Closed-Interval-TSpace (a,b);
let h be Function of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],(Trectangle (a,b,r,s)); ::_thesis: ( h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] implies h is being_homeomorphism )
assume A3: h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] ; ::_thesis: h is being_homeomorphism
reconsider S0 = [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] as non empty SubSpace of [:R^1,R^1:] by BORSUK_3:21;
reconsider g = h as Function of S0,T0 ;
A4: the carrier of (Trectangle (a,b,r,s)) = closed_inside_of_rectangle (a,b,r,s) by PRE_TOPC:8;
A5: g is onto
proof
thus  rng g c= the carrier of T0 ; :: according to XBOOLE_0:def_10,FUNCT_2:def_3 ::_thesis: the carrier of T0 c= rng g
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of T0 or y in rng g )
A6: ( the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] = [:[.a,b.],[.r,s.]:] & dom g = the carrier of S0 ) by A1, Th27, FUNCT_2:def_1;
assume  y in the carrier of T0 ; ::_thesis: y in rng g
then consider p being Point of (TOP-REAL 2) such that
A7: y = p and
A8: ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s ) by A2, A4;
 ( p `1 in [.a,b.] & p `2 in [.r,s.] ) by A8;
then A9: [(p `1),(p `2)] in dom g by A6, ZFMISC_1:def_2;
then g . [(p `1),(p `2)] = R2Homeomorphism . [(p `1),(p `2)] by A3, FUNCT_1:49
.= |[(p `1),(p `2)]| by Def2
.= y by A7, EUCLID:53 ;
hence  y in rng g by A9, FUNCT_1:def_3; ::_thesis: verum
end;
 g = R2Homeomorphism | S0 by A3;
hence  h is being_homeomorphism by A5, Th34, JORDAN16:9; ::_thesis: verum
end;

theorem :: TOPREALA:37
for a, b, r, s being real number st a <= b & r <= s holds
[:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], Trectangle (a,b,r,s) are_homeomorphic
proof
let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], Trectangle (a,b,r,s) are_homeomorphic )
set C1 = Closed-Interval-TSpace (a,b);
set C2 = Closed-Interval-TSpace (r,s);
assume A1: ( a <= b & r <= s ) ; ::_thesis: [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], Trectangle (a,b,r,s) are_homeomorphic
then reconsider h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] as Function of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],(Trectangle (a,b,r,s)) by Th35;
take  h ; :: according to T_0TOPSP:def_1 ::_thesis: h is being_homeomorphism
thus  h is being_homeomorphism by A1, Th36; ::_thesis: verum
end;

theorem Th38: :: TOPREALA:38
for a, b, r, s being real number st a <= b & r <= s holds
for A being Subset of (Closed-Interval-TSpace (a,b))
for B being Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is Subset of (Trectangle (a,b,r,s))
proof
let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies for A being Subset of (Closed-Interval-TSpace (a,b))
for B being Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is Subset of (Trectangle (a,b,r,s)) )
set T = Closed-Interval-TSpace (a,b);
set S = Closed-Interval-TSpace (r,s);
assume  ( a <= b & r <= s ) ; ::_thesis: for A being Subset of (Closed-Interval-TSpace (a,b))
for B being Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is Subset of (Trectangle (a,b,r,s))
then A1: ( the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] & the carrier of (Closed-Interval-TSpace (r,s)) = [.r,s.] ) by TOPMETR:18;
let A be Subset of (Closed-Interval-TSpace (a,b)); ::_thesis: for B being Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is Subset of (Trectangle (a,b,r,s))
let B be Subset of (Closed-Interval-TSpace (r,s)); ::_thesis: product ((1,2) --> (A,B)) is Subset of (Trectangle (a,b,r,s))
 closed_inside_of_rectangle (a,b,r,s) = product ((1,2) --> ([.a,b.],[.r,s.])) by Th30;
then  product ((1,2) --> (A,B)) c= closed_inside_of_rectangle (a,b,r,s) by A1, TOPREAL6:21;
hence  product ((1,2) --> (A,B)) is Subset of (Trectangle (a,b,r,s)) by PRE_TOPC:8; ::_thesis: verum
end;

theorem :: TOPREALA:39
for a, b, r, s being real number st a <= b & r <= s holds
for A being open Subset of (Closed-Interval-TSpace (a,b))
for B being open Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is open Subset of (Trectangle (a,b,r,s))
proof
let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies for A being open Subset of (Closed-Interval-TSpace (a,b))
for B being open Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is open Subset of (Trectangle (a,b,r,s)) )
set T = Closed-Interval-TSpace (a,b);
set S = Closed-Interval-TSpace (r,s);
assume A1: ( a <= b & r <= s ) ; ::_thesis: for A being open Subset of (Closed-Interval-TSpace (a,b))
for B being open Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is open Subset of (Trectangle (a,b,r,s))
then reconsider h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] as Function of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],(Trectangle (a,b,r,s)) by Th35;
let A be open Subset of (Closed-Interval-TSpace (a,b)); ::_thesis: for B being open Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is open Subset of (Trectangle (a,b,r,s))
let B be open Subset of (Closed-Interval-TSpace (r,s)); ::_thesis: product ((1,2) --> (A,B)) is open Subset of (Trectangle (a,b,r,s))
reconsider P = product ((1,2) --> (A,B)) as Subset of (Trectangle (a,b,r,s)) by A1, Th38;
A2: [:A,B:] is open by BORSUK_1:6;
 the carrier of (Closed-Interval-TSpace (r,s)) is Subset of R^1 by TSEP_1:1;
then A3: B is Subset of REAL by TOPMETR:17, XBOOLE_1:1;
 the carrier of (Closed-Interval-TSpace (a,b)) is Subset of R^1 by TSEP_1:1;
then A4: A is Subset of REAL by TOPMETR:17, XBOOLE_1:1;
A5: h .: [:A,B:] = R2Homeomorphism .: [:A,B:] by RELAT_1:129
.= P by A4, A3, Th33 ;
 ( h is being_homeomorphism & not Trectangle (a,b,r,s) is empty ) by A1, Th32, Th36;
hence  product ((1,2) --> (A,B)) is open Subset of (Trectangle (a,b,r,s)) by A5, A2, TOPGRP_1:25; ::_thesis: verum
end;

theorem :: TOPREALA:40
for a, b, r, s being real number st a <= b & r <= s holds
for A being closed Subset of (Closed-Interval-TSpace (a,b))
for B being closed Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is closed Subset of (Trectangle (a,b,r,s))
proof
let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies for A being closed Subset of (Closed-Interval-TSpace (a,b))
for B being closed Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is closed Subset of (Trectangle (a,b,r,s)) )
set T = Closed-Interval-TSpace (a,b);
set S = Closed-Interval-TSpace (r,s);
assume A1: ( a <= b & r <= s ) ; ::_thesis: for A being closed Subset of (Closed-Interval-TSpace (a,b))
for B being closed Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is closed Subset of (Trectangle (a,b,r,s))
then reconsider h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] as Function of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],(Trectangle (a,b,r,s)) by Th35;
let A be closed Subset of (Closed-Interval-TSpace (a,b)); ::_thesis: for B being closed Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is closed Subset of (Trectangle (a,b,r,s))
let B be closed Subset of (Closed-Interval-TSpace (r,s)); ::_thesis: product ((1,2) --> (A,B)) is closed Subset of (Trectangle (a,b,r,s))
reconsider P = product ((1,2) --> (A,B)) as Subset of (Trectangle (a,b,r,s)) by A1, Th38;
A2: [:A,B:] is closed by TOPALG_3:15;
 the carrier of (Closed-Interval-TSpace (r,s)) is Subset of R^1 by TSEP_1:1;
then A3: B is Subset of REAL by TOPMETR:17, XBOOLE_1:1;
 the carrier of (Closed-Interval-TSpace (a,b)) is Subset of R^1 by TSEP_1:1;
then A4: A is Subset of REAL by TOPMETR:17, XBOOLE_1:1;
A5: h .: [:A,B:] = R2Homeomorphism .: [:A,B:] by RELAT_1:129
.= P by A4, A3, Th33 ;
 ( h is being_homeomorphism & not Trectangle (a,b,r,s) is empty ) by A1, Th32, Th36;
hence  product ((1,2) --> (A,B)) is closed Subset of (Trectangle (a,b,r,s)) by A5, A2, TOPS_2:58; ::_thesis: verum
end;