set Y1 = |[(- 1),1]|;

set B0 = {(0. (TOP-REAL 2))};

let D be non empty Subset of (TOP-REAL 2); :: thesis: ( D ` = {(0. (TOP-REAL 2))} implies ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st

( h = (Sq_Circ ") | D & h is continuous ) )

A1: the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:8;

dom (Sq_Circ ") = the carrier of (TOP-REAL 2) by Th29, FUNCT_2:def 1;

then A2: dom ((Sq_Circ ") | D) = the carrier of (TOP-REAL 2) /\ D by RELAT_1:61

.= the carrier of ((TOP-REAL 2) | D) by A1, XBOOLE_1:28 ;

assume A3: D ` = {(0. (TOP-REAL 2))} ; :: thesis: ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st

( h = (Sq_Circ ") | D & h is continuous )

then A4: D = {(0. (TOP-REAL 2))} `

.= NonZero (TOP-REAL 2) by SUBSET_1:def 4 ;

A5: { p where p is Point of (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) ) } c= the carrier of ((TOP-REAL 2) | D)

then reconsider K0 = { p where p is Point of (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) ) } as non empty Subset of ((TOP-REAL 2) | D) by A5;

A7: K0 = the carrier of (((TOP-REAL 2) | D) | K0) by PRE_TOPC:8;

A8: { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } c= the carrier of ((TOP-REAL 2) | D)

then |[(- 1),1]| in { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } by JGRAPH_2:3;

then reconsider K1 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | D) by A8;

A10: K1 = the carrier of (((TOP-REAL 2) | D) | K1) by PRE_TOPC:8;

A11: D c= K0 \/ K1

.= NonZero (TOP-REAL 2) by A4, PRE_TOPC:def 5 ;

A14: K0 c= the carrier of (TOP-REAL 2)

.= the carrier of (TOP-REAL 2) /\ K0 by Th29, FUNCT_2:def 1

.= K0 by A14, XBOOLE_1:28 ;

then reconsider f = (Sq_Circ ") | K0 as Function of (((TOP-REAL 2) | D) | K0),((TOP-REAL 2) | D) by A7, A15, FUNCT_2:2, XBOOLE_1:1;

A32: K1 = [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 5;

A33: K1 c= the carrier of (TOP-REAL 2)

.= the carrier of (TOP-REAL 2) /\ K1 by Th29, FUNCT_2:def 1

.= K1 by A33, XBOOLE_1:28 ;

then reconsider g = (Sq_Circ ") | K1 as Function of (((TOP-REAL 2) | D) | K1),((TOP-REAL 2) | D) by A10, A34, FUNCT_2:2, XBOOLE_1:1;

A51: dom g = K1 by A10, FUNCT_2:def 1;

g = (Sq_Circ ") | K1 ;

then A52: K1 is closed by A4, Th40;

A53: K0 = [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 5;

then A56: K0 is closed by A4, Th39;

A57: dom f = K0 by A7, FUNCT_2:def 1;

D = [#] ((TOP-REAL 2) | D) by PRE_TOPC:def 5;

then A58: ([#] (((TOP-REAL 2) | D) | K0)) \/ ([#] (((TOP-REAL 2) | D) | K1)) = [#] ((TOP-REAL 2) | D) by A53, A32, A11;

A59: ( f is continuous & g is continuous ) by A4, Th39, Th40;

then consider h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) such that

A60: h = f +* g and

h is continuous by A53, A32, A58, A56, A52, A54, JGRAPH_2:1;

( K0 = [#] (((TOP-REAL 2) | D) | K0) & K1 = [#] (((TOP-REAL 2) | D) | K1) ) by PRE_TOPC:def 5;

then A61: f tolerates g by A54, A57, A51, PARTFUN1:def 4;

A62: for x being object st x in dom h holds

h . x = ((Sq_Circ ") | D) . x

then f +* g = (Sq_Circ ") | D by A60, A2, A62;

hence ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st

( h = (Sq_Circ ") | D & h is continuous ) by A53, A32, A58, A56, A59, A52, A54, JGRAPH_2:1; :: thesis: verum

set B0 = {(0. (TOP-REAL 2))};

let D be non empty Subset of (TOP-REAL 2); :: thesis: ( D ` = {(0. (TOP-REAL 2))} implies ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st

( h = (Sq_Circ ") | D & h is continuous ) )

A1: the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:8;

dom (Sq_Circ ") = the carrier of (TOP-REAL 2) by Th29, FUNCT_2:def 1;

then A2: dom ((Sq_Circ ") | D) = the carrier of (TOP-REAL 2) /\ D by RELAT_1:61

.= the carrier of ((TOP-REAL 2) | D) by A1, XBOOLE_1:28 ;

assume A3: D ` = {(0. (TOP-REAL 2))} ; :: thesis: ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st

( h = (Sq_Circ ") | D & h is continuous )

then A4: D = {(0. (TOP-REAL 2))} `

.= NonZero (TOP-REAL 2) by SUBSET_1:def 4 ;

A5: { p where p is Point of (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) ) } c= the carrier of ((TOP-REAL 2) | D)

proof

1.REAL 2 in { p where p is Point of (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) ) }
by Lm9, Lm10;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (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) ) } or x in the carrier of ((TOP-REAL 2) | D) )

assume x in { p where p is Point of (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) ) } ; :: thesis: x in the carrier of ((TOP-REAL 2) | D)

then A6: ex p being Point of (TOP-REAL 2) st

( x = p & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) ;

end;assume x in { p where p is Point of (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) ) } ; :: thesis: x in the carrier of ((TOP-REAL 2) | D)

then A6: ex p being Point of (TOP-REAL 2) st

( x = p & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) ;

now :: thesis: x in D

hence
x in the carrier of ((TOP-REAL 2) | D)
by PRE_TOPC:8; :: thesis: verumassume
not x in D
; :: thesis: contradiction

then x in the carrier of (TOP-REAL 2) \ D by A6, XBOOLE_0:def 5;

then x in D ` by SUBSET_1:def 4;

hence contradiction by A3, A6, TARSKI:def 1; :: thesis: verum

end;then x in the carrier of (TOP-REAL 2) \ D by A6, XBOOLE_0:def 5;

then x in D ` by SUBSET_1:def 4;

hence contradiction by A3, A6, TARSKI:def 1; :: thesis: verum

then reconsider K0 = { p where p is Point of (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) ) } as non empty Subset of ((TOP-REAL 2) | D) by A5;

