Copyright (c) 2001 Association of Mizar Users
environ
vocabulary EUCLID, PCOMPS_1, ARYTM, ARYTM_3, RELAT_1, SQUARE_1, ARYTM_1,
PRE_TOPC, SUBSET_1, BOOLE, ORDINAL2, FUNCT_1, FUNCT_4, METRIC_1,
COMPLEX1, MCART_1, JORDAN2C, FINSEQ_1, FINSEQ_2, FUNCT_5, TOPMETR,
RCOMP_1, PARTFUN1, BORSUK_1, JGRAPH_2;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, NAT_1, STRUCT_0, PARTFUN1,
PRE_TOPC, TOPMETR, PCOMPS_1, METRIC_1, RCOMP_1, FUNCT_2, SQUARE_1,
PSCOMP_1, EUCLID, JGRAPH_1, JORDAN2C, FUNCT_4, WELLFND1;
constructors REAL_1, WEIERSTR, TOPS_2, RCOMP_1, PSCOMP_1, JORDAN2C, WELLFND1,
FUNCT_4, TOPRNS_1, MEMBERED;
clusters SUBSET_1, STRUCT_0, RELSET_1, EUCLID, PRE_TOPC, TOPMETR, SQUARE_1,
PSCOMP_1, BORSUK_1, XREAL_0, ARYTM_3, MEMBERED, ZFMISC_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, AXIOMS, RELAT_1, SUBSET_1, FUNCT_1, FUNCT_2, FUNCT_4, TOPS_1,
TOPS_2, PARTFUN1, PRE_TOPC, REVROT_1, JORDAN2C, FINSEQ_2, FRECHET,
TOPMETR, JORDAN6, EUCLID, REAL_1, REAL_2, JGRAPH_1, SEQ_2, SQUARE_1,
TOPREAL3, TOPREAL6, PSCOMP_1, METRIC_1, SPPOL_2, JORDAN1A, TSEP_1,
XBOOLE_0, XBOOLE_1, XREAL_0, XCMPLX_0, XCMPLX_1;
schemes FUNCT_1, FUNCT_2;
begin
Lm1:TOP-REAL 2=TopSpaceMetr(Euclid 2) by EUCLID:def 8;
canceled;
theorem Th2: for a being real number st 1 <= a holds a <= a^2
proof let a be real number;assume A1: 1 <= a;
then a>=0 by AXIOMS:22;
then a <= a*a by A1,REAL_2:146;
hence a <= a^2 by SQUARE_1:def 3;
end;
theorem for a being real number st -1 >= a holds -a <= a^2
proof let a be real number;assume -1 >= a;
then --1<=-a by REAL_1:50;
then -a<= (-a)^2 by Th2;
hence -a <= a^2 by SQUARE_1:61;
end;
theorem Th4: for a being real number st -1 > a holds -a < a^2
proof let a be real number;assume -1 > a;
then --1< -a by REAL_1:50;
then -a< (-a)^2 by SQUARE_1:76;
hence -a < a^2 by SQUARE_1:61;
end;
theorem Th5: for a,b being real number st b^2<= a^2 & a>=0 holds
-a<=b & b<=a
proof let a,b be real number;
assume A1:b^2<= a^2 & a>=0;
now assume A2:-a>b or b>a;
now per cases by A2;
case -a>b; then --a<-b by REAL_1:50;
then a^2<(-b)^2 by A1,SQUARE_1:78;
hence contradiction by A1,SQUARE_1:61;
case b>a;
hence contradiction by A1,SQUARE_1:78;
end;
hence contradiction;
end;
hence -a<=b & b<=a;
end;
theorem Th6: for a,b being real number st b^2< a^2 & a>=0 holds
-a<b & b<a
proof let a,b be real number;
assume A1:b^2< a^2 & a>=0;
now assume A2:-a>=b or b>=a;
now per cases by A2;
case -a>=b; then --a<= -b by REAL_1:50;
then a^2<=(-b)^2 by A1,SQUARE_1:77;
hence contradiction by A1,SQUARE_1:61;
case b>=a;
hence contradiction by A1,SQUARE_1:77;
end;
hence contradiction;
end;
hence -a<b & b<a;
end;
theorem for a,b being real number st
-a<=b & b<=a holds b^2<= a^2
proof let a,b be real number;assume A1:
-a<=b & b<=a;
per cases;
suppose b>=0;
hence b^2<= a^2 by A1,SQUARE_1:77;
suppose b<0; then A2: -b>0 by REAL_1:66;
--a>=-b by A1,REAL_1:50;
then (-b)^2<= a^2 by A2,SQUARE_1:77;
hence b^2<= a^2 by SQUARE_1:61;
end;
theorem Th8: for a,b being real number st
-a<b & b<a holds b^2< a^2
proof let a,b be real number;assume A1: -a<b & b<a;
per cases;
suppose b>=0;
hence b^2< a^2 by A1,SQUARE_1:78;
suppose b<0; then A2: -b>0 by REAL_1:66;
--a>-b by A1,REAL_1:50;
then (-b)^2< a^2 by A2,SQUARE_1:78;
hence b^2< a^2 by SQUARE_1:61;
end;
reserve T,T1,T2,S for non empty TopSpace;
theorem Th9: :: BORSUK_2:1
for f being map of T1,S, g being map of T2,S,F1,F2 being Subset of T st
T1 is SubSpace of T & T2 is SubSpace of T & F1=[#] T1 & F2=[#] T2 &
([#] T1) \/ ([#] T2) = [#] T &
F1 is closed & F2 is closed &
f is continuous & g is continuous &
( for p be set st p in ([#] T1) /\ ([#] T2) holds f.p = g.p )
ex h being map of T,S st h = f+*g & h is continuous
proof
let f be map of T1,S, g be map of T2,S,F1,F2 being Subset of T;
assume that
A1: T1 is SubSpace of T & T2 is SubSpace of T and
A2:F1=[#] T1 & F2=[#] T2 and
A3: ([#] T1) \/ ([#] T2) = [#] T and
A4: F1 is closed and
A5: F2 is closed and
A6: f is continuous and
A7: g is continuous and
A8: for p be set st p in ([#] T1) /\ ([#] T2) holds f.p = g.p;
set h = f+*g;
A9: dom f = the carrier of T1 by FUNCT_2:def 1 .= [#] T1 by PRE_TOPC:12;
A10: dom g = the carrier of T2 by FUNCT_2:def 1 .= [#] T2 by PRE_TOPC:12;
then A11: dom h = [#] T by A3,A9,FUNCT_4:def 1
.= the carrier of T by PRE_TOPC:12;
rng f \/ rng g c= the carrier of S & rng h c= rng f \/ rng g
by FUNCT_4:18; then rng h c= the carrier of S by XBOOLE_1:1;
then h is Function of the carrier of T, the carrier of S by A11,FUNCT_2:4;
then reconsider h as map of T,S;
take h;
thus h = f+*g;
for P being Subset of S st P is closed holds h"P is closed
proof
let P be Subset of S;
assume A12: P is closed;
A13: h"P c= dom h & dom h = dom f \/ dom g by FUNCT_4:def 1,RELAT_1:167;
then A14: h"P = h"P /\ ([#] T1 \/ [#] T2) by A9,A10,XBOOLE_1:28
.= (h"P /\ [#](T1)) \/ (h"P /\ [#](T2)) by XBOOLE_1:23;
A15: for x being set st x in [#] T1 holds h.x = f.x
proof
let x be set such that A16: x in [#] T1;
now per cases;
suppose A17: x in [#] T2;
then x in [#] T1 /\ [#] T2 by A16,XBOOLE_0:def 3;
then f.x = g.x by A8;
hence thesis by A10,A17,FUNCT_4:14;
suppose not x in [#] T2;
hence h.x = f.x by A10,FUNCT_4:12;
end;
hence thesis;
end;
now let x be set;
thus x in h"P /\ [#] T1 implies x in f"P
proof
assume x in h"P /\ [#] T1;
then x in h"P & x in dom f & x in [#] T1 by A9,XBOOLE_0:def 3;
then h.x in P & x in dom f & f.x = h.x by A15,FUNCT_1:def 13;
hence x in f"P by FUNCT_1:def 13;
end;
assume x in f"P;
then x in dom f & f.x in P by FUNCT_1:def 13;
then x in dom h & x in [#] T1 & h.x in P by A9,A13,A15,XBOOLE_0:def 2;
then x in h"P & x in [#] T1 by FUNCT_1:def 13;
hence x in h"P /\ [#] T1 by XBOOLE_0:def 3;
end;
then A18: h"P /\ [#] T1 = f"P by TARSKI:2;
now let x be set;
thus x in h"P /\ [#] T2 implies x in g"P
proof
assume x in h"P /\ [#] T2;
then x in h"P & x in dom g & x in [#] T2 by A10,XBOOLE_0:def 3;
then h.x in P & x in dom g & g.x = h.x by FUNCT_1:def 13,FUNCT_4:14;
hence x in g"P by FUNCT_1:def 13;
end;
assume x in g"P;
then x in dom g & g.x in P by FUNCT_1:def 13;
then x in dom h & x in [#] T2 & h.x in P
by A10,A13,FUNCT_4:14,XBOOLE_0:def 2;
then x in h"P & x in [#] T2 by FUNCT_1:def 13;
hence x in h"P /\ [#] T2 by XBOOLE_0:def 3;
end;
then A19: h"P = f"P \/ g"P by A14,A18,TARSKI:2;
f"P c= the carrier of T1;
then f"P c= [#] T1 & [#] T1 c= [#] T by A3,PRE_TOPC:12,XBOOLE_1:7;
then f"P c= [#] T by XBOOLE_1:1;
then f"P is Subset of T by PRE_TOPC:12;
then reconsider P1 = f"P as Subset of T;
g"P c= the carrier of T2;
then g"P c= [#] T2 & [#] T2 c= [#] T by A3,PRE_TOPC:12,XBOOLE_1:7;
then g"P c= [#] T by XBOOLE_1:1;
then g"P is Subset of T by PRE_TOPC:12;
then reconsider P2 = g"P as Subset of T;
set P3 = f"P, P4 = g"P;
A20:P3 is closed & P4 is closed by A6,A7,A12,PRE_TOPC:def 12;
then consider F01 being Subset of T such that
A21: F01 is closed & P3=F01 /\ [#]T1 by A1,PRE_TOPC:43;
A22:P1 is closed by A2,A4,A21,TOPS_1:35;
consider F02 being Subset of T such that
A23: F02 is closed & P4=F02 /\ [#]T2 by A1,A20,PRE_TOPC:43;
P2 is closed by A2,A5,A23,TOPS_1:35;
hence h"P is closed by A19,A22,TOPS_1:36;
end;
hence thesis by PRE_TOPC:def 12;
end;
theorem Th10:for n being Nat,q2 being Point of Euclid n,
q being Point of TOP-REAL n,
r being real number st q=q2 holds
Ball(q2,r) = {q3 where q3 is Point of TOP-REAL n: |.q-q3.|<r}
proof let n be Nat,q2 be Point of (Euclid n),
q be Point of TOP-REAL n,r be real number;
assume A1:q=q2;
A2:Ball(q2,r)=
{q4 where q4 is Element of Euclid n: dist(q2,q4) < r}
by METRIC_1:18;
A3:{q4 where q4 is Element of Euclid n: dist(q2,q4) < r}
c= {q3 where q3 is Point of TOP-REAL n: |.q-q3.|<r}
proof let x be set;assume x in
{q4 where q4 is Element of Euclid n: dist(q2,q4) < r};
then consider q4 being Element of Euclid n such that
A4: q4=x & dist(q2,q4) < r;
reconsider q44=q4 as Point of TOP-REAL n by TOPREAL3:13;
dist(q2,q4)=|.q-q44.| by A1,JGRAPH_1:45;
hence thesis by A4;
end;
{q3 where q3 is Point of TOP-REAL n: |.q-q3.|<r}
c={q4 where q4 is Element of Euclid n: dist(q2,q4) < r}
proof let x be set;assume x in
{q3 where q3 is Point of TOP-REAL n: |.q-q3.|<r};
then consider q3 being Point of TOP-REAL n such that
A5: x=q3 & |.q-q3.|<r;
reconsider q34=q3 as Point of Euclid n by TOPREAL3:13;
dist(q2,q34)=|.q-q3.| by A1,JGRAPH_1:45;
hence thesis by A5;
end;
hence thesis by A2,A3,XBOOLE_0:def 10;
end;
theorem Th11:
(0.REAL 2)`1=0 & (0.REAL 2)`2=0 by EUCLID:56,58;
theorem Th12: 1.REAL 2 = <* 1, 1 *>
proof
reconsider f= (2 qua Nat |-> (1 qua Real))
as FinSequence of REAL by FINSEQ_2:77;
thus 1.REAL 2=1*2 by JORDAN2C:def 8 .=f by JORDAN2C:def 7
.=<* 1 qua Real,1 qua Real *> by FINSEQ_2:75;
end;
theorem Th13:
(1.REAL 2)`1=1 & (1.REAL 2)`2=1
proof 1.REAL 2=|[1,1]| by Th12,EUCLID:def 16;
hence thesis by EUCLID:56;
end;
theorem Th14: dom proj1=the carrier of TOP-REAL 2 & dom proj1=REAL 2
proof
thus dom proj1=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
hence thesis by EUCLID:25;
end;
theorem Th15: dom proj2=the carrier of TOP-REAL 2 & dom proj2=REAL 2
proof
thus dom proj2=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
hence thesis by EUCLID:25;
end;
theorem proj1 is map of TOP-REAL2,R^1 by TOPMETR:24;
theorem proj2 is map of TOP-REAL2,R^1 by TOPMETR:24;
theorem Th18: for p being Point of TOP-REAL 2 holds
p=|[proj1.p,proj2.p]|
proof let p be Point of TOP-REAL 2;
A1:p=|[p`1,p`2]| by EUCLID:57;
p`1=proj1.p by PSCOMP_1:def 28;
hence thesis by A1,PSCOMP_1:def 29;
end;
theorem Th19:
for B being Subset of TOP-REAL 2 st
B={0.REAL 2} holds B`<>{} & (the carrier of TOP-REAL 2)\B<>{}
proof let B be Subset of TOP-REAL 2;
assume A1:B={0.REAL 2};
now assume |[0,1]| in B;
then |[0,1]|`2=0 by A1,Th11,TARSKI:def 1;
hence contradiction by EUCLID:56;
end;
then |[0,1]| in (the carrier of TOP-REAL 2) \ B by XBOOLE_0:def 4;
hence thesis by SUBSET_1:def 5;
end;
theorem Th20: :: BORSUK_1:def 2
for X,Y being non empty TopSpace,f being map of X,Y
holds f is continuous iff for p being Point of X,V being Subset of Y
st f.p in V & V is open holds
ex W being Subset of X st p in W & W is open & f.:W c= V
proof let X,Y be non empty TopSpace,f be map of X,Y;
A1:dom f=the carrier of X by FUNCT_2:def 1;
hereby assume A2: f is continuous;
thus for p being Point of X,V being Subset of Y
st f.p in V & V is open holds
ex W being Subset of X st p in W & W is open & f.:W c= V
proof let p be Point of X,V be Subset of Y;
assume A3:f.p in V & V is open;
then A4:f"V is open by A2,TOPS_2:55;
A5:p in f"V by A1,A3,FUNCT_1:def 13;
f.:(f"V) c= V by FUNCT_1:145;
hence ex W being Subset of X st p in W & W is open & f.:W c= V
by A4,A5;
end;
end;
assume A6:for p being Point of X,V being Subset of Y
st f.p in V & V is open holds
ex W being Subset of X st p in W & W is open & f.:W c= V;
for G being Subset of Y st G is open holds f"G is open
proof let G be Subset of Y;
assume A7:G is open;
for z being set holds z in f"G iff
ex Q being Subset of X st Q is open & Q c= f"G & z in Q
proof let z be set;
now assume A8:z in f"G;
then A9: z in dom f & f.z in G by FUNCT_1:def 13;
reconsider p=z as Point of X by A8;
consider W being Subset of X such that
A10: p in W & W is open & f.:W c= G by A6,A7,A9;
A11: f"(f.:W) c= f"G by A10,RELAT_1:178;
W c= f"(f.:W) by A1,FUNCT_1:146;
then W c= f"G by A11,XBOOLE_1:1;
hence ex Q being Subset of X st Q is open & Q c= f"G & z in Q
by A10;
end;
hence thesis;
end;
hence f"G is open by TOPS_1:57;
end;
hence thesis by TOPS_2:55;
end;
theorem Th21: for p being Point of TOP-REAL 2,
G being Subset of TOP-REAL 2
st G is open & p in G
ex r being real number st r>0 & {q where q is Point of TOP-REAL 2:
p`1-r<q`1 & q`1<p`1+r & p`2-r<q`2 & q`2<p`2+r} c= G
proof let p be Point of TOP-REAL 2,G being Subset of TOP-REAL 2;
assume A1: G is open & p in G;
reconsider q2=p as Point of Euclid 2 by TOPREAL3:13;
consider r being real number such that
A2: r>0 & Ball(q2,r) c= G by A1,Lm1,TOPMETR:22;
set s=r/sqrt(2);
sqrt 2>0 by SQUARE_1:93;
then A3: s>0 by A2,REAL_2:127;
A4: Ball(q2,r)= {q3 where q3 is Point of TOP-REAL 2: |.p-q3.|<r} by Th10;
{q where q is Point of TOP-REAL 2:
p`1-s<q`1 & q`1<p`1+s & p`2-s<q`2 & q`2<p`2+s} c= Ball(q2,r)
proof let x be set;assume x in
{q where q is Point of TOP-REAL 2:
p`1-s<q`1 & q`1<p`1+s & p`2-s<q`2 & q`2<p`2+s};
then consider q being Point of TOP-REAL 2 such that
A5: q=x &
( p`1-s<q`1 & q`1<p`1+s & p`2-s<q`2 & q`2<p`2+s);
A6:(|.p-q.|)^2=((p-q)`1)^2+((p-q)`2)^2 by JGRAPH_1:46;
A7:(p-q)`1=p`1-q`1 & (p-q)`2=p`2-q`2 by TOPREAL3:8;
p`1-s+s<q`1+s by A5,REAL_1:67; then p`1<q`1+s by XCMPLX_1:27;
then p`1-q`1<q`1+s-q`1 by REAL_1:92;
then A8: p`1-q`1<s by XCMPLX_1:26;
p`1+s-s>q`1-s by A5,REAL_1:92; then p`1>q`1-s by XCMPLX_1:26;
then p`1-q`1>q`1-s-q`1 by REAL_1:92;
then p`1-q`1>q`1+-s-q`1 by XCMPLX_0:def 8;
then p`1-q`1>-s by XCMPLX_1:26;
then A9: (p`1-q`1)^2<s^2 by A8,Th8;
p`2-s+s<q`2+s by A5,REAL_1:67; then p`2<q`2+s by XCMPLX_1:27;
then p`2-q`2<q`2+s-q`2 by REAL_1:92;
then A10: p`2-q`2<s by XCMPLX_1:26;
p`2+s-s>q`2-s by A5,REAL_1:92; then p`2>q`2-s by XCMPLX_1:26;
then p`2-q`2>q`2-s-q`2 by REAL_1:92;
then p`2-q`2>q`2+-s-q`2 by XCMPLX_0:def 8;
then p`2-q`2>-s by XCMPLX_1:26;
then A11:(p`2-q`2)^2<s^2 by A10,Th8;
s^2=r^2/(sqrt(2))^2 by SQUARE_1:69
.=r^2/2 by SQUARE_1:def 4;
then s^2+s^2=r^2 by XCMPLX_1:66;
then (|.p-q.|)^2<r^2 by A6,A7,A9,A11,REAL_1:67;
then |.p-q.|<r by A2,Th6;
hence x in Ball(q2,r) by A4,A5;
end;
then {q where q is Point of TOP-REAL 2:
p`1-s<q`1 & q`1<p`1+s & p`2-s<q`2 & q`2<p`2+s} c= G by A2,XBOOLE_1:1;
hence thesis by A3;
end;
theorem Th22: for X,Y,Z being non empty TopSpace, B being Subset of Y,
C being Subset of Z,
f being map of X,Y, h being map of Y|B,Z|C
st f is continuous & h is continuous & rng f c= B & B<>{} & C<>{} holds
ex g being map 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 map of X,Y , h be map of Y|B,Z|C;
assume A1:f is continuous & h is continuous & rng f c= B & B<>{} & C<>{};
then reconsider V=B as non empty Subset of Y;
reconsider F=C as non empty Subset of Z by A1;
A2:Z|F is non empty;
A3:Y|V is non empty;
A4:the carrier of Y|B=[#](Y|B) by PRE_TOPC:12 .=B by PRE_TOPC:def 10;
the carrier of X=dom f by FUNCT_2:def 1;
then f is Function of the carrier of X,the carrier of Y|B
by A1,A4,FUNCT_2:4;
then reconsider u=f as map of X,Y|B;
reconsider G=Z|C as non empty TopSpace by A2;
reconsider H=Y|B as non empty TopSpace by A3;
reconsider k=u as map of X,H;
A5:u is continuous by A1,TOPMETR:9;
reconsider j=h as map of H,G;
A6:j*k is map of X,G;
then reconsider w=h*k as map of X,G;
A7:w is continuous by A1,A5,TOPS_2:58;
the carrier of (Z|C)=[#](Z|C) by PRE_TOPC:12
.=C by PRE_TOPC:def 10;
then h*u is Function of the carrier of X,the carrier of Z
by A6,FUNCT_2:9;
then reconsider v=h*u as map of X,Z;
v is continuous by A7,TOPMETR:7;
hence thesis;
end;
reserve p,q for Point of TOP-REAL 2;
definition
func Out_In_Sq -> Function of (the carrier of TOP-REAL 2)\{0.REAL 2},
(the carrier of TOP-REAL 2)\{0.REAL 2} means
:Def1: for p being Point of TOP-REAL 2 st p<>0.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= (the carrier of TOP-REAL 2)\{0.REAL 2} as non empty set
by Th19;
A1:BP c= the carrier of TOP-REAL 2 by XBOOLE_1:36;
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]|));
A2: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 A1,TARSKI:def 3;
now per cases;
case A3:(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.REAL 2};
then 0.REAL 2= |[1/q`1,q`2/q`1/q`1]| by TARSKI:def 1;
then 0=1/q`1 & 0=q`2/q`1/q`1 by Th11,EUCLID:56;
then A4:0=1/q`1*q`1;
now per cases;
case A5:q`1=0;
then q`2=0 by A3;
then q=0.REAL 2 by A5,EUCLID:57,58;
then q in {0.REAL 2} by TARSKI:def 1;
hence contradiction by XBOOLE_0:def 4;
case q`1<>0;
hence contradiction by A4,XCMPLX_1:88;
end;
hence contradiction;
end;
then reconsider r= |[1/q`1,q`2/q`1/q`1]| as Element of BP by XBOOLE_0:def 4;
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 A3;
hence ex y being Element of BP st
(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
y=|[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
y=|[p`1/p`2/p`2,1/p`2]|));
case A6: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.REAL 2};
then 0.REAL 2= |[q`1/q`2/q`2,1/q`2]| by TARSKI:def 1;
then (0.REAL 2)`2=1/q`2 & (0.REAL 2)`1= q`1/q`2/q`2 by EUCLID:56;
then A7:0=1/q`2*q`2 by Th11;
now per cases;
case q`2=0;
then not (0<=q`1 & -0<=q`1 or 0>=q`1 & 0<=-q`1) by A6,REAL_2:110;
then not (0<=q`1 & 0<=q`1 or 0>=q`1 & q`1<= -0) by REAL_2:110;
hence contradiction;
case q`2<>0;
hence contradiction by A7,XCMPLX_1:88;
end;
hence contradiction;
end;
then reconsider r= |[q`1/q`2/q`2,1/q`2]| as Element of BP by XBOOLE_0:def 4;
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 A6;
hence thesis;
end;
hence thesis;
end;
ex h being Function of BP, BP st for x being Element of BP holds
P[x,h.x] from FuncExD(A2);
then consider h being Function of BP,
BP such that A8: 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.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.REAL 2;
then not p in {0.REAL 2} by TARSKI:def 1;
then p in (the carrier of TOP-REAL 2)\{0.REAL 2} by XBOOLE_0:def 4;
hence thesis by A8;
end;
hence thesis;
end;
uniqueness
proof
let h1,h2 be Function of (the carrier of TOP-REAL 2)\{0.REAL 2},
(the carrier of TOP-REAL 2)\{0.REAL 2};
assume A9: ( for p being Point of TOP-REAL 2 st p<>0.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]|))&
( for p being Point of TOP-REAL 2 st p<>0.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]|));
reconsider BP= (the carrier of TOP-REAL 2)\{0.REAL 2} as non empty set
by Th19;
A10:BP c= the carrier of TOP-REAL 2 by XBOOLE_1:36;
for x being set st x in (the carrier of TOP-REAL 2)\{0.REAL 2}
holds h1.x=h2.x
proof let x be set;
assume A11: x in (the carrier of TOP-REAL 2)\{0.REAL 2};
then reconsider q=x as Point of TOP-REAL 2 by A10;
not q in {0.REAL 2} by A11,XBOOLE_0:def 4;
then A12:q<>0.REAL 2 by TARSKI:def 1;
now per cases;
case A13:(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 A9,A12;
hence h1.x=h2.x by A9,A12,A13;
case A14: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 A9,A12;
hence h1.x=h2.x by A9,A12,A14;
end;
hence h1.x=h2.x;
end;
hence h1=h2 by FUNCT_2:18;
end;
end;
theorem Th23: 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;
assume A1:not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1);
A2:-p`1<p`2 implies --p`1>-p`2 by REAL_1:50;
-p`1>p`2 implies --p`1<-p`2 by REAL_1:50;
hence thesis by A1,A2;
end;
theorem Th24: for p being Point of TOP-REAL 2 st p<>0.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.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,AXIOMS:21;
case p`2>=p`1 & p`2<=-p`1; then -p`2>=--p`1 by REAL_1:50;
hence p`1=p`2 or p`1=-p`2 by A3,AXIOMS:21;
end;
now per cases by A5;
case A6:p`1=p`2;
now assume p`1=0;
hence contradiction by A1,A6,EUCLID:57,58;
end;
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;
case A7:p`1=-p`2;
A8:now assume A9:p`1=0;
then p`2=-0 by A7;
hence contradiction by A1,A9,EUCLID:57,58;
end;
A10:-p`1=p`2 by A7;
A11:p`2<>0 by A7,A8;
A12:p`1/p`2/p`2=(-(p`2/p`2))/p`2 by A7,XCMPLX_1:188
.=(-1)/p`2 by A11,XCMPLX_1:60
.= 1/p`1 by A7,XCMPLX_1:193;
1/p`2= -(1/p`1) by A10,XCMPLX_1:189
.=-(p`2/p`1/(-p`1)) by A7,A12,XCMPLX_1:193
.=--(p`2/p`1/p`1) by XCMPLX_1:189.=p`2/p`1/p`1;
hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A1,A4,A12,Def1;
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;
case A13:p`1>=p`2 & p`1<=-p`2;
now assume A14:p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1;
A15: now per cases by A14;
case p`2<=p`1 & -p`1<=p`2; then --p`1>=-p`2 by REAL_1:50;
hence p`1=p`2 or p`1=-p`2 by A13,AXIOMS:21;
case p`2>=p`1 & p`2<=-p`1;
hence p`1=p`2 or p`1=-p`2 by A13,AXIOMS:21;
end;
now per cases by A15;
case A16:p`1=p`2;
then p`1 <> 0 by A1,EUCLID:57,58;
then p`1/p`2/p`2=1/p`1 by A16,XCMPLX_1:60;
hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A1,A14,A16,Def1;
case A17:p`1=-p`2;
A18:now assume A19:p`1=0;
then p`2=-0 by A17;
hence contradiction by A1,A19,EUCLID:57,58;
end;
A20:-p`1=p`2 by A17;
A21:p`2<>0 by A17,A18;
A22:p`1/p`2/p`2 =(-(p`2/p`2))/p`2 by A17,XCMPLX_1:188
.=(-1)/p`2 by A21,XCMPLX_1:60
.= 1/p`1 by A17,XCMPLX_1:193;
then 1/p`2=-(p`1/p`2/p`2) by A20,XCMPLX_1:189 .=-(p`2/p`1/(-p`1))
by A17,XCMPLX_1:192
.=--(p`2/p`1/p`1) by XCMPLX_1:189.=p`2/p`1/p`1;
hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A1,A14,A22,Def1;
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;
hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]|;
end;
hereby assume
A23:not(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2);
A24:-p`2<p`1 implies --p`2>-p`1 by REAL_1:50;
-p`2>p`1 implies --p`2<-p`1 by REAL_1:50;
hence Out_In_Sq.p=|[1/p`1,p`2/p`1/p`1]| by A1,A23,A24,Def1;
end;
end;
theorem Th25: 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.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;
assume A1: K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)
& p<>0.REAL 2};
A2:the carrier of ((TOP-REAL 2)|D) =[#]((TOP-REAL 2)|D) by PRE_TOPC:12
.=D by PRE_TOPC:def 10;
let y be set;assume y in rng (Out_In_Sq|K0);
then consider x being set such that
A3:x in dom (Out_In_Sq|K0)
& y=(Out_In_Sq|K0).x by FUNCT_1:def 5;
A4:x in (dom Out_In_Sq) /\ K0 by A3,FUNCT_1:68;
then A5:x in K0 by XBOOLE_0:def 3;
A6: K0 c= the carrier of TOP-REAL 2 by A2,XBOOLE_1:1;
then reconsider p=x as Point of TOP-REAL 2 by A5;
A7:Out_In_Sq.p=y by A3,A5,FUNCT_1:72;
consider px being Point of TOP-REAL 2 such that A8: x=px &
(px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1)
& px<>0.REAL 2 by A1,A5;
reconsider K00=K0 as Subset of TOP-REAL 2 by A6;
K00=[#]((TOP-REAL 2)|K00) by PRE_TOPC:def 10
.=the carrier of ((TOP-REAL 2)|K00) by PRE_TOPC:12;
then A9:p in the carrier of ((TOP-REAL 2)|K00) by A4,XBOOLE_0:def 3;
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;
assume A10:q in the carrier of (TOP-REAL 2)|K00;
the carrier of (TOP-REAL 2)|K00=[#]((TOP-REAL 2)|K00) by PRE_TOPC:12
.=K0 by PRE_TOPC:def 10;
then consider p3 being Point of TOP-REAL 2 such that
A11: q=p3 & ((p3`2<=p3`1 & -p3`1<=p3`2 or p3`2>=p3`1 & p3`2<=-p3`1)
& p3<>0.REAL 2) by A1,A10;
now assume A12:q`1=0;
then q`2=0 by A11;
hence contradiction by A11,A12,EUCLID:57,58;
end;
hence q`1<>0;
end;
then A13:p`1<>0 by A9;
set p9=|[1/p`1,p`2/p`1/p`1]|;
A14:p9`1=1/p`1 & p9`2=p`2/p`1/p`1 by EUCLID:56;
A15:now assume p9=0.REAL 2;
then 0 *p`1=1/p`1*p`1 by A14,EUCLID:56,58;
hence contradiction by A13,XCMPLX_1:88;
end;
A16:Out_In_Sq.p=|[1/p`1,p`2/p`1/p`1]| by A8,Def1;
now per cases;
case A17: 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 A8,A13,REAL_1:73;
then 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 A13,XCMPLX_1:60,175;
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 A13,A17,REAL_1:73,XCMPLX_1:90;
then p`2/p`1<=1 & -1<=p`2/p`1 or p`2/p`1>=1 & p`2<=(-1)*p`1
by A13,XCMPLX_1:60,175;
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 A13,A17,REAL_1:73;
then A18:p`2/p`1<=1 & -1<=p`2/p`1 or p`2/p`1>=1 & p`2/p`1<=-1
by A13,XCMPLX_1:90;
then (-1)/p`1<= p`2/p`1/p`1 by A13,A17,AXIOMS:22,REAL_1:73;
then A19: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 A13,A17,A18,AXIOMS:22,REAL_1:73,XCMPLX_1:188;
p9`1=1/p`1 & p9`2=p`2/p`1/p`1 by EUCLID:56;
hence y in K0 by A1,A7,A15,A16,A19;
case A20:p`1<0;
then p`2<=p`1 & (-1 *p`1)<=p`2 or p`2/p`1<=p`1/p`1 & p`2/p`1>=(-1 *p`1)/
p`1
by A8,REAL_1:74;
then 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 A20,XCMPLX_1:60,175;
then A21: 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 A20,REAL_1:74,XCMPLX_1:90;
then p`2/p`1>=1 & (-1)*p`1<=p`2 or p`2/p`1<=1 & p`2/p`1>=-1
by A20,XCMPLX_1:60,175;
then p`2/p`1>=1 & (-1)*p`1/p`1>=p`2/p`1 or p`2/p`1<=1 & p`2/p`1>=-1
by A20,REAL_1:74;
then A22:p`2/p`1>=1 & -1>=p`2/p`1 or p`2/p`1<=1 & p`2/p`1>=-1
by A20,XCMPLX_1:90;
not (p`2/p`1>=1 & p`2/p`1<=-1) by AXIOMS:22;
then (-1)/p`1>= p`2/p`1/p`1 by A20,A21,REAL_1:74,XCMPLX_1:60;
then A23: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 A20,A22,AXIOMS:22,REAL_1:74,XCMPLX_1:188;
p9`1=1/p`1 & p9`2=p`2/p`1/p`1 by EUCLID:56;
hence y in K0 by A1,A7,A15,A16,A23;
end;
then y in [#](((TOP-REAL 2)|D)|K0) by PRE_TOPC:def 10;
hence thesis;
end;
theorem Th26: 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.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;
assume A1: K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2)
& p<>0.REAL 2};
A2:the carrier of ((TOP-REAL 2)|D) =[#]((TOP-REAL 2)|D) by PRE_TOPC:12
.=D by PRE_TOPC:def 10;
let y be set;assume y in rng (Out_In_Sq|K0);
then consider x being set such that
A3:x in dom (Out_In_Sq|K0) & y=(Out_In_Sq|K0).x by FUNCT_1:def 5;
x in (dom Out_In_Sq) /\ K0 by A3,FUNCT_1:68;
then A4:x in K0 by XBOOLE_0:def 3;
A5: K0 c= the carrier of TOP-REAL 2 by A2,XBOOLE_1:1;
then reconsider p=x as Point of TOP-REAL 2 by A4;
A6:Out_In_Sq.p=y by A3,A4,FUNCT_1:72;
consider px being Point of TOP-REAL 2 such that A7: x=px &
(px`1<=px`2 & -px`2<=px`1 or px`1>=px`2 & px`1<=-px`2)
& px<>0.REAL 2 by A1,A4;
reconsider K00=K0 as Subset of TOP-REAL 2 by A5;
A8:K00=[#]((TOP-REAL 2)|K00) by PRE_TOPC:def 10
.=the carrier of ((TOP-REAL 2)|K00) by PRE_TOPC:12;
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;
assume A9:q in the carrier of (TOP-REAL 2)|K00;
the carrier of (TOP-REAL 2)|K00=[#]((TOP-REAL 2)|K00) by PRE_TOPC:12
.=K0 by PRE_TOPC:def 10;
then consider p3 being Point of TOP-REAL 2 such that
A10: q=p3 & ((p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 & p3`1<=-p3`2)
& p3<>0.REAL 2) by A1,A9;
now assume A11:q`2=0;
then q`1=0 by A10;
hence contradiction by A10,A11,EUCLID:57,58;
end;
hence q`2<>0;
end;
then A12:p`2<>0 by A4,A8;
set p9=|[p`1/p`2/p`2,1/p`2]|;
A13:p9`2=1/p`2 & p9`1=p`1/p`2/p`2 by EUCLID:56;
A14:now assume p9=0.REAL 2;
then 0 *p`2=1/p`2*p`2 by A13,EUCLID:56,58;
hence contradiction by A12,XCMPLX_1:88;
end;
A15:Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A7,Th24;
now per cases;
case A16: 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 A7,A12,REAL_1:73;
then 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 A12,XCMPLX_1:60,175;
then 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 A12,A16,REAL_1:73,XCMPLX_1:90;
then p`1/p`2<=1 & -1<=p`1/p`2 or p`1/p`2>=1 & p`1<=(-1)*p`2
by A12,XCMPLX_1:60,175;
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 A12,A16,REAL_1:73;
then A17:p`1/p`2<=1 & -1<=p`1/p`2 or p`1/p`2>=1 & p`1/p`2<=-1
by A12,XCMPLX_1:90;
then (-1)/p`2<= p`1/p`2/p`2 by A12,A16,AXIOMS:22,REAL_1:73;
then A18: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 A12,A16,A17,AXIOMS:22,REAL_1:73,XCMPLX_1:188;
p9`2=1/p`2 & p9`1=p`1/p`2/p`2 by EUCLID:56;
hence y in K0 by A1,A6,A14,A15,A18;
case A19: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 A7,REAL_1:74;
then 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 A19,XCMPLX_1:60,175;
then p`1/p`2>=p`2/p`2 & (-1 *p`2)<=p`1 or p`1/p`2<=1 & p`1/p`2>=-1
by A19,REAL_1:74,XCMPLX_1:90;
then p`1/p`2>=1 & (-1)*p`2<=p`1 or p`1/p`2<=1 & p`1/p`2>=-1
by A19,XCMPLX_1:60,175;
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 A19,REAL_1:74;
then A20:p`1/p`2>=1 & -1>=p`1/p`2 or p`1/p`2<=1 & p`1/p`2>=-1
by A19,XCMPLX_1:90;
then (-1)/p`2>= p`1/p`2/p`2 by A19,AXIOMS:22,REAL_1:74;
then A21: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 A19,A20,AXIOMS:22,REAL_1:74,XCMPLX_1:188;
p9`2=1/p`2 & p9`1=p`1/p`2/p`2 by EUCLID:56;
hence y in K0 by A1,A6,A14,A15,A21;
end;
then y in [#](((TOP-REAL 2)|D)|K0) by PRE_TOPC:def 10;
hence thesis;
end;
theorem Th27: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.REAL 2}
& D`={0.REAL 2}
holds K0a is non empty Subset of (TOP-REAL 2)|D &
K0a is non empty Subset of TOP-REAL 2
proof let K0a be set,D be non empty Subset of TOP-REAL 2;
assume A1: 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.REAL 2}
& D`={0.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) &
(1.REAL 2)<>0.REAL 2 by Th13,REVROT_1:19;
then A2:1.REAL 2 in K0a by A1;
A3:the carrier of (TOP-REAL 2)|D=[#]((TOP-REAL 2)|D) by PRE_TOPC:12
.=D by PRE_TOPC:def 10;
A4:K0a c= D
proof let x be set;assume x in K0a;
then consider p8 being Point of TOP-REAL 2 such that
A5: x=p8
& (
(p8`2<=p8`1 & -p8`1<=p8`2 or p8`2>=p8`1 & p8`2<=-p8`1) & p8<>0.REAL 2)
by A1;
A6:D=D``
.=(the carrier of TOP-REAL 2) \ {0.REAL 2} by A1,SUBSET_1:def 5;
not x in {0.REAL 2} by A5,TARSKI:def 1;
hence x in D by A5,A6,XBOOLE_0:def 4;
end;
hence K0a is non empty Subset of ((TOP-REAL 2)|D) by A2,A3;
K0a c= the carrier of TOP-REAL 2 by A4,XBOOLE_1:1;
hence thesis by A2;
end;
theorem Th28: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.REAL 2}
& D`={0.REAL 2}
holds K0a is non empty Subset of (TOP-REAL 2)|D &
K0a is non empty Subset of TOP-REAL 2
proof let K0a be set,D be non empty Subset of TOP-REAL 2;
assume A1: 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.REAL 2}
& D`={0.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) &
(1.REAL 2)<>0.REAL 2
by Th13,REVROT_1:19;
then A2:1.REAL 2 in K0a by A1;
A3:the carrier of (TOP-REAL 2)|D=[#]((TOP-REAL 2)|D) by PRE_TOPC:12
.=D by PRE_TOPC:def 10;
A4:K0a c= D
proof let x be set;assume x in K0a;
then consider p8 being Point of TOP-REAL 2 such that
A5: x=p8 & (
(p8`1<=p8`2 & -p8`2<=p8`1 or p8`1>=p8`2 & p8`1<=-p8`2) & p8<>0.REAL 2)
by A1;
A6:D=D``
.=(the carrier of TOP-REAL 2) \ {0.REAL 2} by A1,SUBSET_1:def 5;
not x in {0.REAL 2} by A5,TARSKI:def 1;
hence x in D by A5,A6,XBOOLE_0:def 4;
end;
hence K0a is non empty Subset of ((TOP-REAL 2)|D)
by A2,A3;
K0a c= the carrier of TOP-REAL 2 by A4,XBOOLE_1:1;
hence thesis by A2;
end;
theorem Th29: for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous &
f2 is continuous holds ex g being map of X,R^1
st (for p being Point of X,r1,r2 being real number 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 map of X,R^1;
assume A1: f1 is continuous & f2 is continuous;
defpred P[set,set] means
(for r1,r2 being real number st f1.$1=r1 & f2.$1=r2 holds $2=r1+r2);
A2: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 by TOPMETR:24;
reconsider r2=f2.x as Real by TOPMETR:24;
set r3=r1+r2;
for r1,r2 being real number st f1.x=r1 & f2.x=r2 holds r3=r1+r2;
hence ex y being Element of REAL
st (for r1,r2 being real number 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 FuncExD(A2);
then consider f being Function of the carrier of X,REAL
such that A3: for x being Element of X holds
(for r1,r2 being real number st f1.x=r1 & f2.x=r2 holds f.x=r1+r2);
reconsider g0=f as map of X,R^1 by TOPMETR:24;
A4: for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g0.p=r1+r2 by A3;
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;
assume A5:g0.p in V & V is open;
reconsider r=g0.p as Real by TOPMETR:24;
consider r0 being Real such that
A6: r0>0 & ].r-r0,r+r0.[ c= V by A5,FRECHET:8;
reconsider r1=f1.p as Real by TOPMETR:24;
reconsider G1=].r1-r0/2,r1+r0/2.[ as Subset of R^1
by TOPMETR:24;
r0/2>0 by A6,SEQ_2:3;
then A7:r1<r1+r0/2 by REAL_1:69;
then r1-r0/2<r1 by REAL_1:84;
then A8:f1.p in G1 by A7,JORDAN6:45;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A9: p in W1 & W1 is open & f1.:W1 c= G1 by A1,A8,Th20;
reconsider r2=f2.p as Real by TOPMETR:24;
reconsider G2=].r2-r0/2,r2+r0/2.[ as Subset of R^1
by TOPMETR:24;
r0/2>0 by A6,SEQ_2:3;
then A10:r2<r2+r0/2 by REAL_1:69;
then r2-r0/2<r2 by REAL_1:84;
then A11:f2.p in G2 by A10,JORDAN6:45;
G2 is open by JORDAN6:46;
then consider W2 being Subset of X such that
A12: p in W2 & W2 is open & f2.:W2 c= G2 by A1,A11,Th20;
set W=W1 /\ W2;
A13:W is open by A9,A12,TOPS_1:38;
A14:p in W by A9,A12,XBOOLE_0:def 3;
g0.:W c= ].r-r0,r+r0.[
proof let x be set;assume x in g0.:W;
then consider z being set such that
A15: z in dom g0 & z in W & g0.z=x by FUNCT_1:def 12;
A16:z in W1 by A15,XBOOLE_0:def 3;
reconsider pz=z as Point of X by A15;
A17:pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then A18:f1.pz in f1.:W1 by A16,FUNCT_1:def 12;
reconsider aa1=f1.pz as Real by TOPMETR:24;
A19:z in W2 by A15,XBOOLE_0:def 3;
pz in dom f2 by A17,FUNCT_2:def 1;
then A20:f2.pz in f2.:W2 by A19,FUNCT_1:def 12;
reconsider aa2=f2.pz as Real by TOPMETR:24;
A21:x=aa1+aa2 by A3,A15;
then reconsider rx=x as Real;
A22:r1-r0/2<aa1 & aa1<r1+r0/2 by A9,A18,JORDAN6:45;
A23:r2-r0/2<aa2 & aa2<r2+r0/2 by A12,A20,JORDAN6:45;
then aa1+aa2<r1+r0/2+(r2+r0/2) by A22,REAL_1:67;
then aa1+aa2<r1+r0/2+r2+r0/2 by XCMPLX_1:1;
then aa1+aa2<r1+r2+r0/2+r0/2 by XCMPLX_1:1;
then aa1+aa2<r1+r2+(r0/2+r0/2) by XCMPLX_1:1;
then aa1+aa2<r1+r2+r0 by XCMPLX_1:66;
then A24:rx<r+r0 by A3,A21;
r1-r0/2+(r2-r0/2)<aa1+aa2 by A22,A23,REAL_1:67;
then r1-r0/2+r2-r0/2<aa1+aa2 by XCMPLX_1:29;
then r1+r2-r0/2-r0/2<aa1+aa2 by XCMPLX_1:29;
then r1+r2-(r0/2+r0/2)<aa1+aa2 by XCMPLX_1:36;
then r1+r2-r0<aa1+aa2 by XCMPLX_1:66;
then r-r0<aa1+aa2 by A3;
hence x in ].r-r0,r+r0.[ by A21,A24,JORDAN6:45;
end;
then g0.:W c= V by A6,XBOOLE_1:1;
hence ex W being Subset of X st p in W & W is open & g0.:W c= V
by A13,A14;
end;
then g0 is continuous by Th20;
hence thesis by A4;
end;
theorem for X being non empty TopSpace, a being real number holds
ex g being map of X,R^1 st (for p being Point of X holds g.p=a)
& g is continuous
proof let X be non empty TopSpace,a be real number;
deffunc F(set)=a;
ex g being Function st dom g=the carrier of X & for x being set st x in
the carrier of X holds g.x=F(x) from Lambda;
then consider g1 being Function such that
A1: dom g1=the carrier of X
& for x being set st x in
the carrier of X holds g1.x=a;
rng g1 c= the carrier of R^1
proof let y be set;assume y in rng g1;
then consider x being set such that
A2: x in dom g1 & y=g1.x by FUNCT_1:def 5;
a in REAL by XREAL_0:def 1;
hence y in the carrier of R^1 by A1,A2,TOPMETR:24;
end;
then g1 is Function of the carrier of X,the carrier of R^1 by A1,FUNCT_2:4;
then reconsider g0=g1 as map of X,R^1;
A3:for p being Point of X holds g1.p=a by A1;
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;
assume A4:g0.p in V & V is open;
set f1=g0;
set G1=V;
A5:[#]X is open by TOPS_1:53;
A6:f1.: [#]X c= G1
proof let y be set;assume y in f1.: [#]X;
then consider x being set such that
A7:x in dom f1 & x in [#]X & y=f1.x by FUNCT_1:def 12;
y=a by A1,A7;
hence y in G1 by A1,A4;
end;
p in the carrier of X;
then p in [#]X by PRE_TOPC:12;
hence ex W being Subset of X st p in W & W is open & g0.:W c= V by A5,A6;
end;
then g0 is continuous by Th20;
hence thesis by A3;
end;
theorem Th31: for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous &
f2 is continuous holds ex g being map of X,R^1
st (for p being Point of X,r1,r2 being real number 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 map of X,R^1;
assume A1: f1 is continuous & f2 is continuous;
defpred P[set,set] means
(for r1,r2 being real number st f1.$1=r1 & f2.$1=r2 holds $2=r1-r2);
A2: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 by TOPMETR:24;
reconsider r2=f2.x as Real by TOPMETR:24;
set r3=r1-r2;
for r1,r2 being real number st f1.x=r1 & f2.x=r2 holds r3=r1-r2;
hence ex y being Element of REAL
st (for r1,r2 being real number 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 FuncExD(A2);
then consider f being Function of the carrier of X,REAL
such that A3: for x being Element of X holds
(for r1,r2 being real number st f1.x=r1 & f2.x=r2 holds f.x=r1-r2);
reconsider g0=f as map of X,R^1 by TOPMETR:24;
A4: for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g0.p=r1-r2 by A3;
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;
assume A5:g0.p in V & V is open;
reconsider r=g0.p as Real by TOPMETR:24;
consider r0 being Real such that
A6: r0>0 & ].r-r0,r+r0.[ c= V by A5,FRECHET:8;
reconsider r1=f1.p as Real by TOPMETR:24;
reconsider G1=].r1-r0/2,r1+r0/2.[ as Subset of R^1
by TOPMETR:24;
r0/2>0 by A6,SEQ_2:3;
then A7:r1<r1+r0/2 by REAL_1:69;
then r1-r0/2<r1 by REAL_1:84;
then A8:f1.p in G1 by A7,JORDAN6:45;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A9: p in W1 & W1 is open & f1.:W1 c= G1 by A1,A8,Th20;
reconsider r2=f2.p as Real by TOPMETR:24;
reconsider G2=].r2-r0/2,r2+r0/2.[ as Subset of R^1
by TOPMETR:24;
r0/2>0 by A6,SEQ_2:3;
then A10:r2<r2+r0/2 by REAL_1:69;
then r2-r0/2<r2 by REAL_1:84;
then A11:f2.p in G2 by A10,JORDAN6:45;
G2 is open by JORDAN6:46;
then consider W2 being Subset of X such that
A12: p in W2 & W2 is open & f2.:W2 c= G2 by A1,A11,Th20;
set W=W1 /\ W2;
A13:W is open by A9,A12,TOPS_1:38;
A14:p in W by A9,A12,XBOOLE_0:def 3;
g0.:W c= ].r-r0,r+r0.[
proof let x be set;assume x in g0.:W;
then consider z being set such that
A15: z in dom g0 & z in W & g0.z=x by FUNCT_1:def 12;
A16:z in W1 by A15,XBOOLE_0:def 3;
reconsider pz=z as Point of X by A15;
A17:pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then A18:f1.pz in f1.:W1 by A16,FUNCT_1:def 12;
reconsider aa1=f1.pz as Real by TOPMETR:24;
A19:z in W2 by A15,XBOOLE_0:def 3;
pz in dom f2 by A17,FUNCT_2:def 1;
then A20:f2.pz in f2.:W2 by A19,FUNCT_1:def 12;
reconsider aa2=f2.pz as Real by TOPMETR:24;
A21:x=aa1-aa2 by A3,A15;
then reconsider rx=x as Real;
A22:r1-r0/2<aa1 & aa1<r1+r0/2 by A9,A18,JORDAN6:45;
A23:r2-r0/2<aa2 & aa2<r2+r0/2 by A12,A20,JORDAN6:45;
then aa1-aa2<r1+r0/2-(r2-r0/2) by A22,REAL_1:92;
then aa1-aa2<r1+r0/2-r2+r0/2 by XCMPLX_1:37;
then aa1-aa2<r1-r2+r0/2+r0/2 by XCMPLX_1:29;
then aa1-aa2<r1-r2+(r0/2+r0/2) by XCMPLX_1:1;
then aa1-aa2<r1-r2+r0 by XCMPLX_1:66;
then A24:rx<r+r0 by A3,A21;
r1-r0/2-(r2+r0/2)<aa1-aa2 by A22,A23,REAL_1:92;
then r1-r0/2-r2-r0/2<aa1-aa2 by XCMPLX_1:36;
then r1-r2-r0/2-r0/2<aa1-aa2 by XCMPLX_1:21;
then r1-r2-(r0/2+r0/2)<aa1-aa2 by XCMPLX_1:36;
then r1-r2-r0<aa1-aa2 by XCMPLX_1:66;
then r-r0<aa1-aa2 by A3;
hence x in ].r-r0,r+r0.[ by A21,A24,JORDAN6:45;
end;
then g0.:W c= V by A6,XBOOLE_1:1;
hence ex W being Subset of X st p in W & W is open & g0.:W c= V
by A13,A14;
end;
then g0 is continuous by Th20;
hence thesis by A4;
end;
theorem Th32:
for X being non empty TopSpace, f1 being map of X,R^1 st f1 is continuous
ex g being map of X,R^1 st (for p being Point of X,r1 being real number st
f1.p=r1 holds g.p=r1*r1) & g is continuous
proof let X being non empty TopSpace,f1 be map of X,R^1;
assume A1: f1 is continuous;
defpred P[set,set] means
(for r1 being real number st f1.$1=r1 holds $2=r1*r1);
A2: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 by TOPMETR:24;
set r3=r1*r1;
for r1 being real number st f1.x=r1 holds r3=r1*r1;
hence ex y being Element of REAL
st (for r1 being real number st f1.x=r1 holds y=r1*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 FuncExD(A2);
then consider f being Function of the carrier of X,REAL
such that A3: for x being Element of X holds
(for r1 being real number st f1.x=r1 holds f.x=r1*r1);
reconsider g0=f as map of X,R^1 by TOPMETR:24;
A4: for p being Point of X,r1 being real number st
f1.p=r1 holds g0.p=r1*r1 by A3;
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;
assume A5:g0.p in V & V is open;
reconsider r=g0.p as Real by TOPMETR:24;
consider r0 being Real such that
A6: r0>0 & ].r-r0,r+r0.[ c= V by A5,FRECHET:8;
reconsider r1=f1.p as Real by TOPMETR:24;
A7: r=r1*r1 by A3;
then A8:r=r1^2 by SQUARE_1:def 3;
then A9:0<=r by SQUARE_1:72;
A10: r+r0>=r+0 by A6,REAL_1:55;
then A11:(sqrt(r+r0))^2=r+r0 by A9,SQUARE_1:def 4;
now per cases;
case A12:r1>=0;
then A13: r1=sqrt r by A8,A9,SQUARE_1:def 4;
set r4=sqrt(r+r0)-sqrt(r);
r+r0>r by A6,REAL_1:69;
then sqrt(r+r0)>sqrt(r) by A9,SQUARE_1:95;
then A14:r4>0 by SQUARE_1:11;
r4^2=(sqrt(r+r0))^2-2*sqrt(r+r0)*sqrt(r)+(sqrt(r))^2 by SQUARE_1:64
.=r+r0-2*sqrt(r+r0)*sqrt(r)+(sqrt(r))^2 by A9,A10,SQUARE_1:def 4
.=r+r0-2*sqrt(r+r0)*sqrt(r)+r by A9,SQUARE_1:def 4
.=r+(r0-2*sqrt(r+r0)*sqrt(r))+r by XCMPLX_1:29
.=r+r+(r0-2*sqrt(r+r0)*sqrt(r)) by XCMPLX_1:1
.=2*r+(r0-2*sqrt(r+r0)*sqrt(r)) by XCMPLX_1:11
.=2*r+r0-2*sqrt(r+r0)*sqrt(r) by XCMPLX_1:29;
then A15:2*r1*r4+r4^2= 2*r1*sqrt(r+r0)-2*r1*sqrt(r)
+(2*r+r0-2*sqrt(r+r0)*sqrt(r)) by XCMPLX_1:40
.= (2*r1*sqrt(r+r0)-2*r1*r1)
+(2*(r1*r1)+r0)-2*sqrt(r+r0)*r1 by A7,A13,XCMPLX_1:29
.= 2*r1*sqrt(r+r0)-2*r1*r1
+(2*(r1*r1)+r0)-2*(sqrt(r+r0)*r1) by XCMPLX_1:4
.= 2*r1*sqrt(r+r0)-2*r1*r1
+(2*r1*r1+r0)-2*(sqrt(r+r0)*r1) by XCMPLX_1:4
.= (2*r1*sqrt(r+r0)-2*r1*r1)
+2*r1*r1+r0-2*(sqrt(r+r0)*r1) by XCMPLX_1:1
.= 2*r1*sqrt(r+r0)-(2*r1*r1
-2*r1*r1)+r0-2*(sqrt(r+r0)*r1) by XCMPLX_1:37
.= 2*r1*sqrt(r+r0)-0+r0-2*(sqrt(r+r0)*r1) by XCMPLX_1:14
.= 2*r1*sqrt(r+r0)+r0-2*r1*sqrt(r+r0) by XCMPLX_1:4
.=r0 by XCMPLX_1:26;
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1
by TOPMETR:24;
A16:r1<r1+r4 by A14,REAL_1:69;
then r1-r4<r1 by REAL_1:84;
then A17:f1.p in G1 by A16,JORDAN6:45;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A18: p in W1 & W1 is open & f1.:W1 c= G1 by A1,A17,Th20;
set W=W1;
g0.:W c= ].r-r0,r+r0.[
proof let x be set;assume x in g0.:W;
then consider z being set such that
A19: z in dom g0 & z in W & g0.z=x by FUNCT_1:def 12;
reconsider pz=z as Point of X by A19;
pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then A20:f1.pz in f1.:W1 by A19,FUNCT_1:def 12;
reconsider aa1=f1.pz as Real by TOPMETR:24;
A21:x=aa1*aa1 by A3,A19;
then reconsider rx=x as Real;
A22:r1-r4<aa1 & aa1<r1+r4 by A18,A20,JORDAN6:45;
-0<=r1 by A12;
then -r1<=0 by REAL_2:110;
then -r1-r4<=r1-r4 by A12,REAL_1:49;
then -(r4+r1)<=r1-r4 by XCMPLX_1:161;
then -(r1+r4)<aa1 by A22,AXIOMS:22;
then aa1--(r1+r4)>0 by SQUARE_1:11;
then A23:r1+r4+aa1>0 by XCMPLX_1:151;
r1+r4-aa1>0 by A22,SQUARE_1:11;
then (r1+r4-aa1)*(r1+r4+aa1)>0 by A23,REAL_2:122;
then (r1+r4)^2-aa1^2>0 by SQUARE_1:67;
then A24: aa1^2<(r1+r4)^2 by REAL_2:106;
(r1+r4)^2 =r1^2+2*r1*r4+r4^2 by SQUARE_1:63
.=r+2*r1*r4+r4^2 by A7,SQUARE_1:def 3
.=r+r0 by A15,XCMPLX_1:1;
then A25:rx<r+r0 by A21,A24,SQUARE_1:def 3;
aa1^2>=0 by SQUARE_1:72;
then A26:0<=aa1*aa1 by SQUARE_1:def 3;
now per cases;
case 0<=r1-r4;
then A27: (r1-r4)^2<aa1^2 by A22,SQUARE_1:78;
r4^2>=0 by SQUARE_1:72;
then (-2)*r4^2<=0 by REAL_2:123;
then -2*r4^2<=0 by XCMPLX_1:175;
then (r1-r4)^2 -aa1^2+-2*r4^2<= (r1-r4)^2 -aa1^2+0 by REAL_1:55;
then (r1-r4)^2 +-2*r4^2 -aa1^2<= (r1-r4)^2 -aa1^2 by XCMPLX_1:29;
then (r1-r4)^2 -2*r4^2 -aa1^2<= (r1-r4)^2 -aa1^2 by XCMPLX_0:def 8;
then (r1-r4)^2 -2*r4^2 -aa1^2<0 by A27,REAL_2:105;
then A28: aa1^2>(r1-r4)^2 -2*r4^2 by SQUARE_1:12;
(r1-r4)^2 -2*r4^2=r1^2-2*r1*r4+r4^2-2*r4^2 by SQUARE_1:64
.=r1^2-2*r1*r4+r4^2-(r4^2+r4^2) by XCMPLX_1:11
.=r1^2-2*r1*r4+(r4^2-(r4^2+r4^2)) by XCMPLX_1:29
.=r1^2-2*r1*r4+(r4^2-r4^2-r4^2) by XCMPLX_1:36
.=r1^2-2*r1*r4+(0-r4^2) by XCMPLX_1:14
.=r-2*r1*r4+-r4^2 by A8,XCMPLX_1:150
.=r-2*r1*r4-r4^2 by XCMPLX_0:def 8
.=r-r0 by A15,XCMPLX_1:36;
hence r-r0< aa1*aa1 by A28,SQUARE_1:def 3;
case 0>r1-r4; then r1<r4 by SQUARE_1:12;
then r1^2<r4^2 by A12,SQUARE_1:78;
then A29:r1^2-r4^2<0 by REAL_2:105;
2*r1>=0 by A12,REAL_2:121;
then 2*r1*r4>=0 by A14,REAL_2:121;
then r1^2-r4^2 -2*r1*r4<0-0 by A29,REAL_1:92;
hence r-r0< aa1*aa1 by A8,A15,A26,XCMPLX_1:36;
end;
hence x in ].r-r0,r+r0.[ by A21,A25,JORDAN6:45;
end;
then g0.:W c= V by A6,XBOOLE_1:1;
hence ex W being Subset of X st p in W & W is open & g0.:W c= V by A18;
case A30:r1<0;
then A31:-r1>0 by REAL_1:66;
A32: (-r1)^2=r1^2 by SQUARE_1:61;
then A33: -r1=sqrt r by A8,A31,SQUARE_1:89;
A34:(sqrt(r))^2 =r1^2 by A8,A31,A32,SQUARE_1:89;
set r4=sqrt(r+r0)-sqrt(r);
r+r0>r by A6,REAL_1:69;
then sqrt(r+r0)>sqrt(r) by A9,SQUARE_1:95;
then A35:r4>0 by SQUARE_1:11;
r4^2=r+r0-2*sqrt(r+r0)*sqrt(r)+(sqrt(r))^2 by A11,SQUARE_1:64
.=r+(r0-2*sqrt(r+r0)*sqrt(r))+r by A8,A34,XCMPLX_1:29
.=r+r+(r0-2*sqrt(r+r0)*sqrt(r)) by XCMPLX_1:1
.=2*r+(r0-2*sqrt(r+r0)*sqrt(r)) by XCMPLX_1:11
.=2*r+r0-2*sqrt(r+r0)*sqrt(r) by XCMPLX_1:29;
then A36:-2*r1*r4+r4^2= -(2*r1*sqrt(r+r0)-2*r1*sqrt(r))
+(2*r+r0-2*sqrt(r+r0)*sqrt(r)) by XCMPLX_1:40
.= -(2*r1*sqrt(r+r0)-2*r1*(-r1))
+(2*(r1*r1)+r0)-2*sqrt(r+r0)*(-r1) by A7,A33,XCMPLX_1:29
.= -(2*r1*sqrt(r+r0)-2*(r1*(-r1)))
+(2*(r1*r1)+r0)-2*sqrt(r+r0)*(-r1) by XCMPLX_1:4
.= -(2*r1*sqrt(r+r0)-2*(-(r1*r1)))
+(2*(r1*r1)+r0)-2*sqrt(r+r0)*(-r1) by XCMPLX_1:175
.= -(2*r1*sqrt(r+r0)--2*(r1*r1))
+(2*(r1*r1)+r0)-2*sqrt(r+r0)*(-r1) by XCMPLX_1:175
.= -(2*r1*sqrt(r+r0)--(2*r1*r1))
+(2*(r1*r1)+r0)-2*sqrt(r+r0)*(-r1) by XCMPLX_1:4
.= -(2*r1*sqrt(r+r0)--(2*r1*r1))
+(2*(r1*r1)+r0)-2*(sqrt(r+r0)*(-r1)) by XCMPLX_1:4
.= -(2*r1*sqrt(r+r0)+2*r1*r1)
+(2*(r1*r1)+r0)-2*(sqrt(r+r0)*(-r1)) by XCMPLX_1:151
.= -(2*r1*sqrt(r+r0)+2*r1*r1)
+(2*(r1*r1)+r0)-2*(-(sqrt(r+r0)*r1)) by XCMPLX_1:175
.= -(2*r1*sqrt(r+r0)+2*r1*r1)
+(2*(r1*r1)+r0)--(2*(sqrt(r+r0)*r1)) by XCMPLX_1:175
.= -(2*r1*sqrt(r+r0)+2*r1*r1)
+(2*(r1*r1)+r0)+2*(sqrt(r+r0)*r1) by XCMPLX_1:151
.= -(2*r1*sqrt(r+r0)+2*r1*r1)
+(2*r1*r1+r0)+2*(sqrt(r+r0)*r1) by XCMPLX_1:4
.= -(2*r1*sqrt(r+r0)+2*r1*r1)
+2*r1*r1+r0+2*(sqrt(r+r0)*r1) by XCMPLX_1:1
.= (-2*r1*sqrt(r+r0)-2*r1*r1)
+2*r1*r1+r0+2*(sqrt(r+r0)*r1) by XCMPLX_1:161
.= (-2*r1*sqrt(r+r0)+2*r1*r1)
-2*r1*r1+r0+2*(sqrt(r+r0)*r1) by XCMPLX_1:29
.= -2*r1*sqrt(r+r0)+(2*r1*r1
-2*r1*r1)+r0+2*(sqrt(r+r0)*r1) by XCMPLX_1:29
.= -2*r1*sqrt(r+r0)+0+r0+2*(sqrt(r+r0)*r1) by XCMPLX_1:14
.= -2*r1*sqrt(r+r0)+r0+2*r1*sqrt(r+r0) by XCMPLX_1:4
.= 2*r1*sqrt(r+r0)+ -2*r1*sqrt(r+r0)+r0 by XCMPLX_1:1
.=r0 by XCMPLX_1:138;
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1
by TOPMETR:24;
A37:r1<r1+r4 by A35,REAL_1:69;
then r1-r4<r1 by REAL_1:84;
then A38:f1.p in G1 by A37,JORDAN6:45;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A39: p in W1 & W1 is open & f1.:W1 c= G1 by A1,A38,Th20;
set W=W1;
g0.:W c= ].r-r0,r+r0.[
proof let x be set;assume x in g0.:W;
then consider z being set such that
A40: z in dom g0 & z in W & g0.z=x by FUNCT_1:def 12;
reconsider pz=z as Point of X by A40;
pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then A41:f1.pz in f1.:W1 by A40,FUNCT_1:def 12;
reconsider aa1=f1.pz as Real by TOPMETR:24;
A42:x=aa1*aa1 by A3,A40;
then reconsider rx=x as Real;
A43:r1-r4<aa1 & aa1<r1+r4 by A39,A41,JORDAN6:45;
-r1>=r1 by A30,A31,AXIOMS:22;
then -r1-r4>=r1-r4 by REAL_1:49;
then -(-r1-r4)<=-(r1-r4) by REAL_1:50;
then r1+r4<=-(r1-r4) by XCMPLX_1:164;
then -(r1-r4)>aa1 by A43,AXIOMS:22;
then -(r1-r4)+(r1-r4)>aa1+(r1-r4) by REAL_1:67;
then (r1-r4)-(r1-r4)>aa1+(r1-r4) by XCMPLX_0:def 8;
then A44:r1-r4+aa1<0 by XCMPLX_1:14;
aa1-(r1-r4)>0 by A43,SQUARE_1:11;
then -(-aa1+(r1-r4))>0 by XCMPLX_1:163;
then ((r1-r4)+-aa1)<0 by REAL_1:66;
then r1-r4-aa1<0 by XCMPLX_0:def 8;
then (r1-r4-aa1)*(r1-r4+aa1)>0 by A44,REAL_2:122;
then (r1-r4)^2-aa1^2>0 by SQUARE_1:67;
then A45: aa1^2<(r1-r4)^2 by REAL_2:106;
(r1-r4)^2 =r1^2-2*r1*r4+r4^2 by SQUARE_1:64
.=r+-2*r1*r4+r4^2 by A8,XCMPLX_0:def 8
.=r+r0 by A36,XCMPLX_1:1;
then A46:rx<r+r0 by A42,A45,SQUARE_1:def 3;
aa1^2>=0 by SQUARE_1:72;
then A47:0<=aa1*aa1 by SQUARE_1:def 3;
now per cases;
case 0>=r1+r4;
then A48:-0<=-(r1+r4) by REAL_1:50;
-aa1>-(r1+r4) by A43,REAL_1:50;
then (-(r1+r4))^2<(-aa1)^2 by A48,SQUARE_1:78;
then (r1+r4)^2<(-aa1)^2 by SQUARE_1:61;
then A49: (r1+r4)^2<aa1^2 by SQUARE_1:61;
r4^2>=0 by SQUARE_1:72;
then (-2)*r4^2<=0 by REAL_2:123;
then -2*r4^2<=0 by XCMPLX_1:175;
then (r1+r4)^2 -aa1^2+-2*r4^2<= (r1+r4)^2 -aa1^2+0 by REAL_1:55;
then (r1+r4)^2 +-2*r4^2 -aa1^2<= (r1+r4)^2 -aa1^2 by XCMPLX_1:29;
then (r1+r4)^2 -2*r4^2 -aa1^2<= (r1+r4)^2 -aa1^2 by XCMPLX_0:def 8;
then (r1+r4)^2 -2*r4^2 -aa1^2<0 by A49,REAL_2:105;
then A50: aa1^2>(r1+r4)^2 -2*r4^2 by SQUARE_1:12;
(r1+r4)^2 -2*r4^2=r1^2+2*r1*r4+r4^2-2*r4^2 by SQUARE_1:63
.=r1^2+2*r1*r4+r4^2-(r4^2+r4^2) by XCMPLX_1:11
.=r1^2+2*r1*r4+(r4^2-(r4^2+r4^2)) by XCMPLX_1:29
.=r1^2+2*r1*r4+(r4^2-r4^2-r4^2) by XCMPLX_1:36
.=r1^2+2*r1*r4+(0-r4^2) by XCMPLX_1:14
.=r+2*r1*r4+-r4^2 by A8,XCMPLX_1:150
.=r+2*r1*r4-r4^2 by XCMPLX_0:def 8
.=r--2*r1*r4-r4^2 by XCMPLX_1:151
.=r-r0 by A36,XCMPLX_1:36;
hence r-r0< aa1*aa1 by A50,SQUARE_1:def 3;
case 0<r1+r4; then 0+-r1<(r1+r4)+-r1 by REAL_1:67;
then -r1<r4 by XCMPLX_1:137;
then (-r1)^2<r4^2 by A31,SQUARE_1:78;
then r1^2<r4^2 by SQUARE_1:61;
then r1^2 -r1^2>r1^2-r4^2 by REAL_1:92;
then A51:r1^2-r4^2<0 by XCMPLX_1:14;
2*r1<=0 by A30,REAL_2:123;
then 2*r1*r4<=0 by A35,REAL_2:123;
then A52:r1^2-r4^2 +2*r1*r4<0+0 by A51,REAL_1:67;
r1^2-r4^2 +2*r1*r4=r+2*r1*r4-r4^2 by A8,XCMPLX_1:29
.=r--2*r1*r4-r4^2 by XCMPLX_1:151
.=r-r0 by A36,XCMPLX_1:36;
hence r-r0< aa1*aa1 by A47,A52;
end;
hence x in ].r-r0,r+r0.[ by A42,A46,JORDAN6:45;
end;
then g0.:W c= V by A6,XBOOLE_1:1;
hence ex W being Subset of X st p in W & W is open & g0.:W c= V by A39;
end;
hence ex W being Subset of X st p in W & W is open & g0.:W c= V;
end;
then g0 is continuous by Th20;
hence thesis by A4;
end;
theorem Th33: for X being non empty TopSpace,
f1 being map of X,R^1,a being real number st f1 is continuous
holds ex g being map of X,R^1
st (for p being Point of X,r1 being real number st
f1.p=r1 holds g.p=a*r1) & g is continuous
proof
let X being non empty TopSpace,f1 be map of X,R^1,a being real number;
assume A1: f1 is continuous;
defpred P[set,set] means
(for r1 being Real st f1.$1=r1 holds $2=a*r1);
A2: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 by TOPMETR:24;
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 FuncExD(A2);
then consider f being Function of the carrier of X,REAL
such that A3: for x being Element of X holds
(for r1 being Real st f1.x=r1 holds f.x=a*r1);
reconsider g0=f as map of X,R^1 by TOPMETR:24;
A4: for p being Point of X,r1 being real number st
f1.p=r1 holds g0.p=a*r1
proof let p be Point of X, r1 be real number such that
A5: f1.p=r1;
reconsider r1 as Element of REAL by XREAL_0:def 1;
g0.p=a*r1 by A3,A5;
hence thesis;
end;
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;
assume A6:g0.p in V & V is open;
reconsider r=g0.p as Real by TOPMETR:24;
consider r0 being Real such that
A7: r0>0 & ].r-r0,r+r0.[ c= V by A6,FRECHET:8;
reconsider r1=f1.p as Real by TOPMETR:24;
A8: r=a*r1 by A3;
A9:r=a*r1 by A3;
now per cases;
case A10:a>=0;
now per cases by A10;
case A11:a>0;
set r4=r0/a;
A12:r4>0 by A7,A11,REAL_2:127;
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1
by TOPMETR:24;
A13:r1<r1+r4 by A12,REAL_1:69;
then r1-r4<r1 by REAL_1:84;
then A14:f1.p in G1 by A13,JORDAN6:45;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A15: p in W1 & W1 is open & f1.:W1 c= G1 by A1,A14,Th20;
set W=W1;
g0.:W c= ].r-r0,r+r0.[
proof let x be set;assume x in g0.:W;
then consider z being set such that
A16: z in dom g0 & z in W & g0.z=x by FUNCT_1:def 12;
reconsider pz=z as Point of X by A16;
pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then A17:f1.pz in f1.:W1 by A16,FUNCT_1:def 12;
reconsider aa1=f1.pz as Real by TOPMETR:24;
A18:x=a*aa1 by A3,A16;
reconsider rx=x as Real by A16,XREAL_0:def 1;
A19:r1-r4<aa1 & aa1<r1+r4 by A15,A17,JORDAN6:45;
a*(r1+r4) =a*r1+a*r4 by XCMPLX_1:8
.=r+r0 by A8,A11,XCMPLX_1:88;
then A20:rx<r+r0 by A11,A18,A19,REAL_1:70;
A21:a*(r1-r4)<a*aa1 by A11,A19,REAL_1:70;
a*(r1-r4) =a*r1-a*r4 by XCMPLX_1:40
.=r-r0 by A8,A11,XCMPLX_1:88;
hence x in ].r-r0,r+r0.[ by A18,A20,A21,JORDAN6:45;
end;
then g0.:W c= V by A7,XBOOLE_1:1;
hence ex W being Subset of X st p in W & W is open & g0.:W c= V by A15;
case A22:a=0;
set r4=r0;
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1
by TOPMETR:24;
A23:r1<r1+r4 by A7,REAL_1:69;
then r1-r4<r1 by REAL_1:84;
then A24:f1.p in G1 by A23,JORDAN6:45;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A25: p in W1 & W1 is open & f1.:W1 c= G1 by A1,A24,Th20;
set W=W1;
g0.:W c= ].r-r0,r+r0.[
proof let x be set;assume x in g0.:W;
then consider z being set such that
A26: z in dom g0 & z in W & g0.z=x by FUNCT_1:def 12;
reconsider pz=z as Point of X by A26;
reconsider aa1=f1.pz as Real by TOPMETR:24;
A27:x=a*aa1 by A3,A26 .=0 by A22;
r-r0<0 & 0<r+r0 by A7,A9,A22,REAL_2:105;
hence x in ].r-r0,r+r0.[ by A27,JORDAN6:45;
end;
then g0.:W c= V by A7,XBOOLE_1:1;
hence ex W being Subset of X st p in W & W is open & g0.:W c= V by A25;
end;
hence ex W being Subset of X st p in W & W is open & g0.:W c= V;
case A28:a<0;
then A29:-a>0 by REAL_1:66;
A30:-a<>0 by A28,REAL_1:66;
set r4=r0/(-a);
A31:r4>0 by A7,A29,REAL_2:127;
A32:(-a)*r4=r0 by A30,XCMPLX_1:88;
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1
by TOPMETR:24;
A33:r1<r1+r4 by A31,REAL_1:69;
then r1-r4<r1 by REAL_1:84;
then A34:f1.p in G1 by A33,JORDAN6:45;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A35: p in W1 & W1 is open & f1.:W1 c= G1 by A1,A34,Th20;
set W=W1;
g0.:W c= ].r-r0,r+r0.[
proof let x be set;assume x in g0.:W;
then consider z being set such that
A36: z in dom g0 & z in W & g0.z=x by FUNCT_1:def 12;
reconsider pz=z as Point of X by A36;
pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then A37:f1.pz in f1.:W1 by A36,FUNCT_1:def 12;
reconsider aa1=f1.pz as Real by TOPMETR:24;
A38:x=a*aa1 by A3,A36;
A39:r1-r4<aa1 & aa1<r1+r4 by A35,A37,JORDAN6:45;
then A40: (a)*aa1<(a)*(r1-r4) by A28,REAL_1:71;
A41:(a)*(r1-r4) =(a)*r1-(a)*r4 by XCMPLX_1:40
.=a*r1+-(a*r4) by XCMPLX_0:def 8
.=a*r1+(-a)*r4 by XCMPLX_1:175
.=r+r0 by A4,A32;
(a)*(r1+r4) =(a)*r1+(a)*r4 by XCMPLX_1:8
.=a*r1--(a*r4) by XCMPLX_1:151
.=a*r1-(-a)*r4 by XCMPLX_1:175
.=r-r0 by A4,A32;
then r-r0< (a)*aa1 by A28,A39,REAL_1:71;
hence x in ].r-r0,r+r0.[ by A38,A40,A41,JORDAN6:45;
end;
then g0.:W c= V by A7,XBOOLE_1:1;
hence ex W being Subset of X st p in W & W is open & g0.:W c= V by A35;
end;
hence ex W being Subset of X st p in W & W is open & g0.:W c= V;
end;
then g0 is continuous by Th20;
hence thesis by A4;
end;
theorem Th34: for X being non empty TopSpace,
f1 being map of X,R^1,a being real number st f1 is continuous
holds ex g being map of X,R^1
st (for p being Point of X,r1 being real number st
f1.p=r1 holds g.p=r1+a) & g is continuous
proof let X being non empty TopSpace,f1 be map of X,R^1,a being real number;
assume A1: f1 is continuous;
defpred P[set,set] means
(for r1 being Real st f1.$1=r1 holds $2=r1+a);
A2: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 by TOPMETR:24;
reconsider r2=a as Element of REAL by XREAL_0:def 1;
set r3 =r1+r2;
for r1 being Real st f1.x=r1 holds r3=r1+r2;
hence ex y being Element of REAL
st (for r1 being Real st f1.x=r1 holds y=r1+a);
end;
ex f being Function of the carrier of X,REAL
st for x being Element of X holds P[x,f.x]
from FuncExD(A2);
then consider f being Function of the carrier of X,REAL
such that
A3: for x being Element of X holds
(for r1 being Real st f1.x=r1 holds f.x=r1+a);
reconsider g0=f as map of X,R^1 by TOPMETR:24;
A4: for p being Point of X,r1 being real number st
f1.p=r1 holds g0.p=r1+a
proof let p be Point of X, r1 be real number such that
A5: f1.p=r1;
reconsider r1 as Element of REAL by XREAL_0:def 1;
g0.p=r1+a by A3,A5;
hence thesis;
end;
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;
assume A6:g0.p in V & V is open;
reconsider r=g0.p as Real by TOPMETR:24;
consider r0 being Real such that
A7: r0>0 & ].r-r0,r+r0.[ c= V by A6,FRECHET:8;
reconsider r1=f1.p as Real by TOPMETR:24;
set r4=r0;
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1
by TOPMETR:24;
A8:r1<r1+r4 by A7,REAL_1:69;
then r1-r4<r1 by REAL_1:84;
then A9:f1.p in G1 by A8,JORDAN6:45;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A10: p in W1 & W1 is open & f1.:W1 c= G1 by A1,A9,Th20;
set W=W1;
g0.:W c= ].r-r0,r+r0.[
proof let x be set;assume x in g0.:W;
then consider z being set such that
A11: z in dom g0 & z in W & g0.z=x by FUNCT_1:def 12;
reconsider pz=z as Point of X by A11;
pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then A12:f1.pz in f1.:W1 by A11,FUNCT_1:def 12;
reconsider aa1=f1.pz as Real by TOPMETR:24;
A13:x=aa1+a by A3,A11;
A14:r1-r4<aa1 & aa1<r1+r4 by A10,A12,JORDAN6:45;
then A15: (r1+r4)+a>aa1+a by REAL_1:67;
A16: (r1+r4)+a =a+r1+r4 by XCMPLX_1:1
.=r+r0 by A3;
A17:(r1-r4)+a<aa1+a by A14,REAL_1:67;
(r1-r4)+a =r1+a-r4 by XCMPLX_1:29
.=r-r0 by A3;
hence x in ].r-r0,r+r0.[ by A13,A15,A16,A17,JORDAN6:45;
end;
then g0.:W c= V by A7,XBOOLE_1:1;
hence ex W being Subset of X st p in W & W is open & g0.:W c= V by A10;
end;
then g0 is continuous by Th20;
hence thesis by A4;
end;
theorem Th35: for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous &
f2 is continuous holds ex g being map of X,R^1
st (for p being Point of X,r1,r2 being real number 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 map of X,R^1;
assume A1:f1 is continuous & f2 is continuous;
then consider g1 being map of X,R^1
such that A2: (for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g1.p=r1+r2) & g1 is continuous by Th29;
consider g2 being map of X,R^1
such that A3: (for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g2.p=r1-r2) & g2 is continuous by A1,Th31;
consider g3 being map of X,R^1
such that A4: (for p being Point of X,r1 being real number st
g1.p=r1 holds g3.p=r1*r1) & g3 is continuous by A2,Th32;
consider g4 being map of X,R^1
such that A5: (for p being Point of X,r1 being real number st
g2.p=r1 holds g4.p=r1*r1) & g4 is continuous by A3,Th32;
consider g5 being map of X,R^1
such that A6: (for p being Point of X,r1,r2 being real number st
g3.p=r1 & g4.p=r2 holds g5.p=r1-r2) & g5 is continuous by A4,A5,Th31;
consider g6 being map of X,R^1 such that
A7: (for p being Point of X,r1 being real number st
g5.p=r1 holds g6.p=(1/4)*r1) & g6 is continuous by A6,Th33;
for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g6.p=r1*r2
proof let p be Point of X,r1,r2 be real number;
assume A8:f1.p=r1 & f2.p=r2;
then A9:g1.p=r1+r2 by A2;
A10:g2.p=r1-r2 by A3,A8;
A11:g3.p=(r1+r2)*(r1+r2) by A4,A9 .=(r1+r2)^2 by SQUARE_1:def 3;
g4.p=(r1-r2)*(r1-r2) by A5,A10.=(r1-r2)^2 by SQUARE_1:def 3;
then g5.p= (r1+r2)^2 -(r1-r2)^2 by A6,A11;
then g6.p=(1/4)*( (r1+r2)^2 -(r1-r2)^2) by A7
.=(1/4)*( r1^2+2*r1*r2+r2^2 -(r1-r2)^2) by SQUARE_1:63
.=(1/4)*( r1^2+2*r1*r2+r2^2 -(r1^2-2*r1*r2+r2^2)) by SQUARE_1:64
.=(1/4)*( r1^2+2*r1*r2+r2^2-r2^2 -(r1^2-2*r1*r2)) by XCMPLX_1:36
.=(1/4)*( r1^2+2*r1*r2 -(r1^2-2*r1*r2)) by XCMPLX_1:26
.=(1/4)*( r1^2+2*r1*r2 -r1^2+2*r1*r2) by XCMPLX_1:37
.=(1/4)*(2*r1*r2+2*r1*r2) by XCMPLX_1:26
.=(1/4)*(2*(r1*r2)+2*r1*r2) by XCMPLX_1:4
.=(1/4)*(2*(r1*r2)+2*(r1*r2)) by XCMPLX_1:4
.=(1/4)*(2*(2*(r1*r2))) by XCMPLX_1:11
.=(1/4)*(2*2*(r1*r2)) by XCMPLX_1:4
.=(1/4)*4*(r1*r2) by XCMPLX_1:4
.= r1*r2;
hence g6.p=r1*r2;
end;
hence thesis by A7;
end;
theorem Th36: for X being non empty TopSpace,
f1 being map of X,R^1 st f1 is continuous &
(for q being Point of X holds f1.q<>0)
holds ex g being map of X,R^1
st (for p being Point of X,r1 being real number st
f1.p=r1 holds g.p=1/r1) & g is continuous
proof let X being non empty TopSpace,f1 be map of X,R^1;
assume A1: f1 is continuous &
(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);
A2: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 by TOPMETR:24;
set r3=1/r1;
for r1 being Real st f1.x=r1 holds r3=1/r1;
hence ex y being Element of REAL
st (for r1 being Real st f1.x=r1 holds y=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 FuncExD(A2);
then consider f being Function of the carrier of X,REAL
such that A3: for x being Element of X holds
(for r1 being Real st f1.x=r1 holds f.x=1/r1);
reconsider g0=f as map of X,R^1 by TOPMETR:24;
A4: for p being Point of X,r1 being real number st
f1.p=r1 holds g0.p=1/r1
proof let p be Point of X,r1 be real number such that
A5: f1.p=r1;
reconsider r1 as Element of REAL by XREAL_0:def 1;
g0.p=1/r1 by A3,A5;
hence thesis;
end;
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;
assume A6:g0.p in V & V is open;
reconsider r=g0.p as Real by TOPMETR:24;
consider r0 being Real such that
A7: r0>0 & ].r-r0,r+r0.[ c= V by A6,FRECHET:8;
reconsider r1=f1.p as Real by TOPMETR:24;
A8:r1<>0 by A1;
A9: r=1/r1 by A3;
then A10:r=r1" by XCMPLX_1:217;
now per cases;
case A11: r1>=0;
then A12:0<r by A8,A10,REAL_1:72;
A13: r+r0>=r+0 by A7,REAL_1:55;
then A14: r+r0>0 by A8,A10,A11,REAL_1:72;
A15:r+r0<r+r0+r0 by A7,REAL_1:69;
then A16:0<r+r0+r0 by A12,A13,AXIOMS:22;
r1*(1/r*r)=r1*1 by A12,XCMPLX_1:88;
then r1*r*(1/r)=r1 by XCMPLX_1:4;
then A17: 1 *(1/r)=r1 by A8,A9,XCMPLX_1:88;
set r4=r0/r/(r+r0);
A18:r0/r>0 by A7,A12,REAL_2:127;
A19: r<r+r0 by A7,REAL_1:69;
then A20:0<r+r0 by A12,AXIOMS:22;
then A21:r4>0 by A18,REAL_2:127;
A22:r1-r4=1/r-r0/(r+r0)/r by A17,XCMPLX_1:48
.=(1-r0/(r+r0))/r by XCMPLX_1:121
.=((r+r0)/(r+r0)-r0/(r+r0))/r by A12,A19,XCMPLX_1:60
.=((r+r0-r0)/(r+r0))/r by XCMPLX_1:121
.=r/(r+r0)/r by XCMPLX_1:26;
r/(r+r0)>0 by A12,A20,REAL_2:127;
then A23:r1-r4>0 by A12,A22,REAL_2:127;
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1
by TOPMETR:24;
A24:r1<r1+r4 by A21,REAL_1:69;
then r1-r4<r1 by REAL_1:84;
then A25:f1.p in G1 by A24,JORDAN6:45;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A26: p in W1 & W1 is open & f1.:W1 c= G1 by A1,A25,Th20;
set W=W1;
g0.:W c= ].r-r0,r+r0.[
proof let x be set;assume x in g0.:W;
then consider z being set such that
A27: z in dom g0 & z in W & g0.z=x by FUNCT_1:def 12;
reconsider pz=z as Point of X by A27;
pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then A28:f1.pz in f1.:W1 by A27,FUNCT_1:def 12;
reconsider aa1=f1.pz as Real by TOPMETR:24;
A29:x=1/aa1 by A3,A27;
A30:r1-r4<aa1 & aa1<r1+r4 by A26,A28,JORDAN6:45;
then 0<aa1 by A23,AXIOMS:22;
then A31:1/(1/r+r4)<1/aa1 by A17,A30,REAL_2:200;
A32:0<r0^2 by A7,SQUARE_1:74;
then 0+r0^2<r0^2+r0^2 by REAL_1:67;
then 0<r0^2+r0^2 by A32,AXIOMS:22;
then 0<r0 *r0+r0^2 by SQUARE_1:def 3;
then 0<r0 *r0+r0 *r0 by SQUARE_1:def 3;
then r0 *r< r0 *r+(r0 *r0+r0 *r0) by REAL_1:69;
then r0 *r-(r0 *r0+r0 *r0)< r0 *r by REAL_1:84;
then (r0 *r-(r0 *r0+r0 *r0))+ r*r<r*r+r0 *r by REAL_1:67;
then r*r+r0 *r-(r0 *r0+r0 *r0)<r*r+r0 *r by XCMPLX_1:29;
then r*r+r0 *r-r0 *r0-r0 *r0<r*r+r0 *r by XCMPLX_1:36;
then r*r+r0 *r-r0 *r0-r0 *r0<r*(r+r0) by XCMPLX_1:8;
then (r*r+r0 *r+r0 *r-r0 *r-r0 *r0)-r0 *r0<r*(r+r0) by XCMPLX_1:26;
then (r*r+r0 *r+r0 *r-(r0 *r+r0 *r0))-r0 *r0<r*(r+r0) by XCMPLX_1:36
;
then r*r+r0 *r+r0 *r-(r0 *r+r0 *r0+r0 *r0)<r*(r+r0) by XCMPLX_1:36;
then r*r+r0 *r+r0 *r-(r+r0+r0)*r0<r*(r+r0) by XCMPLX_1:9;
then (r+r0+r0)*r-(r+r0+r0)*r0<r*(r+r0) by XCMPLX_1:9;
then (r+r0+r0)*(r-r0)<r*(r+r0) by XCMPLX_1:40;
then (r-r0)*(r+r0+r0)/(r+r0+r0)<r*(r+r0)/(r+r0+r0)
by A16,REAL_1:73;
then r-r0<r*(r+r0)/(r+r0+r0) by A14,A15,XCMPLX_1:90;
then r-r0<r/((r+r0+r0)/(r+r0)) by XCMPLX_1:78;
then r-r0<r/((r+r0)/(r+r0)+r0/(r+r0)) by XCMPLX_1:63;
then r-r0<r*1/(1+r0/(r+r0)) by A12,A19,XCMPLX_1:60;
then r-r0<1/((1+r0/(r+r0))/r) by XCMPLX_1:78;
then r-r0<1/(1/r+r0/(r+r0)/r) by XCMPLX_1:63;
then r-r0<1/(1/r+r0/r/(r+r0)) by XCMPLX_1:48;
then A33: r-r0<1/aa1 by A31,AXIOMS:22;
A34: 1/aa1<1/(r1-r4) by A23,A30,REAL_2:151;
1/(r1-r4) =1/(r1-r0 *r"/(r+r0)) by XCMPLX_0:def 9
.=1/(r1-r0 *(1/r)/(r+r0)) by XCMPLX_1:217
.=1/(r1-r0/((r+r0)/r1)) by A17,XCMPLX_1:78
.=1/(r1*1-r1*(r0/(r+r0))) by XCMPLX_1:82
.=1/((1-(r0/(r+r0)))*r1) by XCMPLX_1:40
.=1/(((r+r0)/(r+r0)-(r0/(r+r0)))*r1) by A12,A13,XCMPLX_1:60
.=1/((r+r0-r0)/(r+r0)*r1) by XCMPLX_1:121
.=1/(r/(r+r0)*r1) by XCMPLX_1:26
.=1/(r/((r+r0)/r1)) by XCMPLX_1:82
.=1/(r*r1/(r+r0)) by XCMPLX_1:78
.=(r+r0)/(r*r1)*1 by XCMPLX_1:81
.=(r+r0)/1 by A8,A10,XCMPLX_0:def 7
.=r+r0;
hence x in ].r-r0,r+r0.[ by A29,A33,A34,JORDAN6:45;
end;
then g0.:W c= V by A7,XBOOLE_1:1;
hence ex W being Subset of X st p in W & W is open & g0.:W c= V by A26;
case r1<0;
then A35: r1"<0 by REAL_2:149;
then A36:0<-r by A10,REAL_1:66;
A37: -r+r0>=-r+0 by A7,REAL_1:55;
then A38: -r+r0>0 by A10,A35,REAL_1:66;
A39: -r+r0<-r+r0+r0 by A7,REAL_1:69;
then A40:0<-r+r0+r0 by A36,A37,AXIOMS:22;
r1*((-r)*(1/(-r)))=r1*1 by A36,XCMPLX_1:88;
then r1*(-r)*(1/(-r))=r1 by XCMPLX_1:4;
then (-(r*r1))*(1/(-r))=r1 by XCMPLX_1:175;
then (-1)*(1/(-r))=r1 by A8,A9,XCMPLX_1:88;
then A41: -(1 *(1/(-r)))=r1 by XCMPLX_1:175;
then A42: -r1=1/(-r);
set r4=r0/(-r)/(-r+r0);
A43:r0/(-r)>0 by A7,A36,REAL_2:127;
A44: -r<-r+r0 by A7,REAL_1:69;
then A45:0<-r+r0 by A36,AXIOMS:22;
then A46:r4>0 by A43,REAL_2:127;
A47:r1+r4=-(1/(-r))+r0/(-r+r0)/(-r) by A41,XCMPLX_1:48
.=(-1)/(-r)+r0/(-r+r0)/(-r) by XCMPLX_1:188
.=(-1+r0/(-r+r0))/(-r) by XCMPLX_1:63
.=(-((-r+r0)/(-r+r0))+r0/(-r+r0))/(-r) by A36,A44,XCMPLX_1:60
.=((-(-r+r0))/(-r+r0)+r0/(-r+r0))/(-r) by XCMPLX_1:188
.=((-(-r+r0)+r0)/(-r+r0))/(-r) by XCMPLX_1:63
.=((r-r0+r0)/(-r+r0))/(-r) by XCMPLX_1:163
.=((r+r0-r0)/(-r+r0))/(-r) by XCMPLX_1:29
.=r/(-r+r0)/(-r) by XCMPLX_1:26;
(-r)/(-r+r0)>0 by A36,A45,REAL_2:127;
then -(r/(-r+r0))>0 by XCMPLX_1:188;
then (r/(-r+r0))<0 by REAL_1:66;
then A48: (r1+r4)<0 by A36,A47,REAL_2:128;
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1
by TOPMETR:24;
A49:r1<r1+r4 by A46,REAL_1:69;
then r1-r4<r1 by REAL_1:84;
then A50:f1.p in G1 by A49,JORDAN6:45;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A51: p in W1 & W1 is open & f1.:W1 c= G1 by A1,A50,Th20;
set W=W1;
g0.:W c= ].r-r0,r+r0.[
proof let x be set;assume x in g0.:W;
then consider z being set such that
A52: z in dom g0 & z in W & g0.z=x by FUNCT_1:def 12;
reconsider pz=z as Point of X by A52;
pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then A53:f1.pz in f1.:W1 by A52,FUNCT_1:def 12;
reconsider aa1=f1.pz as Real by TOPMETR:24;
A54:x=1/aa1 by A3,A52;
A55:r1-r4<aa1 & aa1<r1+r4 by A51,A53,JORDAN6:45;
then 0>aa1 by A48,AXIOMS:22;
then A56:1/(-(1/(-r))-r4)>1/aa1 by A41,A55,REAL_2:200;
A57:0<r0^2 by A7,SQUARE_1:74;
then 0+r0^2<r0^2+r0^2 by REAL_1:67;
then 0<r0^2+r0^2 by A57,AXIOMS:22;
then 0<r0 *r0+r0^2 by SQUARE_1:def 3;
then 0<r0 *r0+r0 *r0 by SQUARE_1:def 3;
then r0 *(-r)< r0 *(-r)+(r0 *r0+r0 *r0) by REAL_1:69;
then r0 *(-r)-(r0 *r0+r0 *r0)< r0 *(-r) by REAL_1:84;
then (r0 *(-r)-(r0 *r0+r0 *r0))+ (-r)*(-r)<r0 *(-r)+(-r)*(-r)
by REAL_1:67;
then (-r)*(-r)+r0 *(-r)-(r0 *r0+r0 *r0)<(-r)*(-r)+r0 *(-r)
by XCMPLX_1:29;
then (-r)*(-r)+r0 *(-r)-r0 *r0-r0 *r0<(-r)*(-r)+r0 *(-r) by XCMPLX_1:
36;
then (-r)*(-r)+r0 *(-r)-r0 *r0-r0 *r0<(-r)*((-r)+r0) by XCMPLX_1:8;
then ((-r)*(-r)+r0 *(-r)+r0 *(-r)-r0 *(-r)-r0 *r0)-r0 *r0<(-r)*((-r)
+r0)
by XCMPLX_1:26;
then ((-r)*(-r)+r0 *(-r)+r0 *(-r)-(r0 *(-r)+r0 *r0))-r0 *r0<(-r)*((-
r)+r0)
by XCMPLX_1:36;
then (-r)*(-r)+r0 *(-r)+r0 *(-r)-(r0 *(-r)+r0 *r0+r0 *r0)<(-r)*((-r)
+r0)
by XCMPLX_1:36;
then (-r)*(-r)+r0 *(-r)+r0 *(-r)-((-r)+r0+r0)*r0<(-r)*((-r)+r0)
by XCMPLX_1:9;
then ((-r)+r0+r0)*(-r)-((-r)+r0+r0)*r0<(-r)*((-r)+r0) by XCMPLX_1:9;
then ((-r)+r0+r0)*((-r)-r0)<(-r)*((-r)+r0) by XCMPLX_1:40;
then ((-r)-r0)*((-r)+r0+r0)/((-r)+r0+r0)<(-r)*((-r)+r0)/((-r)+r0+r0)
by A40,REAL_1:73;
then (-r)-r0<(-r)*((-r)+r0)/((-r)+r0+r0) by A38,A39,XCMPLX_1:90;
then (-r)-r0<(-r)/(((-r)+r0+r0)/((-r)+r0)) by XCMPLX_1:78;
then (-r)-r0<(-r)/(((-r)+r0)/((-r)+r0)+r0/((-r)+r0)) by XCMPLX_1:63;
then (-r)-r0<(-r)*1/(1+r0/((-r)+r0)) by A36,A44,XCMPLX_1:60;
then (-r)-r0<1/((1+r0/((-r)+r0))/(-r)) by XCMPLX_1:78;
then (-r)-r0<1/(1/(-r)+r0/((-r)+r0)/(-r)) by XCMPLX_1:63;
then (-r)-r0<1/(1/(-r)+r0/(-r)/((-r)+r0)) by XCMPLX_1:48;
then -(r+r0)<1/(1/(-r)+r4) by XCMPLX_1:161;
then (r+r0)>-(1/(1/(-r)+r4)) by REAL_2:109;
then (r+r0)>(1/-(1/(-r)+r4)) by XCMPLX_1:189;
then r+r0>1/(-(1/(-r))-r4) by XCMPLX_1:161;
then A58: r+r0>1/aa1 by A56,AXIOMS:22;
A59: 1/aa1>1/(r1+r4) by A48,A55,REAL_2:151;
1/(r1+r4) =1/(r1+r0 *(-r)"/(-r+r0)) by XCMPLX_0:def 9
.=1/(r1+r0 *(1/(-r))/(-r+r0)) by XCMPLX_1:217
.=1/(r1+(-(r1*r0))/(-r+r0)) by A42,XCMPLX_1:175
.=1/(r1+-((r1*r0)/(-r+r0))) by XCMPLX_1:188
.=1/(r1-((r1*r0))/(-r+r0)) by XCMPLX_0:def 8
.=1/(r1-r0/((-r+r0)/r1)) by XCMPLX_1:78
.=1/(r1*1-r1*(r0/(-r+r0))) by XCMPLX_1:82
.=1/(r1*(1-r0/(-r+r0))) by XCMPLX_1:40
.=1/(((-r+r0)/(-r+r0)-(r0/(-r+r0)))*r1) by A36,A37,XCMPLX_1:
60
.=1/((-r+r0-r0)/(-r+r0)*(r1)) by XCMPLX_1:121
.=1/((-r+r0-r0)/(-(r-r0))*(r1)) by XCMPLX_1:162
.=1/((-(-r+r0-r0)/(r-r0))*(r1)) by XCMPLX_1:189
.=1/((-r+r0-r0)/((r-r0))*(-r1)) by XCMPLX_1:176
.=1/((-r)/((r-r0))*(-r1)) by XCMPLX_1:26
.=1/((-r)/((r-r0)/(-r1))) by XCMPLX_1:82
.=1/((-r)*(-r1)/(r-r0)) by XCMPLX_1:78
.=(r-r0)/((-r)*(-r1))*1 by XCMPLX_1:81
.=(r-r0)/((-r)*(-r)") by A41,XCMPLX_1:217
.=(r-r0)/1 by A36,XCMPLX_0:def 7
.=r-r0;
hence x in ].r-r0,r+r0.[ by A54,A58,A59,JORDAN6:45;
end;
then g0.:W c= V by A7,XBOOLE_1:1;
hence ex W being Subset of X st p in W & W is open & g0.:W c= V by A51;
end;
hence ex W being Subset of X st p in W & W is open & g0.:W c= V;
end;
then g0 is continuous by Th20;
hence thesis by A4;
end;
theorem Th37: for X being non empty TopSpace,
f1,f2 being map 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 map of X,R^1
st (for p being Point of X,r1,r2 being real number 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 map of X,R^1;
assume A1:f1 is continuous & f2 is continuous
& (for q being Point of X holds f2.q<>0);
then consider g1 being map of X,R^1
such that A2: (for p being Point of X,r2 being real number st
f2.p=r2 holds g1.p=1/r2) & g1 is continuous by Th36;
consider g2 being map of X,R^1
such that A3: (for p being Point of X,r1,r2 being real number st
f1.p=r1 & g1.p=r2 holds g2.p=r1*r2) & g2 is continuous by A1,A2,Th35;
for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g2.p=r1/r2
proof let p be Point of X,r1,r2 be real number;
assume A4:f1.p=r1 & f2.p=r2;
then g1.p=1/r2 by A2;
then g2.p=r1*(1/r2) by A3,A4 .=r1/r2 by XCMPLX_1:100;
hence g2.p=r1/r2;
end;
hence thesis by A3;
end;
theorem Th38: for X being non empty TopSpace,
f1,f2 being map 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 map of X,R^1
st (for p being Point of X,r1,r2 being real number 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 map of X,R^1;
assume A1:f1 is continuous & f2 is continuous
& (for q being Point of X holds f2.q<>0);
then consider g2 being map of X,R^1
such that A2: (for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g2.p=r1/r2) & g2 is continuous by Th37;
consider g3 being map of X,R^1
such that A3: (for p being Point of X,r1,r2 being real number st
g2.p=r1 & f2.p=r2 holds g3.p=r1/r2) & g3 is continuous by A1,A2,Th37;
for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g3.p=r1/r2/r2
proof let p be Point of X,r1,r2 be real number;
assume A4:f1.p=r1 & f2.p=r2;
then g2.p=r1/r2 by A2;
hence g3.p=r1/r2/r2 by A3,A4;
end;
hence thesis by A3;
end;
theorem Th39: for K0 being Subset of TOP-REAL 2,
f being map 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 let K0 be Subset of TOP-REAL 2,
f be map of (TOP-REAL 2)|K0,R^1;
assume A1: (for p being Point of (TOP-REAL 2)|K0 holds f.p=proj1.p);
A2:dom f= the carrier of (TOP-REAL 2)|K0 by FUNCT_2:def 1;
A3: the carrier of (TOP-REAL 2)|K0
=[#]((TOP-REAL 2)|K0) by PRE_TOPC:12
.=K0 by PRE_TOPC:def 10;
A4:(the carrier of TOP-REAL 2)/\K0=K0 by XBOOLE_1:28;
A5:for x being set st x in dom f holds f.x=proj1.x by A1;
reconsider g=proj1 as map of TOP-REAL 2,R^1 by TOPMETR:24;
A6:f=g|K0 by A2,A3,A4,A5,Th14,FUNCT_1:68;
g is continuous by TOPREAL6:83;
hence f is continuous by A6,TOPMETR:10;
end;
theorem Th40: for K0 being Subset of TOP-REAL 2,
f being map 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 map of (TOP-REAL 2)|K0,R^1;
assume A1: (for p being Point of (TOP-REAL 2)|K0 holds f.p=proj2.p);
A2:dom f= the carrier of (TOP-REAL 2)|K0 by FUNCT_2:def 1;
A3: the carrier of (TOP-REAL 2)|K0
=[#]((TOP-REAL 2)|K0) by PRE_TOPC:12
.=K0 by PRE_TOPC:def 10;
A4:(the carrier of TOP-REAL 2) /\ K0=K0 by XBOOLE_1:28;
for x being set st x in dom f holds f.x=proj2.x by A1;
then A5:f=proj2|K0 by A2,A3,A4,Th15,FUNCT_1:68;
reconsider g=proj2 as map of TOP-REAL 2,R^1 by TOPMETR:24;
g is continuous by TOPREAL6:83;
hence f is continuous by A5,TOPMETR:10;
end;
theorem Th41: for K1 being non empty Subset of TOP-REAL 2,
f being map 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 map of (TOP-REAL 2)|K1,R^1;
assume
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) & (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`1<>0 );
A2: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) by PRE_TOPC:12
.=K1 by PRE_TOPC:def 10;
proj1|K1 is Function of K1,the carrier of R^1
by FUNCT_2:38,TOPMETR:24;
then reconsider g1=proj1|K1 as map of (TOP-REAL 2)|K1,R^1 by A2;
A3:for q being Point of (TOP-REAL 2)|K1 holds g1.q=proj1.q
proof let q be Point of (TOP-REAL 2)|K1;
A4: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 A2,A4,XBOOLE_0:def 3;
hence g1.q=proj1.q by FUNCT_1:71;
end;
then A5:g1 is continuous by Th39;
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 A2;
g1.q=proj1.q by A3 .=q2`1 by PSCOMP_1:def 28;
hence g1.q<>0 by A1;
end;
then consider g3 being map of (TOP-REAL 2)|K1,R^1 such that
A6: (for q being Point of
(TOP-REAL 2)|K1,r2 being real number st g1.q=r2
holds g3.q=1/r2) & g3 is continuous by A5,Th36;
dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then A7:dom f=dom g3 by FUNCT_2:def 1;
for x being set st x in dom f holds f.x=g3.x
proof let x be set;assume A8:x in dom f;
then x in the carrier of (TOP-REAL 2)|K1;
then x in [#]((TOP-REAL 2)|K1) by PRE_TOPC:12;
then x in K1 by PRE_TOPC:def 10;
then reconsider r=x as Point of (TOP-REAL 2);
reconsider s=x as Point of (TOP-REAL 2)|K1 by A8;
A9:f.r=1/r`1 by A1,A8;
A10:g1.s=proj1.s by A3;
proj1.r=r`1 by PSCOMP_1:def 28;
hence f.x=g3.x by A6,A9,A10;
end;
hence f is continuous by A6,A7,FUNCT_1:9;
end;
theorem Th42: for K1 being non empty Subset of TOP-REAL 2,
f being map 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 map of (TOP-REAL 2)|K1,R^1;
assume
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) & (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`2<>0 );
A2: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) by PRE_TOPC:12
.=K1 by PRE_TOPC:def 10;
proj2|K1 is Function of K1,the carrier of R^1
by FUNCT_2:38,TOPMETR:24;
then reconsider g1=proj2|K1 as map of (TOP-REAL 2)|K1,R^1 by A2;
A3:for q being Point of (TOP-REAL 2)|K1 holds g1.q=proj2.q
proof let q be Point of (TOP-REAL 2)|K1;
A4: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 A2,A4,XBOOLE_0:def 3;
hence g1.q=proj2.q by FUNCT_1:71;
end;
then A5:g1 is continuous by Th40;
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 A2;
g1.q=proj2.q by A3 .=q2`2 by PSCOMP_1:def 29;
hence g1.q<>0 by A1;
end;
then consider g3 being map of (TOP-REAL 2)|K1,R^1 such that
A6: (for q being Point of
(TOP-REAL 2)|K1,r2 being real number st g1.q=r2
holds g3.q=1/r2) & g3 is continuous by A5,Th36;
dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then A7:dom f=dom g3 by FUNCT_2:def 1;
for x being set st x in dom f holds f.x=g3.x
proof let x be set;assume
A8:x in dom f;
then x in the carrier of (TOP-REAL 2)|K1;
then x in [#]((TOP-REAL 2)|K1) by PRE_TOPC:12;
then x in K1 by PRE_TOPC:def 10;
then reconsider r=x as Point of (TOP-REAL 2);
reconsider s=x as Point of (TOP-REAL 2)|K1 by A8;
A9:f.r=1/r`2 by A1,A8;
A10:g1.s=proj2.s by A3;
proj2.r=r`2 by PSCOMP_1:def 29;
hence f.x=g3.x by A6,A9,A10;
end;
hence f is continuous by A6,A7,FUNCT_1:9;
end;
theorem Th43: for K1 being non empty Subset of TOP-REAL 2,
f being map 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 map of (TOP-REAL 2)|K1,R^1;
assume
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) & (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`1<>0 );
A2: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) by PRE_TOPC:12
.=K1 by PRE_TOPC:def 10;
proj2|K1 is Function of K1,the carrier of R^1 by FUNCT_2:38,TOPMETR:24;
then reconsider g2=proj2|K1 as map of (TOP-REAL 2)|K1,R^1 by A2;
A3:for q being Point of (TOP-REAL 2)|K1 holds g2.q=proj2.q
proof let q be Point of (TOP-REAL 2)|K1;
A4: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 A2,A4,XBOOLE_0:def 3;
hence g2.q=proj2.q by FUNCT_1:71;
end;
then A5:g2 is continuous by Th40;
proj1|K1 is Function of K1,the carrier of R^1 by FUNCT_2:38,TOPMETR:24;
then reconsider g1=proj1|K1 as map of (TOP-REAL 2)|K1,R^1 by A2;
A6:for q being Point of (TOP-REAL 2)|K1 holds g1.q=proj1.q
proof let q be Point of (TOP-REAL 2)|K1;
A7: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 A2,A7,XBOOLE_0:def 3;
hence g1.q=proj1.q by FUNCT_1:71;
end;
then A8:g1 is continuous by Th39;
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 A2;
g1.q=proj1.q by A6 .=q2`1 by PSCOMP_1:def 28;
hence g1.q<>0 by A1;
end;
then consider g3 being map of (TOP-REAL 2)|K1,R^1 such that
A9: (for q being Point of
(TOP-REAL 2)|K1,r1,r2 being real number st g2.q=r1 & g1.q=r2
holds g3.q=r1/r2/r2) & g3 is continuous by A5,A8,Th38;
dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then A10:dom f=dom g3 by FUNCT_2:def 1;
for x being set st x in dom f holds f.x=g3.x
proof let x be set;assume
A11:x in dom f;
then x in the carrier of (TOP-REAL 2)|K1;
then x in [#]((TOP-REAL 2)|K1) by PRE_TOPC:12;
then x in K1 by PRE_TOPC:def 10;
then reconsider r=x as Point of (TOP-REAL 2);
reconsider s=x as Point of (TOP-REAL 2)|K1 by A11;
A12:f.r=r`2/r`1/r`1 by A1,A11;
A13:g2.s=proj2.s by A3;
A14:g1.s=proj1.s by A6;
A15:proj2.r=r`2 by PSCOMP_1:def 29;
proj1.r=r`1 by PSCOMP_1:def 28;
hence f.x=g3.x by A9,A12,A13,A14,A15;
end;
hence f is continuous by A9,A10,FUNCT_1:9;
end;
theorem Th44: for K1 being non empty Subset of TOP-REAL 2,
f being map 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 map of (TOP-REAL 2)|K1,R^1;
assume
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) & (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`2<>0 );
A2: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) by PRE_TOPC:12
.=K1 by PRE_TOPC:def 10;
proj1|K1 is Function of K1,the carrier of R^1 by FUNCT_2:38,TOPMETR:24;
then reconsider g2=proj1|K1 as map of (TOP-REAL 2)|K1,R^1 by A2;
A3:for q being Point of (TOP-REAL 2)|K1 holds g2.q=proj1.q
proof let q be Point of (TOP-REAL 2)|K1;
A4: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 A2,A4,XBOOLE_0:def 3;
hence g2.q=proj1.q by FUNCT_1:71;
end;
then A5:g2 is continuous by Th39;
proj2|K1 is Function of K1,the carrier of R^1 by FUNCT_2:38,TOPMETR:24;
then reconsider g1=proj2|K1 as map of (TOP-REAL 2)|K1,R^1 by A2;
A6:for q being Point of (TOP-REAL 2)|K1 holds g1.q=proj2.q
proof let q be Point of (TOP-REAL 2)|K1;
A7: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 A2,A7,XBOOLE_0:def 3;
hence g1.q=proj2.q by FUNCT_1:71;
end;
then A8:g1 is continuous by Th40;
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 A2;
g1.q=proj2.q by A6 .=q2`2 by PSCOMP_1:def 29;
hence g1.q<>0 by A1;
end;
then consider g3 being map of (TOP-REAL 2)|K1,R^1 such that
A9: (for q being Point of
(TOP-REAL 2)|K1,r1,r2 being real number st g2.q=r1 & g1.q=r2
holds g3.q=r1/r2/r2) & g3 is continuous by A5,A8,Th38;
dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then A10:dom f=dom g3 by FUNCT_2:def 1;
for x being set st x in dom f holds f.x=g3.x
proof let x be set;assume
A11:x in dom f;
then x in the carrier of (TOP-REAL 2)|K1;
then x in [#]((TOP-REAL 2)|K1) by PRE_TOPC:12;
then x in K1 by PRE_TOPC:def 10;
then reconsider r=x as Point of (TOP-REAL 2);
reconsider s=x as Point of (TOP-REAL 2)|K1 by A11;
A12:f.r=r`1/r`2/r`2 by A1,A11;
A13:g2.s=proj1.s by A3;
A14:g1.s=proj2.s by A6;
A15:proj1.r=r`1 by PSCOMP_1:def 28;
proj2.r=r`2 by PSCOMP_1:def 29;
hence f.x=g3.x by A9,A12,A13,A14,A15;
end;
hence f is continuous by A9,A10,FUNCT_1:9;
end;
theorem Th45: for K0,B0 being Subset of TOP-REAL 2, f being map of
(TOP-REAL 2)|K0,(TOP-REAL 2)|B0,
f1,f2 being map of (TOP-REAL 2)|K0,R^1 st f1 is continuous &
f2 is continuous & K0<>{} & B0<>{} &
(for x,y,r,s being real number 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 map of
(TOP-REAL 2)|K0,(TOP-REAL 2)|B0,
f1,f2 be map of (TOP-REAL 2)|K0,R^1;
assume A1:f1 is continuous &
f2 is continuous & K0<>{} & B0<>{} &
(for x,y,r,s being real number st |[x,y]| in K0 &
r=f1.(|[x,y]|) & s=f2.(|[x,y]|) holds
f. |[x,y]|=|[r,s]|);
then reconsider K1=K0 as non empty Subset of TOP-REAL 2;
reconsider B1=B0 as non empty Subset of TOP-REAL 2 by A1;
reconsider X=(TOP-REAL 2)|K1,Y=(TOP-REAL 2)|B1 as non empty TopSpace;
reconsider f0=f as map 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 A2: f0.r in V & V is open;
then consider V2 being Subset of TOP-REAL 2 such that
A3: V2 is open & V=V2 /\ [#]Y by TOPS_2:32;
A4:V2 /\ [#]Y c= V2 by XBOOLE_1:17;
then f0.r in V2 by A2,A3;
then reconsider p=f0.r as Point of TOP-REAL 2;
consider r2 being real number such that
A5: r2>0 & {q where q is Point of TOP-REAL 2:
p`1-r2<q`1 & q`1<p`1+r2 & p`2-r2<q`2 & q`2<p`2+r2} c= V2 by A2,A3,A4,Th21;
A6:r in the carrier of X;
then A7:r in dom f1 by FUNCT_2:def 1;
A8:r in dom f2 by A6,FUNCT_2:def 1;
A9:f1.r in rng f1 by A7,FUNCT_1:12;
f2.r in rng f2 by A8,FUNCT_1:12;
then reconsider r3=f1.r,r4=f2.r as Real by A9,TOPMETR:24;
A10:the carrier of X=[#]X by PRE_TOPC:12 .=K0 by PRE_TOPC:def 10;
then r in K0;
then reconsider pr=r as Point of TOP-REAL 2;
A11:r= |[pr`1,pr`2]| by EUCLID:57;
then A12:f0. |[pr`1,pr`2]|=|[r3,r4]| by A1,A10;
p`1 <p`1+r2 by A5,REAL_1:69;
then p`1-r2< p`1 & p`1<p`1+r2 by REAL_1:84;
then A13: p`1 in ].p`1-r2,p`1+r2.[ by JORDAN6:45;
then A14: f1.r in ].p`1-r2,p`1+r2.[ by A11,A12,EUCLID:56;
p`2 <p`2+r2 by A5,REAL_1:69;
then p`2-r2< p`2 & p`2<p`2+r2 by REAL_1:84;
then A15:p`2 in ].p`2-r2,p`2+r2.[ by JORDAN6:45;
reconsider G1= ].p`1-r2,p`1+r2.[,G2= ].p`2-r2,p`2+r2.[ as
Subset of R^1 by TOPMETR:24;
A16:G1 is open & G2 is open by JORDAN6:46;
A17:f1.r in G1 & f2.r in G2 by A11,A12,A13,A15,EUCLID:56;
consider W1 being Subset of X such that
A18: r in W1 & W1 is open & f1.:W1 c= G1 by A1,A14,A16,Th20;
consider W2 being Subset of X such that
A19: r in W2 & W2 is open & f2.:W2 c= G2 by A1,A16,A17,Th20;
reconsider W5=W1 /\ W2 as Subset of X;
A20:W5 is open by A18,A19,TOPS_1:38;
A21:r in W5 by A18,A19,XBOOLE_0:def 3;
W5 c= W1 by XBOOLE_1:17;
then f1.:W5 c= f1.:W1 by RELAT_1:156;
then A22:f1.:W5 c= G1 by A18,XBOOLE_1:1;
W5 c= W2 by XBOOLE_1:17;
then f2.:W5 c= f2.:W2 by RELAT_1:156;
then A23:f2.:W5 c= G2 by A19,XBOOLE_1:1;
f0.:W5 c= V
proof let v be set;assume A24:v in f0.:W5;
then reconsider q2=v as Point of Y;
consider k being set such that
A25: k in dom f0 & k in W5 & q2=f0.k by A24,FUNCT_1:def 12;
q2 in the carrier of Y;
then A26:q2 in [#]Y by PRE_TOPC:12;
the carrier of X=[#]X by PRE_TOPC:12 .=K0 by PRE_TOPC:def 10;
then k in K0 by A25;
then reconsider r8=k as Point of TOP-REAL 2;
A27:dom f0=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1
.=[#]((TOP-REAL 2)|K1) by PRE_TOPC:12 .=K0 by PRE_TOPC:def 10;
A28:k= |[r8`1,r8`2]| by EUCLID:57;
A29: |[r8`1,r8`2]| in K0 by A25,A27,EUCLID:57;
A30:dom f1=the carrier of (TOP-REAL 2)|K0 by FUNCT_2:def 1
.=[#]((TOP-REAL 2)|K0) by PRE_TOPC:12 .=K0 by PRE_TOPC:def 10;
A31:dom f2=the carrier of (TOP-REAL 2)|K0 by FUNCT_2:def 1
.=[#]((TOP-REAL 2)|K0) by PRE_TOPC:12 .=K0 by PRE_TOPC:def 10;
A32:f1.(|[r8`1,r8`2]|) in rng f1 by A29,A30,FUNCT_1:def 5;
f2.(|[r8`1,r8`2]|) in rng f2 by A29,A31,FUNCT_1:def 5;
then reconsider r7=f1.(|[r8`1,r8`2]|), s7=f2.(|[r8`1,r8`2]|) as Real
by A32,TOPMETR:24;
A33:v=|[r7,s7]| by A1,A25,A27,A28;
A34:(|[r7,s7]|)`1 =r7 by EUCLID:56;
A35:(|[r7,s7]|)`2 =s7 by EUCLID:56;
A36: |[r8`1,r8`2]| in W5 by A25,EUCLID:57;
then A37: f1.(|[r8`1,r8`2]|) in f1.:W5 by A29,A30,FUNCT_1:def 12;
f2.(|[r8`1,r8`2]|) in f2.:W5 by A29,A31,A36,FUNCT_1:def 12;
then p`1-r2< r7 & r7<p`1+r2 &
p`2-r2< s7 & s7<p`2+r2 by A22,A23,A37,JORDAN6:45;
then v in {q3 where q3 is Point of TOP-REAL 2:
p`1-r2<q3`1 & q3`1<p`1+r2 & p`2-r2<q3`2 & q3`2<p`2+r2} by A33,A34,A35;
hence v in V by A3,A5,A26,XBOOLE_0:def 3;
end;
hence ex W being Subset of X st r in W & W is open & f0.:W c= V by A20,A21;
end;
hence f is continuous by Th20;
end;
theorem Th46: for K0,B0 being Subset of TOP-REAL 2,f being
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0
st f=Out_In_Sq|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} &
K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2}
holds f is continuous
proof let K0,B0 be Subset of TOP-REAL 2,f be
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0;
assume A1:f=Out_In_Sq|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} &
K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.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) &
(1.REAL 2)<>0.REAL 2
by Th13,REVROT_1:19;
then A2:1.REAL 2 in K0 by A1;
then reconsider K1=K0 as non empty Subset of TOP-REAL 2;
A3: K0 c= B0
proof let x be set;assume x in K0;
then consider p8 being Point of TOP-REAL 2 such that
A4: x=p8 & (
(p8`2<=p8`1 & -p8`1<=p8`2 or p8`2>=p8`1 & p8`2<=-p8`1) & p8<>0.REAL 2)
by A1;
not x in {0.REAL 2} by A4,TARSKI:def 1;
hence x in B0 by A1,A4,XBOOLE_0:def 4;
end;
A5:dom ((proj2)*(Out_In_Sq|K1)) c= dom (Out_In_Sq|K1) by RELAT_1:44;
A6:dom (Out_In_Sq|K1) c= dom ((proj2)*(Out_In_Sq|K1))
proof let x be set;assume A7:x in dom (Out_In_Sq|K1);
then A8:x in dom Out_In_Sq /\ K1 by FUNCT_1:68;
A9:(Out_In_Sq|K1).x=Out_In_Sq.x by A7,FUNCT_1:68;
A10: dom proj2 = (the carrier of TOP-REAL 2) by FUNCT_2:def 1;
x in dom Out_In_Sq by A8,XBOOLE_0:def 3;
then Out_In_Sq.x in rng Out_In_Sq by FUNCT_1:12;
then Out_In_Sq.x in the carrier of TOP-REAL 2 by XBOOLE_0:def 4;
hence x in dom ((proj2)*(Out_In_Sq|K1)) by A7,A9,A10,FUNCT_1:21;
end;
A11:K1 c= (the carrier of TOP-REAL 2)\{0.REAL 2}
proof let z be set;assume z in K1;
then consider p8 being Point of TOP-REAL 2 such that
A12: p8=z &(
(p8`2<=p8`1 & -p8`1<=p8`2 or p8`2>=p8`1 & p8`2<=-p8`1)
& p8<>0.REAL 2) by A1;
z in (the carrier of TOP-REAL 2) & not z in {0.REAL 2}
by A12,TARSKI:def 1;
hence thesis by XBOOLE_0:def 4;
end;
A13: (the carrier of TOP-REAL 2)\{0.REAL 2}<>{} by Th19;
A14:dom ((proj2)*(Out_In_Sq|K1))
=dom (Out_In_Sq|K1) by A5,A6,XBOOLE_0:def 10
.=dom Out_In_Sq /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2)\{0.REAL 2})/\ K1 by A13,FUNCT_2:def 1
.=K1 by A11,XBOOLE_1:28
.=[#]((TOP-REAL 2)|K1) by PRE_TOPC:def 10
.=the carrier of (TOP-REAL 2)|K1
by PRE_TOPC:12;
rng ((proj2)*(Out_In_Sq|K1)) c= rng (proj2) by RELAT_1:45;
then rng ((proj2)*(Out_In_Sq|K1)) c= the carrier of R^1 by TOPMETR:24,XBOOLE_1:
1;
then (proj2)*(Out_In_Sq|K1) is Function of the carrier of (TOP-REAL 2)|K1,
the carrier of R^1 by A14,FUNCT_2:4;
then reconsider g2=(proj2)*(Out_In_Sq|K1) as map of (TOP-REAL 2)|K1,R^1;
A15:dom ((proj1)*(Out_In_Sq|K1)) c= dom (Out_In_Sq|K1) by RELAT_1:44;
dom (Out_In_Sq|K1) c= dom ((proj1)*(Out_In_Sq|K1))
proof let x be set;assume A16:x in dom (Out_In_Sq|K1);
then A17:x in dom Out_In_Sq /\ K1 by FUNCT_1:68;
A18:(Out_In_Sq|K1).x=Out_In_Sq.x by A16,FUNCT_1:68;
A19: dom proj1 = (the carrier of TOP-REAL 2) by FUNCT_2:def 1;
x in dom Out_In_Sq by A17,XBOOLE_0:def 3;
then Out_In_Sq.x in rng Out_In_Sq by FUNCT_1:12;
then Out_In_Sq.x in the carrier of TOP-REAL 2 by XBOOLE_0:def 4;
hence x in dom ((proj1)*(Out_In_Sq|K1)) by A16,A18,A19,FUNCT_1:21;
end;
then A20:dom ((proj1)*(Out_In_Sq|K1))
=dom (Out_In_Sq|K1) by A15,XBOOLE_0:def 10
.=dom Out_In_Sq /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2)\{0.REAL 2})/\ K1 by A13,FUNCT_2:def 1
.=K1 by A11,XBOOLE_1:28
.=[#]((TOP-REAL 2)|K1) by PRE_TOPC:def 10
.=the carrier of (TOP-REAL 2)|K1 by PRE_TOPC:12;
rng ((proj1)*(Out_In_Sq|K1)) c= rng (proj1) by RELAT_1:45;
then rng ((proj1)*(Out_In_Sq|K1)) c= the carrier of R^1 by TOPMETR:24,XBOOLE_1:
1;
then (proj1)*(Out_In_Sq|K1) is Function of the carrier of (TOP-REAL 2)|K1,
the carrier of R^1 by A20,FUNCT_2:4;
then reconsider g1=(proj1)*(Out_In_Sq|K1) as map of (TOP-REAL 2)|K1,R^1;
A21: 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;
assume A22:q in the carrier of (TOP-REAL 2)|K1;
the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) by PRE_TOPC:12
.=K1 by PRE_TOPC:def 10;
then consider p3 being Point of TOP-REAL 2 such that
A23: q=p3 & ((p3`2<=p3`1 & -p3`1<=p3`2 or p3`2>=p3`1 & p3`2<=-p3`1)
& p3<>0.REAL 2) by A1,A22;
now assume A24:q`1=0;
then q`2=0 by A23;
hence contradiction by A23,A24,EUCLID:57,58;
end;
hence q`1<>0;
end;
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 let p be Point of TOP-REAL 2;
assume A25: p in the carrier of (TOP-REAL 2)|K1;
A26: (the carrier of TOP-REAL 2)\{0.REAL 2}<>{} by Th19;
A27:dom (Out_In_Sq|K1)=dom Out_In_Sq /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2)\{0.REAL 2})/\ K1 by A26,FUNCT_2:def 1
.=K1 by A11,XBOOLE_1:28;
A28:the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) by PRE_TOPC:12
.=K1 by PRE_TOPC:def 10;
then consider p3 being Point of TOP-REAL 2 such that
A29: p=p3 & ((p3`2<=p3`1 & -p3`1<=p3`2 or p3`2>=p3`1 & p3`2<=-p3`1)
& p3<>0.REAL 2) by A1,A25;
A30:Out_In_Sq.p=|[1/p`1,p`2/p`1/p`1]| by A29,Def1;
(Out_In_Sq|K1).p=Out_In_Sq.p by A25,A28,FUNCT_1:72;
then g2.p=(proj2).(|[1/p`1,p`2/p`1/p`1]|) by A25,A27,A28,A30,FUNCT_1:23
.=(|[1/p`1,p`2/p`1/p`1]|)`2 by PSCOMP_1:def 29
.=p`2/p`1/p`1 by EUCLID:56;
hence g2.p=p`2/p`1/p`1;
end;
then consider f2 being map of (TOP-REAL 2)|K1,R^1 such that
A31: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;
A32:f2 is continuous by A21,A31,Th43;
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 let p be Point of TOP-REAL 2;
assume A33: p in the carrier of (TOP-REAL 2)|K1;
A34:K1 c= (the carrier of TOP-REAL 2)\{0.REAL 2}
proof let z be set;assume z in K1;
then consider p8 being Point of TOP-REAL 2 such that
A35: p8=z &(
(p8`2<=p8`1 & -p8`1<=p8`2 or p8`2>=p8`1 & p8`2<=-p8`1)
& p8<>0.REAL 2) by A1;
z in (the carrier of TOP-REAL 2) & not z in {0.REAL 2}
by A35,TARSKI:def 1;
hence z in (the carrier of TOP-REAL 2)\{0.REAL 2} by XBOOLE_0:def 4;
end;
A36: (the carrier of TOP-REAL 2)\{0.REAL 2}<>{} by Th19;
A37:dom (Out_In_Sq|K1)=dom Out_In_Sq /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2)\{0.REAL 2})/\ K1 by A36,FUNCT_2:def 1
.=K1 by A34,XBOOLE_1:28;
A38:the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) by PRE_TOPC:12
.=K1 by PRE_TOPC:def 10;
then consider p3 being Point of TOP-REAL 2 such that
A39: p=p3 & ((p3`2<=p3`1 & -p3`1<=p3`2 or p3`2>=p3`1 & p3`2<=-p3`1)
& p3<>0.REAL 2) by A1,A33;
A40:Out_In_Sq.p=|[1/p`1,p`2/p`1/p`1]| by A39,Def1;
(Out_In_Sq|K1).p=Out_In_Sq.p by A33,A38,FUNCT_1:72;
then g1.p=(proj1).(|[1/p`1,p`2/p`1/p`1]|)
by A33,A37,A38,A40,FUNCT_1:23
.=(|[1/p`1,p`2/p`1/p`1]|)`1 by PSCOMP_1:def 28
.=1/p`1 by EUCLID:56;
hence g1.p=1/p`1;
end;
then consider f1 being map of (TOP-REAL 2)|K1,R^1 such that
A41:for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f1.p=1/p`1;
A42:f1 is continuous by A21,A41,Th41;
for x,y,r,s being real number 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 number;
assume A43: |[x,y]| in K1 & r=f1.(|[x,y]|) & s=f2.(|[x,y]|);
set p99=|[x,y]|;
A44:the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) by PRE_TOPC:12
.=K1 by PRE_TOPC:def 10;
consider p3 being Point of TOP-REAL 2 such that
A45: p99=p3 & ((p3`2<=p3`1 & -p3`1<=p3`2 or p3`2>=p3`1 & p3`2<=-p3`1)
& p3<>0.REAL 2) by A1,A43;
A46:((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]|) &
(not(p99`2<=p99`1 & -p99`1<=p99`2 or p99`2>=p99`1 & p99`2<=-p99`1)
implies
Out_In_Sq.p99=|[p99`1/p99`2/p99`2,1/p99`2]|) by A45,Def1;
A47:f1.p99=1/p99`1 by A41,A43,A44;
(Out_In_Sq|K0). |[x,y]|= |[1/p99`1,p99`2/p99`1/p99`1]| by A43,A45,A46,
FUNCT_1:72
.=|[r,s]| by A31,A43,A44,A47;
hence f. |[x,y]|=|[r,s]| by A1;
end;
hence f is continuous by A2,A3,A32,A42,Th45;
end;
theorem Th47: for K0,B0 being Subset of TOP-REAL 2,f being
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0
st f=Out_In_Sq|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} &
K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.REAL 2}
holds f is continuous
proof let K0,B0 be Subset of TOP-REAL 2,f be
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0;
assume A1:f=Out_In_Sq|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} &
K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.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) &
(1.REAL 2)<>0.REAL 2
by Th13,REVROT_1:19;
then A2:1.REAL 2 in K0 by A1;
then reconsider K1=K0 as non empty Subset of TOP-REAL 2;
A3: K0 c= B0
proof let x be set;assume x in K0;
then consider p8 being Point of TOP-REAL 2 such that
A4: x=p8
& (
(p8`1<=p8`2 & -p8`2<=p8`1 or p8`1>=p8`2 & p8`1<=-p8`2) & p8<>0.REAL 2)
by A1;
not x in {0.REAL 2} by A4,TARSKI:def 1;
hence x in B0 by A1,A4,XBOOLE_0:def 4;
end;
A5:dom ((proj1)*(Out_In_Sq|K1)) c= dom (Out_In_Sq|K1) by RELAT_1:44;
A6:dom (Out_In_Sq|K1) c= dom ((proj1)*(Out_In_Sq|K1))
proof let x be set;assume A7:x in dom (Out_In_Sq|K1);
then A8:x in dom Out_In_Sq /\ K1 by FUNCT_1:68;
A9:(Out_In_Sq|K1).x=Out_In_Sq.x by A7,FUNCT_1:68;
A10: dom proj1 = (the carrier of TOP-REAL 2) by FUNCT_2:def 1;
x in dom Out_In_Sq by A8,XBOOLE_0:def 3;
then Out_In_Sq.x in rng Out_In_Sq by FUNCT_1:12;
then Out_In_Sq.x in the carrier of TOP-REAL 2 by XBOOLE_0:def 4;
hence x in dom ((proj1)*(Out_In_Sq|K1)) by A7,A9,A10,FUNCT_1:21;
end;
A11:K1 c= (the carrier of TOP-REAL 2)\{0.REAL 2}
proof let z be set;assume z in K1;
then consider p8 being Point of TOP-REAL 2 such that
A12: p8=z &(
(p8`1<=p8`2 & -p8`2<=p8`1 or p8`1>=p8`2 & p8`1<=-p8`2)
& p8<>0.REAL 2) by A1;
z in (the carrier of TOP-REAL 2) & not z in {0.REAL 2}
by A12,TARSKI:def 1;
hence z in (the carrier of TOP-REAL 2)\{0.REAL 2} by XBOOLE_0:def 4;
end;
A13: (the carrier of TOP-REAL 2)\{0.REAL 2}<>{} by Th19;
A14:dom ((proj1)*(Out_In_Sq|K1))
=dom (Out_In_Sq|K1) by A5,A6,XBOOLE_0:def 10
.=dom Out_In_Sq /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2)\{0.REAL 2})/\ K1 by A13,FUNCT_2:def 1
.=K1 by A11,XBOOLE_1:28
.=[#]((TOP-REAL 2)|K1) by PRE_TOPC:def 10
.=the carrier of (TOP-REAL 2)|K1 by PRE_TOPC:12;
rng ((proj1)*(Out_In_Sq|K1)) c= rng (proj1) by RELAT_1:45;
then rng ((proj1)*(Out_In_Sq|K1)) c= the carrier of R^1 by TOPMETR:24,XBOOLE_1:
1;
then (proj1)*(Out_In_Sq|K1) is Function of the carrier of (TOP-REAL 2)|K1,
the carrier of R^1 by A14,FUNCT_2:4;
then reconsider g2=(proj1)*(Out_In_Sq|K1) as map of (TOP-REAL 2)|K1,R^1;
A15:dom ((proj2)*(Out_In_Sq|K1)) c= dom (Out_In_Sq|K1) by RELAT_1:44;
dom (Out_In_Sq|K1) c= dom ((proj2)*(Out_In_Sq|K1))
proof let x be set;assume A16:x in dom (Out_In_Sq|K1);
then A17:x in dom Out_In_Sq /\ K1 by FUNCT_1:68;
A18:(Out_In_Sq|K1).x=Out_In_Sq.x by A16,FUNCT_1:68;
A19: dom proj2 = (the carrier of TOP-REAL 2) by FUNCT_2:def 1;
x in dom Out_In_Sq by A17,XBOOLE_0:def 3;
then Out_In_Sq.x in rng Out_In_Sq by FUNCT_1:12;
then Out_In_Sq.x in the carrier of TOP-REAL 2 by XBOOLE_0:def 4;
hence x in dom ((proj2)*(Out_In_Sq|K1)) by A16,A18,A19,FUNCT_1:21;
end;
then A20:dom ((proj2)*(Out_In_Sq|K1))
=dom (Out_In_Sq|K1) by A15,XBOOLE_0:def 10
.=dom Out_In_Sq /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2)\{0.REAL 2})/\ K1 by A13,FUNCT_2:def 1
.=K1 by A11,XBOOLE_1:28
.=[#]((TOP-REAL 2)|K1) by PRE_TOPC:def 10
.=the carrier of (TOP-REAL 2)|K1 by PRE_TOPC:12;
rng ((proj2)*(Out_In_Sq|K1)) c= rng (proj2) by RELAT_1:45;
then rng ((proj2)*(Out_In_Sq|K1)) c= the carrier of R^1 by TOPMETR:24,XBOOLE_1:
1;
then (proj2)*(Out_In_Sq|K1) is Function of the carrier of (TOP-REAL 2)|K1,
the carrier of R^1 by A20,FUNCT_2:4;
then reconsider g1=(proj2)*(Out_In_Sq|K1) as map of (TOP-REAL 2)|K1,R^1;
A21: 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;
assume A22:q in the carrier of (TOP-REAL 2)|K1;
the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) by PRE_TOPC:12
.=K1 by PRE_TOPC:def 10;
then consider p3 being Point of TOP-REAL 2 such that
A23: q=p3 & ((p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 & p3`1<=-p3`2)
& p3<>0.REAL 2) by A1,A22;
now assume A24:q`2=0;
then q`1=0 by A23;
hence contradiction by A23,A24,EUCLID:57,58;
end;
hence q`2<>0;
end;
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 let p be Point of TOP-REAL 2;
assume A25: p in the carrier of (TOP-REAL 2)|K1;
A26: (the carrier of TOP-REAL 2)\{0.REAL 2}<>{} by Th19;
A27:dom (Out_In_Sq|K1)=dom Out_In_Sq /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2)\{0.REAL 2})/\ K1 by A26,FUNCT_2:def 1
.=K1 by A11,XBOOLE_1:28;
A28:the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) by PRE_TOPC:12
.=K1 by PRE_TOPC:def 10;
then consider p3 being Point of TOP-REAL 2 such that
A29: p=p3 & ((p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 & p3`1<=-p3`2)
& p3<>0.REAL 2) by A1,A25;
A30:Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A29,Th24;
(Out_In_Sq|K1).p=Out_In_Sq.p by A25,A28,FUNCT_1:72;
then g2.p=(proj1).(|[p`1/p`2/p`2,1/p`2]|) by A25,A27,A28,A30,FUNCT_1:23
.=(|[p`1/p`2/p`2,1/p`2]|)`1 by PSCOMP_1:def 28
.=p`1/p`2/p`2 by EUCLID:56;
hence g2.p=p`1/p`2/p`2;
end;
then consider f2 being map of (TOP-REAL 2)|K1,R^1 such that
A31: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;
A32:f2 is continuous by A21,A31,Th44;
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 let p be Point of TOP-REAL 2;
assume A33: p in the carrier of (TOP-REAL 2)|K1;
A34:K1 c= (the carrier of TOP-REAL 2)\{0.REAL 2}
proof let z be set;assume z in K1;
then consider p8 being Point of TOP-REAL 2 such that
A35: p8=z &(
(p8`1<=p8`2 & -p8`2<=p8`1 or p8`1>=p8`2 & p8`1<=-p8`2)
& p8<>0.REAL 2) by A1;
z in (the carrier of TOP-REAL 2) & not z in {0.REAL 2}
by A35,TARSKI:def 1;
hence z in (the carrier of TOP-REAL 2)\{0.REAL 2} by XBOOLE_0:def 4;
end;
A36: (the carrier of TOP-REAL 2)\{0.REAL 2}<>{} by Th19;
A37:dom (Out_In_Sq|K1)=dom Out_In_Sq /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2)\{0.REAL 2})/\ K1 by A36,FUNCT_2:def 1
.=K1 by A34,XBOOLE_1:28;
A38:the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) by PRE_TOPC:12
.=K1 by PRE_TOPC:def 10;
then consider p3 being Point of TOP-REAL 2 such that
A39: p=p3 & ((p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 & p3`1<=-p3`2)
& p3<>0.REAL 2) by A1,A33;
A40:Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A39,Th24;
(Out_In_Sq|K1).p=Out_In_Sq.p by A33,A38,FUNCT_1:72;
then g1.p=(proj2).(|[p`1/p`2/p`2,1/p`2]|)
by A33,A37,A38,A40,FUNCT_1:23
.=(|[p`1/p`2/p`2,1/p`2]|)`2 by PSCOMP_1:def 29
.=1/p`2 by EUCLID:56;
hence g1.p=1/p`2;
end;
then consider f1 being map of (TOP-REAL 2)|K1,R^1 such that
A41:for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f1.p=1/p`2;
A42:f1 is continuous by A21,A41,Th42;
for x,y,s,r being real number 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 number;
assume A43: |[x,y]| in K1 & s=f2.(|[x,y]|) & r=f1.(|[x,y]|);
set p99=|[x,y]|;
A44:the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) by PRE_TOPC:12
.=K1 by PRE_TOPC:def 10;
consider p3 being Point of TOP-REAL 2 such that
A45: p99=p3 & ((p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 & p3`1<=-p3`2)
& p3<>0.REAL 2) by A1,A43;
A46:f1.p99=1/p99`2 by A41,A43,A44;
(Out_In_Sq|K0). |[x,y]|=(Out_In_Sq). |[x,y]| by A43,FUNCT_1:72
.= |[p99`1/p99`2/p99`2,1/p99`2]| by A45,Th24
.=|[s,r]| by A31,A43,A44,A46;
hence f. |[x,y]|=|[s,r]| by A1;
end;
hence thesis by A2,A3,A32,A42,Th45;
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 set;
assume x in { p where p is Point of TOP-REAL 2 : P[p] };
then consider p being Point of TOP-REAL 2 such that
A1: p = x & P[p];
thus x in the carrier of TOP-REAL 2 by A1;
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 set;assume A2:x in K()`;
then x in K()`;
then x in (the carrier of TOP-REAL 2) \ K() by SUBSET_1:def 5;
then A3:x in (the carrier of TOP-REAL 2) & not x in K() by XBOOLE_0:def 4;
reconsider qx=x as Point of TOP-REAL 2 by A2;
not P[qx] by A1,A3;
hence x in {p7 where p7 is Point of TOP-REAL 2: not P[p7]};
end;
let x be set;assume
x in {p7 where p7 is Point of TOP-REAL 2: not P[p7]};
then consider p7 being Point of TOP-REAL 2 such that
A4: p7=x & not P[p7];
not ex q7 being Point of TOP-REAL 2 st x=q7 & P[q7] by A4;
then not x in K() by A1;
then x in (the carrier of TOP-REAL 2) \ K() by A4,XBOOLE_0:def 4;
then x in K()` by SUBSET_1:def 5;
hence x in K()`;
end;
Lm2:now let p01, p02,px1,px2 be real number; set r0 = (p01 -p02)/4;
assume p01 - px1 - (p02 - px2)<=r0--r0;
then p01 - px1 - (p02 - px2)<=r0+r0 by XCMPLX_1:151;
then p01 - px1 - p02 + px2<=r0+r0 by XCMPLX_1:37;
then p01 - p02 - px1 + px2<=r0+r0 by XCMPLX_1:21;
then p01 - p02 - (px1 - px2)<=r0+r0 by XCMPLX_1:37;
then p01 - p02<= (px1 - px2)+(r0+r0) by REAL_1:86;
then p01 - p02 - (r0+r0)<= (px1 - px2) by REAL_1:86;
then p01 - p02 - (p01 -p02)/2<= (px1 - px2) by XCMPLX_1:72;
then (p01 - p02)/2+(p01 - p02)/2 - (p01 -p02)/2<= (px1 - px2) by XCMPLX_1:66
;
hence (p01 - p02)/2<= px1 - px2 by XCMPLX_1:26;
end;
scheme ClosedSubset { F,G(Point of TOP-REAL 2) -> real number } :
{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