let P, Kb be Subset of (TOP-REAL 2); :: thesis: for f being Function of ((TOP-REAL 2) | Kb),((TOP-REAL 2) | P) st Kb = { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } & f is being_homeomorphism holds
P is being_simple_closed_curve
let f be Function of ((TOP-REAL 2) | Kb),((TOP-REAL 2) | P); :: thesis: ( Kb = { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } & f is being_homeomorphism implies P is being_simple_closed_curve )
assume A1: ( Kb = { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } & f is being_homeomorphism ) ; :: thesis: P is being_simple_closed_curve
set v = |[1,0 ]|;
( |[1,0 ]| `1 = 1 & |[1,0 ]| `2 = 0 ) by EUCLID:56;
then A2: |[1,0 ]| in { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } ;
dom f = [#] ((TOP-REAL 2) | Kb) by A1, TOPS_2:def 5
.= Kb by PRE_TOPC:def 10 ;
then f . |[1,0 ]| in rng f by A1, A2, FUNCT_1:12;
then reconsider PP = P as non empty Subset of (TOP-REAL 2) ;
reconsider Kbb = Kb as non empty Subset of (TOP-REAL 2) by A1, A2;
reconsider Kbd = Kbb as non empty Subset of (TOP-REAL 2) ;
reconsider g = f as Function of ((TOP-REAL 2) | Kbb),((TOP-REAL 2) | PP) ;
set b = 1;
set a = 0 ;
set A = 2 / (1 - 0 );
set B = 1 - ((2 * 1) / (1 - 0 ));
set C = 2 / (1 - 0 );
set D = 1 - ((2 * 1) / (1 - 0 ));
defpred S1[ set , set ] means for t being Point of (TOP-REAL 2) st t = $1 holds
$2 = |[(((2 / (1 - 0 )) * (t `1 )) + (1 - ((2 * 1) / (1 - 0 )))),(((2 / (1 - 0 )) * (t `2 )) + (1 - ((2 * 1) / (1 - 0 ))))]|;
A5: for x being set st x in the carrier of (TOP-REAL 2) holds
ex y being set st S1[x,y]
proof
let x be set ; :: thesis: ( x in the carrier of (TOP-REAL 2) implies ex y being set st S1[x,y] )
assume x in the carrier of (TOP-REAL 2) ; :: thesis: ex y being set st S1[x,y]
then reconsider t2 = x as Point of (TOP-REAL 2) ;
reconsider y2 = |[(((2 / (1 - 0 )) * (t2 `1 )) + (1 - ((2 * 1) / (1 - 0 )))),(((2 / (1 - 0 )) * (t2 `2 )) + (1 - ((2 * 1) / (1 - 0 ))))]| as set ;
for t being Point of (TOP-REAL 2) st t = x holds
y2 = |[(((2 / (1 - 0 )) * (t `1 )) + (1 - ((2 * 1) / (1 - 0 )))),(((2 / (1 - 0 )) * (t `2 )) + (1 - ((2 * 1) / (1 - 0 ))))]| ;
hence ex y being set st S1[x,y] ; :: thesis: verum
end;
ex ff being Function st
( dom ff = the carrier of (TOP-REAL 2) & ( for x being set st x in the carrier of (TOP-REAL 2) holds
S1[x,ff . x] ) ) from CLASSES1:sch 1(A5);
 then consider ff being Function such that
A6: ( dom ff = the carrier of (TOP-REAL 2) & ( for x being set st x in the carrier of (TOP-REAL 2) holds
for t being Point of (TOP-REAL 2) st t = x holds
ff . x = |[(((2 / (1 - 0 )) * (t `1 )) + (1 - ((2 * 1) / (1 - 0 )))),(((2 / (1 - 0 )) * (t `2 )) + (1 - ((2 * 1) / (1 - 0 ))))]| ) ) ;
A7: for t being Point of (TOP-REAL 2) holds ff . t = |[(((2 / (1 - 0 )) * (t `1 )) + (1 - ((2 * 1) / (1 - 0 )))),(((2 / (1 - 0 )) * (t `2 )) + (1 - ((2 * 1) / (1 - 0 ))))]| by A6;
for x being set st x in the carrier of (TOP-REAL 2) holds
ff . x in the carrier of (TOP-REAL 2)
proof
let x be set ; :: thesis: ( x in the carrier of (TOP-REAL 2) implies ff . x in the carrier of (TOP-REAL 2) )
assume x in the carrier of (TOP-REAL 2) ; :: thesis: ff . x in the carrier of (TOP-REAL 2)
then reconsider t = x as Point of (TOP-REAL 2) ;
ff . t = |[(((2 / (1 - 0 )) * (t `1 )) + (1 - ((2 * 1) / (1 - 0 )))),(((2 / (1 - 0 )) * (t `2 )) + (1 - ((2 * 1) / (1 - 0 ))))]| by A6;
hence ff . x in the carrier of (TOP-REAL 2) ; :: thesis: verum
end;
then reconsider ff = ff as Function of (TOP-REAL 2),(TOP-REAL 2) by A6, FUNCT_2:5;
A8: ff is continuous by A7, JGRAPH_2:53;
reconsider f11 = ff | R^2-unit_square as Function of ((TOP-REAL 2) | R^2-unit_square ),(TOP-REAL 2) by PRE_TOPC:30;
A9: dom f11 = (dom ff) /\ R^2-unit_square by RELAT_1:90
.= R^2-unit_square by A6, XBOOLE_1:28 ;
A10: f11 is continuous by A8, TOPMETR:10;
ff is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 ff or not x2 in proj1 ff or not ff . x1 = ff . x2 or x1 = x2 )
assume A11: ( x1 in dom ff & x2 in dom ff & ff . x1 = ff . x2 ) ; :: thesis: x1 = x2
then reconsider p1 = x1, p2 = x2 as Point of (TOP-REAL 2) ;
A12: ff . x1 = |[(((2 / (1 - 0 )) * (p1 `1 )) + (1 - ((2 * 1) / (1 - 0 )))),(((2 / (1 - 0 )) * (p1 `2 )) + (1 - ((2 * 1) / (1 - 0 ))))]| by A6;
ff . x2 = |[(((2 / (1 - 0 )) * (p2 `1 )) + (1 - ((2 * 1) / (1 - 0 )))),(((2 / (1 - 0 )) * (p2 `2 )) + (1 - ((2 * 1) / (1 - 0 ))))]| by A6;
then ( (((2 / (1 - 0 )) * (p1 `1 )) + (1 - ((2 * 1) / (1 - 0 )))) - (1 - ((2 * 1) / (1 - 0 ))) = (((2 / (1 - 0 )) * (p2 `1 )) + (1 - ((2 * 1) / (1 - 0 )))) - (1 - ((2 * 1) / (1 - 0 ))) & (((2 / (1 - 0 )) * (p1 `2 )) + (1 - ((2 * 1) / (1 - 0 )))) - (1 - ((2 * 1) / (1 - 0 ))) = (((2 / (1 - 0 )) * (p2 `2 )) + (1 - ((2 * 1) / (1 - 0 )))) - (1 - ((2 * 1) / (1 - 0 ))) ) by A11, A12, SPPOL_2:1;
then ( ((2 / (1 - 0 )) * (p1 `1 )) / (2 / (1 - 0 )) = p2 `1 & ((2 / (1 - 0 )) * (p1 `2 )) / (2 / (1 - 0 )) = p2 `2 ) by XCMPLX_1:90;
then ( p1 `1 = p2 `1 & p1 `2 = p2 `2 ) by XCMPLX_1:90;
hence x1 = x2 by TOPREAL3:11; :: thesis: verum
end;
then A13: f11 is one-to-one by FUNCT_1:84;
set X = (TOP-REAL 2) | R^2-unit_square ;
A14: Kbd c= rng f11
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Kbd or y in rng f11 )
assume A15: y in Kbd ; :: thesis: y in rng f11
then reconsider py = y as Point of (TOP-REAL 2) ;
set t = |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]|;
A16: ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = ((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = ((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2 ) by EUCLID:56;
consider q being Point of (TOP-REAL 2) such that
A17: ( py = q & ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) ) by A1, A15;
now
per cases ( ( - 1 = py `1 & - 1 <= py `2 & py `2 <= 1 ) or ( py `1 = 1 & - 1 <= py `2 & py `2 <= 1 ) or ( - 1 = py `2 & - 1 <= py `1 & py `1 <= 1 ) or ( 1 = py `2 & - 1 <= py `1 & py `1 <= 1 ) ) by A17;
case A18: ( - 1 = py `1 & - 1 <= py `2 & py `2 <= 1 ) ; :: thesis: ( ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 >= 0 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 >= 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = 1 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 >= 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = 0 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 >= 0 ) )
then 0 - 1 <= py `2 ;
then 0 <= (py `2 ) + 1 by XREAL_1:22;
then A19: 0 / 2 <= ((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2 ;
2 - 1 >= py `2 by A18;
then 2 >= (py `2 ) + 1 by XREAL_1:21;
then 2 / 2 >= ((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2 by XREAL_1:74;
hence ( ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 >= 0 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 >= 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = 1 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 >= 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = 0 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 >= 0 ) ) by A18, A19, EUCLID:56; :: thesis: verum
end;
case A20: ( py `1 = 1 & - 1 <= py `2 & py `2 <= 1 ) ; :: thesis: ( ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 >= 0 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 >= 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = 1 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 >= 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = 0 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 >= 0 ) )
then 0 - 1 <= py `2 ;
then 0 <= (py `2 ) + 1 by XREAL_1:22;
then A21: 0 / 2 <= ((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2 ;
2 - 1 >= py `2 by A20;
then 2 >= (py `2 ) + 1 by XREAL_1:21;
then 2 / 2 >= ((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2 by XREAL_1:74;
hence ( ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 >= 0 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 >= 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = 1 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 >= 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = 0 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 >= 0 ) ) by A20, A21, EUCLID:56; :: thesis: verum
end;
case A22: ( - 1 = py `2 & - 1 <= py `1 & py `1 <= 1 ) ; :: thesis: ( ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 >= 0 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 >= 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = 1 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 >= 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = 0 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 >= 0 ) )
then 0 - 1 <= py `1 ;
then 0 <= (py `1 ) + 1 by XREAL_1:22;
then A23: 0 / 2 <= ((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2 ;
2 - 1 >= py `1 by A22;
then 2 >= (py `1 ) + 1 by XREAL_1:21;
then 2 / 2 >= ((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2 by XREAL_1:74;
hence ( ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 >= 0 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 >= 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = 1 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 >= 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = 0 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 >= 0 ) ) by A22, A23, EUCLID:56; :: thesis: verum
end;
case A24: ( 1 = py `2 & - 1 <= py `1 & py `1 <= 1 ) ; :: thesis: ( ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 >= 0 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 >= 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = 1 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 >= 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = 0 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 >= 0 ) )
then 0 - 1 <= py `1 ;
then 0 <= (py `1 ) + 1 by XREAL_1:22;
then A25: 0 / 2 <= ((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2 ;
2 - 1 >= py `1 by A24;
then 2 >= (py `1 ) + 1 by XREAL_1:21;
then 2 / 2 >= ((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2 by XREAL_1:74;
hence ( ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 >= 0 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 >= 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = 1 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 >= 0 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 = 0 ) or ( |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 = 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 <= 1 & |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 >= 0 ) ) by A24, A25, EUCLID:56; :: thesis: verum
end;
end;
end;
then A26: |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| in R^2-unit_square by TOPREAL1:20;
py = |[(((2 / (1 - 0 )) * (|[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `1 )) + (1 - ((2 * 1) / (1 - 0 )))),(((2 / (1 - 0 )) * (|[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| `2 )) + (1 - ((2 * 1) / (1 - 0 ))))]| by A16, EUCLID:57;
then py = ff . |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| by A6
.= f11 . |[(((py `1 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2),(((py `2 ) - (1 - ((2 * 1) / (1 - 0 )))) / 2)]| by A26, FUNCT_1:72 ;
hence y in rng f11 by A9, A26, FUNCT_1:def 5; :: thesis: verum
end;
rng f11 c= Kbd
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f11 or y in Kbd )
assume y in rng f11 ; :: thesis: y in Kbd
then consider x being set such that
A27: ( x in dom f11 & y = f11 . x ) by FUNCT_1:def 5;
reconsider t = x as Point of (TOP-REAL 2) by A9, A27;
consider p being Point of (TOP-REAL 2) such that
A28: ( t = p & ( ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) or ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) ) ) by A9, A27, TOPREAL1:20;
A29: y = ff . t by A9, A27, FUNCT_1:72
.= |[(((2 / (1 - 0 )) * (t `1 )) + (1 - ((2 * 1) / (1 - 0 )))),(((2 / (1 - 0 )) * (t `2 )) + (1 - ((2 * 1) / (1 - 0 ))))]| by A6 ;
then reconsider qy = y as Point of (TOP-REAL 2) ;
now
per cases ( ( t `1 = 0 & t `2 <= 1 & t `2 >= 0 ) or ( t `1 <= 1 & t `1 >= 0 & t `2 = 1 ) or ( t `1 <= 1 & t `1 >= 0 & t `2 = 0 ) or ( t `1 = 1 & t `2 <= 1 & t `2 >= 0 ) ) by A28;
suppose A30: ( t `1 = 0 & t `2 <= 1 & t `2 >= 0 ) ; :: thesis: ( ( - 1 = qy `1 & - 1 <= qy `2 & qy `2 <= 1 ) or ( qy `1 = 1 & - 1 <= qy `2 & qy `2 <= 1 ) or ( - 1 = qy `2 & - 1 <= qy `1 & qy `1 <= 1 ) or ( 1 = qy `2 & - 1 <= qy `1 & qy `1 <= 1 ) )
A31: qy `2 = (2 * (t `2 )) - 1 by A29, EUCLID:56;
2 * 0 <= 2 * (t `2 ) by A30;
then A32: 0 - 1 <= ((qy `2 ) + 1) - 1 by A31, XREAL_1:11;
2 * 1 >= 2 * (t `2 ) by A30, XREAL_1:66;
then (1 + 1) - 1 >= ((qy `2 ) + 1) - 1 by A31, XREAL_1:11;
hence ( ( - 1 = qy `1 & - 1 <= qy `2 & qy `2 <= 1 ) or ( qy `1 = 1 & - 1 <= qy `2 & qy `2 <= 1 ) or ( - 1 = qy `2 & - 1 <= qy `1 & qy `1 <= 1 ) or ( 1 = qy `2 & - 1 <= qy `1 & qy `1 <= 1 ) ) by A29, A30, A32, EUCLID:56; :: thesis: verum
end;
suppose A33: ( t `1 <= 1 & t `1 >= 0 & t `2 = 1 ) ; :: thesis: ( ( - 1 = qy `1 & - 1 <= qy `2 & qy `2 <= 1 ) or ( qy `1 = 1 & - 1 <= qy `2 & qy `2 <= 1 ) or ( - 1 = qy `2 & - 1 <= qy `1 & qy `1 <= 1 ) or ( 1 = qy `2 & - 1 <= qy `1 & qy `1 <= 1 ) )
A34: qy `1 = (2 * (t `1 )) - 1 by A29, EUCLID:56;
2 * 0 <= 2 * (t `1 ) by A33;
then A35: 0 - 1 <= ((qy `1 ) + 1) - 1 by A34, XREAL_1:11;
2 * 1 >= 2 * (t `1 ) by A33, XREAL_1:66;
then (1 + 1) - 1 >= ((qy `1 ) + 1) - 1 by A34, XREAL_1:11;
hence ( ( - 1 = qy `1 & - 1 <= qy `2 & qy `2 <= 1 ) or ( qy `1 = 1 & - 1 <= qy `2 & qy `2 <= 1 ) or ( - 1 = qy `2 & - 1 <= qy `1 & qy `1 <= 1 ) or ( 1 = qy `2 & - 1 <= qy `1 & qy `1 <= 1 ) ) by A29, A33, A35, EUCLID:56; :: thesis: verum
end;
suppose A36: ( t `1 <= 1 & t `1 >= 0 & t `2 = 0 ) ; :: thesis: ( ( - 1 = qy `1 & - 1 <= qy `2 & qy `2 <= 1 ) or ( qy `1 = 1 & - 1 <= qy `2 & qy `2 <= 1 ) or ( - 1 = qy `2 & - 1 <= qy `1 & qy `1 <= 1 ) or ( 1 = qy `2 & - 1 <= qy `1 & qy `1 <= 1 ) )
A37: qy `1 = (2 * (t `1 )) - 1 by A29, EUCLID:56;
2 * 0 <= 2 * (t `1 ) by A36;
then A38: 0 - 1 <= ((qy `1 ) + 1) - 1 by A37, XREAL_1:11;
2 * 1 >= 2 * (t `1 ) by A36, XREAL_1:66;
then (1 + 1) - 1 >= ((qy `1 ) + 1) - 1 by A37, XREAL_1:11;
hence ( ( - 1 = qy `1 & - 1 <= qy `2 & qy `2 <= 1 ) or ( qy `1 = 1 & - 1 <= qy `2 & qy `2 <= 1 ) or ( - 1 = qy `2 & - 1 <= qy `1 & qy `1 <= 1 ) or ( 1 = qy `2 & - 1 <= qy `1 & qy `1 <= 1 ) ) by A29, A36, A38, EUCLID:56; :: thesis: verum
end;
suppose A39: ( t `1 = 1 & t `2 <= 1 & t `2 >= 0 ) ; :: thesis: ( ( - 1 = qy `1 & - 1 <= qy `2 & qy `2 <= 1 ) or ( qy `1 = 1 & - 1 <= qy `2 & qy `2 <= 1 ) or ( - 1 = qy `2 & - 1 <= qy `1 & qy `1 <= 1 ) or ( 1 = qy `2 & - 1 <= qy `1 & qy `1 <= 1 ) )
A40: qy `2 = (2 * (t `2 )) - 1 by A29, EUCLID:56;
2 * 0 <= 2 * (t `2 ) by A39;
then A41: 0 - 1 <= ((qy `2 ) + 1) - 1 by A40, XREAL_1:11;
2 * 1 >= 2 * (t `2 ) by A39, XREAL_1:66;
then (1 + 1) - 1 >= ((qy `2 ) + 1) - 1 by A40, XREAL_1:11;
hence ( ( - 1 = qy `1 & - 1 <= qy `2 & qy `2 <= 1 ) or ( qy `1 = 1 & - 1 <= qy `2 & qy `2 <= 1 ) or ( - 1 = qy `2 & - 1 <= qy `1 & qy `1 <= 1 ) or ( 1 = qy `2 & - 1 <= qy `1 & qy `1 <= 1 ) ) by A29, A39, A41, EUCLID:56; :: thesis: verum
end;
end;
end;
hence y in Kbd by A1; :: thesis: verum
end;
then Kbd = rng f11 by A14, XBOOLE_0:def 10;
then consider f1 being Function of ((TOP-REAL 2) | R^2-unit_square ),((TOP-REAL 2) | Kbd) such that
A42: ( f11 = f1 & f1 is being_homeomorphism ) by A10, A13, JGRAPH_1:64;
reconsider f22 = f1 as Function of ((TOP-REAL 2) | R^2-unit_square ),((TOP-REAL 2) | Kbb) ;
reconsider g = g as Function of ((TOP-REAL 2) | Kbb),((TOP-REAL 2) | PP) ;
reconsider h = g * f22 as Function of ((TOP-REAL 2) | R^2-unit_square ),((TOP-REAL 2) | PP) ;
h is being_homeomorphism by A1, A42, TOPS_2:71;
hence P is being_simple_closed_curve by TOPREAL2:def 1; :: thesis: verum