thus
Sq_Circ is Function of (TOP-REAL 2),(TOP-REAL 2)
; ( rng Sq_Circ = the carrier of (TOP-REAL 2) & ( for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = Sq_Circ holds
f is being_homeomorphism ) )
A1:
for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = Sq_Circ holds
( rng Sq_Circ = the carrier of (TOP-REAL 2) & f is being_homeomorphism )
proof
let f be
Function of
(TOP-REAL 2),
(TOP-REAL 2);
( f = Sq_Circ implies ( rng Sq_Circ = the carrier of (TOP-REAL 2) & f is being_homeomorphism ) )
assume A2:
f = Sq_Circ
;
( rng Sq_Circ = the carrier of (TOP-REAL 2) & f is being_homeomorphism )
reconsider g =
f /" as
Function of
(TOP-REAL 2),
(TOP-REAL 2) ;
A3:
dom f = the
carrier of
(TOP-REAL 2)
by FUNCT_2:def 1;
the
carrier of
(TOP-REAL 2) c= rng f
proof
let y be
object ;
TARSKI:def 3 ( not y in the carrier of (TOP-REAL 2) or y in rng f )
assume
y in the
carrier of
(TOP-REAL 2)
;
y in rng f
then reconsider p2 =
y as
Point of
(TOP-REAL 2) ;
set q =
p2;
now ( ( p2 = 0. (TOP-REAL 2) & ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x ) ) or ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ) & ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x ) ) or ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) & ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x ) ) )per cases
( p2 = 0. (TOP-REAL 2) or ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ) ) or ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ) )
;
case A4:
(
p2 <> 0. (TOP-REAL 2) & ( (
p2 `2 <= p2 `1 &
- (p2 `1) <= p2 `2 ) or (
p2 `2 >= p2 `1 &
p2 `2 <= - (p2 `1) ) ) )
;
ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x )set px =
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]|;
A5:
sqrt (1 + (((p2 `2) / (p2 `1)) ^2)) > 0
by Lm1, SQUARE_1:25;
A10:
dom Sq_Circ = the
carrier of
(TOP-REAL 2)
by FUNCT_2:def 1;
A11:
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1 = (p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))
by EUCLID:52;
A12:
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 = (p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))
by EUCLID:52;
then A13:
(|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) / (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) = (p2 `2) / (p2 `1)
by A11, A5, XCMPLX_1:91;
then A14:
(|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) / (sqrt (1 + (((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) / (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1)) ^2))) = p2 `2
by A12, A5, XCMPLX_1:89;
( (
p2 `2 <= p2 `1 &
- (p2 `1) <= p2 `2 ) or (
p2 `2 >= p2 `1 &
(p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) <= (- (p2 `1)) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) ) )
by A4, A5, XREAL_1:64;
then
( (
p2 `2 <= p2 `1 &
(- (p2 `1)) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) <= (p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) ) or (
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 >= |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1 &
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 <= - (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ) )
by A11, A12, A5, XREAL_1:64;
then
( (
(p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) <= (p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) &
- (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) <= |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 ) or (
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 >= |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1 &
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 <= - (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ) )
by A11, A5, EUCLID:52, XREAL_1:64;
then A15:
Sq_Circ . |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| = |[((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) / (sqrt (1 + (((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) / (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1)) ^2)))),((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) / (sqrt (1 + (((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) / (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1)) ^2))))]|
by A11, A12, A6, Def1, JGRAPH_2:3;
(|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) / (sqrt (1 + (((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) / (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1)) ^2))) = p2 `1
by A11, A5, A13, XCMPLX_1:89;
hence
ex
x being
set st
(
x in dom Sq_Circ &
y = Sq_Circ . x )
by A15, A14, A10, EUCLID:53;
verum end; case A16:
(
p2 <> 0. (TOP-REAL 2) & not (
p2 `2 <= p2 `1 &
- (p2 `1) <= p2 `2 ) & not (
p2 `2 >= p2 `1 &
p2 `2 <= - (p2 `1) ) )
;
ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x )set px =
|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]|;
A17:
sqrt (1 + (((p2 `1) / (p2 `2)) ^2)) > 0
by Lm1, SQUARE_1:25;
A20:
|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2 = (p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))
by EUCLID:52;
A21:
|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 = (p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))
by EUCLID:52;
then A22:
(|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) / (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) = (p2 `1) / (p2 `2)
by A20, A17, XCMPLX_1:91;
then A23:
(|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) / (sqrt (1 + (((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) / (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2)) ^2))) = p2 `1
by A21, A17, XCMPLX_1:89;
( (
p2 `1 <= p2 `2 &
- (p2 `2) <= p2 `1 ) or (
p2 `1 >= p2 `2 &
p2 `1 <= - (p2 `2) ) )
by A16, JGRAPH_2:13;
then
( (
p2 `1 <= p2 `2 &
- (p2 `2) <= p2 `1 ) or (
p2 `1 >= p2 `2 &
(p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) <= (- (p2 `2)) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) ) )
by A17, XREAL_1:64;
then
( (
p2 `1 <= p2 `2 &
(- (p2 `2)) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) <= (p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) ) or (
|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 >= |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2 &
|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 <= - (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) ) )
by A20, A21, A17, XREAL_1:64;
then
( (
(p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) <= (p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) &
- (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) <= |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 ) or (
|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 >= |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2 &
|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 <= - (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) ) )
by A20, A17, EUCLID:52, XREAL_1:64;
then A24:
Sq_Circ . |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| = |[((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) / (sqrt (1 + (((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) / (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2)) ^2)))),((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) / (sqrt (1 + (((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) / (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2)) ^2))))]|
by A20, A21, A18, Th4, JGRAPH_2:3;
A25:
dom Sq_Circ = the
carrier of
(TOP-REAL 2)
by FUNCT_2:def 1;
(|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) / (sqrt (1 + (((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) / (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2)) ^2))) = p2 `2
by A20, A17, A22, XCMPLX_1:89;
hence
ex
x being
set st
(
x in dom Sq_Circ &
y = Sq_Circ . x )
by A24, A23, A25, EUCLID:53;
verum end; end; end;
hence
y in rng f
by A2, FUNCT_1:def 3;
verum
end;
then
rng f = the
carrier of
(TOP-REAL 2)
;
then A26:
f is
onto
by FUNCT_2:def 3;
A27:
rng f =
dom (f ")
by A2, FUNCT_1:33
.=
dom (f /")
by A2, A26, TOPS_2:def 4
.=
[#] (TOP-REAL 2)
by FUNCT_2:def 1
;
g = Sq_Circ "
by A26, A2, TOPS_2:def 4;
hence
(
rng Sq_Circ = the
carrier of
(TOP-REAL 2) &
f is
being_homeomorphism )
by A2, A3, A27, Th21, Th42, TOPS_2:def 5;
verum
end;
hence
rng Sq_Circ = the carrier of (TOP-REAL 2)
; for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = Sq_Circ holds
f is being_homeomorphism
thus
for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = Sq_Circ holds
f is being_homeomorphism
by A1; verum