A7: K0 = the carrier of (((TOP-REAL 2) | D) | K0) by PRE_TOPC:8;

A8: { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } c= the carrier of ((TOP-REAL 2) | D)

proof

( |[(- 1),1]| `1 = - 1 & |[(- 1),1]| `2 = 1 )
by EUCLID:52;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } or x in the carrier of ((TOP-REAL 2) | D) )

assume x in { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } ; :: thesis: x in the carrier of ((TOP-REAL 2) | D)

then A9: ex p being Point of (TOP-REAL 2) st

( x = p & ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) ;

end;assume x in { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } ; :: thesis: x in the carrier of ((TOP-REAL 2) | D)

then A9: ex p being Point of (TOP-REAL 2) st

( x = p & ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) ;

now :: thesis: x in D

hence
x in the carrier of ((TOP-REAL 2) | D)
by PRE_TOPC:8; :: thesis: verumassume
not x in D
; :: thesis: contradiction

then x in the carrier of (TOP-REAL 2) \ D by A9, XBOOLE_0:def 5;

then x in D ` by SUBSET_1:def 4;

hence contradiction by A3, A9, TARSKI:def 1; :: thesis: verum

end;then x in the carrier of (TOP-REAL 2) \ D by A9, XBOOLE_0:def 5;

then x in D ` by SUBSET_1:def 4;

hence contradiction by A3, A9, TARSKI:def 1; :: thesis: verum

then |[(- 1),1]| in { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } by JGRAPH_2:3;

then reconsider K1 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | D) by A8;

A10: K1 = the carrier of (((TOP-REAL 2) | D) | K1) by PRE_TOPC:8;

A11: D c= K0 \/ K1

proof

