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

proof

let y be object ; :: 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 :: thesis: ( ( py = 0. (TOP-REAL 2) & ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x ) ) or ( ( ( py `2 <= py `1 & - (py `1) <= py `2 ) or ( py `2 >= py `1 & py `2 <= - (py `1) ) ) & py <> 0. (TOP-REAL 2) & ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x ) ) or ( not ( py `2 <= py `1 & - (py `1) <= py `2 ) & not ( py `2 >= py `1 & py `2 <= - (py `1) ) & py <> 0. (TOP-REAL 2) & ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x ) ) )

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:25;

A5: now :: thesis: ( |[((py `1) * (sqrt (1 + (((py `2) / (py `1)) ^2)))),((py `2) * (sqrt (1 + (((py `2) / (py `1)) ^2))))]| `1 = 0 implies not |[((py `1) * (sqrt (1 + (((py `2) / (py `1)) ^2)))),((py `2) * (sqrt (1 + (((py `2) / (py `1)) ^2))))]| `2 = 0 )

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:52;
then A8: py `2 = 0 by A4, XCMPLX_1:6;
(py `1) * (sqrt (1 + (((py `2) / (py `1)) ^2))) = 0 by A6, EUCLID:52;
then py `1 = 0 by A4, XCMPLX_1:6;
hence contradiction by A3, A8, EUCLID:53, EUCLID:54; :: 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:52;
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:52;
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:91;
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:89;
( ( 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:64;
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:64;
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:52, XREAL_1:64;
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:3;
(|[((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:89;
hence ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x ) by A14, A13, A9, EUCLID:53; :: 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:25;
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:52;

A18: now :: thesis: ( |[((py `1) * (sqrt (1 + (((py `1) / (py `2)) ^2)))),((py `2) * (sqrt (1 + (((py `1) / (py `2)) ^2))))]| `2 = 0 implies not |[((py `1) * (sqrt (1 + (((py `1) / (py `2)) ^2)))),((py `2) * (sqrt (1 + (((py `1) / (py `2)) ^2))))]| `1 = 0 )

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:52;
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:91;
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:89;
( ( py `1 <= py `2 & - (py `2) <= py `1 ) or ( py `1 >= py `2 & py `1 <= - (py `2) ) ) by A15, JGRAPH_2:13;
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:64;
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:64;
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:52, XREAL_1:64;
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, Th4, JGRAPH_2:3;
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:89;
hence ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x ) by A23, A22, A24, EUCLID:53; :: thesis: verum

end;

end;

end;

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

end;

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