set Y1 = |[(- 1),1]|;
reconsider B0 = {(0. (TOP-REAL 2))} as Subset of (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 = Out_In_Sq & 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 = Out_In_Sq & h is continuous )
then A2: D = B0 `
.= NonZero (TOP-REAL 2) by SUBSET_1:def 4 ;
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 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 A4: 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

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

end;

then x in [#] ((TOP-REAL 2) | D) by PRE_TOPC:def 5;
hence x in the carrier of ((TOP-REAL 2) | D) ; :: thesis: verum

end;

A5: NonZero (TOP-REAL 2) <> {} by Th9;
A6: 1.REAL 2 <> 0. (TOP-REAL 2) by Lm1, REVROT_1:19;
( ( (1.REAL 2) `2 <= (1.REAL 2) `1 & - ((1.REAL 2) `1) <= (1.REAL 2) `2 ) or ( (1.REAL 2) `2 >= (1.REAL 2) `1 & (1.REAL 2) `2 <= - ((1.REAL 2) `1) ) ) by Th5;
then 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 A6;
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;
A7: K0 = [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 5
.= the carrier of (((TOP-REAL 2) | D) | K0) ;
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

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) ) ;

now :: thesis: x in D

assume 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 A1, A9, TARSKI:def 1; :: thesis: verum

end;

then x in [#] ((TOP-REAL 2) | D) by PRE_TOPC:def 5;
hence x in the carrier of ((TOP-REAL 2) | D) ; :: thesis: verum

end;

( |[(- 1),1]| `1 = - 1 & |[(- 1),1]| `2 = 1 ) by EUCLID:52;
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 Th3;
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 = [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 5
.= the carrier of (((TOP-REAL 2) | D) | K1) ;
A11: the carrier of ((TOP-REAL 2) | D) = [#] ((TOP-REAL 2) | D)
.= D by PRE_TOPC:def 5 ;
A12: rng (Out_In_Sq | K1) c= the carrier of (((TOP-REAL 2) | D) | K1)

proof

reconsider K10 = K1 as Subset of (TOP-REAL 2) by A11, XBOOLE_1:1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Out_In_Sq | K1) or y in the carrier of (((TOP-REAL 2) | D) | K1) )
A13: 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 )
A14: the carrier of ((TOP-REAL 2) | K10) = [#] ((TOP-REAL 2) | K10)
.= K1 by PRE_TOPC:def 5 ;
assume q in the carrier of ((TOP-REAL 2) | K10) ; :: thesis: q `2 <> 0
then A15: 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 A14;

now :: thesis: not q `2 = 0

assume A16: q `2 = 0 ; :: thesis: contradiction
then q `1 = 0 by A15;
hence contradiction by A15, A16, EUCLID:53, EUCLID:54; :: thesis: verum

end;

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

end;

assume y in rng (Out_In_Sq | K1) ; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K1)
then consider x being object such that
A17: x in dom (Out_In_Sq | K1) and
A18: y = (Out_In_Sq | K1) . x by FUNCT_1:def 3;
A19: x in (dom Out_In_Sq) /\ K1 by A17, RELAT_1:61;
then A20: x in K1 by XBOOLE_0:def 4;
K1 c= the carrier of (TOP-REAL 2) by A11, XBOOLE_1:1;
then reconsider p = x as Point of (TOP-REAL 2) by A20;
A21: Out_In_Sq . p = y by A18, A20, FUNCT_1:49;
set p9 = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]|;
K10 = [#] ((TOP-REAL 2) | K10) by PRE_TOPC:def 5
.= the carrier of ((TOP-REAL 2) | K10) ;
then A22: p in the carrier of ((TOP-REAL 2) | K10) by A19, XBOOLE_0:def 4;

A23: now :: thesis: not |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| = 0. (TOP-REAL 2)

assume |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| = 0. (TOP-REAL 2) ; :: thesis: contradiction
then |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| `2 = 0 by EUCLID:52, EUCLID:54;
then 0 * (p `2) = (1 / (p `2)) * (p `2) by EUCLID:52;
hence contradiction by A22, A13, XCMPLX_1:87; :: thesis: verum

end;

A24: 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 A20;
then A25: Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| by Th14;

now :: thesis: ( ( p `2 >= 0 & y in K1 ) or ( p `2 < 0 & y in K1 ) )

per cases ( p `2 >= 0 or p `2 < 0 ) ;

case A26: p `2 >= 0 ; :: thesis: y in K1

then ( ( (p `1) / (p `2) <= (p `2) / (p `2) & (- (1 * (p `2))) / (p `2) <= (p `1) / (p `2) ) or ( p `1 >= p `2 & p `1 <= - (1 * (p `2)) ) ) by A24, XREAL_1:72;
then A27: ( ( (p `1) / (p `2) <= 1 & ((- 1) * (p `2)) / (p `2) <= (p `1) / (p `2) ) or ( p `1 >= p `2 & p `1 <= - (1 * (p `2)) ) ) by A22, A13, XCMPLX_1:60;
then A28: ( ( (p `1) / (p `2) <= 1 & - 1 <= (p `1) / (p `2) ) or ( (p `1) / (p `2) >= 1 & (p `1) / (p `2) <= ((- 1) * (p `2)) / (p `2) ) ) by A22, A13, A26, XCMPLX_1:89, XREAL_1:72;
( ( (p `1) / (p `2) <= 1 & - 1 <= (p `1) / (p `2) ) or ( (p `1) / (p `2) >= (p `2) / (p `2) & p `1 <= - (1 * (p `2)) ) ) by A22, A13, A26, A27, XCMPLX_1:89;
then (- 1) / (p `2) <= ((p `1) / (p `2)) / (p `2) by A26, XREAL_1:72;
then A29: ( ( ((p `1) / (p `2)) / (p `2) <= 1 / (p `2) & - (1 / (p `2)) <= ((p `1) / (p `2)) / (p `2) ) or ( ((p `1) / (p `2)) / (p `2) >= 1 / (p `2) & ((p `1) / (p `2)) / (p `2) <= - (1 / (p `2)) ) ) by A26, A28, XREAL_1:72;
( |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| `2 = 1 / (p `2) & |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| `1 = ((p `1) / (p `2)) / (p `2) ) by EUCLID:52;
hence y in K1 by A21, A23, A25, A29; :: thesis: verum