A13: the carrier of ((TOP-REAL 2) | D) =
[#] ((TOP-REAL 2) | D)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in K0 \/ K1 )

assume A12: x in D ; :: thesis: x in K0 \/ K1

then reconsider px = x as Point of (TOP-REAL 2) ;

not x in {(0. (TOP-REAL 2))} by A4, A12, XBOOLE_0:def 5;

then ( ( ( ( px `2 <= px `1 & - (px `1) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1) ) ) & px <> 0. (TOP-REAL 2) ) or ( ( ( px `1 <= px `2 & - (px `2) <= px `1 ) or ( px `1 >= px `2 & px `1 <= - (px `2) ) ) & px <> 0. (TOP-REAL 2) ) ) by TARSKI:def 1, XREAL_1:26;

then ( x in K0 or x in K1 ) ;

hence x in K0 \/ K1 by XBOOLE_0:def 3; :: thesis: verum

end;assume A12: x in D ; :: thesis: x in K0 \/ K1

then reconsider px = x as Point of (TOP-REAL 2) ;

not x in {(0. (TOP-REAL 2))} by A4, A12, XBOOLE_0:def 5;

then ( ( ( ( px `2 <= px `1 & - (px `1) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1) ) ) & px <> 0. (TOP-REAL 2) ) or ( ( ( px `1 <= px `2 & - (px `2) <= px `1 ) or ( px `1 >= px `2 & px `1 <= - (px `2) ) ) & px <> 0. (TOP-REAL 2) ) ) by TARSKI:def 1, XREAL_1:26;

then ( x in K0 or x in K1 ) ;

hence x in K0 \/ K1 by XBOOLE_0:def 3; :: thesis: verum

.= NonZero (TOP-REAL 2) by A4, PRE_TOPC:def 5 ;

A14: K0 c= the carrier of (TOP-REAL 2)

proof

