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

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 Th19;
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 Th13;
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 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 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

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 Th11;
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 set ; :: 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

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 set 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

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

now

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;
A29: ( not (p `1) / (p `2) >= 1 or not (p `1) / (p `2) <= - 1 ) ;
( ( (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 A22, A13, A26, A29, XCMPLX_1:60, XREAL_1:72;
then A30: ( ( ((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, A30; :: thesis: verum

end;

case A31: 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 A32: ( ( 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 A31, 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 A31, XCMPLX_1:89;
then (- 1) / (p `2) >= ((p `1) / (p `2)) / (p `2) by A31, XREAL_1:73;
then A33: ( ( ((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 A31, A32, 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, A33; :: 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;

A34: 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 A35: 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, A35, 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;

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

proof

let z be set ; :: 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 A38: 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 A38, XBOOLE_0:def 5; :: thesis: verum

end;

A39: the carrier of ((TOP-REAL 2) | D) = [#] ((TOP-REAL 2) | D)
.= NonZero (TOP-REAL 2) by A2, PRE_TOPC:def 5 ;
A40: 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 set ; :: 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) )
A41: 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 )
A42: 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 A43: 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 A42;

now

assume A44: q `1 = 0 ; :: thesis: contradiction
then q `2 = 0 by A43;
hence contradiction by A43, A44, 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 set such that
A45: x in dom (Out_In_Sq | K0) and
A46: y = (Out_In_Sq | K0) . x by FUNCT_1:def 3;
A47: x in (dom Out_In_Sq) /\ K0 by A45, RELAT_1:61;
then A48: 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 A48;
A49: Out_In_Sq . p = y by A46, A48, 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 A50: p in the carrier of ((TOP-REAL 2) | K00) by A47, XBOOLE_0:def 4;
A51: |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| `1 = 1 / (p `1) by EUCLID:52;

A52: now

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 A51, EUCLID:52, EUCLID:54;
hence contradiction by A50, A41, XCMPLX_1:87; :: thesis: verum

end;

A53: 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 A48;
then A54: Out_In_Sq . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| by Def1;
A55: p `1 <> 0 by A50, A41;

now

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

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

A57: ( not (p `2) / (p `1) >= 1 or not (p `2) / (p `1) <= - 1 ) ;
( ( (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 A53, A56, XREAL_1:72;
then A58: ( ( (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 A50, A41, 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 A50, A41, A56, XCMPLX_1:89;
then (- 1) / (p `1) <= ((p `2) / (p `1)) / (p `1) by A50, A41, A56, A57, XCMPLX_1:60, XREAL_1:72;
then A59: ( ( ((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 A55, A56, A58, 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 A49, A52, A54, A59; :: thesis: verum

end;

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

A61: ( not (p `2) / (p `1) >= 1 or not (p `2) / (p `1) <= - 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 A53, A60, XREAL_1:73;
then A62: ( ( 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 A60, 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 A60, XCMPLX_1:89;
then (- 1) / (p `1) >= ((p `2) / (p `1)) / (p `1) by A60, A61, XCMPLX_1:60, XREAL_1:73;
then A63: ( ( ((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 A60, A62, 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 A49, A52, A54, A63; :: 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;

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

proof

let z be set ; :: 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 A65: 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 A65, 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 A64, XBOOLE_1:28 ;
then reconsider f = Out_In_Sq | K0 as Function of (((TOP-REAL 2) | D) | K0),((TOP-REAL 2) | D) by A7, A40, FUNCT_2:2, XBOOLE_1:1;
A66: 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 A36, FUNCT_2:def 1
.= K1 by A37, 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;
A67: dom g = K1 by A10, FUNCT_2:def 1;
g = Out_In_Sq | K1 ;
then A68: K1 is closed by A2, Th49;
A69: K0 = [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 5;
A70: 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 A71: x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) ; :: thesis: f . x = g . x
then x in K0 by A69, XBOOLE_0:def 4;
then f . x = Out_In_Sq . x by FUNCT_1:49;
hence f . x = g . x by A66, A71, FUNCT_1:49; :: thesis: verum

end;

f = Out_In_Sq | K0 ;
then A72: K0 is closed by A2, Th48;
A73: dom f = K0 by A7, FUNCT_2:def 1;
D = [#] ((TOP-REAL 2) | D) by PRE_TOPC:def 5;
then A74: ([#] (((TOP-REAL 2) | D) | K0)) \/ ([#] (((TOP-REAL 2) | D) | K1)) = [#] ((TOP-REAL 2) | D) by A69, A66, A34, XBOOLE_0:def 10;
A75: ( f is continuous & g is continuous ) by A2, Th48, Th49;
then consider h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) such that
A76: h = f +* g and
h is continuous by A69, A66, A74, A72, A68, A70, Th9;
( K0 = [#] (((TOP-REAL 2) | D) | K0) & K1 = [#] (((TOP-REAL 2) | D) | K1) ) by PRE_TOPC:def 5;
then A77: f tolerates g by A70, A73, A67, PARTFUN1:def 4;
A78: for x being set st x in dom h holds
h . x = Out_In_Sq . x

proof

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

now

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

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

h . p = (g +* f) . p by A76, A77, FUNCT_4:34
.= f . p by A73, A81, FUNCT_4:13 ;
hence h . x = Out_In_Sq . x by A81, 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 A80;
then ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) by XREAL_1:26;
then A82: x in K1 by A80;
then Out_In_Sq . p = g . p by FUNCT_1:49;
hence h . x = Out_In_Sq . x by A76, A67, A82, 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 A39, FUNCT_2:def 1;
then f +* g = Out_In_Sq by A76, A78, 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 A69, A66, A74, A72, A75, A68, A70, Th9; :: thesis: verum