end;

case A30: p `2 < 0 ; :: thesis: y in K1

then ( ( p `1 <= p `2 & - (1 * (p `2)) <= p `1 ) or ( (p `1) / (p `2) <= (p `2) / (p `2) & (p `1) / (p `2) >= (- (1 * (p `2))) / (p `2) ) ) by A24, XREAL_1:73;
then A31: ( ( p `1 <= p `2 & - (1 * (p `2)) <= p `1 ) or ( (p `1) / (p `2) <= 1 & (p `1) / (p `2) >= ((- 1) * (p `2)) / (p `2) ) ) by A30, XCMPLX_1:60;
then ( ( (p `1) / (p `2) >= 1 & ((- 1) * (p `2)) / (p `2) >= (p `1) / (p `2) ) or ( (p `1) / (p `2) <= 1 & (p `1) / (p `2) >= - 1 ) ) by A30, XCMPLX_1:89;
then (- 1) / (p `2) >= ((p `1) / (p `2)) / (p `2) by A30, XREAL_1:73;
then A32: ( ( ((p `1) / (p `2)) / (p `2) <= 1 / (p `2) & - (1 / (p `2)) <= ((p `1) / (p `2)) / (p `2) ) or ( ((p `1) / (p `2)) / (p `2) >= 1 / (p `2) & ((p `1) / (p `2)) / (p `2) <= - (1 / (p `2)) ) ) by A30, A31, XREAL_1:73;
( |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| `2 = 1 / (p `2) & |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| `1 = ((p `1) / (p `2)) / (p `2) ) by EUCLID:52;
hence y in K1 by A21, A23, A25, A32; :: thesis: verum

end;

end;

end;

then y in [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 5;
hence y in the carrier of (((TOP-REAL 2) | D) | K1) ; :: thesis: verum

end;

A33: D c= K0 \/ K1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in K0 \/ K1 )
assume A34: 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 A2, A34, 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;

A35: NonZero (TOP-REAL 2) <> {} by Th9;
A36: K1 c= NonZero (TOP-REAL 2)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in K1 or z in NonZero (TOP-REAL 2) )
assume z in K1 ; :: thesis: z in NonZero (TOP-REAL 2)
then A37: 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) ) ;
then not z in {(0. (TOP-REAL 2))} by TARSKI:def 1;
hence z in NonZero (TOP-REAL 2) by A37, XBOOLE_0:def 5; :: thesis: verum

end;

A38: the carrier of ((TOP-REAL 2) | D) = [#] ((TOP-REAL 2) | D)
.= NonZero (TOP-REAL 2) by A2, PRE_TOPC:def 5 ;
A39: rng (Out_In_Sq | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)

proof

reconsider K00 = K0 as Subset of (TOP-REAL 2) by A11, XBOOLE_1:1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Out_In_Sq | K0) or y in the carrier of (((TOP-REAL 2) | D) | K0) )
A40: 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 )
A41: the carrier of ((TOP-REAL 2) | K00) = [#] ((TOP-REAL 2) | K00)
.= K0 by PRE_TOPC:def 5 ;
assume q in the carrier of ((TOP-REAL 2) | K00) ; :: thesis: q `1 <> 0
then A42: 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 A41;

now :: thesis: not q `1 = 0

assume A43: q `1 = 0 ; :: thesis: contradiction
then q `2 = 0 by A42;
hence contradiction by A42, A43, EUCLID:53, EUCLID:54; :: thesis: verum

end;

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

end;

assume y in rng (Out_In_Sq | K0) ; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K0)
then consider x being object such that
A44: x in dom (Out_In_Sq | K0) and
A45: y = (Out_In_Sq | K0) . x by FUNCT_1:def 3;
A46: x in (dom Out_In_Sq) /\ K0 by A44, RELAT_1:61;
then A47: x in K0 by XBOOLE_0:def 4;
K0 c= the carrier of (TOP-REAL 2) by A11, XBOOLE_1:1;
then reconsider p = x as Point of (TOP-REAL 2) by A47;
A48: Out_In_Sq . p = y by A45, A47, FUNCT_1:49;
set p9 = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]|;
K00 = [#] ((TOP-REAL 2) | K00) by PRE_TOPC:def 5
.= the carrier of ((TOP-REAL 2) | K00) ;
then A49: p in the carrier of ((TOP-REAL 2) | K00) by A46, XBOOLE_0:def 4;
A50: |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| `1 = 1 / (p `1) by EUCLID:52;

A51: now :: thesis: not |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| = 0. (TOP-REAL 2)

assume |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| = 0. (TOP-REAL 2) ; :: thesis: contradiction
then 0 * (p `1) = (1 / (p `1)) * (p `1) by A50, EUCLID:52, EUCLID:54;
hence contradiction by A49, A40, XCMPLX_1:87; :: thesis: verum

end;

A52: 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 A47;
then A53: Out_In_Sq . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| by Def1;
A54: p `1 <> 0 by A49, A40;

now :: thesis: ( ( p `1 >= 0 & y in K0 ) or ( p `1 < 0 & y in K0 ) )

per cases ( p `1 >= 0 or p `1 < 0 ) ;

case A55: p `1 >= 0 ; :: thesis: y in K0

( ( (p `2) / (p `1) <= (p `1) / (p `1) & (- (1 * (p `1))) / (p `1) <= (p `2) / (p `1) ) or ( p `2 >= p `1 & p `2 <= - (1 * (p `1)) ) ) by A52, A55, XREAL_1:72;
then A56: ( ( (p `2) / (p `1) <= 1 & ((- 1) * (p `1)) / (p `1) <= (p `2) / (p `1) ) or ( p `2 >= p `1 & p `2 <= - (1 * (p `1)) ) ) by A49, A40, XCMPLX_1:60;
then ( ( (p `2) / (p `1) <= 1 & - 1 <= (p `2) / (p `1) ) or ( (p `2) / (p `1) >= (p `1) / (p `1) & p `2 <= - (1 * (p `1)) ) ) by A49, A40, A55, XCMPLX_1:89;
then (- 1) / (p `1) <= ((p `2) / (p `1)) / (p `1) by A55, XREAL_1:72;
then A57: ( ( ((p `2) / (p `1)) / (p `1) <= 1 / (p `1) & - (1 / (p `1)) <= ((p `2) / (p `1)) / (p `1) ) or ( ((p `2) / (p `1)) / (p `1) >= 1 / (p `1) & ((p `2) / (p `1)) / (p `1) <= - (1 / (p `1)) ) ) by A54, A55, A56, XREAL_1:72;
( |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| `1 = 1 / (p `1) & |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| `2 = ((p `2) / (p `1)) / (p `1) ) by EUCLID:52;
hence y in K0 by A48, A51, A53, A57; :: thesis: verum