A15:
rng ((Sq_Circ ") | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in K0 or z in the carrier of (TOP-REAL 2) )

assume z in K0 ; :: thesis: z in the carrier of (TOP-REAL 2)

then ex p8 being Point of (TOP-REAL 2) st

( p8 = z & ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) ;

hence z in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;assume z in K0 ; :: thesis: z in the carrier of (TOP-REAL 2)

then ex p8 being Point of (TOP-REAL 2) st

( p8 = z & ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) ;

hence z in the carrier of (TOP-REAL 2) ; :: thesis: verum

proof

dom ((Sq_Circ ") | K0) =
(dom (Sq_Circ ")) /\ K0
by RELAT_1:61
reconsider K00 = K0 as Subset of (TOP-REAL 2) by A14;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((Sq_Circ ") | K0) or y in the carrier of (((TOP-REAL 2) | D) | K0) )

A16: for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K00) holds

q `1 <> 0

then consider x being object such that

A20: x in dom ((Sq_Circ ") | K0) and

A21: y = ((Sq_Circ ") | K0) . x by FUNCT_1:def 3;

A22: x in (dom (Sq_Circ ")) /\ K0 by A20, RELAT_1:61;

then A23: x in K0 by XBOOLE_0:def 4;

then reconsider p = x as Point of (TOP-REAL 2) by A14;

K00 = the carrier of ((TOP-REAL 2) | K00) by PRE_TOPC:8;

then p in the carrier of ((TOP-REAL 2) | K00) by A22, XBOOLE_0:def 4;

then A24: p `1 <> 0 by A16;

set p9 = |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]|;

A25: ( |[((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 `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;

A26: ex px being Point of (TOP-REAL 2) st

( x = px & ( ( px `2 <= px `1 & - (px `1) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1) ) ) & px <> 0. (TOP-REAL 2) ) by A23;

then A27: (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| by Th28;

A28: sqrt (1 + (((p `2) / (p `1)) ^2)) > 0 by Lm1, SQUARE_1:25;

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))) ) or ( (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))) <= (- (p `1)) * (sqrt (1 + (((p `2) / (p `1)) ^2))) ) ) by A26, XREAL_1:64;

then A29: ( ( (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))) ) or ( (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))) <= - ((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))) ) ) ;

A30: |[((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;

then y in K0 by A31, A27, A29, A25;

hence y in the carrier of (((TOP-REAL 2) | D) | K0) by PRE_TOPC:8; :: thesis: verum

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((Sq_Circ ") | K0) or y in the carrier of (((TOP-REAL 2) | D) | K0) )

A16: for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K00) holds

q `1 <> 0

proof

assume
y in rng ((Sq_Circ ") | K0)
; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K0)
let q be Point of (TOP-REAL 2); :: thesis: ( q in the carrier of ((TOP-REAL 2) | K00) implies q `1 <> 0 )

A17: the carrier of ((TOP-REAL 2) | K00) = K0 by PRE_TOPC:8;

assume q in the carrier of ((TOP-REAL 2) | K00) ; :: thesis: q `1 <> 0

then A18: ex p3 being Point of (TOP-REAL 2) st

( q = p3 & ( ( p3 `2 <= p3 `1 & - (p3 `1) <= p3 `2 ) or ( p3 `2 >= p3 `1 & p3 `2 <= - (p3 `1) ) ) & p3 <> 0. (TOP-REAL 2) ) by A17;

end;A17: the carrier of ((TOP-REAL 2) | K00) = K0 by PRE_TOPC:8;

assume q in the carrier of ((TOP-REAL 2) | K00) ; :: thesis: q `1 <> 0

then A18: ex p3 being Point of (TOP-REAL 2) st

( q = p3 & ( ( p3 `2 <= p3 `1 & - (p3 `1) <= p3 `2 ) or ( p3 `2 >= p3 `1 & p3 `2 <= - (p3 `1) ) ) & p3 <> 0. (TOP-REAL 2) ) by A17;

now :: thesis: not q `1 = 0

hence
q `1 <> 0
; :: thesis: verumassume A19:
q `1 = 0
; :: thesis: contradiction

then q `2 = 0 by A18;

hence contradiction by A18, A19, EUCLID:53, EUCLID:54; :: thesis: verum

end;then q `2 = 0 by A18;

hence contradiction by A18, A19, EUCLID:53, EUCLID:54; :: thesis: verum

then consider x being object such that

A20: x in dom ((Sq_Circ ") | K0) and

A21: y = ((Sq_Circ ") | K0) . x by FUNCT_1:def 3;

A22: x in (dom (Sq_Circ ")) /\ K0 by A20, RELAT_1:61;

then A23: x in K0 by XBOOLE_0:def 4;

then reconsider p = x as Point of (TOP-REAL 2) by A14;

K00 = the carrier of ((TOP-REAL 2) | K00) by PRE_TOPC:8;

then p in the carrier of ((TOP-REAL 2) | K00) by A22, XBOOLE_0:def 4;

then A24: p `1 <> 0 by A16;

set p9 = |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]|;

A25: ( |[((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 `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;

A26: ex px being Point of (TOP-REAL 2) st

( x = px & ( ( px `2 <= px `1 & - (px `1) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1) ) ) & px <> 0. (TOP-REAL 2) ) by A23;

then A27: (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| by Th28;

A28: sqrt (1 + (((p `2) / (p `1)) ^2)) > 0 by Lm1, SQUARE_1:25;

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))) ) or ( (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))) <= (- (p `1)) * (sqrt (1 + (((p `2) / (p `1)) ^2))) ) ) by A26, XREAL_1:64;

then A29: ( ( (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))) ) or ( (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))) <= - ((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))) ) ) ;

A30: |[((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;

A31: now :: thesis: not |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| = 0. (TOP-REAL 2)

(Sq_Circ ") . p = y
by A21, A23, FUNCT_1:49;assume
|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| = 0. (TOP-REAL 2)
; :: thesis: contradiction

then 0 / (sqrt (1 + (((p `2) / (p `1)) ^2))) = ((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))) / (sqrt (1 + (((p `2) / (p `1)) ^2))) by A30, EUCLID:52, EUCLID:54;

hence contradiction by A24, A28, XCMPLX_1:89; :: thesis: verum

end;then 0 / (sqrt (1 + (((p `2) / (p `1)) ^2))) = ((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))) / (sqrt (1 + (((p `2) / (p `1)) ^2))) by A30, EUCLID:52, EUCLID:54;

hence contradiction by A24, A28, XCMPLX_1:89; :: thesis: verum

then y in K0 by A31, A27, A29, A25;

hence y in the carrier of (((TOP-REAL 2) | D) | K0) by PRE_TOPC:8; :: thesis: verum

.= the carrier of (TOP-REAL 2) /\ K0 by Th29, FUNCT_2:def 1

.= K0 by A14, XBOOLE_1:28 ;

then reconsider f = (Sq_Circ ") | K0 as Function of (((TOP-REAL 2) | D) | K0),((TOP-REAL 2) | D) by A7, A15, FUNCT_2:2, XBOOLE_1:1;

A32: K1 = [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 5;

A33: K1 c= the carrier of (TOP-REAL 2)

proof

A34:
rng ((Sq_Circ ") | K1) c= the carrier of (((TOP-REAL 2) | D) | K1)
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in K1 or z in the carrier of (TOP-REAL 2) )

assume z in K1 ; :: thesis: z in the carrier of (TOP-REAL 2)

then ex p8 being Point of (TOP-REAL 2) st

( p8 = z & ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) ;

hence z in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;assume z in K1 ; :: thesis: z in the carrier of (TOP-REAL 2)

then ex p8 being Point of (TOP-REAL 2) st

( p8 = z & ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) ;

hence z in the carrier of (TOP-REAL 2) ; :: thesis: verum

proof

dom ((Sq_Circ ") | K1) =
(dom (Sq_Circ ")) /\ K1
by RELAT_1:61
reconsider K10 = K1 as Subset of (TOP-REAL 2) by A33;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((Sq_Circ ") | K1) or y in the carrier of (((TOP-REAL 2) | D) | K1) )

A35: for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K10) holds

q `2 <> 0

then consider x being object such that

A39: x in dom ((Sq_Circ ") | K1) and

A40: y = ((Sq_Circ ") | K1) . x by FUNCT_1:def 3;

A41: x in (dom (Sq_Circ ")) /\ K1 by A39, RELAT_1:61;

then A42: x in K1 by XBOOLE_0:def 4;

then reconsider p = x as Point of (TOP-REAL 2) by A33;

K10 = the carrier of ((TOP-REAL 2) | K10) by PRE_TOPC:8;

then p in the carrier of ((TOP-REAL 2) | K10) by A41, XBOOLE_0:def 4;

then A43: p `2 <> 0 by A35;

set p9 = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]|;

A44: ( |[((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))) & |[((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;

A45: ex px being Point of (TOP-REAL 2) st

( x = px & ( ( px `1 <= px `2 & - (px `2) <= px `1 ) or ( px `1 >= px `2 & px `1 <= - (px `2) ) ) & px <> 0. (TOP-REAL 2) ) by A42;

then A46: (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by Th30;

A47: sqrt (1 + (((p `1) / (p `2)) ^2)) > 0 by Lm1, SQUARE_1:25;

then ( ( (p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2))) <= (p `2) * (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))) ) or ( (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))) ) ) by A45, XREAL_1:64;

then A48: ( ( (p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2))) <= (p `2) * (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))) ) or ( (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)))) ) ) ;

A49: |[((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;

then y in K1 by A50, A46, A48, A44;

hence y in the carrier of (((TOP-REAL 2) | D) | K1) by PRE_TOPC:8; :: thesis: verum

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((Sq_Circ ") | K1) or y in the carrier of (((TOP-REAL 2) | D) | K1) )

A35: for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K10) holds

q `2 <> 0

proof

assume
y in rng ((Sq_Circ ") | K1)
; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K1)
let q be Point of (TOP-REAL 2); :: thesis: ( q in the carrier of ((TOP-REAL 2) | K10) implies q `2 <> 0 )

A36: the carrier of ((TOP-REAL 2) | K10) = K1 by PRE_TOPC:8;

assume q in the carrier of ((TOP-REAL 2) | K10) ; :: thesis: q `2 <> 0

then A37: ex p3 being Point of (TOP-REAL 2) st

( q = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2) ) ) & p3 <> 0. (TOP-REAL 2) ) by A36;

end;A36: the carrier of ((TOP-REAL 2) | K10) = K1 by PRE_TOPC:8;

assume q in the carrier of ((TOP-REAL 2) | K10) ; :: thesis: q `2 <> 0

then A37: ex p3 being Point of (TOP-REAL 2) st

( q = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2) ) ) & p3 <> 0. (TOP-REAL 2) ) by A36;

now :: thesis: not q `2 = 0

hence
q `2 <> 0
; :: thesis: verumassume A38:
q `2 = 0
; :: thesis: contradiction

then q `1 = 0 by A37;

hence contradiction by A37, A38, EUCLID:53, EUCLID:54; :: thesis: verum

end;then q `1 = 0 by A37;

hence contradiction by A37, A38, EUCLID:53, EUCLID:54; :: thesis: verum

then consider x being object such that

A39: x in dom ((Sq_Circ ") | K1) and

A40: y = ((Sq_Circ ") | K1) . x by FUNCT_1:def 3;

A41: x in (dom (Sq_Circ ")) /\ K1 by A39, RELAT_1:61;

then A42: x in K1 by XBOOLE_0:def 4;

then reconsider p = x as Point of (TOP-REAL 2) by A33;

K10 = the carrier of ((TOP-REAL 2) | K10) by PRE_TOPC:8;

then p in the carrier of ((TOP-REAL 2) | K10) by A41, XBOOLE_0:def 4;

then A43: p `2 <> 0 by A35;

set p9 = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]|;

A44: ( |[((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))) & |[((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;

A45: ex px being Point of (TOP-REAL 2) st

( x = px & ( ( px `1 <= px `2 & - (px `2) <= px `1 ) or ( px `1 >= px `2 & px `1 <= - (px `2) ) ) & px <> 0. (TOP-REAL 2) ) by A42;

then A46: (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by Th30;

A47: sqrt (1 + (((p `1) / (p `2)) ^2)) > 0 by Lm1, SQUARE_1:25;

then ( ( (p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2))) <= (p `2) * (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))) ) or ( (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))) ) ) by A45, XREAL_1:64;

then A48: ( ( (p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2))) <= (p `2) * (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))) ) or ( (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)))) ) ) ;

A49: |[((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;

A50: now :: thesis: not |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| = 0. (TOP-REAL 2)

(Sq_Circ ") . p = y
by A40, A42, FUNCT_1:49;assume
|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| = 0. (TOP-REAL 2)
; :: thesis: contradiction

then 0 / (sqrt (1 + (((p `1) / (p `2)) ^2))) = ((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2)))) / (sqrt (1 + (((p `1) / (p `2)) ^2))) by A49, EUCLID:52, EUCLID:54;

hence contradiction by A43, A47, XCMPLX_1:89; :: thesis: verum

end;then 0 / (sqrt (1 + (((p `1) / (p `2)) ^2))) = ((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2)))) / (sqrt (1 + (((p `1) / (p `2)) ^2))) by A49, EUCLID:52, EUCLID:54;

hence contradiction by A43, A47, XCMPLX_1:89; :: thesis: verum

then y in K1 by A50, A46, A48, A44;

hence y in the carrier of (((TOP-REAL 2) | D) | K1) by PRE_TOPC:8; :: thesis: verum

.= the carrier of (TOP-REAL 2) /\ K1 by Th29, FUNCT_2:def 1

.= K1 by A33, XBOOLE_1:28 ;

then reconsider g = (Sq_Circ ") | K1 as Function of (((TOP-REAL 2) | D) | K1),((TOP-REAL 2) | D) by A10, A34, FUNCT_2:2, XBOOLE_1:1;

A51: dom g = K1 by A10, FUNCT_2:def 1;

g = (Sq_Circ ") | K1 ;

then A52: K1 is closed by A4, Th40;

A53: K0 = [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 5;

A54: now :: thesis: for x being object st x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) holds

f . x = g . x

f = (Sq_Circ ") | K0
;f . x = g . x

let x be object ; :: thesis: ( x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) implies f . x = g . x )

assume A55: x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) ; :: thesis: f . x = g . x

then x in K0 by A53, XBOOLE_0:def 4;

then f . x = (Sq_Circ ") . x by FUNCT_1:49;

hence f . x = g . x by A32, A55, FUNCT_1:49; :: thesis: verum

end;assume A55: x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) ; :: thesis: f . x = g . x

then x in K0 by A53, XBOOLE_0:def 4;

then f . x = (Sq_Circ ") . x by FUNCT_1:49;

hence f . x = g . x by A32, A55, FUNCT_1:49; :: thesis: verum

then A56: K0 is closed by A4, Th39;

A57: dom f = K0 by A7, FUNCT_2:def 1;

D = [#] ((TOP-REAL 2) | D) by PRE_TOPC:def 5;

then A58: ([#] (((TOP-REAL 2) | D) | K0)) \/ ([#] (((TOP-REAL 2) | D) | K1)) = [#] ((TOP-REAL 2) | D) by A53, A32, A11;

A59: ( f is continuous & g is continuous ) by A4, Th39, Th40;

then consider h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) such that

A60: h = f +* g and

h is continuous by A53, A32, A58, A56, A52, A54, JGRAPH_2:1;

( K0 = [#] (((TOP-REAL 2) | D) | K0) & K1 = [#] (((TOP-REAL 2) | D) | K1) ) by PRE_TOPC:def 5;

then A61: f tolerates g by A54, A57, A51, PARTFUN1:def 4;

A62: for x being object st x in dom h holds

h . x = ((Sq_Circ ") | D) . x

proof

dom h = the carrier of ((TOP-REAL 2) | D)
by FUNCT_2:def 1;
let x be object ; :: thesis: ( x in dom h implies h . x = ((Sq_Circ ") | D) . x )

assume A63: x in dom h ; :: thesis: h . x = ((Sq_Circ ") | D) . x

then reconsider p = x as Point of (TOP-REAL 2) by A13, XBOOLE_0:def 5;

not x in {(0. (TOP-REAL 2))} by A13, A63, XBOOLE_0:def 5;

then A64: x <> 0. (TOP-REAL 2) by TARSKI:def 1;

x in the carrier of (TOP-REAL 2) \ (D `) by A3, A13, A63;

then A65: x in (D `) ` by SUBSET_1:def 4;

end;assume A63: x in dom h ; :: thesis: h . x = ((Sq_Circ ") | D) . x

then reconsider p = x as Point of (TOP-REAL 2) by A13, XBOOLE_0:def 5;

not x in {(0. (TOP-REAL 2))} by A13, A63, XBOOLE_0:def 5;

then A64: x <> 0. (TOP-REAL 2) by TARSKI:def 1;

x in the carrier of (TOP-REAL 2) \ (D `) by A3, A13, A63;

then A65: x in (D `) ` by SUBSET_1:def 4;

per cases
( x in K0 or not x in K0 )
;

end;

suppose A66:
x in K0
; :: thesis: h . x = ((Sq_Circ ") | D) . x

A67: ((Sq_Circ ") | D) . p =
(Sq_Circ ") . p
by A65, FUNCT_1:49

.= f . p by A66, FUNCT_1:49 ;

h . p = (g +* f) . p by A60, A61, FUNCT_4:34

.= f . p by A57, A66, FUNCT_4:13 ;

hence h . x = ((Sq_Circ ") | D) . x by A67; :: thesis: verum

end;.= f . p by A66, FUNCT_1:49 ;

h . p = (g +* f) . p by A60, A61, FUNCT_4:34

.= f . p by A57, A66, FUNCT_4:13 ;

hence h . x = ((Sq_Circ ") | D) . x by A67; :: thesis: verum

suppose
not x in K0
; :: thesis: h . x = ((Sq_Circ ") | D) . x

then
( not ( p `2 <= p `1 & - (p `1) <= p `2 ) & not ( p `2 >= p `1 & p `2 <= - (p `1) ) )
by A64;

then ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) by XREAL_1:26;

then A68: x in K1 by A64;

((Sq_Circ ") | D) . p = (Sq_Circ ") . p by A65, FUNCT_1:49

.= g . p by A68, FUNCT_1:49 ;

hence h . x = ((Sq_Circ ") | D) . x by A60, A51, A68, FUNCT_4:13; :: thesis: verum

end;then ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) by XREAL_1:26;

then A68: x in K1 by A64;

((Sq_Circ ") | D) . p = (Sq_Circ ") . p by A65, FUNCT_1:49

.= g . p by A68, FUNCT_1:49 ;

hence h . x = ((Sq_Circ ") | D) . x by A60, A51, A68, FUNCT_4:13; :: thesis: verum

then f +* g = (Sq_Circ ") | D by A60, A2, A62;

hence ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st

( h = (Sq_Circ ") | D & h is continuous ) by A53, A32, A58, A56, A59, A52, A54, JGRAPH_2:1; :: thesis: verum