let p1, p2 be Point of (TOP-REAL 2); :: thesis: 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); :: thesis: ( 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} ; :: thesis: 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;

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 "))

reconsider h = h as Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | P) ;

take h ; :: according to TOPREAL2:def 1 :: thesis: 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; :: thesis: verum

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); :: thesis: ( 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} ; :: thesis: 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 :: thesis: 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 ")) . x2

then A106:
h is one-to-one
by A48, A60, A62, A51, A40, A66, TOPMETR2:1;not (ff2 * (g2 ")) . x1 = (ff1 * (g1 ")) . x2

let x1, x2 be set ; :: thesis: ( 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 "))) ; :: thesis: not (ff2 * (g2 ")) . x1 = (ff1 * (g1 ")) . x2

A88: 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 ; :: thesis: contradiction

then (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;

end;assume that

A86: x1 in dom (ff2 * (g2 ")) and

A87: x2 in (dom (ff1 * (g1 "))) \ (dom (ff2 * (g2 "))) ; :: thesis: not (ff2 * (g2 ")) . x1 = (ff1 * (g1 ")) . x2

A88: 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 ; :: thesis: contradiction

then (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;

end;

suppose A94:
(ff2 * (g2 ")) . x1 = p1
; :: thesis: contradiction

A95:
(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; :: thesis: verum

end;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; :: thesis: verum

suppose A100:
(ff2 * (g2 ")) . x1 = p2
; :: thesis: contradiction

A101:
(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; :: thesis: verum

end;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; :: thesis: verum

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

then A111:
rng h = [#] ((TOP-REAL 2) | P9)
by A3, A31, A52, A84, TOPMETR2:2;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ")))) ; :: thesis: 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; :: thesis: verum

end;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 ")))) ; :: thesis: 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; :: thesis: verum

reconsider h = h as Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | P) ;

take h ; :: according to TOPREAL2:def 1 :: thesis: 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; :: thesis: verum