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:56;
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:56; :: 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:56;
A8: sqrt (1 + (((p `2 ) / (p `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
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:56;
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:92;
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:90;

A12: now

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:57, EUCLID:58; :: 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:66;
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:66;
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:56, XREAL_1:66;
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:11;
(|[((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:90;
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:57;
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:56; :: 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:93;
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:56;
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:92;
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:90;
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

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:23;
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:66;
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:66;
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:56, XREAL_1:66;
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, Th14, JGRAPH_2:11;
(|[((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:90;
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:57;
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:56; :: thesis: verum