let p be Point of (TOP-REAL 2); :: thesis: ( ( p = 0. (TOP-REAL 2) implies (Sq_Circ ") . p = 0. (TOP-REAL 2) ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) )
set q = p;
set px = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]|;
A1: |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2 = (p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))) by EUCLID:52;
A2: dom Sq_Circ = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;

hereby :: thesis: ( ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) )

assume A3: p = 0. (TOP-REAL 2) ; :: thesis: (Sq_Circ ") . p = 0. (TOP-REAL 2)
then Sq_Circ . p = p by Def1;
hence (Sq_Circ ") . p = 0. (TOP-REAL 2) by A2, A3, FUNCT_1:34; :: thesis: verum

end;

hereby :: thesis: ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| )

A4: dom Sq_Circ = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
set q = p;
assume that
A5: ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) and
A6: p <> 0. (TOP-REAL 2) ; :: thesis: (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]|
set px = |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]|;
A7: |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1 = (p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2))) by EUCLID:52;
A8: sqrt (1 + (((p `2) / (p `1)) ^2)) > 0 by Lm1, SQUARE_1:25;
A9: |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2 = (p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))) by EUCLID:52;
then A10: (|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2) / (|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1) = (p `2) / (p `1) by A7, A8, XCMPLX_1:91;
then A11: (|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2) / (sqrt (1 + (((|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2) / (|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1)) ^2))) = p `2 by A9, A8, XCMPLX_1:89;

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

assume ( |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1 = 0 & |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2 = 0 ) ; :: thesis: contradiction
then ( p `1 = 0 & p `2 = 0 ) by A7, A9, A8, XCMPLX_1:6;
hence contradiction by A6, EUCLID:53, EUCLID:54; :: thesis: verum

end;

( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & (p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))) <= (- (p `1)) * (sqrt (1 + (((p `2) / (p `1)) ^2))) ) ) by A5, A8, XREAL_1:64;
then ( ( p `2 <= p `1 & (- (p `1)) * (sqrt (1 + (((p `2) / (p `1)) ^2))) <= (p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))) ) or ( |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2 >= |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1 & |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2 <= - (|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1) ) ) by A7, A9, A8, XREAL_1:64;
then ( ( (p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))) <= (p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2))) & - (|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1) <= |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2 ) or ( |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2 >= |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1 & |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2 <= - (|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1) ) ) by A7, A8, EUCLID:52, XREAL_1:64;
then A13: Sq_Circ . |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| = |[((|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1) / (sqrt (1 + (((|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2) / (|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1)) ^2)))),((|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2) / (sqrt (1 + (((|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2) / (|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1)) ^2))))]| by A7, A9, A12, Def1, JGRAPH_2:3;
(|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1) / (sqrt (1 + (((|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2) / (|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1)) ^2))) = p `1 by A7, A8, A10, XCMPLX_1:89;
then p = Sq_Circ . |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| by A13, A11, EUCLID:53;
hence (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| by A4, FUNCT_1:34; :: thesis: verum

end;

A14: dom Sq_Circ = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A15: sqrt (1 + (((p `1) / (p `2)) ^2)) > 0 by Lm1, SQUARE_1:25;
A16: |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1 = (p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2))) by EUCLID:52;
then A17: (|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1) / (|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2) = (p `1) / (p `2) by A1, A15, XCMPLX_1:91;
then A18: (|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1) / (sqrt (1 + (((|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1) / (|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2)) ^2))) = p `1 by A16, A15, XCMPLX_1:89;
assume A19: ( not ( p `2 <= p `1 & - (p `1) <= p `2 ) & not ( p `2 >= p `1 & p `2 <= - (p `1) ) ) ; :: thesis: (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]|

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

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

end;

( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) by A19, JGRAPH_2:13;
then ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & (p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2))) <= (- (p `2)) * (sqrt (1 + (((p `1) / (p `2)) ^2))) ) ) by A15, XREAL_1:64;
then ( ( p `1 <= p `2 & (- (p `2)) * (sqrt (1 + (((p `1) / (p `2)) ^2))) <= (p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2))) ) or ( |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1 >= |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2 & |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1 <= - (|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2) ) ) by A1, A16, A15, XREAL_1:64;
then ( ( (p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2))) <= (p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))) & - (|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2) <= |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1 ) or ( |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1 >= |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2 & |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1 <= - (|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2) ) ) by A1, A15, EUCLID:52, XREAL_1:64;
then A22: Sq_Circ . |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| = |[((|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1) / (sqrt (1 + (((|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1) / (|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2)) ^2)))),((|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2) / (sqrt (1 + (((|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1) / (|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2)) ^2))))]| by A1, A16, A20, Th4, JGRAPH_2:3;
(|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2) / (sqrt (1 + (((|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1) / (|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2)) ^2))) = p `2 by A1, A15, A17, XCMPLX_1:89;
then p = Sq_Circ . |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by A22, A18, EUCLID:53;
hence (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by A14, FUNCT_1:34; :: thesis: verum