A1: the carrier of (TOP-REAL 2) c= rng Sq_Circ

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (TOP-REAL 2) or y in rng Sq_Circ )
assume y in the carrier of (TOP-REAL 2) ; :: thesis: y in rng Sq_Circ
then reconsider py = y as Point of (TOP-REAL 2) ;
A2: dom Sq_Circ = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;

now

per cases ( py = 0. (TOP-REAL 2) or ( ( ( py `2 <= py `1 & - (py `1 ) <= py `2 ) or ( py `2 >= py `1 & py `2 <= - (py `1 ) ) ) & py <> 0. (TOP-REAL 2) ) or ( not ( py `2 <= py `1 & - (py `1 ) <= py `2 ) & not ( py `2 >= py `1 & py `2 <= - (py `1 ) ) & py <> 0. (TOP-REAL 2) ) ) ;

case py = 0. (TOP-REAL 2) ; :: thesis: ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x )

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

end;

case A3: ( ( ( py `2 <= py `1 & - (py `1 ) <= py `2 ) or ( py `2 >= py `1 & py `2 <= - (py `1 ) ) ) & py <> 0. (TOP-REAL 2) ) ; :: thesis: ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x )

set q = py;
set px = |[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]|;
A4: sqrt (1 + (((py `2 ) / (py `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;

A5: now

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

end;

A9: dom Sq_Circ = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A10: |[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `1 = (py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) by EUCLID:56;
A11: |[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `2 = (py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) by EUCLID:56;
then A12: (|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `2 ) / (|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `1 ) = (py `2 ) / (py `1 ) by A10, A4, XCMPLX_1:92;
then A13: (|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `2 ) / (sqrt (1 + (((|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `2 ) / (|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `1 )) ^2 ))) = py `2 by A11, A4, XCMPLX_1:90;
( ( py `2 <= py `1 & - (py `1 ) <= py `2 ) or ( py `2 >= py `1 & (py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) <= (- (py `1 )) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) ) ) by A3, A4, XREAL_1:66;
then ( ( py `2 <= py `1 & (- (py `1 )) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) <= (py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) ) or ( |[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `2 >= |[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `1 & |[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `2 <= - (|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `1 ) ) ) by A10, A11, A4, XREAL_1:66;
then ( ( (py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) <= (py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))) & - (|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `1 ) <= |[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `2 ) or ( |[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `2 >= |[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `1 & |[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `2 <= - (|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `1 ) ) ) by A10, A4, EUCLID:56, XREAL_1:66;
then A14: Sq_Circ . |[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| = |[((|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `1 ) / (sqrt (1 + (((|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `2 ) / (|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `1 )) ^2 )))),((|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `2 ) / (sqrt (1 + (((|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `2 ) / (|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `1 )) ^2 ))))]| by A10, A11, A5, Def1, JGRAPH_2:11;
(|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `1 ) / (sqrt (1 + (((|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `2 ) / (|[((py `1 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `2 ) / (py `1 )) ^2 ))))]| `1 )) ^2 ))) = py `1 by A10, A4, A12, XCMPLX_1:90;
hence ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x ) by A14, A13, A9, EUCLID:57; :: thesis: verum

end;

case A15: ( not ( py `2 <= py `1 & - (py `1 ) <= py `2 ) & not ( py `2 >= py `1 & py `2 <= - (py `1 ) ) & py <> 0. (TOP-REAL 2) ) ; :: thesis: ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x )

set q = py;
set px = |[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]|;
A16: sqrt (1 + (((py `1 ) / (py `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A17: |[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `2 = (py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))) by EUCLID:56;

A18: now

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

end;

A20: |[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `1 = (py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))) by EUCLID:56;
then A21: (|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `1 ) / (|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `2 ) = (py `1 ) / (py `2 ) by A17, A16, XCMPLX_1:92;
then A22: (|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `1 ) / (sqrt (1 + (((|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `1 ) / (|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `2 )) ^2 ))) = py `1 by A20, A16, XCMPLX_1:90;
( ( py `1 <= py `2 & - (py `2 ) <= py `1 ) or ( py `1 >= py `2 & py `1 <= - (py `2 ) ) ) by A15, JGRAPH_2:23;
then ( ( py `1 <= py `2 & - (py `2 ) <= py `1 ) or ( py `1 >= py `2 & (py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))) <= (- (py `2 )) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))) ) ) by A16, XREAL_1:66;
then ( ( py `1 <= py `2 & (- (py `2 )) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))) <= (py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))) ) or ( |[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `1 >= |[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `2 & |[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `1 <= - (|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `2 ) ) ) by A17, A20, A16, XREAL_1:66;
then ( ( (py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))) <= (py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))) & - (|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `2 ) <= |[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `1 ) or ( |[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `1 >= |[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `2 & |[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `1 <= - (|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `2 ) ) ) by A17, A16, EUCLID:56, XREAL_1:66;
then A23: Sq_Circ . |[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| = |[((|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `1 ) / (sqrt (1 + (((|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `1 ) / (|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `2 )) ^2 )))),((|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `2 ) / (sqrt (1 + (((|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `1 ) / (|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `2 )) ^2 ))))]| by A17, A20, A18, Th14, JGRAPH_2:11;
A24: dom Sq_Circ = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
(|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `2 ) / (sqrt (1 + (((|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `1 ) / (|[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]| `2 )) ^2 ))) = py `2 by A17, A16, A21, XCMPLX_1:90;
hence ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x ) by A23, A22, A24, EUCLID:57; :: thesis: verum

end;

end;

end;

hence y in rng Sq_Circ by FUNCT_1:def 5; :: thesis: verum

end;

A25: rng (Sq_Circ " ) = dom Sq_Circ by FUNCT_1:55
.= the carrier of (TOP-REAL 2) by FUNCT_2:def 1 ;
dom (Sq_Circ " ) = rng Sq_Circ by FUNCT_1:55;
then dom (Sq_Circ " ) = the carrier of (TOP-REAL 2) by A1, XBOOLE_0:def 10;
hence Sq_Circ " is Function of (TOP-REAL 2),(TOP-REAL 2) by A25, FUNCT_2:3; :: thesis: verum