A1: dom (Sq_Circ " ) = rng Sq_Circ by FUNCT_1:55;
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: ( |[((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 `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;
A5: sqrt (1 + (((py `2 ) / (py `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
then A6: (|[((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 A4, XCMPLX_1:92;

A7: now

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

end;

( ( 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, A5, 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 A4, A5, 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 A4, A5, XREAL_1:66;
then A10: 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 A4, A7, Def1, JGRAPH_2:11;
A11: (|[((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 A4, A5, A6, XCMPLX_1:90;
A12: (|[((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 A4, A5, A6, XCMPLX_1:90;
dom Sq_Circ = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
hence ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x ) by A10, A11, A12, EUCLID:57; :: thesis: verum

end;

case A13: ( 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 )

then A14: ( py <> 0. (TOP-REAL 2) & ( ( py `1 <= py `2 & - (py `2 ) <= py `1 ) or ( py `1 >= py `2 & py `1 <= - (py `2 ) ) ) ) by JGRAPH_2:23;
set q = py;
set px = |[((py `1 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 )))),((py `2 ) * (sqrt (1 + (((py `1 ) / (py `2 )) ^2 ))))]|;
A15: ( |[((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 ))) & |[((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;
A16: sqrt (1 + (((py `1 ) / (py `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
then A17: (|[((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 A15, XCMPLX_1:92;

A18: now

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

end;

( ( 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 A14, 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 A15, 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 A15, A16, XREAL_1:66;
then A20: 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 A15, A18, Th14, JGRAPH_2:11;
A21: (|[((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 A15, A16, A17, XCMPLX_1:90;
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 A15, A16, A17, XCMPLX_1:90;
dom Sq_Circ = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
hence ex x being set st
( x in dom Sq_Circ & y = Sq_Circ . x ) by A20, A21, A22, EUCLID:57; :: thesis: verum

end;

end;

end;

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

end;

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