0 and A3: p`2<>0; set a=|.p.|; A4: (|.p.|)^2 =(p`1)^2+(p`2)^2 by JGRAPH_3:1; then a^2-(p`1)^2+(p`1)^2>0+(p`1)^2 by A3,SQUARE_1:12,XREAL_1:8; then A5: -a

0+(p`2)^2 by A2,A4,SQUARE_1:12,XREAL_1:8; then A6: -a

=-1 by A1,XREAL_1:24;
hence thesis by A1,A5,A6,XXREAL_0:2;
end;
theorem
for a,b,d,e,r3 being Real,PM,PM2 being non empty MetrStruct, x being
Element of PM, x2 being Element of PM2 st d<=a & a<=b & b<=e & PM=
Closed-Interval-MSpace(a,b) & PM2=Closed-Interval-MSpace(d,e) & x=x2 holds Ball
(x,r3) c= Ball(x2,r3)
proof
let a,b,d,e,r3 be Real,PM,PM2 be non empty MetrStruct, x be Element of PM,
x2 be Element of PM2;
assume that
A1: d<=a and
A2: a<=b and
A3: b<=e and
A4: PM=Closed-Interval-MSpace(a,b) and
A5: PM2=Closed-Interval-MSpace(d,e) and
A6: x=x2;
a<=e by A2,A3,XXREAL_0:2;
then
A7: a in [.d,e.] by A1,XXREAL_1:1;
let z be object;
assume z in Ball(x,r3);
then z in {y where y is Element of PM: dist(x,y) < r3 } by METRIC_1:17;
then consider y being Element of PM such that
A8: y=z & dist(x,y)**=d & t1>=t2 & s1 in [.a,b.]
& s2 in [.a,b.] holds s1<=s2
proof
let a,b,d,e,s1,s2,t1,t2 be Real,
h be Function of Closed-Interval-TSpace(a,b)
,Closed-Interval-TSpace(d,e);
assume that
A1: h is being_homeomorphism and
A2: h.s1=t1 and
A3: h.s2=t2 and
A4: h.b=d and
A5: e>=d and
A6: t1>=t2 and
A7: s1 in [.a,b.] and
A8: s2 in [.a,b.];
A9: s1<=b by A7,XXREAL_1:1;
reconsider C=[.d,e.] as non empty Subset of R^1 by A5,TOPMETR:17,XXREAL_1:1;
A10: R^1|C=Closed-Interval-TSpace(d,e) by A5,TOPMETR:19;
A11: a<=s1 by A7,XXREAL_1:1;
then
A12: the carrier of Closed-Interval-TSpace(a,b) =[.a,b.] by A9,TOPMETR:18
,XXREAL_0:2;
then reconsider B1=[.s1,b.] as Subset of Closed-Interval-TSpace(a,b) by A11,
XXREAL_1:34;
A13: dom h=[#](Closed-Interval-TSpace(a,b)) by A1,TOPS_2:def 5
.=[.a,b.] by A11,A9,TOPMETR:18,XXREAL_0:2;
A14: a<=s2 by A8,XXREAL_1:1;
then reconsider B=[.s2,s1.] as Subset of Closed-Interval-TSpace(a,b) by A9
,A12,XXREAL_1:34;
reconsider Bb=[.s2,s1.] as Subset of Closed-Interval-TSpace(a,b) by A14,A9
,A12,XXREAL_1:34;
reconsider f3=h|Bb as Function of Closed-Interval-TSpace(a,b)|B,
Closed-Interval-TSpace(d,e) by PRE_TOPC:9;
assume
A15: s1>s2;
then
A16: Closed-Interval-TSpace(s2,s1) =Closed-Interval-TSpace(a,b)|B by A14,A9,
TOPMETR:23;
then f3 is Function of Closed-Interval-TSpace(s2,s1),R^1 by A10,JORDAN6:3;
then reconsider f=h|B as Function of Closed-Interval-TSpace(s2,s1),R^1;
s2 in B by A15,XXREAL_1:1;
then
A17: f.s2=t2 by A3,FUNCT_1:49;
set t=(t1+t2)/2;
A18: the carrier of Closed-Interval-TSpace(d,e) =[.d,e.] by A5,TOPMETR:18;
h is one-to-one by A1,TOPS_2:def 5;
then t1<>t2 by A2,A3,A7,A8,A13,A15,FUNCT_1:def 4;
then
A19: t1>t2 by A6,XXREAL_0:1;
then t1+t1>t1+t2 by XREAL_1:8;
then
A20: (2*t1)/2>t by XREAL_1:74;
dom f=the carrier of Closed-Interval-TSpace(s2,s1) by FUNCT_2:def 1;
then dom f=[.s2,s1.] by A15,TOPMETR:18;
then s2 in dom f by A15,XXREAL_1:1;
then t2 in rng f3 by A17,FUNCT_1:def 3;
then
A21: d<=t2 by A18,XXREAL_1:1;
t1+t2>t2+t2 by A19,XREAL_1:8;
then
A22: (2*t2)/2 b & c <> d & (f.O)`1=a & c <=(f.O)`2 & (f.O)`2 <=d
& (f.I)`1=b & c <=(f.I)`2 & (f.I)`2 <=d & (g.O)`2=c & a <=(g.O)`1 & (g.O)`1 <=b
& (g.I)`2=d & a <=(g.I)`1 & (g.I)`1 <=b & (for r being Point of I[01] holds (a
>=(f.r)`1 or (f.r)`1>=b or c >=(f.r)`2 or (f.r)`2>=d) & (a >=(g.r)`1 or (g.r)`1
>=b or c >=(g.r)`2 or (g.r)`2>=d)) holds rng f meets rng g
proof
let f,g be Function of I[01],TOP-REAL 2,a,b,c,d be Real, O,I be Point of
I[01];
assume that
A1: O=0 & I=1 & f is continuous one-to-one & g is continuous one-to-one and
A2: a <> b and
A3: c <> d and
A4: (f.O)`1=a and
A5: c <=(f.O)`2 & (f.O)`2 <=d and
A6: (f.I)`1=b & c <=(f.I)`2 & (f.I)`2 <=d & (g.O)`2=c and
A7: a <=(g.O)`1 & (g.O)`1 <=b and
A8: (g.I)`2=d & a <=(g.I)`1 &( (g.I)`1 <=b & for r being Point of I[01]
holds (a >=(f.r)`1 or (f.r)`1>=b or c >=(f.r)`2 or (f.r)`2>=d) & (a >=(g.r)`1
or (g.r)`1>=b or c >=(g.r)`2 or (g.r) `2 >=d) );
c <= d by A5,XXREAL_0:2;
then
A9: c < d by A3,XXREAL_0:1;
a <= b by A7,XXREAL_0:2;
then a < b by A2,XXREAL_0:1;
hence thesis by A1,A4,A5,A6,A7,A8,A9,JGRAPH_2:45;
end;
Lm1: 0 in [.0,1.] by XXREAL_1:1;
Lm2: 1 in [.0,1.] by XXREAL_1:1;
theorem Th12:
for f being Function of I[01],TOP-REAL 2 st f is continuous
one-to-one ex f2 being Function of I[01],TOP-REAL 2 st f2.0=f.1 & f2.1=f.0 &
rng f2=rng f & f2 is continuous & f2 is one-to-one
proof
let f be Function of I[01],TOP-REAL 2;
A1: I[01] is compact by HEINE:4,TOPMETR:20;
A2: dom f=the carrier of I[01] by FUNCT_2:def 1;
then reconsider P=rng f as non empty Subset of TOP-REAL 2 by Lm1,BORSUK_1:40
,FUNCT_1:3;
f.1 in rng f & f.0 in rng f by A2,Lm1,Lm2,BORSUK_1:40,FUNCT_1:3;
then reconsider p1=f.0,p2=f.1 as Point of TOP-REAL 2;
assume f is continuous one-to-one;
then ex f1 being Function of I[01],(TOP-REAL 2)|P st f1=f & f1 is
being_homeomorphism by A1,JGRAPH_1:46;
then P is_an_arc_of p1,p2 by TOPREAL1:def 1;
then P is_an_arc_of p2,p1 by JORDAN5B:14;
then consider f3 being Function of I[01], (TOP-REAL 2)|P such that
A3: f3 is being_homeomorphism and
A4: f3.0 = p2 & f3.1 = p1 by TOPREAL1:def 1;
A5: ex f4 being Function of I[01], (TOP-REAL 2) st f3=f4 & f4 is continuous
& f4 is one-to-one by A3,JORDAN7:15;
rng f3=[#]((TOP-REAL 2)|P) by A3,TOPS_2:def 5
.=P by PRE_TOPC:def 5;
hence thesis by A4,A5;
end;
reserve p,q for Point of TOP-REAL 2;
theorem Th13:
for f,g being Function 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
KXN & f.I in KXP & 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 Function 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 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 KXN & f.I in KXP & g.O in KYP & g.I in KYN &
rng f c= C0 & rng g c= C0;
then
ex g2 being Function of I[01],TOP-REAL 2 st g2.0=g.1 & g2 .1=g.0 & rng g2
=rng g & g2 is continuous one-to-one by Th12;
hence thesis by A1,JGRAPH_3:44;
end;
theorem Th14:
for f,g being Function 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
KXN & f.I in KXP & 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 Function 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 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 KXN & f.I in KXP & g.O in KYN & g.I in
KYP & rng f c= C0 & rng g c= C0;
A2: dom g=the carrier of I[01] by FUNCT_2:def 1;
reconsider gg=Sq_Circ"*g as Function of I[01],TOP-REAL 2 by FUNCT_2:13
,JGRAPH_3:29;
reconsider ff=Sq_Circ"*f as Function of I[01],TOP-REAL 2 by FUNCT_2:13
,JGRAPH_3:29;
A3: dom gg=the carrier of I[01] by FUNCT_2:def 1;
A4: dom ff=the carrier of I[01] by FUNCT_2:def 1;
A5: (ff.O)`1=-1 & (ff.I)`1=1 & (gg.O)`2=-1 & (gg.I)`2=1
proof
reconsider pz=gg.O as Point of TOP-REAL 2;
reconsider py=ff.I as Point of TOP-REAL 2;
reconsider px=ff.O as Point of TOP-REAL 2;
set q=px;
A6: (|[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) by EUCLID:52;
reconsider pu=gg.I as Point of TOP-REAL 2;
A7: (|[py`1/sqrt(1+(py`2/py`1)^2),py`2/sqrt(1+(py`2/py`1)^2)]|)`1 = py`1/
sqrt(1+(py`2/py`1)^2) by EUCLID:52;
consider p2 being Point of TOP-REAL 2 such that
A8: f.I=p2 and
A9: |.p2.|=1 and
A10: p2`2<=p2`1 and
A11: p2`2>=-p2`1 by A1;
A12: (ff.I)=(Sq_Circ").(f.I) by A4,FUNCT_1:12;
then
A13: p2=Sq_Circ.py by A8,FUNCT_1:32,JGRAPH_3:22,43;
A14: p2<>0.TOP-REAL 2 by A9,TOPRNS_1:23;
then
A15: Sq_Circ".p2=|[p2`1*sqrt(1+(p2`2/p2`1)^2),p2`2*sqrt(1+(p2`2/p2`1) ^2 )
]| by A10,A11,JGRAPH_3:28;
then
A16: py`1 = p2`1*sqrt(1+(p2`2/p2`1)^2) by A12,A8,EUCLID:52;
(p2`2/p2`1)^2 >=0 by XREAL_1:63;
then
A17: sqrt(1+(p2`2/p2`1)^2)>0 by SQUARE_1:25;
A18: py`2 = p2`2*sqrt(1+(p2`2/p2`1)^2) by A12,A8,A15,EUCLID:52;
A19: now
assume py`1=0 & py`2=0;
then p2`1=0 & p2`2=0 by A16,A18,A17,XCMPLX_1:6;
hence contradiction by A14,EUCLID:53,54;
end;
A20: p2`2<=p2`1 & (-p2`1)*sqrt(1+(p2`2/p2`1)^2) <= p2`2*sqrt(1+(p2`2/p2`1
) ^2 ) or py`2>=py`1 & py`2<=-py`1 by A10,A11,A17,XREAL_1:64;
then p2`2*sqrt(1+(p2`2/p2`1)^2) <= p2`1*sqrt(1+(p2`2/p2`1)^2) & -py `1<=
py `2 or py`2>=py`1 & py`2<=-py`1 by A12,A8,A15,A16,A17,EUCLID:52
,XREAL_1:64;
then
A21: Sq_Circ.py=|[py`1/sqrt(1+(py`2/py`1)^2),py`2/sqrt(1+(py`2/py`1)^2)]|
by A16,A18,A19,JGRAPH_2:3,JGRAPH_3:def 1;
A22: (py`2/py`1)^2 >=0 by XREAL_1:63;
then
A23: sqrt(1+(py`2/py`1)^2)>0 by SQUARE_1:25;
A24: now
assume
A25: py`1=-1;
-p2`2<=--p2`1 by A11,XREAL_1:24;
then -p2`2<0 by A13,A21,A7,A22,A25,SQUARE_1:25,XREAL_1:141;
then --p2`2>-0;
hence contradiction by A10,A13,A21,A23,A25,EUCLID:52;
end;
(|[py`1/sqrt(1+(py`2/py`1)^2),py`2/sqrt(1+(py`2/py`1)^2)]|)`2 = py`2/
sqrt(1+(py`2/py`1)^2) by EUCLID:52;
then
(|.p2.|)^2= (py`1/sqrt(1+(py`2/py`1)^2))^2+(py`2/sqrt(1+(py`2/py`1)^2
) ) ^2 by A13,A21,A7,JGRAPH_3:1
.= (py`1)^2/(sqrt(1+(py`2/py`1)^2))^2+(py`2/sqrt(1+(py`2/py`1)^2))^2
by XCMPLX_1:76
.= (py`1)^2/(sqrt(1+(py`2/py`1)^2))^2 +(py`2)^2/(sqrt(1+(py`2/py`1)^2)
)^2 by XCMPLX_1:76
.= (py`1)^2/(1+(py`2/py`1)^2)+(py`2)^2/(sqrt(1+(py`2/py`1)^2))^2 by A22,
SQUARE_1:def 2
.= (py`1)^2/(1+(py`2/py`1)^2)+(py`2)^2/(1+(py`2/py`1)^2) by A22,
SQUARE_1:def 2
.= ((py`1)^2+(py`2)^2)/(1+(py`2/py`1)^2) by XCMPLX_1:62;
then
((py`1)^2+(py`2)^2)/(1+(py`2/py`1)^2)*(1+(py`2/py`1)^2) =(1)*(1+(py`2
/py`1)^2) by A9;
then ((py`1)^2+(py`2)^2)=(1+(py`2/py`1)^2) by A22,XCMPLX_1:87;
then
A26: (py`1)^2+(py`2)^2-1=(py`2)^2/(py`1)^2 by XCMPLX_1:76;
py`1<>0 by A16,A18,A17,A19,A20,XREAL_1:64;
then ((py`1)^2+(py`2)^2-1)*(py`1)^2=(py`2)^2 by A26,XCMPLX_1:6,87;
then
A27: ((py`1)^2-1)*((py`1)^2+(py`2)^2)=0;
((py`1)^2+(py`2)^2)<>0 by A19,COMPLEX1:1;
then (py`1-1)*(py`1+1)=0 by A27,XCMPLX_1:6;
then
A28: py`1-1=0 or py`1+1=0 by XCMPLX_1:6;
A29: (|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|)`2 = pz`2
/ sqrt(1+(pz`1/pz`2)^2) by EUCLID:52;
consider p1 being Point of TOP-REAL 2 such that
A30: f.O=p1 and
A31: |.p1.|=1 and
A32: p1`2>=p1`1 and
A33: p1`2<=-p1`1 by A1;
(p1`2/p1`1)^2 >=0 by XREAL_1:63;
then
A34: sqrt(1+(p1`2/p1`1)^2)>0 by SQUARE_1:25;
A35: (ff.O)=(Sq_Circ").(f.O) by A4,FUNCT_1:12;
then
A36: p1=Sq_Circ.px by A30,FUNCT_1:32,JGRAPH_3:22,43;
A37: p1<>0.TOP-REAL 2 by A31,TOPRNS_1:23;
then
Sq_Circ".p1=|[p1`1*sqrt(1+(p1`2/p1`1)^2),p1`2*sqrt(1+(p1`2/p1`1) ^2 )
]| by A32,A33,JGRAPH_3:28;
then
A38: px`1 = p1`1*sqrt(1+(p1`2/p1`1)^2) & px`2 = p1`2*sqrt(1+(p1`2/p1`1)^2)
by A35,A30,EUCLID:52;
A39: now
assume px`1=0 & px`2=0;
then p1`1=0 & p1`2=0 by A38,A34,XCMPLX_1:6;
hence contradiction by A37,EUCLID:53,54;
end;
p1`2<=p1`1 & -p1`1<=p1`2 or p1`2>=p1`1 & p1`2*sqrt(1+(p1`2/p1`1)^2)
<= (-p1`1)*sqrt(1+(p1`2/p1`1)^2) by A32,A33,A34,XREAL_1:64;
then
A40: p1`2<=p1`1 & (-p1`1)*sqrt(1+(p1`2/p1`1)^2) <= p1`2*sqrt(1+(p1`2/ p1`1
)^2) or px`2>=px`1 & px`2<=-px`1 by A38,A34,XREAL_1:64;
then px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1 by A38,A34,
XREAL_1:64;
then
A41: Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]| by A39,
JGRAPH_2:3,JGRAPH_3:def 1;
A42: (q`2/q`1)^2 >=0 by XREAL_1:63;
then
A43: sqrt(1+(q`2/q`1)^2)>0 by SQUARE_1:25;
A44: now
assume
A45: px`1=1;
-p1`2>=--p1`1 by A33,XREAL_1:24;
then -p1`2>0 by A36,A41,A6,A43,A45,XREAL_1:139;
then --p1`2<-0;
hence contradiction by A32,A36,A41,A43,A45,EUCLID:52;
end;
(|[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:52;
then (|.p1.|)^2= (q`1/sqrt(1+(q`2/q`1)^2))^2+(q`2/sqrt(1+(q`2/q`1)^2)) ^2
by A36,A41,A6,JGRAPH_3:1
.= (q`1)^2/(sqrt(1+(q`2/q`1)^2))^2+(q`2/sqrt(1+(q`2/q`1)^2))^2 by
XCMPLX_1:76
.= (q`1)^2/(sqrt(1+(q`2/q`1)^2))^2+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2 by
XCMPLX_1:76
.= (q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2 by A42,
SQUARE_1:def 2
.= (q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(1+(q`2/q`1)^2) by A42,SQUARE_1:def 2
.= ((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2) by XCMPLX_1:62;
then
((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2)*(1+(q`2/q`1)^2)=(1)*(1+(q`2/q`1 )^2
) by A31;
then ((q`1)^2+(q`2)^2)=(1+(q`2/q`1)^2) by A42,XCMPLX_1:87;
then
A46: (px`1)^2+(px`2)^2-1=(px`2)^2/(px`1)^2 by XCMPLX_1:76;
px`1<>0 by A38,A34,A39,A40,XREAL_1:64;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2=(px`2)^2 by A46,XCMPLX_1:6,87;
then
A47: ((px`1)^2-1)*((px`1)^2+(px`2)^2)=0;
A48: (|[pu`1/sqrt(1+(pu`1/pu`2)^2),pu`2/sqrt(1+(pu`1/pu`2)^2)]|)`2 = pu`2
/ sqrt(1+(pu`1/pu`2)^2) by EUCLID:52;
consider p4 being Point of TOP-REAL 2 such that
A49: g.I=p4 and
A50: |.p4.|=1 and
A51: p4`2>=p4`1 and
A52: p4`2>=-p4`1 by A1;
(p4`1/p4`2)^2 >=0 by XREAL_1:63;
then
A53: sqrt(1+(p4`1/p4`2)^2)>0 by SQUARE_1:25;
A54: -p4`2<=--p4`1 by A52,XREAL_1:24;
then
A55: p4`1<=p4`2 & (-p4`2)*sqrt(1+(p4`1/p4`2)^2) <= p4`1*sqrt(1+(p4`1/p4`2
) ^2 ) or pu`1>=pu`2 & pu`1<=-pu`2 by A51,A53,XREAL_1:64;
A56: (gg.I)=(Sq_Circ").(g.I) by A3,FUNCT_1:12;
then
A57: p4=Sq_Circ.pu by A49,FUNCT_1:32,JGRAPH_3:22,43;
A58: p4<>0.TOP-REAL 2 by A50,TOPRNS_1:23;
then
A59: Sq_Circ".p4=|[p4`1*sqrt(1+(p4`1/p4`2)^2),p4`2*sqrt(1+(p4`1/p4`2) ^2
)]| by A51,A54,JGRAPH_3:30;
then
A60: pu`2 = p4`2*sqrt(1+(p4`1/p4`2)^2) by A56,A49,EUCLID:52;
A61: pu`1 = p4`1*sqrt(1+(p4`1/p4`2)^2) by A56,A49,A59,EUCLID:52;
A62: now
assume pu`2=0 & pu`1=0;
then p4`2=0 & p4`1=0 by A60,A61,A53,XCMPLX_1:6;
hence contradiction by A58,EUCLID:53,54;
end;
p4`1* sqrt(1+(p4`1/p4`2)^2) <= p4`2*sqrt(1+(p4`1/p4`2)^2) & -pu`2<=
pu `1 or pu`1>=pu`2 & pu`1<=-pu`2 by A56,A49,A59,A60,A53,A55,EUCLID:52
,XREAL_1:64;
then
A63: Sq_Circ.pu=|[pu`1/sqrt(1+(pu`1/pu`2)^2),pu`2/sqrt(1+(pu`1/pu`2)^2)]|
by A60,A61,A62,JGRAPH_2:3,JGRAPH_3:4;
A64: (pu`1/pu`2)^2 >=0 by XREAL_1:63;
then
A65: sqrt(1+(pu`1/pu`2)^2)>0 by SQUARE_1:25;
A66: now
assume
A67: pu`2=-1;
then -p4`1<0 by A52,A57,A63,A48,A64,SQUARE_1:25,XREAL_1:141;
then --p4`1>-0;
hence contradiction by A51,A57,A63,A65,A67,EUCLID:52;
end;
(|[pu`1/sqrt(1+(pu`1/pu`2)^2),pu`2/sqrt(1+(pu`1/pu`2)^2)]|)`1 = pu`1
/ sqrt(1+(pu`1/pu`2)^2) by EUCLID:52;
then (|.p4.|)^2= (pu`2/sqrt(1+(pu`1/pu`2)^2))^2+(pu`1/sqrt(1+(pu`1/pu`2)
^2 ) ) ^2 by A57,A63,A48,JGRAPH_3:1
.= (pu`2)^2/(sqrt(1+(pu`1/pu`2)^2))^2+(pu`1/sqrt(1+(pu`1/pu`2)^2))^2
by XCMPLX_1:76
.= (pu`2)^2/(sqrt(1+(pu`1/pu`2)^2))^2 +(pu`1)^2/(sqrt(1+(pu`1/pu`2)^2)
)^2 by XCMPLX_1:76
.= (pu`2)^2/(1+(pu`1/pu`2)^2)+(pu`1)^2/(sqrt(1+(pu`1/pu`2)^2))^2 by A64,
SQUARE_1:def 2
.= (pu`2)^2/(1+(pu`1/pu`2)^2)+(pu`1)^2/(1+(pu`1/pu`2)^2) by A64,
SQUARE_1:def 2
.= ((pu`2)^2+(pu`1)^2)/(1+(pu`1/pu`2)^2) by XCMPLX_1:62;
then ((pu`2)^2+(pu`1)^2)/(1+(pu`1/pu`2)^2)*(1+(pu`1/pu`2)^2)=(1)*(1+(pu`1
/pu `2)^2) by A50;
then ((pu`2)^2+(pu`1)^2)=(1+(pu`1/pu`2)^2) by A64,XCMPLX_1:87;
then
A68: (pu`2)^2+(pu`1)^2-1=(pu`1)^2/(pu`2)^2 by XCMPLX_1:76;
pu`2<>0 by A60,A61,A53,A62,A55,XREAL_1:64;
then ((pu`2)^2+(pu`1)^2-1)*(pu`2)^2=(pu`1)^2 by A68,XCMPLX_1:6,87;
then
A69: ((pu`2)^2-1)*((pu`2)^2+(pu`1)^2)=0;
((pu`2)^2+(pu`1)^2)<>0 by A62,COMPLEX1:1;
then (pu`2-1)*(pu`2+1)=0 by A69,XCMPLX_1:6;
then
A70: pu`2-1=0 or pu`2+1=0 by XCMPLX_1:6;
consider p3 being Point of TOP-REAL 2 such that
A71: g.O=p3 and
A72: |.p3.|=1 and
A73: p3`2<=p3`1 and
A74: p3`2<=-p3`1 by A1;
A75: p3<>0.TOP-REAL 2 by A72,TOPRNS_1:23;
A76: (gg.O)=(Sq_Circ").(g.O) by A3,FUNCT_1:12;
then
A77: p3=Sq_Circ.pz by A71,FUNCT_1:32,JGRAPH_3:22,43;
A78: -p3`2>=--p3`1 by A74,XREAL_1:24;
then
A79: Sq_Circ".p3=|[p3`1*sqrt(1+(p3`1/p3`2)^2),p3`2*sqrt(1+(p3`1/p3`2) ^2)
]| by A73,A75,JGRAPH_3:30;
then
A80: pz`2 = p3`2*sqrt(1+(p3`1/p3`2)^2) by A76,A71,EUCLID:52;
(p3`1/p3`2)^2 >=0 by XREAL_1:63;
then
A81: sqrt(1+(p3`1/p3`2)^2)>0 by SQUARE_1:25;
A82: pz`1 = p3`1*sqrt(1+(p3`1/p3`2)^2) by A76,A71,A79,EUCLID:52;
A83: now
assume pz`2=0 & pz`1=0;
then p3`2=0 & p3`1=0 by A80,A82,A81,XCMPLX_1:6;
hence contradiction by A75,EUCLID:53,54;
end;
p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 & p3`1*sqrt(1+(p3`1/p3`2)^2)
<= (-p3`2)*sqrt(1+(p3`1/p3`2)^2) by A73,A78,A81,XREAL_1:64;
then
A84: p3`1<=p3`2 & (-p3`2)*sqrt(1+(p3`1/p3`2)^2) <= p3`1*sqrt(1+(p3`1/p3 `2
)^2) or pz`1>=pz`2 & pz`1<=-pz`2 by A80,A82,A81,XREAL_1:64;
then
p3`1*sqrt(1+(p3`1/p3`2)^2) <= p3`2*sqrt(1+(p3`1/p3`2)^2) & -pz `2<=pz
`1 or pz`1>=pz`2 & pz`1<=-pz`2 by A76,A71,A79,A80,A81,EUCLID:52,XREAL_1:64;
then
A85: Sq_Circ.pz=|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|
by A80,A82,A83,JGRAPH_2:3,JGRAPH_3:4;
A86: (pz`1/pz`2)^2 >=0 by XREAL_1:63;
then
A87: sqrt(1+(pz`1/pz`2)^2)>0 by SQUARE_1:25;
A88: now
assume
A89: pz`2=1;
then -p3`1>0 by A74,A77,A85,A29,A87,XREAL_1:139;
then --p3`1<-0;
hence contradiction by A73,A77,A85,A87,A89,EUCLID:52;
end;
(|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|)`1 = pz`1
/ sqrt(1+(pz`1/pz`2)^2) by EUCLID:52;
then (|.p3.|)^2= (pz`2/sqrt(1+(pz`1/pz`2)^2))^2+(pz`1/sqrt(1+(pz`1/pz`2)
^2))^2 by A77,A85,A29,JGRAPH_3:1
.= (pz`2)^2/(sqrt(1+(pz`1/pz`2)^2))^2+(pz`1/sqrt(1+(pz`1/pz`2)^2))^2
by XCMPLX_1:76
.= (pz`2)^2/(sqrt(1+(pz`1/pz`2)^2))^2 +(pz`1)^2/(sqrt(1+(pz`1/pz`2)^2)
)^2 by XCMPLX_1:76
.= (pz`2)^2/(1+(pz`1/pz`2)^2)+(pz`1)^2/(sqrt(1+(pz`1/pz`2)^2))^2 by A86,
SQUARE_1:def 2
.= (pz`2)^2/(1+(pz`1/pz`2)^2)+(pz`1)^2/(1+(pz`1/pz`2)^2) by A86,
SQUARE_1:def 2
.= ((pz`2)^2+(pz`1)^2)/(1+(pz`1/pz`2)^2) by XCMPLX_1:62;
then ((pz`2)^2+(pz`1)^2)/(1+(pz`1/pz`2)^2)*(1+(pz`1/pz`2)^2)=(1)*(1+(pz`1
/pz `2 ) ^2 ) by A72;
then ((pz`2)^2+(pz`1)^2)=(1+(pz`1/pz`2)^2) by A86,XCMPLX_1:87;
then
A90: (pz`2)^2+(pz`1)^2-1=(pz`1)^2/(pz`2)^2 by XCMPLX_1:76;
pz`2<>0 by A80,A82,A81,A83,A84,XREAL_1:64;
then ((pz`2)^2+(pz`1)^2-1)*(pz`2)^2=(pz`1)^2 by A90,XCMPLX_1:6,87;
then
A91: ((pz`2)^2-1)*((pz`2)^2+(pz`1)^2)=0;
((pz`2)^2+(pz`1)^2)<>0 by A83,COMPLEX1:1;
then (pz`2-1)*(pz`2+1)=0 by A91,XCMPLX_1:6;
then
A92: pz`2-1=0 or pz`2+1=0 by XCMPLX_1:6;
((px`1)^2+(px`2)^2)<>0 by A39,COMPLEX1:1;
then (px`1-1)*(px`1+1)=0 by A47,XCMPLX_1:6;
then px`1-1=0 or px`1+1=0 by XCMPLX_1:6;
hence thesis by A44,A28,A24,A92,A88,A70,A66;
end;
A93: dom f=the carrier of I[01] by FUNCT_2:def 1;
A94: for r being Point of I[01] holds (-1>=(ff.r)`1 or (ff.r)`1>=1 or -1 >=
(ff.r)`2 or (ff.r)`2>=1) & (-1>=(gg.r)`1 or (gg.r)`1>=1 or -1 >=(gg.r)`2 or (gg
.r)`2>=1)
proof
let r be Point of I[01];
f.r in rng f by A93,FUNCT_1:3;
then f.r in C0 by A1;
then consider p1 being Point of TOP-REAL 2 such that
A95: f.r=p1 and
A96: |.p1.|>=1 by A1;
g.r in rng g by A2,FUNCT_1:3;
then g.r in C0 by A1;
then consider p2 being Point of TOP-REAL 2 such that
A97: g.r=p2 and
A98: |.p2.|>=1 by A1;
A99: (gg.r)=(Sq_Circ").(g.r) by A3,FUNCT_1:12;
A100: now
per cases;
case
p2=0.TOP-REAL 2;
hence contradiction by A98,TOPRNS_1:23;
end;
case
A101: p2<>0.TOP-REAL 2 & (p2`2<=p2`1 & -p2`1<=p2`2 or p2`2>=p2`1 &
p2`2<=-p2`1);
reconsider px=gg.r as Point of TOP-REAL 2;
A102: Sq_Circ".p2=|[p2`1*sqrt(1+(p2`2/p2`1)^2),p2`2*sqrt(1+(p2`2 /p2`1
)^2 )]| by A101,JGRAPH_3:28;
then
A103: px`1 = p2`1*sqrt(1+(p2`2/p2`1)^2) by A99,A97,EUCLID:52;
set q=px;
A104: (px`1)^2 >=0 by XREAL_1:63;
(|.p2.|)^2>=|.p2.| by A98,XREAL_1:151;
then
A105: (|.p2.|)^2>=1 by A98,XXREAL_0:2;
A106: (px`2)^2>=0 by XREAL_1:63;
(p2`2/p2`1)^2 >=0 by XREAL_1:63;
then
A107: sqrt(1+(p2`2/p2`1)^2)>0 by SQUARE_1:25;
A108: px`2 = p2`2*sqrt(1+(p2`2/p2`1)^2) by A99,A97,A102,EUCLID:52;
A109: now
assume px`1=0 & px`2=0;
then p2`1=0 & p2`2=0 by A103,A108,A107,XCMPLX_1:6;
hence contradiction by A101,EUCLID:53,54;
end;
p2`2<=p2`1 & -p2`1<=p2`2 or p2`2>=p2`1 & p2`2*sqrt(1+(p2`2/p2`1)
^2) <= (-p2`1)*sqrt(1+(p2`2/p2`1)^2) by A101,A107,XREAL_1:64;
then
A110: p2`2<=p2`1 & (-p2`1)*sqrt(1+(p2`2/p2`1)^2) <= p2`2*sqrt(1+(p2`2/
p2`1 )^2) or px`2>=px`1 & px`2<=-px`1 by A103,A108,A107,XREAL_1:64;
then
A111: px`1<>0 by A103,A108,A107,A109,XREAL_1:64;
p2`2*sqrt( 1+(p2`2/p2`1)^2) <= p2`1*sqrt(1+(p2`2/p2`1)^2) & -px
`1<= px `2 or px`2>=px`1 & px`2<=-px`1 by A99,A97,A102,A103,A107,A110,EUCLID:52
,XREAL_1:64;
then
A112: Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]| by A103
,A108,A109,JGRAPH_2:3,JGRAPH_3:def 1;
Sq_Circ".p2=q by A3,A97,FUNCT_1:12;
then
A113: p2=Sq_Circ.px by FUNCT_1:32,JGRAPH_3:22,43;
A114: (q`2/q`1)^2 >=0 by XREAL_1:63;
(|[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:52;
then (|.p2.|)^2= (q`1/sqrt(1+(q`2/q`1)^2))^2+(q`2/sqrt(1+(q`2/q`1)^2)
) ^2 by A113,A112,JGRAPH_3:1
.= (q`1)^2/(sqrt(1+(q`2/q`1)^2))^2+(q`2/sqrt(1+(q`2/q`1)^2))^2 by
XCMPLX_1:76
.= (q`1)^2/(sqrt(1+(q`2/q`1)^2))^2+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by XCMPLX_1:76
.= (q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2 by A114,
SQUARE_1:def 2
.= (q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(1+(q`2/q`1)^2) by A114,
SQUARE_1:def 2
.= ((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2) by XCMPLX_1:62;
then ((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2)*(1+(q`2/q`1)^2)>=(1)*(1+(q`2/
q `1)^2) by A114,A105,XREAL_1:64;
then ((q`1)^2+(q`2)^2)>=(1+(q`2/q`1)^2) by A114,XCMPLX_1:87;
then (px`1)^2+(px`2)^2>=1+(px`2)^2/(px`1)^2 by XCMPLX_1:76;
then (px`1)^2+(px`2)^2-1>=1+(px`2)^2/(px`1)^2-1 by XREAL_1:9;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2>=(px`2)^2/(px`1)^2*(px`1)^2 by A104
,XREAL_1:64;
then ((px`1)^2+((px`2)^2-1))*(px`1)^2>=(px`2)^2 by A111,XCMPLX_1:6,87;
then (px`1)^2*(px`1)^2+(px`1)^2*((px`2)^2-1)-(px`2)^2>=(px`2)^2-(px
`2 )^2 by XREAL_1:9;
then
A115: ((px`1)^2-1)*((px`1)^2+(px`2)^2)>=0;
((px`1)^2+(px`2)^2)<>0 by A109,COMPLEX1:1;
then (px`1-1)*(px`1+1)>=0 by A104,A115,A106,XREAL_1:132;
hence -1>=(gg.r)`1 or (gg.r)`1>=1 or -1 >=(gg.r)`2 or (gg.r)`2>=1 by
XREAL_1:95;
end;
case
A116: p2<>0.TOP-REAL 2 & not(p2`2<=p2`1 & -p2`1<=p2`2 or p2`2>=p2
`1 & p2`2<=-p2`1);
reconsider pz=gg.r as Point of TOP-REAL 2;
A117: Sq_Circ".p2=|[p2`1*sqrt(1+(p2`1/p2`2)^2),p2`2*sqrt(1+(p2`1 /p2`2
)^2 )]| by A116,JGRAPH_3:28;
then
A118: pz`2 = p2`2*sqrt(1+(p2`1/p2`2)^2) by A99,A97,EUCLID:52;
(p2`1/p2`2)^2 >=0 by XREAL_1:63;
then
A119: sqrt(1+(p2`1/p2`2)^2)>0 by SQUARE_1:25;
A120: now
assume that
A121: pz`2=0 and
pz`1=0;
p2`2=0 by A118,A119,A121,XCMPLX_1:6;
hence contradiction by A116;
end;
A122: pz`1 = p2`1*sqrt(1+(p2`1/p2`2)^2) by A99,A97,A117,EUCLID:52;
p2`1<=p2`2 & -p2`2<=p2`1 or p2`1>=p2`2 & p2`1<=-p2`2 by A116,
JGRAPH_2:13;
then p2`1<=p2`2 & -p2`2<=p2`1 or p2`1>=p2`2 & p2`1*sqrt(1+(p2`1/p2`2)
^2) <= (-p2`2)*sqrt(1+(p2`1/p2`2)^2) by A119,XREAL_1:64;
then
A123: p2`1<=p2`2 & (-p2`2)*sqrt(1+(p2`1/p2`2)^2) <= p2`1*sqrt(1+(p2`1/
p2`2) ^2) or pz`1>=pz`2 & pz`1<=-pz`2 by A118,A122,A119,XREAL_1:64;
then
A124: pz`2<>0 by A118,A122,A119,A120,XREAL_1:64;
p2`1*sqrt(1+(p2`1/p2`2)^2) <= p2`2*sqrt(1+(p2`1/p2`2)^2) & -pz
`2<=pz `1 or pz`1>=pz`2 & pz`1<=-pz`2 by A99,A97,A117,A118,A119,A123,EUCLID:52
,XREAL_1:64;
then
A125: Sq_Circ.pz=|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)
^2)]| by A118,A122,A120,JGRAPH_2:3,JGRAPH_3:4;
A126: (pz`1/pz`2)^2 >=0 by XREAL_1:63;
(|.p2.|)^2>=|.p2.| by A98,XREAL_1:151;
then
A127: (|.p2.|)^2>=1 by A98,XXREAL_0:2;
A128: (|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|)`1 =
pz`1/ sqrt(1+(pz`1/pz`2)^2) by EUCLID:52;
A129: (pz`1)^2>=0 by XREAL_1:63;
A130: (pz`2)^2 >=0 by XREAL_1:63;
p2=Sq_Circ.pz & (|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/
pz`2)^2)]|) `2 = pz`2/ sqrt(1+(pz`1/pz`2)^2) by A99,A97,EUCLID:52,FUNCT_1:32
,JGRAPH_3:22,43;
then ( |.p2.|)^2= (pz`2/sqrt(1+(pz`1/pz`2)^2))^2+(pz`1/sqrt(1+(pz`1/
pz`2)^2))^2 by A125,A128,JGRAPH_3:1
.= (pz`2)^2/(sqrt(1+(pz`1/pz`2)^2))^2+(pz`1/sqrt(1+(pz`1/pz`2)^2))
^2 by XCMPLX_1:76
.= (pz`2)^2/(sqrt(1+(pz`1/pz`2)^2))^2 +(pz`1)^2/(sqrt(1+(pz`1/pz`2
)^2))^2 by XCMPLX_1:76
.= (pz`2)^2/(1+(pz`1/pz`2)^2)+(pz`1)^2/(sqrt(1+(pz`1/pz`2)^2))^2
by A126,SQUARE_1:def 2
.= (pz`2)^2/(1+(pz`1/pz`2)^2)+(pz`1)^2/(1+(pz`1/pz`2)^2) by A126,
SQUARE_1:def 2
.= ((pz`2)^2+(pz`1)^2)/(1+(pz`1/pz`2)^2) by XCMPLX_1:62;
then ((pz`2)^2+(pz`1)^2)/(1+(pz`1/pz`2)^2)*(1+(pz`1/pz`2)^2) >=(1)*(1
+(pz`1/pz`2)^2) by A126,A127,XREAL_1:64;
then ((pz`2)^2+(pz`1)^2)>=(1+(pz`1/pz`2)^2) by A126,XCMPLX_1:87;
then (pz`2)^2+(pz`1)^2>=1+(pz`1)^2/(pz`2)^2 by XCMPLX_1:76;
then (pz`2)^2+(pz`1)^2-1>=1+(pz`1)^2/(pz`2)^2-1 by XREAL_1:9;
then ((pz`2)^2+(pz`1)^2-1)*(pz`2)^2>=(pz`1)^2/(pz`2)^2*(pz`2)^2 by A130
,XREAL_1:64;
then ((pz`2)^2+((pz`1)^2-1))*(pz`2)^2>=(pz`1)^2 by A124,XCMPLX_1:6,87;
then (pz`2)^2*(pz`2)^2+(pz`2)^2*((pz`1)^2-1)-(pz`1)^2 >=(pz`1)^2-(pz
`1)^2 by XREAL_1:9;
then
A131: ((pz`2)^2-1)*((pz`2)^2+(pz`1)^2)>=0;
((pz`2)^2+(pz`1)^2)<>0 by A120,COMPLEX1:1;
then (pz`2-1)*(pz`2+1)>=0 by A130,A131,A129,XREAL_1:132;
hence -1>=(gg.r)`1 or (gg.r)`1>=1 or -1 >=(gg.r)`2 or (gg.r)`2>=1 by
XREAL_1:95;
end;
end;
A132: (ff.r)=(Sq_Circ").(f.r) by A4,FUNCT_1:12;
now
per cases;
case
p1=0.TOP-REAL 2;
hence contradiction by A96,TOPRNS_1:23;
end;
case
A133: p1<>0.TOP-REAL 2 & (p1`2<=p1`1 & -p1`1<=p1`2 or p1`2>=p1`1 &
p1`2<=-p1`1);
reconsider px=ff.r as Point of TOP-REAL 2;
A134: Sq_Circ".p1=|[p1`1*sqrt(1+(p1`2/p1`1)^2),p1`2*sqrt(1+(p1`2 /p1`1
)^2 )]| by A133,JGRAPH_3:28;
then
A135: px`1 = p1`1*sqrt(1+(p1`2/p1`1)^2) by A132,A95,EUCLID:52;
(p1`2/p1`1)^2 >=0 by XREAL_1:63;
then
A136: sqrt(1+(p1`2/p1`1)^2)>0 by SQUARE_1:25;
A137: px`2 = p1`2*sqrt(1+(p1`2/p1`1)^2) by A132,A95,A134,EUCLID:52;
A138: now
assume px`1=0 & px`2=0;
then p1`1=0 & p1`2=0 by A135,A137,A136,XCMPLX_1:6;
hence contradiction by A133,EUCLID:53,54;
end;
p1`2<=p1`1 & -p1`1<=p1`2 or p1`2>=p1`1 & p1`2*sqrt(1+(p1`2/p1`1)
^2) <= (-p1`1)*sqrt(1+(p1`2/p1`1)^2) by A133,A136,XREAL_1:64;
then
A139: p1`2<=p1`1 & (-p1`1)*sqrt(1+(p1`2/p1`1)^2) <= p1`2*sqrt(1+(p1`2/
p1`1 )^2) or px`2>=px`1 & px`2<=-px`1 by A135,A137,A136,XREAL_1:64;
then
A140: px`1<>0 by A135,A137,A136,A138,XREAL_1:64;
(|.p1.|)^2>=|.p1.| by A96,XREAL_1:151;
then
A141: (|.p1.|)^2>=1 by A96,XXREAL_0:2;
A142: (px`1)^2 >=0 by XREAL_1:63;
set q=px;
A143: (|[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:52;
A144: (px`2)^2>=0 by XREAL_1:63;
A145: (q`2/q`1)^2 >=0 by XREAL_1:63;
p1`2*sqrt(1+(p1`2/p1`1)^2) <= p1`1*sqrt(1+(p1`2/p1`1)^2) & -px`1
<= px `2 or px`2>=px`1 & px`2<=-px`1 by A132,A95,A134,A135,A136,A139,EUCLID:52
,XREAL_1:64;
then
A146: Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]| by A135
,A137,A138,JGRAPH_2:3,JGRAPH_3:def 1;
p1=Sq_Circ.px & (|[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) by A132,A95,EUCLID:52,FUNCT_1:32
,JGRAPH_3:22,43;
then (|.p1.|)^2= (q`1/sqrt(1+(q`2/q`1)^2))^2+(q`2/sqrt(1+(q`2/q`1)^2)
) ^2 by A146,A143,JGRAPH_3:1
.= (q`1)^2/(sqrt(1+(q`2/q`1)^2))^2+(q`2/sqrt(1+(q`2/q`1)^2))^2 by
XCMPLX_1:76
.= (q`1)^2/(sqrt(1+(q`2/q`1)^2))^2+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by XCMPLX_1:76
.= (q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2 by A145,
SQUARE_1:def 2
.= (q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(1+(q`2/q`1)^2) by A145,
SQUARE_1:def 2
.= ((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2) by XCMPLX_1:62;
then ((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2)*(1+(q`2/q`1)^2)>=(1)*(1+(q`2/
q `1)^2) by A145,A141,XREAL_1:64;
then ((q`1)^2+(q`2)^2)>=(1+(q`2/q`1)^2) by A145,XCMPLX_1:87;
then (px`1)^2+(px`2)^2>=1+(px`2)^2/(px`1)^2 by XCMPLX_1:76;
then (px`1)^2+(px`2)^2-1>=1+(px`2)^2/(px`1)^2-1 by XREAL_1:9;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2>=(px`2)^2/(px`1)^2*(px`1)^2 by A142
,XREAL_1:64;
then ((px`1)^2+((px`2)^2-1))*(px`1)^2>=(px`2)^2 by A140,XCMPLX_1:6,87;
then (px`1)^2*(px`1)^2+(px`1)^2*((px`2)^2-1)-(px`2)^2>=(px`2)^2-(px
`2 )^2 by XREAL_1:9;
then
A147: ((px`1)^2-1)*((px`1)^2+(px`2)^2)>=0;
((px`1)^2+(px`2)^2)<>0 by A138,COMPLEX1:1;
then (px`1-1)*(px`1+1)>=0 by A142,A147,A144,XREAL_1:132;
hence -1>=(ff.r)`1 or (ff.r)`1>=1 or -1 >=(ff.r)`2 or (ff.r)`2>=1 by
XREAL_1:95;
end;
case
A148: p1<>0.TOP-REAL 2 & not(p1`2<=p1`1 & -p1`1<=p1`2 or p1`2>=p1
`1 & p1`2<=-p1`1);
reconsider pz=ff.r as Point of TOP-REAL 2;
A149: Sq_Circ".p1=|[p1`1*sqrt(1+(p1`1/p1`2)^2),p1`2*sqrt(1+(p1`1 /p1`2
) ^2)]| by A148,JGRAPH_3:28;
then
A150: pz`2 = p1`2*sqrt(1+(p1`1/p1`2)^2) by A132,A95,EUCLID:52;
(p1`1/p1`2)^2 >=0 by XREAL_1:63;
then
A151: sqrt(1+(p1`1/p1`2)^2)>0 by SQUARE_1:25;
A152: now
assume that
A153: pz`2=0 and
pz`1=0;
p1`2=0 by A150,A151,A153,XCMPLX_1:6;
hence contradiction by A148;
end;
A154: pz`1 = p1`1*sqrt(1+(p1`1/p1`2)^2) by A132,A95,A149,EUCLID:52;
p1`1<=p1`2 & -p1`2<=p1`1 or p1`1>=p1`2 & p1`1<=-p1`2 by A148,
JGRAPH_2:13;
then p1`1<=p1`2 & -p1`2<=p1`1 or p1`1>=p1`2 & p1`1*sqrt(1+(p1`1/p1`2)
^2) <= (-p1`2)*sqrt(1+(p1`1/p1`2)^2) by A151,XREAL_1:64;
then
A155: p1`1<=p1`2 & (-p1`2)*sqrt(1+(p1`1/p1`2)^2) <= p1`1*sqrt(1+(p1`1/
p1`2 )^2) or pz`1>=pz`2 & pz`1<=-pz`2 by A150,A154,A151,XREAL_1:64;
then
A156: pz`2<>0 by A150,A154,A151,A152,XREAL_1:64;
p1`1*sqrt(1+(p1`1/p1`2)^2) <= p1`2*sqrt(1+(p1`1/p1`2)^2) & -pz
`2<=pz `1 or pz`1>=pz`2 & pz`1<=-pz`2 by A132,A95,A149,A150,A151,A155,EUCLID:52
,XREAL_1:64;
then
A157: Sq_Circ.pz=|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)
^2)]| by A150,A154,A152,JGRAPH_2:3,JGRAPH_3:4;
A158: (pz`1/pz`2)^2 >=0 by XREAL_1:63;
(|.p1.|)^2>=|.p1.| by A96,XREAL_1:151;
then
A159: (|.p1.|)^2>=1 by A96,XXREAL_0:2;
A160: (|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|)`1 =
pz`1/ sqrt(1+(pz`1/pz`2)^2) by EUCLID:52;
A161: (pz`1)^2>=0 by XREAL_1:63;
A162: (pz`2)^2 >=0 by XREAL_1:63;
p1=Sq_Circ.pz & (|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/
pz`2)^2)]|) `2 = pz`2/ sqrt(1+(pz`1/pz`2)^2) by A132,A95,EUCLID:52,FUNCT_1:32
,JGRAPH_3:22,43;
then ( |.p1.|)^2= (pz`2/sqrt(1+(pz`1/pz`2)^2))^2+(pz`1/sqrt(1+(pz`1/
pz`2)^2))^2 by A157,A160,JGRAPH_3:1
.= (pz`2)^2/(sqrt(1+(pz`1/pz`2)^2))^2+(pz`1/sqrt(1+(pz`1/pz`2)^2))
^2 by XCMPLX_1:76
.= (pz`2)^2/(sqrt(1+(pz`1/pz`2)^2))^2 +(pz`1)^2/(sqrt(1+(pz`1/pz`2
)^2))^2 by XCMPLX_1:76
.= (pz`2)^2/(1+(pz`1/pz`2)^2)+(pz`1)^2/(sqrt(1+(pz`1/pz`2)^2))^2
by A158,SQUARE_1:def 2
.= (pz`2)^2/(1+(pz`1/pz`2)^2)+(pz`1)^2/(1+(pz`1/pz`2)^2) by A158,
SQUARE_1:def 2
.= ((pz`2)^2+(pz`1)^2)/(1+(pz`1/pz`2)^2) by XCMPLX_1:62;
then ((pz`2)^2+(pz`1)^2)/(1+(pz`1/pz`2)^2)*(1+(pz`1/pz`2)^2) >=(1)*(1
+(pz`1/pz`2)^2) by A158,A159,XREAL_1:64;
then ((pz`2)^2+(pz`1)^2)>=(1+(pz`1/pz`2)^2) by A158,XCMPLX_1:87;
then (pz`2)^2+(pz`1)^2>=1+(pz`1)^2/(pz`2)^2 by XCMPLX_1:76;
then (pz`2)^2+(pz`1)^2-1>=1+(pz`1)^2/(pz`2)^2-1 by XREAL_1:9;
then ((pz`2)^2+(pz`1)^2-1)*(pz`2)^2>=(pz`1)^2/(pz`2)^2*(pz`2)^2 by A162
,XREAL_1:64;
then ((pz`2)^2+((pz`1)^2-1))*(pz`2)^2>=(pz`1)^2 by A156,XCMPLX_1:6,87;
then (pz`2)^2*(pz`2)^2+(pz`2)^2*((pz`1)^2-1)-(pz`1)^2 >=(pz`1)^2-(pz
`1)^2 by XREAL_1:9;
then
A163: ((pz`2)^2-1)*((pz`2)^2+(pz`1)^2)>=0;
((pz`2)^2+(pz`1)^2)<>0 by A152,COMPLEX1:1;
then (pz`2-1)*(pz`2+1)>=0 by A162,A163,A161,XREAL_1:132;
hence -1>=(ff.r)`1 or (ff.r)`1>=1 or -1 >=(ff.r)`2 or (ff.r)`2>=1 by
XREAL_1:95;
end;
end;
hence thesis by A100;
end;
-1 <=(ff.O)`2 & (ff.O)`2 <= 1 & -1 <=(ff.I)`2 & (ff.I)`2 <= 1 & -1 <=(
gg.O)`1 & (gg.O)`1 <= 1 & -1 <=(gg.I)`1 & (gg.I)`1 <= 1
proof
reconsider pz=gg.O as Point of TOP-REAL 2;
reconsider py=ff.I as Point of TOP-REAL 2;
reconsider px=ff.O as Point of TOP-REAL 2;
set q=px;
A164: (|[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:52;
A165: (q`2/q`1)^2 >=0 by XREAL_1:63;
consider p1 being Point of TOP-REAL 2 such that
A166: f.O=p1 and
A167: |.p1.|=1 and
A168: p1`2>=p1`1 & p1`2<=-p1`1 by A1;
A169: (ff.O)=(Sq_Circ").(f.O) by A4,FUNCT_1:12;
then
A170: p1=Sq_Circ.px by A166,FUNCT_1:32,JGRAPH_3:22,43;
(p1`2/p1`1)^2 >=0 by XREAL_1:63;
then
A171: sqrt(1+(p1`2/p1`1)^2)>0 by SQUARE_1:25;
A172: p1<>0.TOP-REAL 2 by A167,TOPRNS_1:23;
then Sq_Circ".p1=|[p1`1*sqrt(1+(p1`2/p1`1)^2),p1`2*sqrt(1+(p1`2/p1`1) ^2)
]| by A168,JGRAPH_3:28;
then
A173: px`1 = p1`1*sqrt(1+(p1`2/p1`1)^2) & px`2 = p1`2*sqrt(1+(p1`2/p1`1)^2
) by A169,A166,EUCLID:52;
A174: now
assume px`1=0 & px`2=0;
then p1`1=0 & p1`2=0 by A173,A171,XCMPLX_1:6;
hence contradiction by A172,EUCLID:53,54;
end;
p1`2<=p1`1 & -p1`1<=p1`2 or p1`2>=p1`1 & p1`2*sqrt(1+(p1`2/p1`1)^2)
<= (-p1`1)*sqrt(1+(p1`2/p1`1)^2) by A168,A171,XREAL_1:64;
then
A175: p1`2<=p1`1 & (-p1`1)*sqrt(1+(p1`2/p1`1)^2) <= p1`2*sqrt(1+(p1`2 /p1
`1 )^2) or px`2>=px`1 & px`2<=-px`1 by A173,A171,XREAL_1:64;
then px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1 by A173,A171,
XREAL_1:64;
then Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]| by A174,
JGRAPH_2:3,JGRAPH_3:def 1;
then (|.p1.|)^2= (q`1/sqrt(1+(q`2/q`1)^2))^2+(q`2/sqrt(1+(q`2/q`1)^2)) ^2
by A170,A164,JGRAPH_3:1
.= (q`1)^2/(sqrt(1+(q`2/q`1)^2))^2+(q`2/sqrt(1+(q`2/q`1)^2))^2 by
XCMPLX_1:76
.= (q`1)^2/(sqrt(1+(q`2/q`1)^2))^2+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2 by
XCMPLX_1:76
.= (q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2 by A165,
SQUARE_1:def 2
.= (q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(1+(q`2/q`1)^2) by A165,SQUARE_1:def 2
.= ((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2) by XCMPLX_1:62;
then ((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2)*(1+(q`2/q`1)^2)=(1)*(1+(q`2/q`1 )
^2) by A167;
then ((q`1)^2+(q`2)^2)=(1+(q`2/q`1)^2) by A165,XCMPLX_1:87;
then
A176: (px`1)^2+(px`2)^2-1=(px`2)^2/(px`1)^2 by XCMPLX_1:76;
px`1<>0 by A173,A171,A174,A175,XREAL_1:64;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2=(px`2)^2 by A176,XCMPLX_1:6,87;
then
A177: ((px`1)^2-1)*((px`1)^2+(px`2)^2)=0;
((px`1)^2+(px`2)^2)<>0 by A174,COMPLEX1:1;
then (px`1-1)*(px`1+1)=0 by A177,XCMPLX_1:6;
then px`1-1=0 or px`1+1=0 by XCMPLX_1:6;
then px`1=1 or px`1=0-1;
hence -1 <=(ff.O)`2 & (ff.O)`2 <= 1 by A173,A171,A175,XREAL_1:64;
A178: (py`2/py`1)^2 >=0 by XREAL_1:63;
reconsider pu=gg.I as Point of TOP-REAL 2;
A179: (|[py`1/sqrt(1+(py`2/py`1)^2),py`2/sqrt(1+(py`2/py`1)^2)]|)`1 = py`1
/ sqrt(1+ (py`2/py`1)^2) & (|[py`1/sqrt(1+(py`2/py`1)^2),py`2/sqrt(1+(py`2/py`1
)^2)]|)`2 = py`2/ sqrt(1+(py`2/py`1)^2) by EUCLID:52;
A180: (pz`1/pz`2)^2 >=0 by XREAL_1:63;
consider p2 being Point of TOP-REAL 2 such that
A181: f.I=p2 and
A182: |.p2.|=1 and
A183: p2`2<=p2`1 & p2`2>=-p2`1 by A1;
A184: (ff.I)=(Sq_Circ").(f.I) by A4,FUNCT_1:12;
then
A185: p2=Sq_Circ.py by A181,FUNCT_1:32,JGRAPH_3:22,43;
A186: p2<>0.TOP-REAL 2 by A182,TOPRNS_1:23;
then
A187: Sq_Circ".p2=|[p2`1*sqrt(1+(p2`2/p2`1)^2),p2`2*sqrt(1+(p2`2/p2`1) ^2)
]| by A183,JGRAPH_3:28;
then
A188: py`1 = p2`1*sqrt(1+(p2`2/p2`1)^2) by A184,A181,EUCLID:52;
A189: py`2 = p2`2*sqrt(1+(p2`2/p2`1)^2) by A184,A181,A187,EUCLID:52;
(p2`2/p2`1)^2 >=0 by XREAL_1:63;
then
A190: sqrt(1+(p2`2/p2`1)^2)>0 by SQUARE_1:25;
A191: now
assume py`1=0 & py`2=0;
then p2`1=0 & p2`2=0 by A188,A189,A190,XCMPLX_1:6;
hence contradiction by A186,EUCLID:53,54;
end;
A192: p2`2<=p2`1 & (-p2`1)*sqrt(1+(p2`2/p2`1)^2) <= p2`2*sqrt(1+(p2`2/p2`1
) ^2 ) or py`2>=py`1 & py`2<=-py`1 by A183,A190,XREAL_1:64;
then
A193: p2`2*sqrt(1+(p2`2/p2`1)^2) <= p2`1*sqrt(1+(p2`2/p2`1)^2) & -py `1<=
py `2 or py`2>=py`1 & py`2<=-py`1 by A184,A181,A187,A188,A190,EUCLID:52
,XREAL_1:64;
then Sq_Circ.py=|[py`1/sqrt(1+(py`2/py`1)^2),py`2/sqrt(1+(py`2/py`1)^2)]|
by A188,A189,A191,JGRAPH_2:3,JGRAPH_3:def 1;
then (|.p2.|)^2= (py`1/sqrt(1+(py`2/py`1)^2))^2+(py`2/sqrt(1+(py`2/py`1)
^2 ) ) ^2 by A185,A179,JGRAPH_3:1
.= (py`1)^2/(sqrt(1+(py`2/py`1)^2))^2+(py`2/sqrt(1+(py`2/py`1)^2))^2
by XCMPLX_1:76
.= (py`1)^2/(sqrt(1+(py`2/py`1)^2))^2 +(py`2)^2/(sqrt(1+(py`2/py`1)^2)
)^2 by XCMPLX_1:76
.= (py`1)^2/(1+(py`2/py`1)^2)+(py`2)^2/(sqrt(1+(py`2/py`1)^2))^2 by A178,
SQUARE_1:def 2
.= (py`1)^2/(1+(py`2/py`1)^2)+(py`2)^2/(1+(py`2/py`1)^2) by A178,
SQUARE_1:def 2
.= ((py`1)^2+(py`2)^2)/(1+(py`2/py`1)^2) by XCMPLX_1:62;
then ((py`1)^2+(py`2)^2)/(1+(py`2/py`1)^2)*(1+(py`2/py`1)^2) =(1)*(1+(py
`2/py`1)^2) by A182;
then ((py`1)^2+(py`2)^2)=(1+(py`2/py`1)^2) by A178,XCMPLX_1:87;
then
A194: (py`1)^2+(py`2)^2-1=(py`2)^2/(py`1)^2 by XCMPLX_1:76;
py`1<>0 by A188,A189,A190,A191,A192,XREAL_1:64;
then ((py`1)^2+(py`2)^2-1)*(py`1)^2=(py`2)^2 by A194,XCMPLX_1:6,87;
then
A195: ((py`1)^2-1)*((py`1)^2+(py`2)^2)=0;
((py`1)^2+(py`2)^2)<>0 by A191,COMPLEX1:1;
then (py`1-1)*(py`1+1)=0 by A195,XCMPLX_1:6;
then py`1-1=0 or py`1+1=0 by XCMPLX_1:6;
hence -1 <=(ff.I)`2 & (ff.I)`2 <= 1 by A188,A189,A193;
A196: (|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|)`2 = pz`2
/ sqrt(1+ (pz`1/pz`2)^2) & (|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2
)^2)]|)`1 = pz`1/ sqrt(1+(pz`1/pz`2)^2) by EUCLID:52;
consider p3 being Point of TOP-REAL 2 such that
A197: g.O=p3 and
A198: |.p3.|=1 and
A199: p3`2<=p3`1 and
A200: p3`2<=-p3`1 by A1;
A201: p3<>0.TOP-REAL 2 by A198,TOPRNS_1:23;
A202: gg.O=(Sq_Circ").(g.O) by A3,FUNCT_1:12;
then
A203: p3=Sq_Circ.pz by A197,FUNCT_1:32,JGRAPH_3:22,43;
A204: -p3`2>=--p3`1 by A200,XREAL_1:24;
then
A205: Sq_Circ".p3=|[p3`1*sqrt(1+(p3`1/p3`2)^2),p3`2*sqrt(1+(p3`1/p3`2) ^2
)]| by A199,A201,JGRAPH_3:30;
then
A206: pz`2 = p3`2*sqrt(1+(p3`1/p3`2)^2) by A202,A197,EUCLID:52;
A207: pz`1 = p3`1*sqrt(1+(p3`1/p3`2)^2) by A202,A197,A205,EUCLID:52;
(p3`1/p3`2)^2 >=0 by XREAL_1:63;
then
A208: sqrt(1+(p3`1/p3`2)^2)>0 by SQUARE_1:25;
A209: now
assume pz`2=0 & pz`1=0;
then p3`2=0 & p3`1=0 by A206,A207,A208,XCMPLX_1:6;
hence contradiction by A201,EUCLID:53,54;
end;
p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 & p3`1*sqrt(1+(p3`1/p3`2)^2)
<= (-p3`2)*sqrt(1+(p3`1/p3`2)^2) by A199,A204,A208,XREAL_1:64;
then
A210: p3`1<=p3`2 & (-p3`2)*sqrt(1+(p3`1/p3`2)^2) <= p3`1*sqrt(1+(p3`1/p3
`2 )^2) or pz`1>=pz`2 & pz`1<=-pz`2 by A206,A207,A208,XREAL_1:64;
then
A211: p3`1*sqrt(1+(p3`1/p3`2)^2) <= p3`2*sqrt(1+(p3`1/p3`2)^2) & -pz `2<=
pz `1 or pz`1>=pz`2 & pz`1<=-pz`2 by A202,A197,A205,A206,A208,EUCLID:52
,XREAL_1:64;
then Sq_Circ.pz=|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|
by A206,A207,A209,JGRAPH_2:3,JGRAPH_3:4;
then (|.p3.|)^2= (pz`2/sqrt(1+(pz`1/pz`2)^2))^2+(pz`1/sqrt(1+(pz`1/pz`2)
^2))^2 by A203,A196,JGRAPH_3:1
.= (pz`2)^2/(sqrt(1+(pz`1/pz`2)^2))^2+(pz`1/sqrt(1+(pz`1/pz`2)^2))^2
by XCMPLX_1:76
.= (pz`2)^2/(sqrt(1+(pz`1/pz`2)^2))^2 +(pz`1)^2/(sqrt(1+(pz`1/pz`2)^2)
)^2 by XCMPLX_1:76
.= (pz`2)^2/(1+(pz`1/pz`2)^2)+(pz`1)^2/(sqrt(1+(pz`1/pz`2)^2))^2 by A180,
SQUARE_1:def 2
.= (pz`2)^2/(1+(pz`1/pz`2)^2)+(pz`1)^2/(1+(pz`1/pz`2)^2) by A180,
SQUARE_1:def 2
.= ((pz`2)^2+(pz`1)^2)/(1+(pz`1/pz`2)^2) by XCMPLX_1:62;
then ((pz`2)^2+(pz`1)^2)/(1+(pz`1/pz`2)^2)*(1+(pz`1/pz`2)^2)=(1)*(1+(pz`1
/pz `2 ) ^2 ) by A198;
then ((pz`2)^2+(pz`1)^2)=(1+(pz`1/pz`2)^2) by A180,XCMPLX_1:87;
then
A212: (pz`2)^2+(pz`1)^2-1=(pz`1)^2/(pz`2)^2 by XCMPLX_1:76;
pz`2<>0 by A206,A207,A208,A209,A210,XREAL_1:64;
then ((pz`2)^2+(pz`1)^2-1)*(pz`2)^2=(pz`1)^2 by A212,XCMPLX_1:6,87;
then
A213: ((pz`2)^2-1)*((pz`2)^2+(pz`1)^2)=0;
((pz`2)^2+(pz`1)^2)<>0 by A209,COMPLEX1:1;
then (pz`2-1)*(pz`2+1)=0 by A213,XCMPLX_1:6;
then pz`2-1=0 or pz`2+1=0 by XCMPLX_1:6;
hence -1 <=(gg.O)`1 & (gg.O)`1 <= 1 by A206,A207,A211;
A214: (|[pu`1/sqrt(1+(pu`1/pu`2)^2),pu`2/sqrt(1+(pu`1/pu`2)^2)]|)`2 = pu`2
/ sqrt(1+ (pu`1/pu`2)^2) & (|[pu`1/sqrt(1+(pu`1/pu`2)^2),pu`2/sqrt(1+(pu`1/pu`2
)^2)]|)`1 = pu`1/ sqrt(1+(pu`1/pu`2)^2) by EUCLID:52;
A215: (pu`1/pu`2)^2 >=0 by XREAL_1:63;
consider p4 being Point of TOP-REAL 2 such that
A216: g.I=p4 and
A217: |.p4.|=1 and
A218: p4`2>=p4`1 and
A219: p4`2>=-p4`1 by A1;
A220: -p4`2<=--p4`1 by A219,XREAL_1:24;
A221: (gg.I)=(Sq_Circ").(g.I) by A3,FUNCT_1:12;
then
A222: p4=Sq_Circ.pu by A216,FUNCT_1:32,JGRAPH_3:22,43;
A223: p4<>0.TOP-REAL 2 by A217,TOPRNS_1:23;
then
A224: Sq_Circ".p4=|[p4`1*sqrt(1+(p4`1/p4`2)^2),p4`2*sqrt(1+(p4`1/p4`2) ^2)
]| by A218,A220,JGRAPH_3:30;
then
A225: pu`2 = p4`2*sqrt(1+(p4`1/p4`2)^2) by A221,A216,EUCLID:52;
A226: pu`1 = p4`1*sqrt(1+(p4`1/p4`2)^2) by A221,A216,A224,EUCLID:52;
(p4`1/p4`2)^2 >=0 by XREAL_1:63;
then
A227: sqrt(1+(p4`1/p4`2)^2)>0 by SQUARE_1:25;
A228: now
assume pu`2=0 & pu`1=0;
then p4`2=0 & p4`1=0 by A225,A226,A227,XCMPLX_1:6;
hence contradiction by A223,EUCLID:53,54;
end;
A229: p4`1<=p4`2 & (-p4`2)*sqrt(1+(p4`1/p4`2)^2) <= p4`1*sqrt(1+(p4`1/p4`2
) ^2 ) or pu`1>=pu`2 & pu`1<=-pu`2 by A218,A220,A227,XREAL_1:64;
then
A230: p4`1* sqrt(1+(p4`1/p4`2)^2) <= p4`2*sqrt(1+(p4`1/p4`2)^2) & -pu`2<=
pu `1 or pu`1>=pu`2 & pu`1<=-pu`2 by A221,A216,A224,A225,A227,EUCLID:52
,XREAL_1:64;
then Sq_Circ.pu=|[pu`1/sqrt(1+(pu`1/pu`2)^2),pu`2/sqrt(1+(pu`1/pu`2)^2)]|
by A225,A226,A228,JGRAPH_2:3,JGRAPH_3:4;
then (|.p4.|)^2= (pu`2/sqrt(1+(pu`1/pu`2)^2))^2+(pu`1/sqrt(1+(pu`1/pu`2)
^2 ) ) ^2 by A222,A214,JGRAPH_3:1
.= (pu`2)^2/(sqrt(1+(pu`1/pu`2)^2))^2+(pu`1/sqrt(1+(pu`1/pu`2)^2))^2
by XCMPLX_1:76
.= (pu`2)^2/(sqrt(1+(pu`1/pu`2)^2))^2 +(pu`1)^2/(sqrt(1+(pu`1/pu`2)^2)
)^2 by XCMPLX_1:76
.= (pu`2)^2/(1+(pu`1/pu`2)^2)+(pu`1)^2/(sqrt(1+(pu`1/pu`2)^2))^2 by A215,
SQUARE_1:def 2
.= (pu`2)^2/(1+(pu`1/pu`2)^2)+(pu`1)^2/(1+(pu`1/pu`2)^2) by A215,
SQUARE_1:def 2
.= ((pu`2)^2+(pu`1)^2)/(1+(pu`1/pu`2)^2) by XCMPLX_1:62;
then ((pu`2)^2+(pu`1)^2)/(1+(pu`1/pu`2)^2)*(1+(pu`1/pu`2)^2)=(1)*(1+(pu`1
/pu `2)^2) by A217;
then ((pu`2)^2+(pu`1)^2)=(1+(pu`1/pu`2)^2) by A215,XCMPLX_1:87;
then
A231: (pu`2)^2+(pu`1)^2-1=(pu`1)^2/(pu`2)^2 by XCMPLX_1:76;
pu`2<>0 by A225,A226,A227,A228,A229,XREAL_1:64;
then ((pu`2)^2+(pu`1)^2-1)*(pu`2)^2=(pu`1)^2 by A231,XCMPLX_1:6,87;
then
A232: ((pu`2)^2-1)*((pu`2)^2+(pu`1)^2)=0;
((pu`2)^2+(pu`1)^2)<>0 by A228,COMPLEX1:1;
then (pu`2-1)*(pu`2+1)=0 by A232,XCMPLX_1:6;
then pu`2-1=0 or pu`2+1=0 by XCMPLX_1:6;
hence thesis by A225,A226,A230;
end;
then rng ff meets rng gg by A1,A5,A94,Th11,JGRAPH_3:22,42;
then consider y being object such that
A233: y in rng ff and
A234: y in rng gg by XBOOLE_0:3;
consider x1 being object such that
A235: x1 in dom ff and
A236: y=ff.x1 by A233,FUNCT_1:def 3;
consider x2 being object such that
A237: x2 in dom gg and
A238: y=gg.x2 by A234,FUNCT_1:def 3;
A239: dom (Sq_Circ")=the carrier of TOP-REAL 2 & gg.x2=Sq_Circ".(g.x2) by A237,
FUNCT_1:12,FUNCT_2:def 1,JGRAPH_3:29;
x1 in dom f by A235,FUNCT_1:11;
then
A240: f.x1 in rng f by FUNCT_1:def 3;
x2 in dom g by A237,FUNCT_1:11;
then
A241: g.x2 in rng g by FUNCT_1:def 3;
ff.x1=Sq_Circ".(f.x1) by A235,FUNCT_1:12;
then f.x1=g.x2 by A236,A238,A240,A241,A239,FUNCT_1:def 4,JGRAPH_3:22;
hence thesis by A240,A241,XBOOLE_0:3;
end;
theorem Th15:
for f,g being Function 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
KXN & f.I in KXP & 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 Function 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 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 KXN & f.I in KXP & g.O in KYP & g.I in KYN &
rng f c= C0 & rng g c= C0;
then
ex g2 being Function of I[01],TOP-REAL 2 st g2.0=g.1 & g2.1=g.0 & rng g2=
rng g & g2 is continuous one-to-one by Th12;
hence thesis by A1,Th14;
end;
theorem Th16:
for f,g being Function of I[01],TOP-REAL 2, C0 being Subset of
TOP-REAL 2 st C0={q: |.q.|>=1} & f is continuous one-to-one & g is continuous
one-to-one & f.0=|[-1,0]| & f.1=|[1,0]| & g.1=|[0,1]| & g.0=|[0,-1]| & rng f c=
C0 & rng g c= C0 holds rng f meets rng g
proof
reconsider I=1 as Point of I[01] by BORSUK_1:40,XXREAL_1:1;
reconsider O=0 as Point of I[01] by BORSUK_1:40,XXREAL_1:1;
defpred P[Point of TOP-REAL 2] means |.$1.|=1 & $1`2<=$1`1 & $1`2>=-$1`1;
let f,g be Function of I[01],TOP-REAL 2, C0 be Subset of TOP-REAL 2;
assume
A1: C0={q: |.q.|>=1} & f is continuous one-to-one & g is continuous
one-to-one & f.0=|[-1,0]| & f.1=|[1,0]| & g.1=|[0,1]| & g.0=|[0,-1]| & rng f c=
C0 & rng g c= C0;
{q1 where q1 is Point of TOP-REAL 2:P[q1] } is Subset of TOP-REAL 2 from
JGRAPH_2:sch 1;
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;
A2: (|[0,1]|)`1=0 by EUCLID:52;
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
JGRAPH_2:sch 1;
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
JGRAPH_2:sch 1;
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
JGRAPH_2:sch 1;
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;
A3: (|[0,-1]|)`1=0 by EUCLID:52;
(|[0,-1]|)`2=-1 by EUCLID:52;
then
A4: |.(|[0,-1]|).|=sqrt(0^2+(-1)^2) by A3,JGRAPH_3:1
.=1 by SQUARE_1:18;
(|[0,-1]|)`2 <=-((|[0,-1]|)`1) by A3,EUCLID:52;
then
A5: g.O in KYN by A1,A3,A4;
A6: (|[-1,0]|)`1=-1 by EUCLID:52;
then
A7: (|[-1,0]|)`2 <=-((|[-1,0]|)`1) by EUCLID:52;
(|[0,1]|)`2=1 by EUCLID:52;
then
A8: |. (|[0,1]|).|=sqrt(0^2+1^2) by A2,JGRAPH_3:1
.=1 by SQUARE_1:18;
(|[0,1]|)`2 >=-((|[0,1]|)`1) by A2,EUCLID:52;
then
A9: g.I in KYP by A1,A2,A8;
A10: (|[1,0]|)`1=1 & (|[1,0]|)`2=0 by EUCLID:52;
then |.(|[1,0]|).|=sqrt(1^2+0^2) by JGRAPH_3:1
.=1 by SQUARE_1:18;
then
A11: f.I in KXP by A1,A10;
A12: (|[-1,0]|)`2=0 by EUCLID:52;
then |. (|[-1,0]|).|=sqrt((-1)^2+0^2) by A6,JGRAPH_3:1
.=1 by SQUARE_1:18;
then f.O in KXN by A1,A6,A12,A7;
hence thesis by A1,A11,A5,A9,Th14;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, C0 being Subset of TOP-REAL
2 st C0={p: |.p.|>=1} & |.p1.|=1 & |.p2.|=1 & |.p3.|=1 & |.p4.|=1 & (ex h being
Function of TOP-REAL 2,TOP-REAL 2 st h is being_homeomorphism & h.:C0 c= C0 & h
.p1=|[-1,0]| & h.p2=|[0,1]| & h.p3=|[1,0]| & h.p4=|[0,-1]|) holds for f,g being
Function of I[01],TOP-REAL 2 st f is continuous one-to-one & g is continuous
one-to-one & f.0=p1 & f.1=p3 & 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, C0 be Subset of TOP-REAL 2;
assume
A1: C0={p: |.p.|>=1} & |.p1.|=1 & |.p2.|=1 & |.p3.|=1 & |.p4.|=1 & ex h
being Function of TOP-REAL 2,TOP-REAL 2 st h is being_homeomorphism & h.:C0 c=
C0 & h.p1=(|[-1,0]|) & h.p2=(|[0,1]|) & h.p3=(|[1,0]|) & h.p4=(|[0,-1]|);
then consider h being Function of TOP-REAL 2,TOP-REAL 2 such that
A2: h is being_homeomorphism and
A3: h.:C0 c= C0 and
A4: h.p1=(|[-1,0]|) and
A5: h.p2=(|[0,1]|) and
A6: h.p3=(|[1,0]|) and
A7: h.p4=(|[0,-1]|);
let f,g be Function of I[01],TOP-REAL 2;
assume that
A8: f is continuous one-to-one & g is continuous one-to-one and
A9: f.0=p1 and
A10: f.1=p3 and
A11: g.0=p4 and
A12: g.1=p2 and
A13: rng f c= C0 and
A14: rng g c= C0;
reconsider f2=h*f as Function of I[01],TOP-REAL 2;
0 in dom f2 by Lm1,BORSUK_1:40,FUNCT_2:def 1;
then
A15: f2.0=|[-1,0]| by A4,A9,FUNCT_1:12;
reconsider g2=h*g as Function of I[01],TOP-REAL 2;
0 in dom g2 by Lm1,BORSUK_1:40,FUNCT_2:def 1;
then
A16: g2.0=|[0,-1]| by A7,A11,FUNCT_1:12;
1 in dom g2 by Lm2,BORSUK_1:40,FUNCT_2:def 1;
then
A17: g2.1=|[0,1]| by A5,A12,FUNCT_1:12;
A18: rng f2 c= C0
proof
let y be object;
A19: dom h=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
assume y in rng f2;
then consider x being object such that
A20: x in dom f2 and
A21: y=f2.x by FUNCT_1:def 3;
x in dom f by A20,FUNCT_1:11;
then
A22: f.x in rng f by FUNCT_1:def 3;
y=h.(f.x) by A20,A21,FUNCT_1:12;
then y in h.:C0 by A13,A22,A19,FUNCT_1:def 6;
hence thesis by A3;
end;
A23: rng g2 c= C0
proof
let y be object;
A24: dom h=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
assume y in rng g2;
then consider x being object such that
A25: x in dom g2 and
A26: y=g2.x by FUNCT_1:def 3;
x in dom g by A25,FUNCT_1:11;
then
A27: g.x in rng g by FUNCT_1:def 3;
y=h.(g.x) by A25,A26,FUNCT_1:12;
then y in h.:C0 by A14,A27,A24,FUNCT_1:def 6;
hence thesis by A3;
end;
1 in dom f2 by Lm2,BORSUK_1:40,FUNCT_2:def 1;
then
A28: f2.1=|[1,0]| by A6,A10,FUNCT_1:12;
h is continuous & h is one-to-one by A2,TOPS_2:def 5;
then rng f2 meets rng g2 by A1,A8,A15,A28,A16,A17,A18,A23,Th16;
then consider q5 being object such that
A29: q5 in rng f2 and
A30: q5 in rng g2 by XBOOLE_0:3;
consider x being object such that
A31: x in dom f2 and
A32: q5=f2.x by A29,FUNCT_1:def 3;
x in dom f by A31,FUNCT_1:11;
then
A33: f.x in rng f by FUNCT_1:def 3;
consider u being object such that
A34: u in dom g2 and
A35: q5=g2.u by A30,FUNCT_1:def 3;
A36: q5=h.(g.u) & g.u in dom h by A34,A35,FUNCT_1:11,12;
A37: h is one-to-one by A2,TOPS_2:def 5;
u in dom g by A34,FUNCT_1:11;
then
A38: g.u in rng g by FUNCT_1:def 3;
q5=h.(f.x) & f.x in dom h by A31,A32,FUNCT_1:11,12;
then f.x=g.u by A37,A36,FUNCT_1:def 4;
hence thesis by A33,A38,XBOOLE_0:3;
end;
begin :: Properties of Fan Morphisms
theorem Th18:
for cn being Real,q being Point of TOP-REAL 2 st -1**