set K1a = { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } ;
set K0a = { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } ;
let B, K0, Kb be Subset of (TOP-REAL 2); ( B = {(0. (TOP-REAL 2))} & K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) } & 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 ) ) } implies ex f being Function of ((TOP-REAL 2) | (B `)),((TOP-REAL 2) | (B `)) st
( f is continuous & f is one-to-one & ( for t being Point of (TOP-REAL 2) st t in K0 & t <> 0. (TOP-REAL 2) holds
not f . t in K0 \/ Kb ) & ( for r being Point of (TOP-REAL 2) st not r in K0 \/ Kb holds
f . r in K0 ) & ( for s being Point of (TOP-REAL 2) st s in Kb holds
f . s = s ) ) )
assume A1:
( B = {(0. (TOP-REAL 2))} & K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) } & 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 ) ) } )
; ex f being Function of ((TOP-REAL 2) | (B `)),((TOP-REAL 2) | (B `)) st
( f is continuous & f is one-to-one & ( for t being Point of (TOP-REAL 2) st t in K0 & t <> 0. (TOP-REAL 2) holds
not f . t in K0 \/ Kb ) & ( for r being Point of (TOP-REAL 2) st not r in K0 \/ Kb holds
f . r in K0 ) & ( for s being Point of (TOP-REAL 2) st s in Kb holds
f . s = s ) )
then reconsider D = B ` as non empty Subset of (TOP-REAL 2) by Th9;
A2:
D ` = {(0. (TOP-REAL 2))}
by A1;
A3:
B ` = NonZero (TOP-REAL 2)
by A1, SUBSET_1:def 4;
A4:
for t being Point of (TOP-REAL 2) st t in K0 & t <> 0. (TOP-REAL 2) holds
not Out_In_Sq . t in K0 \/ Kb
A72:
for t being Point of (TOP-REAL 2) st not t in K0 \/ Kb holds
Out_In_Sq . t in K0
proof
let t be
Point of
(TOP-REAL 2);
( not t in K0 \/ Kb implies Out_In_Sq . t in K0 )
assume A73:
not
t in K0 \/ Kb
;
Out_In_Sq . t in K0
then A74:
not
t in K0
by XBOOLE_0:def 3;
then A75:
not
t = 0. (TOP-REAL 2)
by A1, Th3;
then
not
t in {(0. (TOP-REAL 2))}
by TARSKI:def 1;
then
t in NonZero (TOP-REAL 2)
by XBOOLE_0:def 5;
then
Out_In_Sq . t in NonZero (TOP-REAL 2)
by FUNCT_2:5;
then reconsider p4 =
Out_In_Sq . t as
Point of
(TOP-REAL 2) ;
A76:
not
t in Kb
by A73, XBOOLE_0:def 3;
now ( ( ( ( t `2 <= t `1 & - (t `1) <= t `2 ) or ( t `2 >= t `1 & t `2 <= - (t `1) ) ) & Out_In_Sq . t in K0 ) or ( not ( t `2 <= t `1 & - (t `1) <= t `2 ) & not ( t `2 >= t `1 & t `2 <= - (t `1) ) & Out_In_Sq . t in K0 ) )per cases
( ( t `2 <= t `1 & - (t `1) <= t `2 ) or ( t `2 >= t `1 & t `2 <= - (t `1) ) or ( not ( t `2 <= t `1 & - (t `1) <= t `2 ) & not ( t `2 >= t `1 & t `2 <= - (t `1) ) ) )
;
case A77:
( (
t `2 <= t `1 &
- (t `1) <= t `2 ) or (
t `2 >= t `1 &
t `2 <= - (t `1) ) )
;
Out_In_Sq . t in K0A78:
now ( ( t `1 > 0 & - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) or ( t `1 <= 0 & - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) )per cases
( t `1 > 0 or t `1 <= 0 )
;
case A79:
t `1 > 0
;
( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 )now ( ( t `2 > 0 & - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) or ( t `2 <= 0 & - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) )per cases
( t `2 > 0 or t `2 <= 0 )
;
case A80:
t `2 > 0
;
( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 )
(
- 1
>= t `1 or
t `1 >= 1 or
- 1
>= t `2 or
t `2 >= 1 )
by A1, A74;
then A81:
t `1 >= 1
by A77, A79, A80, XXREAL_0:2;
not
t `1 = 1
by A1, A76, A77;
then A82:
t `1 > 1
by A81, XXREAL_0:1;
then
t `1 < (t `1) ^2
by SQUARE_1:14;
then
t `2 < (t `1) ^2
by A77, A79, XXREAL_0:2;
then
(t `2) / (t `1) < ((t `1) ^2) / (t `1)
by A79, XREAL_1:74;
then
(t `2) / (t `1) < t `1
by A79, XCMPLX_1:89;
then A83:
((t `2) / (t `1)) / (t `1) < (t `1) / (t `1)
by A79, XREAL_1:74;
0 < (t `2) / (t `1)
by A79, A80, XREAL_1:139;
then A84:
((- 1) * (t `1)) / (t `1) < ((t `2) / (t `1)) / (t `1)
by A79, XREAL_1:74;
(t `1) / (t `1) > 1
/ (t `1)
by A82, XREAL_1:74;
hence
(
- 1
< 1
/ (t `1) & 1
/ (t `1) < 1 &
- 1
< ((t `2) / (t `1)) / (t `1) &
((t `2) / (t `1)) / (t `1) < 1 )
by A79, A84, A83, XCMPLX_1:60, XCMPLX_1:89;
verum end; case A85:
t `2 <= 0
;
( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 )
not
t `1 = 1
by A1, A76, A77;
then A87:
t `1 > 1
by A86, XXREAL_0:1;
then A88:
t `1 < (t `1) ^2
by SQUARE_1:14;
- (- (t `1)) >= - (t `2)
by A77, A79, XREAL_1:24;
then
(t `1) ^2 > - (t `2)
by A88, XXREAL_0:2;
then
((t `1) ^2) / (t `1) > (- (t `2)) / (t `1)
by A79, XREAL_1:74;
then
t `1 > - ((t `2) / (t `1))
by A79, XCMPLX_1:89;
then
- (t `1) < - (- ((t `2) / (t `1)))
by XREAL_1:24;
then A89:
((- 1) * (t `1)) / (t `1) < ((t `2) / (t `1)) / (t `1)
by A79, XREAL_1:74;
(t `1) / (t `1) > 1
/ (t `1)
by A87, XREAL_1:74;
hence
(
- 1
< 1
/ (t `1) & 1
/ (t `1) < 1 &
- 1
< ((t `2) / (t `1)) / (t `1) &
((t `2) / (t `1)) / (t `1) < 1 )
by A79, A85, A89, XCMPLX_1:60, XCMPLX_1:89;
verum end; end; end; hence
(
- 1
< 1
/ (t `1) & 1
/ (t `1) < 1 &
- 1
< ((t `2) / (t `1)) / (t `1) &
((t `2) / (t `1)) / (t `1) < 1 )
;
verum end; case A90:
t `1 <= 0
;
( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 )now ( ( t `1 = 0 & contradiction ) or ( t `1 < 0 & - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) )per cases
( t `1 = 0 or t `1 < 0 )
by A90;
case A92:
t `1 < 0
;
( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 )now ( ( t `2 > 0 & - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) or ( t `2 <= 0 & - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) )per cases
( t `2 > 0 or t `2 <= 0 )
;
case A93:
t `2 > 0
;
( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 )
(
- 1
>= t `1 or
t `1 >= 1 or
- 1
>= t `2 or
t `2 >= 1 )
by A1, A74;
then
(
t `1 <= - 1 or 1
<= - (t `1) )
by A77, A92, XXREAL_0:2;
then A94:
(
t `1 <= - 1 or
- 1
>= - (- (t `1)) )
by XREAL_1:24;
not
t `1 = - 1
by A1, A76, A77;
then A95:
t `1 < - 1
by A94, XXREAL_0:1;
then
(t `1) / (t `1) > (- 1) / (t `1)
by XREAL_1:75;
then A96:
- ((t `1) / (t `1)) < - ((- 1) / (t `1))
by XREAL_1:24;
- (t `1) < (t `1) ^2
by A95, SQUARE_1:46;
then
t `2 < (t `1) ^2
by A77, A92, XXREAL_0:2;
then
(t `2) / (t `1) > ((t `1) ^2) / (t `1)
by A92, XREAL_1:75;
then
(t `2) / (t `1) > t `1
by A92, XCMPLX_1:89;
then A97:
((t `2) / (t `1)) / (t `1) < (t `1) / (t `1)
by A92, XREAL_1:75;
0 > (t `2) / (t `1)
by A92, A93, XREAL_1:142;
then
((- 1) * (t `1)) / (t `1) < ((t `2) / (t `1)) / (t `1)
by A92, XREAL_1:75;
hence
(
- 1
< 1
/ (t `1) & 1
/ (t `1) < 1 &
- 1
< ((t `2) / (t `1)) / (t `1) &
((t `2) / (t `1)) / (t `1) < 1 )
by A92, A96, A97, XCMPLX_1:60;
verum end; case A98:
t `2 <= 0
;
( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 )then
(
- 1
>= t `1 or
- 1
>= t `2 )
by A1, A74, A92;
then A99:
t `1 <= - 1
by A77, A92, XXREAL_0:2;
not
t `1 = - 1
by A1, A76, A77;
then A100:
t `1 < - 1
by A99, XXREAL_0:1;
then A101:
- (t `1) < (t `1) ^2
by SQUARE_1:46;
t `1 <= t `2
by A77, A92;
then
- (t `1) >= - (t `2)
by XREAL_1:24;
then
(t `1) ^2 > - (t `2)
by A101, XXREAL_0:2;
then
((t `1) ^2) / (t `1) < (- (t `2)) / (t `1)
by A92, XREAL_1:75;
then
t `1 < - ((t `2) / (t `1))
by A92, XCMPLX_1:89;
then
- (t `1) > - (- ((t `2) / (t `1)))
by XREAL_1:24;
then A102:
((- 1) * (t `1)) / (t `1) < ((t `2) / (t `1)) / (t `1)
by A92, XREAL_1:75;
(t `1) / (t `1) > (- 1) / (t `1)
by A100, XREAL_1:75;
then
1
> (- 1) / (t `1)
by A92, XCMPLX_1:60;
then
- 1
< - ((- 1) / (t `1))
by XREAL_1:24;
hence
(
- 1
< 1
/ (t `1) & 1
/ (t `1) < 1 &
- 1
< ((t `2) / (t `1)) / (t `1) &
((t `2) / (t `1)) / (t `1) < 1 )
by A92, A98, A102, XCMPLX_1:89;
verum end; end; end; hence
(
- 1
< 1
/ (t `1) & 1
/ (t `1) < 1 &
- 1
< ((t `2) / (t `1)) / (t `1) &
((t `2) / (t `1)) / (t `1) < 1 )
;
verum end; end; end; hence
(
- 1
< 1
/ (t `1) & 1
/ (t `1) < 1 &
- 1
< ((t `2) / (t `1)) / (t `1) &
((t `2) / (t `1)) / (t `1) < 1 )
;
verum end; end; end;
Out_In_Sq . t = |[(1 / (t `1)),(((t `2) / (t `1)) / (t `1))]|
by A75, A77, Def1;
then
(
p4 `1 = 1
/ (t `1) &
p4 `2 = ((t `2) / (t `1)) / (t `1) )
by EUCLID:52;
hence
Out_In_Sq . t in K0
by A1, A78;
verum end; case A103:
( not (
t `2 <= t `1 &
- (t `1) <= t `2 ) & not (
t `2 >= t `1 &
t `2 <= - (t `1) ) )
;
Out_In_Sq . t in K0then A104:
( (
t `1 <= t `2 &
- (t `2) <= t `1 ) or (
t `1 >= t `2 &
t `1 <= - (t `2) ) )
by Th13;
A105:
now ( ( t `2 > 0 & - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) or ( t `2 <= 0 & - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) )per cases
( t `2 > 0 or t `2 <= 0 )
;
case A106:
t `2 > 0
;
( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 )now ( ( t `1 > 0 & - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) or ( t `1 <= 0 & - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) )per cases
( t `1 > 0 or t `1 <= 0 )
;
case A107:
t `1 > 0
;
( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 )A108:
(
- 1
>= t `2 or
t `2 >= 1 or
- 1
>= t `1 or
t `1 >= 1 )
by A1, A74;
not
t `2 = 1
by A1, A76, A103, A107;
then A109:
t `2 > 1
by A103, A106, A107, A108, XXREAL_0:1, XXREAL_0:2;
then
t `2 < (t `2) ^2
by SQUARE_1:14;
then
t `1 < (t `2) ^2
by A103, A106, XXREAL_0:2;
then
(t `1) / (t `2) < ((t `2) ^2) / (t `2)
by A106, XREAL_1:74;
then
(t `1) / (t `2) < t `2
by A106, XCMPLX_1:89;
then A110:
((t `1) / (t `2)) / (t `2) < (t `2) / (t `2)
by A106, XREAL_1:74;
0 < (t `1) / (t `2)
by A106, A107, XREAL_1:139;
then A111:
((- 1) * (t `2)) / (t `2) < ((t `1) / (t `2)) / (t `2)
by A106, XREAL_1:74;
(t `2) / (t `2) > 1
/ (t `2)
by A109, XREAL_1:74;
hence
(
- 1
< 1
/ (t `2) & 1
/ (t `2) < 1 &
- 1
< ((t `1) / (t `2)) / (t `2) &
((t `1) / (t `2)) / (t `2) < 1 )
by A106, A111, A110, XCMPLX_1:60, XCMPLX_1:89;
verum end; case A112:
t `1 <= 0
;
( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 )
not
t `2 = 1
by A1, A76, A104;
then A114:
t `2 > 1
by A113, XXREAL_0:1;
then
t `2 < (t `2) ^2
by SQUARE_1:14;
then
(t `2) ^2 > - (t `1)
by A103, A106, XXREAL_0:2;
then
((t `2) ^2) / (t `2) > (- (t `1)) / (t `2)
by A106, XREAL_1:74;
then
t `2 > - ((t `1) / (t `2))
by A106, XCMPLX_1:89;
then
- (t `2) < - (- ((t `1) / (t `2)))
by XREAL_1:24;
then A115:
((- 1) * (t `2)) / (t `2) < ((t `1) / (t `2)) / (t `2)
by A106, XREAL_1:74;
(t `2) / (t `2) > 1
/ (t `2)
by A114, XREAL_1:74;
hence
(
- 1
< 1
/ (t `2) & 1
/ (t `2) < 1 &
- 1
< ((t `1) / (t `2)) / (t `2) &
((t `1) / (t `2)) / (t `2) < 1 )
by A106, A112, A115, XCMPLX_1:60, XCMPLX_1:89;
verum end; end; end; hence
(
- 1
< 1
/ (t `2) & 1
/ (t `2) < 1 &
- 1
< ((t `1) / (t `2)) / (t `2) &
((t `1) / (t `2)) / (t `2) < 1 )
;
verum end; case A116:
t `2 <= 0
;
( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 )then A117:
t `2 < 0
by A103;
A118:
(
t `1 <= t `2 or
t `1 <= - (t `2) )
by A103, Th13;
now ( ( t `1 > 0 & - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) or ( t `1 <= 0 & - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) )per cases
( t `1 > 0 or t `1 <= 0 )
;
case A119:
t `1 > 0
;
( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 )
(
- 1
>= t `2 or
t `2 >= 1 or
- 1
>= t `1 or
t `1 >= 1 )
by A1, A74;
then
(
t `2 <= - 1 or 1
<= - (t `2) )
by A104, A116, XXREAL_0:2;
then A120:
(
t `2 <= - 1 or
- 1
>= - (- (t `2)) )
by XREAL_1:24;
not
t `2 = - 1
by A1, A76, A104;
then A121:
t `2 < - 1
by A120, XXREAL_0:1;
then
(t `2) / (t `2) > (- 1) / (t `2)
by XREAL_1:75;
then A122:
- ((t `2) / (t `2)) < - ((- 1) / (t `2))
by XREAL_1:24;
- (t `2) < (t `2) ^2
by A121, SQUARE_1:46;
then
t `1 < (t `2) ^2
by A116, A118, XXREAL_0:2;
then
(t `1) / (t `2) > ((t `2) ^2) / (t `2)
by A117, XREAL_1:75;
then
(t `1) / (t `2) > t `2
by A117, XCMPLX_1:89;
then A123:
((t `1) / (t `2)) / (t `2) < (t `2) / (t `2)
by A117, XREAL_1:75;
0 > (t `1) / (t `2)
by A117, A119, XREAL_1:142;
then
((- 1) * (t `2)) / (t `2) < ((t `1) / (t `2)) / (t `2)
by A117, XREAL_1:75;
hence
(
- 1
< 1
/ (t `2) & 1
/ (t `2) < 1 &
- 1
< ((t `1) / (t `2)) / (t `2) &
((t `1) / (t `2)) / (t `2) < 1 )
by A117, A122, A123, XCMPLX_1:60;
verum end; case A124:
t `1 <= 0
;
( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 )A125:
not
t `2 = - 1
by A1, A76, A104;
(
- 1
>= t `2 or
- 1
>= t `1 )
by A1, A74, A116, A124;
then A126:
t `2 < - 1
by A103, A116, A125, XXREAL_0:1, XXREAL_0:2;
then A127:
- (t `2) < (t `2) ^2
by SQUARE_1:46;
- (t `2) >= - (t `1)
by A103, A116, XREAL_1:24;
then
(t `2) ^2 > - (t `1)
by A127, XXREAL_0:2;
then
((t `2) ^2) / (t `2) < (- (t `1)) / (t `2)
by A117, XREAL_1:75;
then
t `2 < - ((t `1) / (t `2))
by A117, XCMPLX_1:89;
then
- (t `2) > - (- ((t `1) / (t `2)))
by XREAL_1:24;
then A128:
((- 1) * (t `2)) / (t `2) < ((t `1) / (t `2)) / (t `2)
by A117, XREAL_1:75;
(t `2) / (t `2) > (- 1) / (t `2)
by A126, XREAL_1:75;
then
1
> (- 1) / (t `2)
by A117, XCMPLX_1:60;
then
- 1
< - ((- 1) / (t `2))
by XREAL_1:24;
hence
(
- 1
< 1
/ (t `2) & 1
/ (t `2) < 1 &
- 1
< ((t `1) / (t `2)) / (t `2) &
((t `1) / (t `2)) / (t `2) < 1 )
by A103, A116, A124, A128, XCMPLX_1:89;
verum end; end; end; hence
(
- 1
< 1
/ (t `2) & 1
/ (t `2) < 1 &
- 1
< ((t `1) / (t `2)) / (t `2) &
((t `1) / (t `2)) / (t `2) < 1 )
;
verum end; end; end;
Out_In_Sq . t = |[(((t `1) / (t `2)) / (t `2)),(1 / (t `2))]|
by A75, A103, Def1;
then
(
p4 `2 = 1
/ (t `2) &
p4 `1 = ((t `1) / (t `2)) / (t `2) )
by EUCLID:52;
hence
Out_In_Sq . t in K0
by A1, A105;
verum end; end; end;
hence
Out_In_Sq . t in K0
;
verum
end;
A129:
D = NonZero (TOP-REAL 2)
by A1, SUBSET_1:def 4;
for x1, x2 being object st x1 in dom Out_In_Sq & x2 in dom Out_In_Sq & Out_In_Sq . x1 = Out_In_Sq . x2 holds
x1 = x2
proof
A130:
{ p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } c= D
A132:
1.REAL 2
<> 0. (TOP-REAL 2)
by Lm1, REVROT_1:19;
( (
(1.REAL 2) `1 <= (1.REAL 2) `2 &
- ((1.REAL 2) `2) <= (1.REAL 2) `1 ) or (
(1.REAL 2) `1 >= (1.REAL 2) `2 &
(1.REAL 2) `1 <= - ((1.REAL 2) `2) ) )
by Th5;
then A133:
1.REAL 2
in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) }
by A132;
the
carrier of
((TOP-REAL 2) | D) =
[#] ((TOP-REAL 2) | D)
.=
D
by PRE_TOPC:def 5
;
then reconsider K11 =
{ p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } as non
empty Subset of
((TOP-REAL 2) | D) by A133, A130;
reconsider K01 =
{ p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } as non
empty Subset of
((TOP-REAL 2) | D) by A2, Th17;
let x1,
x2 be
object ;
( x1 in dom Out_In_Sq & x2 in dom Out_In_Sq & Out_In_Sq . x1 = Out_In_Sq . x2 implies x1 = x2 )
assume that A134:
x1 in dom Out_In_Sq
and A135:
x2 in dom Out_In_Sq
and A136:
Out_In_Sq . x1 = Out_In_Sq . x2
;
x1 = x2
NonZero (TOP-REAL 2) <> {}
by Th9;
then A137:
dom Out_In_Sq = NonZero (TOP-REAL 2)
by FUNCT_2:def 1;
then A138:
x2 in D
by A1, A135, SUBSET_1:def 4;
reconsider p1 =
x1,
p2 =
x2 as
Point of
(TOP-REAL 2) by A134, A135, XBOOLE_0:def 5;
A139:
D c= K01 \/ K11
A141:
x1 in D
by A1, A134, A137, SUBSET_1:def 4;
now ( ( x1 in K01 & x1 = x2 ) or ( x1 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } & x1 = x2 ) )per cases
( x1 in K01 or x1 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } )
by A139, A141, XBOOLE_0:def 3;
case
x1 in K01
;
x1 = x2then A142:
ex
p7 being
Point of
(TOP-REAL 2) st
(
p1 = p7 & ( (
p7 `2 <= p7 `1 &
- (p7 `1) <= p7 `2 ) or (
p7 `2 >= p7 `1 &
p7 `2 <= - (p7 `1) ) ) &
p7 <> 0. (TOP-REAL 2) )
;
then A143:
Out_In_Sq . p1 = |[(1 / (p1 `1)),(((p1 `2) / (p1 `1)) / (p1 `1))]|
by Def1;
now ( ( x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } & x1 = x2 ) or ( x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } & not x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } & contradiction ) )per cases
( x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } or ( x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } & not x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } ) )
by A139, A138, XBOOLE_0:def 3;
case
x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) }
;
x1 = x2then
ex
p8 being
Point of
(TOP-REAL 2) st
(
p2 = p8 & ( (
p8 `2 <= p8 `1 &
- (p8 `1) <= p8 `2 ) or (
p8 `2 >= p8 `1 &
p8 `2 <= - (p8 `1) ) ) &
p8 <> 0. (TOP-REAL 2) )
;
then A144:
|[(1 / (p2 `1)),(((p2 `2) / (p2 `1)) / (p2 `1))]| = |[(1 / (p1 `1)),(((p1 `2) / (p1 `1)) / (p1 `1))]|
by A136, A143, Def1;
A145:
p1 = |[(p1 `1),(p1 `2)]|
by EUCLID:53;
set qq =
|[(1 / (p2 `1)),(((p2 `2) / (p2 `1)) / (p2 `1))]|;
A146:
(1 / (p1 `1)) " =
((p1 `1) ") "
.=
p1 `1
;
|[(1 / (p2 `1)),(((p2 `2) / (p2 `1)) / (p2 `1))]| `1 = 1
/ (p2 `1)
by EUCLID:52;
then A149:
1
/ (p1 `1) = 1
/ (p2 `1)
by A144, EUCLID:52;
|[(1 / (p2 `1)),(((p2 `2) / (p2 `1)) / (p2 `1))]| `2 = ((p2 `2) / (p2 `1)) / (p2 `1)
by EUCLID:52;
then
(p1 `2) / (p1 `1) = (p2 `2) / (p1 `1)
by A144, A149, A146, A147, EUCLID:52, XCMPLX_1:53;
then
p1 `2 = p2 `2
by A147, XCMPLX_1:53;
hence
x1 = x2
by A149, A146, A145, EUCLID:53;
verum end; case A150:
(
x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } & not
x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } )
;
contradictionA159:
ex
p8 being
Point of
(TOP-REAL 2) st
(
p2 = p8 & ( (
p8 `1 <= p8 `2 &
- (p8 `2) <= p8 `1 ) or (
p8 `1 >= p8 `2 &
p8 `1 <= - (p8 `2) ) ) &
p8 <> 0. (TOP-REAL 2) )
by A150;
( ( not (
p2 `2 <= p2 `1 &
- (p2 `1) <= p2 `2 ) & not (
p2 `2 >= p2 `1 &
p2 `2 <= - (p2 `1) ) ) or not
p2 <> 0. (TOP-REAL 2) )
by A150;
then A162:
Out_In_Sq . p2 = |[(((p2 `1) / (p2 `2)) / (p2 `2)),(1 / (p2 `2))]|
by A159, Def1;
then
((p1 `2) / (p1 `1)) / (p1 `1) = 1
/ (p2 `2)
by A136, A143, SPPOL_2:1;
then A163:
(p1 `2) / (p1 `1) =
(1 / (p2 `2)) * (p1 `1)
by A151, XCMPLX_1:87
.=
(p1 `1) / (p2 `2)
;
1
/ (p1 `1) = ((p2 `1) / (p2 `2)) / (p2 `2)
by A136, A143, A162, SPPOL_2:1;
then A164:
(p2 `1) / (p2 `2) =
(1 / (p1 `1)) * (p2 `2)
by A160, XCMPLX_1:87
.=
(p2 `2) / (p1 `1)
;
then A165:
((p2 `1) / (p2 `2)) * ((p1 `2) / (p1 `1)) = 1
by A160, A151, A163, XCMPLX_1:112;
A166:
(((p2 `1) / (p2 `2)) * ((p1 `2) / (p1 `1))) * (p1 `1) = 1
* (p1 `1)
by A160, A151, A164, A163, XCMPLX_1:112;
then A167:
p1 `2 <> 0
by A151;
A168:
ex
p9 being
Point of
(TOP-REAL 2) st
(
p2 = p9 & ( (
p9 `1 <= p9 `2 &
- (p9 `2) <= p9 `1 ) or (
p9 `1 >= p9 `2 &
p9 `1 <= - (p9 `2) ) ) &
p9 <> 0. (TOP-REAL 2) )
by A150;
((p2 `1) / (p2 `2)) * (((p1 `2) / (p1 `1)) * (p1 `1)) = p1 `1
by A166;
then A172:
((p2 `1) / (p2 `2)) * (p1 `2) = p1 `1
by A151, XCMPLX_1:87;
then A173:
(p2 `1) / (p2 `2) = (p1 `1) / (p1 `2)
by A167, XCMPLX_1:89;
now ( ( 0 <= (p2 `1) / (p2 `2) & contradiction ) or ( 0 > (p2 `1) / (p2 `2) & contradiction ) )end; hence
contradiction
;
verum end; end; end; hence
x1 = x2
;
verum end; case
x1 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) }
;
x1 = x2then A179:
ex
p7 being
Point of
(TOP-REAL 2) st
(
p1 = p7 & ( (
p7 `1 <= p7 `2 &
- (p7 `2) <= p7 `1 ) or (
p7 `1 >= p7 `2 &
p7 `1 <= - (p7 `2) ) ) &
p7 <> 0. (TOP-REAL 2) )
;
then A180:
Out_In_Sq . p1 = |[(((p1 `1) / (p1 `2)) / (p1 `2)),(1 / (p1 `2))]|
by Th14;
now ( ( x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } & x1 = x2 ) or ( x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } & not x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } & contradiction ) )per cases
( x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } or ( x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } & not x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } ) )
by A139, A138, XBOOLE_0:def 3;
case
x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) }
;
x1 = x2then
ex
p8 being
Point of
(TOP-REAL 2) st
(
p2 = p8 & ( (
p8 `1 <= p8 `2 &
- (p8 `2) <= p8 `1 ) or (
p8 `1 >= p8 `2 &
p8 `1 <= - (p8 `2) ) ) &
p8 <> 0. (TOP-REAL 2) )
;
then A181:
|[(((p2 `1) / (p2 `2)) / (p2 `2)),(1 / (p2 `2))]| = |[(((p1 `1) / (p1 `2)) / (p1 `2)),(1 / (p1 `2))]|
by A136, A180, Th14;
A182:
p1 = |[(p1 `1),(p1 `2)]|
by EUCLID:53;
set qq =
|[(((p2 `1) / (p2 `2)) / (p2 `2)),(1 / (p2 `2))]|;
A183:
(1 / (p1 `2)) " =
((p1 `2) ") "
.=
p1 `2
;
|[(((p2 `1) / (p2 `2)) / (p2 `2)),(1 / (p2 `2))]| `2 = 1
/ (p2 `2)
by EUCLID:52;
then A186:
1
/ (p1 `2) = 1
/ (p2 `2)
by A181, EUCLID:52;
|[(((p2 `1) / (p2 `2)) / (p2 `2)),(1 / (p2 `2))]| `1 = ((p2 `1) / (p2 `2)) / (p2 `2)
by EUCLID:52;
then
(p1 `1) / (p1 `2) = (p2 `1) / (p1 `2)
by A181, A186, A183, A184, EUCLID:52, XCMPLX_1:53;
then
p1 `1 = p2 `1
by A184, XCMPLX_1:53;
hence
x1 = x2
by A186, A183, A182, EUCLID:53;
verum end; case A187:
(
x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } & not
x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } )
;
contradictionA196:
ex
p8 being
Point of
(TOP-REAL 2) st
(
p2 = p8 & ( (
p8 `2 <= p8 `1 &
- (p8 `1) <= p8 `2 ) or (
p8 `2 >= p8 `1 &
p8 `2 <= - (p8 `1) ) ) &
p8 <> 0. (TOP-REAL 2) )
by A187;
A199:
ex
p9 being
Point of
(TOP-REAL 2) st
(
p2 = p9 & ( (
p9 `2 <= p9 `1 &
- (p9 `1) <= p9 `2 ) or (
p9 `2 >= p9 `1 &
p9 `2 <= - (p9 `1) ) ) &
p9 <> 0. (TOP-REAL 2) )
by A187;
A203:
Out_In_Sq . p2 = |[(1 / (p2 `1)),(((p2 `2) / (p2 `1)) / (p2 `1))]|
by A196, Def1;
then
1
/ (p1 `2) = ((p2 `2) / (p2 `1)) / (p2 `1)
by A136, A180, SPPOL_2:1;
then A204:
(p2 `2) / (p2 `1) =
(1 / (p1 `2)) * (p2 `1)
by A197, XCMPLX_1:87
.=
(p2 `1) / (p1 `2)
;
((p1 `1) / (p1 `2)) / (p1 `2) = 1
/ (p2 `1)
by A136, A180, A203, SPPOL_2:1;
then (p1 `1) / (p1 `2) =
(1 / (p2 `1)) * (p1 `2)
by A188, XCMPLX_1:87
.=
(p1 `2) / (p2 `1)
;
then A205:
((p2 `2) / (p2 `1)) * ((p1 `1) / (p1 `2)) = 1
by A197, A188, A204, XCMPLX_1:112;
then A206:
p1 `1 <> 0
;
(((p2 `2) / (p2 `1)) * ((p1 `1) / (p1 `2))) * (p1 `2) = p1 `2
by A205;
then
((p2 `2) / (p2 `1)) * (((p1 `1) / (p1 `2)) * (p1 `2)) = p1 `2
;
then
((p2 `2) / (p2 `1)) * (p1 `1) = p1 `2
by A188, XCMPLX_1:87;
then A207:
(p2 `2) / (p2 `1) = (p1 `2) / (p1 `1)
by A206, XCMPLX_1:89;
now ( ( 0 <= (p2 `2) / (p2 `1) & contradiction ) or ( 0 > (p2 `2) / (p2 `1) & contradiction ) )end; hence
contradiction
;
verum end; end; end; hence
x1 = x2
;
verum end; end; end;
hence
x1 = x2
;
verum
end;
then A213:
Out_In_Sq is one-to-one
by FUNCT_1:def 4;
A214:
for s being Point of (TOP-REAL 2) st s in Kb holds
Out_In_Sq . s = s
ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = Out_In_Sq & h is continuous )
by A2, Th40;
hence
ex f being Function of ((TOP-REAL 2) | (B `)),((TOP-REAL 2) | (B `)) st
( f is continuous & f is one-to-one & ( for t being Point of (TOP-REAL 2) st t in K0 & t <> 0. (TOP-REAL 2) holds
not f . t in K0 \/ Kb ) & ( for r being Point of (TOP-REAL 2) st not r in K0 \/ Kb holds
f . r in K0 ) & ( for s being Point of (TOP-REAL 2) st s in Kb holds
f . s = s ) )
by A213, A4, A72, A214; verum