let p1, p2 be Point of (TOP-REAL 2); for P, P1, P2 being non empty Subset of (TOP-REAL 2) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} holds
P is being_simple_closed_curve
reconsider RS = R^2-unit_square as non empty Subset of (TOP-REAL 2) ;
let P, P1, P2 be non empty Subset of (TOP-REAL 2); ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} implies P is being_simple_closed_curve )
assume that
A1:
P1 is_an_arc_of p1,p2
and
A2:
P2 is_an_arc_of p1,p2
and
A3:
P = P1 \/ P2
and
A4:
P1 /\ P2 = {p1,p2}
; P is being_simple_closed_curve
reconsider P9 = P, P19 = P1, P29 = P2 as non empty Subset of (TOP-REAL 2) ;
A5:
[#] ((TOP-REAL 2) | P1) = P1
by PRE_TOPC:def 5;
consider h1, h2 being FinSequence of (TOP-REAL 2) such that
A6:
h1 is being_S-Seq
and
A7:
h2 is being_S-Seq
and
A8:
R^2-unit_square = (L~ h1) \/ (L~ h2)
and
A9:
(L~ h1) /\ (L~ h2) = {|[0,0]|,|[1,1]|}
and
A10:
h1 /. 1 = |[0,0]|
and
A11:
h1 /. (len h1) = |[1,1]|
and
A12:
h2 /. 1 = |[0,0]|
and
A13:
h2 /. (len h2) = |[1,1]|
by TOPREAL1:24;
A14:
len h2 >= 2
by A7, TOPREAL1:def 8;
len h1 >= 2
by A6, TOPREAL1:def 8;
then reconsider Lh1 = L~ h1, Lh2 = L~ h2 as non empty Subset of (TOP-REAL 2) by A14, TOPREAL1:23;
set T1 = (TOP-REAL 2) | Lh1;
set T2 = (TOP-REAL 2) | Lh2;
set T = (TOP-REAL 2) | RS;
A15:
[#] ((TOP-REAL 2) | RS) = R^2-unit_square
by PRE_TOPC:def 5;
A16:
[#] ((TOP-REAL 2) | Lh2) = L~ h2
by PRE_TOPC:def 5;
then A17:
(TOP-REAL 2) | Lh2 is SubSpace of (TOP-REAL 2) | RS
by A8, A15, TOPMETR:3, XBOOLE_1:7;
A18:
[#] ((TOP-REAL 2) | Lh1) = L~ h1
by PRE_TOPC:def 5;
then A19:
(TOP-REAL 2) | Lh1 is SubSpace of (TOP-REAL 2) | RS
by A8, A15, TOPMETR:3, XBOOLE_1:7;
A20:
[#] ((TOP-REAL 2) | P) = P
by PRE_TOPC:def 5;
A21:
[#] ((TOP-REAL 2) | P2) = P2
by PRE_TOPC:def 5;
then A22:
(TOP-REAL 2) | P29 is SubSpace of (TOP-REAL 2) | P9
by A3, A20, TOPMETR:3, XBOOLE_1:7;
consider f2 being Function of I[01],((TOP-REAL 2) | P2) such that
A23:
f2 is being_homeomorphism
and
A24:
f2 . 0 = p1
and
A25:
f2 . 1 = p2
by A2, TOPREAL1:def 1;
A26:
dom f2 = the carrier of I[01]
by FUNCT_2:def 1;
P2 c= P
by A3, XBOOLE_1:7;
then
rng f2 c= the carrier of ((TOP-REAL 2) | P)
by A21, A20;
then reconsider ff2 = f2 as Function of I[01],((TOP-REAL 2) | P9) by A26, RELSET_1:4;
A27:
dom ff2 = the carrier of I[01]
by FUNCT_2:def 1;
then A28:
0 in dom ff2
by BORSUK_1:40, XXREAL_1:1;
f2 is continuous
by A23;
then A29:
ff2 is continuous
by A22, PRE_TOPC:26;
A30:
1 in dom ff2
by A27, BORSUK_1:40, XXREAL_1:1;
A31:
[#] ((TOP-REAL 2) | P) = P
by PRE_TOPC:def 5;
then A32:
(TOP-REAL 2) | P19 is SubSpace of (TOP-REAL 2) | P9
by A3, A5, TOPMETR:3, XBOOLE_1:7;
consider f1 being Function of I[01],((TOP-REAL 2) | P1) such that
A33:
f1 is being_homeomorphism
and
A34:
f1 . 0 = p1
and
A35:
f1 . 1 = p2
by A1, TOPREAL1:def 1;
A36:
dom f1 = the carrier of I[01]
by FUNCT_2:def 1;
P1 c= P
by A3, XBOOLE_1:7;
then
rng f1 c= the carrier of ((TOP-REAL 2) | P)
by A5, A31;
then reconsider ff1 = f1 as Function of I[01],((TOP-REAL 2) | P9) by A36, RELSET_1:4;
A37:
dom f1 = the carrier of I[01]
by FUNCT_2:def 1;
A38:
I[01] is compact
by HEINE:4, TOPMETR:20;
f1 is continuous
by A33;
then A39:
ff1 is continuous
by A32, PRE_TOPC:26;
A40:
f1 is one-to-one
by A33;
reconsider L1 = L~ h1, L2 = L~ h2 as non empty Subset of (TOP-REAL 2) by A9;
L1 is_an_arc_of |[0,0]|,|[1,1]|
by A6, A10, A11, TOPREAL1:25;
then consider g1 being Function of I[01],((TOP-REAL 2) | L1) such that
A41:
g1 is being_homeomorphism
and
A42:
g1 . 0 = |[0,0]|
and
A43:
g1 . 1 = |[1,1]|
by TOPREAL1:def 1;
L2 is_an_arc_of |[0,0]|,|[1,1]|
by A7, A12, A13, TOPREAL1:25;
then consider g2 being Function of I[01],((TOP-REAL 2) | L2) such that
A44:
g2 is being_homeomorphism
and
A45:
g2 . 0 = |[0,0]|
and
A46:
g2 . 1 = |[1,1]|
by TOPREAL1:def 1;
R^2-unit_square =
[#] ((TOP-REAL 2) | RS)
by PRE_TOPC:def 5
.=
the carrier of ((TOP-REAL 2) | RS)
;
then reconsider p00 = |[0,0]|, p11 = |[1,1]| as Point of ((TOP-REAL 2) | RS) by Lm28, Lm29, TOPREAL1:14;
A47:
(TOP-REAL 2) | RS is T_2
by TOPMETR:2;
set k1 = ff1 * (g1 ");
set k2 = ff2 * (g2 ");
reconsider g1 = g1 as Function of I[01],((TOP-REAL 2) | Lh1) ;
A48:
g1 is one-to-one
by A41;
A49:
dom g1 = the carrier of I[01]
by FUNCT_2:def 1;
A50:
rng g1 = [#] ((TOP-REAL 2) | Lh1)
by A41;
then
g1 is onto
by FUNCT_2:def 3;
then A51:
g1 " = g1 "
by A48, TOPS_2:def 4;
then
rng (g1 ") = dom g1
by A48, FUNCT_1:33;
then A52: rng (ff1 * (g1 ")) =
rng f1
by A37, A49, RELAT_1:28
.=
P1
by A33, A5
;
A53:
dom g1 = the carrier of I[01]
by FUNCT_2:def 1;
then A54:
0 in dom g1
by BORSUK_1:40, XXREAL_1:1;
then A55:
0 = (g1 ") . p00
by A42, A48, A51, FUNCT_1:32;
A56:
dom (g1 ") = rng g1
by A48, A51, FUNCT_1:32;
then A57:
p00 in dom (g1 ")
by A42, A54, FUNCT_1:def 3;
A58:
1 in dom g1
by A53, BORSUK_1:40, XXREAL_1:1;
then A59:
p11 in dom (g1 ")
by A43, A56, FUNCT_1:def 3;
reconsider g2 = g2 as Function of I[01],((TOP-REAL 2) | Lh2) ;
A60:
g2 is one-to-one
by A44;
A61:
rng g2 = [#] ((TOP-REAL 2) | Lh2)
by A44;
then
g2 is onto
by FUNCT_2:def 3;
then A62:
g2 " = g2 "
by A60, TOPS_2:def 4;
g2 is continuous
by A44;
then A63:
(TOP-REAL 2) | Lh2 is compact
by A38, A61, COMPTS_1:14;
A64:
g2 " is continuous
by A44;
g1 is continuous
by A41;
then A65:
(TOP-REAL 2) | Lh1 is compact
by A38, A50, COMPTS_1:14;
A66:
f2 is one-to-one
by A23;
A67:
dom g2 = the carrier of I[01]
by FUNCT_2:def 1;
then A68:
0 in dom g2
by BORSUK_1:40, XXREAL_1:1;
then A69:
p00 in rng g2
by A45, FUNCT_1:def 3;
then A70:
p00 in dom (g2 ")
by A60, A62, FUNCT_1:32;
(g2 ") . p00 in dom ff2
by A45, A60, A62, A53, A67, A27, A54, FUNCT_1:32;
then A71:
p00 in dom (ff2 * (g2 "))
by A70, FUNCT_1:11;
A72:
dom ff1 = the carrier of I[01]
by FUNCT_2:def 1;
then
(g1 ") . p00 in dom ff1
by A42, A48, A51, A53, A54, FUNCT_1:32;
then
p00 in dom (ff1 * (g1 "))
by A57, FUNCT_1:11;
then A73: (ff1 * (g1 ")) . p00 =
ff1 . ((g1 ") . p00)
by FUNCT_1:12
.=
p1
by A34, A42, A48, A51, A54, FUNCT_1:32
;
then A74: (ff1 * (g1 ")) . p00 =
ff2 . ((g2 ") . p00)
by A24, A45, A60, A62, A68, FUNCT_1:32
.=
(ff2 * (g2 ")) . p00
by A71, FUNCT_1:12
;
A75:
1 in dom g2
by A67, BORSUK_1:40, XXREAL_1:1;
then A76:
1 = (g2 ") . p11
by A46, A60, A62, FUNCT_1:32;
A77:
dom (g2 ") = rng g2
by A60, A62, FUNCT_1:32;
then A78:
p11 in dom (g2 ")
by A46, A75, FUNCT_1:def 3;
(g2 ") . p11 in dom ff2
by A46, A60, A62, A53, A67, A27, A58, FUNCT_1:32;
then A79:
p11 in dom (ff2 * (g2 "))
by A78, FUNCT_1:11;
(g1 ") . p11 in dom ff1
by A43, A48, A51, A53, A72, A58, FUNCT_1:32;
then
p11 in dom (ff1 * (g1 "))
by A59, FUNCT_1:11;
then A80: (ff1 * (g1 ")) . p11 =
ff1 . ((g1 ") . p11)
by FUNCT_1:12
.=
p2
by A35, A43, A48, A51, A58, FUNCT_1:32
;
then A81: (ff1 * (g1 ")) . p11 =
ff2 . ((g2 ") . p11)
by A25, A46, A60, A62, A75, FUNCT_1:32
.=
(ff2 * (g2 ")) . p11
by A79, FUNCT_1:12
;
g1 " is continuous
by A41;
then reconsider h = (ff1 * (g1 ")) +* (ff2 * (g2 ")) as continuous Function of ((TOP-REAL 2) | RS),((TOP-REAL 2) | P) by A8, A9, A39, A29, A18, A16, A15, A65, A63, A47, A64, A74, A81, A19, A17, COMPTS_1:21;
A82:
1 = (g1 ") . p11
by A43, A48, A51, A58, FUNCT_1:32;
A83:
rng (g2 ") = dom g2
by A60, A62, FUNCT_1:33;
then A84: rng (ff2 * (g2 ")) =
rng f2
by A67, A27, RELAT_1:28
.=
[#] ((TOP-REAL 2) | P2)
by A23
.=
P2
by PRE_TOPC:def 5
;
A85:
0 = (g2 ") . p00
by A45, A60, A62, A68, FUNCT_1:32;
now for x1, x2 being set st x1 in dom (ff2 * (g2 ")) & x2 in (dom (ff1 * (g1 "))) \ (dom (ff2 * (g2 "))) holds
not (ff2 * (g2 ")) . x1 = (ff1 * (g1 ")) . x2let x1,
x2 be
set ;
( x1 in dom (ff2 * (g2 ")) & x2 in (dom (ff1 * (g1 "))) \ (dom (ff2 * (g2 "))) implies not (ff2 * (g2 ")) . x1 = (ff1 * (g1 ")) . x2 )assume that A86:
x1 in dom (ff2 * (g2 "))
and A87:
x2 in (dom (ff1 * (g1 "))) \ (dom (ff2 * (g2 ")))
;
not (ff2 * (g2 ")) . x1 = (ff1 * (g1 ")) . x2A88:
x1 in dom (g2 ")
by A86, FUNCT_1:11;
A89:
(ff2 * (g2 ")) . x1 in P2
by A84, A86, FUNCT_1:def 3;
A90:
x2 in dom (ff1 * (g1 "))
by A87, XBOOLE_0:def 5;
then A91:
x2 in dom (g1 ")
by FUNCT_1:11;
assume A92:
(ff2 * (g2 ")) . x1 = (ff1 * (g1 ")) . x2
;
contradictionthen
(ff2 * (g2 ")) . x1 in P1
by A52, A90, FUNCT_1:def 3;
then A93:
(ff2 * (g2 ")) . x1 in P1 /\ P2
by A89, XBOOLE_0:def 4;
per cases
( (ff2 * (g2 ")) . x1 = p1 or (ff2 * (g2 ")) . x1 = p2 )
by A4, A93, TARSKI:def 2;
suppose A94:
(ff2 * (g2 ")) . x1 = p1
;
contradictionA95:
(g1 ") . x2 in dom ff1
by A90, FUNCT_1:11;
p1 = ff1 . ((g1 ") . x2)
by A92, A90, A94, FUNCT_1:12;
then A96:
(g1 ") . x2 = 0
by A34, A72, A28, A40, A95, FUNCT_1:def 4;
A97:
p00 in dom (g2 ")
by A60, A62, A69, FUNCT_1:32;
A98:
(g2 ") . x1 in dom ff2
by A86, FUNCT_1:11;
p1 = ff2 . ((g2 ") . x1)
by A86, A94, FUNCT_1:12;
then
(g2 ") . x1 = 0
by A24, A28, A66, A98, FUNCT_1:def 4;
then A99:
x1 = p00
by A60, A62, A85, A88, A97, FUNCT_1:def 4;
p00 in dom (g1 ")
by A42, A53, A28, A56, FUNCT_1:def 3;
then
x2 in dom (ff2 * (g2 "))
by A48, A51, A55, A86, A91, A99, A96, FUNCT_1:def 4;
hence
contradiction
by A87, XBOOLE_0:def 5;
verum end; suppose A100:
(ff2 * (g2 ")) . x1 = p2
;
contradictionA101:
(g1 ") . x2 in dom ff1
by A90, FUNCT_1:11;
p2 = ff1 . ((g1 ") . x2)
by A92, A90, A100, FUNCT_1:12;
then A102:
(g1 ") . x2 = 1
by A35, A72, A30, A40, A101, FUNCT_1:def 4;
A103:
p11 in dom (g2 ")
by A46, A67, A77, A30, FUNCT_1:def 3;
A104:
(g2 ") . x1 in dom ff2
by A86, FUNCT_1:11;
p2 = ff2 . ((g2 ") . x1)
by A86, A100, FUNCT_1:12;
then
(g2 ") . x1 = 1
by A25, A30, A66, A104, FUNCT_1:def 4;
then A105:
x1 = p11
by A60, A62, A76, A88, A103, FUNCT_1:def 4;
p11 in dom (g1 ")
by A43, A53, A56, A30, FUNCT_1:def 3;
then
x2 in dom (ff2 * (g2 "))
by A48, A51, A82, A86, A91, A105, A102, FUNCT_1:def 4;
hence
contradiction
by A87, XBOOLE_0:def 5;
verum end; end;
then A106:
h is one-to-one
by A48, A60, A62, A51, A40, A66, TOPMETR2:1;
A107:
(TOP-REAL 2) | P9 is T_2
by TOPMETR:2;
A108:
dom (ff2 * (g2 ")) = dom (g2 ")
by A27, A83, RELAT_1:27;
(ff1 * (g1 ")) .: ((dom (ff1 * (g1 "))) /\ (dom (ff2 * (g2 ")))) c= rng (ff2 * (g2 "))
proof
let a be
object ;
TARSKI:def 3 ( not a in (ff1 * (g1 ")) .: ((dom (ff1 * (g1 "))) /\ (dom (ff2 * (g2 ")))) or a in rng (ff2 * (g2 ")) )
A109:
dom (ff2 * (g2 ")) = the
carrier of
((TOP-REAL 2) | Lh2)
by FUNCT_2:def 1;
assume
a in (ff1 * (g1 ")) .: ((dom (ff1 * (g1 "))) /\ (dom (ff2 * (g2 "))))
;
a in rng (ff2 * (g2 "))
then A110:
ex
x being
object st
(
x in dom (ff1 * (g1 ")) &
x in (dom (ff1 * (g1 "))) /\ (dom (ff2 * (g2 "))) &
a = (ff1 * (g1 ")) . x )
by FUNCT_1:def 6;
dom (ff1 * (g1 ")) = the
carrier of
((TOP-REAL 2) | Lh1)
by FUNCT_2:def 1;
then
(
a = p1 or
a = p2 )
by A9, A18, A16, A73, A80, A110, A109, TARSKI:def 2;
hence
a in rng (ff2 * (g2 "))
by A70, A73, A74, A78, A80, A81, A108, FUNCT_1:def 3;
verum
end;
then A111:
rng h = [#] ((TOP-REAL 2) | P9)
by A3, A31, A52, A84, TOPMETR2:2;
reconsider h = h as Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | P) ;
take
h
; TOPREAL2:def 1 h is being_homeomorphism
(TOP-REAL 2) | RS is compact
by Th2, COMPTS_1:3;
hence
h is being_homeomorphism
by A107, A111, A106, COMPTS_1:17; verum