let D be non empty Subset of (TOP-REAL 2); :: thesis: ( D ` = {(0.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.REAL 2)} ; :: thesis: ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = Out_In_Sq & h is continuous )
reconsider B0 = {(0.REAL 2)} as Subset of (TOP-REAL 2) ;
A2: D = B0 ` by A1
.= the carrier of (TOP-REAL 2) \ {(0.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.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.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.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.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;
then x in [#] ((TOP-REAL 2) | D) by PRE_TOPC:def 10;
hence x in the carrier of ((TOP-REAL 2) | D) ; :: thesis: verum
end;
( ( ( (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 ) ) ) & 1.REAL 2 <> 0.REAL 2 ) by Th13, REVROT_1:19;
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.REAL 2 ) } ;
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.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.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.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.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.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;
then x in [#] ((TOP-REAL 2) | D) by PRE_TOPC:def 10;
hence x in the carrier of ((TOP-REAL 2) | D) ; :: 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.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.REAL 2 ) } as non empty Subset of ((TOP-REAL 2) | D) by A5;
A7: the carrier of ((TOP-REAL 2) | D) = [#] ((TOP-REAL 2) | D)
.= D by PRE_TOPC:def 10 ;
A8: K0 c= the carrier of (TOP-REAL 2) \ {(0.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) \ {(0.REAL 2)} )
assume z in K0 ; :: thesis: z in the carrier of (TOP-REAL 2) \ {(0.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.REAL 2 ) ;
( z in the carrier of (TOP-REAL 2) & not z in {(0.REAL 2)} ) by A9, TARSKI:def 1;
hence z in the carrier of (TOP-REAL 2) \ {(0.REAL 2)} by XBOOLE_0:def 5; :: thesis: verum
end;
A10: the carrier of (TOP-REAL 2) \ {(0.REAL 2)} <> {} by Th19;
A11: dom (Out_In_Sq | K0) = (dom Out_In_Sq ) /\ K0 by FUNCT_1:68
.= (the carrier of (TOP-REAL 2) \ {(0.REAL 2)}) /\ K0 by A10, FUNCT_2:def 1
.= K0 by A8, XBOOLE_1:28 ;
A12: K0 = [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 10
.= the carrier of (((TOP-REAL 2) | D) | K0) ;
rng (Out_In_Sq | 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 (Out_In_Sq | K0) or y in the carrier of (((TOP-REAL 2) | D) | K0) )
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
A13: ( x in dom (Out_In_Sq | K0) & y = (Out_In_Sq | K0) . x ) by FUNCT_1:def 5;
A14: x in (dom Out_In_Sq ) /\ K0 by A13, FUNCT_1:68;
then A15: 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 A15;
A16: Out_In_Sq . p = y by A13, A15, FUNCT_1:72;
consider px being Point of (TOP-REAL 2) such that
A17: ( x = px & ( ( px `2 <= px `1 & - (px `1 ) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1 ) ) ) & px <> 0.REAL 2 ) by A15;
reconsider K00 = K0 as Subset of (TOP-REAL 2) by A7, XBOOLE_1:1;
K00 = [#] ((TOP-REAL 2) | K00) by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL 2) | K00) ;
then A18: p in the carrier of ((TOP-REAL 2) | K00) by A14, XBOOLE_0:def 4;
A19: 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 A20: q in the carrier of ((TOP-REAL 2) | K00) ; :: thesis: q `1 <> 0
the carrier of ((TOP-REAL 2) | K00) = [#] ((TOP-REAL 2) | K00)
.= K0 by PRE_TOPC:def 10 ;
then consider p3 being Point of (TOP-REAL 2) such that
A21: ( q = p3 & ( ( p3 `2 <= p3 `1 & - (p3 `1 ) <= p3 `2 ) or ( p3 `2 >= p3 `1 & p3 `2 <= - (p3 `1 ) ) ) & p3 <> 0.REAL 2 ) by A20;
hence q `1 <> 0 ; :: thesis: verum
end;
then A23: p `1 <> 0 by A18;
set p9 = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]|;
A24: ( |[(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:56;
A25: now
assume |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| = 0.REAL 2 ; :: thesis: contradiction
then 0 * (p `1 ) = (1 / (p `1 )) * (p `1 ) by A24, EUCLID:56, EUCLID:58;
hence contradiction by A18, A19, XCMPLX_1:88; :: thesis: verum
end;
A26: Out_In_Sq . p = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| by A17, Def1;
now
per cases ( p `1 >= 0 or p `1 < 0 ) ;
case A27: p `1 >= 0 ; :: thesis: y in K0
then ( ( (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 A17, XREAL_1:74;
then B28: ( ( (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 A18, A19, XCMPLX_1:60;
then A28: ( ( (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 A18, A19, A27, XCMPLX_1:90;
( not (p `2 ) / (p `1 ) >= 1 or not (p `2 ) / (p `1 ) <= - 1 ) ;
then (- 1) / (p `1 ) <= ((p `2 ) / (p `1 )) / (p `1 ) by A19, A18, A27, A28, XCMPLX_1:60, XREAL_1:74;
then A30: ( ( ((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 A23, A27, B28, XREAL_1:74;
( |[(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:56;
hence y in K0 by A16, A25, A26, A30; :: thesis: verum
end;
case A31: p `1 < 0 ; :: thesis: y in K0
then ( ( 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 A17, XREAL_1:75;
then B32: ( ( 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 A31, XCMPLX_1:60;
then A32: ( ( (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 A31, XCMPLX_1:90;
( not (p `2 ) / (p `1 ) >= 1 or not (p `2 ) / (p `1 ) <= - 1 ) ;
then (- 1) / (p `1 ) >= ((p `2 ) / (p `1 )) / (p `1 ) by A31, A32, XCMPLX_1:60, XREAL_1:75;
then A34: ( ( ((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 A31, B32, XREAL_1:75;
( |[(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:56;
hence y in K0 by A16, A25, A26, A34; :: thesis: verum
end;
end;
end;
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 = Out_In_Sq | K0 as Function of (((TOP-REAL 2) | D) | K0),((TOP-REAL 2) | D) by A11, A12, FUNCT_2:4, XBOOLE_1:1;
A35: K1 c= the carrier of (TOP-REAL 2) \ {(0.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) \ {(0.REAL 2)} )
assume z in K1 ; :: thesis: z in the carrier of (TOP-REAL 2) \ {(0.REAL 2)}
then consider p8 being Point of (TOP-REAL 2) such that
A36: ( p8 = z & ( ( p8 `1 <= p8 `2 & - (p8 `2 ) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2 ) ) ) & p8 <> 0.REAL 2 ) ;
( z in the carrier of (TOP-REAL 2) & not z in {(0.REAL 2)} ) by A36, TARSKI:def 1;
hence z in the carrier of (TOP-REAL 2) \ {(0.REAL 2)} by XBOOLE_0:def 5; :: thesis: verum
end;
A37: the carrier of (TOP-REAL 2) \ {(0.REAL 2)} <> {} by Th19;
A38: dom (Out_In_Sq | K1) = (dom Out_In_Sq ) /\ K1 by FUNCT_1:68
.= (the carrier of (TOP-REAL 2) \ {(0.REAL 2)}) /\ K1 by A37, FUNCT_2:def 1
.= K1 by A35, XBOOLE_1:28 ;
A39: K1 = [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 10
.= the carrier of (((TOP-REAL 2) | D) | K1) ;
rng (Out_In_Sq | 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 (Out_In_Sq | K1) or y in the carrier of (((TOP-REAL 2) | D) | K1) )
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
A40: ( x in dom (Out_In_Sq | K1) & y = (Out_In_Sq | K1) . x ) by FUNCT_1:def 5;
A41: x in (dom Out_In_Sq ) /\ K1 by A40, FUNCT_1:68;
then A42: x in K1 by XBOOLE_0:def 4;
K1 c= the carrier of (TOP-REAL 2) by A7, XBOOLE_1:1;
then reconsider p = x as Point of (TOP-REAL 2) by A42;
A43: Out_In_Sq . p = y by A40, A42, FUNCT_1:72;
consider px being Point of (TOP-REAL 2) such that
A44: ( x = px & ( ( px `1 <= px `2 & - (px `2 ) <= px `1 ) or ( px `1 >= px `2 & px `1 <= - (px `2 ) ) ) & px <> 0.REAL 2 ) by A42;
reconsider K10 = K1 as Subset of (TOP-REAL 2) by A7, XBOOLE_1:1;
K10 = [#] ((TOP-REAL 2) | K10) by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL 2) | K10) ;
then A45: p in the carrier of ((TOP-REAL 2) | K10) by A41, XBOOLE_0:def 4;
A46: 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 A47: q in the carrier of ((TOP-REAL 2) | K10) ; :: thesis: q `2 <> 0
the carrier of ((TOP-REAL 2) | K10) = [#] ((TOP-REAL 2) | K10)
.= K1 by PRE_TOPC:def 10 ;
then consider p3 being Point of (TOP-REAL 2) such that
A48: ( q = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2 ) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2 ) ) ) & p3 <> 0.REAL 2 ) by A47;
hence q `2 <> 0 ; :: thesis: verum
end;
set p9 = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]|;
A51: now
assume |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| = 0.REAL 2 ; :: thesis: contradiction
then ( |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| `2 = 0 & |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| `1 = 0 ) by EUCLID:56, EUCLID:58;
then 0 * (p `2 ) = (1 / (p `2 )) * (p `2 ) by EUCLID:56;
hence contradiction by A45, A46, XCMPLX_1:88; :: thesis: verum
end;
A52: Out_In_Sq . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| by A44, Th24;
now
per cases ( p `2 >= 0 or p `2 < 0 ) ;
case A53: 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 A44, XREAL_1:74;
then B54: ( ( (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 A45, A46, XCMPLX_1:60;
then A54: ( ( (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 A45, A46, A53, XCMPLX_1:90;
A55: ( ( (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 A46, A45, A53, B54, XCMPLX_1:90, XREAL_1:74;
( not (p `1 ) / (p `2 ) >= 1 or not (p `1 ) / (p `2 ) <= - 1 ) ;
then (- 1) / (p `2 ) <= ((p `1 ) / (p `2 )) / (p `2 ) by A45, A46, A53, A54, XCMPLX_1:60, XREAL_1:74;
then A56: ( ( ((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 A53, A55, XREAL_1:74;
( |[(((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:56;
hence y in K1 by A43, A51, A52, A56; :: thesis: verum
end;
case A57: 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 A44, XREAL_1:75;
then B58: ( ( 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 A57, 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 A57, XCMPLX_1:90;
then (- 1) / (p `2 ) >= ((p `1 ) / (p `2 )) / (p `2 ) by A57, XREAL_1:75;
then A59: ( ( ((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 B58, A57, XREAL_1:75;
( |[(((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:56;
hence y in K1 by A43, A51, A52, A59; :: thesis: verum
end;
end;
end;
then y in [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 10;
hence y in the carrier of (((TOP-REAL 2) | D) | K1) ; :: thesis: verum
end;
then reconsider g = Out_In_Sq | K1 as Function of (((TOP-REAL 2) | D) | K1),((TOP-REAL 2) | D) by A38, A39, FUNCT_2:4, XBOOLE_1:1;
A60: K0 = [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 10;
A61: K1 = [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 10;
A62: 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 A67: x in D ; :: thesis: x in K0 \/ K1
then A68: ( x in the carrier of (TOP-REAL 2) & not x in {(0.REAL 2)} ) by A2, XBOOLE_0:def 5;
reconsider px = x as Point of (TOP-REAL 2) by A67;
( ( ( ( px `2 <= px `1 & - (px `1 ) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1 ) ) ) & px <> 0.REAL 2 ) or ( ( ( px `1 <= px `2 & - (px `2 ) <= px `1 ) or ( px `1 >= px `2 & px `1 <= - (px `2 ) ) ) & px <> 0.REAL 2 ) ) by A68, 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 A69: ([#] (((TOP-REAL 2) | D) | K0)) \/ ([#] (((TOP-REAL 2) | D) | K1)) = [#] ((TOP-REAL 2) | D) by A60, A61, A62, XBOOLE_0:def 10;
( f = Out_In_Sq | K0 & D = the carrier of (TOP-REAL 2) \ {(0.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.REAL 2 ) } ) by A2;
then A70: ( f is continuous & K0 is closed ) by Th48;
( g = Out_In_Sq | K1 & D = the carrier of (TOP-REAL 2) \ {(0.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.REAL 2 ) } ) by A2;
then A71: ( g is continuous & K1 is closed ) by Th49;
A72: 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 Z: 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 A60, A61, XBOOLE_0:def 4;
then f . x = Out_In_Sq . x by FUNCT_1:72;
hence f . x = g . x by Z, A61, FUNCT_1:72; :: thesis: verum
end;
then consider h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) such that
A74: ( h = f +* g & h is continuous ) by A60, A61, A69, A70, A71, Th9;
A75: dom h = the carrier of ((TOP-REAL 2) | D) by FUNCT_2:def 1;
A76: the carrier of ((TOP-REAL 2) | D) = [#] ((TOP-REAL 2) | D)
.= the carrier of (TOP-REAL 2) \ {(0.REAL 2)} by A2, PRE_TOPC:def 10 ;
then A77: dom Out_In_Sq = the carrier of ((TOP-REAL 2) | D) by FUNCT_2:def 1;
A78: dom f = K0 by A12, FUNCT_2:def 1;
A79: K0 = [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 10;
A80: dom g = K1 by A39, FUNCT_2:def 1;
K1 = [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 10;
then A81: f tolerates g by A72, A78, A79, A80, PARTFUN1:def 6;
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 A82: x in dom h ; :: thesis: h . x = Out_In_Sq . x
then ( x in the carrier of (TOP-REAL 2) & not x in {(0.REAL 2)} ) by A76, XBOOLE_0:def 5;
then A83: x <> 0.REAL 2 by TARSKI:def 1;
reconsider p = x as Point of (TOP-REAL 2) by A76, A82, XBOOLE_0:def 5;
now
per cases ( x in K0 or not x in K0 ) ;
case A84: x in K0 ; :: thesis: h . x = Out_In_Sq . x
h . p = (g +* f) . p by A74, A81, FUNCT_4:35
.= f . p by A78, A84, FUNCT_4:14 ;
hence h . x = Out_In_Sq . x by A84, FUNCT_1:72; :: 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 A83;
then ( ( p `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) by XREAL_1:28;
then A85: x in K1 by A83;
then Out_In_Sq . p = g . p by FUNCT_1:72;
hence h . x = Out_In_Sq . x by A74, A80, A85, FUNCT_4:14; :: thesis: verum
end;
end;
end;
hence h . x = Out_In_Sq . x ; :: thesis: verum
end;
then f +* g = Out_In_Sq by A74, A75, A77, FUNCT_1:9;
hence ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = Out_In_Sq & h is continuous ) by A60, A61, A69, A70, A71, A72, Th9; :: thesis: verum