thus Sq_Circ is Function of (TOP-REAL 2),(TOP-REAL 2) ; :: thesis: ( 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); :: thesis: ( f = Sq_Circ implies ( rng Sq_Circ = the carrier of (TOP-REAL 2) & f is being_homeomorphism ) )
assume A2: f = Sq_Circ ; :: thesis: ( 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 set ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (TOP-REAL 2) or y in rng f )
assume y in the carrier of (TOP-REAL 2) ; :: thesis: y in rng f
then reconsider p2 = y as Point of (TOP-REAL 2) ;
set q = p2;

now

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 p2 = 0. (TOP-REAL 2) ; :: thesis: ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x )

then y = Sq_Circ . p2 by Def1;
hence ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x ) by A2, A3; :: thesis: verum

end;

case A4: ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) ; :: thesis: 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:93;

A6: now

assume that
A7: |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 = 0 and
A8: |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 = 0 ; :: thesis: contradiction
(p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = 0 by A8, EUCLID:56;
then A9: p2 `2 = 0 by A5, XCMPLX_1:6;
(p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = 0 by A7, EUCLID:56;
then p2 `1 = 0 by A5, XCMPLX_1:6;
hence contradiction by A4, A9, EUCLID:57, EUCLID:58; :: thesis: verum

end;

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:56;
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:56;
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:92;
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:90;
( ( 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:66;
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:66;
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:56, XREAL_1:66;
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:11;
(|[((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:90;
hence ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x ) by A15, A14, A10, EUCLID:57; :: thesis: 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 ) ) ) ; :: thesis: 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:93;

A18: now

assume that
A19: |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 = 0 and
|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 = 0 ; :: thesis: contradiction
(p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) = 0 by A19, EUCLID:56;
then p2 `2 = 0 by A17, XCMPLX_1:6;
hence contradiction by A16; :: thesis: verum

end;

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:56;
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:56;
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:92;
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:90;
( ( p2 `1 <= p2 `2 & - (p2 `2 ) <= p2 `1 ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2 ) ) ) by A16, JGRAPH_2:23;
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:66;
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:66;
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:56, XREAL_1:66;
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, Th14, JGRAPH_2:11;
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:90;
hence ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x ) by A24, A23, A25, EUCLID:57; :: thesis: verum

end;

end;

end;

hence y in rng f by A2, FUNCT_1:def 5; :: thesis: verum

end;

then A26: rng f = the carrier of (TOP-REAL 2) by XBOOLE_0:def 10;
A27: rng f = dom (f " ) by A2, FUNCT_1:55
.= dom (f /" ) by A2, A26, TOPS_2:def 4
.= [#] (TOP-REAL 2) by FUNCT_2:def 1 ;
then g = Sq_Circ " by A2, TOPS_2:def 4;
hence ( rng Sq_Circ = the carrier of (TOP-REAL 2) & f is being_homeomorphism ) by A2, A3, A27, Th31, Th52, TOPS_2:def 5; :: thesis: verum

end;

hence rng Sq_Circ = the carrier of (TOP-REAL 2) ; :: thesis: 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; :: thesis: verum