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 ) )
assume A1: 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 A2: D = {(0. (TOP-REAL 2))} `
.= NonZero (TOP-REAL 2) by SUBSET_1:def 5 ;
A3: { 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

let x be set ; :: 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 consider p being Point of (TOP-REAL 2) such that
A4: ( 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

assume not x in D ; :: thesis: contradiction
then x in the carrier of (TOP-REAL 2) \ D by A4, XBOOLE_0:def 5;
then x in D ` by SUBSET_1:def 5;
hence contradiction by A1, A4, TARSKI:def 1; :: thesis: verum

end;

hence x in the carrier of ((TOP-REAL 2) | D) by PRE_TOPC:29; :: thesis: verum

end;

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 Lm7;
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 A3;
A5: { 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

let x be set ; :: 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 consider p being Point of (TOP-REAL 2) such that
A6: ( 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

assume 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 5;
hence contradiction by A1, A6, TARSKI:def 1; :: thesis: verum

end;

hence x in the carrier of ((TOP-REAL 2) | D) by PRE_TOPC:29; :: thesis: verum

end;

set Y1 = |[(- 1),1]|;
( |[(- 1),1]| `1 = - 1 & |[(- 1),1]| `2 = 1 ) by EUCLID:56;
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:11;
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 A5;
A7: the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:29;
A8: K0 c= the carrier of (TOP-REAL 2)

proof

let z be set ; :: 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 consider p8 being Point of (TOP-REAL 2) such that
A9: ( p8 = z & ( ( p8 `2 <= p8 `1 & - (p8 `1 ) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1 ) ) ) & p8 <> 0. (TOP-REAL 2) ) ;
thus z in the carrier of (TOP-REAL 2) by A9; :: thesis: verum

end;

A10: dom (Sq_Circ | K0) = (dom Sq_Circ ) /\ K0 by RELAT_1:90
.= the carrier of (TOP-REAL 2) /\ K0 by FUNCT_2:def 1
.= K0 by A8, XBOOLE_1:28 ;
A11: K0 = the carrier of (((TOP-REAL 2) | D) | K0) by PRE_TOPC:29;
rng (Sq_Circ | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Sq_Circ | K0) or y in the carrier of (((TOP-REAL 2) | D) | K0) )
assume y in rng (Sq_Circ | K0) ; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K0)
then consider x being set such that
A12: ( x in dom (Sq_Circ | K0) & y = (Sq_Circ | K0) . x ) by FUNCT_1:def 5;
A13: x in (dom Sq_Circ ) /\ K0 by A12, RELAT_1:90;
then A14: x in K0 by XBOOLE_0:def 4;
K0 c= the carrier of (TOP-REAL 2) by A7, XBOOLE_1:1;
then reconsider p = x as Point of (TOP-REAL 2) by A14;
A15: Sq_Circ . p = y by A12, A14, FUNCT_1:72;
consider px being Point of (TOP-REAL 2) such that
A16: ( 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 A14;
reconsider K00 = K0 as Subset of (TOP-REAL 2) by A7, XBOOLE_1:1;
K00 = the carrier of ((TOP-REAL 2) | K00) by PRE_TOPC:29;
then A17: p in the carrier of ((TOP-REAL 2) | K00) by A13, XBOOLE_0:def 4;
for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K00) holds
q `1 <> 0

proof

let q be Point of (TOP-REAL 2); :: thesis: ( q in the carrier of ((TOP-REAL 2) | K00) implies q `1 <> 0 )
assume A18: q in the carrier of ((TOP-REAL 2) | K00) ; :: thesis: q `1 <> 0
the carrier of ((TOP-REAL 2) | K00) = K0 by PRE_TOPC:29;
then consider p3 being Point of (TOP-REAL 2) such that
A19: ( 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 A18;

now

assume A20: q `1 = 0 ; :: thesis: contradiction
then q `2 = 0 by A19;
hence contradiction by A19, A20, EUCLID:57, EUCLID:58; :: thesis: verum

end;

hence q `1 <> 0 ; :: thesis: verum

end;

then A21: p `1 <> 0 by A17;
set p9 = |[((p `1 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]|;
A22: ( |[((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:56;
A23: sqrt (1 + (((p `2 ) / (p `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;

A24: now

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 A22, EUCLID:56, EUCLID:58;
hence contradiction by A21, A23, XCMPLX_1:88; :: thesis: verum

end;

A25: Sq_Circ . p = |[((p `1 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]| by A16, Def1;
( ( (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 A16, A23, XREAL_1:74;
then A26: ( ( (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 XCMPLX_1:188;
( |[((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:56;
then y in K0 by A15, A24, A25, A26;
then y in [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 10;
hence y in the carrier of (((TOP-REAL 2) | D) | K0) ; :: thesis: verum

end;

then reconsider f = Sq_Circ | K0 as Function of (((TOP-REAL 2) | D) | K0),((TOP-REAL 2) | D) by A10, A11, FUNCT_2:4, XBOOLE_1:1;
A27: K1 c= the carrier of (TOP-REAL 2)

proof

let z be set ; :: 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 consider p8 being Point of (TOP-REAL 2) such that
A28: ( p8 = z & ( ( p8 `1 <= p8 `2 & - (p8 `2 ) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2 ) ) ) & p8 <> 0. (TOP-REAL 2) ) ;
thus z in the carrier of (TOP-REAL 2) by A28; :: thesis: verum

end;

A29: dom (Sq_Circ | K1) = (dom Sq_Circ ) /\ K1 by RELAT_1:90
.= the carrier of (TOP-REAL 2) /\ K1 by FUNCT_2:def 1
.= K1 by A27, XBOOLE_1:28 ;
A30: K1 = the carrier of (((TOP-REAL 2) | D) | K1) by PRE_TOPC:29;
rng (Sq_Circ | K1) c= the carrier of (((TOP-REAL 2) | D) | K1)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Sq_Circ | K1) or y in the carrier of (((TOP-REAL 2) | D) | K1) )
assume y in rng (Sq_Circ | K1) ; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K1)
then consider x being set such that
A31: ( x in dom (Sq_Circ | K1) & y = (Sq_Circ | K1) . x ) by FUNCT_1:def 5;
A32: x in (dom Sq_Circ ) /\ K1 by A31, RELAT_1:90;
then A33: x in K1 by XBOOLE_0:def 4;
then reconsider p = x as Point of (TOP-REAL 2) by A27;
A34: Sq_Circ . p = y by A31, A33, FUNCT_1:72;
consider px being Point of (TOP-REAL 2) such that
A35: ( 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 A33;
reconsider K10 = K1 as Subset of (TOP-REAL 2) by A27;
K10 = the carrier of ((TOP-REAL 2) | K10) by PRE_TOPC:29;
then A36: p in the carrier of ((TOP-REAL 2) | K10) by A32, XBOOLE_0:def 4;
for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K10) holds
q `2 <> 0

proof

let q be Point of (TOP-REAL 2); :: thesis: ( q in the carrier of ((TOP-REAL 2) | K10) implies q `2 <> 0 )
assume A37: q in the carrier of ((TOP-REAL 2) | K10) ; :: thesis: q `2 <> 0
the carrier of ((TOP-REAL 2) | K10) = K1 by PRE_TOPC:29;
then consider p3 being Point of (TOP-REAL 2) such that
A38: ( 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 A37;

now

assume A39: q `2 = 0 ; :: thesis: contradiction
then q `1 = 0 by A38;
hence contradiction by A38, A39, EUCLID:57, EUCLID:58; :: thesis: verum

end;

hence q `2 <> 0 ; :: thesis: verum

end;

then A40: p `2 <> 0 by A36;
set p9 = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]|;
A41: ( |[((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 `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;
A42: sqrt (1 + (((p `1 ) / (p `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;

A43: now

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 A41, EUCLID:56, EUCLID:58;
hence contradiction by A40, A42, XCMPLX_1:88; :: thesis: verum

end;

A44: Sq_Circ . p = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| by A35, Th14;
( ( (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 A35, A42, XREAL_1:74;
then A45: ( ( (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 XCMPLX_1:188;
( |[((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:56;
then y in K1 by A34, A43, A44, A45;
hence y in the carrier of (((TOP-REAL 2) | D) | K1) by PRE_TOPC:29; :: thesis: verum

end;

then reconsider g = Sq_Circ | K1 as Function of (((TOP-REAL 2) | D) | K1),((TOP-REAL 2) | D) by A29, A30, FUNCT_2:4, XBOOLE_1:1;
A46: K0 = [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 10;
A47: K1 = [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 10;
A48: D = [#] ((TOP-REAL 2) | D) by PRE_TOPC:def 10;
D c= K0 \/ K1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in K0 \/ K1 )
assume A49: x in D ; :: thesis: x in K0 \/ K1
then A50: ( x in the carrier of (TOP-REAL 2) & not x in {(0. (TOP-REAL 2))} ) by A2, XBOOLE_0:def 5;
reconsider px = x as Point of (TOP-REAL 2) by A49;
( ( ( ( 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 A50, TARSKI:def 1, XREAL_1:28;
then ( x in K0 or x in K1 ) ;
hence x in K0 \/ K1 by XBOOLE_0:def 3; :: thesis: verum

end;

then A51: ([#] (((TOP-REAL 2) | D) | K0)) \/ ([#] (((TOP-REAL 2) | D) | K1)) = [#] ((TOP-REAL 2) | D) by A46, A47, A48, XBOOLE_0:def 10;
( f = Sq_Circ | K0 & D = NonZero (TOP-REAL 2) & 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) ) } ) by A2;
then A52: ( f is continuous & K0 is closed ) by Th27;
( g = Sq_Circ | K1 & D = NonZero (TOP-REAL 2) & 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) ) } ) by A2;
then A53: ( g is continuous & K1 is closed ) by Th28;
A54: for x being set st x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) holds
f . x = g . x

proof

let x be set ; :: 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 & x in K1 ) by A46, A47, XBOOLE_0:def 4;
then f . x = Sq_Circ . x by FUNCT_1:72;
hence f . x = g . x by A47, A55, FUNCT_1:72; :: thesis: verum

end;

then consider h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) such that
A56: ( h = f +* g & h is continuous ) by A46, A47, A51, A52, A53, JGRAPH_2:9;
A57: dom h = the carrier of ((TOP-REAL 2) | D) by FUNCT_2:def 1;
A58: the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:29;
A59: the carrier of ((TOP-REAL 2) | D) = [#] ((TOP-REAL 2) | D)
.= NonZero (TOP-REAL 2) by A2, PRE_TOPC:def 10 ;
dom Sq_Circ = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A60: dom (Sq_Circ | D) = the carrier of (TOP-REAL 2) /\ D by RELAT_1:90
.= the carrier of ((TOP-REAL 2) | D) by A58, XBOOLE_1:28 ;
A61: dom f = K0 by A11, FUNCT_2:def 1;
A62: K0 = [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 10;
A63: dom g = K1 by A30, FUNCT_2:def 1;
K1 = [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 10;
then A64: f tolerates g by A54, A61, A62, A63, PARTFUN1:def 6;
for x being set st x in dom h holds
h . x = (Sq_Circ | D) . x

proof

let x be set ; :: thesis: ( x in dom h implies h . x = (Sq_Circ | D) . x )
assume A65: x in dom h ; :: thesis: h . x = (Sq_Circ | D) . x
then ( x in the carrier of (TOP-REAL 2) & not x in {(0. (TOP-REAL 2))} ) by A59, XBOOLE_0:def 5;
then A66: x <> 0. (TOP-REAL 2) by TARSKI:def 1;
reconsider p = x as Point of (TOP-REAL 2) by A59, A65, XBOOLE_0:def 5;
x in the carrier of (TOP-REAL 2) \ (D ` ) by A1, A59, A65;
then A67: x in (D ` ) ` by SUBSET_1:def 5;

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

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

A69: (Sq_Circ | D) . p = Sq_Circ . p by A67, FUNCT_1:72
.= f . p by A68, FUNCT_1:72 ;
h . p = (g +* f) . p by A56, A64, FUNCT_4:35
.= f . p by A61, A68, FUNCT_4:14 ;
hence h . x = (Sq_Circ | D) . x by A69; :: thesis: verum

end;

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 A66;
then ( ( p `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) by XREAL_1:28;
then A70: x in K1 by A66;
(Sq_Circ | D) . p = Sq_Circ . p by A67, FUNCT_1:72
.= g . p by A70, FUNCT_1:72 ;
hence h . x = (Sq_Circ | D) . x by A56, A63, A70, FUNCT_4:14; :: thesis: verum

end;

end;

end;

then f +* g = Sq_Circ | D by A56, A57, A60, FUNCT_1:9;
hence ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = Sq_Circ | D & h is continuous ) by A46, A47, A51, A52, A53, A54, JGRAPH_2:9; :: thesis: verum