set X = (TOP-REAL 2) | R^2-unit_square;
set b = 1;
set a = 0 ;
set v = |[1,0]|;
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
( |[1,0]| `1 = 1 & |[1,0]| `2 = 0 ) by EUCLID:52;
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 ) ) } ;
then reconsider Kbb = Kb as non empty Subset of (TOP-REAL 2) by A1;
set A = 2 / (1 - 0);
set B = 1 - ((2 * 1) / (1 - 0));
set C = 2 / (1 - 0);
set D = 1 - ((2 * 1) / (1 - 0));
reconsider Kbd = Kbb as non empty Subset of (TOP-REAL 2) ;
defpred S1[ object , object ] 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))))]|;
A3: for x being object st x in the carrier of (TOP-REAL 2) holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in the carrier of (TOP-REAL 2) implies ex y being object st S1[x,y] )
assume x in the carrier of (TOP-REAL 2) ; :: thesis: ex y being object 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 object st S1[x,y] ; :: thesis: verum
end;
ex ff being Function st
( dom ff = the carrier of (TOP-REAL 2) & ( for x being object st x in the carrier of (TOP-REAL 2) holds
S1[x,ff . x] ) ) from CLASSES1:sch 1(A3);
 then consider ff being Function such that
A4: dom ff = the carrier of (TOP-REAL 2) and
A5: for x being object 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))))]| ;
A6: 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 A5;
for x being object st x in the carrier of (TOP-REAL 2) holds
ff . x in the carrier of (TOP-REAL 2)
proof
let x be object ; :: 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 A5;
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 A4, FUNCT_2:3;
reconsider f11 = ff | R^2-unit_square as Function of ((TOP-REAL 2) | R^2-unit_square),(TOP-REAL 2) by PRE_TOPC:9;
A7: f11 is continuous by A6, JGRAPH_2:43, TOPMETR:7;
ff is one-to-one
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom ff or not x2 in dom ff or not ff . x1 = ff . x2 or x1 = x2 )
assume that
A8: ( x1 in dom ff & x2 in dom ff ) and
A9: ff . x1 = ff . x2 ; :: thesis: x1 = x2
reconsider p1 = x1, p2 = x2 as Point of (TOP-REAL 2) by A8;
A10: ( ff . x1 = |[(((2 / (1 - 0)) * (p1 `1)) + (1 - ((2 * 1) / (1 - 0)))),(((2 / (1 - 0)) * (p1 `2)) + (1 - ((2 * 1) / (1 - 0))))]| & ff . x2 = |[(((2 / (1 - 0)) * (p2 `1)) + (1 - ((2 * 1) / (1 - 0)))),(((2 / (1 - 0)) * (p2 `2)) + (1 - ((2 * 1) / (1 - 0))))]| ) by A5;
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))) by A9, SPPOL_2:1;
then ((2 / (1 - 0)) * (p1 `1)) / (2 / (1 - 0)) = p2 `1 by XCMPLX_1:89;
then A11: p1 `1 = p2 `1 by XCMPLX_1:89;
(((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 A9, A10, SPPOL_2:1;
then ((2 / (1 - 0)) * (p1 `2)) / (2 / (1 - 0)) = p2 `2 by XCMPLX_1:89;
hence x1 = x2 by A11, TOPREAL3:6, XCMPLX_1:89; :: thesis: verum
end;
then A12: f11 is one-to-one by FUNCT_1:52;
A13: dom f11 = (dom ff) /\ R^2-unit_square by RELAT_1:61
.= R^2-unit_square by A4, XBOOLE_1:28 ;
A14: Kbd c= rng f11
proof
let y be object ; :: 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: ex q being Point of (TOP-REAL 2) st
( 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 :: thesis: ( ( - 1 = py `1 & - 1 <= py `2 & py `2 <= 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 & |[(((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 ) ) ) or ( py `1 = 1 & - 1 <= py `2 & py `2 <= 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 & |[(((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 ) ) ) or ( - 1 = py `2 & - 1 <= py `1 & py `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 & |[(((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 ) ) ) or ( 1 = py `2 & - 1 <= py `1 & py `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 & |[(((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 ) ) ) )
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 A16;
case A17: ( - 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 2 - 1 >= py `2 ;
then 2 >= (py `2) + 1 by XREAL_1:19;
then A18: 2 / 2 >= ((py `2) - (1 - ((2 * 1) / (1 - 0)))) / 2 by XREAL_1:72;
0 - 1 <= py `2 by A17;
then 0 <= (py `2) + 1 by XREAL_1:20;
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 A17, A18, EUCLID:52; :: thesis: verum
end;
case A19: ( 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 2 - 1 >= py `2 ;
then 2 >= (py `2) + 1 by XREAL_1:19;
then A20: 2 / 2 >= ((py `2) - (1 - ((2 * 1) / (1 - 0)))) / 2 by XREAL_1:72;
0 - 1 <= py `2 by A19;
then 0 <= (py `2) + 1 by XREAL_1:20;
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 A19, A20, EUCLID:52; :: thesis: verum
end;
case A21: ( - 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 2 - 1 >= py `1 ;
then 2 >= (py `1) + 1 by XREAL_1:19;
then A22: 2 / 2 >= ((py `1) - (1 - ((2 * 1) / (1 - 0)))) / 2 by XREAL_1:72;
0 - 1 <= py `1 by A21;
then 0 <= (py `1) + 1 by XREAL_1:20;
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 A21, A22, EUCLID:52; :: thesis: verum
end;
case A23: ( 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 2 - 1 >= py `1 ;
then 2 >= (py `1) + 1 by XREAL_1:19;
then A24: 2 / 2 >= ((py `1) - (1 - ((2 * 1) / (1 - 0)))) / 2 by XREAL_1:72;
0 - 1 <= py `1 by A23;
then 0 <= (py `1) + 1 by XREAL_1:20;
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 A23, A24, EUCLID:52; :: thesis: verum
end;
end;
end;
then A25: |[(((py `1) - (1 - ((2 * 1) / (1 - 0)))) / 2),(((py `2) - (1 - ((2 * 1) / (1 - 0)))) / 2)]| in R^2-unit_square by TOPREAL1:14;
( |[(((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:52;
then 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 EUCLID:53;
then py = ff . |[(((py `1) - (1 - ((2 * 1) / (1 - 0)))) / 2),(((py `2) - (1 - ((2 * 1) / (1 - 0)))) / 2)]| by A5
.= f11 . |[(((py `1) - (1 - ((2 * 1) / (1 - 0)))) / 2),(((py `2) - (1 - ((2 * 1) / (1 - 0)))) / 2)]| by A25, FUNCT_1:49 ;
hence y in rng f11 by A13, A25, FUNCT_1:def 3; :: thesis: verum
end;
rng f11 c= Kbd
proof
let y be object ; :: 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 object such that
A26: x in dom f11 and
A27: y = f11 . x by FUNCT_1:def 3;
reconsider t = x as Point of (TOP-REAL 2) by A13, A26;
A28: y = ff . t by A13, A26, A27, FUNCT_1:49
.= |[(((2 / (1 - 0)) * (t `1)) + (1 - ((2 * 1) / (1 - 0)))),(((2 / (1 - 0)) * (t `2)) + (1 - ((2 * 1) / (1 - 0))))]| by A5 ;
then reconsider qy = y as Point of (TOP-REAL 2) ;
A29: ex p being Point of (TOP-REAL 2) st
( 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 A13, A26, TOPREAL1:14;
now :: 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 ) )
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 A29;
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 A28, EUCLID:52;
2 * 1 >= 2 * (t `2) by A30, XREAL_1:64;
then A32: (1 + 1) - 1 >= ((qy `2) + 1) - 1 by A31, XREAL_1:9;
0 - 1 <= ((qy `2) + 1) - 1 by A30, A31, XREAL_1:9;
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 A28, A30, A32, EUCLID:52; :: 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 A28, EUCLID:52;
2 * 1 >= 2 * (t `1) by A33, XREAL_1:64;
then A35: (1 + 1) - 1 >= ((qy `1) + 1) - 1 by A34, XREAL_1:9;
0 - 1 <= ((qy `1) + 1) - 1 by A33, A34, XREAL_1:9;
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 A28, A33, A35, EUCLID:52; :: 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 A28, EUCLID:52;
2 * 1 >= 2 * (t `1) by A36, XREAL_1:64;
then A38: (1 + 1) - 1 >= ((qy `1) + 1) - 1 by A37, XREAL_1:9;
0 - 1 <= ((qy `1) + 1) - 1 by A36, A37, XREAL_1:9;
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 A28, A36, A38, EUCLID:52; :: 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 A28, EUCLID:52;
2 * 1 >= 2 * (t `2) by A39, XREAL_1:64;
then A41: (1 + 1) - 1 >= ((qy `2) + 1) - 1 by A40, XREAL_1:9;
0 - 1 <= ((qy `2) + 1) - 1 by A39, A40, XREAL_1:9;
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 A28, A39, A41, EUCLID:52; :: thesis: verum
end;
end;
end;
hence y in Kbd by A1; :: thesis: verum
end;
then Kbd = rng f11 by A14;
then consider f1 being Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | Kbd) such that
f11 = f1 and
A42: f1 is being_homeomorphism by A7, A12, JGRAPH_1:46;
dom f = [#] ((TOP-REAL 2) | Kb) by A1, TOPS_2:def 5
.= Kb by PRE_TOPC:def 5 ;
then f . |[1,0]| in rng f by A1, A2, FUNCT_1:3;
then reconsider PP = P as non empty Subset of (TOP-REAL 2) ;
reconsider g = f as Function of ((TOP-REAL 2) | Kbb),((TOP-REAL 2) | PP) ;
reconsider g = g as Function of ((TOP-REAL 2) | Kbb),((TOP-REAL 2) | PP) ;
reconsider f22 = f1 as Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | Kbb) ;
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:57;
hence P is being_simple_closed_curve by TOPREAL2:def 1; :: thesis: verum