end;

case A58: p `1 < 0 ; :: thesis: y in K0

A59: - (1 / (p `1)) = (- 1) / (p `1) ;
( ( p `2 <= p `1 & - (1 * (p `1)) <= p `2 ) or ( (p `2) / (p `1) <= (p `1) / (p `1) & (p `2) / (p `1) >= (- (1 * (p `1))) / (p `1) ) ) by A52, A58, XREAL_1:73;
then A60: ( ( p `2 <= p `1 & - (1 * (p `1)) <= p `2 ) or ( (p `2) / (p `1) <= 1 & (p `2) / (p `1) >= ((- 1) * (p `1)) / (p `1) ) ) by A58, XCMPLX_1:60;
then ( ( (p `2) / (p `1) >= (p `1) / (p `1) & - (1 * (p `1)) <= p `2 ) or ( (p `2) / (p `1) <= 1 & (p `2) / (p `1) >= - 1 ) ) by A58, XCMPLX_1:89;
then (- 1) / (p `1) >= ((p `2) / (p `1)) / (p `1) by A58, XREAL_1:73;
then A61: ( ( ((p `2) / (p `1)) / (p `1) <= 1 / (p `1) & (- 1) / (p `1) <= ((p `2) / (p `1)) / (p `1) ) or ( ((p `2) / (p `1)) / (p `1) >= 1 / (p `1) & ((p `2) / (p `1)) / (p `1) <= - (1 / (p `1)) ) ) by A58, A60, XREAL_1:73;
( |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| `1 = 1 / (p `1) & |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| `2 = ((p `2) / (p `1)) / (p `1) ) by EUCLID:52;
hence y in K0 by A48, A51, A53, A61, A59; :: thesis: verum

end;

end;

end;

then y in [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 5;
hence y in the carrier of (((TOP-REAL 2) | D) | K0) ; :: thesis: verum

end;

A62: K0 c= NonZero (TOP-REAL 2)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in K0 or z in NonZero (TOP-REAL 2) )
assume z in K0 ; :: thesis: z in NonZero (TOP-REAL 2)
then A63: 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) ) ;
then not z in {(0. (TOP-REAL 2))} by TARSKI:def 1;
hence z in NonZero (TOP-REAL 2) by A63, XBOOLE_0:def 5; :: thesis: verum

end;

dom (Out_In_Sq | K0) = (dom Out_In_Sq) /\ K0 by RELAT_1:61
.= (NonZero (TOP-REAL 2)) /\ K0 by A5, FUNCT_2:def 1
.= K0 by A62, XBOOLE_1:28 ;
then reconsider f = Out_In_Sq | K0 as Function of (((TOP-REAL 2) | D) | K0),((TOP-REAL 2) | D) by A7, A39, FUNCT_2:2, XBOOLE_1:1;
A64: K1 = [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 5;
dom (Out_In_Sq | K1) = (dom Out_In_Sq) /\ K1 by RELAT_1:61
.= (NonZero (TOP-REAL 2)) /\ K1 by A35, FUNCT_2:def 1
.= K1 by A36, XBOOLE_1:28 ;
then reconsider g = Out_In_Sq | K1 as Function of (((TOP-REAL 2) | D) | K1),((TOP-REAL 2) | D) by A10, A12, FUNCT_2:2, XBOOLE_1:1;
A65: dom g = K1 by A10, FUNCT_2:def 1;
g = Out_In_Sq | K1 ;
then A66: K1 is closed by A2, Th39;
A67: K0 = [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 5;
A68: for x being object st x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) holds
f . x = g . x

proof

let x be object ; :: thesis: ( x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) implies f . x = g . x )
assume A69: x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) ; :: thesis: f . x = g . x
then x in K0 by A67, XBOOLE_0:def 4;
then f . x = Out_In_Sq . x by FUNCT_1:49;
hence f . x = g . x by A64, A69, FUNCT_1:49; :: thesis: verum

end;

f = Out_In_Sq | K0 ;
then A70: K0 is closed by A2, Th38;
A71: dom f = K0 by A7, FUNCT_2:def 1;
D = [#] ((TOP-REAL 2) | D) by PRE_TOPC:def 5;
then A72: ([#] (((TOP-REAL 2) | D) | K0)) \/ ([#] (((TOP-REAL 2) | D) | K1)) = [#] ((TOP-REAL 2) | D) by A67, A64, A33;
A73: ( f is continuous & g is continuous ) by A2, Th38, Th39;
then consider h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) such that
A74: h = f +* g and
h is continuous by A67, A64, A72, A70, A66, A68, Th1;
( K0 = [#] (((TOP-REAL 2) | D) | K0) & K1 = [#] (((TOP-REAL 2) | D) | K1) ) by PRE_TOPC:def 5;
then A75: f tolerates g by A68, A71, A65, PARTFUN1:def 4;
A76: for x being object st x in dom h holds
h . x = Out_In_Sq . x

proof

let x be object ; :: thesis: ( x in dom h implies h . x = Out_In_Sq . x )
assume A77: x in dom h ; :: thesis: h . x = Out_In_Sq . x
then reconsider p = x as Point of (TOP-REAL 2) by A38, XBOOLE_0:def 5;
not x in {(0. (TOP-REAL 2))} by A38, A77, XBOOLE_0:def 5;
then A78: x <> 0. (TOP-REAL 2) by TARSKI:def 1;

now :: thesis: ( ( x in K0 & h . x = Out_In_Sq . x ) or ( not x in K0 & h . x = Out_In_Sq . x ) )

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

case A79: x in K0 ; :: thesis: h . x = Out_In_Sq . x

h . p = (g +* f) . p by A74, A75, FUNCT_4:34
.= f . p by A71, A79, FUNCT_4:13 ;
hence h . x = Out_In_Sq . x by A79, FUNCT_1:49; :: thesis: verum

end;

case not x in K0 ; :: thesis: h . x = Out_In_Sq . x

then ( not ( p `2 <= p `1 & - (p `1) <= p `2 ) & not ( p `2 >= p `1 & p `2 <= - (p `1) ) ) by A78;
then ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) by XREAL_1:26;
then A80: x in K1 by A78;
then Out_In_Sq . p = g . p by FUNCT_1:49;
hence h . x = Out_In_Sq . x by A74, A65, A80, FUNCT_4:13; :: thesis: verum

end;

end;

end;

hence h . x = Out_In_Sq . x ; :: thesis: verum

end;

( dom h = the carrier of ((TOP-REAL 2) | D) & dom Out_In_Sq = the carrier of ((TOP-REAL 2) | D) ) by A38, FUNCT_2:def 1;
then f +* g = Out_In_Sq by A74, A76, FUNCT_1:2;
hence ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = Out_In_Sq & h is continuous ) by A67, A64, A72, A70, A73, A66, A68, Th1; :: thesis: verum