0 and A4: Ball(q2,r) c= GG by A2,TOPMETR:15; set s=r/sqrt(2); A5: Ball(q2,r)= {q3 where q3 is Point of TOP-REAL 2: |.p-q3.|q`1-s by A9,XREAL_1:14; then A12: p`1-q`1>q`1+-s-q`1 by XREAL_1:14; p`2+s-s>q`2-s by A11,XREAL_1:14; then A13: p`2-q`2>q`2+-s-q`2 by XREAL_1:14; p`2-s+s 0 by A3,XREAL_1:139; hence thesis by A4,A6,XBOOLE_1:1; end; theorem Th12: for X,Y,Z being non empty TopSpace, B being Subset of Y, C being Subset of Z, f being Function of X,Y, h being Function of Y|B,Z|C st f is continuous & h is continuous & rng f c= B & B<>{} & C<>{} holds ex g being Function of X,Z st g is continuous & g=h*f proof let X,Y,Z be non empty TopSpace, B be Subset of Y, C be Subset of Z, f be Function of X,Y, h be Function of Y|B,Z|C; assume that A1: f is continuous and A2: h is continuous and A3: rng f c= B and A4: B<>{} and A5: C<>{}; A6: the carrier of X=dom f by FUNCT_2:def 1; the carrier of Y|B=[#](Y|B) .=B by PRE_TOPC:def 5; then reconsider u=f as Function of X,Y|B by A3,A6,FUNCT_2:2; reconsider V=B as non empty Subset of Y by A4; Y|V is non empty; then reconsider H=Y|B as non empty TopSpace; reconsider F=C as non empty Subset of Z by A5; reconsider k=u as Function of X,H; Z|F is non empty; then reconsider G=Z|C as non empty TopSpace; reconsider j=h as Function of H,G; A7: the carrier of (Z|C)=[#](Z|C) .=C by PRE_TOPC:def 5; j*k is Function of X,G; then reconsider v=h*u as Function of X,Z by A7,FUNCT_2:7; u is continuous by A1,TOPMETR:6; then v is continuous by A2,A4,A5,PRE_TOPC:26; hence thesis; end; reserve p,q for Point of TOP-REAL 2; definition func Out_In_Sq -> Function of NonZero TOP-REAL 2, NonZero TOP-REAL 2 means : Def1: for p being Point of TOP-REAL 2 st p<>0.TOP-REAL 2 holds ((p`2<=p`1 & -p `1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies it.p=|[1/p`1,p`2/p`1/p`1]|) & (not(p`2 <=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies it.p=|[p`1/p`2/p`2,1/p`2]|); existence proof reconsider BP= NonZero TOP-REAL 2 as non empty set by Th9; defpred P[set,set] means (for p being Point of TOP-REAL 2 st p=$1 holds (( p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)implies $2=|[1/p`1,p`2/p`1/p`1]|) & (not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies $2=|[p`1/p`2/p`2,1 /p`2]|)); A1: for x being Element of BP ex y being Element of BP st P[x,y] proof let x be Element of BP; reconsider q=x as Point of TOP-REAL 2 by TARSKI:def 3; now per cases; case A2: q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1; now assume |[1/q`1,q`2/q`1/q`1]| in {0.TOP-REAL 2}; then 0.TOP-REAL 2= |[1/q`1,q`2/q`1/q`1]| by TARSKI:def 1; then 0=1/q`1 by Th3,EUCLID:52; then A3: 0=1/q`1*q`1; now per cases; case A4: q`1=0; then q`2=0 by A2; then q=0.TOP-REAL 2 by A4,EUCLID:53,54; then q in {0.TOP-REAL 2} by TARSKI:def 1; hence contradiction by XBOOLE_0:def 5; end; case q`1<>0; hence contradiction by A3,XCMPLX_1:87; end; end; hence contradiction; end; then reconsider r= |[1/q`1,q`2/q`1/q`1]| as Element of BP by XBOOLE_0:def 5; for p being Point of TOP-REAL 2 st p=x holds ((p`2<=p`1 & -p`1 <=p`2 or p`2>=p`1 & p`2<=-p`1)implies r=|[1/p`1,p`2/p`1/p`1]|) & (not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies r=|[p`1/p`2/p`2,1/p`2]|) by A2; hence thesis; end; case A5: not (q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1); now assume |[q`1/q`2/q`2,1/q`2]| in {0.TOP-REAL 2}; then 0.TOP-REAL 2= |[q`1/q`2/q`2,1/q`2]| by TARSKI:def 1; then (0.TOP-REAL 2)`2=1/q`2 by EUCLID:52; then A6: 0=1/q`2*q`2 by Th3; q`2 <> 0 by A5; hence contradiction by A6,XCMPLX_1:87; end; then reconsider r= |[q`1/q`2/q`2,1/q`2]| as Element of BP by XBOOLE_0:def 5; for p being Point of TOP-REAL 2 st p=x holds ((p`2<=p`1 & -p`1 <=p`2 or p`2>=p`1 & p`2<=-p`1)implies r=|[1/p`1,p`2/p`1/p`1]|) & (not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies r=|[p`1/p`2/p`2,1/p`2]|) by A5; hence thesis; end; end; hence thesis; end; ex h being Function of BP, BP st for x being Element of BP holds P[x, h.x] from FUNCT_2:sch 3(A1); then consider h being Function of BP, BP such that A7: for x being Element of BP holds for p being Point of TOP-REAL 2 st p=x holds ((p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)implies h.x=|[1/p`1 ,p`2/p`1/p`1]|) & (not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies h. x=|[p`1/p`2/p`2,1/p`2]|); for p being Point of TOP-REAL 2 st p<>0.TOP-REAL 2 holds ((p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)implies h.p=|[1/p`1,p`2/p`1/p`1]|) & (not(p`2 <=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies h.p=|[p`1/p`2/p`2,1/p`2]|) proof let p be Point of TOP-REAL 2; assume p<>0.TOP-REAL 2; then not p in {0.TOP-REAL 2} by TARSKI:def 1; then p in NonZero TOP-REAL 2 by XBOOLE_0:def 5; hence thesis by A7; end; hence thesis; end; uniqueness proof let h1,h2 be Function of NonZero TOP-REAL 2, NonZero TOP-REAL 2; assume that A8: for p being Point of TOP-REAL 2 st p<>0.TOP-REAL 2 holds ((p`2<=p `1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)implies h1.p=|[1/p`1,p`2/p`1/p`1]|) & ( not(p `2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies h1.p=|[p`1/p`2/p`2,1 /p`2]| ) and A9: for p being Point of TOP-REAL 2 st p<>0.TOP-REAL 2 holds ((p`2<=p `1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)implies h2.p=|[1/p`1,p`2/p`1/p`1]|) & ( not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies h2.p=|[p`1/p`2/p`2,1/ p`2]|); for x being object st x in NonZero TOP-REAL 2 holds h1.x=h2.x proof let x be object; assume A10: x in NonZero TOP-REAL 2; then reconsider q=x as Point of TOP-REAL 2; not q in {0.TOP-REAL 2} by A10,XBOOLE_0:def 5; then A11: q<>0.TOP-REAL 2 by TARSKI:def 1; now per cases; case A12: q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1; then h1.q=|[1/q`1,q`2/q`1/q`1]| by A8,A11; hence thesis by A9,A11,A12; end; case A13: not (q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1); then h1.q=|[q`1/q`2/q`2,1/q`2]| by A8,A11; hence thesis by A9,A11,A13; end; end; hence thesis; end; hence h1=h2 by FUNCT_2:12; end; end; theorem Th13: for p being Point of TOP-REAL 2 st not(p`2<=p`1 & -p`1<=p`2 or p `2>=p`1 & p`2<=-p`1) holds p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2 proof let p being Point of TOP-REAL 2; A1: -p`1-p`2 by XREAL_1:24; A2: -p`1>p`2 implies --p`1<-p`2 by XREAL_1:24; assume not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1); hence thesis by A1,A2; end; theorem Th14: for p being Point of TOP-REAL 2 st p<>0.TOP-REAL 2 holds ((p`1<= p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2)implies Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2 ]|) & (not (p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) implies Out_In_Sq.p= |[1/p`1,p`2/p`1/p`1]|) proof let p be Point of TOP-REAL 2; assume A1: p<>0.TOP-REAL 2; hereby assume A2: p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2; now per cases by A2; case A3: p`1<=p`2 & -p`2<=p`1; now assume A4: p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1; A5: now per cases by A4; case p`2<=p`1 & -p`1<=p`2; hence p`1=p`2 or p`1=-p`2 by A3,XXREAL_0:1; end; case p`2>=p`1 & p`2<=-p`1; then -p`2>=--p`1 by XREAL_1:24; hence p`1=p`2 or p`1=-p`2 by A3,XXREAL_0:1; end; end; now per cases by A5; case A6: p`1=p`2; then p`1<>0 by A1,EUCLID:53,54; then p`1/p`2/p`2=1/p`1 by A6,XCMPLX_1:60; hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A1,A4,A6,Def1; end; case A7: p`1=-p`2; then A8: p`2<>0 by A1,EUCLID:53,54; A9: p`1/p`2/p`2=(-(p`2/p`2))/p`2 by A7 .=(-1)/p`2 by A8,XCMPLX_1:60 .= 1/p`1 by A7,XCMPLX_1:192; -p`1=p`2 by A7; then 1/p`2= -(1/p`1) by XCMPLX_1:188 .=-(p`2/p`1/(-p`1)) by A7,A9,XCMPLX_1:192 .=--(p`2/p`1/p`1) by XCMPLX_1:188 .=p`2/p`1/p`1; hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A1,A4,A9,Def1; end; end; hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]|; end; hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A1,Def1; end; case A10: p`1>=p`2 & p`1<=-p`2; now assume A11: p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1; A12: now per cases by A11; case p`2<=p`1 & -p`1<=p`2; then --p`1>=-p`2 by XREAL_1:24; hence p`1=p`2 or p`1=-p`2 by A10,XXREAL_0:1; end; case p`2>=p`1 & p`2<=-p`1; hence p`1=p`2 or p`1=-p`2 by A10,XXREAL_0:1; end; end; now per cases by A12; case A13: p`1=p`2; then p`1 <> 0 by A1,EUCLID:53,54; then p`1/p`2/p`2=1/p`1 by A13,XCMPLX_1:60; hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A1,A11,A13,Def1; end; case A14: p`1=-p`2; then A15: p`2<>0 by A1,EUCLID:53,54; A16: p`1/p`2/p`2 =(-(p`2/p`2))/p`2 by A14 .=(-1)/p`2 by A15,XCMPLX_1:60 .= 1/p`1 by A14,XCMPLX_1:192; -p`1=p`2 by A14; then 1/p`2=-(p`1/p`2/p`2) by A16,XCMPLX_1:188 .=-(p`2/p`1/(-p`1)) by A14,XCMPLX_1:191 .=--(p`2/p`1/p`1) by XCMPLX_1:188 .=p`2/p`1/p`1; hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A1,A11,A16,Def1; end; end; hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]|; end; hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A1,Def1; end; end; hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]|; end; hereby A17: -p`2>p`1 implies --p`2<-p`1 by XREAL_1:24; A18: -p`2

-p`1 by XREAL_1:24; assume not(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2); hence Out_In_Sq.p=|[1/p`1,p`2/p`1/p`1]| by A1,A18,A17,Def1; end; end; theorem Th15: for D being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL 2 )|D st K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2} holds rng (Out_In_Sq|K0) c= the carrier of ((TOP-REAL 2)|D)|K0 proof let D be Subset of TOP-REAL 2, K0 be Subset of (TOP-REAL 2)|D; A1: the carrier of ((TOP-REAL 2)|D) =[#]((TOP-REAL 2)|D) .=D by PRE_TOPC:def 5; then reconsider K00=K0 as Subset of TOP-REAL 2 by XBOOLE_1:1; assume A2: K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2}; A3: 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; A4: 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; then A5: 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 A2,A4; now assume A6: q`1=0; then q`2=0 by A5; hence contradiction by A5,A6,EUCLID:53,54; end; hence thesis; end; let y be object; assume y in rng (Out_In_Sq|K0); then consider x being object such that A7: x in dom (Out_In_Sq|K0) and A8: y=(Out_In_Sq|K0).x by FUNCT_1:def 3; A9: x in (dom Out_In_Sq) /\ K0 by A7,RELAT_1:61; then A10: x in K0 by XBOOLE_0:def 4; K0 c= the carrier of TOP-REAL 2 by A1,XBOOLE_1:1; then reconsider p=x as Point of TOP-REAL 2 by A10; A11: Out_In_Sq.p=y by A8,A10,FUNCT_1:49; A12: 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 A2,A10; then A13: Out_In_Sq.p=|[1/p`1,p`2/p`1/p`1]| by Def1; 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 A14: p in the carrier of ((TOP-REAL 2)|K00) by A9,XBOOLE_0:def 4; A15: p9`1=1/p`1 by EUCLID:52; A16: now assume p9=0.TOP-REAL 2; then 0 *p`1=1/p`1*p`1 by A15,EUCLID:52,54; hence contradiction by A14,A3,XCMPLX_1:87; end; A17: p`1<>0 by A14,A3; now per cases; suppose A18: p`1>=0; 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 A12,XREAL_1:72; then A19: 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 A14,A3, XCMPLX_1:60; then p`2/p`1<=1 & -1<=p`2/p`1 or p`2/p`1>=1 & p`2/p`1<=(-1)*p`1/p`1 by A17,A18,XCMPLX_1:89; then (-1)/p`1<= p`2/p`1/p`1 by A18,XREAL_1:72; then A20: 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 A17,A18,A19,XREAL_1:72; p9`1=1/p`1 & p9`2=p`2/p`1/p`1 by EUCLID:52; hence y in K0 by A2,A11,A16,A13,A20; end; suppose A21: p`1<0; A22: now per cases by A12; case that A23: p`2<=p`1 and A24: (-1 *p`1)<=p`2; p`2/p`1 >=1 by A21,A23,XREAL_1:182; hence p`2/p`1/p`1 <=1/p`1 by A21,XREAL_1:73; (-1) *p`1<=p`2 by A24; then -1 >= p`2/p`1 by A21,XREAL_1:78; then (-1)/p`1<= p`2/p`1/p`1 by A21,XREAL_1:73; hence -(1/p`1)<= p`2/p`1/p`1; end; case that A25: p`2>=p`1 and A26: p`2<=-1 *p`1; p`2/p`1 <=1 by A21,A25,XREAL_1:186; hence p`2/p`1/p`1 >=1/p`1 by A21,XREAL_1:73; (-1) *p`1>=p`2 by A26; then -1 <= p`2/p`1 by A21,XREAL_1:80; then (-1)/p`1>= p`2/p`1/p`1 by A21,XREAL_1:73; hence -(1/p`1)>= p`2/p`1/p`1; end; end; p9`1=1/p`1 & p9`2=p`2/p`1/p`1 by EUCLID:52; hence y in K0 by A2,A11,A16,A13,A22; end; end; then y in [#](((TOP-REAL 2)|D)|K0) by PRE_TOPC:def 5; hence thesis; end; theorem Th16: for D being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL 2 )|D st K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2} holds rng (Out_In_Sq|K0) c= the carrier of ((TOP-REAL 2)|D)|K0 proof let D be Subset of TOP-REAL 2, K0 be Subset of (TOP-REAL 2)|D; A1: the carrier of ((TOP-REAL 2)|D) =[#]((TOP-REAL 2)|D) .=D by PRE_TOPC:def 5; then reconsider K00=K0 as Subset of TOP-REAL 2 by XBOOLE_1:1; assume A2: K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2}; A3: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K00 holds q`2<>0 proof let q be Point of TOP-REAL 2; A4: 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; then A5: 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 A2,A4; now assume A6: q`2=0; then q`1=0 by A5; hence contradiction by A5,A6,EUCLID:53,54; end; hence thesis; end; let y be object; assume y in rng (Out_In_Sq|K0); then consider x being object such that A7: x in dom (Out_In_Sq|K0) and A8: y=(Out_In_Sq|K0).x by FUNCT_1:def 3; x in (dom Out_In_Sq) /\ K0 by A7,RELAT_1:61; then A9: x in K0 by XBOOLE_0:def 4; K0 c= the carrier of TOP-REAL 2 by A1,XBOOLE_1:1; then reconsider p=x as Point of TOP-REAL 2 by A9; A10: Out_In_Sq.p=y by A8,A9,FUNCT_1:49; A11: 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 A2,A9; then A12: Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by Th14; A13: K00=[#]((TOP-REAL 2)|K00) by PRE_TOPC:def 5 .=the carrier of ((TOP-REAL 2)|K00); set p9=|[p`1/p`2/p`2,1/p`2]|; A14: p9`2=1/p`2 by EUCLID:52; A15: now assume p9=0.TOP-REAL 2; then 0 *p`2=1/p`2*p`2 by A14,EUCLID:52,54; hence contradiction by A9,A13,A3,XCMPLX_1:87; end; A16: p`2<>0 by A9,A13,A3; now per cases; case A17: p`2>=0; 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 A11,XREAL_1:72; then A18: 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 A9,A13 ,A3,XCMPLX_1:60; then 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 A16,A17,XCMPLX_1:89; then (-1)/p`2<= p`1/p`2/p`2 by A17,XREAL_1:72; then A19: 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 A16,A17,A18,XREAL_1:72; p9`2=1/p`2 & p9`1=p`1/p`2/p`2 by EUCLID:52; hence y in K0 by A2,A10,A15,A12,A19; end; case A20: p`2<0; 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 A11,XREAL_1:73; then A21: 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 A20, 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 A20,XCMPLX_1:89; then (-1)/p`2>= p`1/p`2/p`2 by A20,XREAL_1:73; then A22: 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 A20,A21,XREAL_1:73; p9`2=1/p`2 & p9`1=p`1/p`2/p`2 by EUCLID:52; hence y in K0 by A2,A10,A15,A12,A22; end; end; then y in [#](((TOP-REAL 2)|D)|K0) by PRE_TOPC:def 5; hence thesis; end; Lm1: 0.TOP-REAL 2 = 0.REAL 2 by EUCLID:66; theorem Th17: for K0a being set,D being non empty Subset of TOP-REAL 2 st K0a= {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} & D`={0.TOP-REAL 2} holds K0a is non empty Subset of ( TOP-REAL 2)|D & K0a is non empty Subset of TOP-REAL 2 proof A1: (1.REAL 2)<>0.TOP-REAL 2 by Lm1,REVROT_1:19; let K0a be set,D be non empty Subset of TOP-REAL 2; assume that A2: K0a={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} and A3: D`={0.TOP-REAL 2}; (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 A4: 1.REAL 2 in K0a by A2,A1; A5: K0a c= D proof let x be object; A6: D=D`` .=NonZero TOP-REAL 2 by A3,SUBSET_1:def 4; assume x in K0a; then A7: ex p8 being Point of TOP-REAL 2 st x=p8 &( p8`2<=p8`1 & - p8`1<=p8`2 or p8`2>=p8`1 & p8`2<=-p8`1)& p8<>0.TOP-REAL 2 by A2; then not x in {0.TOP-REAL 2} by TARSKI:def 1; hence thesis by A7,A6,XBOOLE_0:def 5; end; the carrier of (TOP-REAL 2)|D=[#]((TOP-REAL 2)|D) .=D by PRE_TOPC:def 5; hence K0a is non empty Subset of ((TOP-REAL 2)|D) by A4,A5; thus thesis by A4,A5,XBOOLE_1:1; end; theorem Th18: for K0a being set,D being non empty Subset of TOP-REAL 2 st K0a= {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} & D`={0.TOP-REAL 2} holds K0a is non empty Subset of ( TOP-REAL 2)|D & K0a is non empty Subset of TOP-REAL 2 proof A1: (1.REAL 2)<>0.TOP-REAL 2 by Lm1,REVROT_1:19; let K0a be set,D be non empty Subset of TOP-REAL 2; assume that A2: K0a={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} and A3: D`={0.TOP-REAL 2}; (1.REAL 2)`1<=(1.REAL 2)`2 & -(1.REAL 2)`2<=(1.REAL 2)`1 or (1.REAL 2) `1>=(1.REAL 2)`2 & (1.REAL 2)`1<=-(1.REAL 2)`2 by Th5; then A4: 1.REAL 2 in K0a by A2,A1; A5: K0a c= D proof let x be object; A6: D=D`` .=NonZero TOP-REAL 2 by A3,SUBSET_1:def 4; assume x in K0a; then A7: ex p8 being Point of TOP-REAL 2 st x=p8 &( p8`1<=p8`2 & - p8`2<=p8`1 or p8`1>=p8`2 & p8`1<=-p8`2)& p8<>0.TOP-REAL 2 by A2; then not x in {0.TOP-REAL 2} by TARSKI:def 1; hence thesis by A7,A6,XBOOLE_0:def 5; end; the carrier of (TOP-REAL 2)|D=[#]((TOP-REAL 2)|D) .=D by PRE_TOPC:def 5; hence K0a is non empty Subset of ((TOP-REAL 2)|D) by A4,A5; thus thesis by A4,A5,XBOOLE_1:1; end; theorem Th19: for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r1+r2 ) & g is continuous proof let X being non empty TopSpace,f1,f2 be Function of X,R^1; assume that A1: f1 is continuous and A2: f2 is continuous; defpred P[set,set] means (for r1,r2 being Real st f1.$1=r1 & f2.$1=r2 holds $2=r1+r2); A3: for x being Element of X ex y being Element of REAL st P[x,y] proof let x be Element of X; reconsider r1=f1.x as Element of REAL by TOPMETR:17; reconsider r2=f2.x as Element of REAL by TOPMETR:17; set r3=r1+r2; for r1,r2 being Real st f1.x=r1 & f2.x=r2 holds r3=r1+r2; hence ex y being Element of REAL st for r1,r2 being Real st f1.x=r1 & f2.x=r2 holds y=r1+r2; end; ex f being Function of the carrier of X,REAL st for x being Element of X holds P[x,f.x] from FUNCT_2:sch 3(A3); then consider f being Function of the carrier of X,REAL such that A4: for x being Element of X holds for r1,r2 being Real st f1.x= r1 & f2.x=r2 holds f.x=r1+r2; reconsider g0=f as Function of X,R^1 by TOPMETR:17; for p being Point of X,V being Subset of R^1 st g0.p in V & V is open holds ex W being Subset of X st p in W & W is open & g0.:W c= V proof let p be Point of X,V be Subset of R^1; reconsider r=g0.p as Real; reconsider r1=f1.p as Real; reconsider r2=f2.p as Real; assume g0.p in V & V is open; then consider r0 being Real such that A5: r0>0 and A6: ].r-r0,r+r0.[ c= V by FRECHET:8; reconsider G1=].r1-r0/2,r1+r0/2.[ as Subset of R^1 by TOPMETR:17; A7: r1

a1; reconsider g0=g1 as Function of X,R^1; for p being Point of X,V being Subset of R^1 st g0.p in V & V is open holds ex W being Subset of X st p in W & W is open & g0.:W c= V proof set f1=g0; let p be Point of X,V be Subset of R^1; assume that A1: g0.p in V and V is open; set G1=V; f1.: [#]X c= G1 proof let y be object; assume y in f1.: [#]X; then ex x being object st x in dom f1 & x in [#]X & y=f1.x by FUNCT_1:def 6; then y=a by FUNCOP_1:7; hence thesis by A1,FUNCOP_1:7; end; hence thesis; end; then ( for p being Point of X holds g1.p=a)& g0 is continuous by Th10, FUNCOP_1:7; hence thesis; end; theorem Th21: for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r1-r2 ) & g is continuous proof let X being non empty TopSpace,f1,f2 be Function of X,R^1; assume that A1: f1 is continuous and A2: f2 is continuous; defpred P[set,set] means (for r1,r2 being Real st f1.$1=r1 & f2.$1=r2 holds $2=r1-r2); A3: for x being Element of X ex y being Element of REAL st P[x,y] proof let x be Element of X; reconsider r1=f1.x as Element of REAL by TOPMETR:17; reconsider r2=f2.x as Element of REAL by TOPMETR:17; set r3=r1-r2; for r1,r2 being Real st f1.x=r1 & f2.x=r2 holds r3=r1-r2; hence ex y being Element of REAL st for r1,r2 being Real st f1.x=r1 & f2.x=r2 holds y=r1-r2; end; ex f being Function of the carrier of X,REAL st for x being Element of X holds P[x,f.x] from FUNCT_2:sch 3(A3); then consider f being Function of the carrier of X,REAL such that A4: for x being Element of X holds for r1,r2 being Real st f1.x= r1 & f2.x=r2 holds f.x=r1-r2; reconsider g0=f as Function of X,R^1 by TOPMETR:17; for p being Point of X,V being Subset of R^1 st g0.p in V & V is open holds ex W being Subset of X st p in W & W is open & g0.:W c= V proof let p be Point of X,V be Subset of R^1; reconsider r=g0.p as Real; reconsider r1=f1.p as Real; reconsider r2=f2.p as Real; assume g0.p in V & V is open; then consider r0 being Real such that A5: r0>0 and A6: ].r-r0,r+r0.[ c= V by FRECHET:8; reconsider G1=].r1-r0/2,r1+r0/2.[ as Subset of R^1 by TOPMETR:17; A7: r1 0 and A5: ].r-r0,r+r0.[ c= V by FRECHET:8; A6: r=r1^2 by A2; A7: r=r1*r1 by A2; then A8: 0<=r; then A9: (sqrt(r+r0))^2=r+r0 by A4,SQUARE_1:def 2; now per cases; case A10: r1>=0; set r4=sqrt(r+r0)-sqrt(r); reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1 by TOPMETR:17; A11: G1 is open by JORDAN6:35; r+r0>r by A4,XREAL_1:29; then sqrt(r+r0)>sqrt(r) by A7,SQUARE_1:27; then A12: r4>0 by XREAL_1:50; then A13: r1 r1-r4; then r1 0 by XREAL_1:50; aa1 0 by XREAL_1:50; then (r1+r4-aa1)*(r1+r4+aa1)>0 by A26,XREAL_1:129; then (r1+r4)^2-aa1^2>0; then A27: aa1^2<(r1+r4)^2 by XREAL_1:47; x=aa1*aa1 by A2,A20; hence thesis by A7,A16,A17,A27,A23,XXREAL_1:4; end; hence thesis by A5,A14,XBOOLE_1:1; end; case A28: r1<0; set r4=sqrt(r+r0)-sqrt(r); reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1 by TOPMETR:17; A29: G1 is open by JORDAN6:35; r+r0>r by A4,XREAL_1:29; then sqrt(r+r0)>sqrt(r) by A7,SQUARE_1:27; then A30: r4>0 by XREAL_1:50; then A31: r1 =r1+r4; A45: (r1+r4)^2 -aa1^2+-2*r4^2<= (r1+r4)^2 -aa1^2+0 by XREAL_1:7; -aa1>-(r1+r4) by A42,XREAL_1:24; then (-(r1+r4))^2<(-aa1)^2 by A44,SQUARE_1:16; then (r1+r4)^2 -2*r4^2 -aa1^2<0 by A45,XREAL_1:49; hence r-r0< aa1*aa1 by A7,A37,XREAL_1:48; end; case 0 r1^2-r4^2 by XREAL_1:15; then r1^2-r4^2 +2*r1*r4<0+0 by A28,A30; hence r-r0< aa1*aa1 by A7,A35,A36; end; end; r1-r4 0 by XREAL_1:50; then -(-aa1+(r1-r4))>0; then A46: ((r1-r4)+-aa1)<0; -r1-r4>=r1-r4 by A28,XREAL_1:9; then -(-r1-r4)<=-(r1-r4) by XREAL_1:24; then -(r1-r4)>aa1 by A42,XXREAL_0:2; then -(r1-r4)+(r1-r4)>aa1+(r1-r4) by XREAL_1:8; then (r1-r4-aa1)*(r1-r4+aa1)>0 by A46,XREAL_1:130; then (r1-r4)^2-aa1^2>0; then A47: aa1^2<(r1-r4)^2 by XREAL_1:47; x=aa1*aa1 by A2,A40; hence thesis by A7,A37,A47,A43,XXREAL_1:4; end; hence thesis by A5,A32,XBOOLE_1:1; end; end; hence thesis; end; then A48: g0 is continuous by Th10; for p being Point of X,r1 being Real st f1.p=r1 holds g0.p=r1*r1 by A2; hence thesis by A48; end; theorem Th23: for X being non empty TopSpace, f1 being Function of X,R^1,a being Real st f1 is continuous holds ex g being Function of X,R^1 st ( for p being Point of X,r1 being Real st f1.p=r1 holds g.p=a*r1) & g is continuous proof let X being non empty TopSpace,f1 be Function of X,R^1,a being Real; defpred P[set,set] means (for r1 being Real st f1.$1=r1 holds $2=a*r1); A1: for x being Element of X ex y being Element of REAL st P[x,y] proof let x be Element of X; reconsider r1=f1.x as Real; reconsider r3=a*r1 as Element of REAL by XREAL_0:def 1; for r1 being Real st f1.x=r1 holds r3=a*r1; hence ex y being Element of REAL st for r1 being Real st f1.x=r1 holds y=a* r1; end; ex f being Function of the carrier of X,REAL st for x being Element of X holds P[x,f.x] from FUNCT_2:sch 3(A1); then consider f being Function of the carrier of X,REAL such that A2: for x being Element of X holds for r1 being Real st f1.x=r1 holds f. x=a*r1; reconsider g0=f as Function of X,R^1 by TOPMETR:17; A3: for p being Point of X,r1 being Real st f1.p=r1 holds g0.p=a*r1 by A2; assume A4: f1 is continuous; for p being Point of X,V being Subset of R^1 st g0.p in V & V is open holds ex W being Subset of X st p in W & W is open & g0.:W c= V proof let p be Point of X,V be Subset of R^1; reconsider r=g0.p as Real; reconsider r1=f1.p as Real; assume g0.p in V & V is open; then consider r0 being Real such that A5: r0>0 and A6: ].r-r0,r+r0.[ c= V by FRECHET:8; A7: r=a*r1 by A2; A8: r=a*r1 by A2; now per cases; case A9: a>=0; now per cases by A9; case A10: a>0; set r4=r0/a; reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1 by TOPMETR:17; A11: r1 0 by A29,XREAL_1:58; then A30: r1 0 by A29; then A34: (-a)*r4=r0 by XCMPLX_1:87; g0.:W c= ].r-r0,r+r0.[ proof let x be object; assume x in g0.:W; then consider z being object such that A35: z in dom g0 and A36: z in W and A37: g0.z=x by FUNCT_1:def 6; reconsider pz=z as Point of X by A35; reconsider aa1=f1.pz as Real; pz in the carrier of X; then pz in dom f1 by FUNCT_2:def 1; then A38: f1.pz in f1.:W1 by A36,FUNCT_1:def 6; then r1-r4 0 and A5: ].r-r0,r+r0.[ c= V by FRECHET:8; set r4=r0; reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1 by TOPMETR:17; A6: r1 aa1+a by XREAL_1:8; x=aa1+a by A2,A12; hence thesis by A16,A14,A15,XXREAL_1:4; end; hence thesis by A5,A8,XBOOLE_1:1; end; then A17: g0 is continuous by Th10; for p being Point of X,r1 being Real st f1.p=r1 holds g0.p=r1+a by A2; hence thesis by A17; end; theorem Th25: for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r1*r2 ) & g is continuous proof let X be non empty TopSpace, f1,f2 be Function of X,R^1; assume A1: f1 is continuous & f2 is continuous; then consider g1 being Function of X,R^1 such that A2: for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g1.p=r1+r2 and A3: g1 is continuous by Th19; consider g3 being Function of X,R^1 such that A4: for p being Point of X,r1 being Real st g1.p=r1 holds g3.p=r1 *r1 and A5: g3 is continuous by A3,Th22; consider g2 being Function of X,R^1 such that A6: for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g2.p=r1-r2 and A7: g2 is continuous by A1,Th21; consider g4 being Function of X,R^1 such that A8: for p being Point of X,r1 being Real st g2.p=r1 holds g4.p=r1 *r1 and A9: g4 is continuous by A7,Th22; consider g5 being Function of X,R^1 such that A10: for p being Point of X,r1,r2 being Real st g3.p=r1 & g4.p=r2 holds g5.p=r1-r2 and A11: g5 is continuous by A5,A9,Th21; consider g6 being Function of X,R^1 such that A12: for p being Point of X,r1 being Real st g5.p=r1 holds g6.p=( 1/4) *r1 and A13: g6 is continuous by A11,Th23; for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g6.p=r1*r2 proof let p be Point of X,r1,r2 be Real; assume A14: f1.p=r1 & f2.p=r2; then g2.p=r1-r2 by A6; then A15: g4.p=(r1-r2)^2 by A8; g1.p=r1+r2 by A2,A14; then g3.p=(r1+r2)^2 by A4; then g5.p= (r1+r2)^2 -(r1-r2)^2 by A10,A15; then g6.p=(1/4)*( r1^2+2*r1*r2+r2^2 -(r1-r2)^2) by A12 .= r1*r2; hence thesis; end; hence thesis by A13; end; theorem Th26: for X being non empty TopSpace, f1 being Function of X,R^1 st f1 is continuous & (for q being Point of X holds f1.q<>0) holds ex g being Function of X,R^1 st (for p being Point of X,r1 being Real st f1.p=r1 holds g.p=1/r1) & g is continuous proof let X being non empty TopSpace,f1 be Function of X,R^1; assume that A1: f1 is continuous and A2: for q being Point of X holds f1.q<>0; defpred P[set,set] means (for r1 being Real st f1.$1=r1 holds $2=1/r1); A3: for x being Element of X ex y being Element of REAL st P[x,y] proof let x be Element of X; reconsider r1=f1.x as Element of REAL by TOPMETR:17; reconsider r3=1/r1 as Element of REAL by XREAL_0:def 1; take r3; thus for r1 being Real st f1.x=r1 holds r3=1/r1; end; ex f being Function of the carrier of X,REAL st for x being Element of X holds P[x,f.x] from FUNCT_2:sch 3(A3); then consider f being Function of the carrier of X,REAL such that A4: for x being Element of X holds for r1 being Real st f1.x=r1 holds f. x=1/r1; reconsider g0=f as Function of X,R^1 by TOPMETR:17; for p being Point of X,V being Subset of R^1 st g0.p in V & V is open holds ex W being Subset of X st p in W & W is open & g0.:W c= V proof let p be Point of X,V be Subset of R^1; reconsider r=g0.p as Real; reconsider r1=f1.p as Real; assume g0.p in V & V is open; then consider r0 being Real such that A5: r0>0 and A6: ].r-r0,r+r0.[ c= V by FRECHET:8; A7: r=1/r1 by A4; A8: r1<>0 by A2; now per cases; case A9: r1>=0; set r4=r0/r/(r+r0); reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1 by TOPMETR:17; r0/r>0 by A5,A8,A7,A9,XREAL_1:139; then A10: r1 0 by A5,A8,A7,A9,XREAL_1:139; G1 is open by JORDAN6:35; then consider W1 being Subset of X such that A13: p in W1 & W1 is open and A14: f1.:W1 c= G1 by A1,A11,Th10; set W=W1; r1-r4=1/r-r0/(r+r0)/r by A7 .=(1-r0/(r+r0))/r .=((r+r0)/(r+r0)-r0/(r+r0))/r by A5,A7,A9,XCMPLX_1:60 .=((r+r0-r0)/(r+r0))/r .=r/(r+r0)/r; then A15: r1-r4>0 by A8,A7,A9,A12,XREAL_1:139; g0.:W c= ].r-r0,r+r0.[ proof 0 0 by A5,XREAL_1:139; then -(r/(-r+r0))>0; then A28: (r/(-r+r0))<0; r0/(-r)>0 by A5,A27,XREAL_1:139; then A29: r1 -(1/(1/(-r)+r4)) by XREAL_1:25; then A34: (r+r0)>(1/-(1/(-r)+r4)) by XCMPLX_1:188; let x be object; assume x in g0.:W; then consider z being object such that A35: z in dom g0 and A36: z in W and A37: g0.z=x by FUNCT_1:def 6; reconsider pz=z as Point of X by A35; reconsider aa1=f1.pz as Real; A38: x=1/aa1 by A4,A37; pz in the carrier of X; then pz in dom f1 by FUNCT_2:def 1; then A39: f1.pz in f1.:W1 by A36,FUNCT_1:def 6; then A40: aa1 1/(r1+r4) by A33,XREAL_1:87; r1-r4 1/aa1 by A32,A33,A40,XREAL_1:99; then A42: r+r0>1/aa1 by A34,XXREAL_0:2; 1/(r1+r4) =1/(r1+r0 *(-r)"/(-r+r0)) .=1/(r1+r0 *(1/(-r))/(-r+r0)) .=1/(r1+(-(r1*r0))/(-r+r0)) by A32 .=1/(r1+-((r1*r0)/(-r+r0))) .=1/(r1-((r1*r0))/(-r+r0)) .=1/(r1-r0/((-r+r0)/r1)) by XCMPLX_1:77 .=1/(r1*1-r1*(r0/(-r+r0))) by XCMPLX_1:81 .=1/(r1*(1-r0/(-r+r0))) .=1/(((-r+r0)/(-r+r0)-(r0/(-r+r0)))*r1) by A5,A7,A25,XCMPLX_1:60 .=1/((-r+r0-r0)/(-(r-r0))*(r1)) .=1/((-(-r+r0-r0)/(r-r0))*(r1)) by XCMPLX_1:188 .=1/((-r+r0-r0)/((r-r0))*(-r1)) .=1/((-r)/((r-r0)/(-r1))) by XCMPLX_1:81 .=1/((-r)*(-r1)/(r-r0)) by XCMPLX_1:77 .=(r-r0)/((-r)*(-r1))*1 by XCMPLX_1:80 .=(r-r0)/((-r)*(-r)") by A32 .=(r-r0)/1 by A27,XCMPLX_0:def 7 .=r-r0; hence thesis by A38,A42,A41,XXREAL_1:4; end; hence thesis by A6,A30,XBOOLE_1:1; end; end; hence thesis; end; then A43: g0 is continuous by Th10; for p being Point of X,r1 being Real st f1.p=r1 holds g0.p=1/r1 by A4; hence thesis by A43; end; theorem Th27: for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0) holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r1/r2) & g is continuous proof let X be non empty TopSpace, f1,f2 be Function of X,R^1; assume that A1: f1 is continuous and A2: f2 is continuous & for q being Point of X holds f2.q<>0; consider g1 being Function of X,R^1 such that A3: for p being Point of X,r2 being Real st f2.p=r2 holds g1.p=1/ r2 and A4: g1 is continuous by A2,Th26; consider g2 being Function of X,R^1 such that A5: for p being Point of X,r1,r2 being Real st f1.p=r1 & g1.p=r2 holds g2.p=r1*r2 and A6: g2 is continuous by A1,A4,Th25; for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g2.p=r1/r2 proof let p be Point of X,r1,r2 be Real; assume that A7: f1.p=r1 and A8: f2.p=r2; g1.p=1/r2 by A3,A8; then g2.p=r1*(1/r2) by A5,A7 .=r1/r2; hence thesis; end; hence thesis by A6; end; theorem Th28: for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0) holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r1/r2/r2) & g is continuous proof let X be non empty TopSpace, f1,f2 be Function of X,R^1; assume that A1: f1 is continuous and A2: f2 is continuous & for q being Point of X holds f2.q<>0; consider g2 being Function of X,R^1 such that A3: for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g2.p=r1/r2 and A4: g2 is continuous by A1,A2,Th27; consider g3 being Function of X,R^1 such that A5: for p being Point of X,r1,r2 being Real st g2.p=r1 & f2.p=r2 holds g3.p=r1/r2 and A6: g3 is continuous by A2,A4,Th27; for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g3.p=r1/r2/r2 proof let p be Point of X,r1,r2 be Real; assume that A7: f1.p=r1 and A8: f2.p=r2; g2.p=r1/r2 by A3,A7,A8; hence thesis by A5,A8; end; hence thesis by A6; end; theorem Th29: for K0 being Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K0,R^1 st (for p being Point of (TOP-REAL 2)|K0 holds f.p=proj1.p) holds f is continuous proof reconsider g=proj1 as Function of TOP-REAL 2,R^1 by TOPMETR:17; let K0 be Subset of TOP-REAL 2, f be Function of (TOP-REAL 2)|K0,R^1; A1: dom f= the carrier of (TOP-REAL 2)|K0 & (the carrier of TOP-REAL 2)/\K0= K0 by FUNCT_2:def 1,XBOOLE_1:28; A2: g is continuous by JORDAN5A:27; assume for p being Point of (TOP-REAL 2)|K0 holds f.p=proj1.p; then A3: for x being object st x in dom f holds f.x=proj1.x; the carrier of (TOP-REAL 2)|K0 =[#]((TOP-REAL 2)|K0) .=K0 by PRE_TOPC:def 5; then f=g|K0 by A1,A3,Th6,FUNCT_1:46; hence thesis by A2,TOPMETR:7; end; theorem Th30: for K0 being Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K0,R^1 st (for p being Point of (TOP-REAL 2)|K0 holds f.p=proj2.p) holds f is continuous proof let K0 be Subset of TOP-REAL 2, f be Function of (TOP-REAL 2)|K0,R^1; A1: dom f= the carrier of (TOP-REAL 2)|K0 & (the carrier of TOP-REAL 2) /\ K0=K0 by FUNCT_2:def 1,XBOOLE_1:28; assume for p being Point of (TOP-REAL 2)|K0 holds f.p=proj2.p; then A2: for x being object st x in dom f holds f.x=proj2.x; the carrier of (TOP-REAL 2)|K0 =[#]((TOP-REAL 2)|K0) .=K0 by PRE_TOPC:def 5; then f=proj2|K0 by A1,A2,Th7,FUNCT_1:46; hence thesis by JORDAN5A:27; end; theorem Th31: for K1 being non empty Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K1,R^1 st (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=1/p`1) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1<>0 ) holds f is continuous proof let K1 be non empty Subset of TOP-REAL 2, f be Function of (TOP-REAL 2)|K1, R^1; assume that A1: for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2 )| K1 holds f.p=1/p`1 and A2: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2) |K1 holds q`1<>0; reconsider g1=proj1|K1 as Function of (TOP-REAL 2)|K1,R^1 by TOPMETR:17; A3: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) .=K1 by PRE_TOPC:def 5; A4: for q being Point of (TOP-REAL 2)|K1 holds g1.q=proj1.q proof let q be Point of (TOP-REAL 2)|K1; q in the carrier of (TOP-REAL 2)|K1 & dom proj1=the carrier of TOP-REAL 2 by FUNCT_2:def 1; then q in dom proj1 /\ K1 by A3,XBOOLE_0:def 4; hence thesis by FUNCT_1:48; end; A5: for q being Point of (TOP-REAL 2)|K1 holds g1.q<>0 proof let q be Point of (TOP-REAL 2)|K1; q in the carrier of (TOP-REAL 2)|K1; then reconsider q2=q as Point of TOP-REAL 2 by A3; g1.q=proj1.q by A4 .=q2`1 by PSCOMP_1:def 5; hence thesis by A2; end; g1 is continuous by A4,Th29; then consider g3 being Function of (TOP-REAL 2)|K1,R^1 such that A6: for q being Point of (TOP-REAL 2)|K1,r2 being Real st g1.q= r2 holds g3.q=1/r2 and A7: g3 is continuous by A5,Th26; A8: for x being object st x in dom f holds f.x=g3.x proof let x be object; assume A9: x in dom f; then reconsider s=x as Point of (TOP-REAL 2)|K1; x in [#]((TOP-REAL 2)|K1) by A9; then x in K1 by PRE_TOPC:def 5; then reconsider r=x as Point of (TOP-REAL 2); A10: g1.s=proj1.s & proj1.r=r`1 by A4,PSCOMP_1:def 5; f.r=1/r`1 by A1,A9; hence thesis by A6,A10; end; dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1; then dom f=dom g3 by FUNCT_2:def 1; hence thesis by A7,A8,FUNCT_1:2; end; theorem Th32: for K1 being non empty Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K1,R^1 st (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=1/p`2) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2<>0 ) holds f is continuous proof let K1 be non empty Subset of TOP-REAL 2, f be Function of (TOP-REAL 2)|K1, R^1; assume that A1: for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2 )| K1 holds f.p=1/p`2 and A2: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2) |K1 holds q`2<>0; reconsider g1=proj2|K1 as Function of (TOP-REAL 2)|K1,R^1 by TOPMETR:17; A3: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) .=K1 by PRE_TOPC:def 5; A4: for q being Point of (TOP-REAL 2)|K1 holds g1.q=proj2.q proof let q be Point of (TOP-REAL 2)|K1; q in the carrier of (TOP-REAL 2)|K1 & dom proj2=the carrier of TOP-REAL 2 by FUNCT_2:def 1; then q in dom proj2 /\ K1 by A3,XBOOLE_0:def 4; hence thesis by FUNCT_1:48; end; A5: for q being Point of (TOP-REAL 2)|K1 holds g1.q<>0 proof let q be Point of (TOP-REAL 2)|K1; q in the carrier of (TOP-REAL 2)|K1; then reconsider q2=q as Point of TOP-REAL 2 by A3; g1.q=proj2.q by A4 .=q2`2 by PSCOMP_1:def 6; hence thesis by A2; end; g1 is continuous by A4,Th30; then consider g3 being Function of (TOP-REAL 2)|K1,R^1 such that A6: for q being Point of (TOP-REAL 2)|K1,r2 being Real st g1.q= r2 holds g3.q=1/r2 and A7: g3 is continuous by A5,Th26; A8: for x being object st x in dom f holds f.x=g3.x proof let x be object; assume A9: x in dom f; then reconsider s=x as Point of (TOP-REAL 2)|K1; x in [#]((TOP-REAL 2)|K1) by A9; then x in K1 by PRE_TOPC:def 5; then reconsider r=x as Point of (TOP-REAL 2); A10: g1.s=proj2.s & proj2.r=r`2 by A4,PSCOMP_1:def 6; f.r=1/r`2 by A1,A9; hence thesis by A6,A10; end; dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1; then dom f=dom g3 by FUNCT_2:def 1; hence thesis by A7,A8,FUNCT_1:2; end; theorem Th33: for K1 being non empty Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K1,R^1 st (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=p`2/p`1/p`1) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1<>0 ) holds f is continuous proof let K1 be non empty Subset of TOP-REAL 2, f be Function of (TOP-REAL 2)|K1, R^1; assume that A1: for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2 )| K1 holds f.p=p`2/p`1/p`1 and A2: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2) |K1 holds q`1<>0; reconsider g2=proj2|K1 as Function of (TOP-REAL 2)|K1,R^1 by TOPMETR:17; reconsider g1=proj1|K1 as Function of (TOP-REAL 2)|K1,R^1 by TOPMETR:17; A3: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) .=K1 by PRE_TOPC:def 5; A4: for q being Point of (TOP-REAL 2)|K1 holds g1.q=proj1.q proof let q be Point of (TOP-REAL 2)|K1; q in the carrier of (TOP-REAL 2)|K1 & dom proj1=the carrier of TOP-REAL 2 by FUNCT_2:def 1; then q in dom proj1 /\ K1 by A3,XBOOLE_0:def 4; hence thesis by FUNCT_1:48; end; then A5: g1 is continuous by Th29; A6: for q being Point of (TOP-REAL 2)|K1 holds g1.q<>0 proof let q be Point of (TOP-REAL 2)|K1; q in the carrier of (TOP-REAL 2)|K1; then reconsider q2=q as Point of TOP-REAL 2 by A3; g1.q=proj1.q by A4 .=q2`1 by PSCOMP_1:def 5; hence thesis by A2; end; A7: for q being Point of (TOP-REAL 2)|K1 holds g2.q=proj2.q proof let q be Point of (TOP-REAL 2)|K1; q in the carrier of (TOP-REAL 2)|K1 & dom proj2=the carrier of TOP-REAL 2 by FUNCT_2:def 1; then q in dom proj2 /\ K1 by A3,XBOOLE_0:def 4; hence thesis by FUNCT_1:48; end; then g2 is continuous by Th30; then consider g3 being Function of (TOP-REAL 2)|K1,R^1 such that A8: for q being Point of (TOP-REAL 2)|K1,r1,r2 being Real st g2. q= r1 & g1.q=r2 holds g3.q=r1/r2/r2 and A9: g3 is continuous by A5,A6,Th28; A10: for x being object st x in dom f holds f.x=g3.x proof let x be object; assume A11: x in dom f; then reconsider s=x as Point of (TOP-REAL 2)|K1; x in [#]((TOP-REAL 2)|K1) by A11; then x in K1 by PRE_TOPC:def 5; then reconsider r=x as Point of (TOP-REAL 2); A12: proj2.r=r`2 & proj1.r=r`1 by PSCOMP_1:def 5,def 6; A13: g2.s=proj2.s & g1.s=proj1.s by A7,A4; f.r=r`2/r`1/r`1 by A1,A11; hence thesis by A8,A13,A12; end; dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1; then dom f=dom g3 by FUNCT_2:def 1; hence thesis by A9,A10,FUNCT_1:2; end; theorem Th34: for K1 being non empty Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K1,R^1 st (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=p`1/p`2/p`2) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2<>0 ) holds f is continuous proof let K1 be non empty Subset of TOP-REAL 2, f be Function of (TOP-REAL 2)|K1, R^1; assume that A1: for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2 )| K1 holds f.p=p`1/p`2/p`2 and A2: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2) |K1 holds q`2<>0; reconsider g2=proj1|K1 as Function of (TOP-REAL 2)|K1,R^1 by TOPMETR:17; reconsider g1=proj2|K1 as Function of (TOP-REAL 2)|K1,R^1 by TOPMETR:17; A3: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) .=K1 by PRE_TOPC:def 5; A4: for q being Point of (TOP-REAL 2)|K1 holds g1.q=proj2.q proof let q be Point of (TOP-REAL 2)|K1; q in the carrier of (TOP-REAL 2)|K1 & dom proj2=the carrier of TOP-REAL 2 by FUNCT_2:def 1; then q in dom proj2 /\ K1 by A3,XBOOLE_0:def 4; hence thesis by FUNCT_1:48; end; then A5: g1 is continuous by Th30; A6: for q being Point of (TOP-REAL 2)|K1 holds g1.q<>0 proof let q be Point of (TOP-REAL 2)|K1; q in the carrier of (TOP-REAL 2)|K1; then reconsider q2=q as Point of TOP-REAL 2 by A3; g1.q=proj2.q by A4 .=q2`2 by PSCOMP_1:def 6; hence thesis by A2; end; A7: for q being Point of (TOP-REAL 2)|K1 holds g2.q=proj1.q proof let q be Point of (TOP-REAL 2)|K1; q in the carrier of (TOP-REAL 2)|K1 & dom proj1=the carrier of TOP-REAL 2 by FUNCT_2:def 1; then q in dom proj1 /\ K1 by A3,XBOOLE_0:def 4; hence thesis by FUNCT_1:48; end; then g2 is continuous by Th29; then consider g3 being Function of (TOP-REAL 2)|K1,R^1 such that A8: for q being Point of (TOP-REAL 2)|K1,r1,r2 being Real st g2. q= r1 & g1.q=r2 holds g3.q=r1/r2/r2 and A9: g3 is continuous by A5,A6,Th28; A10: for x being object st x in dom f holds f.x=g3.x proof let x be object; assume A11: x in dom f; then reconsider s=x as Point of (TOP-REAL 2)|K1; x in [#]((TOP-REAL 2)|K1) by A11; then x in K1 by PRE_TOPC:def 5; then reconsider r=x as Point of (TOP-REAL 2); A12: proj1.r=r`1 & proj2.r=r`2 by PSCOMP_1:def 5,def 6; A13: g2.s=proj1.s & g1.s=proj2.s by A7,A4; f.r=r`1/r`2/r`2 by A1,A11; hence thesis by A8,A13,A12; end; dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1; then dom f=dom g3 by FUNCT_2:def 1; hence thesis by A9,A10,FUNCT_1:2; end; theorem Th35: for K0,B0 being Subset of TOP-REAL 2, f being Function of ( TOP-REAL 2)|K0,(TOP-REAL 2)|B0, f1,f2 being Function of (TOP-REAL 2)|K0,R^1 st f1 is continuous & f2 is continuous & K0<>{} & B0<>{} & (for x,y,r,s being Real st |[x,y]| in K0 & r=f1.(|[x,y]|) & s=f2.(|[x,y]|) holds f.(|[x,y]|)=|[r ,s]|) holds f is continuous proof let K0,B0 be Subset of TOP-REAL 2, f be Function of (TOP-REAL 2)|K0,( TOP-REAL 2)|B0, f1,f2 be Function of (TOP-REAL 2)|K0,R^1; assume that A1: f1 is continuous and A2: f2 is continuous and A3: K0<>{} and A4: B0<>{} and A5: for x,y,r,s being Real st |[x,y]| in K0 & r=f1.(|[x,y]|) & s =f2.(|[x,y]|) holds f. |[x,y]|=|[r,s]|; reconsider B1=B0 as non empty Subset of TOP-REAL 2 by A4; reconsider K1=K0 as non empty Subset of TOP-REAL 2 by A3; reconsider X=(TOP-REAL 2)|K1,Y=(TOP-REAL 2)|B1 as non empty TopSpace; reconsider f0=f as Function of X,Y; for r being Point of X,V being Subset of Y st f0.r in V & V is open holds ex W being Subset of X st r in W & W is open & f0.:W c= V proof let r be Point of X,V be Subset of Y; assume that A6: f0.r in V and A7: V is open; consider V2 being Subset of TOP-REAL 2 such that A8: V2 is open and A9: V=V2 /\ [#]Y by A7,TOPS_2:24; A10: V2 /\ [#]Y c= V2 by XBOOLE_1:17; then f0.r in V2 by A6,A9; then reconsider p=f0.r as Point of TOP-REAL 2; consider r2 being Real such that A11: r2>0 and A12: {q where q is Point of TOP-REAL 2: p`1-r2 =p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2} holds f is continuous proof let K0,B0 be Subset of TOP-REAL 2,f be Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0; A1: (1.REAL 2)<>0.TOP-REAL 2 by Lm1,REVROT_1:19; assume A2: f=Out_In_Sq|K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2}; A3: K0 c= B0 proof let x be object; assume A4: x in K0; then ex p8 being Point of TOP-REAL 2 st x=p8 &( p8`2<=p8`1 & - p8`1<=p8`2 or p8`2>=p8`1 & p8`2<=-p8`1)& p8<>0.TOP-REAL 2 by A2; then not x in {0.TOP-REAL 2} by TARSKI:def 1; hence thesis by A2,A4,XBOOLE_0:def 5; 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 by Th5; then A5: 1.REAL 2 in K0 by A2,A1; then reconsider K1=K0 as non empty Subset of TOP-REAL 2; A6: K1 c= NonZero TOP-REAL 2 proof let z be object; assume A7: z in K1; 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 by A2; then not z in {0.TOP-REAL 2} by TARSKI:def 1; hence thesis by A7,XBOOLE_0:def 5; end; A8: dom (Out_In_Sq|K1) c= dom ((proj2)*(Out_In_Sq|K1)) proof let x be object; assume A9: x in dom (Out_In_Sq|K1); then x in dom Out_In_Sq /\ K1 by RELAT_1:61; then x in dom Out_In_Sq by XBOOLE_0:def 4; then Out_In_Sq.x in rng Out_In_Sq by FUNCT_1:3; then A10: dom proj2 = (the carrier of TOP-REAL 2) & Out_In_Sq.x in the carrier of TOP-REAL 2 by FUNCT_2:def 1,XBOOLE_0:def 5; (Out_In_Sq|K1).x=Out_In_Sq.x by A9,FUNCT_1:47; hence thesis by A9,A10,FUNCT_1:11; end; A11: rng ((proj2)*(Out_In_Sq|K1)) c= the carrier of R^1 by TOPMETR:17; A12: NonZero TOP-REAL 2<>{} by Th9; A13: dom (Out_In_Sq|K1) c= dom ((proj1)*(Out_In_Sq|K1)) proof let x be object; assume A14: x in dom (Out_In_Sq|K1); then x in dom Out_In_Sq /\ K1 by RELAT_1:61; then x in dom Out_In_Sq by XBOOLE_0:def 4; then Out_In_Sq.x in rng Out_In_Sq by FUNCT_1:3; then A15: dom proj1 = (the carrier of TOP-REAL 2) & Out_In_Sq.x in the carrier of TOP-REAL 2 by FUNCT_2:def 1,XBOOLE_0:def 5; (Out_In_Sq|K1).x=Out_In_Sq.x by A14,FUNCT_1:47; hence thesis by A14,A15,FUNCT_1:11; end; A16: rng ((proj1)*(Out_In_Sq|K1)) c= the carrier of R^1 by TOPMETR:17; dom ((proj1)*(Out_In_Sq|K1)) c= dom (Out_In_Sq|K1) by RELAT_1:25; then dom ((proj1)*(Out_In_Sq|K1)) =dom (Out_In_Sq|K1) by A13 .=dom Out_In_Sq /\ K1 by RELAT_1:61 .=(NonZero TOP-REAL 2)/\ K1 by A12,FUNCT_2:def 1 .=K1 by A6,XBOOLE_1:28 .=[#]((TOP-REAL 2)|K1) by PRE_TOPC:def 5 .=the carrier of (TOP-REAL 2)|K1; then reconsider g1=(proj1)*(Out_In_Sq|K1) as Function of (TOP-REAL 2)|K1,R^1 by A16,FUNCT_2:2 ; for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1 holds g1.p=1/p`1 proof A17: K1 c= NonZero TOP-REAL 2 proof let z be object; assume A18: z in K1; 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 by A2; then not z in {0.TOP-REAL 2} by TARSKI:def 1; hence thesis by A18,XBOOLE_0:def 5; end; A19: NonZero TOP-REAL 2<>{} by Th9; A20: dom (Out_In_Sq|K1)=dom Out_In_Sq /\ K1 by RELAT_1:61 .=(NonZero TOP-REAL 2)/\ K1 by A19,FUNCT_2:def 1 .=K1 by A17,XBOOLE_1:28; let p be Point of TOP-REAL 2; A21: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) .=K1 by PRE_TOPC:def 5; assume A22: p in the carrier of (TOP-REAL 2)|K1; then ex p3 being Point of TOP-REAL 2 st p=p3 &( p3`2<=p3`1 & - p3`1<=p3`2 or p3`2>=p3`1 & p3`2<=-p3`1)& p3<>0.TOP-REAL 2 by A2,A21; then A23: Out_In_Sq.p=|[1/p`1,p`2/p`1/p`1]| by Def1; (Out_In_Sq|K1).p=Out_In_Sq.p by A22,A21,FUNCT_1:49; then g1.p=(proj1).(|[1/p`1,p`2/p`1/p`1]|) by A22,A20,A21,A23,FUNCT_1:13 .=(|[1/p`1,p`2/p`1/p`1]|)`1 by PSCOMP_1:def 5 .=1/p`1 by EUCLID:52; hence thesis; end; then consider f1 being Function of (TOP-REAL 2)|K1,R^1 such that A24: for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2) |K1 holds f1.p=1/p`1; dom ((proj2)*(Out_In_Sq|K1)) c= dom (Out_In_Sq|K1) by RELAT_1:25; then dom ((proj2)*(Out_In_Sq|K1)) =dom (Out_In_Sq|K1) by A8 .=dom Out_In_Sq /\ K1 by RELAT_1:61 .=(NonZero TOP-REAL 2)/\ K1 by A12,FUNCT_2:def 1 .=K1 by A6,XBOOLE_1:28 .=[#]((TOP-REAL 2)|K1) by PRE_TOPC:def 5 .=the carrier of (TOP-REAL 2)|K1; then reconsider g2=(proj2)*(Out_In_Sq|K1) as Function of (TOP-REAL 2)|K1,R^1 by A11,FUNCT_2:2 ; for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1 holds g2.p=p`2/p`1/p`1 proof A25: NonZero TOP-REAL 2<>{} by Th9; A26: dom (Out_In_Sq|K1)=dom Out_In_Sq /\ K1 by RELAT_1:61 .=(NonZero TOP-REAL 2)/\ K1 by A25,FUNCT_2:def 1 .=K1 by A6,XBOOLE_1:28; let p be Point of TOP-REAL 2; A27: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) .=K1 by PRE_TOPC:def 5; assume A28: p in the carrier of (TOP-REAL 2)|K1; then ex p3 being Point of TOP-REAL 2 st p=p3 &( p3`2<=p3`1 & - p3`1<=p3`2 or p3`2>=p3`1 & p3`2<=-p3`1)& p3<>0.TOP-REAL 2 by A2,A27; then A29: Out_In_Sq.p=|[1/p`1,p`2/p`1/p`1]| by Def1; (Out_In_Sq|K1).p=Out_In_Sq.p by A28,A27,FUNCT_1:49; then g2.p=(proj2).(|[1/p`1,p`2/p`1/p`1]|) by A28,A26,A27,A29,FUNCT_1:13 .=(|[1/p`1,p`2/p`1/p`1]|)`2 by PSCOMP_1:def 6 .=p`2/p`1/p`1 by EUCLID:52; hence thesis; end; then consider f2 being Function of (TOP-REAL 2)|K1,R^1 such that A30: for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2) |K1 holds f2.p=p`2/p`1/p`1; A31: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1<>0 proof let q be Point of TOP-REAL 2; A32: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) .=K1 by PRE_TOPC:def 5; assume q in the carrier of (TOP-REAL 2)|K1; then A33: 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 A2,A32; now assume A34: q`1=0; then q`2=0 by A33; hence contradiction by A33,A34,EUCLID:53,54; end; hence thesis; end; then A35: f1 is continuous by A24,Th31; A36: for x,y,r,s being Real st |[x,y]| in K1 & r=f1.(|[x,y]|) & s=f2. (|[x,y]|) holds f. |[x,y]|=|[r,s]| proof let x,y,r,s be Real; assume that A37: |[x,y]| in K1 and A38: r=f1.(|[x,y]|) & s=f2.(|[x,y]|); set p99=|[x,y]|; A39: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) .=K1 by PRE_TOPC:def 5; then A40: f1.p99=1/p99`1 by A24,A37; A41: ex p3 being Point of TOP-REAL 2 st p99=p3 &( p3`2<=p3`1 & -p3`1<=p3`2 or p3`2>=p3`1 & p3`2<=-p3`1)& p3<>0.TOP-REAL 2 by A2,A37; then (p99`2<=p99`1 & -p99`1<=p99`2 or p99`2>=p99`1 & p99`2<=-p99`1) implies Out_In_Sq.p99=|[1/p99`1,p99`2/p99`1/p99`1]| by Def1; then (Out_In_Sq|K0). |[x,y]|= |[1/p99`1,p99`2/p99`1/p99`1]| by A37,A41,FUNCT_1:49 .=|[r,s]| by A30,A37,A38,A39,A40; hence thesis by A2; end; f2 is continuous by A31,A30,Th33; hence thesis by A5,A3,A35,A36,Th35; end; theorem Th37: for K0,B0 being Subset of TOP-REAL 2,f being Function of ( TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=Out_In_Sq|K0 & B0=NonZero TOP-REAL 2 & K0={ p: (p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2} holds f is continuous proof let K0,B0 be Subset of TOP-REAL 2,f be Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0; A1: (1.REAL 2)<>0.TOP-REAL 2 by Lm1,REVROT_1:19; assume A2: f=Out_In_Sq|K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2}; A3: K0 c= B0 proof let x be object; assume A4: x in K0; then ex p8 being Point of TOP-REAL 2 st x=p8 &( p8`1<=p8`2 & - p8`2<=p8`1 or p8`1>=p8`2 & p8`1<=-p8`2)& p8<>0.TOP-REAL 2 by A2; then not x in {0.TOP-REAL 2} by TARSKI:def 1; hence thesis by A2,A4,XBOOLE_0:def 5; end; (1.REAL 2)`1<=(1.REAL 2)`2 & -(1.REAL 2)`2<=(1.REAL 2)`1 or (1.REAL 2) `1>=(1.REAL 2)`2 & (1.REAL 2)`1<=-(1.REAL 2)`2 by Th5; then A5: 1.REAL 2 in K0 by A2,A1; then reconsider K1=K0 as non empty Subset of TOP-REAL 2; A6: K1 c= NonZero TOP-REAL 2 proof let z be object; assume A7: z in K1; 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 by A2; then not z in {0.TOP-REAL 2} by TARSKI:def 1; hence thesis by A7,XBOOLE_0:def 5; end; A8: dom (Out_In_Sq|K1) c= dom ((proj1)*(Out_In_Sq|K1)) proof let x be object; assume A9: x in dom (Out_In_Sq|K1); then x in dom Out_In_Sq /\ K1 by RELAT_1:61; then x in dom Out_In_Sq by XBOOLE_0:def 4; then Out_In_Sq.x in rng Out_In_Sq by FUNCT_1:3; then A10: dom proj1 = (the carrier of TOP-REAL 2) & Out_In_Sq.x in the carrier of TOP-REAL 2 by FUNCT_2:def 1,XBOOLE_0:def 5; (Out_In_Sq|K1).x=Out_In_Sq.x by A9,FUNCT_1:47; hence thesis by A9,A10,FUNCT_1:11; end; A11: rng ((proj1)*(Out_In_Sq|K1)) c= the carrier of R^1 by TOPMETR:17; A12: NonZero TOP-REAL 2<>{} by Th9; A13: dom (Out_In_Sq|K1) c= dom ((proj2)*(Out_In_Sq|K1)) proof let x be object; assume A14: x in dom (Out_In_Sq|K1); then x in dom Out_In_Sq /\ K1 by RELAT_1:61; then x in dom Out_In_Sq by XBOOLE_0:def 4; then Out_In_Sq.x in rng Out_In_Sq by FUNCT_1:3; then A15: dom proj2 = (the carrier of TOP-REAL 2) & Out_In_Sq.x in the carrier of TOP-REAL 2 by FUNCT_2:def 1,XBOOLE_0:def 5; (Out_In_Sq|K1).x=Out_In_Sq.x by A14,FUNCT_1:47; hence thesis by A14,A15,FUNCT_1:11; end; A16: rng ((proj2)*(Out_In_Sq|K1)) c= the carrier of R^1 by TOPMETR:17; dom ((proj2)*(Out_In_Sq|K1)) c= dom (Out_In_Sq|K1) by RELAT_1:25; then dom ((proj2)*(Out_In_Sq|K1)) =dom (Out_In_Sq|K1) by A13 .=dom Out_In_Sq /\ K1 by RELAT_1:61 .=(NonZero TOP-REAL 2)/\ K1 by A12,FUNCT_2:def 1 .=K1 by A6,XBOOLE_1:28 .=[#]((TOP-REAL 2)|K1) by PRE_TOPC:def 5 .=the carrier of (TOP-REAL 2)|K1; then reconsider g1=(proj2)*(Out_In_Sq|K1) as Function of (TOP-REAL 2)|K1,R^1 by A16,FUNCT_2:2 ; for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1 holds g1.p=1/p`2 proof A17: K1 c= NonZero TOP-REAL 2 proof let z be object; assume A18: z in K1; 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 by A2; then not z in {0.TOP-REAL 2} by TARSKI:def 1; hence thesis by A18,XBOOLE_0:def 5; end; A19: NonZero TOP-REAL 2<>{} by Th9; A20: dom (Out_In_Sq|K1)=dom Out_In_Sq /\ K1 by RELAT_1:61 .=(NonZero TOP-REAL 2)/\ K1 by A19,FUNCT_2:def 1 .=K1 by A17,XBOOLE_1:28; let p be Point of TOP-REAL 2; A21: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) .=K1 by PRE_TOPC:def 5; assume A22: p in the carrier of (TOP-REAL 2)|K1; then ex p3 being Point of TOP-REAL 2 st p=p3 &( p3`1<=p3`2 & - p3`2<=p3`1 or p3`1>=p3`2 & p3`1<=-p3`2)& p3<>0.TOP-REAL 2 by A2,A21; then A23: Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by Th14; (Out_In_Sq|K1).p=Out_In_Sq.p by A22,A21,FUNCT_1:49; then g1.p=(proj2).(|[p`1/p`2/p`2,1/p`2]|) by A22,A20,A21,A23,FUNCT_1:13 .=(|[p`1/p`2/p`2,1/p`2]|)`2 by PSCOMP_1:def 6 .=1/p`2 by EUCLID:52; hence thesis; end; then consider f1 being Function of (TOP-REAL 2)|K1,R^1 such that A24: for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2) |K1 holds f1.p=1/p`2; dom ((proj1)*(Out_In_Sq|K1)) c= dom (Out_In_Sq|K1) by RELAT_1:25; then dom ((proj1)*(Out_In_Sq|K1)) =dom (Out_In_Sq|K1) by A8 .=dom Out_In_Sq /\ K1 by RELAT_1:61 .=(NonZero TOP-REAL 2)/\ K1 by A12,FUNCT_2:def 1 .=K1 by A6,XBOOLE_1:28 .=[#]((TOP-REAL 2)|K1) by PRE_TOPC:def 5 .=the carrier of (TOP-REAL 2)|K1; then reconsider g2=(proj1)*(Out_In_Sq|K1) as Function of (TOP-REAL 2)|K1,R^1 by A11,FUNCT_2:2 ; for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1 holds g2.p=p`1/p`2/p`2 proof A25: NonZero TOP-REAL 2<>{} by Th9; A26: dom (Out_In_Sq|K1)=dom Out_In_Sq /\ K1 by RELAT_1:61 .=(NonZero TOP-REAL 2)/\ K1 by A25,FUNCT_2:def 1 .=K1 by A6,XBOOLE_1:28; let p be Point of TOP-REAL 2; A27: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) .=K1 by PRE_TOPC:def 5; assume A28: p in the carrier of (TOP-REAL 2)|K1; then ex p3 being Point of TOP-REAL 2 st p=p3 &( p3`1<=p3`2 & - p3`2<=p3`1 or p3`1>=p3`2 & p3`1<=-p3`2)& p3<>0.TOP-REAL 2 by A2,A27; then A29: Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by Th14; (Out_In_Sq|K1).p=Out_In_Sq.p by A28,A27,FUNCT_1:49; then g2.p=(proj1).(|[p`1/p`2/p`2,1/p`2]|) by A28,A26,A27,A29,FUNCT_1:13 .=(|[p`1/p`2/p`2,1/p`2]|)`1 by PSCOMP_1:def 5 .=p`1/p`2/p`2 by EUCLID:52; hence thesis; end; then consider f2 being Function of (TOP-REAL 2)|K1,R^1 such that A30: for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2) |K1 holds f2.p=p`1/p`2/p`2; A31: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2<>0 proof let q be Point of TOP-REAL 2; A32: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) .=K1 by PRE_TOPC:def 5; assume q in the carrier of (TOP-REAL 2)|K1; then A33: 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 A2,A32; now assume A34: q`2=0; then q`1=0 by A33; hence contradiction by A33,A34,EUCLID:53,54; end; hence thesis; end; then A35: f1 is continuous by A24,Th32; A36: for x,y,s,r being Real st |[x,y]| in K1 & s=f2.(|[x,y]|) & r=f1. (|[x,y]|) holds f. |[x,y]|=|[s,r]| proof let x,y,s,r be Real; assume that A37: |[x,y]| in K1 and A38: s=f2.(|[x,y]|) & r=f1.(|[x,y]|); set p99=|[x,y]|; A39: ex p3 being Point of TOP-REAL 2 st p99=p3 &( p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 & p3`1<=-p3`2)& p3<>0.TOP-REAL 2 by A2,A37; A40: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) .=K1 by PRE_TOPC:def 5; then A41: f1.p99=1/p99`2 by A24,A37; (Out_In_Sq|K0). |[x,y]|=(Out_In_Sq). |[x,y]| by A37,FUNCT_1:49 .= |[p99`1/p99`2/p99`2,1/p99`2]| by A39,Th14 .=|[s,r]| by A30,A37,A38,A40,A41; hence thesis by A2; end; f2 is continuous by A31,A30,Th34; hence thesis by A5,A3,A35,A36,Th35; end; scheme TopSubset { P[set] } : { p where p is Point of TOP-REAL 2 : P[p] } is Subset of TOP-REAL 2 proof { p where p is Point of TOP-REAL 2 : P[p] } c= the carrier of TOP-REAL 2 proof let x be object; assume x in { p where p is Point of TOP-REAL 2 : P[p] }; then ex p being Point of TOP-REAL 2 st p = x & P[p]; hence thesis; end; hence thesis; end; scheme TopCompl { P[set], K() -> Subset of TOP-REAL 2 } : K()` = { p where p is Point of TOP-REAL 2 : not P[p] } provided A1: K() = { p where p is Point of TOP-REAL 2 : P[p] } proof thus K()` c= { p where p is Point of TOP-REAL 2: not P[p] } proof let x be object; assume A2: x in K()`; then reconsider qx=x as Point of TOP-REAL 2; x in (the carrier of TOP-REAL 2) \ K() by A2,SUBSET_1:def 4; then not x in K() by XBOOLE_0:def 5; then not P[qx] by A1; hence thesis; end; let x be object; assume x in {p7 where p7 is Point of TOP-REAL 2: not P[p7]}; then A3: ex p7 being Point of TOP-REAL 2 st p7=x & not P[p7]; then not ex q7 being Point of TOP-REAL 2 st x=q7 & P[q7]; then not x in K() by A1; then x in (the carrier of TOP-REAL 2) \ K() by A3,XBOOLE_0:def 5; hence thesis by SUBSET_1:def 4; end; Lm2: now let p01, p02,px1,px2 be Real; set r0 = (p01 -p02)/4; assume p01 - px1 - (p02 - px2)<=r0--r0; then p01 - p02 - (px1 - px2)<=r0+r0; then p01 - p02<= (px1 - px2)+(r0+r0) by XREAL_1:20; then p01 - p02 - (p01 -p02)/2<= (px1 - px2) by XREAL_1:20; hence (p01 - p02)/2<= px1 - px2; end; scheme ClosedSubset { F,G(Point of TOP-REAL 2) -> Real } : {p where p is Point of TOP-REAL 2 : F(p) <= G(p) } is closed Subset of TOP-REAL 2 provided A1: for p,q being Point of TOP-REAL 2 holds F(p-q) = F(p) - F(q) & G(p-q ) = G(p) - G(q) and A2: for p,q being Point of TOP-REAL 2 holds (|. (p-q).|)^2 = (F(p-q))^2+ (G(p-q))^2 proof defpred P[Point of TOP-REAL 2] means F($1) <= G($1); reconsider K2 = {p7 where p7 is Point of TOP-REAL 2: P[p7] } as Subset of TOP-REAL 2 from TopSubset; A3: the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8; then reconsider K21 = K2` as Subset of TopSpaceMetr Euclid 2; A4: K2 = {p7 where p7 is Point of TOP-REAL 2: P[p7] }; A5: K2`={p7 where p7 is Point of TOP-REAL 2:not P[p7]} from TopCompl(A4); for p being Point of Euclid 2 st p in K21 ex r being Real st r>0 & Ball(p,r) c= K21 proof let p be Point of Euclid 2; assume A6: p in K21; then reconsider p0=p as Point of TOP-REAL 2; set r0=(F(p0) -G(p0))/4; ex p7 being Point of TOP-REAL 2 st p0=p7 & F(p7)>G(p7) by A5,A6; then A7: F(p0)- G(p0)>0 by XREAL_1:50; then A8: (F(p0) -G(p0))/2 >0 by XREAL_1:139; Ball(p,r0) c= K2` proof let x be object; A9: Ball(p,r0)={q where q is Element of Euclid 2: dist(p,q) < r0} by METRIC_1:17; assume A10: x in Ball(p,r0); then reconsider px=x as Point of TOP-REAL 2 by TOPREAL3:8; consider q being Element of Euclid 2 such that A11: q=x and A12: dist(p,q) < r0 by A10,A9; dist(p,q)= |. (p0-px).| by A11,JGRAPH_1:28; then A13: (|.(p0-px).|)^2 <= r0^2 by A12,SQUARE_1:15; A14: F(p0-px)=F(p0) - F(px) by A1; A15: (|. (p0-px).|)^2 =(F(p0-px))^2+(G(p0-px))^2 by A2; 0+(F(p0-px))^2 <= (G(p0-px))^2 + (F(p0-px))^2 by XREAL_1:7; then (F(p0-px))^2 <= r0^2 by A15,A13,XXREAL_0:2; then A16: F(p0) - F(px)<=r0 by A7,A14,SQUARE_1:47; A17: G(p0-px)=G(p0) - G(px) by A1; (G(p0-px))^2+0 <= (G(p0-px))^2 + (F(p0-px))^2 by XREAL_1:7; then (G(p0-px))^2 <= r0^2 by A15,A13,XXREAL_0:2; then -r0 <=G(p0) - G(px) by A7,A17,SQUARE_1:47; then F(p0) - F(px) - (G(p0) - G(px))<=r0--r0 by A16,XREAL_1:13; then F(px)-G(px)>0 by A8,Lm2; then F(px)>G(px) by XREAL_1:47; hence thesis by A5; end; hence thesis by A7,XREAL_1:139; end; then K21 is open by TOPMETR:15; then K2` is open by A3,PRE_TOPC:30; hence thesis by TOPS_1:3; end; deffunc F(Point of TOP-REAL 2)=$1`1; deffunc G(Point of TOP-REAL 2)=$1`2; Lm3: for p,q being Point of TOP-REAL 2 holds F(p-q) = F(p) - F(q) & G(p-q) = G (p) - G(q) by TOPREAL3:3; Lm4: for p,q being Point of TOP-REAL 2 holds (|. (p-q).|)^2 = (F(p-q))^2+(G(p- q))^2 by JGRAPH_1:29; Lm5: {p7 where p7 is Point of TOP-REAL 2:F(p7)<=G(p7) } is closed Subset of TOP-REAL 2 from ClosedSubset(Lm3,Lm4); Lm6: for p,q being Point of TOP-REAL 2 holds G(p-q) = G(p) - G(q) & F(p-q) = F (p) - F(q) by TOPREAL3:3; Lm7: for p,q being Point of TOP-REAL 2 holds (|. (p-q).|)^2 = (G(p-q))^2+(F(p- q))^2 by JGRAPH_1:29; Lm8: {p7 where p7 is Point of TOP-REAL 2:G(p7)<=F(p7) } is closed Subset of TOP-REAL 2 from ClosedSubset(Lm6,Lm7); deffunc H(Point of TOP-REAL 2)=-$1`1; deffunc I(Point of TOP-REAL 2)=-$1`2; Lm9: now let p,q be Point of TOP-REAL 2; thus H(p-q) = -(p`1 - q`1) by TOPREAL3:3 .= H(p) - H(q); thus G(p-q) = G(p) - G(q) by TOPREAL3:3; end; Lm10: now let p,q be Point of TOP-REAL 2; (H(p-q))^2 = (F(p-q))^2; hence (|. (p-q).|)^2 = (H(p-q))^2+(G(p-q))^2 by JGRAPH_1:29; end; Lm11: {p7 where p7 is Point of TOP-REAL 2:H(p7)<=G(p7) } is closed Subset of TOP-REAL 2 from ClosedSubset(Lm9,Lm10); Lm12: now let p,q be Point of TOP-REAL 2; thus G(p-q) = G(p) - G(q) by TOPREAL3:3; thus H(p-q) = -(p`1 - q`1) by TOPREAL3:3 .= H(p) - H(q); end; Lm13: now let p,q be Point of TOP-REAL 2; (-(p-q)`1)^2 = ((p-q)`1)^2; hence (|. (p-q).|)^2 = (G(p-q))^2+(H(p-q))^2 by JGRAPH_1:29; end; Lm14: {p7 where p7 is Point of TOP-REAL 2:G(p7)<=H(p7) } is closed Subset of TOP-REAL 2 from ClosedSubset(Lm12,Lm13); Lm15: now let p,q be Point of TOP-REAL 2; thus I(p-q) = -(p`2 - q`2) by TOPREAL3:3 .= I(p) - I(q); thus F(p-q) = F(p) - F(q) by TOPREAL3:3; end; Lm16: now let p,q be Point of TOP-REAL 2; (-(p-q)`2)^2 = ((p-q)`2)^2; hence (|. (p-q).|)^2 = (I(p-q))^2+(F(p-q))^2 by JGRAPH_1:29; end; Lm17: {p7 where p7 is Point of TOP-REAL 2:I(p7)<=F(p7) } is closed Subset of TOP-REAL 2 from ClosedSubset(Lm15,Lm16); Lm18: now let p,q be Point of TOP-REAL 2; thus F(p-q) = F(p) - F(q) by TOPREAL3:3; thus I(p-q) = -(p`2 - q`2) by TOPREAL3:3 .= I(p) - I(q); end; Lm19: now let p,q be Point of TOP-REAL 2; (I(p-q))^2 = (G(p-q))^2; hence (|. (p-q).|)^2 = (F(p-q))^2+(I(p-q))^2 by JGRAPH_1:29; end; Lm20: {p7 where p7 is Point of TOP-REAL 2: F(p7)<=I(p7) } is closed Subset of TOP-REAL 2 from ClosedSubset(Lm18,Lm19); theorem Th38: for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2 )|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=Out_In_Sq| K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p `1) & p<>0.TOP-REAL 2} holds f is continuous & K0 is closed proof reconsider K5={p7 where p7 is Point of TOP-REAL 2: p7`2<=-p7`1 } as closed Subset of TOP-REAL 2 by Lm14; reconsider K4={p7 where p7 is Point of TOP-REAL 2: p7`1<=p7`2 } as closed Subset of TOP-REAL 2 by Lm5; reconsider K3={p7 where p7 is Point of TOP-REAL 2: -p7`1<=p7`2 } as closed Subset of TOP-REAL 2 by Lm11; reconsider K2={p7 where p7 is Point of TOP-REAL 2: p7`2<=p7`1 } as closed Subset of TOP-REAL 2 by Lm8; let B0 be Subset of TOP-REAL 2,K0 be Subset of (TOP-REAL 2)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0); defpred P[Point of TOP-REAL 2] means ($1`2<=$1`1 & -$1`1<=$1`2 or $1`2>=$1`1 & $1`2<=-$1`1); the carrier of (TOP-REAL 2)|B0=[#]((TOP-REAL 2)|B0) .= B0 by PRE_TOPC:def 5; then reconsider K1=K0 as Subset of TOP-REAL 2 by XBOOLE_1:1; assume A1: f=Out_In_Sq|K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2}; K0 c= B0 proof let x be object; assume x in K0; then A2: ex p8 being Point of TOP-REAL 2 st x=p8 &( p8`2<=p8`1 & - p8`1<=p8`2 or p8`2>=p8`1 & p8`2<=-p8`1)& p8<>0.TOP-REAL 2 by A1; then not x in {0.TOP-REAL 2} by TARSKI:def 1; hence thesis by A1,A2,XBOOLE_0:def 5; end; then A3: ((TOP-REAL 2)|B0)|K0=(TOP-REAL 2)|K1 by PRE_TOPC:7; reconsider K1={p7 where p7 is Point of TOP-REAL 2: P[p7]} as Subset of TOP-REAL 2 from TopSubset; A4: K1 /\ B0 c= K0 proof let x be object; assume A5: x in K1 /\ B0; then x in B0 by XBOOLE_0:def 4; then not x in {0.TOP-REAL 2} by A1,XBOOLE_0:def 5; then A6: not x=0.TOP-REAL 2 by TARSKI:def 1; x in K1 by A5,XBOOLE_0:def 4; then ex p7 being Point of TOP-REAL 2 st p7=x &( p7`2<=(p7`1) & -(p7`1)<=p7 `2 or p7`2>=(p7`1) & p7`2<=-(p7`1)); hence thesis by A1,A6; end; A7: K2 /\ K3 \/ K4 /\ K5 c= K1 proof let x be object; assume A8: x in K2 /\ K3 \/ K4 /\ K5; now per cases by A8,XBOOLE_0:def 3; case A9: x in K2 /\ K3; then x in K3 by XBOOLE_0:def 4; then A10: ex p8 being Point of TOP-REAL 2 st p8=x & -p8`1<=p8`2; x in K2 by A9,XBOOLE_0:def 4; then ex p7 being Point of TOP-REAL 2 st p7=x & p7`2<=(p7`1); hence thesis by A10; end; case A11: x in K4 /\ K5; then x in K5 by XBOOLE_0:def 4; then A12: ex p8 being Point of TOP-REAL 2 st p8=x & p8`2<= -p8`1; x in K4 by A11,XBOOLE_0:def 4; then ex p7 being Point of TOP-REAL 2 st p7=x & p7`2>=(p7`1); hence thesis by A12; end; end; hence thesis; end; K1 c= K2 /\ K3 \/ K4 /\ K5 proof let x be object; assume x in K1; then ex p being Point of TOP-REAL 2 st p=x &( p`2<=p`1 & -p`1 <=p`2 or p`2 >=p`1 & p`2<=-p`1); then x in K2 & x in K3 or x in K4 & x in K5; then x in K2 /\ K3 or x in K4 /\ K5 by XBOOLE_0:def 4; hence thesis by XBOOLE_0:def 3; end; then K1=K2 /\ K3 \/ K4 /\ K5 by A7; then A13: K1 is closed; K0 c= K1 /\ B0 proof let x be object; assume x in K0; then A14: 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 by A1; then not x in {0.TOP-REAL 2} by TARSKI:def 1; then A15: x in B0 by A1,A14,XBOOLE_0:def 5; x in K1 by A14; hence thesis by A15,XBOOLE_0:def 4; end; then K0=K1 /\ B0 by A4 .=K1 /\ [#]((TOP-REAL 2)|B0) by PRE_TOPC:def 5; hence thesis by A1,A3,A13,Th36,PRE_TOPC:13; end; theorem Th39: for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2 )|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=Out_In_Sq| K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p `2) & p<>0.TOP-REAL 2} holds f is continuous & K0 is closed proof reconsider K5={p7 where p7 is Point of TOP-REAL 2: p7`1<=-p7`2 } as closed Subset of TOP-REAL 2 by Lm20; reconsider K4={p7 where p7 is Point of TOP-REAL 2: p7`2<=p7`1 } as closed Subset of TOP-REAL 2 by Lm8; reconsider K3={p7 where p7 is Point of TOP-REAL 2: -p7`2<=p7`1 } as closed Subset of TOP-REAL 2 by Lm17; reconsider K2={p7 where p7 is Point of TOP-REAL 2: p7`1<=p7`2 } as closed Subset of TOP-REAL 2 by Lm5; let B0 be Subset of TOP-REAL 2,K0 be Subset of (TOP-REAL 2)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0); defpred P[Point of TOP-REAL 2] means ($1`1<=$1`2 & -$1`2<=$1`1 or $1`1>=$1`2 & $1`1<=-$1`2); the carrier of (TOP-REAL 2)|B0=[#]((TOP-REAL 2)|B0) .= B0 by PRE_TOPC:def 5; then reconsider K1=K0 as Subset of TOP-REAL 2 by XBOOLE_1:1; assume A1: f=Out_In_Sq|K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2}; K0 c= B0 proof let x be object; assume x in K0; then A2: ex p8 being Point of TOP-REAL 2 st x=p8 &( p8`1<=p8`2 & - p8`2<=p8`1 or p8`1>=p8`2 & p8`1<=-p8`2)& p8<>0.TOP-REAL 2 by A1; then not x in {0.TOP-REAL 2} by TARSKI:def 1; hence thesis by A1,A2,XBOOLE_0:def 5; end; then A3: ((TOP-REAL 2)|B0)|K0=(TOP-REAL 2)|K1 by PRE_TOPC:7; reconsider K1={p7 where p7 is Point of TOP-REAL 2: P[p7]} as Subset of TOP-REAL 2 from TopSubset; A4: K1 /\ B0 c= K0 proof let x be object; assume A5: x in K1 /\ B0; then x in B0 by XBOOLE_0:def 4; then not x in {0.TOP-REAL 2} by A1,XBOOLE_0:def 5; then A6: not x=0.TOP-REAL 2 by TARSKI:def 1; x in K1 by A5,XBOOLE_0:def 4; then ex p7 being Point of TOP-REAL 2 st p7=x &( p7`1<=(p7`2) & -(p7`2)<=p7 `1 or p7`1>=(p7`2) & p7`1<=-(p7`2)); hence thesis by A1,A6; end; A7: K2 /\ K3 \/ K4 /\ K5 c= K1 proof let x be object; assume A8: x in K2 /\ K3 \/ K4 /\ K5; now per cases by A8,XBOOLE_0:def 3; case A9: x in K2 /\ K3; then x in K3 by XBOOLE_0:def 4; then A10: ex p8 being Point of TOP-REAL 2 st p8=x & -p8`2<=p8`1; x in K2 by A9,XBOOLE_0:def 4; then ex p7 being Point of TOP-REAL 2 st p7=x & p7`1<=(p7`2); hence thesis by A10; end; case A11: x in K4 /\ K5; then x in K5 by XBOOLE_0:def 4; then A12: ex p8 being Point of TOP-REAL 2 st p8=x & p8`1<= -p8`2; x in K4 by A11,XBOOLE_0:def 4; then ex p7 being Point of TOP-REAL 2 st p7=x & p7`1>=(p7`2); hence thesis by A12; end; end; hence thesis; end; K1 c= K2 /\ K3 \/ K4 /\ K5 proof let x be object; assume x in K1; then ex p being Point of TOP-REAL 2 st p=x &( p`1<=p`2 & -p`2 <=p`1 or p`1 >=p`2 & p`1<=-p`2); then x in K2 & x in K3 or x in K4 & x in K5; then x in K2 /\ K3 or x in K4 /\ K5 by XBOOLE_0:def 4; hence thesis by XBOOLE_0:def 3; end; then K1=K2 /\ K3 \/ K4 /\ K5 by A7; then A13: K1 is closed; K0 c= K1 /\ B0 proof let x be object; assume x in K0; then A14: 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 by A1; then not x in {0.TOP-REAL 2} by TARSKI:def 1; then A15: x in B0 by A1,A14,XBOOLE_0:def 5; x in K1 by A14; hence thesis by A15,XBOOLE_0:def 4; end; then K0=K1 /\ B0 by A4 .=K1 /\ [#]((TOP-REAL 2)|B0) by PRE_TOPC:def 5; hence thesis by A1,A3,A13,Th37,PRE_TOPC:13; end; theorem Th40: for D being non empty Subset of TOP-REAL 2 st D`={0.TOP-REAL 2} holds ex h being Function of (TOP-REAL 2)|D,(TOP-REAL 2)|D st h=Out_In_Sq & h is continuous proof 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; assume A1: D`={0.TOP-REAL 2}; then A2: D=(B0)` .=(NonZero TOP-REAL 2) by SUBSET_1:def 4; A3: {p:(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; assume x in {p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0. TOP-REAL 2}; then A4: ex p 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; 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; end; then x in [#]((TOP-REAL 2)|D) by PRE_TOPC:def 5; hence thesis; 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:(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:(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; assume x in {p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0. TOP-REAL 2}; then A9: ex p 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; 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; end; then x in [#]((TOP-REAL 2)|D) by PRE_TOPC:def 5; hence thesis; end; Y1`1=-1 & Y1`2=1 by EUCLID:52; then Y1 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:(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; 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; 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; 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; then q`1=0 by A15; hence contradiction by A15,A16,EUCLID:53,54; end; hence thesis; end; assume y in rng (Out_In_Sq|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 assume p9=0.TOP-REAL 2; then p9`2=0 by EUCLID:52,54; then 0 *p`2=1/p`2*p`2 by EUCLID:52; hence contradiction by A22,A13,XCMPLX_1:87; 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 per cases; case A26: p`2>=0; 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; p9`2=1/p`2 & p9`1=p`1/p`2/p`2 by EUCLID:52; hence y in K1 by A21,A23,A25,A29; end; case A30: p`2<0; 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; p9`2=1/p`2 & p9`1=p`1/p`2/p`2 by EUCLID:52; hence y in K1 by A21,A23,A25,A32; end; end; then y in [#](((TOP-REAL 2)|D)|K1) by PRE_TOPC:def 5; hence thesis; end; A33: D c= K0 \/ K1 proof let x be object; assume A34: x in D; 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 thesis by XBOOLE_0:def 3; end; A35: NonZero TOP-REAL 2<> {} by Th9; A36: K1 c= NonZero TOP-REAL 2 proof let z be object; assume z in K1; 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 thesis by A37,XBOOLE_0:def 5; 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; 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; 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; 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 assume A43: q`1=0; then q`2=0 by A42; hence contradiction by A42,A43,EUCLID:53,54; end; hence thesis; end; assume y in rng (Out_In_Sq|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: p9`1=1/p`1 by EUCLID:52; A51: now assume p9=0.TOP-REAL 2; then 0 *p`1=1/p`1*p`1 by A50,EUCLID:52,54; hence contradiction by A49,A40,XCMPLX_1:87; 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 per cases; case A55: p`1>=0; 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; p9`1=1/p`1 & p9`2=p`2/p`1/p`1 by EUCLID:52; hence y in K0 by A48,A51,A53,A57; end; case A58: p`1<0; 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; p9`1=1/p`1 & p9`2=p`2/p`1/p`1 by EUCLID:52; hence y in K0 by A48,A51,A53,A61,A59; end; end; then y in [#](((TOP-REAL 2)|D)|K0) by PRE_TOPC:def 5; hence thesis; end; A62: K0 c= NonZero TOP-REAL 2 proof let z be object; assume z in K0; 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 thesis by A63,XBOOLE_0:def 5; 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 be object st x in ([#]((((TOP-REAL 2)|D)|K0))) /\ ([#] ((((TOP-REAL 2)|D)|K1))) holds f.x = g.x proof let x be object; assume A69: x in ([#]((((TOP-REAL 2)|D)|K0))) /\ ([#] ((((TOP-REAL 2)|D)|K1) )); then x in K0 by A67,XBOOLE_0:def 4; then f.x=Out_In_Sq.x by FUNCT_1:49; hence thesis by A64,A69,FUNCT_1:49; 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; assume A77: x in dom h; 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 per cases; case A79: x in K0; h.p=(g+*f).p by A74,A75,FUNCT_4:34 .=f.p by A71,A79,FUNCT_4:13; hence thesis by A79,FUNCT_1:49; end; case not x in K0; then not (p`2<=p`1 & -p`1<=p`2 or 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 thesis by A74,A65,A80,FUNCT_4:13; end; end; hence thesis; 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 thesis by A67,A64,A72,A70,A73,A66,A68,Th1; end; theorem Th41: for B,K0,Kb being Subset of TOP-REAL 2 st B={0.TOP-REAL 2} & K0= {p: -10.TOP-REAL 2 holds not f.t in K0 \/ Kb) &(for r being Point of TOP-REAL 2 st not r in K0 \/ Kb holds f.r in K0) & for s being Point of TOP-REAL 2 st s in Kb holds f.s=s proof set K1a={p8 where p8 is Point of TOP-REAL 2: (p8`1<=p8`2 & -p8`2<=p8`1 or p8 `1>=p8`2 & p8`1<=-p8`2) & p8<>0.TOP-REAL 2 }; set K0a={p8 where p8 is Point of TOP-REAL 2: (p8`2<=p8`1 & -p8`1<=p8`2 or p8 `2>=p8`1 & p8`2<=-p8`1) & p8<>0.TOP-REAL 2}; let B,K0,Kb be Subset of TOP-REAL 2; assume A1: B={0.TOP-REAL 2} & K0={p: -1

0.TOP-REAL 2 holds not Out_In_Sq.t in K0 \/ Kb proof let t be Point of TOP-REAL 2; assume that A5: t in K0 and A6: t<>0.TOP-REAL 2; A7: ex p3 being Point of TOP-REAL 2 st p3=t & -1

=t`1 & t`2<=-t`1; then Out_In_Sq.t=|[1/t`1,t`2/t`1/t`1]| by A6,Def1; then A15: p4`1=1/t`1 by A9,EUCLID:52; now per cases; case A16: t`1>=0; now per cases by A16; case A17: t`1>0; then 1/t`1*t`1<1 *t`1 by A11,A15,XREAL_1:68; hence contradiction by A7,A17,XCMPLX_1:87; end; case A18: t`1=0; then t`2=0 by A14; hence contradiction by A6,A18,EUCLID:53,54; end; end; hence contradiction; end; case A19: t`1<0; then (-1)*t`1>1/t`1*t`1 by A10,A15,XREAL_1:69; then (-1)*t`1>1 by A19,XCMPLX_1:87; then --t`1<=-1 by XREAL_1:24; hence contradiction by A7; end; end; hence contradiction; end; case A20: not(t`2<=t`1 & -t`1<=t`2 or t`2>=t`1 & t`2<=-t`1); then Out_In_Sq.t=|[t`1/t`2/t`2,1/t`2]| by A6,Def1; then A21: p4`2=1/t`2 by A9,EUCLID:52; now per cases; case A22: t`2>=0; now per cases by A22; case A23: t`2>0; then 1/t`2*t`2<1 *t`2 by A13,A21,XREAL_1:68; hence contradiction by A7,A23,XCMPLX_1:87; end; case t`2=0; hence contradiction by A20; end; end; hence contradiction; end; case A24: t`2<0; then (-1)*t`2>1/t`2*t`2 by A12,A21,XREAL_1:69; then (-1)*t`2>1 by A24,XCMPLX_1:87; then --t`2<=-1 by XREAL_1:24; hence contradiction by A7; end; end; hence contradiction; end; end; hence contradiction; end; case Out_In_Sq.t in Kb; then consider p4 being Point of TOP-REAL 2 such that A25: p4=Out_In_Sq.t and A26: -1=p4`1 & -1<=p4`2 & p4`2<=1 or p4`1=1 & -1<=p4`2 & p4`2<= 1 or -1 =p4`2 & -1<=p4`1 & p4`1<=1 or 1=p4`2 & -1<=p4`1 & p4`1<=1 by A1; now per cases; case A27: t`2<=t`1 & -t`1<=t`2 or t`2>=t`1 & t`2<=-t`1; then A28: Out_In_Sq.t=|[1/t`1,t`2/t`1/t`1]| by A6,Def1; then A29: p4`1=1/t`1 by A25,EUCLID:52; now per cases by A26; case -1=p4`1 & -1<=p4`2 & p4`2<=1; then A30: (t`1)*(t`1)" =-t`1 by A29; now per cases; case t`1<>0; then -t`1=1 by A30,XCMPLX_0:def 7; hence contradiction by A7; end; case A31: t`1=0; then t`2=0 by A27; hence contradiction by A6,A31,EUCLID:53,54; end; end; hence contradiction; end; case p4`1=1 & -1<=p4`2 & p4`2<=1; then A32: (t`1)*(t`1)"=t`1 by A29; now per cases; case t`1<>0; hence contradiction by A7,A32,XCMPLX_0:def 7; end; case A33: t`1=0; then t`2=0 by A27; hence contradiction by A6,A33,EUCLID:53,54; end; end; hence contradiction; end; case A34: -1=p4`2 & -1<=p4`1 & p4`1<=1; reconsider K01=K0a as non empty Subset of (TOP-REAL 2)|D by A2,Th17; A35: the carrier of ((TOP-REAL 2)|D)|K01=[#](((TOP-REAL 2)| D)|K01) .=K01 by PRE_TOPC:def 5; A36: dom (Out_In_Sq|K01)=(dom Out_In_Sq) /\ K01 by RELAT_1:61 .=D /\ K01 by A3,FUNCT_2:def 1 .=[#]((TOP-REAL 2)|D) /\ K01 by PRE_TOPC:def 5 .=(the carrier of ((TOP-REAL 2)|D)) /\ K01 .=K01 by XBOOLE_1:28; t in K01 by A6,A27; then A37: (Out_In_Sq|K01).t in rng (Out_In_Sq|K01) by A36,FUNCT_1:3; rng (Out_In_Sq|K01) c= the carrier of ((TOP-REAL 2)|D) |K01 by Th15; then A38: (Out_In_Sq|K01).t in the carrier of (( TOP-REAL 2)|D)| K01 by A37; t in K01 by A6,A27; then Out_In_Sq.t in K0a by A38,A35,FUNCT_1:49; then A39: ex p5 being Point of TOP-REAL 2 st p5=p4 &( p5`2<=p5`1 & -p5`1<=p5`2 or p5`2>=p5`1 & p5`2<=-p5`1)& p5<>0.TOP-REAL 2 by A25; now per cases by A34,A39,XREAL_1:24; case A40: p4`1>=1; then t`2/t`1/t`1=(t`2/t`1)*1 by A29,A34,XXREAL_0:1 .=t`2*1 by A29,A34,A40,XXREAL_0:1 .=t`2; hence contradiction by A7,A25,A28,A34,EUCLID:52; end; case A41: -1>=p4`1; then t`2/t`1/t`1=(t`2/t`1)*(-1) by A29,A34,XXREAL_0:1 .=-(t`2/t`1) .=-(t`2*(-1)) by A29,A34,A41,XXREAL_0:1 .=t`2; hence contradiction by A7,A25,A28,A34,EUCLID:52; end; end; hence contradiction; end; case A42: 1=p4`2 & -1<=p4`1 & p4`1<=1; reconsider K01=K0a as non empty Subset of (TOP-REAL 2)|D by A2,Th17; t in K01 by A6,A27; then A43: Out_In_Sq.t=(Out_In_Sq|K01).t by FUNCT_1:49; dom (Out_In_Sq|K01)=(dom Out_In_Sq) /\ K01 by RELAT_1:61 .=D /\ K01 by A3,FUNCT_2:def 1 .=[#]((TOP-REAL 2)|D) /\ K01 by PRE_TOPC:def 5 .=(the carrier of ((TOP-REAL 2)|D)) /\ K01 .=K01 by XBOOLE_1:28; then t in dom (Out_In_Sq|K01) by A6,A27; then A44: (Out_In_Sq|K01).t in rng (Out_In_Sq|K01) by FUNCT_1:3; rng (Out_In_Sq|K01) c= the carrier of ((TOP-REAL 2)|D) |K01 by Th15; then A45: (Out_In_Sq|K01).t in the carrier of (( TOP-REAL 2)|D)| K01 by A44; the carrier of ((TOP-REAL 2)|D)|K01=[#](((TOP-REAL 2)| D)|K01) .=K01 by PRE_TOPC:def 5; then A46: ex p5 being Point of TOP-REAL 2 st p5=p4 &( p5`2<=p5`1 & -p5`1<=p5`2 or p5`2>=p5`1 & p5`2<=-p5`1)& p5<>0.TOP-REAL 2 by A25,A45,A43; now per cases by A42,A46,XREAL_1:25; case A47: p4`1>=1; then t`2/t`1/t`1=(t`2/t`1)*1 by A29,A42,XXREAL_0:1 .=t`2*1 by A29,A42,A47,XXREAL_0:1 .=t`2; hence contradiction by A7,A25,A28,A42,EUCLID:52; end; case A48: -1>=p4`1; then t`2/t`1/t`1=(t`2/t`1)*(-1) by A29,A42,XXREAL_0:1 .=-(t`2/t`1) .=-(t`2*(-1)) by A29,A42,A48,XXREAL_0:1 .=t`2; hence contradiction by A7,A25,A28,A42,EUCLID:52; end; end; hence contradiction; end; end; hence contradiction; end; case A49: not(t`2<=t`1 & -t`1<=t`2 or t`2>=t`1 & t`2<=-t`1); then A50: Out_In_Sq.t=|[t`1/t`2/t`2,1/t`2]| by A6,Def1; then A51: p4`2=1/t`2 by A25,EUCLID:52; now per cases by A26; case -1=p4`2 & -1<=p4`1 & p4`1<=1; then A52: (t`2)*(t`2)"=-t`2 by A51; now per cases; case t`2<>0; then -t`2=1 by A52,XCMPLX_0:def 7; hence contradiction by A7; end; case t`2=0; hence contradiction by A49; end; end; hence contradiction; end; case p4`2=1 & -1<=p4`1 & p4`1<=1; then A53: (t`2)*(t`2)" =t`2 by A51; now per cases; case t`2<>0; hence contradiction by A7,A53,XCMPLX_0:def 7; end; case t`2=0; hence contradiction by A49; end; end; hence contradiction; end; case A54: -1=p4`1 & -1<=p4`2 & p4`2<=1; reconsider K11=K1a as non empty Subset of (TOP-REAL 2)|D by A2,Th18; A55: dom (Out_In_Sq|K11)=(dom Out_In_Sq) /\ K11 by RELAT_1:61 .=D /\ K11 by A3,FUNCT_2:def 1 .=[#]((TOP-REAL 2)|D) /\ K11 by PRE_TOPC:def 5 .=(the carrier of ((TOP-REAL 2)|D)) /\ K11 .=K11 by XBOOLE_1:28; A56: t`1<=t`2 & -t`2<=t`1 or t`1>=t`2 & t`1<=-t`2 by A49,Th13; then t in K11 by A6; then A57: Out_In_Sq.t=(Out_In_Sq|K11).t by FUNCT_1:49; t in K11 by A6,A56; then A58: (Out_In_Sq|K11).t in rng (Out_In_Sq|K11) by A55,FUNCT_1:3; rng (Out_In_Sq|K11) c= the carrier of ((TOP-REAL 2)|D) |K11 by Th16; then A59: (Out_In_Sq|K11).t in the carrier of (( TOP-REAL 2)|D)| K11 by A58; the carrier of ((TOP-REAL 2)|D)|K11=[#](((TOP-REAL 2)| D)|K11) .=K11 by PRE_TOPC:def 5; then A60: ex p5 being Point of TOP-REAL 2 st p5=p4 &( p5`1<=p5`2 & -p5`2<=p5`1 or p5`1>=p5`2 & p5`1<=-p5`2)& p5<>0.TOP-REAL 2 by A25,A59,A57; now per cases by A54,A60,XREAL_1:24; case A61: p4`2>=1; then t`1/t`2/t`2=(t`1/t`2)*1 by A51,A54,XXREAL_0:1 .=t`1*1 by A51,A54,A61,XXREAL_0:1 .=t`1; hence contradiction by A7,A25,A50,A54,EUCLID:52; end; case A62: -1>=p4`2; then t`1/t`2/t`2=(t`1/t`2)*(-1) by A51,A54,XXREAL_0:1 .=-(t`1/t`2) .=-(t`1*(-1)) by A51,A54,A62,XXREAL_0:1 .=t`1; hence contradiction by A7,A25,A50,A54,EUCLID:52; end; end; hence contradiction; end; case A63: 1=p4`1 & -1<=p4`2 & p4`2<=1; reconsider K11=K1a as non empty Subset of (TOP-REAL 2)|D by A2,Th18; A64: the carrier of ((TOP-REAL 2)|D)|K11=[#](((TOP-REAL 2)| D)|K11) .=K11 by PRE_TOPC:def 5; A65: dom (Out_In_Sq|K11)=(dom Out_In_Sq) /\ K11 by RELAT_1:61 .=D /\ K11 by A3,FUNCT_2:def 1 .=[#]((TOP-REAL 2)|D) /\ K11 by PRE_TOPC:def 5 .=(the carrier of ((TOP-REAL 2)|D)) /\ K11 .=K11 by XBOOLE_1:28; A66: t`1<=t`2 & -t`2<=t`1 or t`1>=t`2 & t`1<=-t`2 by A49,Th13; then t in K11 by A6; then A67: (Out_In_Sq|K11).t in rng (Out_In_Sq|K11) by A65,FUNCT_1:3; rng (Out_In_Sq|K11) c= the carrier of ((TOP-REAL 2)|D) |K11 by Th16; then A68: (Out_In_Sq|K11).t in the carrier of (( TOP-REAL 2)|D)| K11 by A67; t in K11 by A6,A66; then Out_In_Sq.t in K1a by A68,A64,FUNCT_1:49; then A69: ex p5 being Point of TOP-REAL 2 st p5=p4 &( p5`1<=p5`2 & -p5`2<=p5`1 or p5`1>=p5`2 & p5`1<=-p5`2)& p5<>0.TOP-REAL 2 by A25; now per cases by A63,A69,XREAL_1:25; case A70: p4`2>=1; then t`1/t`2/t`2=(t`1/t`2)*1 by A51,A63,XXREAL_0:1 .=t`1*1 by A51,A63,A70,XXREAL_0:1 .=t`1; hence contradiction by A7,A25,A50,A63,EUCLID:52; end; case A71: -1>=p4`2; then t`1/t`2/t`2=(t`1/t`2)*(-1) by A51,A63,XXREAL_0:1 .=-(t`1/t`2) .=-(t`1*(-1)) by A51,A63,A71,XXREAL_0:1 .=t`1; hence contradiction by A7,A25,A50,A63,EUCLID:52; end; end; hence contradiction; end; end; hence contradiction; end; end; hence contradiction; end; end; hence contradiction; end; hence thesis; end; A72: for t being Point of TOP-REAL 2 st not t in K0 \/ Kb holds Out_In_Sq.t in K0 proof let t be Point of TOP-REAL 2; assume A73: not t in K0 \/ Kb; then A74: not t in K0 by XBOOLE_0:def 3; then A75: not t=0.TOP-REAL 2 by A1,Th3; then not t in {0.TOP-REAL 2} by TARSKI:def 1; then t in NonZero TOP-REAL 2 by XBOOLE_0:def 5; then Out_In_Sq.t in NonZero TOP-REAL 2 by FUNCT_2:5; then reconsider p4=Out_In_Sq.t as Point of TOP-REAL 2; A76: not t in Kb by A73,XBOOLE_0:def 3; now per cases; case A77: t`2<=t`1 & -t`1<=t`2 or t`2>=t`1 & t`2<=-t`1; A78: now per cases; case A79: t`1>0; now per cases; case A80: t`2>0; -1>=t`1 or t`1>=1 or -1>=t`2 or t`2>=1 by A1,A74; then A81: t`1>=1 by A77,A79,A80,XXREAL_0:2; not t`1=1 by A1,A76,A77; then A82: t`1>1 by A81,XXREAL_0:1; then t`1<(t`1)^2 by SQUARE_1:14; then (t`2)<(t`1)^2 by A77,A79,XXREAL_0:2; then t`2/t`1<(t`1)^2/t`1 by A79,XREAL_1:74; then t`2/t`1<(t`1) by A79,XCMPLX_1:89; then A83: t`2/t`1/t`1<(t`1)/t`1 by A79,XREAL_1:74; 0 1/t`1 by A82,XREAL_1:74; hence -1<1/t`1 & 1/t`1<1 & -1< t`2/t`1/t`1 & t`2/t`1/t`1<1 by A79,A84,A83,XCMPLX_1:60,89; end; case A85: t`2<=0; A86: now assume t`1<1; then -1>=t`2 by A1,A74,A79,A85; then -t`1<=-1 by A77,A79,XXREAL_0:2; hence t`1>=1 by XREAL_1:24; end; not t`1=1 by A1,A76,A77; then A87: t`1>1 by A86,XXREAL_0:1; then A88: t`1<(t`1)^2 by SQUARE_1:14; --t`1>=-t`2 by A77,A79,XREAL_1:24; then (t`1)^2 >-t`2 by A88,XXREAL_0:2; then (t`1)^2/t`1 >(-t`2)/t`1 by A79,XREAL_1:74; then t`1>-(t`2/t`1) by A79,XCMPLX_1:89; then -t`1<--(t`2/t`1) by XREAL_1:24; then A89: (-1)*t`1/t`1< t`2/t`1/t`1 by A79,XREAL_1:74; t`1/t`1>1/t`1 by A87,XREAL_1:74; hence -1<1/t`1 & 1/t`1<1 & -1< t`2/t`1/t`1 & t`2/t`1/t`1<1 by A79,A85,A89,XCMPLX_1:60,89; end; end; hence -1<1/t`1 & 1/t`1<1 & -1< t`2/t`1/t`1 & t`2/t`1/t`1<1; end; case A90: t`1<=0; now per cases by A90; case A91: t`1=0; then t`2=0 by A77; hence contradiction by A1,A74,A91; end; case A92: t`1<0; now per cases; case A93: t`2>0; -1>=t`1 or t`1>=1 or -1>=t`2 or t`2>=1 by A1,A74; then t`1<=-1 or 1<=-t`1 by A77,A92,XXREAL_0:2; then A94: t`1<=-1 or -1>=--t`1 by XREAL_1:24; not t`1=-1 by A1,A76,A77; then A95: t`1<-1 by A94,XXREAL_0:1; then t`1/t`1>(-1)/t`1 by XREAL_1:75; then A96: -(t`1/t`1)<-((-1)/t`1) by XREAL_1:24; -t`1<(t`1)^2 by A95,SQUARE_1:46; then (t`2)<(t`1)^2 by A77,A92,XXREAL_0:2; then t`2/t`1>(t`1)^2/t`1 by A92,XREAL_1:75; then t`2/t`1>(t`1) by A92,XCMPLX_1:89; then A97: t`2/t`1/t`1<(t`1)/t`1 by A92,XREAL_1:75; 0>t`2/t`1 by A92,A93,XREAL_1:142; then (-1)*t`1/t`1< t`2/t`1/t`1 by A92,XREAL_1:75; hence -1<1/t`1 & 1/t`1<1 & -1< t`2/t`1/t`1 & t`2/t`1/t`1<1 by A92,A96,A97,XCMPLX_1:60; end; case A98: t`2<=0; then -1>=t`1 or -1>=t`2 by A1,A74,A92; then A99: t`1<=-1 by A77,A92,XXREAL_0:2; not t`1=-1 by A1,A76,A77; then A100: t`1< -1 by A99,XXREAL_0:1; then A101: -t`1<(t`1)^2 by SQUARE_1:46; t`1<=t`2 by A77,A92; then -t`1>=-t`2 by XREAL_1:24; then (t`1)^2 >-t`2 by A101,XXREAL_0:2; then (t`1)^2/t`1 <(-t`2)/t`1 by A92,XREAL_1:75; then t`1<-(t`2/t`1) by A92,XCMPLX_1:89; then -t`1>--(t`2/t`1) by XREAL_1:24; then A102: (-1)*t`1/t`1< t`2/t`1/t`1 by A92,XREAL_1:75; t`1/t`1> (-1)/t`1 by A100,XREAL_1:75; then 1> (-1)/t`1 by A92,XCMPLX_1:60; then -1<-(-1)/t`1 by XREAL_1:24; hence -1<1/t`1 & 1/t`1<1 & -1< t`2/t`1/t`1 & t`2/t`1/t`1<1 by A92,A98,A102,XCMPLX_1:89; end; end; hence -1<1/t`1 & 1/t`1<1 & -1< t`2/t`1/t`1 & t`2/t`1/t`1<1; end; end; hence -1<1/t`1 & 1/t`1<1 & -1< t`2/t`1/t`1 & t`2/t`1/t`1<1; end; end; Out_In_Sq.t=|[1/t`1,t`2/t`1/t`1]| by A75,A77,Def1; then p4`1=1/t`1 & p4`2=t`2/t`1/t`1 by EUCLID:52; hence thesis by A1,A78; end; case A103: not(t`2<=t`1 & -t`1<=t`2 or t`2>=t`1 & t`2<=-t`1); then A104: t`1<=t`2 & -t`2<=t`1 or t`1>=t`2 & t`1<=-t`2 by Th13; A105: now per cases; case A106: t`2>0; now per cases; case A107: t`1>0; A108: -1>=t`2 or t`2>=1 or -1>=t`1 or t`1>=1 by A1,A74; not t`2=1 by A1,A76,A103,A107; then A109: t`2>1 by A103,A106,A107,A108,XXREAL_0:1,2; then t`2<(t`2)^2 by SQUARE_1:14; then (t`1)<(t`2)^2 by A103,A106,XXREAL_0:2; then t`1/t`2<(t`2)^2/t`2 by A106,XREAL_1:74; then t`1/t`2<(t`2) by A106,XCMPLX_1:89; then A110: t`1/t`2/t`2<(t`2)/t`2 by A106,XREAL_1:74; 0 1/t`2 by A109,XREAL_1:74; hence -1<1/t`2 & 1/t`2<1 & -1< t`1/t`2/t`2 & t`1/t`2/t`2<1 by A106,A111,A110,XCMPLX_1:60,89; end; case A112: t`1<=0; A113: now assume t`2<1; then -1>=t`1 by A1,A74,A106,A112; then -t`2<=-1 by A104,A106,XXREAL_0:2; hence t`2>=1 by XREAL_1:24; end; not t`2=1 by A1,A76,A104; then A114: t`2>1 by A113,XXREAL_0:1; then t`2<(t`2)^2 by SQUARE_1:14; then (t`2)^2 >-t`1 by A103,A106,XXREAL_0:2; then (t`2)^2/t`2 >(-t`1)/t`2 by A106,XREAL_1:74; then t`2>-(t`1/t`2) by A106,XCMPLX_1:89; then -t`2<--(t`1/t`2) by XREAL_1:24; then A115: (-1)*t`2/t`2< t`1/t`2/t`2 by A106,XREAL_1:74; t`2/t`2>1/t`2 by A114,XREAL_1:74; hence -1<1/t`2 & 1/t`2<1 & -1< t`1/t`2/t`2 & t`1/t`2/t`2<1 by A106,A112,A115,XCMPLX_1:60,89; end; end; hence -1<1/t`2 & 1/t`2<1 & -1< t`1/t`2/t`2 & t`1/t`2/t`2<1; end; case A116: t`2<=0; then A117: t`2<0 by A103; A118: t`1<=t`2 or t`1<=-t`2 by A103,Th13; now per cases; case A119: t`1>0; -1>=t`2 or t`2>=1 or -1>=t`1 or t`1>=1 by A1,A74; then t`2<=-1 or 1<=-t`2 by A104,A116,XXREAL_0:2; then A120: t`2<=-1 or -1>=--t`2 by XREAL_1:24; not t`2=-1 by A1,A76,A104; then A121: t`2<-1 by A120,XXREAL_0:1; then t`2/t`2>(-1)/t`2 by XREAL_1:75; then A122: -(t`2/t`2)<-((-1)/t`2) by XREAL_1:24; -t`2<(t`2)^2 by A121,SQUARE_1:46; then (t`1)<(t`2)^2 by A116,A118,XXREAL_0:2; then t`1/t`2>(t`2)^2/t`2 by A117,XREAL_1:75; then t`1/t`2>(t`2) by A117,XCMPLX_1:89; then A123: t`1/t`2/t`2<(t`2)/t`2 by A117,XREAL_1:75; 0>t`1/t`2 by A117,A119,XREAL_1:142; then (-1)*t`2/t`2< t`1/t`2/t`2 by A117,XREAL_1:75; hence -1<1/t`2 & 1/t`2<1 & -1< t`1/t`2/t`2 & t`1/t`2/t`2<1 by A117,A122,A123,XCMPLX_1:60; end; case A124: t`1<=0; A125: not t`2=-1 by A1,A76,A104; -1>=t`2 or -1>=t`1 by A1,A74,A116,A124; then A126: t`2< -1 by A103,A116,A125,XXREAL_0:1,2; then A127: -t`2<(t`2)^2 by SQUARE_1:46; -t`2>=-t`1 by A103,A116,XREAL_1:24; then (t`2)^2 >-t`1 by A127,XXREAL_0:2; then (t`2)^2/t`2 <(-t`1)/t`2 by A117,XREAL_1:75; then t`2<-(t`1/t`2) by A117,XCMPLX_1:89; then -t`2>--(t`1/t`2) by XREAL_1:24; then A128: (-1)*t`2/t`2< t`1/t`2/t`2 by A117,XREAL_1:75; t`2/t`2> (-1)/t`2 by A126,XREAL_1:75; then 1> (-1)/t`2 by A117,XCMPLX_1:60; then -1<-(-1)/t`2 by XREAL_1:24; hence -1<1/t`2 & 1/t`2<1 & -1< t`1/t`2/t`2 & t`1/t`2/t`2<1 by A103,A116,A124,A128,XCMPLX_1:89; end; end; hence -1<1/t`2 & 1/t`2<1 & -1< t`1/t`2/t`2 & t`1/t`2/t`2<1; end; end; Out_In_Sq.t=|[t`1/t`2/t`2,1/t`2]| by A75,A103,Def1; then p4`2=1/t`2 & p4`1=t`1/t`2/t`2 by EUCLID:52; hence thesis by A1,A105; end; end; hence thesis; end; A129: D =(NonZero TOP-REAL 2) by A1,SUBSET_1:def 4; for x1,x2 being object st x1 in dom Out_In_Sq & x2 in dom Out_In_Sq & Out_In_Sq.x1=Out_In_Sq.x2 holds x1=x2 proof A130: K1a c= D proof let x be object; assume x in K1a; then A131: ex p8 being Point of TOP-REAL 2 st x=p8 &( p8`1<=p8`2 & - p8`2<=p8`1 or p8`1>=p8`2 & p8`1<=-p8`2)& p8<>0.TOP-REAL 2; then not x in {0.TOP-REAL 2} by TARSKI:def 1; hence thesis by A3,A131,XBOOLE_0:def 5; end; A132: (1.REAL 2)<>0.TOP-REAL 2 by Lm1,REVROT_1:19; (1.REAL 2)`1<=(1.REAL 2)`2 & -(1.REAL 2)`2<=(1.REAL 2)`1 or (1.REAL 2 ) `1>=(1.REAL 2)`2 & (1.REAL 2)`1<=-(1.REAL 2)`2 by Th5; then A133: 1.REAL 2 in K1a by A132; the carrier of (TOP-REAL 2)|D=[#]((TOP-REAL 2)|D) .=D by PRE_TOPC:def 5; then reconsider K11=K1a as non empty Subset of ((TOP-REAL 2)|D) by A133 ,A130; reconsider K01=K0a as non empty Subset of ((TOP-REAL 2)|D) by A2,Th17; let x1,x2 be object; assume that A134: x1 in dom Out_In_Sq and A135: x2 in dom Out_In_Sq and A136: Out_In_Sq.x1=Out_In_Sq.x2; NonZero TOP-REAL 2<>{} by Th9; then A137: dom Out_In_Sq=NonZero TOP-REAL 2 by FUNCT_2:def 1; then A138: x2 in D by A1,A135,SUBSET_1:def 4; reconsider p1=x1,p2=x2 as Point of TOP-REAL 2 by A134,A135,XBOOLE_0:def 5; A139: D c= K01 \/ K11 proof let x be object; assume A140: x in D; then reconsider px=x as Point of TOP-REAL 2; not x in {0.TOP-REAL 2} by A129,A140,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:25; then x in K01 or x in K11; hence thesis by XBOOLE_0:def 3; end; A141: x1 in D by A1,A134,A137,SUBSET_1:def 4; now per cases by A139,A141,XBOOLE_0:def 3; case x1 in K01; then A142: ex p7 being Point of TOP-REAL 2 st p1=p7 &( p7`2<=p7`1 & -p7`1<=p7 `2 or p7`2>=p7`1 & p7`2<=-p7`1)& p7<>0.TOP-REAL 2; then A143: Out_In_Sq.p1=|[1/p1`1,p1`2/p1`1/p1`1]| by Def1; now per cases by A139,A138,XBOOLE_0:def 3; case x2 in K0a; then ex p8 being Point of (TOP-REAL 2) st p2=p8 &( p8`2<=p8`1 & -p8 `1<=p8`2 or p8`2>=p8`1 & p8`2<=-p8`1)& p8<>0.TOP-REAL 2; then A144: |[1/p2`1,p2`2/p2`1/p2`1]| =|[1/p1`1,p1`2/p1`1/p1`1]| by A136,A143 ,Def1; A145: p1=|[p1`1,p1`2]| by EUCLID:53; set qq=|[1/p2`1,p2`2/p2`1/p2`1]|; A146: (1/p1`1)"=(p1`1)"" .=p1`1; A147: now assume A148: p1`1=0; then p1`2=0 by A142; hence contradiction by A142,A148,EUCLID:53,54; end; qq`1=1/p2`1 by EUCLID:52; then A149: 1/p1`1= 1/p2`1 by A144,EUCLID:52; qq`2=p2`2/p2`1/p2`1 by EUCLID:52; then p1`2/p1`1= p2`2/p1`1 by A144,A149,A146,A147,EUCLID:52 ,XCMPLX_1:53; then p1`2=p2`2 by A147,XCMPLX_1:53; hence thesis by A149,A146,A145,EUCLID:53; end; case A150: x2 in K1a & not x2 in K0a; A151: now assume A152: p1`1=0; then p1`2=0 by A142; hence contradiction by A142,A152,EUCLID:53,54; end; A153: now per cases by A142; case A154: p1`2<=p1`1 & -p1`1<=p1`2; then -p1`1 <= p1`1 by XXREAL_0:2; then p1`1>=0; then p1`2/p1`1<=p1`1/p1`1 by A154,XREAL_1:72; hence p1`2/p1`1<=1 by A151,XCMPLX_1:60; end; case A155: p1`2>=p1`1 & p1`2<=-p1`1; then -p1`1 >= p1`1 by XXREAL_0:2; then p1`1 <= 0; then p1`2/p1`1<=p1`1/p1`1 by A155,XREAL_1:73; hence p1`2/p1`1<=1 by A151,XCMPLX_1:60; end; end; A156: now per cases by A142; case A157: p1`2<=p1`1 & -p1`1<=p1`2; then -p1`1 <= p1`1 by XXREAL_0:2; then p1`1>=0; then (-p1`1)/p1`1<=p1`2/p1`1 by A157,XREAL_1:72; hence -1<=p1`2/p1`1 by A151,XCMPLX_1:197; end; case A158: p1`2>=p1`1 & p1`2<=-p1`1; -p1`2>=--p1`1 & p1`1 <= 0 by XREAL_1:24,A158; then (-p1`2)/(-p1`1)>=p1`1/(-p1`1) by XREAL_1:72; then (-p1`2)/(-p1`1)>= -1 by A151,XCMPLX_1:198; hence -1<=p1`2/p1`1 by XCMPLX_1:191; end; end; A159: ex p8 being Point of (TOP-REAL 2) st p2=p8 &( p8`1<=p8`2 & -p8 `2<=p8`1 or p8`1>=p8`2 & p8`1<=-p8`2)& p8<>0.TOP-REAL 2 by A150; A160: now assume A161: p2`2=0; then p2`1=0 by A159; hence contradiction by A159,A161,EUCLID:53,54; end; not((p2`2<=p2`1 & -p2`1<=p2`2 or p2`2>=p2`1 & p2`2<=-p2`1) & p2 <> 0.TOP-REAL 2) by A150; then A162: Out_In_Sq.p2=|[p2`1/p2`2/p2`2,1/p2`2]| by A159,Def1; then p1`2/p1`1/p1`1=1/p2`2 by A136,A143,SPPOL_2:1; then A163: p1`2/p1`1=1/p2`2*p1`1 by A151,XCMPLX_1:87 .= p1`1/p2`2; 1/p1`1=p2`1/p2`2/p2`2 by A136,A143,A162,SPPOL_2:1; then A164: p2`1/p2`2=1/p1`1*p2`2 by A160,XCMPLX_1:87 .= p2`2/p1`1; then A165: (p2`1/p2`2)* (p1`2/p1`1)=1 by A160,A151,A163,XCMPLX_1:112; A166: (p2`1/p2`2)* (p1`2/p1`1)*p1`1=1 *p1`1 by A160,A151,A164,A163, XCMPLX_1:112; then A167: p1`2<>0 by A151; A168: ex p9 being Point of (TOP-REAL 2) st p2=p9 &( p9`1<=p9`2 & -p9 `2<=p9`1 or p9`1>=p9`2 & p9`1<=-p9`2)& p9<>0.TOP-REAL 2 by A150; A169: now per cases by A168; case A170: p2`1<=p2`2 & -p2`2<=p2`1; then -p2`2 <= p2`2 by XXREAL_0:2; then p2`2>=0; then (-p2`2)/p2`2<=p2`1/p2`2 by A170,XREAL_1:72; hence -1<=p2`1/p2`2 by A160,XCMPLX_1:197; end; case A171: p2`1>=p2`2 & p2`1<=-p2`2; -p2`1>=--p2`2 & p2`2 <= 0 by XREAL_1:24,A171; then (-p2`1)/(-p2`2)>=p2`2/(-p2`2) by XREAL_1:72; then (-p2`1)/(-p2`2)>= -1 by A160,XCMPLX_1:198; hence -1<=p2`1/p2`2 by XCMPLX_1:191; end; end; (p2`1/p2`2)* ((p1`2/p1`1)*p1`1)=p1`1 by A166; then A172: (p2`1/p2`2)*p1`2=p1`1 by A151,XCMPLX_1:87; then A173: (p2`1/p2`2)=p1`1/p1`2 by A167,XCMPLX_1:89; A174: now per cases by A168; case A175: p2`1<=p2`2 & -p2`2<=p2`1; then -p2`2 <= p2`2 by XXREAL_0:2; then p2`2>=0; then p2`1/p2`2<=p2`2/p2`2 by A175,XREAL_1:72; hence p2`1/p2`2<=1 by A160,XCMPLX_1:60; end; case A176: p2`1>=p2`2 & p2`1<=-p2`2; then -p2`2 >= p2`2 by XXREAL_0:2; then p2`2 <= 0; then p2`1/p2`2<=p2`2/p2`2 by A176,XREAL_1:73; hence p2`1/p2`2<=1 by A160,XCMPLX_1:60; end; end; now per cases; case 0<=p2`1/p2`2; then A177: p1`2>0 & p1`1>=0 or p1`2<0 & p1`1<=0 by A151,A172; now assume p1`2/p1`1<>1; then p1`2/p1`1<1 by A153,XXREAL_0:1; hence contradiction by A165,A174,A177,XREAL_1:162; end; then p1`2=(1)*p1`1 by A151,XCMPLX_1:87; then (p2`1/p2`2)*p2`2=(1)*p2`2 by A151,A173,XCMPLX_1:60 .=p2`2; then p2`1=p2`2 by A160,XCMPLX_1:87; hence contradiction by A150,A168; end; case 0>p2`1/p2`2; then A178: p1`2<0 & p1`1>0 or p1`2>0 & p1`1<0 by A173,XREAL_1:143; now assume p1`2/p1`1<>-1; then -1 =p7`2 & p7`1<=-p7`2)& p7<>0.TOP-REAL 2; then A180: Out_In_Sq.p1=|[p1`1/p1`2/p1`2,1/p1`2]| by Th14; now per cases by A139,A138,XBOOLE_0:def 3; case x2 in K1a; then ex p8 being Point of (TOP-REAL 2) st p2=p8 &( p8`1<=p8`2 & - p8`2<=p8`1 or p8`1>=p8`2 & p8`1<=-p8`2)& p8<>0.TOP-REAL 2; then A181: |[p2`1/p2`2/p2`2,1/p2`2]| =|[p1`1/p1`2/p1`2,1/p1`2]| by A136,A180 ,Th14; A182: p1=|[p1`1,p1`2]| by EUCLID:53; set qq=|[p2`1/p2`2/p2`2,1/p2`2]|; A183: (1/p1`2)"=(p1`2)"" .=p1`2; A184: now assume A185: p1`2=0; then p1`1=0 by A179; hence contradiction by A179,A185,EUCLID:53,54; end; qq`2=1/p2`2 by EUCLID:52; then A186: 1/p1`2= 1/p2`2 by A181,EUCLID:52; qq`1=p2`1/p2`2/p2`2 by EUCLID:52; then p1`1/p1`2= p2`1/p1`2 by A181,A186,A183,A184,EUCLID:52 ,XCMPLX_1:53; then p1`1=p2`1 by A184,XCMPLX_1:53; hence thesis by A186,A183,A182,EUCLID:53; end; case A187: x2 in K0a & not x2 in K1a; A188: now assume A189: p1`2=0; then p1`1=0 by A179; hence contradiction by A179,A189,EUCLID:53,54; end; A190: now per cases by A179; case A191: p1`1<=p1`2 & -p1`2<=p1`1; then -p1`2 <= p1`2 by XXREAL_0:2; then p1`2>=0; then p1`1/p1`2<=p1`2/p1`2 by A191,XREAL_1:72; hence p1`1/p1`2<=1 by A188,XCMPLX_1:60; end; case A192: p1`1>=p1`2 & p1`1<=-p1`2; then -p1`2 >= p1`2 by XXREAL_0:2; then p1`2 <= 0; then p1`1/p1`2<=p1`2/p1`2 by A192,XREAL_1:73; hence p1`1/p1`2<=1 by A188,XCMPLX_1:60; end; end; A193: now per cases by A179; case A194: p1`1<=p1`2 & -p1`2<=p1`1; then -p1`2 <= p1`2 by XXREAL_0:2; then p1`2>=0; then (-p1`2)/p1`2<=p1`1/p1`2 by A194,XREAL_1:72; hence -1<=p1`1/p1`2 by A188,XCMPLX_1:197; end; case A195: p1`1>=p1`2 & p1`1<=-p1`2; -p1`1>=--p1`2 & p1`2 <= 0 by XREAL_1:24,A195; then (-p1`1)/(-p1`2)>=p1`2/(-p1`2) by XREAL_1:72; then (-p1`1)/(-p1`2)>= -1 by A188,XCMPLX_1:198; hence -1<=p1`1/p1`2 by XCMPLX_1:191; end; end; A196: ex p8 being Point of (TOP-REAL 2) st p2=p8 &( p8`2<=p8`1 & - p8`1<=p8`2 or p8`2>=p8`1 & p8`2<=-p8`1)& p8<>0.TOP-REAL 2 by A187; A197: now assume A198: p2`1=0; then p2`2=0 by A196; hence contradiction by A196,A198,EUCLID:53,54; end; A199: ex p9 being Point of (TOP-REAL 2) st p2=p9 &( p9`2<=p9`1 & - p9`1<=p9`2 or p9`2>=p9`1 & p9`2<=-p9`1)& p9<>0.TOP-REAL 2 by A187; A200: now per cases by A199; case A201: p2`2<=p2`1 & -p2`1<=p2`2; then -p2`1 <= p2`1 by XXREAL_0:2; then p2`1>=0; then (-p2`1)/p2`1<=p2`2/p2`1 by A201,XREAL_1:72; hence -1<=p2`2/p2`1 by A197,XCMPLX_1:197; end; case A202: p2`2>=p2`1 & p2`2<=-p2`1; -p2`2>=--p2`1 & p2`1 <= 0 by XREAL_1:24,A202; then (-p2`2)/(-p2`1)>=p2`1/(-p2`1) by XREAL_1:72; then (-p2`2)/(-p2`1)>= -1 by A197,XCMPLX_1:198; hence -1<=p2`2/p2`1 by XCMPLX_1:191; end; end; A203: Out_In_Sq.p2=|[1/p2`1,p2`2/p2`1/p2`1]| by A196,Def1; then 1/p1`2=p2`2/p2`1/p2`1 by A136,A180,SPPOL_2:1; then A204: p2`2/p2`1=1/p1`2*p2`1 by A197,XCMPLX_1:87 .= p2`1/p1`2; p1`1/p1`2/p1`2=1/p2`1 by A136,A180,A203,SPPOL_2:1; then p1`1/p1`2=1/p2`1*p1`2 by A188,XCMPLX_1:87 .= p1`2/p2`1; then A205: (p2`2/p2`1)* (p1`1/p1`2)=1 by A197,A188,A204,XCMPLX_1:112; then A206: p1`1<>0; (p2`2/p2`1)* (p1`1/p1`2)*p1`2=p1`2 by A205; then (p2`2/p2`1)* ((p1`1/p1`2)*p1`2)=p1`2; then (p2`2/p2`1)*p1`1=p1`2 by A188,XCMPLX_1:87; then A207: (p2`2/p2`1)=p1`2/p1`1 by A206,XCMPLX_1:89; A208: now per cases by A199; case A209: p2`2<=p2`1 & -p2`1<=p2`2; then -p2`1 <= p2`1 by XXREAL_0:2; then p2`1>=0; then p2`2/p2`1<=p2`1/p2`1 by A209,XREAL_1:72; hence p2`2/p2`1<=1 by A197,XCMPLX_1:60; end; case A210: p2`2>=p2`1 & p2`2<=-p2`1; then -p2`1 >= p2`1 by XXREAL_0:2; then p2`1 <= 0; then p2`2/p2`1<=p2`1/p2`1 by A210,XREAL_1:73; hence p2`2/p2`1<=1 by A197,XCMPLX_1:60; end; end; now per cases; case 0<=p2`2/p2`1; then A211: p1`1>0 & p1`2>=0 or p1`1<0 & p1`2<=0 by A205,A206; now assume p1`1/p1`2<>1; then p1`1/p1`2<1 by A190,XXREAL_0:1; hence contradiction by A205,A208,A211,XREAL_1:162; end; then p1`1=(1)*p1`2 by A188,XCMPLX_1:87; then (p2`2/p2`1)*p2`1 =(1)*p2`1 by A188,A207,XCMPLX_1:60 .=p2`1; then p2`2=p2`1 by A197,XCMPLX_1:87; hence contradiction by A187,A199; end; case 0>p2`2/p2`1; then A212: p1`1<0 & p1`2>0 or p1`1>0 & p1`2<0 by A207,XREAL_1:143; now assume p1`1/p1`2<>-1; then -1 0.TOP-REAL 2 by EUCLID:52,54; A217: not t=0.TOP-REAL 2 by A215,EUCLID:52,54; now per cases; case A218: t`2<=t`1 & -t`1<=t`2 or t`2>=t`1 & t`2<=-t`1; then A219: Out_In_Sq.t=|[1/t`1,t`2/t`1/t`1]| by A217,Def1; A220: 1<=t`1 & t`1>=-1 or 1>=t`1 & -1>=--t`1 by A215,A218,XREAL_1:24; now per cases by A215,A220,XXREAL_0:1; case t`1=1; hence thesis by A219,EUCLID:53; end; case t`1=-1; hence thesis by A219,EUCLID:53; end; end; hence thesis; end; case A221: not (t`2<=t`1 & -t`1<=t`2 or t`2>=t`1 & t`2<=-t`1); then A222: Out_In_Sq.t=|[t`1/t`2/t`2,1/t`2]| by A216,Def1; now per cases by A215,A221; case t`2=1; hence thesis by A222,EUCLID:53; end; case t`2=-1; hence thesis by A222,EUCLID:53; end; end; hence thesis; end; end; hence thesis; end; ex h being Function of (TOP-REAL 2)|D,(TOP-REAL 2)|D st h =Out_In_Sq & h is continuous by A2,Th40; hence thesis by A213,A4,A72,A214; end; theorem Th42: for f,g being Function of I[01],TOP-REAL 2, K0 being Subset of TOP-REAL 2, O,I being Point of I[01] st O=0 & I=1 & f is continuous one-to-one & g is continuous one-to-one & K0={p: -1 {} by Th9; reconsider W=B` as non empty Subset of TOP-REAL 2 by Th9; defpred P[Point of TOP-REAL 2] means -1=$1`1 & -1<=$1`2 & $1`2<=1 or $1`1=1 & -1<=$1`2 & $1`2<=1 or -1=$1`2 & -1<=$1`1 & $1`1<=1 or 1=$1`2 & -1<=$1`1 & $1 `1<=1; A2: the carrier of (TOP-REAL 2)|B` =[#]((TOP-REAL 2)|B`) .=B` by PRE_TOPC:def 5; reconsider Kb={q: P[q]} as Subset of TOP-REAL 2 from TopSubset; let f,g be Function of I[01],TOP-REAL 2, K0 be Subset of TOP-REAL 2, O,I be Point of I[01]; A3: dom f =the carrier of I[01] by FUNCT_2:def 1; assume A4: O=0 & I=1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & K0={p: -1

0.TOP-REAL 2 holds not h .t in K0 \/ Kb and A7: for r being Point of TOP-REAL 2 st not r in K0 \/ Kb holds h.r in K0 and A8: for s being Point of TOP-REAL 2 st s in Kb holds h.s=s by Th41; rng f c= B` proof let x be object; assume A9: x in rng f; now assume x in B; then A10: x=0.TOP-REAL 2 by TARSKI:def 1; (0.TOP-REAL 2)`1=0 & (0.TOP-REAL 2)`2=0 by EUCLID:52,54; then 0.TOP-REAL 2 in K0 by A4; hence contradiction by A4,A9,A10,XBOOLE_0:def 4; end; then x in (the carrier of TOP-REAL 2)\ B by A9,XBOOLE_0:def 5; hence thesis by SUBSET_1:def 4; end; then A11: ex w being Function of I[01],TOP-REAL 2 st w is continuous & w=h*f by A4 ,A5,A1,Th12; then reconsider d1=h*f as Function of I[01],TOP-REAL 2; the carrier of (TOP-REAL 2)|W <>{}; then A12: dom h=the carrier of (TOP-REAL 2)|B` by FUNCT_2:def 1; rng g c= B` proof let x be object; assume A13: x in rng g; now assume x in B; then A14: x=0.TOP-REAL 2 by TARSKI:def 1; 0.TOP-REAL 2 in K0 by A4,Th3; hence contradiction by A4,A13,A14,XBOOLE_0:def 4; end; then x in (the carrier of TOP-REAL 2)\ B by A13,XBOOLE_0:def 5; hence thesis by SUBSET_1:def 4; end; then A15: ex w2 being Function of I[01],TOP-REAL 2 st w2 is continuous & w2=h*g by A4,A5,A1,Th12; then reconsider d2=h*g as Function of I[01],TOP-REAL 2; A16: dom g =the carrier of I[01] by FUNCT_2:def 1; A17: for r being Point of I[01] holds -1<=(d1.r)`1 & (d1.r)`1<=1 & -1<=(d2.r )`1 & (d2.r)`1<=1 & -1<=(d1.r)`2 & (d1.r)`2<=1 & -1<=(d2.r)`2 & (d2.r)`2<=1 proof let r be Point of I[01]; A18: g.r in Kb implies d2.r in K0 \/ Kb proof A19: d2.r=h.(g.r) by A16,FUNCT_1:13; assume A20: g.r in Kb; then h.(g.r)=g.r by A8; hence thesis by A20,A19,XBOOLE_0:def 3; end; f.r in rng f by A3,FUNCT_1:3; then A21: not f.r in K0 by A4,XBOOLE_0:def 4; A22: not f.r in Kb implies d1.r in K0 \/ Kb proof assume not f.r in Kb; then not f.r in K0 \/ Kb by A21,XBOOLE_0:def 3; then A23: h.(f.r) in K0 by A7; d1.r=h.(f.r) by A3,FUNCT_1:13; hence thesis by A23,XBOOLE_0:def 3; end; g.r in rng g by A16,FUNCT_1:3; then A24: not g.r in K0 by A4,XBOOLE_0:def 4; A25: not g.r in Kb implies d2.r in K0 \/ Kb proof assume not g.r in Kb; then not g.r in K0 \/ Kb by A24,XBOOLE_0:def 3; then A26: h.(g.r) in K0 by A7; d2.r=h.(g.r) by A16,FUNCT_1:13; hence thesis by A26,XBOOLE_0:def 3; end; A27: f.r in Kb implies d1.r in K0 \/ Kb proof A28: d1.r=h.(f.r) by A3,FUNCT_1:13; assume A29: f.r in Kb; then h.(f.r)=f.r by A8; hence thesis by A29,A28,XBOOLE_0:def 3; end; now per cases by A22,A27,A25,A18,XBOOLE_0:def 3; case d1.r in K0 & d2.r in K0; then (ex p being Point of TOP-REAL 2 st p=d1.r & -1

{}; then s in rng d1 by XBOOLE_0:def 4; then consider t1 being object such that A35: t1 in dom d1 and A36: s=d1.t1 by FUNCT_1:def 3; A37: f.t1 in rng f by A3,A35,FUNCT_1:3; s in rng d2 by A34,XBOOLE_0:def 4; then consider t2 being object such that A38: t2 in dom d2 and A39: s=d2.t2 by FUNCT_1:def 3; h.(f.t1)=d1.t1 by A35,FUNCT_1:12; then A40: h.(f.t1)=h.(g.t2) by A36,A38,A39,FUNCT_1:12; rng g c=(the carrier of (TOP-REAL 2))\B proof let e be object; assume A41: e in rng g; now assume e in B; then A42: e=0.TOP-REAL 2 by TARSKI:def 1; 0.TOP-REAL 2 in {p: -1

{} by A37,A44,XBOOLE_0:def 4; hence thesis; end; theorem Th43: for A,B,C,D being Real, f being Function of TOP-REAL 2, TOP-REAL 2 st (for t being Point of TOP-REAL 2 holds f.t=|[A*(t`1)+B,C*(t`2)+D ]|) holds f is continuous proof reconsider h11=proj1 as Function of TOP-REAL 2,R^1 by TOPMETR:17; set K0=[#](TOP-REAL 2); let A,B,C,D be Real,f be Function of TOP-REAL 2,TOP-REAL 2; A1: (TOP-REAL 2)| [#](TOP-REAL 2)=the TopStruct of TOP-REAL 2 by TSEP_1:93; then reconsider h1=h11 as Function of (TOP-REAL 2)| [#](TOP-REAL 2),R^1; h11 is continuous by JORDAN5A:27; then h1 is continuous by A1,PRE_TOPC:32; then consider g1 being Function of (TOP-REAL 2)| [#](TOP-REAL 2),R^1 such that A2: for p being Point of (TOP-REAL 2)| [#](TOP-REAL 2),r1 being Real st h1.p=r1 holds g1.p=A*r1 and A3: g1 is continuous by Th23; reconsider f1=proj1*f as Function of (TOP-REAL 2)| [#](TOP-REAL 2),R^1 by A1, TOPMETR:17; consider g11 being Function of (TOP-REAL 2)| [#](TOP-REAL 2),R^1 such that A4: for p being Point of (TOP-REAL 2)| [#](TOP-REAL 2),r1 being Real st g1.p=r1 holds g11.p=r1+B and A5: g11 is continuous by A3,Th24; reconsider f2=proj2*f as Function of (TOP-REAL 2)| [#](TOP-REAL 2),R^1 by A1, TOPMETR:17; reconsider h11=proj2 as Function of TOP-REAL 2,R^1 by TOPMETR:17; reconsider h1=h11 as Function of (TOP-REAL 2)| [#](TOP-REAL 2),R^1 by A1; dom f1=the carrier of TOP-REAL 2 by FUNCT_2:def 1; then A6: dom f1=dom g11 by A1,FUNCT_2:def 1; assume A7: for t being Point of TOP-REAL 2 holds f.t=|[A*(t`1)+B,C*(t`2)+D]|; A8: for x being object st x in dom f1 holds f1.x=g11.x proof let x be object; assume A9: x in dom f1; then reconsider p=x as Point of TOP-REAL 2 by FUNCT_2:def 1; f1.x=proj1.(f.x) by A9,FUNCT_1:12; then A10: f1.x=proj1.(|[A*(p`1)+B,C*(p`2)+D]|) by A7 .=A*(p`1)+B by PSCOMP_1:65 .=A*(proj1.p)+B by PSCOMP_1:def 5; A*(proj1.p)=g1.p by A1,A2; hence thesis by A1,A4,A10; end; h11 is continuous by JORDAN5A:27; then h1 is continuous by A1,PRE_TOPC:32; then consider g1 being Function of (TOP-REAL 2)| [#](TOP-REAL 2),R^1 such that A11: for p being Point of (TOP-REAL 2)| [#](TOP-REAL 2),r1 being Real st h1.p=r1 holds g1.p=C*r1 and A12: g1 is continuous by Th23; consider g11 being Function of (TOP-REAL 2)| [#](TOP-REAL 2),R^1 such that A13: for p being Point of (TOP-REAL 2)| [#](TOP-REAL 2),r1 being Real st g1.p=r1 holds g11.p=r1+D and A14: g11 is continuous by A12,Th24; A15: for x being object st x in dom f2 holds f2.x=g11.x proof let x be object; assume A16: x in dom f2; then reconsider p=x as Point of TOP-REAL 2 by FUNCT_2:def 1; f2.x=proj2.(f.x) by A16,FUNCT_1:12; then A17: f2.x=proj2.(|[A*(p`1)+B,C*(p`2)+D]|) by A7 .=C*(p`2)+D by PSCOMP_1:65 .=C*(proj2.p)+D by PSCOMP_1:def 6; C*(proj2.p)=g1.p by A1,A11; hence thesis by A1,A13,A17; end; reconsider f0=f as Function of (TOP-REAL 2)| [#](TOP-REAL 2), (TOP-REAL 2)| [#](TOP-REAL 2) by A1; A18: for x,y,r,s being Real st |[x,y]| in K0 & r=f1.(|[x,y]|) & s=f2. (|[x,y]|) holds f0. |[x,y]|=|[r,s]| proof let x,y,r,s be Real; assume that |[x,y]| in K0 and A19: r=f1.(|[x,y]|) & s=f2.(|[x,y]|); A20: f. |[x,y]| is Point of TOP-REAL 2; dom f =the carrier of TOP-REAL 2 by FUNCT_2:def 1; then proj1.(f0. |[x,y]|) =r & proj2.(f0. |[x,y]|) =s by A19,FUNCT_1:13; hence thesis by A20,Th8; end; dom f2=the carrier of TOP-REAL 2 by FUNCT_2:def 1; then dom f2=dom g11 by A1,FUNCT_2:def 1; then A21: f2 is continuous by A14,A15,FUNCT_1:2; f1 is continuous by A5,A6,A8,FUNCT_1:2; then f0 is continuous by A21,A18,Th35; hence f is continuous by A1,PRE_TOPC:34; end; definition let A,B,C,D be Real; func AffineMap(A,B,C,D) -> Function of TOP-REAL 2,TOP-REAL 2 means :Def2: for t being Point of TOP-REAL 2 holds it.t=|[A*(t`1)+B,C*(t`2)+D]|; existence proof defpred P[object,object] means for t being Point of TOP-REAL 2 st t=$1 holds $2= |[A*(t`1)+B,C*(t`2)+D]|; A1: for x being object st x in the carrier of TOP-REAL 2 ex y being object st P[ x,y] proof let x be object; assume x in the carrier of TOP-REAL 2; then reconsider t2=x as Point of TOP-REAL 2; reconsider y2=|[A*(t2`1)+B,C*(t2`2)+D]| as set; for t being Point of TOP-REAL 2 st t=x holds y2 =|[A*(t`1)+B,C*(t`2) +D]|; hence thesis; end; ex ff being Function st dom ff=(the carrier of TOP-REAL 2) & for x being object st x in (the carrier of TOP-REAL 2) holds P[x,ff.x] from CLASSES1:sch 1(A1); then consider ff being Function such that A2: dom ff=the carrier of TOP-REAL 2 and A3: for x being object st x in the carrier of TOP-REAL 2 holds for t being Point of TOP-REAL 2 st t=x holds ff.x=|[A*(t`1)+B,C*(t`2)+D]|; for x being object st x in the carrier of TOP-REAL 2 holds ff.x in the carrier of TOP-REAL 2 proof let x be object; assume x in the carrier of TOP-REAL 2; then reconsider t=x as Point of TOP-REAL 2; ff.t=|[A*(t`1)+B,C*(t`2)+D]| by A3; hence thesis; end; then reconsider ff as Function of TOP-REAL 2,TOP-REAL 2 by A2,FUNCT_2:3; take ff; thus thesis by A3; end; uniqueness proof let m1,m2 be Function of TOP-REAL 2,TOP-REAL 2 such that A4: for t being Point of TOP-REAL 2 holds m1.t=|[A*(t`1)+B,C*(t`2)+D ]| and A5: for t being Point of TOP-REAL 2 holds m2.t=|[A*(t`1)+B,C*(t`2)+D ]|; for x being Point of TOP-REAL 2 holds m1.x = m2.x proof let t be Point of TOP-REAL 2; thus m1.t = |[A*(t`1)+B,C*(t`2)+D]| by A4 .= m2.t by A5; end; hence m1 = m2 by FUNCT_2:63; end; end; registration let a,b,c,d be Real; cluster AffineMap(a,b,c,d) -> continuous; coherence proof for t being Point of TOP-REAL 2 holds AffineMap(a,b,c,d).t=|[a*(t`1)+b ,c*(t`2)+d]| by Def2; hence thesis by Th43; end; end; theorem Th44: for A,B,C,D being Real st A>0 & C>0 holds AffineMap(A,B,C ,D) is one-to-one proof let A,B,C,D be Real such that A1: A>0 and A2: C>0; set ff = AffineMap(A,B,C,D); for x1,x2 being object st x1 in dom ff & x2 in dom ff & ff.x1=ff.x2 holds x1=x2 proof let x1,x2 be object; assume that A3: x1 in dom ff and A4: x2 in dom ff and A5: ff.x1=ff.x2; reconsider p2=x2 as Point of TOP-REAL 2 by A4; reconsider p1=x1 as Point of TOP-REAL 2 by A3; A6: ff.x1= |[A*(p1`1)+B,C*(p1`2)+D]| & ff.x2= |[A*(p2`1)+B,C*(p2`2)+D]| by Def2 ; then A*(p1`1)+B=A*(p2`1)+B by A5,SPPOL_2:1; then (p1`1)=A*(p2`1)/A by A1,XCMPLX_1:89; then A7: (p1`1)=(p2`1) by A1,XCMPLX_1:89; C*(p1`2)+D=C*(p2`2)+D by A5,A6,SPPOL_2:1; then (p1`2)=C*(p2`2)/C by A2,XCMPLX_1:89; hence thesis by A2,A7,TOPREAL3:6,XCMPLX_1:89; end; hence thesis by FUNCT_1:def 4; end; theorem for f,g being Function of I[01],TOP-REAL 2,a,b,c,d being Real , O,I being Point of I[01] st O=0 & I=1 & f is continuous one-to-one & g is continuous one-to-one & (f.O)`1=a & (f.I)`1=b & c <=(f.O)`2 & (f.O)`2<=d & c <= (f.I)`2 & (f.I)`2<=d & (g.O)`2=c & (g.I)`2=d & a<=(g.O)`1 & (g.O)`1<=b & a<=(g. I)`1 & (g.I)`1<=b & a < b & c < d & not (ex r being Point of I[01] st a<(f.r)`1 & (f.r)`1

0 by A16,XREAL_1:50; then A20: C>0 by XREAL_1:139; A21: dom g=the carrier of I[01] by FUNCT_2:def 1; then A22: g2.I=ff.(g.I) by FUNCT_1:13 .=|[A*((g.I)`1)+B,C*d+D]| by A10,Def2; then A23: (g2.I)`2=C*d+D by EUCLID:52 .= d*2/(d-c)+(1-2*d/(d-c)) .= 1; A24: g2.O=ff.(g.O) by A21,FUNCT_1:13 .=|[A*((g.O)`1)+B,C*c+D]| by A9,Def2; then A25: (g2.O)`2=2/(d-c)*c+(1-2*d/(d-c)) by EUCLID:52 .= c*2/(d-c)+(1-2*d/(d-c)) .= c*2/(d-c)+((d-c)/(d-c)-2*d/(d-c)) by A19,XCMPLX_1:60 .= c*2/(d-c)+((d-c)-2*d)/(d-c) .= (c*2+((d-c)-2*d))/(d-c) .= (-(d-c))/(d-c) .= -((d-c)/(d-c)) .= -1 by A19,XCMPLX_1:60; A26: b-a>0 by A15,XREAL_1:50; A27: -1<=(g2.O)`1 & (g2.O)`1<=1 & -1<=(g2.I)`1 & (g2.I)`1<=1 proof reconsider s1=(g.I)`1 as Real; reconsider s0=(g.O)`1 as Real; A28: (a-b)/(b-a) = (-(b-a))/(b-a) .= -((b-a)/(b-a)) .= -1 by A26,XCMPLX_1:60; A29: (g2.I)`1=A*s1+B by A22,EUCLID:52 .= s1*2/(b-a)+(1-2*b/(b-a)) .= s1*2/(b-a)+((b-a)/(b-a)-2*b/(b-a)) by A26,XCMPLX_1:60 .= s1*2/(b-a)+((b-a)-2*b)/(b-a) .= (s1*2+((b-a)-2*b))/(b-a) .= ((s1-b)+(s1-b)-(a-b))/(b-a); b-b>=s0-b by A12,XREAL_1:9; then 0+(b-b)-(a-b)>=(s0-b)+(s0-b)-(a-b) by XREAL_1:9; then A30: (b-a)/(b-a)>=((s0-b)+(s0-b)-(a-b))/(b-a) by A26,XREAL_1:72; b-b>=s1-b by A14,XREAL_1:9; then A31: 0+(b-b)-(a-b)>=(s1-b)+(s1-b)-(a-b) by XREAL_1:9; a-b<=s1-b by A13,XREAL_1:9; then a-b+(a-b)<=(s1-b)+(s1-b) by XREAL_1:7; then A32: a-b+(a-b)-(a-b)<=(s1-b)+(s1-b)-(a-b) by XREAL_1:9; a-b<=s0-b by A11,XREAL_1:9; then a-b+(a-b)<=(s0-b)+(s0-b) by XREAL_1:7; then A33: a-b+(a-b)-(a-b)<=(s0-b)+(s0-b)-(a-b) by XREAL_1:9; (g2.O)`1=A*s0+B by A24,EUCLID:52 .= s0 *2/(b-a)+(1-2*b/(b-a)) .= s0 *2/(b-a)+((b-a)/(b-a)-2*b/(b-a)) by A26,XCMPLX_1:60 .= s0 *2/(b-a)+((b-a)-2*b)/(b-a) .= (s0 *2+((b-a)-2*b))/(b-a) .= ((s0-b)+(s0-b)-(a-b))/(b-a); hence thesis by A26,A33,A28,A30,A29,A32,A31,XREAL_1:72; end; A34: now assume rng f2 meets K0; then consider x being object such that A35: x in rng f2 and A36: x in K0 by XBOOLE_0:3; reconsider q=x as Point of TOP-REAL 2 by A35; consider p such that A37: p=q and A38: -1(2*((t`2)-d)-(c-d))/(d-c)*(d-c) by A19,A46,XREAL_1:68; then (1)*(d-c)> 2*((t`2)-d)-(c-d) by A19,XCMPLX_1:87; then (1)*(d-c)+(c-d)> 2*((t`2)-d)-(c-d)+(c-d) by XREAL_1:8; then 0/2>((t`2)-d)*2/2; then A49: 0+d>t`2 by XREAL_1:19; A*(t`1)+B<1 by A39,A47,A45,EUCLID:52; then (1)*(b-a)> (2*((t`1)-b)-(a-b))/(b-a)*(b-a) by A26,A44,XREAL_1:68; then (1)*(b-a)> 2*((t`1)-b)-(a-b) by A26,XCMPLX_1:87; then (1)*(b-a)+(a-b)> 2*((t`1)-b)-(a-b)+(a-b) by XREAL_1:8; then 0/2>((t`1)-b)*2/2; then A50: 0+b>t`1 by XREAL_1:19; -1 (2*((t`2)-d)-(c-d))/(d-c)*(d-c) by A19,A68,XREAL_1:68; then (1)*(d-c)> 2*((t`2)-d)-(c-d) by A19,XCMPLX_1:87; then (1)*(d-c)+(c-d)> 2*((t`2)-d)-(c-d)+(c-d) by XREAL_1:8; then 0/2>((t`2)-d)*2/2; then A71: 0+d>t`2 by XREAL_1:19; A*(t`1)+B<1 by A61,A69,A67,EUCLID:52; then (1)*(b-a)> (2*((t`1)-b)-(a-b))/(b-a)*(b-a) by A26,A66,XREAL_1:68; then (1)*(b-a)> 2*((t`1)-b)-(a-b) by A26,XCMPLX_1:87; then (1)*(b-a)+(a-b)> 2*((t`1)-b)-(a-b)+(a-b) by XREAL_1:8; then 0/2>((t`1)-b)*2/2; then A72: 0+b>t`1 by XREAL_1:19; -1=s0-d by A6,XREAL_1:9; then 0+(d-d)-(c-d)>=(s0-d)+(s0-d)-(c-d) by XREAL_1:9; then A76: (d-c)/(d-c)>=((s0-d)+(s0-d)-(c-d))/(d-c) by A19,XREAL_1:72; d-d>=s1-d by A8,XREAL_1:9; then A77: 0+(d-d)-(c-d)>=(s1-d)+(s1-d)-(c-d) by XREAL_1:9; c-d<=s1-d by A7,XREAL_1:9; then c-d+(c-d)<=(s1-d)+(s1-d) by XREAL_1:7; then A78: c-d+(c-d)-(c-d)<=(s1-d)+(s1-d)-(c-d) by XREAL_1:9; c-d<=s0-d by A5,XREAL_1:9; then c-d+(c-d)<=(s0-d)+(s0-d) by XREAL_1:7; then A79: c-d+(c-d)-(c-d)<=(s0-d)+(s0-d)-(c-d) by XREAL_1:9; (f2.O)`2=C*s0+D by A54,EUCLID:52 .= s0 *2/(d-c)+(1-2*d/(d-c)) .= s0 *2/(d-c)+((d-c)/(d-c)-2*d/(d-c)) by A19,XCMPLX_1:60 .= s0 *2/(d-c)+((d-c)-2*d)/(d-c) .= (s0 *2+((d-c)-2*d))/(d-c) .= ((s0-d)+(s0-d)-(c-d))/(d-c); hence thesis by A19,A79,A74,A76,A75,A78,A77,XREAL_1:72; end; set y = the Element of rng f2 /\ rng g2; A>0 by A26,XREAL_1:139; then A80: ff is one-to-one by A20,Th44; then f2 is one-to-one & g2 is one-to-one by A2,FUNCT_1:24; then rng f2 meets rng g2 by A1,A2,A55,A53,A25,A23,A73,A27,A34,A56,Th42; then A81: rng f2 /\ rng g2 <> {}; then y in rng f2 by XBOOLE_0:def 4; then consider x being object such that A82: x in dom f2 and A83: y=f2.x by FUNCT_1:def 3; dom f2 c= dom f by RELAT_1:25; then A84: f.x in rng f by A82,FUNCT_1:3; y in rng g2 by A81,XBOOLE_0:def 4; then consider x2 being object such that A85: x2 in dom g2 and A86: y=g2.x2 by FUNCT_1:def 3; A87: y=ff.(g.x2) by A85,A86,FUNCT_1:12; dom g2 c= dom g by RELAT_1:25; then A88: g.x2 in rng g by A85,FUNCT_1:3; dom ff=the carrier of TOP-REAL 2 & y=ff.(f.x) by A82,A83,FUNCT_1:12 ,FUNCT_2:def 1; then f.x=g.x2 by A80,A87,A84,A88,FUNCT_1:def 4; then rng f /\ rng g <> {} by A84,A88,XBOOLE_0:def 4; hence thesis; end; theorem {p7 where p7 is Point of TOP-REAL 2: p7`2<=p7`1 } is closed Subset of TOP-REAL 2 & {p7 where p7 is Point of TOP-REAL 2: p7`1<=p7`2 } is closed Subset of TOP-REAL 2 by Lm5,Lm8; theorem {p7 where p7 is Point of TOP-REAL 2: -p7`1<=p7`2 } is closed Subset of TOP-REAL 2 & {p7 where p7 is Point of TOP-REAL 2: p7`2<=-p7`1 } is closed Subset of TOP-REAL 2 by Lm11,Lm14; theorem {p7 where p7 is Point of TOP-REAL 2: -p7`2<=p7`1 } is closed Subset of TOP-REAL 2 & {p7 where p7 is Point of TOP-REAL 2: p7`1<=-p7`2 } is closed Subset of TOP-REAL 2 by Lm17,Lm20;