let p1, p2 be Point of (TOP-REAL 2); :: thesis:
let P, P1, P2 be non empty Subset of (TOP-REAL 2); :: thesis:
assume that
( p1 <> p2 & p1 in P & p2 in P ) and
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:
consider f1 being Function of I[01] ,((TOP-REAL 2) | P1) such that
A5: f1 is being_homeomorphism and
A6: ( f1 . 0 = p1 & f1 . 1 = p2 ) by A1, TOPREAL1:def 2;
consider f2 being Function of I[01] ,((TOP-REAL 2) | P2) such that
A7: f2 is being_homeomorphism and
A8: ( f2 . 0 = p1 & f2 . 1 = p2 ) by A2, TOPREAL1:def 2;
consider h1, h2 being FinSequence of (TOP-REAL 2) such that
A9: ( h1 is being_S-Seq & h2 is being_S-Seq ) and
A10: ( R^2-unit_square = (L~ h1) \/ (L~ h2) & (L~ h1) /\ (L~ h2) = {|[0 ,0 ]|,|[1,1]|} ) and
A11: ( h1 /. 1 = |[0 ,0 ]| & h1 /. (len h1) = |[1,1]| ) and
A12: ( h2 /. 1 = |[0 ,0 ]| & h2 /. (len h2) = |[1,1]| ) by TOPREAL1:30;
reconsider L1 = L~ h1, L2 = L~ h2 as non empty Subset of (TOP-REAL 2) by A10;
L1 is_an_arc_of |[0 ,0 ]|,|[1,1]| by A9, A11, TOPREAL1:31;
then consider g1 being Function of I[01] ,((TOP-REAL 2) | L1) such that
A13: ( g1 is being_homeomorphism & g1 . 0 = |[0 ,0 ]| & g1 . 1 = |[1,1]| ) by TOPREAL1:def 2;
L2 is_an_arc_of |[0 ,0 ]|,|[1,1]| by A9, A12, TOPREAL1:31;
then consider g2 being Function of I[01] ,((TOP-REAL 2) | L2) such that
A14: ( g2 is being_homeomorphism & g2 . 0 = |[0 ,0 ]| & g2 . 1 = |[1,1]| ) by TOPREAL1:def 2;
A15: ( [#] ((TOP-REAL 2) | P1) = P1 & [#] ((TOP-REAL 2) | P) = P & P1 c= P ) by A3, PRE_TOPC:def 10, XBOOLE_1:7;
reconsider P' = P, P1' = P1, P2' = P2 as non empty Subset of (TOP-REAL 2) ;
( dom f1 = the carrier of I[01] & rng f1 c= the carrier of ((TOP-REAL 2) | P) ) by A15, FUNCT_2:def 1, XBOOLE_1:1;
then reconsider ff1 = f1 as Function of I[01] ,((TOP-REAL 2) | P') by FUNCT_2:def 1, RELSET_1:11;
( f1 is continuous & (TOP-REAL 2) | P1' is SubSpace of (TOP-REAL 2) | P' ) by A5, A15, TOPMETR:4, TOPS_2:def 5;
then A16: ff1 is continuous by PRE_TOPC:56;
A17: ( [#] ((TOP-REAL 2) | P2) = P2 & [#] ((TOP-REAL 2) | P) = P & P2 c= P ) by A3, PRE_TOPC:def 10, XBOOLE_1:7;
then ( dom f2 = the carrier of I[01] & rng f2 c= the carrier of ((TOP-REAL 2) | P) ) by FUNCT_2:def 1, XBOOLE_1:1;
then reconsider ff2 = f2 as Function of I[01] ,((TOP-REAL 2) | P') by FUNCT_2:def 1, RELSET_1:11;
( f2 is continuous & (TOP-REAL 2) | P2' is SubSpace of (TOP-REAL 2) | P' ) by A7, A17, TOPMETR:4, TOPS_2:def 5;
then A18: ff2 is continuous by PRE_TOPC:56;
set k1 = ff1 * (g1 " );
set k2 = ff2 * (g2 " );
reconsider RS = R^2-unit_square as non empty Subset of (TOP-REAL 2) ;
( len h1 >= 2 & len h2 >= 2 ) by A9, TOPREAL1:def 10;
then reconsider Lh1 = L~ h1, Lh2 = L~ h2 as non empty Subset of (TOP-REAL 2) by TOPREAL1:29;
reconsider g1 = g1 as Function of I[01] ,((TOP-REAL 2) | Lh1) ;
reconsider g2 = g2 as Function of I[01] ,((TOP-REAL 2) | Lh2) ;
set T1 = (TOP-REAL 2) | Lh1;
set T2 = (TOP-REAL 2) | Lh2;
set T = (TOP-REAL 2) | RS;
R^2-unit_square = [#] ((TOP-REAL 2) | RS) by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL 2) | RS) ;
then reconsider p00 = |[0 ,0 ]|, p11 = |[1,1]| as Point of ((TOP-REAL 2) | RS) by Lm21, Lm22, TOPREAL1:20;
A19: ( [#] ((TOP-REAL 2) | Lh1) = L~ h1 & [#] ((TOP-REAL 2) | Lh2) = L~ h2 & [#] ((TOP-REAL 2) | RS) = R^2-unit_square ) by PRE_TOPC:def 10;
A20: I[01] is compact by HEINE:11, TOPMETR:27;
A21: ( g1 is continuous & g2 is continuous & rng g1 = [#] ((TOP-REAL 2) | Lh1) & rng g2 = [#] ((TOP-REAL 2) | Lh2) & dom g1 = [#] I[01] & dom g2 = [#] I[01] ) by A13, A14, TOPS_2:def 5;
then A22: ( (TOP-REAL 2) | Lh1 is compact & (TOP-REAL 2) | Lh2 is compact ) by A20, COMPTS_1:23;
A23: (TOP-REAL 2) | RS is T_2 by TOPMETR:3;
( g1 " is continuous & g2 " is continuous ) by A13, A14, TOPS_2:def 5;
then A24: ( ff1 * (g1 " ) is continuous & ff2 * (g2 " ) is continuous ) by A16, A18;
A25: ( g1 is one-to-one & g2 is one-to-one ) by A13, A14, TOPS_2:def 5;
then A26: g2 " = g2 " by A21, TOPS_2:def 4;
A27: g1 " = g1 " by A21, A25, TOPS_2:def 4;
A28: ( dom g1 = the carrier of I[01] & the carrier of I[01] = [.0 ,1.] & dom g2 = the carrier of I[01] & dom ff1 = the carrier of I[01] & dom ff2 = the carrier of I[01] ) by BORSUK_1:83, FUNCT_2:def 1;
then A29: ( 0 in dom g1 & 0 in dom g2 ) by XXREAL_1:1;
A30: ( 0 in dom ff2 & 0 in dom ff1 ) by A28, XXREAL_1:1;
A31: p00 in rng g2 by A14, A29, FUNCT_1:def 5;
A32: dom (g2 " ) = rng g2 by A25, A26, FUNCT_1:54;
A33: p00 in dom (g2 " ) by A25, A26, A31, FUNCT_1:54;
A34: 0 = (g2 " ) . p00 by A14, A25, A26, A29, FUNCT_1:54;
(g2 " ) . p00 in dom ff2 by A14, A25, A26, A28, A29, FUNCT_1:54;
then A35: p00 in dom (ff2 * (g2 " )) by A33, FUNCT_1:21;
A36: dom (g1 " ) = rng g1 by A25, A27, FUNCT_1:54;
then A37: p00 in dom (g1 " ) by A13, A29, FUNCT_1:def 5;
A38: 0 = (g1 " ) . p00 by A13, A25, A27, A29, FUNCT_1:54;
(g1 " ) . p00 in dom ff1 by A13, A25, A27, A28, A29, FUNCT_1:54;
then p00 in dom (ff1 * (g1 " )) by A37, FUNCT_1:21;
then A39: (ff1 * (g1 " )) . p00 = ff1 . ((g1 " ) . p00) by FUNCT_1:22
.= p1 by A6, A13, A25, A27, A29, FUNCT_1:54 ;
then A40: (ff1 * (g1 " )) . p00 = ff2 . ((g2 " ) . p00) by A8, A14, A25, A26, A29, FUNCT_1:54
.= (ff2 * (g2 " )) . p00 by A35, FUNCT_1:22 ;
A41: ( 1 in dom g1 & 1 in dom g2 ) by A28, XXREAL_1:1;
A42: ( 1 in dom ff2 & 1 in dom ff1 ) by A28, XXREAL_1:1;
A43: ( p11 in dom (g2 " ) & p11 in dom (g1 " ) ) by A13, A14, A32, A36, A41, FUNCT_1:def 5;
A44: 1 = (g2 " ) . p11 by A14, A25, A26, A41, FUNCT_1:54;
(g2 " ) . p11 in dom ff2 by A14, A25, A26, A28, A41, FUNCT_1:54;
then A45: p11 in dom (ff2 * (g2 " )) by A43, FUNCT_1:21;
A46: 1 = (g1 " ) . p11 by A13, A25, A27, A41, FUNCT_1:54;
(g1 " ) . p11 in dom ff1 by A13, A25, A27, A28, A41, FUNCT_1:54;
then p11 in dom (ff1 * (g1 " )) by A43, FUNCT_1:21;
then A47: (ff1 * (g1 " )) . p11 = ff1 . ((g1 " ) . p11) by FUNCT_1:22
.= p2 by A6, A13, A25, A27, A41, FUNCT_1:54 ;
then A48: (ff1 * (g1 " )) . p11 = ff2 . ((g2 " ) . p11) by A8, A14, A25, A26, A41, FUNCT_1:54
.= (ff2 * (g2 " )) . p11 by A45, FUNCT_1:22 ;
( (TOP-REAL 2) | Lh1 is SubSpace of (TOP-REAL 2) | RS & (TOP-REAL 2) | Lh2 is SubSpace of (TOP-REAL 2) | RS ) by A10, A19, TOPMETR:4, XBOOLE_1:7;
then reconsider h = (ff1 * (g1 " )) +* (ff2 * (g2 " )) as continuous Function of ((TOP-REAL 2) | RS),((TOP-REAL 2) | P) by A10, A19, A22, A23, A24, A40, A48, COMPTS_1:30;
A49: (TOP-REAL 2) | RS is compact by Th2, COMPTS_1:12;
A50: (TOP-REAL 2) | P' is T_2 by TOPMETR:3;
A51: f1 is one-to-one by A5, TOPS_2:def 5;
A52: g1 " is one-to-one by A25, A27;
then A53: ff1 * (g1 " ) is one-to-one by A51;
A54: f2 is one-to-one by A7, TOPS_2:def 5;
A55: g2 " is one-to-one by A25, A26;
then A56: ff2 * (g2 " ) is one-to-one by A54;
A57: rng (g1 " ) = dom g1 by A25, A27, FUNCT_1:55;
A58: rng (g2 " ) = dom g2 by A25, A26, FUNCT_1:55;
then A59: dom (ff2 * (g2 " )) = dom (g2 " ) by A28, RELAT_1:46;
A60: (ff1 * (g1 " )) .: ((dom (ff1 * (g1 " ))) /\ (dom (ff2 * (g2 " )))) c= rng (ff2 * (g2 " ))

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in (ff1 * (g1 " )) .: ((dom (ff1 * (g1 " ))) /\ (dom (ff2 * (g2 " )))) ; :: thesis:
then A61: ex x being set st
( x in dom (ff1 * (g1 " )) & x in (dom (ff1 * (g1 " ))) /\ (dom (ff2 * (g2 " ))) & a = (ff1 * (g1 " )) . x ) by FUNCT_1:def 12;
( dom (ff1 * (g1 " )) = the carrier of ((TOP-REAL 2) | Lh1) & dom (ff2 * (g2 " )) = the carrier of ((TOP-REAL 2) | Lh2) & the carrier of ((TOP-REAL 2) | Lh1) = [#] ((TOP-REAL 2) | Lh1) & the carrier of ((TOP-REAL 2) | Lh2) = [#] ((TOP-REAL 2) | Lh2) ) by FUNCT_2:def 1;
then ( a = p1 or a = p2 ) by A10, A19, A39, A47, A61, TARSKI:def 2;
hence a in rng (ff2 * (g2 " )) by A33, A39, A40, A43, A47, A48, A59, FUNCT_1:def 5; :: thesis:

end;

( dom f1 = the carrier of I[01] & dom g1 = the carrier of I[01] ) by FUNCT_2:def 1;
then A62: rng (ff1 * (g1 " )) = rng f1 by A57, RELAT_1:47
.= P1 by A5, A15, TOPS_2:def 5 ;
A63: rng (ff2 * (g2 " )) = rng f2 by A28, A58, RELAT_1:47
.= [#] ((TOP-REAL 2) | P2) by A7, TOPS_2:def 5
.= P2 by PRE_TOPC:def 10 ;
then A64: rng h = [#] ((TOP-REAL 2) | P') by A3, A15, A60, A62, TOPMETR2:3;
A65: dom h = [#] ((TOP-REAL 2) | RS) by FUNCT_2:def 1;

now

let x1, x2 be set ; :: thesis:
assume that
A66: x1 in dom (ff2 * (g2 " )) and
A67: x2 in (dom (ff1 * (g1 " ))) \ (dom (ff2 * (g2 " ))) ; :: thesis:
assume A68: (ff2 * (g2 " )) . x1 = (ff1 * (g1 " )) . x2 ; :: thesis:
A69: x2 in dom (ff1 * (g1 " )) by A67, XBOOLE_0:def 5;
then ( (ff2 * (g2 " )) . x1 in P2 & (ff2 * (g2 " )) . x1 in P1 ) by A62, A63, A66, A68, FUNCT_1:def 5;
then A70: (ff2 * (g2 " )) . x1 in P1 /\ P2 by XBOOLE_0:def 4;
A71: x1 in dom (g2 " ) by A66, FUNCT_1:21;
A72: x2 in dom (g1 " ) by A69, FUNCT_1:21;

per cases ) . x1 = p1 or (ff2 * (g2 " )) . x1 = p2 ) by A4, A70, TARSKI:def 2;

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

then ( p1 = ff2 . ((g2 " ) . x1) & (g2 " ) . x1 in dom ff2 & ff2 . 0 = p1 ) by A8, A66, FUNCT_1:21, FUNCT_1:22;
then ( (g2 " ) . x1 = 0 & p00 in dom (g2 " ) ) by A25, A26, A30, A31, A54, FUNCT_1:54, FUNCT_1:def 8;
then A74: x1 = p00 by A34, A55, A71, FUNCT_1:def 8;
( p1 = ff1 . ((g1 " ) . x2) & (g1 " ) . x2 in dom ff1 & ff1 . 0 = p1 ) by A6, A68, A69, A73, FUNCT_1:21, FUNCT_1:22;
then ( (g1 " ) . x2 = 0 & p00 in dom (g1 " ) ) by A13, A28, A30, A36, A51, FUNCT_1:def 5, FUNCT_1:def 8;
then x2 in dom (ff2 * (g2 " )) by A38, A52, A66, A72, A74, FUNCT_1:def 8;
hence contradiction by A67, XBOOLE_0:def 5; :: thesis:

end;

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

then ( p2 = ff2 . ((g2 " ) . x1) & (g2 " ) . x1 in dom ff2 & ff2 . 1 = p2 ) by A8, A66, FUNCT_1:21, FUNCT_1:22;
then ( (g2 " ) . x1 = 1 & p11 in dom (g2 " ) ) by A14, A28, A32, A42, A54, FUNCT_1:def 5, FUNCT_1:def 8;
then A76: x1 = p11 by A44, A55, A71, FUNCT_1:def 8;
( p2 = ff1 . ((g1 " ) . x2) & (g1 " ) . x2 in dom ff1 & ff1 . 1 = p2 ) by A6, A68, A69, A75, FUNCT_1:21, FUNCT_1:22;
then ( (g1 " ) . x2 = 1 & p11 in dom (g1 " ) ) by A13, A28, A36, A42, A51, FUNCT_1:def 5, FUNCT_1:def 8;
then x2 in dom (ff2 * (g2 " )) by A46, A52, A66, A72, A76, FUNCT_1:def 8;
hence contradiction by A67, XBOOLE_0:def 5; :: thesis:

end;

then A77: h is one-to-one by A53, A56, TOPMETR2:2;
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:
thus h is being_homeomorphism by A49, A50, A64, A65, A77, COMPTS_1:26; :: thesis: