Copyright (c) 2003 Association of Mizar Users
environ
vocabulary FUNCT_1, BOOLE, ABSVALUE, EUCLID, PRE_TOPC, SQUARE_1, RELAT_1,
SUBSET_1, ARYTM_3, METRIC_1, RCOMP_1, FUNCT_5, TOPMETR, COMPTS_1,
ORDINAL2, TOPS_2, ARYTM_1, ARYTM, COMPLEX1, MCART_1, PCOMPS_1, JGRAPH_3,
BORSUK_1, TOPREAL1, TOPREAL2, JORDAN3, PSCOMP_1, REALSET1, JORDAN5C,
JORDAN6, JGRAPH_2, JGRAPH_6, RELAT_2, FINSEQ_1, FINSEQ_4, TARSKI, TOPS_1,
FUNCT_4, JORDAN17;
notation XBOOLE_0, ORDINAL1, ABSVALUE, EUCLID, TARSKI, RELAT_1, TOPS_2,
FUNCT_1, FUNCT_2, SUBSET_1, FINSEQ_1, STRUCT_0, TOPMETR, PCOMPS_1,
COMPTS_1, METRIC_1, SQUARE_1, RCOMP_1, PRE_TOPC, FUNCT_4, JGRAPH_3,
JORDAN5C, JORDAN6, TOPREAL2, CONNSP_1, FINSEQ_4, TOPS_1, JORDAN17,
JGRAPH_2, NUMBERS, XCMPLX_0, XREAL_0, TOPRNS_1, TOPREAL1, PSCOMP_1,
REAL_1, NAT_1;
constructors TOPS_1, RCOMP_1, JGRAPH_2, TOPREAL2, TOPGRP_1, CONNSP_1,
WELLFND1, JGRAPH_3, JORDAN5C, JORDAN6, TOPRNS_1, TREAL_1, FINSEQ_4,
TOPS_2, JORDAN17, TOPREAL1, PSCOMP_1, REAL_1, NAT_1;
clusters STRUCT_0, RELSET_1, FUNCT_1, EUCLID, PRE_TOPC, TOPMETR, SQUARE_1,
PSCOMP_1, BORSUK_1, TOPREAL2, BORSUK_2, TOPREAL1, JGRAPH_3, TOPS_1,
JGRAPH_2, TOPREAL6, XREAL_0, NAT_1, MEMBERED, XBOOLE_0;
requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
definitions TARSKI, XBOOLE_0, TOPREAL1;
theorems TARSKI, XBOOLE_0, XBOOLE_1, AXIOMS, RELAT_1, FUNCT_1, FUNCT_2,
TOPS_1, TOPS_2, PRE_TOPC, TOPMETR, JORDAN6, EUCLID, REAL_1, REAL_2,
JGRAPH_1, SQUARE_1, PSCOMP_1, METRIC_1, JGRAPH_2, RCOMP_1, COMPTS_1,
RFUNCT_2, BORSUK_1, TOPREAL1, TOPREAL3, TOPREAL5, JGRAPH_3, ABSVALUE,
JORDAN7, HEINE, JGRAPH_4, JORDAN5C, JGRAPH_5, GOBOARD6, JORDAN2C,
TOPREAL2, TREAL_1, SEQ_2, FINSEQ_1, FINSEQ_3, FINSEQ_4, ZFMISC_1, NAT_1,
ENUMSET1, UNIFORM1, BORSUK_4, TSEP_1, FUNCT_4, JORDAN1A, JORDAN17,
JORDAN1, GOBOARD7, XREAL_0, TOPRNS_1, COMPLEX1, XCMPLX_0, XCMPLX_1;
schemes FUNCT_2, JGRAPH_2, TOPREAL1, FRAENKEL, FUNCT_1, DOMAIN_1;
begin :: Preliminaries
canceled;
theorem Th2: for a,b,r being real number st 0<=r & r<=1 & a<=b holds
a<=(1-r)*a+r*b & (1-r)*a+r*b<=b
proof let a,b,r be real number;
assume A1: 0<=r & r<=1 & a<=b;
then A2: 1-r>=0 by SQUARE_1:12;
r*a<=r*b by A1,AXIOMS:25;
then (1-r)*a+r*a<=(1-r)*a+r*b by REAL_1:55;
then ((1-r)+r)*a<=(1-r)*a+r*b by XCMPLX_1:8;
then 1*a<=(1-r)*a+r*b by XCMPLX_1:27;
hence a<=(1-r)*a+r*b;
(1-r)*a<=(1-r)*b by A1,A2,AXIOMS:25;
then (1-r)*a+r*b<=(1-r)*b+r*b by REAL_1:55;
then ((1-r)+r)*b>=(1-r)*a+r*b by XCMPLX_1:8;
then 1*b>=(1-r)*a+r*b by XCMPLX_1:27;
hence (1-r)*a+r*b<=b;
end;
theorem Th3:
for a,b being real number st a>=0 & b>0 or a>0 & b>=0 holds a+b>0
proof let a,b be real number;
assume A1: a>=0 & b>0 or a>0 & b>=0;
now per cases by A1;
case a>=0 & b>0;
hence a+b>0 by REAL_1:69;
case a>0 & b>=0;
hence a+b>0 by REAL_1:69;
end;
hence a+b>0;
end;
theorem Th4: for a,b being real number st -1<=a & a<=1 & -1<=b & b<=1
holds a^2*b^2<=1
proof let a,b be real number;
assume A1: -1<=a & a<=1 & -1<=b & b<=1;
then A2: a^2<=1 by JGRAPH_2:7,SQUARE_1:59;
A3: b^2<=1 by A1,JGRAPH_2:7,SQUARE_1:59;
0<=b^2 by SQUARE_1:72;
then a^2*b^2 <= 1*b^2 by A2,AXIOMS:25;
hence a^2*b^2<=1 by A3,AXIOMS:22;
end;
theorem Th5: for a,b being real number st a>=0 & b>=0
holds a*sqrt(b)=sqrt(a^2*b)
proof let a,b be real number;
assume A1: a>=0 & b>=0;
then A2: sqrt(a^2)=a by SQUARE_1:89;
a^2>=0 by SQUARE_1:72;
hence a*sqrt(b)=sqrt(a^2*b) by A1,A2,SQUARE_1:97;
end;
Lm1: for a,b being real number st -1<=a & a<=1 & -1<=b & b<=1
holds (1+a^2)*b^2<=1+b^2
proof let a,b be real number;
assume -1<=a & a<=1 & -1<=b & b<=1;
then a^2*b^2<=1 by Th4;
then 1*b^2+a^2*b^2<=1+b^2 by REAL_1:55;
hence (1+a^2)*b^2<=1+b^2 by XCMPLX_1:8;
end;
theorem Th6: for a,b being real number st -1<=a & a<=1 & -1<=b & b<=1
holds (-b)*sqrt(1+a^2)<=sqrt(1+b^2) & -sqrt(1+b^2)<= b*sqrt(1+a^2)
proof let a,b be real number;
assume A1: -1<=a & a<=1 & -1<=b & b<=1;
a^2>=0 by SQUARE_1:72;
then 1+a^2>=1+0 by REAL_1:55;
then A2: 1+a^2>=0 by AXIOMS:22;
then A3: sqrt(1+a^2)>=0 by SQUARE_1:def 4;
b^2>=0 by SQUARE_1:72;
then 1+b^2>=1+0 by REAL_1:55;
then 1+b^2>=0 by AXIOMS:22;
then A4: sqrt(1+b^2)>=0 by SQUARE_1:def 4;
A5: now per cases;
case b>=0;
then -b<=0 by REAL_1:66;
hence (-b)*sqrt(1+a^2)<=sqrt(1+b^2) by A3,A4,SQUARE_1:23;
case b<0; then -b>0 by REAL_1:66;
then A6: (-b)*sqrt(1+a^2)=sqrt((-b)^2*(1+a^2)) by A2,Th5;
(1+a^2)*b^2<=1+b^2 by A1,Lm1;
then A7: (-b)^2*(1+a^2)<=1+b^2 by SQUARE_1:61;
(-b)^2>=0 by SQUARE_1:72;
then (-b)^2*(1+a^2)>=0 by A2,SQUARE_1:19;
hence (-b)*sqrt(1+a^2)<=sqrt(1+b^2) by A6,A7,SQUARE_1:94;
end;
then -((-b)*sqrt(1+a^2)) >= - sqrt(1+b^2) by REAL_1:50;
then ((--b)*sqrt(1+a^2)) >= - sqrt(1+b^2) by XCMPLX_1:175;
hence (-b)*sqrt(1+a^2)<=sqrt(1+b^2) & -sqrt(1+b^2)<= b*sqrt(1+a^2) by A5;
end;
theorem Th7: for a,b being real number st -1<=a & a<=1 & -1<=b & b<=1
holds b*sqrt(1+a^2)<=sqrt(1+b^2)
proof let a,b be real number;
assume A1: -1<=a & a<=1 & -1<=b & b<=1;
then A2: --1>=-b by REAL_1:50;
-1<=-b by A1,REAL_1:50;
then (--b)*sqrt(1+a^2)<=sqrt(1+(-b)^2) by A1,A2,Th6;
hence b*sqrt(1+a^2)<=sqrt(1+b^2) by SQUARE_1:61;
end;
Lm2: for a,b being real number st b<=0 & a<=b
holds a*sqrt(1+b^2)<= b*sqrt(1+a^2)
proof let a,b be real number;
assume A1: b<=0 & a<=b;
a^2>=0 by SQUARE_1:72;
then 1+a^2>=1+0 by REAL_1:55;
then A2: 1+a^2>=0 by AXIOMS:22;
b^2>=0 by SQUARE_1:72;
then 1+b^2>=1+0 by REAL_1:55;
then A3: 1+b^2>=0 by AXIOMS:22;
--b<=0 by A1;
then -b>=0 by REAL_1:66;
then A4: (-b)*sqrt(1+a^2)=sqrt((-b)^2*(1+a^2)) by A2,Th5;
--a<=0 by A1;
then -a>=0 by REAL_1:66;
then A5: (-a)*sqrt(1+b^2)=sqrt((-a)^2*(1+b^2)) by A3,Th5;
A6: (-a)^2=a^2 by SQUARE_1:61;
A7: (-b)^2=b^2 by SQUARE_1:61;
a<b or a=b by A1,REAL_1:def 5;
then b^2<a^2 or a=b by A1,JGRAPH_5:2;
then b^2*1+b^2*a^2<=a^2*1+a^2*b^2 by REAL_1:55;
then b^2*1+b^2*a^2<=a^2*(1+b^2) by XCMPLX_1:8;
then A8: b^2*(1+a^2)<=a^2*(1+b^2) by XCMPLX_1:8;
(b)^2>=0 by SQUARE_1:72;
then (b)^2*(1+a^2)>=0 by A2,SQUARE_1:19;
then sqrt((a)^2*(1+b^2))>=sqrt(b^2*(1+a^2)) by A8,SQUARE_1:94;
then -(a*sqrt(1+b^2))>=(-b)*sqrt(1+a^2) by A4,A5,A6,A7,XCMPLX_1:175;
then -(a*sqrt(1+b^2))>= -(b*sqrt(1+a^2)) by XCMPLX_1:175;
hence (a)*sqrt(1+b^2)<=b*sqrt(1+a^2) by REAL_1:50;
end;
Lm3: for a,b being real number st a<=0 & a<=b
holds a*sqrt(1+b^2)<= b*sqrt(1+a^2)
proof let a,b be real number;
assume A1: a<=0 & a<=b;
now per cases;
case b<=0;
hence b*sqrt(1+a^2)>= a*sqrt(1+b^2) by A1,Lm2;
case A2: b>0;
A3: (b)^2 >=0 by SQUARE_1:72;
1+(b)^2 >(b)^2 by REAL_1:69;
then sqrt(1+(b)^2)>0 by A3,SQUARE_1:93;
then A4: a*sqrt(1+b^2)<=0 by A1,SQUARE_1:23;
A5: (a)^2 >=0 by SQUARE_1:72;
1+(a)^2 >(a)^2 by REAL_1:69;
then sqrt(1+(a)^2)>0 by A5,SQUARE_1:93;
hence b*sqrt(1+a^2)>= a*sqrt(1+b^2) by A2,A4,REAL_2:121;
end;
hence thesis;
end;
Lm4: for a,b being real number st a>=0 & a>=b
holds a*sqrt(1+b^2)>= b*sqrt(1+a^2)
proof let a,b be real number;
assume A1: a>=0 & a>=b;
then A2: -a<=0 by REAL_1:66;
-a <= -b by A1,REAL_1:50;
then (-a)*sqrt(1+(-b)^2)<= (-b)*sqrt(1+(-a)^2) by A2,Lm3;
then (-a)*sqrt(1+(b)^2)<= (-b)*sqrt(1+(-a)^2) by SQUARE_1:61;
then (-a)*sqrt(1+(b)^2)<= (-b)*sqrt(1+(a)^2) by SQUARE_1:61;
then -(a*sqrt(1+(b)^2))<= (-b)*sqrt(1+(a)^2) by XCMPLX_1:175;
then -(a*sqrt(1+(b)^2))<= -(b*sqrt(1+(a)^2)) by XCMPLX_1:175;
hence a*sqrt(1+b^2)>= b*sqrt(1+a^2) by REAL_1:50;
end;
theorem Th8: for a,b being real number st a>=b
holds a*sqrt(1+b^2)>= b*sqrt(1+a^2)
proof let a,b be real number;
assume A1: a>=b;
per cases;
suppose a>=0;
hence thesis by A1,Lm4;
suppose a<0;
hence thesis by A1,Lm2;
end;
theorem Th9: for a,c,d being real number,p being Point of TOP-REAL 2
st c <=d & p in LSeg(|[a,c]|,|[a,d]|) holds p`1=a & c <=p`2 & p`2<=d
proof let a,c,d be real number,p be Point of TOP-REAL 2;
assume A1: c <=d & p in LSeg(|[a,c]|,|[a,d]|);
reconsider a2=a,c2=c,d2=d as Real by XREAL_0:def 1;
p in LSeg(|[a2,c2]|,|[a2,d2]|) by A1;
hence p`1=a by TOPREAL3:17;
A2: (|[a,c]|)`2=c by EUCLID:56;
(|[a,d]|)`2=d by EUCLID:56;
hence c <=p`2 & p`2<=d by A1,A2,TOPREAL1:10;
end;
theorem Th10: for a,c,d being real number,p being Point of TOP-REAL 2
st c <d & p`1=a & c <=p`2 & p`2<=d holds p in LSeg(|[a,c]|,|[a,d]|)
proof let a,c,d be real number,p be Point of TOP-REAL 2;
assume A1: c <d & p`1=a & c <=p`2 & p`2<=d;
then A2: d-c>0 by SQUARE_1:11;
reconsider w=(p`2-c)/(d-c) as Real by XREAL_0:def 1;
A3: (1-w)*(|[a,c]|)+w*(|[a,d]|)
=|[(1-w)*a,(1-w)*c]|+w*(|[a,d]|) by EUCLID:62
.=|[(1-w)*a,(1-w)*c]|+(|[w*a,w*d]|) by EUCLID:62
.=|[(1-w)*a+w*a,(1-w)*c+w*d]| by EUCLID:60
.=|[((1-w)+w)*a,(1-w)*c+w*d]| by XCMPLX_1:8
.=|[(1)*a,(1-w)*c+w*d]| by XCMPLX_1:27
.=|[a,(1*c-w*c)+w*d]| by XCMPLX_1:40
.= |[a,c+w*d-w*c]| by XCMPLX_1:29
.= |[a,c+(w*d-w*c)]| by XCMPLX_1:29
.= |[a,c+w*(d-c)]| by XCMPLX_1:40
.= |[a,c+(p`2-c)]| by A2,XCMPLX_1:88
.= |[a,p`2]| by XCMPLX_1:27
.= p by A1,EUCLID:57;
A4: p`2-c>=0 by A1,SQUARE_1:12;
p`2-c <=d-c by A1,REAL_1:49;
then w<=(d-c)/(d-c) by A2,REAL_1:73;
then 0<=w & w<=1 by A2,A4,REAL_2:125,XCMPLX_1:60;
then p in { (1-lambda)*(|[a,c]|) + lambda*(|[a,d]|) where lambda is Real
: 0 <= lambda & lambda <= 1 } by A3;
hence thesis by TOPREAL1:def 4;
end;
theorem Th11: for a,b,d being real number,p being Point of TOP-REAL 2
st a <=b & p in LSeg(|[a,d]|,|[b,d]|) holds p`2=d & a <=p`1 & p`1<=b
proof let a,b,d be real number,p be Point of TOP-REAL 2;
assume A1: a <=b & p in LSeg(|[a,d]|,|[b,d]|);
reconsider a2=a,b2=b,d2=d as Real by XREAL_0:def 1;
p in LSeg(|[a2,d2]|,|[b2,d2]|) by A1;
hence p`2=d by TOPREAL3:18;
A2: (|[a,d]|)`1=a by EUCLID:56;
(|[b,d]|)`1=b by EUCLID:56;
hence a <=p`1 & p`1<=b by A1,A2,TOPREAL1:9;
end;
theorem Th12: :: BORSUK_4:48
for a,b being real number,B being Subset of I[01] st
B=[.a,b.] holds B is closed
proof let a,b be real number,B be Subset of I[01];
assume A1: B=[.a,b.];
B c= the carrier of R^1 by BORSUK_1:83,TOPMETR:24,XBOOLE_1:1;
then reconsider B2=B as Subset of R^1;
A2: B2 is closed by A1,TREAL_1:4;
reconsider I1=[.0,1.] as Subset of R^1 by TOPMETR:24;
A3: [#](R^1|I1)=the carrier of I[01] by BORSUK_1:83,PRE_TOPC:def 10;
A4: I[01]=R^1|I1 by TOPMETR:26,27;
B=B2 /\ [#](R^1|I1) by A3,XBOOLE_1:28;
hence B is closed by A2,A4,PRE_TOPC:43;
end;
theorem Th13: for X being TopStruct,Y,Z being non empty TopStruct,
f being map of X,Y, g being map of X,Z holds dom f=dom g
& dom f=the carrier of X & dom f=[#]X
proof let X be TopStruct,Y,Z be non empty TopStruct,
f be map of X,Y, g be map of X,Z;
dom f=the carrier of X by FUNCT_2:def 1;
hence dom f=dom g
& dom f=the carrier of X & dom f=[#]X by FUNCT_2:def 1,PRE_TOPC:12;
end;
theorem Th14:
for X being non empty TopSpace,B being non empty Subset of X
ex f being map of X|B,X st (for p being Point of X|B holds f.p=p) &
f is continuous
proof let X be non empty TopSpace,B be non empty Subset of X;
defpred P[set,set] means (for p being Point of X|B holds $2=$1);
A1: the carrier of X|B = [#](X|B) by PRE_TOPC:12;
A2: [#](X|B)= B by PRE_TOPC:def 10;
A3: for x being Element of X|B
ex y being Element of X st P[x,y]
proof let x be Element of X|B;
x in B by A1,A2;
then reconsider px=x as Point of X;
set y0=px;
P[x,y0];
hence ex y being Element of X st P[x,y];
end;
ex g being Function of the carrier of X|B,the carrier of X st
for x being Element of X|B holds P[x,g.x]
from FuncExD(A3);
then consider g being Function of the carrier of X|B,the carrier of X such
that
A4: for x being Element of X|B holds P[x,g.x];
A5: for p being Point of X|B holds g.p=p by A4;
A6: for r0 being Point of X|B,V being Subset of X
st g.r0 in V & V is open holds
ex W being Subset of X|B st r0 in W & W is open & g.:W c= V
proof let r0 be Point of X|B,V be Subset of X;
assume A7: g.r0 in V & V is open;
V /\ [#](X|B) c= [#](X|B) by XBOOLE_1:17;
then reconsider W2=V /\ [#](X|B) as Subset of X|B by A1;
r0 in the carrier of (X|B);
then A8: r0 in [#](X|B) by PRE_TOPC:12;
g.r0=r0 by A4;
then A9: r0 in W2 by A7,A8,XBOOLE_0:def 3;
A10: W2 is open by A7,TOPS_2:32;
g.:W2 c= V
proof let y be set;assume y in g.:W2;
then consider x being set such that
A11: x in dom g & x in W2 & y=g.x by FUNCT_1:def 12;
reconsider px=x as Point of X|B by A11;
g.px=px by A4;
hence y in V by A11,XBOOLE_0:def 3;
end;
hence ex W being Subset of X|B st r0 in W & W is open & g.:W c= V
by A9,A10;
end;
reconsider g1=g as map of X|B,X ;
g1 is continuous by A6,JGRAPH_2:20;
hence thesis by A5;
end;
theorem Th15:
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 be non empty TopSpace,
f1 be map of X,R^1,a be real number;
assume f1 is continuous;
then consider g1 being map of X,R^1 such that
A1: (for p being Point of X,r1 being real number st
f1.p=r1 holds g1.p=r1+-a) & g1 is continuous by JGRAPH_2:34;
for p being Point of X,r1 being real number st
f1.p=r1 holds g1.p=r1-a
proof let p be Point of X,r1 be real number;
assume f1.p=r1;
then g1.p=r1+-a by A1;
hence g1.p=r1-a by XCMPLX_0:def 8;
end;
hence thesis by A1;
end;
theorem Th16:
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 be non empty TopSpace,
f1 be map of X,R^1,a be real number;
assume f1 is continuous;
then consider g1 being map of X,R^1 such that
A1: (for p being Point of X,r1 being real number st
f1.p=r1 holds g1.p=r1-a) & g1 is continuous by Th15;
consider g2 being map of X,R^1 such that
A2: (for p being Point of X,r1 being real number st
g1.p=r1 holds g2.p= -r1) & g2 is continuous by A1,JGRAPH_4:13;
for p being Point of X,r1 being real number st
f1.p=r1 holds g2.p=a-r1
proof let p be Point of X,r1 be real number;
assume f1.p=r1; then g1.p=r1-a by A1;
then g2.p=-(r1-a) by A2 .=0-(r1-a) by XCMPLX_1:150
.=0-r1+a by XCMPLX_1:37
.=a+-r1 by XCMPLX_1:150 .=a-r1 by XCMPLX_0:def 8;
hence g2.p=a-r1;
end;
hence thesis by A2;
end;
theorem Th17: for X being non empty TopSpace, n being Nat,
p being Point of TOP-REAL n,
f being map of X,R^1 st f is continuous ex g being map of X,TOP-REAL n
st (for r being Point of X holds g.r=(f.r)*p) &
g is continuous
proof let X be non empty TopSpace, n be Nat,
p be Point of TOP-REAL n,
f be map of X,R^1;
assume A1: f is continuous;
defpred P[set,set] means $2=(f.$1)*p;
A2: for x being Element of X
ex y being Element of TOP-REAL n st P[x,y];
ex g being Function of the carrier of X,the carrier of TOP-REAL n st
for x being Element of X holds P[x,g.x]
from FuncExD(A2);
then consider g being Function of the carrier of X,the carrier of TOP-REAL n
such that
A3: for x being Element of X holds P[x,g.x];
reconsider g as map of X,TOP-REAL n ;
for r0 being Point of X,V being Subset of TOP-REAL n
st g.r0 in V & V is open holds
ex W being Subset of X st r0 in W & W is open & g.:W c= V
proof let r0 be Point of X,V be Subset of TOP-REAL n;
assume A4: g.r0 in V & V is open;
then A5: g.r0 in Int V by TOPS_1:55;
reconsider u=g.r0 as Point of Euclid n by TOPREAL3:13;
consider s being real number such that
A6: s>0 & Ball(u,s) c= V by A5,GOBOARD6:8;
now per cases;
case p <> 0.REAL n;
then A7: |.p.| <> 0 by TOPRNS_1:25;
A8: |.p.| >=0 by TOPRNS_1:26;
set r2=s/|.p.|;
reconsider G1=].f.r0-r2,f.r0+r2.[ as Subset of R^1
by TOPMETR:24;
r2>0 by A6,A7,A8,SEQ_2:6;
then A9: f.r0<f.r0+r2 by REAL_1:69;
then f.r0-r2<f.r0 by REAL_1:84;
then A10:f.r0 in G1 by A9,JORDAN6:45;
G1 is open by JORDAN6:46;
then consider W2 being Subset of X such that
A11: r0 in W2 & W2 is open & f.:W2 c= G1 by A1,A10,JGRAPH_2:20;
g.:W2 c= V
proof let y be set;assume y in g.:W2;
then consider r being set such that
A12: r in dom g & r in W2 & y=g.r by FUNCT_1:def 12;
reconsider r as Point of X by A12;
dom f=the carrier of X by FUNCT_2:def 1;
then f.r in f.:W2 by A12,FUNCT_1:def 12;
then A13: abs(f.r - f.r0) <r2 by A11,RCOMP_1:8;
reconsider t=f.r,t0=f.r0 as Real by XREAL_0:def 1;
A14: abs(t0 - t)=abs(t-t0) by UNIFORM1:13;
reconsider v=g.r as Point of Euclid n by TOPREAL3:13;
g.r0=(f.r0)*p by A3;
then A15: |.g.r0 -g.r.| = |.(f.r0)*p -(f.r)*p.| by A3
.= |.((f.r0)-(f.r))*p.| by EUCLID:54
.=abs(t0-t)*|.p.| by TOPRNS_1:8;
abs(f.r - f.r0)*|.p.| < r2*|.p.| by A7,A8,A13,REAL_1:70;
then |.g.r0 -g.r .|<s by A7,A14,A15,XCMPLX_1:88;
then dist(u,v)<s by JGRAPH_1:45;
then g.r in Ball(u,s) by METRIC_1:12;
hence y in V by A6,A12;
end;
hence ex W being Subset of X st r0 in W & W is open
& g.:W c= V by A11;
case A16: p =0.REAL n;
A17: for r being Point of X holds g.r=0.REAL n
proof let r be Point of X;
thus g.r=(f.r)*p by A3 .=0.REAL n by A16,EUCLID:32;
end;
then A18: 0.REAL n in V by A4;
set W2=[#]X;
r0 in the carrier of X;
then A19: r0 in W2 by PRE_TOPC:12;
g.:W2 c= V
proof let y be set;assume y in g.:W2;
then consider x being set such that
A20: x in dom g & x in W2 & y=g.x by FUNCT_1:def 12;
thus y in V by A17,A18,A20;
end;
hence ex W being Subset of X st r0 in W & W is open
& g.:W c= V by A19;
end;
hence ex W being Subset of X st r0 in W & W is open
& g.:W c= V;
end;
then g is continuous by JGRAPH_2:20;
hence thesis by A3;
end;
theorem Th18: Sq_Circ.(|[-1,0]|)= |[-1,0]|
proof
set p= |[-1,0]|;
A1: p`1=-1 & p`2=0 by EUCLID:56;
then A2: p<>0.REAL 2 by EUCLID:56,58;
p`2>=p`1 & p`2<=-p`1 by A1;
then Sq_Circ.p= |[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|
by A2,JGRAPH_3:def 1;
hence thesis by A1,SQUARE_1:60,83;
end;
theorem for P being compact non empty Subset of TOP-REAL 2
st P={p where p is Point of TOP-REAL 2: |.p.|=1}
holds Sq_Circ.(|[-1,0]|)=W-min(P) by Th18,JGRAPH_5:32;
theorem Th20: for X being non empty TopSpace, n being Nat,
g1,g2 being map of X,TOP-REAL n st
g1 is continuous & g2 is continuous
ex g being map of X,TOP-REAL n st
(for r being Point of X holds g.r=g1.r + g2.r) &
g is continuous
proof let X being non empty TopSpace,n be Nat, g1,g2 be map of X,TOP-REAL n;
assume A1: g1 is continuous & g2 is continuous;
defpred P[set,set] means
(for r1,r2 being Element of TOP-REAL n
st g1.$1=r1 & g2.$1=r2 holds $2=r1+r2);
A2:for x being Element of X
ex y being Element of TOP-REAL n
st P[x,y]
proof let x be Element of X;
set rr1=g1.x;
set rr2=g2.x;
set r3=rr1+rr2;
for s1,s2 being Point of TOP-REAL n st g1.x=s1 & g2.x=s2
holds r3=s1+s2;
hence thesis;
end;
ex f being Function of the carrier of X,the carrier of TOP-REAL n
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,the carrier of TOP-REAL n
such that A3: for x being Element of X holds
(for r1,r2 being Element of TOP-REAL n
st g1.x=r1 & g2.x=r2 holds f.x=r1+r2);
reconsider g0=f as map of X,TOP-REAL n ;
A4: for r being Point of X holds g0.r=g1.r + g2.r by A3;
for p being Point of X,V being Subset of TOP-REAL n
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 TOP-REAL n;
assume g0.p in V & V is open;
then A5: g0.p in Int V by TOPS_1:55;
reconsider r=g0.p as Point of Euclid n by TOPREAL3:13;
consider r0 being real number such that
A6: r0>0 & Ball(r,r0) c= V by A5,GOBOARD6:8;
reconsider r01=g1.p as Point of Euclid n by TOPREAL3:13;
A7: the carrier of Euclid n=the carrier of TOP-REAL n
by TOPREAL3:13;
then reconsider G1=Ball(r01,r0/2) as Subset of TOP-REAL n
;
A8: r0/2>0 by A6,SEQ_2:3;
then A9:g1.p in G1 by GOBOARD6:4;
TOP-REAL n=TopSpaceMetr(Euclid n) by EUCLID:def 8;
then G1 is open by TOPMETR:21;
then consider W1 being Subset of X such that
A10: p in W1 & W1 is open & g1.:W1 c= G1 by A1,A9,JGRAPH_2:20;
reconsider r02=g2.p as Point of Euclid n by TOPREAL3:13;
reconsider G2=Ball(r02,r0/2) as Subset of TOP-REAL n
by A7;
A11:g2.p in G2 by A8,GOBOARD6:4;
TOP-REAL n=TopSpaceMetr(Euclid n) by EUCLID:def 8;
then G2 is open by TOPMETR:21;
then consider W2 being Subset of X such that
A12: p in W2 & W2 is open & g2.:W2 c= G2 by A1,A11,JGRAPH_2:20;
set W=W1 /\ W2;
A13:W is open by A10,A12,TOPS_1:38;
A14:p in W by A10,A12,XBOOLE_0:def 3;
g0.:W c= Ball(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;
dom g1=the carrier of X by FUNCT_2:def 1;
then A17: g1.pz in g1.:W1 by A16,FUNCT_1:def 12;
reconsider aa1=g1.pz as Point of TOP-REAL n;
reconsider bb1=aa1 as Point of Euclid n by TOPREAL3:13;
dist(r01,bb1)<r0/2 by A10,A17,METRIC_1:12;
then A18: |.g1.p - g1.pz .|<r0/2 by JGRAPH_1:45;
A19:z in W2 by A15,XBOOLE_0:def 3;
dom g2=the carrier of X by FUNCT_2:def 1;
then A20: g2.pz in g2.:W2 by A19,FUNCT_1:def 12;
reconsider aa2=g2.pz as Point of TOP-REAL n;
reconsider bb2=aa2 as Point of Euclid n by TOPREAL3:13;
dist(r02,bb2)<r0/2 by A12,A20,METRIC_1:12;
then A21: |.g2.p - g2.pz .|<r0/2 by JGRAPH_1:45;
A22: aa1+aa2=x by A3,A15;
reconsider bb0=aa1+aa2 as Point of Euclid n by TOPREAL3:13;
A23: g0.pz= g1.pz+g2.pz by A3;
(g1.p +g2.p)-(g1.pz+g2.pz)=g1.p+g2.p-g1.pz-g2.pz by EUCLID:50
.= g1.p+g2.p+-g1.pz-g2.pz by EUCLID:45
.= g1.p+g2.p+-g1.pz+-g2.pz by EUCLID:45
.= g1.p+-g1.pz+g2.p+-g2.pz by EUCLID:30
.= g1.p+-g1.pz+(g2.p+-g2.pz) by EUCLID:30
.= g1.p-g1.pz+(g2.p+-g2.pz) by EUCLID:45
.= g1.p-g1.pz+(g2.p-g2.pz) by EUCLID:45;
then A24: |.(g1.p +g2.p)-(g1.pz+g2.pz).|
<= |.g1.p-g1.pz.| + |.g2.p-g2.pz.| by TOPRNS_1:30;
|.g1.p-g1.pz.| + |.g2.p-g2.pz.| < r0/2 +r0/2
by A18,A21,REAL_1:67;
then |.g1.p-g1.pz.| + |.g2.p-g2.pz.| < r0 by XCMPLX_1:66;
then |.(g1.p +g2.p)-(g1.pz+g2.pz).|<r0 by A24,AXIOMS:22;
then |.g0.p - g0.pz .|<r0 by A3,A23;
then dist(r,bb0)<r0 by A15,A22,JGRAPH_1:45;
hence x in Ball(r,r0) by A22,METRIC_1:12;
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 JGRAPH_2:20;
hence thesis by A4;
end;
theorem Th21: for X being non empty TopSpace, n being Nat,
p1,p2 being Point of TOP-REAL n,
f1,f2 being map of X,R^1 st
f1 is continuous & f2 is continuous
ex g being map of X,TOP-REAL n st
(for r being Point of X holds g.r=(f1.r)*p1+(f2.r)*p2) &
g is continuous
proof let X be non empty TopSpace, n be Nat,
p1,p2 be Point of TOP-REAL n,
f1,f2 be map of X,R^1;
assume A1: f1 is continuous & f2 is continuous;
then consider g1 being map of X,TOP-REAL n such that
A2: (for r being Point of X holds g1.r=(f1.r)*p1) &
g1 is continuous by Th17;
consider g2 being map of X,TOP-REAL n such that
A3: (for r being Point of X holds g2.r=(f2.r)*p2) &
g2 is continuous by A1,Th17;
consider g being map of X,TOP-REAL n such that
A4: (for r being Point of X holds g.r=g1.r + g2.r) &
g is continuous by A2,A3,Th20;
(for r being Point of X holds g.r=(f1.r)*p1+(f2.r)*p2)
proof let r be Point of X;
g.r=g1.r+g2.r by A4;
then g.r=g1.r+(f2.r)*p2 by A3;
hence g.r=(f1.r)*p1+(f2.r)*p2 by A2;
end;
hence thesis by A4;
end;
theorem Th22:
for f being Function,A being set st f is one-to-one & A c= dom f
holds f".:(f.:A)=A
proof let f be Function,A be set;
set B = f.:A;
assume A1: f is one-to-one & A c= dom f;
A2: f".:B c= A
proof let y be set;assume y in f".:B;
then consider x being set such that
A3: x in dom (f") & x in B & y=f".x by FUNCT_1:def 12;
consider y2 being set such that
A4: y2 in dom f & y2 in A & x=f.y2 by A3,FUNCT_1:def 12;
thus y in A by A1,A3,A4,FUNCT_1:54;
end;
A c= f".:B
proof let x be set;assume
A5: x in A;
set y0=f.x;
A6: f".y0=x by A1,A5,FUNCT_1:56;
y0 in rng f by A1,A5,FUNCT_1:12;
then A7: y0 in dom (f") by A1,FUNCT_1:55;
y0 in B by A1,A5,FUNCT_1:def 12;
hence x in f".:B by A6,A7,FUNCT_1:def 12;
end;
hence f".:B=A by A2,XBOOLE_0:def 10;
end;
begin :: General Fashoda Theorem for Unit Circle
Lm5: (|[-1,0]|)`1 =-1 & (|[-1,0]|)`2=0 & (|[1,0]|)`1 =1 & (|[1,0]|)`2=0 &
(|[0,-1]|)`1 =0 & (|[0,-1]|)`2=-1 & (|[0,1]|)`1 =0 & (|[0,1]|)`2=1
by EUCLID:56;
Lm6: now thus |.(|[-1,0]|).|=sqrt((-1)^2+0^2) by Lm5,JGRAPH_3:10
.=1 by SQUARE_1:59,60,61,83;
thus |.(|[1,0]|).|=sqrt(1^2+0^2) by Lm5,JGRAPH_3:10
.=1 by SQUARE_1:59,60,83;
thus |.(|[0,-1]|).|=sqrt(0^2+(-1)^2) by Lm5,JGRAPH_3:10
.=1 by SQUARE_1:59,60,61,83;
thus |.(|[0,1]|).|=sqrt(0^2+1^2) by Lm5,JGRAPH_3:10
.=1 by SQUARE_1:59,60,83;
end;
Lm7: 0 in [.0,1.] by TOPREAL5:1;
Lm8: 1 in [.0,1.] by TOPREAL5:1;
reserve p,p1,p2,p3,q,q1,q2 for Point of TOP-REAL 2,i,j for Nat,
r,lambda for Real;
theorem Th23: for f,g being map of I[01],TOP-REAL 2,
C0,KXP,KXN,KYP,KYN being Subset of TOP-REAL 2,
O,I being Point of I[01] st O=0 & I=1 &
f is continuous one-to-one &
g is continuous one-to-one &
C0={p: |.p.|<=1}&
KXP={q1 where q1 is Point of TOP-REAL 2:
|.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} &
KXN={q2 where q2 is Point of TOP-REAL 2:
|.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} &
KYP={q3 where q3 is Point of TOP-REAL 2:
|.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} &
KYN={q4 where q4 is Point of TOP-REAL 2:
|.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} &
f.O in KXP & f.I in KXN &
g.O in KYP & g.I in KYN &
rng f c= C0 & rng g c= C0
holds rng f meets rng g
proof let f,g be map of I[01],TOP-REAL 2,
C0,KXP,KXN,KYP,KYN be Subset of TOP-REAL 2,
O,I be Point of I[01];
assume A1: O=0 & I=1 &
f is continuous & f is one-to-one &
g is continuous & g is one-to-one &
C0={p: |.p.|<=1}&
KXP={q1 where q1 is Point of TOP-REAL 2:
|.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} &
KXN={q2 where q2 is Point of TOP-REAL 2:
|.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} &
KYP={q3 where q3 is Point of TOP-REAL 2:
|.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} &
KYN={q4 where q4 is Point of TOP-REAL 2:
|.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} &
f.O in KXP & f.I in KXN &
g.O in KYP & g.I in KYN &
rng f c= C0 & rng g c= C0;
then consider f2 being map of I[01],TOP-REAL 2 such that
A2: f2.0=f.1 & f2.1=f.0 &
rng f2=rng f & f2 is continuous & f2 is one-to-one by JGRAPH_5:15;
thus rng f meets rng g by A1,A2,JGRAPH_5:16;
end;
theorem Th24: for f,g being map of I[01],TOP-REAL 2,
C0,KXP,KXN,KYP,KYN being Subset of TOP-REAL 2,
O,I being Point of I[01] st O=0 & I=1 &
f is continuous & f is one-to-one &
g is continuous & g is one-to-one &
C0={p: |.p.|<=1}&
KXP={q1 where q1 is Point of TOP-REAL 2:
|.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} &
KXN={q2 where q2 is Point of TOP-REAL 2:
|.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} &
KYP={q3 where q3 is Point of TOP-REAL 2:
|.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} &
KYN={q4 where q4 is Point of TOP-REAL 2:
|.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} &
f.O in KXP & f.I in KXN &
g.O in KYN & g.I in KYP &
rng f c= C0 & rng g c= C0
holds rng f meets rng g
proof let f,g be map of I[01],TOP-REAL 2,
C0,KXP,KXN,KYP,KYN be Subset of TOP-REAL 2,
O,I be Point of I[01];
assume A1: O=0 & I=1 &
f is continuous & f is one-to-one &
g is continuous & g is one-to-one &
C0={p: |.p.|<=1}&
KXP={q1 where q1 is Point of TOP-REAL 2:
|.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} &
KXN={q2 where q2 is Point of TOP-REAL 2:
|.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} &
KYP={q3 where q3 is Point of TOP-REAL 2:
|.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} &
KYN={q4 where q4 is Point of TOP-REAL 2:
|.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} &
f.O in KXP & f.I in KXN &
g.O in KYN & g.I in KYP &
rng f c= C0 & rng g c= C0;
then consider g2 being map of I[01],TOP-REAL 2 such that
A2: g2.0=g.1 & g2.1=g.0 &
rng g2=rng g & g2 is continuous & g2 is one-to-one by JGRAPH_5:15;
thus rng f meets rng g by A1,A2,Th23;
end;
theorem Th25:
for p1,p2,p3,p4 being Point of TOP-REAL 2,
P being compact non empty Subset of TOP-REAL 2,C0 being Subset of TOP-REAL 2
st P={p where p is Point of TOP-REAL 2: |.p.|=1}
& LE p1,p2,P & LE p2,p3,P & LE p3,p4,P
holds
(for f,g being map of I[01],TOP-REAL 2 st
f is continuous one-to-one & g is continuous one-to-one &
C0={p8 where p8 is Point of TOP-REAL 2: |.p8.|<=1}&
f.0=p3 & f.1=p1 & g.0=p2 & g.1=p4 &
rng f c= C0 & rng g c= C0 holds rng f meets rng g)
proof let p1,p2,p3,p4 be Point of TOP-REAL 2,
P be compact non empty Subset of TOP-REAL 2,C0 be Subset of TOP-REAL 2;
assume A1: P={p where p is Point of TOP-REAL 2: |.p.|=1}
& LE p1,p2,P & LE p2,p3,P & LE p3,p4,P;
let f,g be map of I[01],TOP-REAL 2;
assume A2:f is continuous one-to-one & g is continuous one-to-one &
C0={p8 where p8 is Point of TOP-REAL 2: |.p8.|<=1}&
f.0=p3 & f.1=p1 & g.0=p2 & g.1=p4 &
rng f c= C0 & rng g c= C0;
A3: dom f=the carrier of I[01] by FUNCT_2:def 1;
A4: dom g=the carrier of I[01] by FUNCT_2:def 1;
per cases;
suppose A5: not (p1<>p2 & p2<>p3 & p3<>p4);
now per cases by A5;
case A6: p1=p2;
thus rng f meets rng g
proof
A7: p1 in rng f by A2,A3,Lm8,BORSUK_1:83,FUNCT_1:def 5;
p2 in rng g by A2,A4,Lm7,BORSUK_1:83,FUNCT_1:def 5;
hence thesis by A6,A7,XBOOLE_0:3;
end;
case A8: p2=p3;
thus rng f meets rng g
proof
A9: p3 in rng f by A2,A3,Lm7,BORSUK_1:83,FUNCT_1:def 5;
p2 in rng g by A2,A4,Lm7,BORSUK_1:83,FUNCT_1:def 5;
hence thesis by A8,A9,XBOOLE_0:3;
end;
case A10: p3=p4;
thus rng f meets rng g
proof
A11: p3 in rng f by A2,A3,Lm7,BORSUK_1:83,FUNCT_1:def 5;
p4 in rng g by A2,A4,Lm8,BORSUK_1:83,FUNCT_1:def 5;
hence thesis by A10,A11,XBOOLE_0:3;
end;
end;
hence thesis;
suppose p1<>p2 & p2<>p3 & p3<>p4;
then consider h being map of TOP-REAL 2,TOP-REAL 2 such that
A12: h is_homeomorphism &
(for q being Point of TOP-REAL 2 holds |.(h.q).|=|.q.|)&
|[-1,0]|=h.p1 & |[0,1]|=h.p2 & |[1,0]|=h.p3 & |[0,-1]|=h.p4
by A1,JGRAPH_5:70;
A13: h is one-to-one by A12,TOPS_2:def 5;
reconsider f2=h*f as map of I[01],TOP-REAL 2;
reconsider g2=h*g as map of I[01],TOP-REAL 2;
A14: dom f2=the carrier of I[01] by FUNCT_2:def 1;
A15: dom g2=the carrier of I[01] by FUNCT_2:def 1;
A16: f2.1= |[-1,0]| by A2,A12,A14,Lm8,BORSUK_1:83,FUNCT_1:22;
A17: g2.1= |[0,-1]| by A2,A12,A15,Lm8,BORSUK_1:83,FUNCT_1:22;
A18: f2.0= |[1,0]| by A2,A12,A14,Lm7,BORSUK_1:83,FUNCT_1:22;
A19: g2.0= |[0,1]| by A2,A12,A15,Lm7,BORSUK_1:83,FUNCT_1:22;
A20: f2 is continuous one-to-one &
g2 is continuous one-to-one &
f2.1=|[-1,0]| & f2.0=|[1,0]| & g2.1=|[0,-1]| & g2.0= |[0,1]|
by A2,A12,A14,A15,Lm7,Lm8,BORSUK_1:83,FUNCT_1:22,
JGRAPH_5:8,9;
A21: rng f2 c= C0
proof let y be set;assume y in rng f2;
then consider x being set such that
A22: x in dom f2 & y=f2.x by FUNCT_1:def 5;
A23: f2.x=h.(f.x) by A22,FUNCT_1:22;
A24: f.x in rng f by A3,A14,A22,FUNCT_1:def 5;
then A25: f.x in C0 by A2;
reconsider qf=f.x as Point of TOP-REAL 2 by A24;
consider q5 being Point of TOP-REAL 2 such that
A26: q5=f.x & |.q5.|<=1 by A2,A25;
|.(h.qf).|=|.qf.| by A12;
hence y in C0 by A2,A22,A23,A26;
end;
A27: rng g2 c= C0
proof let y be set;assume y in rng g2;
then consider x being set such that
A28: x in dom g2 & y=g2.x by FUNCT_1:def 5;
A29: g2.x=h.(g.x) by A28,FUNCT_1:22;
A30: g.x in rng g by A4,A15,A28,FUNCT_1:def 5;
then A31: g.x in C0 by A2;
reconsider qg=g.x as Point of TOP-REAL 2 by A30;
consider q5 being Point of TOP-REAL 2 such that
A32: q5=g.x & |.q5.|<=1 by A2,A31;
|.(h.qg).|=|.qg.| by A12;
hence y in C0 by A2,A28,A29,A32;
end;
defpred Q[Point of TOP-REAL 2] means
|.$1.|=1 & $1`2<=$1`1 & $1`2>=-$1`1;
{q1 where q1 is Point of TOP-REAL 2:Q[q1]} is
Subset of TOP-REAL 2 from TopSubset;
then reconsider KXP={q1 where q1 is Point of TOP-REAL 2:
|.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} as Subset of TOP-REAL 2;
defpred Q[Point of TOP-REAL 2] means
|.$1.|=1 & $1`2>=$1`1 & $1`2<=-$1`1;
{q2 where q2 is Point of TOP-REAL 2:Q[q2]} is
Subset of TOP-REAL 2 from TopSubset;
then reconsider KXN={q2 where q2 is Point of TOP-REAL 2:
|.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} as Subset of TOP-REAL 2;
defpred Q[Point of TOP-REAL 2] means
|.$1.|=1 & $1`2>=$1`1 & $1`2>=-$1`1;
{q3 where q3 is Point of TOP-REAL 2:Q[q3]} is
Subset of TOP-REAL 2 from TopSubset;
then reconsider KYP={q3 where q3 is Point of TOP-REAL 2:
|.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} as Subset of TOP-REAL 2;
defpred Q[Point of TOP-REAL 2] means
|.$1.|=1 & $1`2<=$1`1 & $1`2<=-$1`1;
{q4 where q4 is Point of TOP-REAL 2:Q[q4]} is
Subset of TOP-REAL 2 from TopSubset;
then reconsider KYN={q4 where q4 is Point of TOP-REAL 2:
|.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} as Subset of TOP-REAL 2;
reconsider O=0,I=1 as Point of I[01] by BORSUK_1:83,TOPREAL5:1;
-(|[-1,0]|)`1=1 by Lm5;
then A33: f2.I in KXN by A16,Lm5,Lm6;
A34: f2.O in KXP by A18,Lm5,Lm6;
-(|[0,-1]|)`1= 0 by Lm5;
then A35: g2.I in KYN by A17,Lm5,Lm6;
-(|[0,1]|)`1= 0 by Lm5;
then g2.O in KYP by A19,Lm5,Lm6;
then rng f2 meets rng g2 by A2,A20,A21,A27,A33,A34,A35,Th23;
then consider x2 being set such that
A36: x2 in rng f2 & x2 in rng g2 by XBOOLE_0:3;
consider z2 being set such that
A37: z2 in dom f2 & x2=f2.z2 by A36,FUNCT_1:def 5;
consider z3 being set such that
A38: z3 in dom g2 & x2=g2.z3 by A36,FUNCT_1:def 5;
A39: dom h=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
A40: g.z3 in rng g by A4,A15,A38,FUNCT_1:def 5;
A41: f.z2 in rng f by A3,A14,A37,FUNCT_1:def 5;
reconsider h1=h as Function;
A42: h1".x2=h1".(h.(f.z2)) by A37,FUNCT_1:22 .=f.z2
by A13,A39,A41,FUNCT_1:56;
h1".x2=h1".(h.(g.z3)) by A38,FUNCT_1:22 .=g.z3
by A13,A39,A40,FUNCT_1:56;
then h1".x2 in rng f & h1".x2 in rng g by A3,A4,A14,A15,A37,A38,A42,FUNCT_1
:def 5;
hence thesis by XBOOLE_0:3;
end;
theorem Th26:
for p1,p2,p3,p4 being Point of TOP-REAL 2,
P being compact non empty Subset of TOP-REAL 2,C0 being Subset of TOP-REAL 2
st P={p where p is Point of TOP-REAL 2: |.p.|=1}
& LE p1,p2,P & LE p2,p3,P & LE p3,p4,P
holds
(for f,g being map of I[01],TOP-REAL 2 st
f is continuous one-to-one & g is continuous one-to-one &
C0={p8 where p8 is Point of TOP-REAL 2: |.p8.|<=1}&
f.0=p3 & f.1=p1 & g.0=p4 & g.1=p2 &
rng f c= C0 & rng g c= C0 holds rng f meets rng g)
proof let p1,p2,p3,p4 be Point of TOP-REAL 2,
P be compact non empty Subset of TOP-REAL 2,C0 be Subset of TOP-REAL 2;
assume A1: P={p where p is Point of TOP-REAL 2: |.p.|=1}
& LE p1,p2,P & LE p2,p3,P & LE p3,p4,P;
let f,g be map of I[01],TOP-REAL 2;
assume A2:f is continuous one-to-one & g is continuous one-to-one &
C0={p8 where p8 is Point of TOP-REAL 2: |.p8.|<=1}&
f.0=p3 & f.1=p1 & g.0=p4 & g.1=p2 &
rng f c= C0 & rng g c= C0;
A3: dom f=the carrier of I[01] by FUNCT_2:def 1;
A4: dom g=the carrier of I[01] by FUNCT_2:def 1;
per cases;
suppose A5: not (p1<>p2 & p2<>p3 & p3<>p4);
now per cases by A5;
case A6: p1=p2;
thus rng f meets rng g
proof
A7: p1 in rng f by A2,A3,Lm8,BORSUK_1:83,FUNCT_1:def 5;
p2 in rng g by A2,A4,Lm8,BORSUK_1:83,FUNCT_1:def 5;
hence thesis by A6,A7,XBOOLE_0:3;
end;
case A8: p2=p3;
thus rng f meets rng g
proof
A9: p3 in rng f by A2,A3,Lm7,BORSUK_1:83,FUNCT_1:def 5;
p2 in rng g by A2,A4,Lm8,BORSUK_1:83,FUNCT_1:def 5;
hence thesis by A8,A9,XBOOLE_0:3;
end;
case A10: p3=p4;
thus rng f meets rng g
proof
A11: p3 in rng f by A2,A3,Lm7,BORSUK_1:83,FUNCT_1:def 5;
p4 in rng g by A2,A4,Lm7,BORSUK_1:83,FUNCT_1:def 5;
hence thesis by A10,A11,XBOOLE_0:3;
end;
end;
hence thesis;
suppose p1<>p2 & p2<>p3 & p3<>p4;
then consider h being map of TOP-REAL 2,TOP-REAL 2 such that
A12: h is_homeomorphism &
(for q being Point of TOP-REAL 2 holds |.(h.q).|=|.q.|)&
|[-1,0]|=h.p1 & |[0,1]|=h.p2 & |[1,0]|=h.p3 & |[0,-1]|=h.p4
by A1,JGRAPH_5:70;
A13: h is one-to-one by A12,TOPS_2:def 5;
reconsider f2=h*f as map of I[01],TOP-REAL 2;
reconsider g2=h*g as map of I[01],TOP-REAL 2;
A14: dom f2=the carrier of I[01] by FUNCT_2:def 1;
A15: dom g2=the carrier of I[01] by FUNCT_2:def 1;
A16: f2.1= |[-1,0]| by A2,A12,A14,Lm8,BORSUK_1:83,FUNCT_1:22;
A17: g2.1= |[0,1]| by A2,A12,A15,Lm8,BORSUK_1:83,FUNCT_1:22;
A18: f2.0= |[1,0]| by A2,A12,A14,Lm7,BORSUK_1:83,FUNCT_1:22;
A19: g2.0= |[0,-1]| by A2,A12,A15,Lm7,BORSUK_1:83,FUNCT_1:22;
A20: f2 is continuous one-to-one &
g2 is continuous one-to-one &
f2.1=|[-1,0]| & f2.0=|[1,0]| & g2.1=|[0,1]| & g2.0= |[0,-1]|
by A2,A12,A14,A15,Lm7,Lm8,BORSUK_1:83,FUNCT_1:22,
JGRAPH_5:8,9;
A21: rng f2 c= C0
proof let y be set;assume y in rng f2;
then consider x being set such that
A22: x in dom f2 & y=f2.x by FUNCT_1:def 5;
A23: f2.x=h.(f.x) by A22,FUNCT_1:22;
A24: f.x in rng f by A3,A14,A22,FUNCT_1:def 5;
then A25: f.x in C0 by A2;
reconsider qf=f.x as Point of TOP-REAL 2 by A24;
consider q5 being Point of TOP-REAL 2 such that
A26: q5=f.x & |.q5.|<=1 by A2,A25;
|.(h.qf).|=|.qf.| by A12;
hence y in C0 by A2,A22,A23,A26;
end;
A27: rng g2 c= C0
proof let y be set;assume y in rng g2;
then consider x being set such that
A28: x in dom g2 & y=g2.x by FUNCT_1:def 5;
A29: g2.x=h.(g.x) by A28,FUNCT_1:22;
A30: g.x in rng g by A4,A15,A28,FUNCT_1:def 5;
then A31: g.x in C0 by A2;
reconsider qg=g.x as Point of TOP-REAL 2 by A30;
consider q5 being Point of TOP-REAL 2 such that
A32: q5=g.x & |.q5.|<=1 by A2,A31;
|.(h.qg).|=|.qg.| by A12;
hence y in C0 by A2,A28,A29,A32;
end;
defpred P[Point of TOP-REAL 2] means
|.$1.|=1 & $1`2<=$1`1 & $1`2>=-$1`1;
{q1 where q1 is Point of TOP-REAL 2:P[q1]} is
Subset of TOP-REAL 2 from TopSubset;
then reconsider KXP={q1 where q1 is Point of TOP-REAL 2:
|.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} as Subset of TOP-REAL 2;
defpred P[Point of TOP-REAL 2] means
|.$1.|=1 & $1`2>=$1`1 & $1`2<=-$1`1;
{q2 where q2 is Point of TOP-REAL 2:P[q2]} is
Subset of TOP-REAL 2 from TopSubset;
then reconsider KXN={q2 where q2 is Point of TOP-REAL 2:
|.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} as Subset of TOP-REAL 2;
defpred P[Point of TOP-REAL 2] means
|.$1.|=1 & $1`2>=$1`1 & $1`2>=-$1`1;
{q3 where q3 is Point of TOP-REAL 2:P[q3]} is
Subset of TOP-REAL 2 from TopSubset;
then reconsider KYP={q3 where q3 is Point of TOP-REAL 2:
|.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} as Subset of TOP-REAL 2;
defpred P[Point of TOP-REAL 2] means
|.$1.|=1 & $1`2<=$1`1 & $1`2<=-$1`1;
{q4 where q4 is Point of TOP-REAL 2:P[q4]} is
Subset of TOP-REAL 2 from TopSubset;
then reconsider KYN={q4 where q4 is Point of TOP-REAL 2:
|.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} as Subset of TOP-REAL 2;
reconsider O=0,I=1 as Point of I[01] by BORSUK_1:83,TOPREAL5:1;
-(|[-1,0]|)`1=1 by Lm5;
then A33: f2.I in KXN by A16,Lm5,Lm6;
A34: f2.O in KXP by A18,Lm5,Lm6;
-(|[0,-1]|)`1= 0 by Lm5;
then A35: g2.I in KYP by A17,Lm5,Lm6;
-(|[0,1]|)`1= 0 by Lm5;
then g2.O in KYN by A19,Lm5,Lm6;
then rng f2 meets rng g2 by A2,A20,A21,A27,A33,A34,A35,Th24;
then consider x2 being set such that
A36: x2 in rng f2 & x2 in rng g2 by XBOOLE_0:3;
consider z2 being set such that
A37: z2 in dom f2 & x2=f2.z2 by A36,FUNCT_1:def 5;
consider z3 being set such that
A38: z3 in dom g2 & x2=g2.z3 by A36,FUNCT_1:def 5;
A39: dom h=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
A40: g.z3 in rng g by A4,A15,A38,FUNCT_1:def 5;
A41: f.z2 in rng f by A3,A14,A37,FUNCT_1:def 5;
reconsider h1=h as Function;
A42: h1".x2=h1".(h.(f.z2)) by A37,FUNCT_1:22 .=f.z2
by A13,A39,A41,FUNCT_1:56;
h1".x2=h1".(h.(g.z3)) by A38,FUNCT_1:22 .=g.z3
by A13,A39,A40,FUNCT_1:56;
then h1".x2 in rng f & h1".x2 in rng g by A3,A4,A14,A15,A37,A38,A42,FUNCT_1
:def 5;
hence thesis by XBOOLE_0:3;
end;
theorem Th27:
for p1,p2,p3,p4 being Point of TOP-REAL 2,
P being compact non empty Subset of TOP-REAL 2,
C0 being Subset of TOP-REAL 2 st
P={p where p is Point of TOP-REAL 2: |.p.|=1} &
p1,p2,p3,p4 are_in_this_order_on P holds
(for f,g being map of I[01],TOP-REAL 2 st
f is continuous one-to-one & g is continuous one-to-one &
C0={p8 where p8 is Point of TOP-REAL 2: |.p8.|<=1}&
f.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 &
rng f c= C0 & rng g c= C0 holds rng f meets rng g)
proof let p1,p2,p3,p4 be Point of TOP-REAL 2,
P be compact non empty Subset of TOP-REAL 2,C0 be Subset of TOP-REAL 2;
assume A1: P={p where p is Point of TOP-REAL 2: |.p.|=1}
& p1,p2,p3,p4 are_in_this_order_on P;
per cases by A1,JORDAN17:def 1;
suppose LE p1,p2,P & LE p2,p3,P & LE p3,p4,P;
hence thesis by A1,JGRAPH_5:71;
suppose LE p2,p3,P & LE p3,p4,P & LE p4,p1,P;
hence thesis by A1,JGRAPH_5:72;
suppose LE p3,p4,P & LE p4,p1,P & LE p1,p2,P;
hence thesis by A1,Th26;
suppose LE p4,p1,P & LE p1,p2,P & LE p2,p3,P;
hence thesis by A1,Th25;
end;
begin :: General Rectangles and Circles
definition let a,b,c,d be real number;
func rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals :Def1:
{p: p`1=a & c <=p`2 & p`2<=d or p`2=d & a<=p`1 & p`1<=b or
p`1=b & c <=p`2 & p`2<=d or p`2=c & a<=p`1 & p`1<=b};
coherence
proof
defpred P[Point of TOP-REAL 2] means
$1`1=a & c <=$1`2 & $1`2<=d or $1`2=d & a<=$1`1 & $1`1<=b or
$1`1=b & c <=$1`2 & $1`2<=d or $1`2=c & a<=$1`1 & $1`1<=b;
{p: P[p]}
c= the carrier of TOP-REAL 2 from Fr_Set0;
hence thesis;
end;
end;
theorem Th28: for a,b,c,d being real number, p being Point of TOP-REAL 2
st a<=b & c <=d & p in rectangle(a,b,c,d) holds
a<=p`1 & p`1<=b & c <=p`2 & p`2<=d
proof let a,b,c,d be real number, p be Point of TOP-REAL 2;
assume A1: a<=b & c <=d & p in rectangle(a,b,c,d);
then p in {p2: p2`1=a & c <=p2`2 & p2`2<=d or p2`2=d & a<=p2`1 & p2`1<=b or
p2`1=b & c <=p2`2 & p2`2<=d or p2`2=c & a<=p2`1 & p2`1<=b} by Def1;
then consider p2 such that
A2: p2=p &
(p2`1=a & c <=p2`2 & p2`2<=d or p2`2=d & a<=p2`1 & p2`1<=b or
p2`1=b & c <=p2`2 & p2`2<=d or p2`2=c & a<=p2`1 & p2`1<=b);
per cases by A2;
suppose p`1=a & c <=p`2 & p`2<=d;
hence thesis by A1;
suppose p`2=d & a<=p`1 & p`1<=b;
hence thesis by A1;
suppose p`1=b & c <=p`2 & p`2<=d;
hence thesis by A1;
suppose p`2=c & a<=p`1 & p`1<=b;
hence thesis by A1;
end;
definition let a,b,c,d be real number;
func inside_of_rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals :Def2:
{p: a <p`1 & p`1< b & c <p`2 & p`2< d};
coherence
proof
defpred P[Point of TOP-REAL 2] means
a <$1`1 & $1`1< b & c <$1`2 & $1`2< d;
{p: P[p]}
c= the carrier of TOP-REAL 2 from Fr_Set0;
hence thesis;
end;
end;
definition let a,b,c,d be real number;
func closed_inside_of_rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals
:Def3:
{p: a <=p`1 & p`1<= b & c <=p`2 & p`2<= d};
coherence
proof
defpred P[Point of TOP-REAL 2] means
a <=$1`1 & $1`1<= b & c <=$1`2 & $1`2<= d;
{p: P[p]}
c= the carrier of TOP-REAL 2 from Fr_Set0;
hence thesis;
end;
end;
definition let a,b,c,d be real number;
func outside_of_rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals
:Def4:
{p: not(a <=p`1 & p`1<= b & c <=p`2 & p`2<= d)};
coherence
proof
defpred P[Point of TOP-REAL 2] means
not(a <=$1`1 & $1`1<= b & c <=$1`2 & $1`2<= d);
{p: P[p] }
c= the carrier of TOP-REAL 2 from Fr_Set0;
hence thesis;
end;
end;
definition let a,b,c,d be real number;
func closed_outside_of_rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals
:Def5:
{p: not(a <p`1 & p`1< b & c <p`2 & p`2< d)};
coherence
proof
defpred P[Point of TOP-REAL 2] means
not(a <$1`1 & $1`1< b & c <$1`2 & $1`2< d);
{p: P[p] }
c= the carrier of TOP-REAL 2 from Fr_Set0;
hence thesis;
end;
end;
theorem Th29:
for a,b,r being real number,Kb,Cb being Subset of TOP-REAL 2 st
r>=0 & Kb={q: |.q.|=1}&
Cb={p2 where p2 is Point of TOP-REAL 2: |.(p2- |[a,b]|).|=r} holds
AffineMap(r,a,r,b).:Kb=Cb
proof let a,b,r be real number,Kb,Cb be Subset of TOP-REAL 2;
assume A1: r>=0 & Kb={q: |.q.|=1}&
Cb={p2 where p2 is Point of TOP-REAL 2: |.(p2- |[a,b]|).|=r};
reconsider rr=r as Real by XREAL_0:def 1;
A2: AffineMap(r,a,r,b).:Kb c= Cb
proof let y be set;assume y in AffineMap(r,a,r,b).:Kb;
then consider x being set such that
A3: x in dom (AffineMap(r,a,r,b)) & x in Kb &
y=(AffineMap(r,a,r,b)).x by FUNCT_1:def 12;
consider p being Point of TOP-REAL 2 such that
A4: x=p & |.p.|=1 by A1,A3;
A5: (AffineMap(r,a,r,b)).p=|[r*(p`1)+a,r*(p`2)+b]| by JGRAPH_2:def 2;
then reconsider q=y as Point of TOP-REAL 2 by A3,A4;
A6: q- |[a,b]|= |[r*(p`1)+a-a,r*(p`2)+b-b]| by A3,A4,A5,EUCLID:66
.= |[r*(p`1),r*(p`2)+b-b]| by XCMPLX_1:26
.= |[r*(p`1),r*(p`2)]| by XCMPLX_1:26
.= r*(|[(p`1),(p`2)]|) by EUCLID:62
.= r*p by EUCLID:57;
|.r*p.|=abs(rr)*(|.p.|) by TOPRNS_1:8.=r by A1,A4,ABSVALUE:def 1;
hence y in Cb by A1,A6;
end;
Cb c= AffineMap(r,a,r,b).:Kb
proof let y be set;assume y in Cb;
then consider p2 being Point of TOP-REAL 2 such that
A7: y=p2 & |.(p2- |[a,b]|).|=r by A1;
now per cases by A1;
case A8: r>0; then r" >0 by REAL_1:72;
then A9: 1/r >0 by XCMPLX_1:217;
set p1=(1/r)*(p2- |[a,b]|);
|.p1.|=abs(1/rr)*|.(p2- |[a,b]|).| by TOPRNS_1:8
.=(1/r)*r by A7,A9,ABSVALUE:def 1 .= 1 by A8,XCMPLX_1:88;
then A10: p1 in Kb by A1;
p1=|[(1/r)*(p2- |[a,b]|)`1,(1/r)*(p2- |[a,b]|)`2]| by EUCLID:61;
then A11: p1`1=(1/r)*(p2- |[a,b]|)`1 &
p1`2=(1/r)*(p2- |[a,b]|)`2 by EUCLID:56;
then A12: r*p1`1=r*(1/r)*(p2- |[a,b]|)`1 by XCMPLX_1:4
.=1*(p2- |[a,b]|)`1 by A8,XCMPLX_1:88
.=p2`1 -(|[a,b]|)`1 by TOPREAL3:8
.=p2`1 - a by EUCLID:56;
A13: r*p1`2=r*(1/r)*(p2- |[a,b]|)`2 by A11,XCMPLX_1:4
.=1*(p2- |[a,b]|)`2 by A8,XCMPLX_1:88
.=p2`2 -(|[a,b]|)`2 by TOPREAL3:8
.=p2`2 - b by EUCLID:56;
A14: (AffineMap(r,a,r,b)).p1= |[r*(p1`1)+a,r*(p1`2)+b]| by JGRAPH_2:def 2
.= |[p2`1,p2`2 -b+b]| by A12,A13,XCMPLX_1:27
.= |[p2`1,p2`2]| by XCMPLX_1:27
.=p2 by EUCLID:57;
dom (AffineMap(r,a,r,b))=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
hence y in AffineMap(r,a,r,b).:Kb by A7,A10,A14,FUNCT_1:def 12;
case A15: r=0;
set p1= |[1,0]|;
p1`1=1 & p1`2=0 by EUCLID:56;
then |.p1.|=sqrt(1^2+0) by JGRAPH_3:10,SQUARE_1:60
.=1 by SQUARE_1:89;
then A16: p1 in Kb by A1;
A17: (AffineMap(r,a,r,b)).p1= |[(0)*(p1`1)+a,(0)*(p1`2)+b]|
by A15,JGRAPH_2:def 2
.=p2 by A7,A15,TOPRNS_1:29;
dom (AffineMap(r,a,r,b))=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
hence y in AffineMap(r,a,r,b).:Kb by A7,A16,A17,FUNCT_1:def 12;
end;
hence y in AffineMap(r,a,r,b).:Kb;
end;
hence AffineMap(r,a,r,b).:Kb=Cb by A2,XBOOLE_0:def 10;
end;
theorem Th30: for P,Q being Subset of TOP-REAL 2 st
(ex f being map of (TOP-REAL 2)|P,(TOP-REAL 2)|Q st
f is_homeomorphism) & P is_simple_closed_curve holds
Q is_simple_closed_curve
proof let P,Q be Subset of TOP-REAL 2;
assume A1: (ex f being map of (TOP-REAL 2)|P,(TOP-REAL 2)|Q st
f is_homeomorphism) & P is_simple_closed_curve;
then consider f being map of (TOP-REAL 2)|P,(TOP-REAL 2)|Q such that
A2: f is_homeomorphism;
consider g being map of (TOP-REAL 2)|R^2-unit_square,
(TOP-REAL 2)|P such that
A3: g is_homeomorphism by A1,TOPREAL2:def 1;
(|[1,0]|)`1=1 & (|[1,0]|)`2=0 by EUCLID:56;
then A4: |[1,0]| in R^2-unit_square by TOPREAL1:def 3;
A5: dom g=[#]((TOP-REAL 2)|R^2-unit_square) &
rng g=[#]((TOP-REAL 2)|P) by A3,TOPS_2:def 5;
then dom g= R^2-unit_square by PRE_TOPC:def 10;
then A6: g.(|[1,0]|) in rng g by A4,FUNCT_1:12;
then A7: g.(|[1,0]|) in P by A5,PRE_TOPC:def 10;
reconsider P1=P as non empty Subset of TOP-REAL 2 by A5,A6,PRE_TOPC:def 10;
A8: dom f=[#]((TOP-REAL 2)|P) &
rng f=[#]((TOP-REAL 2)|Q) by A2,TOPS_2:def 5;
then dom f= P by PRE_TOPC:def 10;
then f.(g.(|[1,0]|)) in rng f by A7,FUNCT_1:12;
then reconsider Q1=Q as non empty Subset of TOP-REAL 2 by A8,PRE_TOPC:def 10
;
reconsider f1=f as map of (TOP-REAL 2)|P1,(TOP-REAL 2)|Q1;
reconsider g1=g as map of (TOP-REAL 2)|R^2-unit_square,(TOP-REAL 2)|P1;
reconsider h=f1*g1 as map of (TOP-REAL 2)|R^2-unit_square,
(TOP-REAL 2)|Q1;
h is_homeomorphism by A2,A3,TOPS_2:71;
hence Q is_simple_closed_curve by TOPREAL2:def 1;
end;
theorem Th31: for P being Subset of TOP-REAL 2 st
P is being_simple_closed_curve holds P is compact
proof
let P be Subset of TOP-REAL 2;
assume P is being_simple_closed_curve;
then reconsider P'=P as being_simple_closed_curve Subset of TOP-REAL 2;
P' is compact;
hence thesis;
end;
theorem Th32:
for a,b,r be real number, Cb being Subset of TOP-REAL 2 st r>0 &
Cb={p where p is Point of TOP-REAL 2: |.(p- |[a,b]|).|=r}
holds Cb is_simple_closed_curve
proof let a,b,r be real number,
Cb be Subset of TOP-REAL 2;
assume A1: r>0 & Cb={p where p is Point of TOP-REAL 2:
|.(p- |[a,b]|).|=r};
A2:(|[r,0]|)`1=r & (|[r,0]|)`2=0 by EUCLID:56;
|.(|[r+a,b]| - |[a,b]|).|=|.(|[r+a,0+b]| - |[a,b]|).|
.=|.(|[r,0]|+|[a,b]|- |[a,b]|).| by EUCLID:60
.= |.(|[r,0]|+(|[a,b]|- |[a,b]|)).| by EUCLID:49
.=|.|[r,0]|+(0.REAL 2).| by EUCLID:46
.=|.|[r,0]|.| by EUCLID:31 .=sqrt(r^2+0) by A2,JGRAPH_3:10,SQUARE_1:60
.=r by A1,SQUARE_1:89;
then |[r+a,b]| in Cb by A1;
then reconsider Cbb=Cb as non empty Subset of TOP-REAL 2;
set v= |[1,0]|;
v`1=1 & v`2=0 by EUCLID:56;
then |.v.|=sqrt(1^2+0) by JGRAPH_3:10,SQUARE_1:60
.=1 by SQUARE_1:89;
then A3: |[1,0]| in {q: |.q.|=1};
defpred P[Point of TOP-REAL 2] means |.$1.|=1;
{q where q is Element of TOP-REAL 2:P[q]}
is Subset of TOP-REAL 2 from SubsetD;
then reconsider Kb= {q: |.q.|=1}
as non empty Subset of TOP-REAL 2 by A3;
A4:the carrier of (TOP-REAL 2)|Kb=Kb by JORDAN1:1;
set SC= AffineMap(r,a,r,b);
A5: SC is one-to-one by A1,JGRAPH_2:54;
A6:dom SC = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
A7:dom (SC|Kb)=(dom SC)/\ Kb by FUNCT_1:68
.=the carrier of ((TOP-REAL 2)|Kb) by A4,A6,XBOOLE_1:28;
A8:rng (SC|Kb) c= rng (SC) by FUNCT_1:76;
A9:rng (SC|Kb) c= (SC|Kb).:(the carrier of ((TOP-REAL 2)|Kb))
proof let u be set;assume u in rng (SC|Kb);
then consider z being set such that
A10: z in dom ((SC|Kb)) & u=(SC|Kb).z by FUNCT_1:def 5;
thus u in (SC|Kb).:(the carrier of ((TOP-REAL 2)|Kb))
by A7,A10,FUNCT_1:def 12;
end;
(SC|Kb).: (the carrier of ((TOP-REAL 2)|Kb))
= SC.:Kb by A4,RFUNCT_2:5
.= Cb by A1,Th29
.=the carrier of (TOP-REAL 2)|Cbb by JORDAN1:1;
then SC|Kb is Function of the carrier of (TOP-REAL 2)|Kb,
the carrier of (TOP-REAL 2)|Cbb by A7,A9,FUNCT_2:4;
then reconsider f0=SC|Kb
as map of (TOP-REAL 2)|Kb, (TOP-REAL 2)|Cbb ;
rng (SC|Kb) c= the carrier of (TOP-REAL 2) by A8,XBOOLE_1:1;
then f0 is Function of the carrier of (TOP-REAL 2)|Kb,
the carrier of TOP-REAL 2 by A7,FUNCT_2:4;
then reconsider f00=f0 as map of (TOP-REAL 2)|Kb,TOP-REAL 2;
A11:rng f0 = (SC|Kb).:
(the carrier of ((TOP-REAL 2)|Kb)) by FUNCT_2:45
.= SC.:Kb by A4,RFUNCT_2:5
.= Cb by A1,Th29;
A12:f0 is one-to-one by A5,FUNCT_1:84;
A13:f00 is continuous by TOPMETR:10;
A14: Kb is being_simple_closed_curve by JGRAPH_3:36;
then Kb is compact by Th31;
then (TOP-REAL 2)|Kb is compact by COMPTS_1:12;
then ex f1 being map of (TOP-REAL 2)|Kb,(TOP-REAL 2)|Cbb st
f00=f1 & f1 is_homeomorphism by A11,A12,A13,JGRAPH_1:64;
hence thesis by A14,Th30;
end;
definition let a,b,r be real number;
assume A1: r>0;
func circle(a,b,r) -> compact non empty Subset of TOP-REAL 2 equals:Def6:
{p where p is Point of TOP-REAL 2: |.p- |[a,b]| .|=r};
coherence
proof
defpred P[Point of TOP-REAL 2] means |.$1- |[a,b]| .|=r;
{p where p is Point of TOP-REAL 2:P[p]}
c= the carrier of TOP-REAL 2 from Fr_Set0;
then reconsider Cb={p where p is Point of TOP-REAL 2: |.p- |[a,b]| .|=r}
as Subset of TOP-REAL 2;
A2:(|[r,0]|)`1=r & (|[r,0]|)`2=0 by EUCLID:56;
|.(|[r+a,b]| - |[a,b]|).|=|.(|[r+a,0+b]| - |[a,b]|).|
.=|.(|[r,0]|+|[a,b]|- |[a,b]|).| by EUCLID:60
.= |.(|[r,0]|+(|[a,b]|- |[a,b]|)).| by EUCLID:49
.=|.|[r,0]|+(0.REAL 2).| by EUCLID:46
.=|.|[r,0]|.| by EUCLID:31 .=sqrt(r^2+0^2) by A2,JGRAPH_3:10
.=r by A1,SQUARE_1:60,89;
then A3: |[r+a,b]| in Cb;
Cb is_simple_closed_curve by A1,Th32;
hence thesis by A3,Th31;
end;
end;
definition let a,b,r be real number;
func inside_of_circle(a,b,r) -> Subset of TOP-REAL 2 equals :Def7:
{p where p is Point of TOP-REAL 2: |.p- |[a,b]| .|<r};
coherence
proof
defpred P[Point of TOP-REAL 2] means |.$1- |[a,b]| .|<r;
{p where p is Point of TOP-REAL 2: P[p]}
c= the carrier of TOP-REAL 2 from Fr_Set0;
hence thesis;
end;
end;
definition let a,b,r be real number;
func closed_inside_of_circle(a,b,r) -> Subset of TOP-REAL 2 equals :Def8:
{p where p is Point of TOP-REAL 2: |.p- |[a,b]| .|<=r};
coherence
proof
defpred P[Point of TOP-REAL 2] means |.$1- |[a,b]| .|<=r;
{p where p is Point of TOP-REAL 2: P[p]}
c= the carrier of TOP-REAL 2 from Fr_Set0;
hence thesis;
end;
end;
definition let a,b,r be real number;
func outside_of_circle(a,b,r) -> Subset of TOP-REAL 2 equals :Def9:
{p where p is Point of TOP-REAL 2: |.p- |[a,b]| .|>r};
coherence
proof
defpred P[Point of TOP-REAL 2] means |.$1- |[a,b]| .|>r;
{p where p is Point of TOP-REAL 2: P[p]}
c= the carrier of TOP-REAL 2 from Fr_Set0;
hence thesis;
end;
end;
definition let a,b,r be real number;
func closed_outside_of_circle(a,b,r) -> Subset of TOP-REAL 2 equals :Def10:
{p where p is Point of TOP-REAL 2: |.p- |[a,b]| .|>=r};
coherence
proof
defpred P[Point of TOP-REAL 2] means |.$1- |[a,b]| .|>=r;
{p where p is Point of TOP-REAL 2: P[p]}
c= the carrier of TOP-REAL 2 from Fr_Set0;
hence thesis;
end;
end;
theorem Th33: for r being real number holds
inside_of_circle(0,0,r)={p : |.p.|<r} &
(r>0 implies circle(0,0,r)={p2 : |.p2.|=r}) &
outside_of_circle(0,0,r)={p3 : |.p3.|>r} &
closed_inside_of_circle(0,0,r)={q : |.q.|<=r} &
closed_outside_of_circle(0,0,r)={q2 : |.q2.|>=r}
proof let r be real number;
defpred P[Point of TOP-REAL 2] means |.$1- |[0,0]| .|<r;
defpred Q[Point of TOP-REAL 2] means |.$1.|<r;
deffunc F(set)=$1;
A1: for p holds P[p] iff Q[p] by EUCLID:58,JORDAN2C:13;
inside_of_circle(0,0,r)
= {F(p) where p is Point of TOP-REAL 2: P[p]} by Def7
.= {F(p2) where p2 is Point of TOP-REAL 2: Q[p2]} from Fraenkel6'(A1);
hence inside_of_circle(0,0,r)={p : |.p.|<r};
defpred P[Point of TOP-REAL 2] means |.$1- |[0,0]| .|=r;
defpred Q[Point of TOP-REAL 2] means |.$1.|=r;
A2: for p holds P[p] iff Q[p] by EUCLID:58,JORDAN2C:13;
hereby assume r>0;
then circle(0,0,r)= {F(p): P[p]} by Def6
.= {F(p2) where p2 is Point of TOP-REAL 2: Q[p2]} from Fraenkel6'(A2);
hence circle(0,0,r)={p2 : |.p2.|=r};
end;
defpred P[Point of TOP-REAL 2] means |.$1- |[0,0]| .|>r;
defpred Q[Point of TOP-REAL 2] means |.$1.|>r;
A3: for p holds P[p] iff Q[p] by EUCLID:58,JORDAN2C:13;
outside_of_circle(0,0,r)= {F(p): P[p]} by Def9
.= {F(p2) where p2 is Point of TOP-REAL 2: Q[p2]} from Fraenkel6'(A3);
hence outside_of_circle(0,0,r)={p3 : |.p3.|>r};
defpred P[Point of TOP-REAL 2] means |.$1- |[0,0]| .|<=r;
defpred Q[Point of TOP-REAL 2] means |.$1.|<=r;
A4: for p holds P[p] iff Q[p] by EUCLID:58,JORDAN2C:13;
closed_inside_of_circle(0,0,r)= {F(p): P[p]} by Def8
.= {F(p2) where p2 is Point of TOP-REAL 2: Q[p2]} from Fraenkel6'(A4);
hence closed_inside_of_circle(0,0,r)={p : |.p.|<=r};
defpred P[Point of TOP-REAL 2] means |.$1- |[0,0]| .|>=r;
defpred Q[Point of TOP-REAL 2] means |.$1.|>=r;
A5: for p holds P[p] iff Q[p] by EUCLID:58,JORDAN2C:13;
closed_outside_of_circle(0,0,r)= {F(p): P[p]} by Def10
.= {F(p2) where p2 is Point of TOP-REAL 2: Q[p2]} from Fraenkel6'(A5);
hence closed_outside_of_circle(0,0,r)={p3 : |.p3.|>=r};
end;
theorem Th34: for Kb,Cb being Subset of TOP-REAL 2 st
Kb={p: -1 <p`1 & p`1< 1 & -1 <p`2 & p`2< 1}&
Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|<1} holds Sq_Circ.:Kb=Cb
proof let Kb,Cb be Subset of TOP-REAL 2;
assume
A1:Kb={p: -1 <p`1 & p`1< 1 & -1 <p`2 & p`2< 1}&
Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|<1};
thus Sq_Circ.:Kb c= Cb
proof let y be set;assume y in Sq_Circ.:Kb;
then consider x being set such that
A2: x in dom Sq_Circ & x in Kb & y=Sq_Circ.x by FUNCT_1:def 12;
consider q being Point of TOP-REAL 2 such that
A3:q=x & -1 <q`1 & q`1< 1 & -1 <q`2 & q`2< 1 by A1,A2;
now per cases;
case A4: q=0.REAL 2;
then A5: Sq_Circ.q=q by JGRAPH_3:def 1;
|.q.|=0 by A4,TOPRNS_1:24;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|<1 by A2,A3,A5;
case A6:q<>0.REAL 2 &
(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then A7:Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|
by JGRAPH_3:def 1;
A8: (|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`1
= q`1/sqrt(1+(q`2/q`1)^2) &
(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`2
= q`2/sqrt(1+(q`2/q`1)^2) by EUCLID:56;
0<=(q`2/q`1)^2 by SQUARE_1:72;
then A9:1+(q`2/q`1)^2>0 by Th3;
A10: now assume A11: q`1=0;
then q`2=0 by A6;
hence contradiction by A6,A11,EUCLID:57,58;
end;
then A12: (q`1)^2>0 by SQUARE_1:74;
A13: (q`1)^2+(q`2)^2<>0 by A10,COMPLEX1:2;
(q`1)^2<1^2 by A3,JGRAPH_2:8;
then A14: sqrt((q`1)^2)<1 by A12,SQUARE_1:59,83,95;
A15: |.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|^2
=((q`1)/sqrt(1+(q`2/(q`1))^2))^2+(q`2/sqrt(1+(q`2/(q`1))^2))^2
by A8,JGRAPH_3:10
.=(q`1)^2/(sqrt(1+(q`2/(q`1))^2))^2+(q`2/sqrt(1+(q`2/(q`1))^2))^2
by SQUARE_1:69
.=(q`1)^2/(sqrt(1+(q`2/(q`1))^2))^2
+(q`2)^2/(sqrt(1+(q`2/(q`1))^2))^2 by SQUARE_1:69
.=(q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by A9,SQUARE_1:def 4
.=(q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(1+(q`2/q`1)^2)
by A9,SQUARE_1:def 4
.=((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2) by XCMPLX_1:63
.=((q`1)^2+(q`2)^2)/(1+(q`2)^2/(q`1)^2) by SQUARE_1:69
.=((q`1)^2+(q`2)^2)/((q`1)^2/(q`1)^2+(q`2)^2/(q`1)^2)
by A12,XCMPLX_1:60
.=((q`1)^2+(q`2)^2)/(((q`1)^2+(q`2)^2)/(q`1)^2)
by XCMPLX_1:63
.=(q`1)^2*(((q`1)^2+(q`2)^2)/((q`1)^2+(q`2)^2))
by XCMPLX_1:82
.=(q`1)^2*1 by A13,XCMPLX_1:60
.=(q`1)^2;
0<=|.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|
by TOPRNS_1:26;
then |.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|<1
by A14,A15,SQUARE_1:89;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|<1
by A2,A3,A7;
case A16:q<>0.REAL 2 &
not(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then A17:Sq_Circ.q=|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|
by JGRAPH_3:def 1;
A18: (|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|)`1
= q`1/sqrt(1+(q`1/q`2)^2) &
(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|)`2
= q`2/sqrt(1+(q`1/q`2)^2) by EUCLID:56;
0<=(q`1/q`2)^2 by SQUARE_1:72;
then A19:1+(q`1/q`2)^2>0 by Th3;
A20: q`2 <> 0 by A16,REAL_1:66;
then A21: (q`2)^2>0 by SQUARE_1:74;
A22: (q`1)^2+(q`2)^2 <>0 by A20,COMPLEX1:2;
(q`2)^2<1^2 by A3,JGRAPH_2:8;
then A23: sqrt((q`2)^2)<1 by A21,SQUARE_1:59,83,95;
A24: |.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|^2
=((q`1)/sqrt(1+(q`1/(q`2))^2))^2+(q`2/sqrt(1+(q`1/(q`2))^2))^2
by A18,JGRAPH_3:10
.=(q`1)^2/(sqrt(1+(q`1/(q`2))^2))^2+(q`2/sqrt(1+(q`1/(q`2))^2))^2
by SQUARE_1:69
.=(q`1)^2/(sqrt(1+(q`1/(q`2))^2))^2
+(q`2)^2/(sqrt(1+(q`1/(q`2))^2))^2 by SQUARE_1:69
.=(q`1)^2/(1+(q`1/q`2)^2)+(q`2)^2/(sqrt(1+(q`1/q`2)^2))^2
by A19,SQUARE_1:def 4
.=(q`1)^2/(1+(q`1/q`2)^2)+(q`2)^2/(1+(q`1/q`2)^2)
by A19,SQUARE_1:def 4
.=((q`1)^2+(q`2)^2)/(1+(q`1/q`2)^2) by XCMPLX_1:63
.=((q`1)^2+(q`2)^2)/(1+(q`1)^2/(q`2)^2) by SQUARE_1:69
.=((q`1)^2+(q`2)^2)/((q`1)^2/(q`2)^2+(q`2)^2/(q`2)^2)
by A21,XCMPLX_1:60
.=((q`1)^2+(q`2)^2)/(((q`1)^2+(q`2)^2)/(q`2)^2)
by XCMPLX_1:63
.=(q`2)^2*(((q`1)^2+(q`2)^2)/((q`1)^2+(q`2)^2))
by XCMPLX_1:82
.=(q`2)^2*1 by A22,XCMPLX_1:60
.=(q`2)^2;
0<=|.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|
by TOPRNS_1:26;
then |.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|<1
by A23,A24,SQUARE_1:89;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|<1
by A2,A3,A17;
end;
hence y in Cb by A1;
end;
let y be set;assume y in Cb;
then consider p2 being Point of TOP-REAL 2 such that
A25: p2=y & |.p2.|<1 by A1;
set q=p2;
now per cases;
case A26: q=0.REAL 2;
then q`1=0 & q`2=0 by EUCLID:56,58;
then A27: y in Kb by A1,A25;
A28: Sq_Circ".y=y by A25,A26,JGRAPH_3:38;
A29: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
y=Sq_Circ.y by A25,A28,FUNCT_1:57,JGRAPH_3:54;
hence ex x being set st x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by A27,A29;
case A30:q<>0.REAL 2 &
(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
set px=|[q`1*sqrt(1+(q`2/q`1)^2),q`2*sqrt(1+(q`2/q`1)^2)]|;
A31: px`1 = q`1*sqrt(1+(q`2/q`1)^2) &
px`2 = q`2*sqrt(1+(q`2/q`1)^2) by EUCLID:56;
0<=(q`2/q`1)^2 by SQUARE_1:72;
then 1+(q`2/q`1)^2>0 by Th3;
then A32:sqrt(1+(q`2/q`1)^2)>0 by SQUARE_1:93;
0<=(px`2/px`1)^2 by SQUARE_1:72;
then A33:1+(px`2/px`1)^2>0 by Th3;
A34:px`2/px`1=q`2/q`1 by A31,A32,XCMPLX_1:92;
A35: q`1=q`1*sqrt(1+(q`2/q`1)^2)/(sqrt(1+(q`2/q`1)^2))by A32,XCMPLX_1:
90
.=px`1/(sqrt(1+(q`2/q`1)^2)) by EUCLID:56;
A36: q`2=q`2*sqrt(1+(q`2/q`1)^2)/(sqrt(1+(q`2/q`1)^2))by A32,XCMPLX_1:
90
.=px`2/(sqrt(1+(q`2/q`1)^2)) by EUCLID:56;
A37: |.q.|^2=q`1^2+q`2^2 by JGRAPH_3:10;
|.q.| >=0 by TOPRNS_1:26;
then A38: |.q.|^2<1 by A25,SQUARE_1:59,78;
A39:now assume px`1=0 & px`2=0;
then A40:q`1*sqrt(1+(q`2/q`1)^2)=0 & q`2*sqrt(1+(q`2/q`1)^2)=0
by EUCLID:56;
then A41:q`1=0 by A32,XCMPLX_1:6;
q`2=0 by A32,A40,XCMPLX_1:6;
hence contradiction by A30,A41,EUCLID:57,58;
end;
q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 &
q`2*sqrt(1+(q`2/q`1)^2) <= (-q`1)*sqrt(1+(q`2/q`1)^2)
by A30,A32,AXIOMS:25;
then q`2<=q`1 & (-q`1)*sqrt(1+(q`2/q`1)^2) <= q`2*sqrt(1+(q`2/q`1)^2)
or px`2>=px`1 & px`2<=-px`1 by A31,A32,AXIOMS:25,XCMPLX_1:175;
then A42:px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1
by A31,A32,AXIOMS:25,XCMPLX_1:175;
then A43:Sq_Circ.px=|[px`1/sqrt(1+(px`2/px`1)^2),px`2/sqrt(1+(px`2/px`1)^2)
]|
by A39,JGRAPH_2:11,JGRAPH_3:def 1;
px`2<=px`1 & --px`1>=-px`2 or px`2>=px`1 & px`2<=-px`1
by A42,REAL_1:50;
then A44:px`2<=px`1 & px`1>=-px`2 or px`2>=px`1 & -px`2>=--px`1
by REAL_1:50;
A45:px`1/sqrt(1+(px`2/px`1)^2)=q`1 by A31,A32,A34,XCMPLX_1:90;
px`2/sqrt(1+(px`2/px`1)^2)=q`2 by A31,A32,A34,XCMPLX_1:90;
then A46:q=Sq_Circ.px by A43,A45,EUCLID:57;
A47: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
not px`1=0 by A39,A42;
then A48: (px`1)^2>0 by SQUARE_1:74;
A49: (px`2)^2>=0 by SQUARE_1:72;
(px`1)^2/(sqrt(1+(px`2/px`1)^2))^2+(px`2/sqrt(1+(px`2/px`1)^2))^2<1
by A34,A35,A36,A37,A38,SQUARE_1:69;
then (px`1)^2/(sqrt(1+(px`2/px`1)^2))^2+(px`2)^2/(sqrt(1+(px`2/px`1)^2))
^2<1
by SQUARE_1:69;
then (px`1)^2/(1+(px`2/px`1)^2)+(px`2)^2/(sqrt(1+(px`2/px`1)^2))^2<1
by A33,SQUARE_1:def 4;
then (px`1)^2/(1+(px`2/px`1)^2)+(px`2)^2/(1+(px`2/px`1)^2)<1
by A33,SQUARE_1:def 4;
then ((px`1)^2/(1+(px`2/px`1)^2)
+(px`2)^2/(1+(px`2/px`1)^2))*(1+(px`2/px`1)^2)<1 *(1+(px`2/px`1)^2)
by A33,REAL_1:70;
then (px`1)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)
+(px`2)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)<1 *(1+(px`2/px`1)^2)
by XCMPLX_1:8;
then (px`1)^2+(px`2)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)<1 *(1+(px`2/px
`1)^2)
by A33,XCMPLX_1:88;
then A50: (px`1)^2+(px`2)^2<1 *(1+(px`2/px`1)^2) by A33,XCMPLX_1:88;
1 *(1+(px`2/px`1)^2)
=1+(px`2)^2/(px`1)^2 by SQUARE_1:69;
then (px`1)^2+(px`2)^2-1<1+(px`2)^2/(px`1)^2-1 by A50,REAL_1:54;
then (px`1)^2+(px`2)^2-1<(px`2)^2/(px`1)^2 by XCMPLX_1:26;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2<((px`2)^2/(px`1)^2)*(px`1)^2
by A48,REAL_1:70;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2<(px`2)^2 by A48,XCMPLX_1:88;
then ((px`1)^2+((px`2)^2-1))*(px`1)^2<(px`2)^2 by XCMPLX_1:29;
then (px`1)^2*(px`1)^2+((px`2)^2-1)*(px`1)^2<(px`2)^2 by XCMPLX_1:8;
then (px`1)^2*(px`1)^2+(px`1)^2*((px`2)^2-1)-(px`2)^2<0
by REAL_2:105;
then A51: 0>(px`1)^2*(px`1)^2+((px`1)^2*(px`2)^2-(px`1)^2*1)-(px`2)^2
by XCMPLX_1:40;
(px`1)^2*(px`1)^2+((px`1)^2*(px`2)^2-(px`1)^2*1)-(px`2)^2
= (px`1)^2*(px`1)^2+(px`1)^2*(px`2)^2-(px`1)^2*1-(px`2)^2
by XCMPLX_1:29
.= (px`1)^2*(px`1)^2-(px`1)^2*1+(px`1)^2*(px`2)^2-1 *(px`2)^2
by XCMPLX_1:29
.= (px`1)^2*((px`1)^2-1)+(px`1)^2*(px`2)^2-1 *(px`2)^2 by XCMPLX_1:40
.= (px`1)^2*((px`1)^2-1)+((px`1)^2*(px`2)^2-1 *(px`2)^2) by XCMPLX_1:
29
.= (px`1)^2*((px`1)^2-1)+((px`1)^2-1)*(px`2)^2 by XCMPLX_1:40
.= ((px`1)^2-1)*((px`1)^2+(px`2)^2) by XCMPLX_1:8;
then ((px`1)^2-1<0 or ((px`1)^2+(px`2)^2)<0)
&((px`1)^2-1>0 or (px`1)^2+(px`2)^2>0) by A51,REAL_2:121;
then (px`1)^2-1+1<0+1 & ((px`1)^2+(px`2)^2)>0 by A48,A49,Th3,REAL_1:53
;
then (px`1)^2<1 by XCMPLX_1:27;
then A52:px`1<1 & px`1>-1 by JGRAPH_2:6,SQUARE_1:59;
then px`2<1 & 1>-px`2 or px`2>=px`1 & -px`2>=px`1
by A44,AXIOMS:22;
then px`2<1 & -1< --px`2 or px`2>-1 & -px`2> -1
by A52,AXIOMS:22,REAL_1:50;
then px`2<1 & -1<px`2 or px`2>-1 & --px`2< --1
by REAL_1:50;
then px in Kb by A1,A52;
hence ex x being set st x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by A25,A46,A47;
case A53:q<>0.REAL 2 & not(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
set px=|[q`1*sqrt(1+(q`1/q`2)^2),q`2*sqrt(1+(q`1/q`2)^2)]|;
A54:q<>0.REAL 2 & (q`1<=q`2 & -q`2<=q`1 or q`1>=q`2 & q`1<=-q`2)
by A53,JGRAPH_2:23;
A55: px`2 = q`2*sqrt(1+(q`1/q`2)^2) &
px`1 = q`1*sqrt(1+(q`1/q`2)^2) by EUCLID:56;
0<=(q`1/q`2)^2 by SQUARE_1:72;
then 1+(q`1/q`2)^2>0 by Th3;
then A56:sqrt(1+(q`1/q`2)^2)>0 by SQUARE_1:93;
0<=(px`1/px`2)^2 by SQUARE_1:72;
then A57:1+(px`1/px`2)^2>0 by Th3;
A58:px`1/px`2=q`1/q`2 by A55,A56,XCMPLX_1:92;
A59: q`2=q`2*sqrt(1+(q`1/q`2)^2)/(sqrt(1+(q`1/q`2)^2))by A56,XCMPLX_1:
90
.=px`2/(sqrt(1+(q`1/q`2)^2)) by EUCLID:56;
A60: q`1=q`1*sqrt(1+(q`1/q`2)^2)/(sqrt(1+(q`1/q`2)^2))by A56,XCMPLX_1:
90
.=px`1/(sqrt(1+(q`1/q`2)^2)) by EUCLID:56;
A61: |.q.|^2=q`2^2+q`1^2 by JGRAPH_3:10;
|.q.| >=0 by TOPRNS_1:26;
then A62: |.q.|^2<1 by A25,SQUARE_1:59,78;
A63:now assume px`2=0 & px`1=0;
then A64:q`2*sqrt(1+(q`1/q`2)^2)=0 & q`1*sqrt(1+(q`1/q`2)^2)=0
by EUCLID:56;
then q`1=0 by A56,XCMPLX_1:6;
hence contradiction by A53,A56,A64,XCMPLX_1:6;
end;
q`1<=q`2 & -q`2<=q`1 or q`1>=q`2 &
q`1*sqrt(1+(q`1/q`2)^2) <= (-q`2)*sqrt(1+(q`1/q`2)^2)
by A54,A56,AXIOMS:25;
then q`1<=q`2 & (-q`2)*sqrt(1+(q`1/q`2)^2) <= q`1*sqrt(1+(q`1/q`2)^2)
or px`1>=px`2 & px`1<=-px`2 by A55,A56,AXIOMS:25,XCMPLX_1:175;
then A65:px`1<=px`2 & -px`2<=px`1 or px`1>=px`2 & px`1<=-px`2
by A55,A56,AXIOMS:25,XCMPLX_1:175;
then A66:Sq_Circ.px=|[px`1/sqrt(1+(px`1/px`2)^2),px`2/sqrt(1+(px`1/px`2)^2)
]|
by A63,JGRAPH_2:11,JGRAPH_3:14;
px`1<=px`2 & --px`2>=-px`1 or px`1>=px`2 & px`1<=-px`2
by A65,REAL_1:50;
then A67:px`1<=px`2 & px`2>=-px`1 or px`1>=px`2 & -px`1>=--px`2
by REAL_1:50;
A68:px`2/sqrt(1+(px`1/px`2)^2)=q`2 by A55,A56,A58,XCMPLX_1:90;
px`1/sqrt(1+(px`1/px`2)^2)=q`1 by A55,A56,A58,XCMPLX_1:90;
then A69:q=Sq_Circ.px by A66,A68,EUCLID:57;
A70: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
not px`2=0 by A63,A65;
then A71: (px`2)^2>0 by SQUARE_1:74;
A72: (px`1)^2>=0 by SQUARE_1:72;
(px`2)^2/(sqrt(1+(px`1/px`2)^2))^2+(px`1/sqrt(1+(px`1/px`2)^2))^2<1
by A58,A59,A60,A61,A62,SQUARE_1:69;
then (px`2)^2/(sqrt(1+(px`1/px`2)^2))^2+(px`1)^2/(sqrt(1+(px`1/px`2)^2))
^2<1
by SQUARE_1:69;
then (px`2)^2/(1+(px`1/px`2)^2)+(px`1)^2/(sqrt(1+(px`1/px`2)^2))^2<1
by A57,SQUARE_1:def 4;
then (px`2)^2/(1+(px`1/px`2)^2)+(px`1)^2/(1+(px`1/px`2)^2)<1
by A57,SQUARE_1:def 4;
then ((px`2)^2/(1+(px`1/px`2)^2)
+(px`1)^2/(1+(px`1/px`2)^2))*(1+(px`1/px`2)^2)<1 *(1+(px`1/px`2)^2)
by A57,REAL_1:70;
then (px`2)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)
+(px`1)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)<1 *(1+(px`1/px`2)^2)
by XCMPLX_1:8;
then (px`2)^2+(px`1)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)<1 *(1+(px`1/px
`2)^2)
by A57,XCMPLX_1:88;
then A73: (px`2)^2+(px`1)^2<1 *(1+(px`1/px`2)^2) by A57,XCMPLX_1:88;
1 *(1+(px`1/px`2)^2)
=1+(px`1)^2/(px`2)^2 by SQUARE_1:69;
then (px`2)^2+(px`1)^2-1<1+(px`1)^2/(px`2)^2-1 by A73,REAL_1:54;
then (px`2)^2+(px`1)^2-1<(px`1)^2/(px`2)^2 by XCMPLX_1:26;
then ((px`2)^2+(px`1)^2-1)*(px`2)^2<((px`1)^2/(px`2)^2)*(px`2)^2
by A71,REAL_1:70;
then ((px`2)^2+(px`1)^2-1)*(px`2)^2<(px`1)^2 by A71,XCMPLX_1:88;
then ((px`2)^2+((px`1)^2-1))*(px`2)^2<(px`1)^2 by XCMPLX_1:29;
then (px`2)^2*(px`2)^2+((px`1)^2-1)*(px`2)^2<(px`1)^2 by XCMPLX_1:8;
then (px`2)^2*(px`2)^2+(px`2)^2*((px`1)^2-1)-(px`1)^2<0
by REAL_2:105;
then A74: 0>(px`2)^2*(px`2)^2+((px`2)^2*(px`1)^2-(px`2)^2*1)-(px`1)^2
by XCMPLX_1:40;
(px`2)^2*(px`2)^2+((px`2)^2*(px`1)^2-(px`2)^2*1)-(px`1)^2
= (px`2)^2*(px`2)^2+(px`2)^2*(px`1)^2-(px`2)^2*1-(px`1)^2
by XCMPLX_1:29
.= (px`2)^2*(px`2)^2-(px`2)^2*1+(px`2)^2*(px`1)^2-1 *(px`1)^2
by XCMPLX_1:29
.= (px`2)^2*((px`2)^2-1)+(px`2)^2*(px`1)^2-1 *(px`1)^2 by XCMPLX_1:40
.= (px`2)^2*((px`2)^2-1)+((px`2)^2*(px`1)^2-1 *(px`1)^2) by XCMPLX_1:
29
.= (px`2)^2*((px`2)^2-1)+((px`2)^2-1)*(px`1)^2 by XCMPLX_1:40
.= ((px`2)^2-1)*((px`2)^2+(px`1)^2) by XCMPLX_1:8;
then ((px`2)^2-1<0 or ((px`2)^2+(px`1)^2)<0)
&((px`2)^2-1>0 or (px`2)^2+(px`1)^2>0) by A74,REAL_2:121;
then (px`2)^2-1+1<0+1 & ((px`2)^2+(px`1)^2)>0 by A71,A72,Th3,REAL_1:53
;
then (px`2)^2<1 by XCMPLX_1:27;
then A75:px`2<1 & px`2>-1 by JGRAPH_2:6,SQUARE_1:59;
then px`1<1 & 1>-px`1 or px`1>=px`2 & -px`1>=px`2
by A67,AXIOMS:22;
then px`1<1 & -1< --px`1 or px`1>-1 & -px`1> -1
by A75,AXIOMS:22,REAL_1:50;
then px`1<1 & -1<px`1 or px`1>-1 & --px`1< --1
by REAL_1:50;
then px in Kb by A1,A75;
hence ex x being set st x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by A25,A69,A70;
end;
hence thesis by FUNCT_1:def 12;
end;
theorem Th35: for Kb,Cb being Subset of TOP-REAL 2 st
Kb={p: not(-1 <=p`1 & p`1<= 1 & -1 <=p`2 & p`2<= 1)}&
Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|>1} holds Sq_Circ.:Kb=Cb
proof let Kb,Cb be Subset of TOP-REAL 2;
assume
A1:Kb={p: not(-1 <=p`1 & p`1<= 1 & -1 <=p`2 & p`2<= 1)}&
Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|>1};
thus Sq_Circ.:Kb c= Cb
proof let y be set;assume y in Sq_Circ.:Kb;
then consider x being set such that
A2: x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by FUNCT_1:def 12;
consider q being Point of TOP-REAL 2 such that
A3:q=x &( not(-1 <=q`1 & q`1<= 1 & -1 <=q`2 & q`2<= 1) )
by A1,A2;
now per cases;
case q=0.REAL 2;
then q`1=0 & q`2=0 by EUCLID:56,58;
hence contradiction by A3;
case A4:q<>0.REAL 2 &
(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then A5:Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|
by JGRAPH_3:def 1;
A6: not(-1 <=q`2 & q`2<= 1) implies -1>q`1 or q`1>1
proof assume A7: not(-1 <=q`2 & q`2<= 1);
now per cases by A7;
case A8: -1>q`2;
then -q`1< -1 or q`2>=q`1 & q`2<= -q`1 by A4,AXIOMS:22;
hence -1>q`1 or q`1>1 by A8,AXIOMS:22,REAL_1:50;
case q`2>1;
then 1<q`1 or 1< -q`1 by A4,AXIOMS:22;
then 1<q`1 or --q`1< -1 by REAL_1:50;
hence -1>q`1 or q`1>1;
end;
hence -1>q`1 or q`1>1;
end;
A9: (|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`1
= q`1/sqrt(1+(q`2/q`1)^2) &
(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`2
= q`2/sqrt(1+(q`2/q`1)^2) by EUCLID:56;
0<=(q`2/q`1)^2 by SQUARE_1:72;
then A10:1+(q`2/q`1)^2>0 by Th3;
A11: now assume A12: q`1=0;
then q`2=0 by A4;
hence contradiction by A4,A12,EUCLID:57,58;
end;
then A13: (q`1)^2>0 by SQUARE_1:74;
A14: (q`1)^2+(q`2)^2 <>0 by A11,COMPLEX1:2;
(q`1)^2>1^2 by A3,A6,JGRAPH_2:5;
then A15: sqrt((q`1)^2)>1 by SQUARE_1:59,83,95;
A16: |.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|^2
=((q`1)/sqrt(1+(q`2/(q`1))^2))^2+(q`2/sqrt(1+(q`2/(q`1))^2))^2
by A9,JGRAPH_3:10
.=(q`1)^2/(sqrt(1+(q`2/(q`1))^2))^2+(q`2/sqrt(1+(q`2/(q`1))^2))^2
by SQUARE_1:69
.=(q`1)^2/(sqrt(1+(q`2/(q`1))^2))^2
+(q`2)^2/(sqrt(1+(q`2/(q`1))^2))^2 by SQUARE_1:69
.=(q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by A10,SQUARE_1:def 4
.=(q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(1+(q`2/q`1)^2)
by A10,SQUARE_1:def 4
.=((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2) by XCMPLX_1:63
.=((q`1)^2+(q`2)^2)/(1+(q`2)^2/(q`1)^2) by SQUARE_1:69
.=((q`1)^2+(q`2)^2)/((q`1)^2/(q`1)^2+(q`2)^2/(q`1)^2)
by A13,XCMPLX_1:60
.=((q`1)^2+(q`2)^2)/(((q`1)^2+(q`2)^2)/(q`1)^2) by XCMPLX_1:63
.=(q`1)^2*(((q`1)^2+(q`2)^2)/((q`1)^2+(q`2)^2)) by XCMPLX_1:82
.=(q`1)^2*1 by A14,XCMPLX_1:60
.=(q`1)^2;
0<=|.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|
by TOPRNS_1:26;
then |.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|>1
by A15,A16,SQUARE_1:89;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|>1
by A2,A3,A5;
case A17:q<>0.REAL 2 &
not(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then A18:Sq_Circ.q=|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|
by JGRAPH_3:def 1;
A19: (|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|)`1
= q`1/sqrt(1+(q`1/q`2)^2) &
(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|)`2
= q`2/sqrt(1+(q`1/q`2)^2) by EUCLID:56;
0<=(q`1/q`2)^2 by SQUARE_1:72;
then A20:1+(q`1/q`2)^2>0 by Th3;
A21: q`2 <> 0 by A17,REAL_1:66;
then A22: (q`2)^2>0 by SQUARE_1:74;
A23: (q`1)^2+(q`2)^2 <>0 by A21,COMPLEX1:2;
not(-1 <=q`1 & q`1<= 1) implies -1>q`2 or q`2>1
proof assume A24: not(-1 <=q`1 & q`1<= 1);
now per cases by A24;
case A25: -1>q`1;
then q`2< -1 or q`1<q`2 & -q`2< --q`1 by A17,AXIOMS:22,REAL_1:50;
then -q`2< -1 or -1>q`2 by A25,AXIOMS:22;
hence -1>q`2 or q`2>1 by REAL_1:50;
case A26: q`1>1;
--q`1< -q`2 & q`2<q`1 or q`2>q`1 & q`2> -q`1 by A17,REAL_1:50;
then 1< -q`2 or q`2>q`1 & q`2> -q`1 by A26,AXIOMS:22;
then -1> --q`2 or 1<q`2 by A26,AXIOMS:22,REAL_1:50;
hence -1>q`2 or q`2>1;
end;
hence -1>q`2 or q`2>1;
end;
then (q`2)^2>1^2 by A3,JGRAPH_2:5;
then A27: sqrt((q`2)^2)>1 by SQUARE_1:59,83,95;
A28: |.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|^2
=((q`1)/sqrt(1+(q`1/(q`2))^2))^2+(q`2/sqrt(1+(q`1/(q`2))^2))^2
by A19,JGRAPH_3:10
.=(q`1)^2/(sqrt(1+(q`1/(q`2))^2))^2+(q`2/sqrt(1+(q`1/(q`2))^2))^2
by SQUARE_1:69
.=(q`1)^2/(sqrt(1+(q`1/(q`2))^2))^2
+(q`2)^2/(sqrt(1+(q`1/(q`2))^2))^2 by SQUARE_1:69
.=(q`1)^2/(1+(q`1/q`2)^2)+(q`2)^2/(sqrt(1+(q`1/q`2)^2))^2
by A20,SQUARE_1:def 4
.=(q`1)^2/(1+(q`1/q`2)^2)+(q`2)^2/(1+(q`1/q`2)^2)
by A20,SQUARE_1:def 4
.=((q`1)^2+(q`2)^2)/(1+(q`1/q`2)^2) by XCMPLX_1:63
.=((q`1)^2+(q`2)^2)/(1+(q`1)^2/(q`2)^2) by SQUARE_1:69
.=((q`1)^2+(q`2)^2)/((q`1)^2/(q`2)^2+(q`2)^2/(q`2)^2)
by A22,XCMPLX_1:60
.=((q`1)^2+(q`2)^2)/(((q`1)^2+(q`2)^2)/(q`2)^2)
by XCMPLX_1:63
.=(q`2)^2*(((q`1)^2+(q`2)^2)/((q`1)^2+(q`2)^2))
by XCMPLX_1:82
.=(q`2)^2*1 by A23,XCMPLX_1:60
.=(q`2)^2;
0<=|.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|
by TOPRNS_1:26;
then |.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|>1
by A27,A28,SQUARE_1:89;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|>1
by A2,A3,A18;
end;
hence y in Cb by A1;
end;
let y be set;assume y in Cb;
then consider p2 being Point of TOP-REAL 2 such that
A29: p2=y & |.p2.|>1 by A1;
set q=p2;
now per cases;
case q=0.REAL 2;
then |.q.|=0 by TOPRNS_1:24;
hence contradiction by A29;
case A30:q<>0.REAL 2 &
(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
set px=|[q`1*sqrt(1+(q`2/q`1)^2),q`2*sqrt(1+(q`2/q`1)^2)]|;
A31: px`1 = q`1*sqrt(1+(q`2/q`1)^2) &
px`2 = q`2*sqrt(1+(q`2/q`1)^2) by EUCLID:56;
0<=(q`2/q`1)^2 by SQUARE_1:72;
then 1+(q`2/q`1)^2>0 by Th3;
then A32:sqrt(1+(q`2/q`1)^2)>0 by SQUARE_1:93;
0<=(px`2/px`1)^2 by SQUARE_1:72;
then A33:1+(px`2/px`1)^2>0 by Th3;
A34:px`2/px`1=q`2/q`1 by A31,A32,XCMPLX_1:92;
A35: q`1=q`1*sqrt(1+(q`2/q`1)^2)/(sqrt(1+(q`2/q`1)^2))by A32,XCMPLX_1:
90
.=px`1/(sqrt(1+(q`2/q`1)^2)) by EUCLID:56;
A36: q`2=q`2*sqrt(1+(q`2/q`1)^2)/(sqrt(1+(q`2/q`1)^2))by A32,XCMPLX_1:
90
.=px`2/(sqrt(1+(q`2/q`1)^2)) by EUCLID:56;
A37: |.q.|^2=q`1^2+q`2^2 by JGRAPH_3:10;
A38: |.q.|^2>1 by A29,SQUARE_1:59,78;
A39:now assume px`1=0 & px`2=0;
then A40:q`1*sqrt(1+(q`2/q`1)^2)=0 & q`2*sqrt(1+(q`2/q`1)^2)=0
by EUCLID:56;
then A41:q`1=0 by A32,XCMPLX_1:6;
q`2=0 by A32,A40,XCMPLX_1:6;
hence contradiction by A30,A41,EUCLID:57,58;
end;
q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 &
q`2*sqrt(1+(q`2/q`1)^2) <= (-q`1)*sqrt(1+(q`2/q`1)^2)
by A30,A32,AXIOMS:25;
then q`2<=q`1 & (-q`1)*sqrt(1+(q`2/q`1)^2) <= q`2*sqrt(1+(q`2/q`1)^2)
or px`2>=px`1 & px`2<=-px`1 by A31,A32,AXIOMS:25,XCMPLX_1:175;
then A42:px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1
by A31,A32,AXIOMS:25,XCMPLX_1:175;
then A43:Sq_Circ.px=|[px`1/sqrt(1+(px`2/px`1)^2),px`2/sqrt(1+(px`2/px`1)^2)
]|
by A39,JGRAPH_2:11,JGRAPH_3:def 1;
A44:px`1/sqrt(1+(px`2/px`1)^2)=q`1 by A31,A32,A34,XCMPLX_1:90;
px`2/sqrt(1+(px`2/px`1)^2)=q`2 by A31,A32,A34,XCMPLX_1:90;
then A45:q=Sq_Circ.px by A43,A44,EUCLID:57;
A46: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
not px`1=0 by A39,A42;
then A47: (px`1)^2>0 by SQUARE_1:74;
A48: (px`2)^2>=0 by SQUARE_1:72;
(px`1)^2/(sqrt(1+(px`2/px`1)^2))^2+(px`2/sqrt(1+(px`2/px`1)^2))^2>1
by A34,A35,A36,A37,A38,SQUARE_1:69;
then (px`1)^2/(sqrt(1+(px`2/px`1)^2))^2+(px`2)^2/(sqrt(1+(px`2/px`1)^2))
^2>1
by SQUARE_1:69;
then (px`1)^2/(1+(px`2/px`1)^2)+(px`2)^2/(sqrt(1+(px`2/px`1)^2))^2>1
by A33,SQUARE_1:def 4;
then (px`1)^2/(1+(px`2/px`1)^2)+(px`2)^2/(1+(px`2/px`1)^2)>1
by A33,SQUARE_1:def 4;
then ((px`1)^2/(1+(px`2/px`1)^2)
+(px`2)^2/(1+(px`2/px`1)^2))*(1+(px`2/px`1)^2)>1 *(1+(px`2/px`1)^2)
by A33,REAL_1:70;
then (px`1)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)
+(px`2)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)>1 *(1+(px`2/px`1)^2)
by XCMPLX_1:8;
then (px`1)^2+(px`2)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)>1 *(1+(px`2/px
`1)^2)
by A33,XCMPLX_1:88;
then A49: (px`1)^2+(px`2)^2>1 *(1+(px`2/px`1)^2) by A33,XCMPLX_1:88;
1 *(1+(px`2/px`1)^2)
=1+(px`2)^2/(px`1)^2 by SQUARE_1:69;
then (px`1)^2+(px`2)^2-1>1+(px`2)^2/(px`1)^2-1 by A49,REAL_1:54;
then (px`1)^2+(px`2)^2-1>(px`2)^2/(px`1)^2 by XCMPLX_1:26;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2>((px`2)^2/(px`1)^2)*(px`1)^2
by A47,REAL_1:70;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2>(px`2)^2 by A47,XCMPLX_1:88;
then ((px`1)^2+((px`2)^2-1))*(px`1)^2>(px`2)^2 by XCMPLX_1:29;
then (px`1)^2*(px`1)^2+((px`2)^2-1)*(px`1)^2>(px`2)^2 by XCMPLX_1:8;
then (px`1)^2*(px`1)^2+(px`1)^2*((px`2)^2-1)-(px`2)^2>0
by SQUARE_1:11;
then A50: 0<(px`1)^2*(px`1)^2+((px`1)^2*(px`2)^2-(px`1)^2*1)-(px`2)^2
by XCMPLX_1:40;
(px`1)^2*(px`1)^2+((px`1)^2*(px`2)^2-(px`1)^2*1)-(px`2)^2
= (px`1)^2*(px`1)^2+(px`1)^2*(px`2)^2-(px`1)^2*1-(px`2)^2
by XCMPLX_1:29
.= (px`1)^2*(px`1)^2-(px`1)^2*1+(px`1)^2*(px`2)^2-1 *(px`2)^2
by XCMPLX_1:29
.= (px`1)^2*((px`1)^2-1)+(px`1)^2*(px`2)^2-1 *(px`2)^2 by XCMPLX_1:40
.= (px`1)^2*((px`1)^2-1)+((px`1)^2*(px`2)^2-1 *(px`2)^2) by XCMPLX_1:
29
.= (px`1)^2*((px`1)^2-1)+((px`1)^2-1)*(px`2)^2 by XCMPLX_1:40
.= ((px`1)^2-1)*((px`1)^2+(px`2)^2) by XCMPLX_1:8;
then ( (px`1)^2-1<0 or (px`1)^2+(px`2)^2>0)&
((px`1)^2-1>0 or (px`1)^2+(px`2)^2<0) by A50,REAL_2:123;
then (px`1)^2-1+1>0+1 & ((px`1)^2+(px`2)^2)>0 by A47,A48,Th3,REAL_1:53
;
then (px`1)^2>1 by XCMPLX_1:27;
then px`1>1 or px`1< -1 by JGRAPH_2:7,SQUARE_1:59;
then px in Kb by A1;
hence ex x being set st x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by A29,A45,A46;
case A51:q<>0.REAL 2 & not(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
set px=|[q`1*sqrt(1+(q`1/q`2)^2),q`2*sqrt(1+(q`1/q`2)^2)]|;
A52:q<>0.REAL 2 & (q`1<=q`2 & -q`2<=q`1 or q`1>=q`2 & q`1<=-q`2)
by A51,JGRAPH_2:23;
A53: px`2 = q`2*sqrt(1+(q`1/q`2)^2) &
px`1 = q`1*sqrt(1+(q`1/q`2)^2) by EUCLID:56;
0<=(q`1/q`2)^2 by SQUARE_1:72;
then 1+(q`1/q`2)^2>0 by Th3;
then A54:sqrt(1+(q`1/q`2)^2)>0 by SQUARE_1:93;
0<=(px`1/px`2)^2 by SQUARE_1:72;
then A55:1+(px`1/px`2)^2>0 by Th3;
A56:px`1/px`2=q`1/q`2 by A53,A54,XCMPLX_1:92;
A57: q`2=q`2*sqrt(1+(q`1/q`2)^2)/(sqrt(1+(q`1/q`2)^2))by A54,XCMPLX_1:
90
.=px`2/(sqrt(1+(q`1/q`2)^2)) by EUCLID:56;
A58: q`1=q`1*sqrt(1+(q`1/q`2)^2)/(sqrt(1+(q`1/q`2)^2))by A54,XCMPLX_1:
90
.=px`1/(sqrt(1+(q`1/q`2)^2)) by EUCLID:56;
A59: |.q.|^2=q`2^2+q`1^2 by JGRAPH_3:10;
A60: |.q.|^2>1 by A29,SQUARE_1:59,78;
A61:now assume px`2=0 & px`1=0;
then A62:q`2*sqrt(1+(q`1/q`2)^2)=0 & q`1*sqrt(1+(q`1/q`2)^2)=0
by EUCLID:56;
then q`1=0 by A54,XCMPLX_1:6;
hence contradiction by A51,A54,A62,XCMPLX_1:6;
end;
q`1<=q`2 & -q`2<=q`1 or q`1>=q`2 &
q`1*sqrt(1+(q`1/q`2)^2) <= (-q`2)*sqrt(1+(q`1/q`2)^2)
by A52,A54,AXIOMS:25;
then q`1<=q`2 & (-q`2)*sqrt(1+(q`1/q`2)^2) <= q`1*sqrt(1+(q`1/q`2)^2)
or px`1>=px`2 & px`1<=-px`2 by A53,A54,AXIOMS:25,XCMPLX_1:175;
then A63:px`1<=px`2 & -px`2<=px`1 or px`1>=px`2 & px`1<=-px`2
by A53,A54,AXIOMS:25,XCMPLX_1:175;
then A64:Sq_Circ.px=|[px`1/sqrt(1+(px`1/px`2)^2),px`2/sqrt(1+(px`1/px`2)^2)
]|
by A61,JGRAPH_2:11,JGRAPH_3:14;
A65:px`2/sqrt(1+(px`1/px`2)^2)=q`2 by A53,A54,A56,XCMPLX_1:90;
px`1/sqrt(1+(px`1/px`2)^2)=q`1 by A53,A54,A56,XCMPLX_1:90;
then A66:q=Sq_Circ.px by A64,A65,EUCLID:57;
A67: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
not px`2=0 by A61,A63;
then A68: (px`2)^2>0 by SQUARE_1:74;
A69: (px`1)^2>=0 by SQUARE_1:72;
(px`2)^2/(sqrt(1+(px`1/px`2)^2))^2+(px`1/sqrt(1+(px`1/px`2)^2))^2>1
by A56,A57,A58,A59,A60,SQUARE_1:69;
then (px`2)^2/(sqrt(1+(px`1/px`2)^2))^2+(px`1)^2/(sqrt(1+(px`1/px`2)^2))
^2>1
by SQUARE_1:69;
then (px`2)^2/(1+(px`1/px`2)^2)+(px`1)^2/(sqrt(1+(px`1/px`2)^2))^2>1
by A55,SQUARE_1:def 4;
then (px`2)^2/(1+(px`1/px`2)^2)+(px`1)^2/(1+(px`1/px`2)^2)>1
by A55,SQUARE_1:def 4;
then ((px`2)^2/(1+(px`1/px`2)^2)
+(px`1)^2/(1+(px`1/px`2)^2))*(1+(px`1/px`2)^2)>1 *(1+(px`1/px`2)^2)
by A55,REAL_1:70;
then (px`2)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)
+(px`1)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)>1 *(1+(px`1/px`2)^2)
by XCMPLX_1:8;
then (px`2)^2+(px`1)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)>1 *(1+(px`1/px
`2)^2)
by A55,XCMPLX_1:88;
then A70: (px`2)^2+(px`1)^2>1 *(1+(px`1/px`2)^2) by A55,XCMPLX_1:88;
1 *(1+(px`1/px`2)^2)
=1+(px`1)^2/(px`2)^2 by SQUARE_1:69;
then (px`2)^2+(px`1)^2-1>1+(px`1)^2/(px`2)^2-1 by A70,REAL_1:54;
then (px`2)^2+(px`1)^2-1>(px`1)^2/(px`2)^2 by XCMPLX_1:26;
then ((px`2)^2+(px`1)^2-1)*(px`2)^2>((px`1)^2/(px`2)^2)*(px`2)^2
by A68,REAL_1:70;
then ((px`2)^2+(px`1)^2-1)*(px`2)^2>(px`1)^2 by A68,XCMPLX_1:88;
then ((px`2)^2+((px`1)^2-1))*(px`2)^2>(px`1)^2 by XCMPLX_1:29;
then (px`2)^2*(px`2)^2+((px`1)^2-1)*(px`2)^2>(px`1)^2 by XCMPLX_1:8;
then (px`2)^2*(px`2)^2+(px`2)^2*((px`1)^2-1)-(px`1)^2>0
by SQUARE_1:11;
then A71: 0<(px`2)^2*(px`2)^2+((px`2)^2*(px`1)^2-(px`2)^2*1)-(px`1)^2
by XCMPLX_1:40;
(px`2)^2*(px`2)^2+((px`2)^2*(px`1)^2-(px`2)^2*1)-(px`1)^2
= (px`2)^2*(px`2)^2+(px`2)^2*(px`1)^2-(px`2)^2*1-(px`1)^2
by XCMPLX_1:29
.= (px`2)^2*(px`2)^2-(px`2)^2*1+(px`2)^2*(px`1)^2-1 *(px`1)^2
by XCMPLX_1:29
.= (px`2)^2*((px`2)^2-1)+(px`2)^2*(px`1)^2-1 *(px`1)^2 by XCMPLX_1:40
.= (px`2)^2*((px`2)^2-1)+((px`2)^2*(px`1)^2-1 *(px`1)^2) by XCMPLX_1:
29
.= (px`2)^2*((px`2)^2-1)+((px`2)^2-1)*(px`1)^2 by XCMPLX_1:40
.= ((px`2)^2-1)*((px`2)^2+(px`1)^2) by XCMPLX_1:8;
then ( (px`2)^2-1<0 or (px`1)^2+(px`2)^2>0)&
((px`2)^2-1>0 or (px`1)^2+(px`2)^2<0) by A71,REAL_2:123;
then (px`2)^2-1+1>0+1 & ((px`1)^2+(px`2)^2)>0 by A68,A69,Th3,REAL_1:53
;
then (px`2)^2>1 by XCMPLX_1:27;
then px`2>1 or px`2< -1 by JGRAPH_2:7,SQUARE_1:59;
then px in Kb by A1;
hence ex x being set st x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by A29,A66,A67;
end;
hence thesis by FUNCT_1:def 12;
end;
theorem Th36: for Kb,Cb being Subset of TOP-REAL 2 st
Kb={p: -1 <=p`1 & p`1<= 1 & -1 <=p`2 & p`2<= 1}&
Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|<=1} holds Sq_Circ.:Kb=Cb
proof let Kb,Cb be Subset of TOP-REAL 2;
assume
A1:Kb={p: -1 <=p`1 & p`1<= 1 & -1 <=p`2 & p`2<= 1}&
Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|<=1};
thus Sq_Circ.:Kb c= Cb
proof let y be set;assume y in Sq_Circ.:Kb;
then consider x being set such that
A2: x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by FUNCT_1:def 12;
consider q being Point of TOP-REAL 2 such that
A3:q=x &( -1 <=q`1 & q`1<= 1 & -1 <=q`2 & q`2<= 1 ) by A1,A2;
now per cases;
case A4: q=0.REAL 2;
then A5: Sq_Circ.q=q by JGRAPH_3:def 1;
|.q.|=0 by A4,TOPRNS_1:24;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|<=1 by A2,A3,A5;
case A6:q<>0.REAL 2 &
(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then A7:Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|
by JGRAPH_3:def 1;
A8: (|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`1
= q`1/sqrt(1+(q`2/q`1)^2) &
(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`2
= q`2/sqrt(1+(q`2/q`1)^2) by EUCLID:56;
0<=(q`2/q`1)^2 by SQUARE_1:72;
then A9:1+(q`2/q`1)^2>0 by Th3;
A10: now assume A11: q`1=0;
then q`2=0 by A6;
hence contradiction by A6,A11,EUCLID:57,58;
end;
then A12: (q`1)^2>0 by SQUARE_1:74;
A13: (q`1)^2+(q`2)^2 <>0 by A10,COMPLEX1:2;
(q`1)^2<=1^2 by A3,JGRAPH_2:7;
then A14: sqrt((q`1)^2)<=1 by A12,SQUARE_1:59,83,94;
A15: |.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|^2
=((q`1)/sqrt(1+(q`2/(q`1))^2))^2+(q`2/sqrt(1+(q`2/(q`1))^2))^2
by A8,JGRAPH_3:10
.=(q`1)^2/(sqrt(1+(q`2/(q`1))^2))^2+(q`2/sqrt(1+(q`2/(q`1))^2))^2
by SQUARE_1:69
.=(q`1)^2/(sqrt(1+(q`2/(q`1))^2))^2
+(q`2)^2/(sqrt(1+(q`2/(q`1))^2))^2 by SQUARE_1:69
.=(q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by A9,SQUARE_1:def 4
.=(q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(1+(q`2/q`1)^2)
by A9,SQUARE_1:def 4
.=((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2) by XCMPLX_1:63
.=((q`1)^2+(q`2)^2)/(1+(q`2)^2/(q`1)^2) by SQUARE_1:69
.=((q`1)^2+(q`2)^2)/((q`1)^2/(q`1)^2+(q`2)^2/(q`1)^2)
by A12,XCMPLX_1:60
.=((q`1)^2+(q`2)^2)/(((q`1)^2+(q`2)^2)/(q`1)^2)
by XCMPLX_1:63
.=(q`1)^2*(((q`1)^2+(q`2)^2)/((q`1)^2+(q`2)^2))
by XCMPLX_1:82
.=(q`1)^2*1 by A13,XCMPLX_1:60
.=(q`1)^2;
0<=|.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|
by TOPRNS_1:26;
then |.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|<=1
by A14,A15,SQUARE_1:89;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|<=1
by A2,A3,A7;
case A16:q<>0.REAL 2 &
not(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then A17:Sq_Circ.q=|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|
by JGRAPH_3:def 1;
A18: (|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|)`1
= q`1/sqrt(1+(q`1/q`2)^2) &
(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|)`2
= q`2/sqrt(1+(q`1/q`2)^2) by EUCLID:56;
0<=(q`1/q`2)^2 by SQUARE_1:72;
then A19:1+(q`1/q`2)^2>0 by Th3;
A20: q`2 <>0 by A16,REAL_1:66;
then A21: (q`2)^2>0 by SQUARE_1:74;
A22: (q`1)^2+(q`2)^2 <>0 by A20,COMPLEX1:2;
(q`2)^2<=1 by A3,JGRAPH_2:7,SQUARE_1:59;
then A23: sqrt((q`2)^2)<=1 by A21,SQUARE_1:83,94;
A24: |.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|^2
=((q`1)/sqrt(1+(q`1/(q`2))^2))^2+(q`2/sqrt(1+(q`1/(q`2))^2))^2
by A18,JGRAPH_3:10
.=(q`1)^2/(sqrt(1+(q`1/(q`2))^2))^2+(q`2/sqrt(1+(q`1/(q`2))^2))^2
by SQUARE_1:69
.=(q`1)^2/(sqrt(1+(q`1/(q`2))^2))^2
+(q`2)^2/(sqrt(1+(q`1/(q`2))^2))^2 by SQUARE_1:69
.=(q`1)^2/(1+(q`1/q`2)^2)+(q`2)^2/(sqrt(1+(q`1/q`2)^2))^2
by A19,SQUARE_1:def 4
.=(q`1)^2/(1+(q`1/q`2)^2)+(q`2)^2/(1+(q`1/q`2)^2)
by A19,SQUARE_1:def 4
.=((q`1)^2+(q`2)^2)/(1+(q`1/q`2)^2) by XCMPLX_1:63
.=((q`1)^2+(q`2)^2)/(1+(q`1)^2/(q`2)^2) by SQUARE_1:69
.=((q`1)^2+(q`2)^2)/((q`1)^2/(q`2)^2+(q`2)^2/(q`2)^2)
by A21,XCMPLX_1:60
.=((q`1)^2+(q`2)^2)/(((q`1)^2+(q`2)^2)/(q`2)^2)
by XCMPLX_1:63
.=(q`2)^2*(((q`1)^2+(q`2)^2)/((q`1)^2+(q`2)^2)) by XCMPLX_1:82
.=(q`2)^2*1 by A22,XCMPLX_1:60
.=(q`2)^2;
0<=|.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|
by TOPRNS_1:26;
then |.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|<=1
by A23,A24,SQUARE_1:89;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|<=1
by A2,A3,A17;
end;
hence y in Cb by A1;
end;
let y be set;assume y in Cb;
then consider p2 being Point of TOP-REAL 2 such that
A25: p2=y & |.p2.|<=1 by A1;
set q=p2;
now per cases;
case A26: q=0.REAL 2;
then q`1=0 & q`2=0 by EUCLID:56,58;
then A27: y in Kb by A1,A25;
A28: Sq_Circ".y=y by A25,A26,JGRAPH_3:38;
A29: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
y=Sq_Circ.y by A25,A28,FUNCT_1:57,JGRAPH_3:54;
hence ex x being set st x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by A27,A29;
case A30:q<>0.REAL 2 &
(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
set px=|[q`1*sqrt(1+(q`2/q`1)^2),q`2*sqrt(1+(q`2/q`1)^2)]|;
A31: px`1 = q`1*sqrt(1+(q`2/q`1)^2) &
px`2 = q`2*sqrt(1+(q`2/q`1)^2) by EUCLID:56;
0<=(q`2/q`1)^2 by SQUARE_1:72;
then 1+(q`2/q`1)^2>0 by Th3;
then A32:sqrt(1+(q`2/q`1)^2)>0 by SQUARE_1:93;
0<=(px`2/px`1)^2 by SQUARE_1:72;
then A33:1+(px`2/px`1)^2>0 by Th3;
A34:px`2/px`1=q`2/q`1 by A31,A32,XCMPLX_1:92;
A35: q`1=q`1*sqrt(1+(q`2/q`1)^2)/(sqrt(1+(q`2/q`1)^2))by A32,XCMPLX_1:
90
.=px`1/(sqrt(1+(q`2/q`1)^2)) by EUCLID:56;
A36: q`2=q`2*sqrt(1+(q`2/q`1)^2)/(sqrt(1+(q`2/q`1)^2))by A32,XCMPLX_1:
90
.=px`2/(sqrt(1+(q`2/q`1)^2)) by EUCLID:56;
A37: |.q.|^2=q`1^2+q`2^2 by JGRAPH_3:10;
|.q.| >=0 by TOPRNS_1:26;
then A38: |.q.|^2<=1 by A25,SQUARE_1:59,77;
A39:now assume px`1=0 & px`2=0;
then A40:q`1*sqrt(1+(q`2/q`1)^2)=0 & q`2*sqrt(1+(q`2/q`1)^2)=0
by EUCLID:56;
then A41:q`1=0 by A32,XCMPLX_1:6;
q`2=0 by A32,A40,XCMPLX_1:6;
hence contradiction by A30,A41,EUCLID:57,58;
end;
q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 &
q`2*sqrt(1+(q`2/q`1)^2) <= (-q`1)*sqrt(1+(q`2/q`1)^2)
by A30,A32,AXIOMS:25;
then q`2<=q`1 & (-q`1)*sqrt(1+(q`2/q`1)^2) <= q`2*sqrt(1+(q`2/q`1)^2)
or px`2>=px`1 & px`2<=-px`1 by A31,A32,AXIOMS:25,XCMPLX_1:175;
then A42:px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1
by A31,A32,AXIOMS:25,XCMPLX_1:175;
then A43:Sq_Circ.px=|[px`1/sqrt(1+(px`2/px`1)^2),px`2/sqrt(1+(px`2/px`1)^2)
]|
by A39,JGRAPH_2:11,JGRAPH_3:def 1;
px`2<=px`1 & --px`1>=-px`2 or px`2>=px`1 & px`2<=-px`1
by A42,REAL_1:50;
then A44:px`2<=px`1 & px`1>=-px`2 or px`2>=px`1 & -px`2>=--px`1
by REAL_1:50;
A45:px`1/sqrt(1+(px`2/px`1)^2)=q`1 by A31,A32,A34,XCMPLX_1:90;
px`2/sqrt(1+(px`2/px`1)^2)=q`2 by A31,A32,A34,XCMPLX_1:90;
then A46:q=Sq_Circ.px by A43,A45,EUCLID:57;
A47: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
not px`1=0 by A39,A42;
then A48: (px`1)^2>0 by SQUARE_1:74;
A49: (px`2)^2>=0 by SQUARE_1:72;
(px`1)^2/(sqrt(1+(px`2/px`1)^2))^2+(px`2/sqrt(1+(px`2/px`1)^2))^2
<=1
by A34,A35,A36,A37,A38,SQUARE_1:69;
then (px`1)^2/(sqrt(1+(px`2/px`1)^2))^2+(px`2)^2/(sqrt(1+(px`2/px`1)^2))
^2<=1
by SQUARE_1:69;
then (px`1)^2/(1+(px`2/px`1)^2)+(px`2)^2/(sqrt(1+(px`2/px`1)^2))^2<=1
by A33,SQUARE_1:def 4;
then (px`1)^2/(1+(px`2/px`1)^2)+(px`2)^2/(1+(px`2/px`1)^2)<=1
by A33,SQUARE_1:def 4;
then ((px`1)^2/(1+(px`2/px`1)^2)
+(px`2)^2/(1+(px`2/px`1)^2))*(1+(px`2/px`1)^2)<=1 *(1+(px`2/px`1)^2)
by A33,AXIOMS:25;
then (px`1)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)
+(px`2)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)<=1 *(1+(px`2/px`1)^2)
by XCMPLX_1:8;
then (px`1)^2+(px`2)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)
<=1 *(1+(px`2/px`1)^2)
by A33,XCMPLX_1:88;
then A50: (px`1)^2+(px`2)^2<=1 *(1+(px`2/px`1)^2) by A33,XCMPLX_1:88;
1 *(1+(px`2/px`1)^2)
=1+(px`2)^2/(px`1)^2 by SQUARE_1:69;
then (px`1)^2+(px`2)^2-1<=1+(px`2)^2/(px`1)^2-1 by A50,REAL_1:49;
then (px`1)^2+(px`2)^2-1<=(px`2)^2/(px`1)^2 by XCMPLX_1:26;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2<=((px`2)^2/(px`1)^2)*(px`1)^2
by A48,AXIOMS:25;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2<=(px`2)^2 by A48,XCMPLX_1:88;
then ((px`1)^2+((px`2)^2-1))*(px`1)^2<=(px`2)^2 by XCMPLX_1:29;
then (px`1)^2*(px`1)^2+((px`2)^2-1)*(px`1)^2<=(px`2)^2 by XCMPLX_1:8;
then (px`1)^2*(px`1)^2+(px`1)^2*((px`2)^2-1)-(px`2)^2<=0
by REAL_2:106;
then A51: 0>=(px`1)^2*(px`1)^2+((px`1)^2*(px`2)^2-(px`1)^2*1)-(px`2)^2
by XCMPLX_1:40;
(px`1)^2*(px`1)^2+((px`1)^2*(px`2)^2-(px`1)^2*1)-(px`2)^2
= (px`1)^2*(px`1)^2+(px`1)^2*(px`2)^2-(px`1)^2*1-(px`2)^2
by XCMPLX_1:29
.= (px`1)^2*(px`1)^2-(px`1)^2*1+(px`1)^2*(px`2)^2-1 *(px`2)^2
by XCMPLX_1:29
.= (px`1)^2*((px`1)^2-1)+(px`1)^2*(px`2)^2-1 *(px`2)^2 by XCMPLX_1:40
.= (px`1)^2*((px`1)^2-1)+((px`1)^2*(px`2)^2-1 *(px`2)^2) by XCMPLX_1:
29
.= (px`1)^2*((px`1)^2-1)+((px`1)^2-1)*(px`2)^2 by XCMPLX_1:40
.= ((px`1)^2-1)*((px`1)^2+(px`2)^2) by XCMPLX_1:8;
then (px`1)^2-1<=0 & (px`1)^2-1>=0 or
(px`1)^2-1<=0 & (px`1)^2+(px`2)^2>=0 or
(px`1)^2+(px`2)^2<=0 & (px`1)^2-1>=0 or
(px`1)^2+(px`2)^2<=0 & (px`1)^2+(px`2)^2>=0 by A51,REAL_2:122;
then (px`1)^2-1+1<=0+1 & ((px`1)^2+(px`2)^2)>=0 by A48,A49,Th3,REAL_1:
55;
then (px`1)^2<=1 by XCMPLX_1:27;
then A52:px`1<=1 & px`1>= -1 by JGRAPH_2:5,SQUARE_1:59;
then px`2<=1 & 1>= -px`2 or px`2>= -1 & -px`2>=px`1
by A44,AXIOMS:22;
then px`2<=1 & -1<= --px`2 or px`2>= -1 & -px`2>= -1
by A52,AXIOMS:22,REAL_1:50;
then px`2<=1 & -1<=px`2 or px`2>= -1 & --px`2<= --1
by REAL_1:50;
then px in Kb by A1,A52;
hence ex x being set st x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by A25,A46,A47;
case A53:q<>0.REAL 2 & not(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
set px=|[q`1*sqrt(1+(q`1/q`2)^2),q`2*sqrt(1+(q`1/q`2)^2)]|;
A54:q<>0.REAL 2 & (q`1<=q`2 & -q`2<=q`1 or q`1>=q`2 & q`1<=-q`2)
by A53,JGRAPH_2:23;
A55: px`2 = q`2*sqrt(1+(q`1/q`2)^2) &
px`1 = q`1*sqrt(1+(q`1/q`2)^2) by EUCLID:56;
0<=(q`1/q`2)^2 by SQUARE_1:72;
then 1+(q`1/q`2)^2>0 by Th3;
then A56:sqrt(1+(q`1/q`2)^2)>0 by SQUARE_1:93;
0<=(px`1/px`2)^2 by SQUARE_1:72;
then A57:1+(px`1/px`2)^2>0 by Th3;
A58:px`1/px`2=q`1/q`2 by A55,A56,XCMPLX_1:92;
A59: q`2=q`2*sqrt(1+(q`1/q`2)^2)/(sqrt(1+(q`1/q`2)^2))by A56,XCMPLX_1:
90
.=px`2/(sqrt(1+(q`1/q`2)^2)) by EUCLID:56;
A60: q`1=q`1*sqrt(1+(q`1/q`2)^2)/(sqrt(1+(q`1/q`2)^2))by A56,XCMPLX_1:
90
.=px`1/(sqrt(1+(q`1/q`2)^2)) by EUCLID:56;
A61: |.q.|^2=q`2^2+q`1^2 by JGRAPH_3:10;
|.q.| >=0 by TOPRNS_1:26;
then A62: |.q.|^2<=1 by A25,SQUARE_1:59,77;
A63:now assume px`2=0 & px`1=0;
then A64:q`2*sqrt(1+(q`1/q`2)^2)=0 & q`1*sqrt(1+(q`1/q`2)^2)=0
by EUCLID:56;
then q`1=0 by A56,XCMPLX_1:6;
hence contradiction by A53,A56,A64,XCMPLX_1:6;
end;
q`1<=q`2 & -q`2<=q`1 or q`1>=q`2 &
q`1*sqrt(1+(q`1/q`2)^2) <= (-q`2)*sqrt(1+(q`1/q`2)^2)
by A54,A56,AXIOMS:25;
then q`1<=q`2 & (-q`2)*sqrt(1+(q`1/q`2)^2) <= q`1*sqrt(1+(q`1/q`2)^2)
or px`1>=px`2 & px`1<=-px`2 by A55,A56,AXIOMS:25,XCMPLX_1:175;
then A65:px`1<=px`2 & -px`2<=px`1 or px`1>=px`2 & px`1<=-px`2
by A55,A56,AXIOMS:25,XCMPLX_1:175;
then A66:Sq_Circ.px=|[px`1/sqrt(1+(px`1/px`2)^2),px`2/sqrt(1+(px`1/px`2)^2)
]|
by A63,JGRAPH_2:11,JGRAPH_3:14;
px`1<=px`2 & --px`2>=-px`1 or px`1>=px`2 & px`1<=-px`2
by A65,REAL_1:50;
then A67:px`1<=px`2 & px`2>=-px`1 or px`1>=px`2 & -px`1>=--px`2
by REAL_1:50;
A68:px`2/sqrt(1+(px`1/px`2)^2)=q`2 by A55,A56,A58,XCMPLX_1:90;
px`1/sqrt(1+(px`1/px`2)^2)=q`1 by A55,A56,A58,XCMPLX_1:90;
then A69:q=Sq_Circ.px by A66,A68,EUCLID:57;
A70: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
not px`2=0 by A63,A65;
then A71: (px`2)^2>0 by SQUARE_1:74;
A72: (px`1)^2>=0 by SQUARE_1:72;
(px`2)^2/(sqrt(1+(px`1/px`2)^2))^2+(px`1/sqrt(1+(px`1/px`2)^2))^2<=1
by A58,A59,A60,A61,A62,SQUARE_1:69;
then (px`2)^2/(sqrt(1+(px`1/px`2)^2))^2+(px`1)^2/(sqrt(1+(px`1/px`2)^2))
^2<=1
by SQUARE_1:69;
then (px`2)^2/(1+(px`1/px`2)^2)+(px`1)^2/(sqrt(1+(px`1/px`2)^2))^2<=1
by A57,SQUARE_1:def 4;
then (px`2)^2/(1+(px`1/px`2)^2)+(px`1)^2/(1+(px`1/px`2)^2)<=1
by A57,SQUARE_1:def 4;
then ((px`2)^2/(1+(px`1/px`2)^2)
+(px`1)^2/(1+(px`1/px`2)^2))*(1+(px`1/px`2)^2)<=1 *(1+(px`1/px`2)^2)
by A57,AXIOMS:25;
then (px`2)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)
+(px`1)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)<=1 *(1+(px`1/px`2)^2)
by XCMPLX_1:8;
then (px`2)^2+(px`1)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)
<=1 *(1+(px`1/px`2)^2)
by A57,XCMPLX_1:88;
then A73: (px`2)^2+(px`1)^2<=1 *(1+(px`1/px`2)^2) by A57,XCMPLX_1:88;
1 *(1+(px`1/px`2)^2)
=1+(px`1)^2/(px`2)^2 by SQUARE_1:69;
then (px`2)^2+(px`1)^2-1<=1+(px`1)^2/(px`2)^2-1 by A73,REAL_1:49;
then (px`2)^2+(px`1)^2-1<=(px`1)^2/(px`2)^2 by XCMPLX_1:26;
then ((px`2)^2+(px`1)^2-1)*(px`2)^2<=((px`1)^2/(px`2)^2)*(px`2)^2
by A71,AXIOMS:25;
then ((px`2)^2+(px`1)^2-1)*(px`2)^2<=(px`1)^2 by A71,XCMPLX_1:88;
then ((px`2)^2+((px`1)^2-1))*(px`2)^2<=(px`1)^2 by XCMPLX_1:29;
then (px`2)^2*(px`2)^2+((px`1)^2-1)*(px`2)^2<=(px`1)^2 by XCMPLX_1:8;
then (px`2)^2*(px`2)^2+(px`2)^2*((px`1)^2-1)-(px`1)^2<=0
by REAL_2:106;
then A74: 0>=(px`2)^2*(px`2)^2+((px`2)^2*(px`1)^2-(px`2)^2*1)-(px`1)^2
by XCMPLX_1:40;
(px`2)^2*(px`2)^2+((px`2)^2*(px`1)^2-(px`2)^2*1)-(px`1)^2
= (px`2)^2*(px`2)^2+(px`2)^2*(px`1)^2-(px`2)^2*1-(px`1)^2
by XCMPLX_1:29
.= (px`2)^2*(px`2)^2-(px`2)^2*1+(px`2)^2*(px`1)^2-1 *(px`1)^2
by XCMPLX_1:29
.= (px`2)^2*((px`2)^2-1)+(px`2)^2*(px`1)^2-1 *(px`1)^2 by XCMPLX_1:40
.= (px`2)^2*((px`2)^2-1)+((px`2)^2*(px`1)^2-1 *(px`1)^2) by XCMPLX_1:
29
.= (px`2)^2*((px`2)^2-1)+((px`2)^2-1)*(px`1)^2 by XCMPLX_1:40
.= ((px`2)^2-1)*((px`2)^2+(px`1)^2) by XCMPLX_1:8;
then ((px`2)^2-1<=0 or ((px`2)^2+(px`1)^2)<=0)
&((px`2)^2-1>=0 or (px`2)^2+(px`1)^2>=0) by A74,REAL_2:122;
then (px`2)^2-1+1<=0+1 & ((px`2)^2+(px`1)^2)>=0 by A71,A72,Th3,REAL_1:
55;
then (px`2)^2<=1 by XCMPLX_1:27;
then A75:px`2<=1 & px`2>= -1 by JGRAPH_2:5,SQUARE_1:59;
then px`1<=1 & 1>= -px`1 or px`1>= -1 & -px`1>=px`2
by A67,AXIOMS:22;
then px`1<=1 & -1<= --px`1 or px`1>= -1 & -px`1>= -1
by A75,AXIOMS:22,REAL_1:50;
then px`1<=1 & -1<=px`1 or px`1>= -1 & --px`1<= --1
by REAL_1:50;
then px in Kb by A1,A75;
hence ex x being set st x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by A25,A69,A70;
end;
hence thesis by FUNCT_1:def 12;
end;
theorem Th37: for Kb,Cb being Subset of TOP-REAL 2 st
Kb={p: not(-1 <p`1 & p`1< 1 & -1 <p`2 & p`2< 1)}&
Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|>=1} holds Sq_Circ.:Kb=Cb
proof let Kb,Cb be Subset of TOP-REAL 2;
assume
A1:
Kb={p: not(-1 <p`1 & p`1< 1 & -1 <p`2 & p`2< 1)}&
Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|>=1};
thus Sq_Circ.:Kb c= Cb
proof let y be set;assume y in Sq_Circ.:Kb;
then consider x being set such that
A2: x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by FUNCT_1:def 12;
consider q being Point of TOP-REAL 2 such that
A3:q=x &( not(-1 <q`1 & q`1< 1 & -1 <q`2 & q`2< 1) ) by A1,A2;
now per cases;
case q=0.REAL 2;
then q`1=0 & q`2=0 by EUCLID:56,58;
hence contradiction by A3;
case A4:q<>0.REAL 2 &
(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then A5:Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|
by JGRAPH_3:def 1;
A6: not(-1 <q`2 & q`2< 1) implies -1>=q`1 or q`1>=1
proof assume A7: not(-1 <q`2 & q`2< 1);
now per cases by A7;
case A8: -1>=q`2;
then -q`1<= -1 or q`2>=q`1 & q`2<= -q`1 by A4,AXIOMS:22;
hence -1>=q`1 or q`1>=1 by A8,AXIOMS:22,REAL_1:50;
case q`2>=1;
then 1<=q`1 or 1<= -q`1 by A4,AXIOMS:22;
then 1<=q`1 or --q`1<= -1 by REAL_1:50;
hence -1>=q`1 or q`1>=1;
end;
hence -1>=q`1 or q`1>=1;
end;
A9: (|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`1
= q`1/sqrt(1+(q`2/q`1)^2) &
(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`2
= q`2/sqrt(1+(q`2/q`1)^2) by EUCLID:56;
0<=(q`2/q`1)^2 by SQUARE_1:72;
then A10:1+(q`2/q`1)^2>0 by Th3;
A11: now assume A12: q`1=0;
then q`2=0 by A4;
hence contradiction by A4,A12,EUCLID:57,58;
end;
then A13: (q`1)^2>0 by SQUARE_1:74;
A14: (q`1)^2+(q`2)^2 <>0 by A11,COMPLEX1:2;
(q`1)^2>=1^2 by A3,A6,JGRAPH_2:6;
then A15: sqrt((q`1)^2)>=1 by SQUARE_1:59,83,94;
A16: |.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|^2
=((q`1)/sqrt(1+(q`2/(q`1))^2))^2+(q`2/sqrt(1+(q`2/(q`1))^2))^2
by A9,JGRAPH_3:10
.=(q`1)^2/(sqrt(1+(q`2/(q`1))^2))^2+(q`2/sqrt(1+(q`2/(q`1))^2))^2
by SQUARE_1:69
.=(q`1)^2/(sqrt(1+(q`2/(q`1))^2))^2
+(q`2)^2/(sqrt(1+(q`2/(q`1))^2))^2 by SQUARE_1:69
.=(q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by A10,SQUARE_1:def 4
.=(q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(1+(q`2/q`1)^2)
by A10,SQUARE_1:def 4
.=((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2) by XCMPLX_1:63
.=((q`1)^2+(q`2)^2)/(1+(q`2)^2/(q`1)^2) by SQUARE_1:69
.=((q`1)^2+(q`2)^2)/((q`1)^2/(q`1)^2+(q`2)^2/(q`1)^2)
by A13,XCMPLX_1:60
.=((q`1)^2+(q`2)^2)/(((q`1)^2+(q`2)^2)/(q`1)^2)
by XCMPLX_1:63
.=(q`1)^2*(((q`1)^2+(q`2)^2)/((q`1)^2+(q`2)^2))
by XCMPLX_1:82
.=(q`1)^2*1 by A14,XCMPLX_1:60
.=(q`1)^2;
0<=|.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|
by TOPRNS_1:26;
then |.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|>=1
by A15,A16,SQUARE_1:89;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|>=1
by A2,A3,A5;
case A17:q<>0.REAL 2 &
not(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then A18:Sq_Circ.q=|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|
by JGRAPH_3:def 1;
A19: (|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|)`1
= q`1/sqrt(1+(q`1/q`2)^2) &
(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|)`2
= q`2/sqrt(1+(q`1/q`2)^2) by EUCLID:56;
0<=(q`1/q`2)^2 by SQUARE_1:72;
then A20:1+(q`1/q`2)^2>0 by Th3;
A21: q`2 <> 0 by A17,REAL_1:66;
then A22: (q`2)^2>0 by SQUARE_1:74;
A23: (q`1)^2+(q`2)^2 <>0 by A21,COMPLEX1:2;
not(-1 <q`1 & q`1< 1) implies -1>=q`2 or q`2>=1
proof assume A24: not(-1 <q`1 & q`1< 1);
now per cases by A24;
case A25: -1>=q`1;
then q`2<= -1 or q`1<q`2 & -q`2<= --q`1 by A17,AXIOMS:22,REAL_1:50;
then -q`2<= -1 or -1>=q`2 by A25,AXIOMS:22;
hence -1>=q`2 or q`2>=1 by REAL_1:50;
case A26: q`1>=1;
--q`1<= -q`2 & q`2<=q`1 or q`2>=q`1 & q`2>= -q`1
by A17,REAL_1:50;
then 1<= -q`2 or q`2>=q`1 & q`2>= -q`1 by A26,AXIOMS:22;
then -1>= --q`2 or 1<=q`2 by A26,AXIOMS:22,REAL_1:50;
hence -1>=q`2 or q`2>=1;
end;
hence -1>=q`2 or q`2>=1;
end;
then (q`2)^2>=1^2 by A3,JGRAPH_2:6;
then A27: sqrt((q`2)^2)>=1 by SQUARE_1:59,83,94;
A28: |.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|^2
=((q`1)/sqrt(1+(q`1/(q`2))^2))^2+(q`2/sqrt(1+(q`1/(q`2))^2))^2
by A19,JGRAPH_3:10
.=(q`1)^2/(sqrt(1+(q`1/(q`2))^2))^2+(q`2/sqrt(1+(q`1/(q`2))^2))^2
by SQUARE_1:69
.=(q`1)^2/(sqrt(1+(q`1/(q`2))^2))^2
+(q`2)^2/(sqrt(1+(q`1/(q`2))^2))^2 by SQUARE_1:69
.=(q`1)^2/(1+(q`1/q`2)^2)+(q`2)^2/(sqrt(1+(q`1/q`2)^2))^2
by A20,SQUARE_1:def 4
.=(q`1)^2/(1+(q`1/q`2)^2)+(q`2)^2/(1+(q`1/q`2)^2)
by A20,SQUARE_1:def 4
.=((q`1)^2+(q`2)^2)/(1+(q`1/q`2)^2) by XCMPLX_1:63
.=((q`1)^2+(q`2)^2)/(1+(q`1)^2/(q`2)^2) by SQUARE_1:69
.=((q`1)^2+(q`2)^2)/((q`1)^2/(q`2)^2+(q`2)^2/(q`2)^2)
by A22,XCMPLX_1:60
.=((q`1)^2+(q`2)^2)/(((q`1)^2+(q`2)^2)/(q`2)^2) by XCMPLX_1:63
.=(q`2)^2*(((q`1)^2+(q`2)^2)/((q`1)^2+(q`2)^2)) by XCMPLX_1:82
.=(q`2)^2*1 by A23,XCMPLX_1:60
.=(q`2)^2;
0<=|.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|
by TOPRNS_1:26;
then |.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|>=1
by A27,A28,SQUARE_1:89;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|>=1
by A2,A3,A18;
end;
hence y in Cb by A1;
end;
let y be set;assume y in Cb;
then consider p2 being Point of TOP-REAL 2 such that
A29: p2=y & |.p2.|>=1 by A1;
set q=p2;
now per cases;
case q=0.REAL 2;
then |.q.|=0 by TOPRNS_1:24;
hence contradiction by A29;
case A30:q<>0.REAL 2 &
(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
set px=|[q`1*sqrt(1+(q`2/q`1)^2),q`2*sqrt(1+(q`2/q`1)^2)]|;
A31: px`1 = q`1*sqrt(1+(q`2/q`1)^2) &
px`2 = q`2*sqrt(1+(q`2/q`1)^2) by EUCLID:56;
0<=(q`2/q`1)^2 by SQUARE_1:72;
then 1+(q`2/q`1)^2>0 by Th3;
then A32:sqrt(1+(q`2/q`1)^2)>0 by SQUARE_1:93;
0<=(px`2/px`1)^2 by SQUARE_1:72;
then A33:1+(px`2/px`1)^2>0 by Th3;
A34:px`2/px`1=q`2/q`1 by A31,A32,XCMPLX_1:92;
A35: q`1=q`1*sqrt(1+(q`2/q`1)^2)/(sqrt(1+(q`2/q`1)^2))by A32,XCMPLX_1:
90
.=px`1/(sqrt(1+(q`2/q`1)^2)) by EUCLID:56;
A36: q`2=q`2*sqrt(1+(q`2/q`1)^2)/(sqrt(1+(q`2/q`1)^2))by A32,XCMPLX_1:
90
.=px`2/(sqrt(1+(q`2/q`1)^2)) by EUCLID:56;
A37: |.q.|^2=q`1^2+q`2^2 by JGRAPH_3:10;
A38: |.q.|^2>=1 by A29,SQUARE_1:59,77;
A39:now assume px`1=0 & px`2=0;
then A40:q`1*sqrt(1+(q`2/q`1)^2)=0 & q`2*sqrt(1+(q`2/q`1)^2)=0
by EUCLID:56;
then A41:q`1=0 by A32,XCMPLX_1:6;
q`2=0 by A32,A40,XCMPLX_1:6;
hence contradiction by A30,A41,EUCLID:57,58;
end;
q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 &
q`2*sqrt(1+(q`2/q`1)^2) <= (-q`1)*sqrt(1+(q`2/q`1)^2)
by A30,A32,AXIOMS:25;
then q`2<=q`1 & (-q`1)*sqrt(1+(q`2/q`1)^2) <= q`2*sqrt(1+(q`2/q`1)^2)
or px`2>=px`1 & px`2<=-px`1 by A31,A32,AXIOMS:25,XCMPLX_1:175;
then A42:px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1
by A31,A32,AXIOMS:25,XCMPLX_1:175;
then A43:Sq_Circ.px=|[px`1/sqrt(1+(px`2/px`1)^2),px`2/sqrt(1+(px`2/px`1)^2)
]|
by A39,JGRAPH_2:11,JGRAPH_3:def 1;
A44:px`1/sqrt(1+(px`2/px`1)^2)=q`1 by A31,A32,A34,XCMPLX_1:90;
px`2/sqrt(1+(px`2/px`1)^2)=q`2 by A31,A32,A34,XCMPLX_1:90;
then A45:q=Sq_Circ.px by A43,A44,EUCLID:57;
A46: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
not px`1=0 by A39,A42;
then A47: (px`1)^2>0 by SQUARE_1:74;
(px`2)^2>=0 by SQUARE_1:72;
then A48: (px`1)^2+(px`2)^2>0 by A47,Th3;
(px`1)^2/(sqrt(1+(px`2/px`1)^2))^2+(px`2/sqrt(1+(px`2/px`1)^2))^2>=1
by A34,A35,A36,A37,A38,SQUARE_1:69;
then (px`1)^2/(sqrt(1+(px`2/px`1)^2))^2+(px`2)^2/(sqrt(1+(px`2/px`1)^2))
^2>=1
by SQUARE_1:69;
then (px`1)^2/(1+(px`2/px`1)^2)+(px`2)^2/(sqrt(1+(px`2/px`1)^2))^2>=1
by A33,SQUARE_1:def 4;
then (px`1)^2/(1+(px`2/px`1)^2)+(px`2)^2/(1+(px`2/px`1)^2)>=1
by A33,SQUARE_1:def 4;
then ((px`1)^2/(1+(px`2/px`1)^2)
+(px`2)^2/(1+(px`2/px`1)^2))*(1+(px`2/px`1)^2)>=1 *(1+(px`2/px`1)^2)
by A33,AXIOMS:25;
then (px`1)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)
+(px`2)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)>=1 *(1+(px`2/px`1)^2)
by XCMPLX_1:8;
then (px`1)^2+(px`2)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)
>=1 *(1+(px`2/px`1)^2) by A33,XCMPLX_1:88;
then A49: (px`1)^2+(px`2)^2>=1 *(1+(px`2/px`1)^2) by A33,XCMPLX_1:88;
1 *(1+(px`2/px`1)^2)
=1+(px`2)^2/(px`1)^2 by SQUARE_1:69;
then (px`1)^2+(px`2)^2-1>=1+(px`2)^2/(px`1)^2-1 by A49,REAL_1:49;
then (px`1)^2+(px`2)^2-1>=(px`2)^2/(px`1)^2 by XCMPLX_1:26;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2>=((px`2)^2/(px`1)^2)*(px`1)^2
by A47,AXIOMS:25;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2>=(px`2)^2 by A47,XCMPLX_1:88;
then ((px`1)^2+((px`2)^2-1))*(px`1)^2>=(px`2)^2 by XCMPLX_1:29;
then (px`1)^2*(px`1)^2+((px`2)^2-1)*(px`1)^2>=(px`2)^2 by XCMPLX_1:8;
then (px`1)^2*(px`1)^2+(px`1)^2*((px`2)^2-1)-(px`2)^2>=0
by SQUARE_1:12;
then A50: 0<=(px`1)^2*(px`1)^2+((px`1)^2*(px`2)^2-(px`1)^2*1)-(px`2)^2
by XCMPLX_1:40;
(px`1)^2*(px`1)^2+((px`1)^2*(px`2)^2-(px`1)^2*1)-(px`2)^2
= (px`1)^2*(px`1)^2+(px`1)^2*(px`2)^2-(px`1)^2*1-(px`2)^2
by XCMPLX_1:29
.= (px`1)^2*(px`1)^2-(px`1)^2*1+(px`1)^2*(px`2)^2-1 *(px`2)^2
by XCMPLX_1:29
.= (px`1)^2*((px`1)^