Copyright (c) 2001 Association of Mizar Users
environ
vocabulary ARYTM, SQUARE_1, EUCLID, PCOMPS_1, RELAT_1, FUNCT_5, PRE_TOPC,
MCART_1, ARYTM_1, ARYTM_3, RCOMP_1, COMPLEX1, FUNCT_1, BOOLE, SUBSET_1,
COMPTS_1, ORDINAL2, TOPMETR, JORDAN2C, FUNCT_4, PARTFUN1, METRIC_1,
TOPS_2, TOPREAL2, TOPREAL1, BORSUK_1, JGRAPH_3, SEQ_1;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, EUCLID, RELAT_1, TOPS_2, FUNCT_1, STRUCT_0, PARTFUN1, TOPREAL1,
TOPMETR, PCOMPS_1, COMPTS_1, METRIC_1, RCOMP_1, SQUARE_1, FUNCT_2,
PSCOMP_1, PRE_TOPC, JGRAPH_1, JORDAN2C, FUNCT_4, WELLFND1, TOPREAL2,
TOPGRP_1;
constructors REAL_1, GOBOARD5, TOPS_2, RCOMP_1, PSCOMP_1, JORDAN2C, COMPTS_1,
TOPREAL2, TOPGRP_1, CONNSP_1, TOPMETR, WELLFND1, TOPRNS_1;
clusters XREAL_0, STRUCT_0, RELSET_1, FUNCT_1, EUCLID, PRE_TOPC, SQUARE_1,
BORSUK_1, TOPREAL2, TOPREAL6, BORSUK_2, BORSUK_3, MEMBERED;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FUNCT_1, XBOOLE_0;
theorems TARSKI, AXIOMS, RELAT_1, SUBSET_1, FUNCT_1, FUNCT_2, FUNCT_4, TOPS_1,
TOPS_2, PARTFUN1, PRE_TOPC, REVROT_1, FRECHET, TOPMETR, JORDAN6, EUCLID,
RELSET_1, REAL_1, REAL_2, JGRAPH_1, SEQ_2, SQUARE_1, TOPREAL3, PSCOMP_1,
METRIC_1, SPPOL_2, JGRAPH_2, RCOMP_1, COMPTS_1, ZFMISC_1, GOBOARD6,
TOPGRP_1, TOPREAL1, TOPREAL2, RFUNCT_2, COMPLEX1, JORDAN1, XBOOLE_0,
XBOOLE_1, XREAL_0, TOPRNS_1, XCMPLX_0, XCMPLX_1;
schemes FUNCT_1, FUNCT_2, DOMAIN_1, JGRAPH_2;
begin ::Preliminaries
reserve x,y,z,u,a for real number;
Lm1: x^2+1 > 0
proof
x^2 >= 0 by SQUARE_1:72;
then x^2+1 >= 0+1 by REAL_1:55;
hence thesis by AXIOMS:22;
end;
Lm2:TOP-REAL 2=TopSpaceMetr(Euclid 2) by EUCLID:def 8;
Lm3:dom proj1=the carrier of TOP-REAL 2 &
dom proj2=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
theorem Th1: x^2=y^2 implies x=y or x=-y
proof assume x^2=y^2; then x^2-y^2=0 by XCMPLX_1:14;
then (x-y)*(x+y)=0 by SQUARE_1:67;
then x-y=0 or x+y=0 by XCMPLX_1:6;
then x=y or x=0-y by XCMPLX_1:15,26;
hence x=y or x=-y by XCMPLX_1:150;
end;
theorem Th2: x^2=1 implies x=1 or x=-1
proof assume x^2=1;
then x^2-1^2=0 by SQUARE_1:59;
then (x-1)*(x+1)=0 by SQUARE_1:67;
then x-1=0 or x+1=0 by XCMPLX_1:6;
then x-1+1=1 or x+1-1=0-1;
hence x=1 or x=-1 by XCMPLX_1:26,27;
end;
theorem Th3: 0<=x & x<=1 implies x^2<=x
proof assume A1:0<=x & x<=1;
per cases by A1;
suppose 0=x; hence x^2<=x by SQUARE_1:60;
suppose A2:0<x;
now per cases by A1,REAL_1:def 5;
case x=1; hence x^2<=x by SQUARE_1:59;
case x<1; hence x^2<=x by A2,SQUARE_1:75;
end;
hence x^2<=x;
end;
theorem Th4: a>=0 & (x-a)*(x+a)<=0 implies -a<=x & x<=a
proof assume A1:a>=0 & (x-a)*(x+a)<=0;
then A2:x-a>=0 & x+a<=0 or x-a<=0 & x+a>=0 by REAL_2:129;
x+0<=x+a by A1,REAL_1:55;
then x-a<=x+a-a by REAL_1:49;
then x-a<=x by XCMPLX_1:26;
then x<=a+0 & x+a>=0 by A1,A2,REAL_1:86;
then x<=a & x>=0-a by REAL_1:86;
hence -a<=x & x<=a by XCMPLX_1:150;
end;
theorem Th5:
x^2-1<=0 implies -1<=x & x<=1
proof assume x^2-1<=0;
then 1>=0 & (x-1)*(x+1)<=0 by SQUARE_1:59,67;
hence thesis by Th4;
end;
theorem Th6:
x < y & x < z iff x < min(y,z)
proof
thus x < y & x < z implies x < min(y,z) by SQUARE_1:38;
assume A1:x < min(y,z);
y>=min(y,z) & z>=min(y,z) by SQUARE_1:35;
hence thesis by A1,AXIOMS:22;
end;
theorem Th7:0<x implies x/3<x & x/4<x
proof
assume A1:0<x;
then A2: 0<x/3 by SEQ_2:6;
then A3:0+x/3<x/3+x/3 by REAL_1:53;
x/3+x/3+0<x/3+x/3+x/3 by A2,REAL_1:53;
then x/3+x/3<x by XCMPLX_1:69;
hence x/3<x by A3,AXIOMS:22;
A4: 0<x/4 by A1,SEQ_2:6;
then A5:0+x/4<x/4+x/4 by REAL_1:53;
x/4+x/4+0<x/4+x/4+x/4 by A4,REAL_1:53;
then x/4< x/4+x/4+x/4 by A5,AXIOMS:22;
then x/4+x/4<x/4+x/4+x/4+x/4 by REAL_1:53;
then x/4+x/4< x by XCMPLX_1:71;
hence x/4<x by A5,AXIOMS:22;
end;
theorem Th8: (x>=1 implies sqrt x>=1) & (x>1 implies sqrt x>1)
proof
hereby assume x>=1; hence sqrt x>=1 by SQUARE_1:83,94;
end;
assume x>1; hence sqrt x>1 by SQUARE_1:83,95;
end;
theorem Th9: x<=y & z<=u implies ].y,z.[ c= ].x,u.[
proof assume A1:x<=y & z<=u;
let a be set;assume a in ].y,z.[;
then a in {b where b is Real: y<b & b<z} by RCOMP_1:def 2;
then consider b being Real such that A2:b=a & y<b & b<z;
x<b & b<u by A1,A2,AXIOMS:22;
hence a in ].x,u.[ by A2,JORDAN6:45;
end;
theorem for p being Point of TOP-REAL 2 holds
|.p.| = sqrt((p`1)^2+(p`2)^2) &
|.p.|^2 = (p`1)^2+(p`2)^2 by JGRAPH_1:46,47;
theorem for f being Function,B,C being set holds (f|B).:C = f.:(C /\ B)
proof let f be Function,B,C be set;
thus (f|B).:C c=f.:(C /\ B)
proof let x be set;assume x in (f|B).:C;
then consider y being set such that
A1: y in dom (f|B) & y in C & x=(f|B).y by FUNCT_1:def 12;
dom (f|B)=(dom f)/\ B by FUNCT_1:68;
then A2:y in dom f & y in B by A1,XBOOLE_0:def 3;
then A3:y in C /\ B by A1,XBOOLE_0:def 3;
(f|B).y=f.y by A1,FUNCT_1:68;
hence thesis by A1,A2,A3,FUNCT_1:def 12;
end;
let x be set;assume x in f.:(C /\ B);
then consider y being set such that
A4: y in dom f & y in C /\ B & x=f.y by FUNCT_1:def 12;
A5: y in C & y in B by A4,XBOOLE_0:def 3;
then y in (dom f)/\ B by A4,XBOOLE_0:def 3;
then A6:y in dom (f|B) by FUNCT_1:68;
then (f|B).y=f.y by FUNCT_1:68;
hence thesis by A4,A5,A6,FUNCT_1:def 12;
end;
theorem Th12: for X being TopStruct,Y being non empty TopStruct,
f being map of X,Y,
P being Subset of X holds f|P is map of X|P,Y
proof let X be TopStruct,Y be non empty TopStruct,f be map of X,Y,
P be Subset of X;
set Q=P;
Q = the carrier of (X|Q) by JORDAN1:1;
then f|P is Function of the carrier of (X|P),the carrier of Y by FUNCT_2:38;
hence thesis ;
end;
theorem Th13:for X,Y being non empty TopSpace,
p0 being Point of X,
D being non empty Subset of X,
E being non empty Subset of Y,
f being map of X,Y
st D`={p0} & E`={f.p0} & X is_T2 & Y is_T2 &
(for p being Point of X|D holds f.p<>f.p0)&
(ex h being map of X|D,Y|E st h=f|D & h is continuous) &
(for V being Subset of Y st f.p0 in V & V is open
ex W being Subset of X st p0 in W & W is open & f.:W c= V)
holds f is continuous
proof let X,Y be non empty TopSpace,
p0 be Point of X,
D be non empty Subset of X,
E be non empty Subset of Y,
f be map of X,Y;
assume A1:D`={p0} & E`={f.p0} & X is_T2 & Y is_T2 &
(for p being Point of X|D holds f.p<>f.p0)&
(ex h being map of X|D,Y|E st h=f|D & h is continuous) &
(for V being Subset of Y st f.p0 in V & V is open
ex W being Subset of X st p0 in W & W is open & f.:W c= V);
for p being Point of X,V being Subset of Y
st f.p in V & V is open holds
ex W being Subset of X st p in W & W is open & f.:W c= V
proof let p be Point of X,V be Subset of Y;
assume A2:f.p in V & V is open;
A3:the carrier of X|D=D by JORDAN1:1;
per cases;
suppose p=p0;
hence thesis by A1,A2;
suppose A4:p<>p0;
then not p in D` by A1,TARSKI:def 1;
then p in (the carrier of X)\D` by XBOOLE_0:def 4;
then A5: p in D`` by SUBSET_1:def 5;
then f.p<>f.p0 by A1,A3;
then consider G1,G2 being Subset of Y such that
A6: G1 is open & G2 is open &
f.p in G1 & f.p0 in G2 & G1 misses G2 by A1,COMPTS_1:def 4;
consider h being map of X|D,Y|E such that
A7: h=f|D & h is continuous by A1;
A8:[#](X|D)=D by PRE_TOPC:def 10;
then reconsider p22=p as Point of X|D by A5;
A9:the carrier of Y|E=[#](Y|E) by PRE_TOPC:12;
A10:[#](Y|E)=E by PRE_TOPC:def 10;
then (G1 /\ V) /\ E c= the carrier of Y|E by A9,XBOOLE_1:17;
then reconsider V20=(G1 /\ V) /\ E as Subset of Y|E;
A11:h.p=f.p by A5,A7,FUNCT_1:72;
f.p<>f.p0 by A1,A5,A8;
then not f.p in E` by A1,TARSKI:def 1;
then not f.p in (the carrier of Y) \E by SUBSET_1:def 5;
then A12:h.p22 in E by A11,XBOOLE_0:def 4;
h.p22 in G1 /\ V by A2,A6,A11,XBOOLE_0:def 3;
then A13:h.p22 in V20 by A12,XBOOLE_0:def 3;
G1 /\ V is open by A2,A6,TOPS_1:38;
then V20 is open by A10,TOPS_2:32;
then consider W2 being Subset of X|D such that
A14:p22 in W2 & W2 is open & h.:W2 c= V20 by A7,A13,JGRAPH_2:20;
consider W3b being Subset of X such that
A15: W3b is open & W2=W3b /\ D by A8,A14,TOPS_2:32;
A16:p22 in W3b by A14,A15,XBOOLE_0:def 3;
consider H1,H2 being Subset of X such that
A17: H1 is open & H2 is open &
p in H1 & p0 in H2 & H1 misses H2 by A1,A4,COMPTS_1:def 4;
A18:H1 /\ W3b is open by A15,A17,TOPS_1:38;
A19:p in H1 /\ W3b by A16,A17,XBOOLE_0:def 3;
reconsider W3=H1 /\ W3b as Subset of X;
A20:W3 c= W3b by XBOOLE_1:17;
A21:f.:W3 c= h.:W2
proof let xx be set;assume xx in f.:W3;
then consider yy being set such that
A22: yy in dom f & yy in W3 & xx=f.yy by FUNCT_1:def 12;
A23:dom h=dom f /\ D by A7,FUNCT_1:68;
A24:W3 c= H1 by XBOOLE_1:17;
H2 c= H1` by A17,SUBSET_1:43;
then D` c= H1` by A1,A17,ZFMISC_1:37;
then H1 c= D by SUBSET_1:31;
then A25:W3 c= D by A24,XBOOLE_1:1;
then A26:yy in dom h by A22,A23,XBOOLE_0:def 3;
then A27:h.yy=f.yy by A7,FUNCT_1:70;
yy in W2 by A15,A20,A22,A25,XBOOLE_0:def 3;
hence xx in h.:W2 by A22,A26,A27,FUNCT_1:def 12;
end;
A28:(G1 /\ V) /\ E c= G1 /\ V by XBOOLE_1:17;
A29:G1 /\ V c= V by XBOOLE_1:17;
h.:W2 c= G1 /\ V by A14,A28,XBOOLE_1:1;
then h.:W2 c= V by A29,XBOOLE_1:1;
then f.:W3 c= V by A21,XBOOLE_1:1;
hence thesis by A18,A19;
end;
hence thesis by JGRAPH_2:20;
end;
begin ::The Circle is a Simple Closed Curve
reserve p,q for Point of TOP-REAL 2;
definition
func Sq_Circ -> Function of the carrier of TOP-REAL 2,
the carrier of TOP-REAL 2 means :Def1:
for p being Point of TOP-REAL 2 holds
(p=0.REAL 2 implies it.p=p) &
((p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
it.p=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|)&
(not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
it.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|);
existence
proof
set BP= the carrier of TOP-REAL 2;
defpred P[set,set] means
(for p being Point of TOP-REAL 2 st p=$1 holds
(p=0.REAL 2 implies $2=p)&
((p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
$2=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|)&
(not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
$2=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|));
A1:for x being Element of BP ex y being Element of BP st P[x,y]
proof let x be Element of BP;
set q=x;
per cases;
suppose q=0.REAL 2;
then for p being Point of TOP-REAL 2 st p=x holds
(p=0.REAL 2 implies 0.REAL 2=p)&
((p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
0.REAL 2=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|)&
(not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
0.REAL 2=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|);
hence thesis;
suppose A2:(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1) & q<>0.REAL 2;
set r= |[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|;
for p being Point of TOP-REAL 2 st p=x holds
(p=0.REAL 2 implies r=p)&
((p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
r=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|)&
(not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
r=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|) by A2;
hence thesis;
suppose A3:not (q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1) & q<>0.REAL 2;
set r= |[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|;
for p being Point of TOP-REAL 2 st p=x holds
(p=0.REAL 2 implies r=p)&
((p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
r=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|)&
(not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
r=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|) by A3;
hence thesis;
end;
ex h being Function of BP, BP st for x being Element of BP holds
P[x,h.x] from FuncExD(A1);
then consider h being Function of BP,BP such that
A4: for x being Element of BP holds
for p being Point of TOP-REAL 2 st p=x holds
(p=0.REAL 2 implies h.x=p)&
((p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
h.x=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|)&
(not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
h.x=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|);
for p being Point of TOP-REAL 2 holds
(p=0.REAL 2 implies h.p=p)&
((p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
h.p=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|)&
(not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
h.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|) by A4;
hence thesis;
end;
uniqueness
proof
let h1,h2 be Function of the carrier of TOP-REAL 2,
the carrier of TOP-REAL 2;
assume A5:(for p being Point of TOP-REAL 2 holds
(p=0.REAL 2 implies h1.p=p)&
((p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
h1.p=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|)&
(not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
h1.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|))&
(for p being Point of TOP-REAL 2 holds
(p=0.REAL 2 implies h2.p=p)&
((p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
h2.p=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|)&
(not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
h2.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|));
for x being set st x in (the carrier of TOP-REAL 2) holds h1.x=h2.x
proof let x be set;
assume x in the carrier of TOP-REAL 2;
then reconsider q=x as Point of TOP-REAL 2;
per cases;
suppose A6:q=0.REAL 2;
then h1.q=q by A5;
hence h1.x=h2.x by A5,A6;
suppose A7:(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1)& q<>0.REAL 2;
then h1.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]| by A5;
hence h1.x=h2.x by A5,A7;
suppose A8:not (q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1)
& q<>0.REAL 2;
then h1.q=|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]| by A5;
hence h1.x=h2.x by A5,A8;
end;
hence h1=h2 by FUNCT_2:18;
end;
end;
theorem Th14: for p being Point of TOP-REAL 2 st p<>0.REAL 2 holds
((p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2)implies
Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|) &
(not(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) implies
Sq_Circ.p=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|)
proof let p be Point of TOP-REAL 2;assume
A1: p<>0.REAL 2;
hereby assume A2:p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2;
now per cases by A2;
case A3:p`1<=p`2 & -p`2<=p`1;
now assume A4:p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1;
A5: now per cases by A4;
case p`2<=p`1 & -p`1<=p`2;
hence p`1=p`2 or p`1=-p`2 by A3,AXIOMS:21;
case p`2>=p`1 & p`2<=-p`1; then -p`2>=--p`1 by REAL_1:50;
hence p`1=p`2 or p`1=-p`2 by A3,AXIOMS:21;
end;
now per cases by A5;
case p`1=p`2;
hence Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)
]|
by A1,A4,Def1;
case A6:p`1=-p`2;
A7:now assume A8:p`1=0;
then p`2=-0 by A6 .=0;
hence contradiction by A1,A8,EUCLID:57,58;
end;
A9:-p`1=p`2 by A6;
p`2<>0 by A6,A7;
then p`1/p`2=-1 by A6,XCMPLX_1:198;
then A10:(p`1/p`2)^2=1^2 by SQUARE_1:61;
p`2/p`1=-1 by A7,A9,XCMPLX_1:198;
then (p`2/p`1)^2=1^2 by SQUARE_1:61;
hence Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|
by A1,A4,A10,Def1;
end;
hence Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|;
end;
hence Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|
by A1,Def1;
case A11:p`1>=p`2 & p`1<=-p`2;
now assume A12:p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1;
A13: now per cases by A12;
case p`2<=p`1 & -p`1<=p`2; then --p`1>=-p`2 by REAL_1:50;
hence p`1=p`2 or p`1=-p`2 by A11,AXIOMS:21;
case p`2>=p`1 & p`2<=-p`1;
hence p`1=p`2 or p`1=-p`2 by A11,AXIOMS:21;
end;
now per cases by A13;
case p`1=p`2;
hence Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|
by A1,A12,Def1;
case A14:p`1=-p`2;
A15:now assume A16:p`1=0;
then p`2=-0 by A14 .=0;
hence contradiction by A1,A16,EUCLID:57,58;
end;
A17:-p`1=p`2 by A14;
p`2<>0 by A14,A15;
then p`1/p`2=-1 by A14,XCMPLX_1:198;
then A18:(p`1/p`2)^2=1^2 by SQUARE_1:61;
p`2/p`1=-1 by A15,A17,XCMPLX_1:198;
then (p`2/p`1)^2=1^2 by SQUARE_1:61;
hence Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|
by A1,A12,A18,Def1;
end;
hence Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|;
end;
hence Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|
by A1,Def1;
end;
hence Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|;
end;
assume A19:not(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2);
A20:-p`2<p`1 implies --p`2>-p`1 by REAL_1:50;
-p`2>p`1 implies --p`2<-p`1 by REAL_1:50;
hence thesis by A1,A19,A20,Def1;
end;
theorem Th15: for X being non empty TopSpace,
f1 being map of X,R^1 st f1 is continuous &
(for q being Point of X ex r being real number st f1.q=r & r>=0)
holds ex g being map of X,R^1
st (for p being Point of X,r1 being real number st
f1.p=r1 holds g.p=sqrt(r1)) & g is continuous
proof let X being non empty TopSpace,f1 be map of X,R^1;
assume A1: f1 is continuous &
(for q being Point of X ex r being real number st f1.q=r & r>=0);
defpred P[set,set] means
(for r11 being real number st f1.$1=r11 holds $2=sqrt(r11));
A2:for x being Element of X
ex y being Element of REAL st P[x,y]
proof let x be Element of X;
reconsider pp=x as Point of X;
reconsider r1=f1.pp as Real by TOPMETR:24;
for r11 being real number st f1.x=r11 holds sqrt(r1)=sqrt(r11);
hence thesis;
end;
ex f being Function of the carrier of X,REAL
st for x2 being Element of X holds P[x2,f.x2]
from FuncExD(A2);
then consider f being Function of the carrier of X,REAL
such that A3: for x2 being Element of X holds
(for r11 being real number st f1.x2=r11 holds f.x2=sqrt(r11));
reconsider g0=f as map of X,R^1 by TOPMETR:24;
A4: for p being Point of X,r11 being real number st
f1.p=r11 holds g0.p=sqrt(r11) by A3;
for p being Point of X,V being Subset of R^1
st g0.p in V & V is open holds
ex W being Subset of X st p in W & W is open & g0.:W c= V
proof let p be Point of X,V be Subset of R^1;
assume A5:g0.p in V & V is open;
reconsider r=g0.p as Real by TOPMETR:24;
reconsider r1=f1.p as Real by TOPMETR:24;
consider r8 being real number such that
A6: f1.p=r8 & r8>=0 by A1;
A7: r=sqrt(r1) by A3;
then A8:r>=0 by A6,SQUARE_1:82,94;
consider r01 being Real such that
A9: r01>0 & ].r-r01,r+r01.[ c= V by A5,FRECHET:8;
set r0=min(r01,1);
A10:r0>0 by A9,Th6;
A11:r1=r^2 by A6,A7,SQUARE_1:def 4;
A12: r+r0>=r+0 by A10,REAL_1:55;
r0<=r01 by SQUARE_1:35;
then r-r01<=r-r0 & r+r0<=r+r01 by REAL_1:55,REAL_2:106;
then ].r-r0,r+r0.[ c= ].r-r01,r+r01.[ by Th9;
then A13: r0>0 & ].r-r0,r+r0.[ c= V by A9,Th6,XBOOLE_1:1;
then A14:r0^2>0 by SQUARE_1:74;
2*r>=0 by A8,REAL_2:121;
then 2*r*r0>=0 by A13,REAL_2:121;
then A15:2*r*r0+r0^2>0+0 by A14,REAL_1:67;
A16:(r-r0)^2>=0 by SQUARE_1:72;
per cases;
suppose A17: r-r0>0;
now assume r1=0; then r=0 by A3,SQUARE_1:82;
then -r0>0 by A17,XCMPLX_1:150;
hence contradiction by A10,REAL_1:66;
end;
then A18:0<r by A6,A7,SQUARE_1:93;
set r4=r0*(r-r0);
A19:r4>0 by A13,A17,REAL_2:122;
then A20:r1+r4>0+0 by A6,REAL_1:67;
r0*r0>0 by A13,REAL_2:122;
then A21:2*(r0*r0)>0 by REAL_2:122;
A22:r0*r>0 by A13,A18,REAL_2:122;
then 0+r*r0< r*r0+r*r0 by REAL_1:67;
then r0*r< 2*(r*r0) by XCMPLX_1:11;
then r0*r< 2*r*r0 by XCMPLX_1:4;
then r0*r+0< 2*r*r0+2*(r0*r0) by A21,REAL_1:67;
then r0*r< 2*r*r0+(r0*r0+r0*r0) by XCMPLX_1:11;
then r0*r< 2*r*r0+r0*r0+r0*r0 by XCMPLX_1:1;
then r0*r-r0*r0+r0*r0< 2*r*r0+r0*r0+r0*r0 by XCMPLX_1:27;
then r0*r-r0*r0< 2*r*r0+r0*r0 by REAL_1:55;
then r4 <2*r*r0+r0*r0 by XCMPLX_1:40;
then r4 <2*r*r0+r0^2 by SQUARE_1:def 3;
then r1+r4 <r^2+(2*r*r0+r0^2) by A11,REAL_1:67;
then r1+r4 <r^2+2*r*r0+r0^2 by XCMPLX_1:1;
then r1+r4 <(r+r0)^2 by SQUARE_1:63;
then sqrt(r1+r4)<sqrt((r+r0)^2) by A20,SQUARE_1:95;
then A23:r+r0>sqrt(r1+r4) by A8,A12,SQUARE_1:89;
0+r*r0< r*r0+r*r0 by A22,REAL_1:67;
then r0*r< 2*(r*r0) by XCMPLX_1:11;
then r0*r< 2*r*r0 by XCMPLX_1:4;
then r0*r-r0*r0< 2*r*r0-r0*r0 by REAL_1:92;
then r4 <2*r*r0-r0*r0 by XCMPLX_1:40;
then r4 <2*r*r0-r0^2 by SQUARE_1:def 3;
then -r4 >-(2*r*r0-r0^2) by REAL_1:50;
then r1+-r4 >r^2+-(2*r*r0-r0^2) by A11,REAL_1:67;
then r1-r4 >r^2+-(2*r*r0-r0^2) by XCMPLX_0:def 8;
then r1-r4 >r^2-(2*r*r0-r0^2) by XCMPLX_0:def 8;
then r1-r4 >r^2-2*r*r0+r0^2 by XCMPLX_1:37;
then r1-r4 >(r-r0)^2 by SQUARE_1:64;
then sqrt(r1-r4)>sqrt((r-r0)^2) by A16,SQUARE_1:95;
then A24:sqrt(r1-r4)>r-r0 by A17,SQUARE_1:89;
4=2*2 .= 2^2 by SQUARE_1:def 3;
then A25:1/4=(1/2)^2 by SQUARE_1:59,69;
A26:r1-r4=r^2-(r0*r-r0*r0)by A11,XCMPLX_1:40
.=r^2-r0*r+r0*r0 by XCMPLX_1:37
.=r^2-(2*(1/2))*r0*r+r0^2 by SQUARE_1:def 3
.=r^2-2*((1/2)*r0)*r+(1/4+3/4)*r0^2 by XCMPLX_1:4
.=r^2-2*((1/2)*r0)*r+((1/4)*r0^2+(3/4)*r0^2) by XCMPLX_1:8
.=r^2-2*((1/2)*r0)*r+(1/4)*r0^2+(3/4)*r0^2 by XCMPLX_1:1
.=r^2-2*((1/2)*r0)*r+((1/2)*r0)^2+(3/4)*r0^2 by A25,SQUARE_1:68
.=r^2-2*r*((1/2)*r0)+((1/2)*r0)^2+(3/4)*r0^2 by XCMPLX_1:4
.=(r-(1/2)*r0)^2+(3/4)*r0^2 by SQUARE_1:64;
A27:(r-(1/2)*r0)^2>=0 by SQUARE_1:72;
r0^2>=0 by SQUARE_1:72;
then (3/4)*r0^2>=0 by REAL_2:121;
then A28:r1-r4>=0+0 by A26,A27,REAL_1:55;
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1
by TOPMETR:24;
A29:r1<r1+r4 by A19,REAL_1:69;
then r1-r4<r1 by REAL_1:84;
then A30:f1.p in G1 by A29,JORDAN6:45;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A31: p in W1 & W1 is open & f1.:W1 c= G1 by A1,A30,JGRAPH_2:20;
set W=W1;
g0.:W c= ].r-r0,r+r0.[
proof let x be set;assume x in g0.:W;
then consider z being set such that
A32: z in dom g0 & z in W & g0.z=x by FUNCT_1:def 12;
reconsider pz=z as Point of X by A32;
pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then A33:f1.pz in f1.:W1 by A32,FUNCT_1:def 12;
reconsider aa1=f1.pz as Real by TOPMETR:24;
consider r9 being real number such that A34:f1.pz=r9 & r9>=0 by A1;
A35:x=sqrt(aa1) by A3,A32;
A36:r1-r4<aa1 & aa1<r1+r4 by A31,A33,JORDAN6:45;
then sqrt(aa1)<sqrt(r1+r4) by A34,SQUARE_1:95;
then A37: sqrt(aa1)< r+r0 by A23,AXIOMS:22;
now per cases;
case 0<=r1-r4; then sqrt(r1-r4)<=sqrt(aa1) by A36,SQUARE_1:94;
hence r-r0< sqrt(aa1) by A24,AXIOMS:22;
case 0>r1-r4; hence contradiction by A28;
end;
hence x in ].r-r0,r+r0.[ by A35,A37,JORDAN6:45;
end;
then g0.:W c= V by A13,XBOOLE_1:1;
hence thesis by A31;
suppose A38:r-r0<=0;
set r4=(2*r*r0+r0^2)/3;
A39:(2*r*r0+r0^2)/3>0 by A15,REAL_2:127;
then A40: r1+r4>0+0 by A6,REAL_1:67;
(2*r*r0+r0^2)/3<(2*r*r0+r0^2) by A15,Th7;
then r1+r4 <r^2+(2*r*r0+r0^2) by A11,REAL_1:67;
then r1+r4 <=r^2+2*r*r0+r0^2 by XCMPLX_1:1;
then r1+r4 <=(r+r0)^2 by SQUARE_1:63;
then sqrt(r1+r4)<=sqrt((r+r0)^2) by A40,SQUARE_1:94;
then A41:r+r0>=sqrt(r1+r4) by A8,A12,SQUARE_1:89;
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1
by TOPMETR:24;
A42:r1<r1+r4 by A39,REAL_1:69;
then r1-r4<r1 by REAL_1:84;
then A43:f1.p in G1 by A42,JORDAN6:45;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A44: p in W1 & W1 is open & f1.:W1 c= G1 by A1,A43,JGRAPH_2:20;
set W=W1;
g0.:W c= ].r-r0,r+r0.[
proof let x be set;assume x in g0.:W;
then consider z being set such that
A45: z in dom g0 & z in W & g0.z=x by FUNCT_1:def 12;
reconsider pz=z as Point of X by A45;
pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then A46:f1.pz in f1.:W1 by A45,FUNCT_1:def 12;
reconsider aa1=f1.pz as Real by TOPMETR:24;
consider r9 being real number such that A47:f1.pz=r9 & r9>=0 by A1;
A48:x=sqrt(aa1) by A3,A45;
A49:r1-r4<aa1 & aa1<r1+r4 by A44,A46,JORDAN6:45;
then sqrt(aa1)<sqrt(r1+r4) by A47,SQUARE_1:95;
then A50: sqrt(aa1)< r+r0 by A41,AXIOMS:22;
A51:0<=sqrt(aa1) by A47,SQUARE_1:82,94;
now per cases by A38;
case A52:r-r0=0;
then r=r0 by XCMPLX_1:15;
then r4=(2*(r0*r0)+r0^2)/3 by XCMPLX_1:4
.=(2*r0^2+r0^2)/3 by SQUARE_1:def 3
.=(r0^2+r0^2+r0^2)/3 by XCMPLX_1:11
.=r0^2 by XCMPLX_1:68;
then r1-r4=(r-r0)*(r+r0) by A11,SQUARE_1:67 .=0 by A52;
hence r-r0<sqrt(aa1) by A49,A52,SQUARE_1:82,95;
case r-r0<0;
hence r-r0<sqrt(aa1) by A51;
end;
hence x in ].r-r0,r+r0.[ by A48,A50,JORDAN6:45;
end;
then g0.:W c= V by A13,XBOOLE_1:1;
hence thesis by A44;
end;
then g0 is continuous by JGRAPH_2:20;
hence thesis by A4;
end;
theorem Th16: for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous & f2 is continuous &
(for q being Point of X holds f2.q<>0)
holds ex g being map of X,R^1
st (for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g.p=(r1/r2)^2) & g is continuous
proof let X be non empty TopSpace,
f1,f2 be map of X,R^1;
assume f1 is continuous & f2 is continuous
& (for q being Point of X holds f2.q<>0);
then consider g2 being map of X,R^1 such that
A1: (for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g2.p=r1/r2) & g2 is continuous by JGRAPH_2:37;
consider g3 being map of X,R^1 such that
A2: (for p being Point of X,r1 being real number st
g2.p=r1 holds g3.p=r1*r1) & g3 is continuous by A1,JGRAPH_2:32;
for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g3.p=(r1/r2)^2
proof let p be Point of X,r1,r2 be real number;
assume f1.p=r1 & f2.p=r2;
then g2.p=r1/r2 by A1;
then g3.p=(r1/r2)*(r1/r2) by A2;
hence thesis by SQUARE_1:def 3;
end;
hence thesis by A2;
end;
theorem Th17: for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous & f2 is continuous &
(for q being Point of X holds f2.q<>0)
holds ex g being map of X,R^1
st (for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g.p=1+(r1/r2)^2) & g is continuous
proof let X be non empty TopSpace,
f1,f2 be map of X,R^1;
assume f1 is continuous & f2 is continuous
& (for q being Point of X holds f2.q<>0);
then consider g2 being map of X,R^1
such that A1: (for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g2.p=(r1/r2)^2) & g2 is continuous by Th16;
consider g3 being map of X,R^1 such that
A2: (for p being Point of X,r1 being real number st
g2.p=r1 holds g3.p=r1+1) & g3 is continuous by A1,JGRAPH_2:34;
for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g3.p=1+(r1/r2)^2
proof let p be Point of X,r1,r2 be real number;
assume f1.p=r1 & f2.p=r2;
then g2.p=(r1/r2)^2 by A1;
hence thesis by A2;
end;
hence thesis by A2;
end;
theorem Th18: for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous & f2 is continuous &
(for q being Point of X holds f2.q<>0)
holds ex g being map of X,R^1
st (for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g.p=sqrt(1+(r1/r2)^2)) & g is continuous
proof let X be non empty TopSpace,
f1,f2 be map of X,R^1;
assume f1 is continuous & f2 is continuous
& (for q being Point of X holds f2.q<>0);
then consider g2 being map of X,R^1
such that A1: (for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g2.p=1+(r1/r2)^2) & g2 is continuous by Th17;
for q being Point of X ex r being real number st g2.q=r & r>=0
proof let q be Point of X;
reconsider r1=f1.q,r2=f2.q as Real by TOPMETR:24;
A2:g2.q=1+(r1/r2)^2 by A1;
1+(r1/r2)^2>0 by Lm1;
hence thesis by A2;
end;
then consider g3 being map of X,R^1 such that
A3: (for p being Point of X,r1 being real number st
g2.p=r1 holds g3.p=sqrt(r1)) & g3 is continuous by A1,Th15;
for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g3.p=sqrt(1+(r1/r2)^2)
proof let p be Point of X,r1,r2 be real number;
assume f1.p=r1 & f2.p=r2;
then g2.p=1+(r1/r2)^2 by A1;
hence thesis by A3;
end;
hence thesis by A3;
end;
theorem Th19: for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous & f2 is continuous &
(for q being Point of X holds f2.q<>0)
holds ex g being map of X,R^1
st (for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g.p=r1/sqrt(1+(r1/r2)^2)) & g is continuous
proof let X be non empty TopSpace,f1,f2 be map of X,R^1;
assume A1:f1 is continuous & f2 is continuous
& (for q being Point of X holds f2.q<>0);
then consider g2 being map of X,R^1
such that A2: (for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g2.p=sqrt(1+(r1/r2)^2)) & g2 is continuous
by Th18;
for q being Point of X holds g2.q<>0
proof let q be Point of X;
reconsider r1=f1.q,r2=f2.q as Real by TOPMETR:24;
1+(r1/r2)^2>0 by Lm1;
then sqrt(1+(r1/r2)^2)>0 by SQUARE_1:93;
hence thesis by A2;
end;
then consider g3 being map of X,R^1 such that
A3: (for p being Point of X,r1,r0 being real number st
f1.p=r1 & g2.p=r0 holds g3.p=r1/r0) & g3 is continuous
by A1,A2,JGRAPH_2:37;
for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g3.p=r1/sqrt(1+(r1/r2)^2)
proof let p be Point of X,r1,r2 be real number;
assume A4:f1.p=r1 & f2.p=r2;
then g2.p=sqrt(1+(r1/r2)^2) by A2;
hence thesis by A3,A4;
end;
hence thesis by A3;
end;
theorem Th20: for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous & f2 is continuous &
(for q being Point of X holds f2.q<>0)
holds ex g being map of X,R^1
st (for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g.p=r2/sqrt(1+(r1/r2)^2)) & g is continuous
proof let X be non empty TopSpace,
f1,f2 be map of X,R^1;
assume A1:f1 is continuous & f2 is continuous
& (for q being Point of X holds f2.q<>0);
then consider g2 being map of X,R^1
such that A2: (for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g2.p=sqrt(1+(r1/r2)^2)) & g2 is continuous
by Th18;
for q being Point of X holds g2.q<>0
proof let q be Point of X;
reconsider r1=f1.q,r2=f2.q as Real by TOPMETR:24;
1+(r1/r2)^2>0 by Lm1;
then sqrt(1+(r1/r2)^2)>0 by SQUARE_1:93;
hence thesis by A2;
end;
then consider g3 being map of X,R^1
such that A3: (for p being Point of X,r2,r0 being real number st
f2.p=r2 & g2.p=r0 holds g3.p=r2/r0) & g3 is continuous
by A1,A2,JGRAPH_2:37;
for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g3.p=r2/sqrt(1+(r1/r2)^2)
proof let p be Point of X,r1,r2 be real number;
assume A4:f1.p=r1 & f2.p=r2;
then g2.p=sqrt(1+(r1/r2)^2) by A2;
hence thesis by A3,A4;
end;
hence thesis by A3;
end;
Lm4: for K1 being non empty Subset of TOP-REAL 2 holds
for q being Point of (TOP-REAL 2)|K1 holds (proj2|K1).q=proj2.q
proof
let K1 be non empty Subset of TOP-REAL 2;
let q be Point of (TOP-REAL 2)|K1;
A1: the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
q in the carrier of (TOP-REAL 2)|K1;
then q in dom proj2 /\ K1 by A1,Lm3,XBOOLE_0:def 3;
hence thesis by FUNCT_1:71;
end;
Lm5: for K1 being non empty Subset of TOP-REAL 2 holds
proj2|K1 is continuous map of (TOP-REAL 2)|K1,R^1
proof
let K1 be non empty Subset of TOP-REAL 2;
A1: the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
proj2|K1 is Function of K1,the carrier of R^1 by FUNCT_2:38,TOPMETR:24;
then reconsider g2=proj2|K1 as map of (TOP-REAL 2)|K1,R^1 by A1;
for q be Point of (TOP-REAL 2)|K1 holds g2.q=proj2.q by Lm4;
hence thesis by JGRAPH_2:40;
end;
Lm6: for K1 being non empty Subset of TOP-REAL 2 holds
for q being Point of (TOP-REAL 2)|K1 holds (proj1|K1).q=proj1.q
proof
let K1 be non empty Subset of TOP-REAL 2;
let q be Point of (TOP-REAL 2)|K1;
A1: the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
q in the carrier of (TOP-REAL 2)|K1;
then q in dom proj1 /\ K1 by A1,Lm3,XBOOLE_0:def 3;
hence thesis by FUNCT_1:71;
end;
Lm7: for K1 being non empty Subset of TOP-REAL 2 holds
proj1|K1 is continuous map of (TOP-REAL 2)|K1,R^1
proof
let K1 be non empty Subset of TOP-REAL 2;
A1: the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
proj1|K1 is Function of K1,the carrier of R^1 by FUNCT_2:38,TOPMETR:24;
then reconsider g2=proj1|K1 as map of (TOP-REAL 2)|K1,R^1 by A1;
for q be Point of (TOP-REAL 2)|K1 holds g2.q=proj1.q by Lm6;
hence thesis by JGRAPH_2:39;
end;
theorem Th21: for K1 being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K1,R^1 st
(for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f.p=p`1/sqrt(1+(p`2/p`1)^2)) & (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`1<>0 ) holds
f is continuous
proof let K1 be non empty Subset of TOP-REAL 2,
f be map of (TOP-REAL 2)|K1,R^1;
assume
A1:(for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1
holds f.p=p`1/sqrt(1+(p`2/p`1)^2)) &
(for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`1<>0 );
A2: the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
reconsider g2=proj2|K1 as continuous map of (TOP-REAL 2)|K1,R^1 by Lm5;
reconsider g1=proj1|K1 as continuous map of (TOP-REAL 2)|K1,R^1 by Lm7;
now let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1;
then reconsider q2=q as Point of TOP-REAL 2 by A2;
g1.q=proj1.q by Lm6 .=q2`1 by PSCOMP_1:def 28;
hence g1.q<>0 by A1;
end;
then consider g3 being map of (TOP-REAL 2)|K1,R^1 such that
A3: (for q being Point of
(TOP-REAL 2)|K1,r1,r2 being real number st g2.q=r1 & g1.q=r2
holds g3.q=r2/sqrt(1+(r1/r2)^2)) & g3 is continuous by Th20;
dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then A4:dom f=dom g3 by FUNCT_2:def 1;
for x being set st x in dom f holds f.x=g3.x
proof let x be set;assume
A5:x in dom f;
then x in the carrier of (TOP-REAL 2)|K1;
then x in K1 by JORDAN1:1;
then reconsider r=x as Point of (TOP-REAL 2);
reconsider s=x as Point of (TOP-REAL 2)|K1 by A5;
A6:f.r=r`1/sqrt(1+(r`2/r`1)^2) by A1,A5;
A7:g2.s=proj2.s by Lm4;
A8:g1.s=proj1.s by Lm6;
A9:proj2.r=r`2 by PSCOMP_1:def 29;
proj1.r=r`1 by PSCOMP_1:def 28;
hence f.x=g3.x by A3,A6,A7,A8,A9;
end;
hence thesis by A3,A4,FUNCT_1:9;
end;
theorem Th22: for K1 being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K1,R^1 st
(for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f.p=p`2/sqrt(1+(p`2/p`1)^2)) &
(for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`1<>0 ) holds
f is continuous
proof let K1 be non empty Subset of TOP-REAL 2,
f be map of (TOP-REAL 2)|K1,R^1;
assume
A1:(for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f.p=p`2/sqrt(1+(p`2/p`1)^2)) &
(for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`1<>0 );
A2: the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
reconsider g2=proj2|K1 as continuous map of (TOP-REAL 2)|K1,R^1 by Lm5;
reconsider g1=proj1|K1 as continuous map of (TOP-REAL 2)|K1,R^1 by Lm7;
now let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1;
then reconsider q2=q as Point of TOP-REAL 2 by A2;
g1.q=proj1.q by Lm6 .=q2`1 by PSCOMP_1:def 28;
hence g1.q<>0 by A1;
end;
then consider g3 being map of (TOP-REAL 2)|K1,R^1 such that
A3: (for q being Point of
(TOP-REAL 2)|K1,r1,r2 being real number st g2.q=r1 & g1.q=r2
holds g3.q=r1/sqrt(1+(r1/r2)^2)) & g3 is continuous by Th19;
dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then A4:dom f=dom g3 by FUNCT_2:def 1;
for x being set st x in dom f holds f.x=g3.x
proof let x be set;assume
A5:x in dom f;
then x in the carrier of (TOP-REAL 2)|K1;
then x in K1 by JORDAN1:1;
then reconsider r=x as Point of (TOP-REAL 2);
reconsider s=x as Point of (TOP-REAL 2)|K1 by A5;
A6:f.r=r`2/sqrt(1+(r`2/r`1)^2) by A1,A5;
A7:g2.s=proj2.s by Lm4;
A8:g1.s=proj1.s by Lm6;
A9:proj2.r=r`2 by PSCOMP_1:def 29;
proj1.r=r`1 by PSCOMP_1:def 28;
hence f.x=g3.x by A3,A6,A7,A8,A9;
end;
hence f is continuous by A3,A4,FUNCT_1:9;
end;
theorem Th23: for K1 being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K1,R^1 st
(for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f.p=p`2/sqrt(1+(p`1/p`2)^2)) & (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`2<>0 ) holds
f is continuous
proof let K1 be non empty Subset of TOP-REAL 2,
f be map of (TOP-REAL 2)|K1,R^1;
assume
A1:(for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f.p=p`2/sqrt(1+(p`1/p`2)^2)) &
(for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`2<>0 );
A2: the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
reconsider g2=proj2|K1 as continuous map of (TOP-REAL 2)|K1,R^1 by Lm5;
reconsider g1=proj1|K1 as continuous map of (TOP-REAL 2)|K1,R^1 by Lm7;
now let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1;
then reconsider q2=q as Point of TOP-REAL 2 by A2;
g2.q=proj2.q by Lm4 .=q2`2 by PSCOMP_1:def 29;
hence g2.q<>0 by A1;
end;
then consider g3 being map of (TOP-REAL 2)|K1,R^1 such that
A3: (for q being Point of
(TOP-REAL 2)|K1,r1,r2 being real number st g1.q=r1 & g2.q=r2
holds g3.q=r2/sqrt(1+(r1/r2)^2)) & g3 is continuous by Th20;
dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then A4:dom f=dom g3 by FUNCT_2:def 1;
for x being set st x in dom f holds f.x=g3.x
proof let x be set;assume
A5:x in dom f;
then x in the carrier of (TOP-REAL 2)|K1;
then x in K1 by JORDAN1:1;
then reconsider r=x as Point of (TOP-REAL 2);
reconsider s=x as Point of (TOP-REAL 2)|K1 by A5;
A6:f.r=r`2/sqrt(1+(r`1/r`2)^2) by A1,A5;
A7:g2.s=proj2.s by Lm4;
A8:g1.s=proj1.s by Lm6;
A9:proj2.r=r`2 by PSCOMP_1:def 29;
proj1.r=r`1 by PSCOMP_1:def 28;
hence f.x=g3.x by A3,A6,A7,A8,A9;
end;
hence f is continuous by A3,A4,FUNCT_1:9;
end;
theorem Th24: for K1 being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K1,R^1 st
(for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f.p=p`1/sqrt(1+(p`1/p`2)^2)) &
(for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`2<>0 ) holds
f is continuous
proof let K1 be non empty Subset of TOP-REAL 2,
f be map of (TOP-REAL 2)|K1,R^1;
assume
A1:(for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f.p=p`1/sqrt(1+(p`1/p`2)^2)) &
(for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`2<>0 );
A2: the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
reconsider g2=proj2|K1 as continuous map of (TOP-REAL 2)|K1,R^1 by Lm5;
reconsider g1=proj1|K1 as continuous map of (TOP-REAL 2)|K1,R^1 by Lm7;
now let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1;
then reconsider q2=q as Point of TOP-REAL 2 by A2;
g2.q=proj2.q by Lm4 .=q2`2 by PSCOMP_1:def 29;
hence g2.q<>0 by A1;
end;
then consider g3 being map of (TOP-REAL 2)|K1,R^1 such that
A3: (for q being Point of
(TOP-REAL 2)|K1,r1,r2 being real number st g1.q=r1 & g2.q=r2
holds g3.q=r1/sqrt(1+(r1/r2)^2)) & g3 is continuous by Th19;
dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then A4:dom f=dom g3 by FUNCT_2:def 1;
for x being set st x in dom f holds f.x=g3.x
proof let x be set;assume
A5:x in dom f;
then x in the carrier of (TOP-REAL 2)|K1;
then x in K1 by JORDAN1:1;
then reconsider r=x as Point of (TOP-REAL 2);
reconsider s=x as Point of (TOP-REAL 2)|K1 by A5;
A6:f.r=r`1/sqrt(1+(r`1/r`2)^2) by A1,A5;
A7:g2.s=proj2.s by Lm4;
A8:g1.s=proj1.s by Lm6;
A9:proj2.r=r`2 by PSCOMP_1:def 29;
proj1.r=r`1 by PSCOMP_1:def 28;
hence f.x=g3.x by A3,A6,A7,A8,A9;
end;
hence f is continuous by A3,A4,FUNCT_1:9;
end;
Lm8: ((1.REAL 2)`2<=(1.REAL 2)`1 & -(1.REAL 2)`1<=(1.REAL 2)`2 or
(1.REAL 2)`2>=(1.REAL 2)`1 & (1.REAL 2)`2<=-(1.REAL 2)`1) &
(1.REAL 2)<>0.REAL 2 by JGRAPH_2:13,REVROT_1:19;
Lm9:for K1 being non empty Subset of TOP-REAL 2 holds
dom ((proj2)*(Sq_Circ|K1)) = the carrier of (TOP-REAL 2)|K1
proof
let K1 be non empty Subset of TOP-REAL 2;
A1:dom ((proj2)*(Sq_Circ|K1)) c= dom (Sq_Circ|K1) by RELAT_1:44;
dom (Sq_Circ|K1) c= dom ((proj2)*(Sq_Circ|K1))
proof let x be set;assume A2:x in dom (Sq_Circ|K1);
then A3:x in dom Sq_Circ /\ K1 by FUNCT_1:68;
A4:(Sq_Circ|K1).x=Sq_Circ.x by A2,FUNCT_1:68;
x in dom Sq_Circ by A3,XBOOLE_0:def 3;
then Sq_Circ.x in rng Sq_Circ by FUNCT_1:12;
hence x in dom ((proj2)*(Sq_Circ|K1)) by A2,A4,Lm3,FUNCT_1:21;
end;
hence dom ((proj2)*(Sq_Circ|K1)) = dom (Sq_Circ|K1) by A1,XBOOLE_0:def 10
.=dom Sq_Circ /\ K1 by FUNCT_1:68
.=(the carrier of TOP-REAL 2)/\ K1 by FUNCT_2:def 1
.=K1 by XBOOLE_1:28
.=the carrier of (TOP-REAL 2)|K1 by JORDAN1:1;
end;
Lm10:for K1 being non empty Subset of TOP-REAL 2 holds
dom ((proj1)*(Sq_Circ|K1)) = the carrier of (TOP-REAL 2)|K1
proof
let K1 be non empty Subset of TOP-REAL 2;
A1:dom ((proj1)*(Sq_Circ|K1)) c= dom (Sq_Circ|K1) by RELAT_1:44;
dom (Sq_Circ|K1) c= dom ((proj1)*(Sq_Circ|K1))
proof let x be set;assume A2:x in dom (Sq_Circ|K1);
then A3:x in dom Sq_Circ /\ K1 by FUNCT_1:68;
A4:(Sq_Circ|K1).x=Sq_Circ.x by A2,FUNCT_1:68;
x in dom Sq_Circ by A3,XBOOLE_0:def 3;
then Sq_Circ.x in rng Sq_Circ by FUNCT_1:12;
hence x in dom ((proj1)*(Sq_Circ|K1)) by A2,A4,Lm3,FUNCT_1:21;
end;
hence dom ((proj1)*(Sq_Circ|K1))
=dom (Sq_Circ|K1) by A1,XBOOLE_0:def 10
.=dom Sq_Circ /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2))/\ K1 by FUNCT_2:def 1
.=K1 by XBOOLE_1:28
.=the carrier of (TOP-REAL 2)|K1 by JORDAN1:1;
end;
Lm11:(the carrier of TOP-REAL 2) \ {0.REAL 2} <> {} by JGRAPH_2:19;
theorem Th25: for K0,B0 being Subset of TOP-REAL 2,f being
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0
st f=Sq_Circ|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} &
K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2}
holds f is continuous
proof let K0,B0 be Subset of TOP-REAL 2,f be
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0;
assume A1:f=Sq_Circ|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} &
K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2};
then 1.REAL 2 in K0 by Lm8;
then reconsider K1=K0 as non empty Subset of TOP-REAL 2;
A2:rng ((proj2)*(Sq_Circ|K1)) c= rng (proj2) by RELAT_1:45;
A3:dom ((proj2)*(Sq_Circ|K1)) = the carrier of (TOP-REAL 2)|K1 by Lm9;
rng proj2 c= the carrier of R^1 by JGRAPH_2:17,RELSET_1:12;
then rng ((proj2)*(Sq_Circ|K1)) c= the carrier of R^1 by A2,XBOOLE_1:1;
then (proj2)*(Sq_Circ|K1) is Function of the carrier of (TOP-REAL 2)|K1,
the carrier of R^1 by A3,FUNCT_2:4;
then reconsider g2=(proj2)*(Sq_Circ|K1) as map of (TOP-REAL 2)|K1,R^1
;
A4:dom ((proj1)*(Sq_Circ|K1)) = the carrier of (TOP-REAL 2)|K1 by Lm10;
A5:rng ((proj1)*(Sq_Circ|K1)) c= rng (proj1) by RELAT_1:45;
rng proj1 c= the carrier of R^1 by JGRAPH_2:16,RELSET_1:12;
then rng ((proj1)*(Sq_Circ|K1)) c= the carrier of R^1 by A5,XBOOLE_1:1;
then (proj1)*(Sq_Circ|K1) is Function of the carrier of (TOP-REAL 2)|K1,
the carrier of R^1 by A4,FUNCT_2:4;
then reconsider g1=(proj1)*(Sq_Circ|K1) as map of (TOP-REAL 2)|K1,R^1
;
A6: now let q be Point of TOP-REAL 2;
assume A7:q in the carrier of (TOP-REAL 2)|K1;
the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
then consider p3 being Point of TOP-REAL 2 such that
A8: q=p3 & ((p3`2<=p3`1 & -p3`1<=p3`2 or p3`2>=p3`1 & p3`2<=-p3`1)
& p3<>0.REAL 2) by A1,A7;
now assume A9:q`1=0;
then q`2=0 by A8;
hence contradiction by A8,A9,EUCLID:57,58;
end;
hence q`1<>0;
end;
for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds g2.p=p`2/sqrt(1+(p`2/p`1)^2)
proof let p be Point of TOP-REAL 2;
assume A10: p in the carrier of (TOP-REAL 2)|K1;
A11:dom (Sq_Circ|K1)=dom Sq_Circ /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2))/\ K1 by FUNCT_2:def 1
.=K1 by XBOOLE_1:28;
A12:the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
then consider p3 being Point of TOP-REAL 2 such that
A13: p=p3 & ((p3`2<=p3`1 & -p3`1<=p3`2 or p3`2>=p3`1 & p3`2<=-p3`1)
& p3<>0.REAL 2) by A1,A10;
A14:Sq_Circ.p
=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]| by A13,Def1;
(Sq_Circ|K1).p=Sq_Circ.p by A10,A12,FUNCT_1:72;
then g2.p=(proj2).(|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|)
by A10,A11,A12,A14,FUNCT_1:23
.=(|[p`1/sqrt(1+(p`2/p`1)^2),
p`2/sqrt(1+(p`2/p`1)^2)]|)`2 by PSCOMP_1:def 29
.=p`2/sqrt(1+(p`2/p`1)^2) by EUCLID:56;
hence g2.p=p`2/sqrt(1+(p`2/p`1)^2);
end;
then consider f2 being map of (TOP-REAL 2)|K1,R^1 such that
A15:for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f2.p=p`2/sqrt(1+(p`2/p`1)^2);
A16:f2 is continuous by A6,A15,Th22;
for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds g1.p=p`1/sqrt(1+(p`2/p`1)^2)
proof let p be Point of TOP-REAL 2;
assume A17: p in the carrier of (TOP-REAL 2)|K1;
A18:dom (Sq_Circ|K1)=dom Sq_Circ /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2))/\ K1 by FUNCT_2:def 1
.=K1 by XBOOLE_1:28;
A19:the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
then consider p3 being Point of TOP-REAL 2 such that
A20: p=p3 & ((p3`2<=p3`1 & -p3`1<=p3`2 or p3`2>=p3`1 & p3`2<=-p3`1)
& p3<>0.REAL 2) by A1,A17;
A21:Sq_Circ.p=|[p`1/sqrt(1+(p`2/p`1)^2),
p`2/sqrt(1+(p`2/p`1)^2)]| by A20,Def1;
(Sq_Circ|K1).p=Sq_Circ.p by A17,A19,FUNCT_1:72;
then g1.p=(proj1).(|[p`1/sqrt(1+(p`2/p`1)^2),
p`2/sqrt(1+(p`2/p`1)^2)]|) by A17,A18,A19,A21,FUNCT_1:23
.=(|[p`1/sqrt(1+(p`2/p`1)^2),
p`2/sqrt(1+(p`2/p`1)^2)]|)`1 by PSCOMP_1:def 28
.=p`1/sqrt(1+(p`2/p`1)^2) by EUCLID:56;
hence g1.p=p`1/sqrt(1+(p`2/p`1)^2);
end;
then consider f1 being map of (TOP-REAL 2)|K1,R^1 such that
A22:for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f1.p=p`1/sqrt(1+(p`2/p`1)^2);
A23:f1 is continuous by A6,A22,Th21;
for x,y,r,s being real number st |[x,y]| in K1 &
r=f1.(|[x,y]|) & s=f2.(|[x,y]|) holds f.(|[x,y]|)=|[r,s]|
proof let x,y,r,s be real number;
assume A24: |[x,y]| in K1 & r=f1.(|[x,y]|) & s=f2.(|[x,y]|);
set p99=|[x,y]|;
A25:the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
consider p3 being Point of TOP-REAL 2 such that
A26: p99=p3 & ((p3`2<=p3`1 & -p3`1<=p3`2 or p3`2>=p3`1 & p3`2<=-p3`1)
& p3<>0.REAL 2) by A1,A24;
A27:f1.p99=p99`1/sqrt(1+(p99`2/p99`1)^2) by A22,A24,A25;
(Sq_Circ|K0).(|[x,y]|)=(Sq_Circ).(|[x,y]|) by A24,FUNCT_1:72
.= |[p99`1/sqrt(1+(p99`2/p99`1)^2),
p99`2/sqrt(1+(p99`2/p99`1)^2)]| by A26,Def1
.=|[r,s]| by A15,A24,A25,A27;
hence f.(|[x,y]|)=|[r,s]| by A1;
end;
hence thesis by A1,A16,A23,Lm11,JGRAPH_2:45;
end;
Lm12: ((1.REAL 2)`1<=(1.REAL 2)`2 & -(1.REAL 2)`2<=(1.REAL 2)`1 or
(1.REAL 2)`1>=(1.REAL 2)`2 & (1.REAL 2)`1<=-(1.REAL 2)`2) &
(1.REAL 2)<>0.REAL 2 by JGRAPH_2:13,REVROT_1:19;
theorem Th26: for K0,B0 being Subset of TOP-REAL 2,f being
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0
st f=Sq_Circ|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} &
K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.REAL 2}
holds f is continuous
proof let K0,B0 be Subset of TOP-REAL 2,f be
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0;
assume A1:f=Sq_Circ|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} &
K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.REAL 2};
then 1.REAL 2 in K0 by Lm12;
then reconsider K1=K0 as non empty Subset of TOP-REAL 2;
A2:dom ((proj1)*(Sq_Circ|K1))=the carrier of (TOP-REAL 2)|K1 by Lm10;
A3:rng ((proj1)*(Sq_Circ|K1)) c= rng (proj1) by RELAT_1:45;
rng proj1 c= the carrier of R^1 by JGRAPH_2:16,RELSET_1:12;
then rng ((proj1)*(Sq_Circ|K1)) c= the carrier of R^1 by A3,XBOOLE_1:1;
then (proj1)*(Sq_Circ|K1) is Function of the carrier of (TOP-REAL 2)|K1,
the carrier of R^1 by A2,FUNCT_2:4;
then reconsider g2=(proj1)*(Sq_Circ|K1) as map of (TOP-REAL 2)|K1,R^1
;
A4:dom ((proj2)*(Sq_Circ|K1))=the carrier of (TOP-REAL 2)|K1 by Lm9;
A5:rng ((proj2)*(Sq_Circ|K1)) c= rng (proj2) by RELAT_1:45;
rng proj2 c= the carrier of R^1 by JGRAPH_2:17,RELSET_1:12;
then rng ((proj2)*(Sq_Circ|K1)) c= the carrier of R^1 by A5,XBOOLE_1:1;
then (proj2)*(Sq_Circ|K1) is Function of the carrier of (TOP-REAL 2)|K1,
the carrier of R^1 by A4,FUNCT_2:4;
then reconsider g1=(proj2)*(Sq_Circ|K1) as map of (TOP-REAL 2)|K1,R^1
;
A6: for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`2<>0
proof let q be Point of TOP-REAL 2;
assume A7:q in the carrier of (TOP-REAL 2)|K1;
the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
then consider p3 being Point of TOP-REAL 2 such that
A8: q=p3 & ((p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 & p3`1<=-p3`2)
& p3<>0.REAL 2) by A1,A7;
now assume A9:q`2=0;
then q`1=0 by A8;
hence contradiction by A8,A9,EUCLID:57,58;
end;
hence q`2<>0;
end;
for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds g2.p=p`1/sqrt(1+(p`1/p`2)^2)
proof let p be Point of TOP-REAL 2;
assume A10: p in the carrier of (TOP-REAL 2)|K1;
A11:dom (Sq_Circ|K1)=dom Sq_Circ /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2))/\ K1 by FUNCT_2:def 1
.=K1 by XBOOLE_1:28;
A12:the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
then consider p3 being Point of TOP-REAL 2 such that
A13: p=p3 & ((p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 & p3`1<=-p3`2)
& p3<>0.REAL 2) by A1,A10;
A14:Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),
p`2/sqrt(1+(p`1/p`2)^2)]| by A13,Th14;
(Sq_Circ|K1).p=Sq_Circ.p by A10,A12,FUNCT_1:72;
then g2.p=(proj1).(|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|)
by A10,A11,A12,A14,FUNCT_1:23
.=(|[p`1/sqrt(1+(p`1/p`2)^2),
p`2/sqrt(1+(p`1/p`2)^2)]|)`1 by PSCOMP_1:def 28
.=p`1/sqrt(1+(p`1/p`2)^2) by EUCLID:56;
hence g2.p=p`1/sqrt(1+(p`1/p`2)^2);
end;
then consider f2 being map of (TOP-REAL 2)|K1,R^1 such that
A15:for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f2.p=p`1/sqrt(1+(p`1/p`2)^2);
A16:f2 is continuous by A6,A15,Th24;
for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds g1.p=p`2/sqrt(1+(p`1/p`2)^2)
proof let p be Point of TOP-REAL 2;
assume A17: p in the carrier of (TOP-REAL 2)|K1;
A18:dom (Sq_Circ|K1)=dom Sq_Circ /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2))/\ K1 by FUNCT_2:def 1
.=K1 by XBOOLE_1:28;
A19:the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
then consider p3 being Point of TOP-REAL 2 such that
A20: p=p3 & ((p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 & p3`1<=-p3`2)
& p3<>0.REAL 2) by A1,A17;
A21:Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),
p`2/sqrt(1+(p`1/p`2)^2)]| by A20,Th14;
(Sq_Circ|K1).p=Sq_Circ.p by A17,A19,FUNCT_1:72;
then g1.p=(proj2).(|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|)
by A17,A18,A19,A21,FUNCT_1:23
.=(|[p`1/sqrt(1+(p`1/p`2)^2),
p`2/sqrt(1+(p`1/p`2)^2)]|)`2 by PSCOMP_1:def 29
.=p`2/sqrt(1+(p`1/p`2)^2) by EUCLID:56;
hence g1.p=p`2/sqrt(1+(p`1/p`2)^2);
end;
then consider f1 being map of (TOP-REAL 2)|K1,R^1 such that
A22:for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f1.p=p`2/sqrt(1+(p`1/p`2)^2);
A23:f1 is continuous by A6,A22,Th23;
now let x,y,s,r be real number;
assume A24: |[x,y]| in K1 & s=f2.(|[x,y]|) & r=f1.(|[x,y]|);
set p99=|[x,y]|;
A25:the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
consider p3 being Point of TOP-REAL 2 such that
A26: p99=p3 & ((p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 & p3`1<=-p3`2)
& p3<>0.REAL 2) by A1,A24;
A27:f1.p99=p99`2/sqrt(1+(p99`1/p99`2)^2) by A22,A24,A25;
(Sq_Circ|K0).(|[x,y]|)=(Sq_Circ).(|[x,y]|) by A24,FUNCT_1:72
.= |[p99`1/sqrt(1+(p99`1/p99`2)^2),
p99`2/sqrt(1+(p99`1/p99`2)^2)]| by A26,Th14
.=|[s,r]| by A15,A24,A25,A27;
hence f.(|[x,y]|)=|[s,r]| by A1;
end;
hence thesis by A1,A16,A23,Lm11,JGRAPH_2:45;
end;
scheme TopIncl { P[set] } :
{ p: P[p] & p<>0.REAL 2 } c= (the carrier of TOP-REAL 2) \ {0.REAL 2}
proof
let x be set;assume x in { p: P[p] & p<>0.REAL 2 };
then consider p8 being Point of TOP-REAL 2 such that
A1: x=p8 & P[p8] & p8<>0.REAL 2;
not x in {0.REAL 2} by A1,TARSKI:def 1;
hence thesis by A1,XBOOLE_0:def 4;
end;
scheme TopInter { P[set] } :
{ p: P[p] & p<>0.REAL 2 } =
{ p7 where p7 is Point of TOP-REAL 2 : P[p7]} /\
((the carrier of TOP-REAL 2) \ {0.REAL 2})
proof
set K0 = { p: P[p] & p<>0.REAL 2 };
set K1 = { p7 where p7 is Point of TOP-REAL 2 : P[p7]};
set B0 = (the carrier of TOP-REAL 2) \ {0.REAL 2};
A1:K1 /\ B0 c= K0
proof let x be set;assume x in K1 /\ B0;
then A2:x in K1 & x in B0 by XBOOLE_0:def 3;
then consider p7 being Point of TOP-REAL 2 such that
A3: p7=x & P[p7];
x in the carrier of TOP-REAL 2 & not x in {0.REAL 2}
by A2,XBOOLE_0:def 4;
then x <> 0.REAL 2 by TARSKI:def 1;
hence x in K0 by A3;
end;
K0 c= K1 /\ B0
proof let x be set;assume x in K0;
then consider p being Point of TOP-REAL 2 such that
A4: x=p & P[p] & p<>0.REAL 2;
x in the carrier of TOP-REAL 2 & not x in {0.REAL 2}
by A4,TARSKI:def 1;
then x in K1 & x in B0 by A4,XBOOLE_0:def 4;
hence x in K1 /\ B0 by XBOOLE_0:def 3;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th27: for B0 being Subset of TOP-REAL 2,K0 being Subset of
(TOP-REAL 2)|B0,f being map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0)
st f=Sq_Circ|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2}
holds f is continuous & K0 is closed
proof let B0 be Subset of TOP-REAL 2,K0 be Subset of
(TOP-REAL 2)|B0,f being map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0);
assume A1: f=Sq_Circ|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2};
the carrier of (TOP-REAL 2)|B0 = B0 by JORDAN1:1;
then K0 c= the carrier of TOP-REAL 2 by XBOOLE_1:1;
then reconsider K1=K0 as Subset of TOP-REAL 2;
defpred P[Point of TOP-REAL 2] means
($1`2<=$1`1 & -$1`1<=$1`2 or $1`2>=$1`1 & $1`2<=-$1`1);
{p:P[p] & p<>0.REAL 2} c=
(the carrier of TOP-REAL 2) \ {0.REAL 2} from TopIncl;
then A2: ((TOP-REAL 2)|B0)|K0=(TOP-REAL 2)|K1 by A1,JORDAN6:47;
defpred P[Point of TOP-REAL 2] means
($1`2<=$1`1 & -$1`1<=$1`2 or $1`2>=$1`1 & $1`2<=-$1`1);
reconsider K1={p7 where p7 is Point of TOP-REAL 2: P[p7]}
as Subset of TOP-REAL 2 from TopSubset;
reconsider K2={p7 where p7 is Point of TOP-REAL 2: p7`2<=p7`1 }
as closed Subset of TOP-REAL 2 by JGRAPH_2:56;
reconsider K3={p7 where p7 is Point of TOP-REAL 2: -p7`1<=p7`2 }
as closed Subset of TOP-REAL 2 by JGRAPH_2:57;
reconsider K4={p7 where p7 is Point of TOP-REAL 2: p7`1<=p7`2 }
as closed Subset of TOP-REAL 2 by JGRAPH_2:56;
reconsider K5={p7 where p7 is Point of TOP-REAL 2:p7`2<=-p7`1 }
as closed Subset of TOP-REAL 2 by JGRAPH_2:57;
A3:K2 /\ K3 is closed by TOPS_1:35;
A4:K4 /\ K5 is closed by TOPS_1:35;
A5:K2 /\ K3 \/ K4 /\ K5 c= K1
proof let x be set;assume
A6:x in K2 /\ K3 \/ K4 /\ K5;
per cases by A6,XBOOLE_0:def 2;
suppose x in K2 /\ K3;
then A7:x in K2 & x in K3 by XBOOLE_0:def 3;
then consider p7 being Point of TOP-REAL 2 such that
A8: p7=x & p7`2<=(p7`1);
consider p8 being Point of TOP-REAL 2 such that
A9: p8=x & -p8`1<=p8`2 by A7;
thus x in K1 by A8,A9;
suppose x in K4 /\ K5;
then A10:x in K4 & x in K5 by XBOOLE_0:def 3;
then consider p7 being Point of TOP-REAL 2 such that
A11: p7=x & p7`2>=(p7`1);
consider p8 being Point of TOP-REAL 2 such that
A12: p8=x & p8`2<= -p8`1 by A10;
thus x in K1 by A11,A12;
end;
K1 c= K2 /\ K3 \/ K4 /\ K5
proof let x be set;assume x in K1;
then consider p being Point of TOP-REAL 2 such that
A13: p=x & (p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1);
x in K2 & x in K3 or x in K4 & x in K5 by A13;
then x in K2 /\ K3 or x in K4 /\ K5 by XBOOLE_0:def 3;
hence x in K2 /\ K3 \/ K4 /\ K5 by XBOOLE_0:def 2;
end;
then K1=K2 /\ K3 \/ K4 /\ K5 by A5,XBOOLE_0:def 10;
then A14:K1 is closed by A3,A4,TOPS_1:36;
defpred P[Point of TOP-REAL 2] means
($1`2<=$1`1 & -$1`1<=$1`2 or $1`2>=$1`1 & $1`2<=-$1`1);
{p: P[p] & p<>0.REAL 2} =
{p7 where p7 is Point of TOP-REAL 2: P[p7]}
/\ ((the carrier of TOP-REAL 2) \ {0.REAL 2}) from TopInter;
then K0=K1 /\ [#]((TOP-REAL 2)|B0) by A1,PRE_TOPC:def 10;
hence thesis by A1,A2,A14,Th25,PRE_TOPC:43;
end;
theorem Th28: for B0 being Subset of TOP-REAL 2,K0 being Subset of
(TOP-REAL 2)|B0,f being map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0)
st f=Sq_Circ|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.REAL 2}
holds f is continuous & K0 is closed
proof let B0 be Subset of TOP-REAL 2,K0 be Subset of
(TOP-REAL 2)|B0,f being map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0);
assume A1: f=Sq_Circ|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.REAL 2};
defpred P0[Point of TOP-REAL 2] means
($1`1<=$1`2 & -$1`2<=$1`1 or $1`1>=$1`2 & $1`1<=-$1`2);
set k0 = {p:P0[p] & p<>0.REAL 2};
set b0 = (the carrier of TOP-REAL 2) \ {0.REAL 2};
the carrier of (TOP-REAL 2)|B0= B0 by JORDAN1:1;
then K0 c= the carrier of TOP-REAL 2 by XBOOLE_1:1;
then reconsider K1=K0 as Subset of TOP-REAL 2;
defpred P[Point of TOP-REAL 2] means
($1`1<=$1`2 & -$1`2<=$1`1 or $1`1>=$1`2 & $1`1<=-$1`2);
{p:P[p] & p<>0.REAL 2} c=
(the carrier of TOP-REAL 2) \ {0.REAL 2} from TopIncl;
then A2: ((TOP-REAL 2)|B0)|K0=(TOP-REAL 2)|K1 by A1,JORDAN6:47;
defpred P[Point of TOP-REAL 2] means
($1`1<=$1`2 & -$1`2<=$1`1 or $1`1>=$1`2 & $1`1<=-$1`2);
reconsider K1={p7 where p7 is Point of TOP-REAL 2:P[p7]}
as Subset of TOP-REAL 2 from TopSubset;
reconsider K2={p7 where p7 is Point of TOP-REAL 2: p7`1<=p7`2 }
as closed Subset of TOP-REAL 2 by JGRAPH_2:56;
reconsider K3={p7 where p7 is Point of TOP-REAL 2: -p7`2<=p7`1 }
as closed Subset of TOP-REAL 2 by JGRAPH_2:58;
reconsider K4={p7 where p7 is Point of TOP-REAL 2: p7`2<=p7`1 }
as closed Subset of TOP-REAL 2 by JGRAPH_2:56;
reconsider K5={p7 where p7 is Point of TOP-REAL 2: p7`1<=-p7`2 }
as closed Subset of TOP-REAL 2 by JGRAPH_2:58;
A3:K2 /\ K3 is closed by TOPS_1:35;
A4:K4 /\ K5 is closed by TOPS_1:35;
A5:K2 /\ K3 \/ K4 /\ K5 c= K1
proof let x be set;assume
A6:x in K2 /\ K3 \/ K4 /\ K5;
per cases by A6,XBOOLE_0:def 2;
suppose x in K2 /\ K3;
then A7:x in K2 & x in K3 by XBOOLE_0:def 3;
then consider p7 being Point of TOP-REAL 2 such that
A8: p7=x & p7`1<=(p7`2);
consider p8 being Point of TOP-REAL 2 such that
A9: p8=x & -p8`2<=p8`1 by A7;
thus x in K1 by A8,A9;
suppose x in K4 /\ K5;
then A10:x in K4 & x in K5 by XBOOLE_0:def 3;
then consider p7 being Point of TOP-REAL 2 such that
A11: p7=x & p7`1>=(p7`2);
consider p8 being Point of TOP-REAL 2 such that
A12: p8=x & p8`1<= -p8`2 by A10;
thus x in K1 by A11,A12;
end;
K1 c= K2 /\ K3 \/ K4 /\ K5
proof let x be set;assume x in K1;
then consider p being Point of TOP-REAL 2 such that
A13: p=x &
(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2);
x in K2 & x in K3 or x in K4 & x in K5 by A13;
then x in K2 /\ K3 or x in K4 /\ K5 by XBOOLE_0:def 3;
hence x in K2 /\ K3 \/ K4 /\ K5 by XBOOLE_0:def 2;
end;
then K1=K2 /\ K3 \/ K4 /\ K5 by A5,XBOOLE_0:def 10;
then A14:K1 is closed by A3,A4,TOPS_1:36;
k0 = {p7 where p7 is Point of TOP-REAL 2:P0[p7]} /\ b0
from TopInter;
then K0=K1 /\ [#]((TOP-REAL 2)|B0) by A1,PRE_TOPC:def 10;
hence thesis by A1,A2,A14,Th26,PRE_TOPC:43;
end;
theorem Th29:for D being non empty Subset of TOP-REAL 2
st D`={0.REAL 2} holds
ex h being map of (TOP-REAL 2)|D,(TOP-REAL 2)|D
st h=Sq_Circ|D & h is continuous
proof let D be non empty Subset of TOP-REAL 2;
assume A1:D`={0.REAL 2};
then A2: D = {0.REAL 2}`
.=((the carrier of TOP-REAL 2)\ {0.REAL 2}) by SUBSET_1:def 5;
A3:{p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)
& p<>0.REAL 2} c= the carrier of (TOP-REAL 2)|D
proof let x be set;
assume x in {p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)
& p<>0.REAL 2};
then consider p such that A4: x=p &
(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2;
now assume not x in D;
then x in (the carrier of TOP-REAL 2) \ D by A4,XBOOLE_0:def 4;
then x in D` by SUBSET_1:def 5;
hence contradiction by A1,A4,TARSKI:def 1;
end;
hence x in the carrier of (TOP-REAL 2)|D by JORDAN1:1;
end;
1.REAL 2 in {p where p is Point of TOP-REAL 2:
(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)
& p<>0.REAL 2} by Lm8;
then reconsider K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)
& p<>0.REAL 2} as non empty Subset of (TOP-REAL 2)|D by A3;
A5:{p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2)
& p<>0.REAL 2} c= the carrier of (TOP-REAL 2)|D
proof let x be set;
assume x in {p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2)
& p<>0.REAL 2};
then consider p such that A6: x=p &
(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2)& p<>0.REAL 2;
now assume not x in D;
then x in (the carrier of TOP-REAL 2) \ D by A6,XBOOLE_0:def 4;
then x in D` by SUBSET_1:def 5;
hence contradiction by A1,A6,TARSKI:def 1;
end;
hence x in the carrier of (TOP-REAL 2)|D by JORDAN1:1;
end;
set Y1=|[-1,1]|;
Y1`1=-1 & Y1`2=1 by EUCLID:56;
then Y1 in {p where p is Point of TOP-REAL 2:
(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2)
& p<>0.REAL 2} by JGRAPH_2:11;
then reconsider K1={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2)
& p<>0.REAL 2} as non empty Subset of (TOP-REAL 2)|D by A5;
A7:the carrier of ((TOP-REAL 2)|D) =D by JORDAN1:1;
A8:K0 c= the carrier of TOP-REAL 2
proof let z be set;assume z in K0;
then consider p8 being Point of TOP-REAL 2 such that
A9: p8=z &((p8`2<=p8`1 & -p8`1<=p8`2 or p8`2>=p8`1 & p8`2<=-p8`1)
& p8<>0.REAL 2);
thus z in the carrier of TOP-REAL 2 by A9;
end;
A10:dom (Sq_Circ|K0)= dom (Sq_Circ) /\ K0 by FUNCT_1:68
.=((the carrier of TOP-REAL 2)) /\ K0 by FUNCT_2:def 1
.=K0 by A8,XBOOLE_1:28;
A11: K0=the carrier of ((TOP-REAL 2)|D)|K0 by JORDAN1:1;
rng (Sq_Circ|K0) c= the carrier of ((TOP-REAL 2)|D)|K0
proof let y be set;assume y in rng (Sq_Circ|K0);
then consider x being set such that
A12:x in dom (Sq_Circ|K0) & y=(Sq_Circ|K0).x by FUNCT_1:def 5;
A13:x in (dom Sq_Circ) /\ K0 by A12,FUNCT_1:68;
then A14:x in K0 by XBOOLE_0:def 3;
A15: K0 c= the carrier of TOP-REAL 2 by A7,XBOOLE_1:1;
then reconsider p=x as Point of TOP-REAL 2 by A14;
A16:Sq_Circ.p=y by A12,A14,FUNCT_1:72;
consider px being Point of TOP-REAL 2 such that A17: x=px &
(px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1)
& px<>0.REAL 2 by A14;
reconsider K00=K0 as Subset of TOP-REAL 2 by A15;
K00=the carrier of ((TOP-REAL 2)|K00) by JORDAN1:1;
then A18:p in the carrier of ((TOP-REAL 2)|K00) by A13,XBOOLE_0:def 3;
for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K00 holds q`1<>0
proof let q be Point of TOP-REAL 2;
assume A19:q in the carrier of (TOP-REAL 2)|K00;
the carrier of (TOP-REAL 2)|K00=K0 by JORDAN1:1;
then consider p3 being Point of TOP-REAL 2 such that
A20: q=p3 & ((p3`2<=p3`1 & -p3`1<=p3`2 or p3`2>=p3`1 & p3`2<=-p3`1)
& p3<>0.REAL 2) by A19;
now assume A21:q`1=0;
then q`2=0 by A20;
hence contradiction by A20,A21,EUCLID:57,58;
end;
hence q`1<>0;
end;
then A22:p`1<>0 by A18;
set p9=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|;
A23:p9`1=p`1/sqrt(1+(p`2/p`1)^2) & p9`2=p`2/sqrt(1+(p`2/p`1)^2)
by EUCLID:56;
1+(p`2/p`1)^2>0 by Lm1;
then A24:sqrt(1+(p`2/p`1)^2)>0 by SQUARE_1:93;
A25:now assume p9=0.REAL 2;
then 0 *sqrt(1+(p`2/p`1)^2)=p`1/sqrt(1+(p`2/p`1)^2)*sqrt(1+(p`2/p`1)^2)
by A23,EUCLID:56,58;
hence contradiction by A22,A24,XCMPLX_1:88;
end;
A26:Sq_Circ.p=|[p`1/sqrt(1+(p`2/p`1)^2),
p`2/sqrt(1+(p`2/p`1)^2)]| by A17,Def1;
p`2/sqrt(1+(p`2/p`1)^2)<=p`1/sqrt(1+(p`2/p`1)^2)
& (-p`1)/sqrt(1+(p`2/p`1)^2)<=p`2/sqrt(1+(p`2/p`1)^2) or
p`2/sqrt(1+(p`2/p`1)^2)>=p`1/sqrt(1+(p`2/p`1)^2) &
p`2/sqrt(1+(p`2/p`1)^2)<=(-p`1)/sqrt(1+(p`2/p`1)^2)
by A17,A24,REAL_1:73;
then A27:p`2/sqrt(1+(p`2/p`1)^2)<=p`1/sqrt(1+(p`2/p`1)^2)
& -(p`1/sqrt(1+(p`2/p`1)^2))<=p`2/sqrt(1+(p`2/p`1)^2) or
p`2/sqrt(1+(p`2/p`1)^2)>=p`1/sqrt(1+(p`2/p`1)^2) &
p`2/sqrt(1+(p`2/p`1)^2)<=-(p`1/sqrt(1+(p`2/p`1)^2)) by XCMPLX_1:188;
p9`1=p`1/sqrt(1+(p`2/p`1)^2) & p9`2=p`2/sqrt(1+(p`2/p`1)^2) by EUCLID:56
;
then y in K0 by A16,A25,A26,A27;
then y in [#](((TOP-REAL 2)|D)|K0) by PRE_TOPC:def 10;
hence y in the carrier of ((TOP-REAL 2)|D)|K0;
end;
then rng (Sq_Circ|K0)c= the carrier of ((TOP-REAL 2)|D) by A11,XBOOLE_1:1;
then Sq_Circ|K0 is Function of the carrier of ((TOP-REAL 2)|D)|K0,
the carrier of ((TOP-REAL 2)|D) by A10,A11,FUNCT_2:4;
then reconsider f=Sq_Circ|K0 as map of ((TOP-REAL 2)|D)|K0,
(TOP-REAL 2)|D ;
A28:K1 c= the carrier of TOP-REAL 2
proof let z be set;assume z in K1;
then consider p8 being Point of TOP-REAL 2 such that
A29: p8=z &((p8`1<=p8`2 & -p8`2<=p8`1 or p8`1>=p8`2 & p8`1<=-p8`2)
& p8<>0.REAL 2);
thus z in the carrier of TOP-REAL 2 by A29;
end;
A30:dom (Sq_Circ|K1)= dom (Sq_Circ) /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2)) /\ K1 by FUNCT_2:def 1
.=K1 by A28,XBOOLE_1:28;
A31: K1=the carrier of ((TOP-REAL 2)|D)|K1 by JORDAN1:1;
rng (Sq_Circ|K1) c= the carrier of ((TOP-REAL 2)|D)|K1
proof let y be set;assume y in rng (Sq_Circ|K1);
then consider x being set such that
A32:x in dom (Sq_Circ|K1) & y=(Sq_Circ|K1).x by FUNCT_1:def 5;
A33:x in (dom Sq_Circ) /\ K1 by A32,FUNCT_1:68;
then A34:x in K1 by XBOOLE_0:def 3;
then reconsider p=x as Point of TOP-REAL 2 by A28;
A35:Sq_Circ.p=y by A32,A34,FUNCT_1:72;
consider px being Point of TOP-REAL 2 such that A36: x=px &
(px`1<=px`2 & -px`2<=px`1 or px`1>=px`2 & px`1<=-px`2)
& px<>0.REAL 2 by A34;
reconsider K10=K1 as Subset of TOP-REAL 2 by A28;
K10=the carrier of ((TOP-REAL 2)|K10) by JORDAN1:1;
then A37:p in the carrier of ((TOP-REAL 2)|K10) by A33,XBOOLE_0:def 3;
for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K10 holds q`2<>0
proof let q be Point of TOP-REAL 2;
assume A38:q in the carrier of (TOP-REAL 2)|K10;
the carrier of (TOP-REAL 2)|K10=K1 by JORDAN1:1;
then consider p3 being Point of TOP-REAL 2 such that
A39: q=p3 & ((p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 & p3`1<=-p3`2)
& p3<>0.REAL 2) by A38;
now assume A40:q`2=0;
then q`1=0 by A39;
hence contradiction by A39,A40,EUCLID:57,58;
end;
hence q`2<>0;
end;
then A41:p`2<>0 by A37;
set p9=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|;
A42:p9`1=p`1/sqrt(1+(p`1/p`2)^2) & p9`2=p`2/sqrt(1+(p`1/p`2)^2)
by EUCLID:56;
1+(p`1/p`2)^2>0 by Lm1;
then A43:sqrt(1+(p`1/p`2)^2)>0 by SQUARE_1:93;
A44:now assume p9=0.REAL 2;
then 0 *sqrt(1+(p`1/p`2)^2)=p`2/sqrt(1+(p`1/p`2)^2)*sqrt(1+(p`1/p`2)^2)
by A42,EUCLID:56,58;
hence contradiction by A41,A43,XCMPLX_1:88;
end;
A45:Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),
p`2/sqrt(1+(p`1/p`2)^2)]| by A36,Th14;
p`1/sqrt(1+(p`1/p`2)^2)<=p`2/sqrt(1+(p`1/p`2)^2)
& (-p`2)/sqrt(1+(p`1/p`2)^2)<=p`1/sqrt(1+(p`1/p`2)^2) or
p`1/sqrt(1+(p`1/p`2)^2)>=p`2/sqrt(1+(p`1/p`2)^2) &
p`1/sqrt(1+(p`1/p`2)^2)<=(-p`2)/sqrt(1+(p`1/p`2)^2)
by A36,A43,REAL_1:73;
then A46:p`1/sqrt(1+(p`1/p`2)^2)<=p`2/sqrt(1+(p`1/p`2)^2)
& -(p`2/sqrt(1+(p`1/p`2)^2))<=p`1/sqrt(1+(p`1/p`2)^2) or
p`1/sqrt(1+(p`1/p`2)^2)>=p`2/sqrt(1+(p`1/p`2)^2) &
p`1/sqrt(1+(p`1/p`2)^2)<=-(p`2/sqrt(1+(p`1/p`2)^2))
by XCMPLX_1:188;
p9`2=p`2/sqrt(1+(p`1/p`2)^2) & p9`1=p`1/sqrt(1+(p`1/p`2)^2)
by EUCLID:56;
then y in K1 by A35,A44,A45,A46;
hence y in the carrier of ((TOP-REAL 2)|D)|K1 by JORDAN1:1;
end;
then rng (Sq_Circ|K1)c= the carrier of ((TOP-REAL 2)|D) by A31,XBOOLE_1:1;
then Sq_Circ|K1 is Function of the carrier of ((TOP-REAL 2)|D)|K1,
the carrier of ((TOP-REAL 2)|D) by A30,A31,FUNCT_2:4;
then reconsider g=Sq_Circ|K1 as map of ((TOP-REAL 2)|D)|K1,
((TOP-REAL 2)|D) ;
A47:K0=[#](((TOP-REAL 2)|D)|K0) by PRE_TOPC:def 10;
A48:K1=[#](((TOP-REAL 2)|D)|K1) by PRE_TOPC:def 10;
A49:D= [#]((TOP-REAL 2)|D) by PRE_TOPC:def 10;
A50:K0 \/ K1 c= D
proof let x be set;assume A51:x in K0 \/ K1;
now per cases by A51,XBOOLE_0:def 2;
case x in K0;
then consider p such that A52:p=x &
(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2;
thus x in the carrier of TOP-REAL 2 & not x=0.REAL 2 by A52;
case x in K1;
then consider p such that A53:p=x &
(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2)
& p<>0.REAL 2;
thus x in the carrier of TOP-REAL 2 & not x=0.REAL 2 by A53;
end;
then x in the carrier of TOP-REAL 2 & not x in {0.REAL 2} by TARSKI:def 1
;
hence x in D by A2,XBOOLE_0:def 4;
end;
D c= K0 \/ K1
proof let x be set;assume A54: x in D;
then A55:x in (the carrier of TOP-REAL 2) & not x in {0.REAL 2}
by A2,XBOOLE_0:def 4;
reconsider px=x as Point of TOP-REAL 2 by A54;
(px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1)
& px<>0.REAL 2 or
(px`1<=px`2 & -px`2<=px`1 or px`1>=px`2 & px`1<=-px`2)
& px<>0.REAL 2 by A55,REAL_2:110,TARSKI:def 1;
then x in K0 or x in K1;
hence x in K0 \/ K1 by XBOOLE_0:def 2;
end;
then A56:([#](((TOP-REAL 2)|D)|K0)) \/ ([#](((TOP-REAL 2)|D)|K1))
= [#]((TOP-REAL 2)|D) by A47,A48,A49,A50,XBOOLE_0:def 10;
f=Sq_Circ|K0 & D=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2}
by A2;
then A57: f is continuous & K0 is closed by Th27;
g=Sq_Circ|K1 & D=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K1={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.REAL 2}
by A2;
then A58: g is continuous & K1 is closed by Th28;
A59: for x be set st x in ([#](((TOP-REAL 2)|D)|K0))
/\ ([#] (((TOP-REAL 2)|D)|K1)) holds f.x = g.x
proof let x be set;assume x in ([#](((TOP-REAL 2)|D)|K0))
/\ [#] (((TOP-REAL 2)|D)|K1);
then A60:x in K0 & x in K1 by A47,A48,XBOOLE_0:def 3;
then f.x=Sq_Circ.x by FUNCT_1:72;
hence f.x = g.x by A60,FUNCT_1:72;
end;
then consider h being map of (TOP-REAL 2)|D,(TOP-REAL 2)|D
such that A61: h= f+*g & h is continuous
by A47,A48,A56,A57,A58,JGRAPH_2:9;
A62:dom h=the carrier of ((TOP-REAL 2)|D) by FUNCT_2:def 1;
A63:the carrier of ((TOP-REAL 2)|D)=D by JORDAN1:1;
A64:the carrier of ((TOP-REAL 2)|D)
=[#](((TOP-REAL 2)|D)) by PRE_TOPC:12
.=((the carrier of TOP-REAL 2)\ {0.REAL 2}) by A2,PRE_TOPC:def 10;
dom Sq_Circ=(the carrier of (TOP-REAL 2)) by FUNCT_2:def 1;
then A65:dom (Sq_Circ|D)=(the carrier of (TOP-REAL 2))/\ D by FUNCT_1:68
.=the carrier of ((TOP-REAL 2)|D) by A63,XBOOLE_1:28;
A66:dom f=K0 by A11,FUNCT_2:def 1;
A67:K0=[#](((TOP-REAL 2)|D)|K0) by PRE_TOPC:def 10;
A68:dom g=K1 by A31,FUNCT_2:def 1;
K1=[#](((TOP-REAL 2)|D)|K1) by PRE_TOPC:def 10;
then A69:f tolerates g by A59,A66,A67,A68,PARTFUN1:def 6;
for x being set st x in dom h holds h.x=(Sq_Circ|D).x
proof let x be set;assume A70: x in dom h;
then x in (the carrier of TOP-REAL 2) & not x in {0.REAL 2}
by A64,XBOOLE_0:def 4;
then A71:x <>0.REAL 2 by TARSKI:def 1;
reconsider p=x as Point of TOP-REAL 2 by A64,A70,XBOOLE_0:def 4;
x in (the carrier of TOP-REAL 2)\D` by A1,A64,A70;
then A72:x in D`` by SUBSET_1:def 5;
per cases;
suppose A73:x in K0;
A74:Sq_Circ|D.p=Sq_Circ.p by A72,FUNCT_1:72.=f.p by A73,FUNCT_1:72;
h.p=(g+*f).p by A61,A69,FUNCT_4:35 .=f.p by A66,A73,FUNCT_4:14;
hence thesis by A74;
suppose not x in K0;
then not (p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) by A71;
then (p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2)by REAL_2:110;
then A75:x in K1 by A71;
Sq_Circ|D.p=Sq_Circ.p by A72,FUNCT_1:72.=g.p by A75,FUNCT_1:72;
hence thesis by A61,A68,A75,FUNCT_4:14;
end;
then f+*g=Sq_Circ|D by A61,A62,A65,FUNCT_1:9;
hence thesis by A47,A48,A56,A57,A58,A59,JGRAPH_2:9;
end;
theorem Th30:
for D being non empty Subset of TOP-REAL 2 st
D=(the carrier of TOP-REAL 2) \ {0.REAL 2} holds D`= {0.REAL 2}
proof
let D be non empty Subset of TOP-REAL 2;
assume A1:D=(the carrier of TOP-REAL 2) \{0.REAL 2};
A2:{0.REAL 2} c= D`
proof let x be set;assume A3: x in {0.REAL 2};
then not x in D by A1,XBOOLE_0:def 4;
then x in (the carrier of TOP-REAL 2)\D by A3,XBOOLE_0:def 4;
hence x in D` by SUBSET_1:def 5;
end;
D` c= {0.REAL 2}
proof let x be set;assume x in D`;
then x in (the carrier of TOP-REAL 2)\D by SUBSET_1:def 5;
then x in (the carrier of TOP-REAL 2) & not x in D by XBOOLE_0:def 4;
hence x in {0.REAL 2} by A1,XBOOLE_0:def 4;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem Th31:
ex h being map of TOP-REAL 2, TOP-REAL 2 st h=Sq_Circ & h is continuous
proof
reconsider f=Sq_Circ as map of (TOP-REAL 2),(TOP-REAL 2) ;
(the carrier of TOP-REAL 2) \{0.REAL 2} c=(the carrier of TOP-REAL 2)
by XBOOLE_1:36;
then reconsider D=(the carrier of TOP-REAL 2) \{0.REAL 2}
as non empty Subset of TOP-REAL 2 by JGRAPH_2:19;
A1: f.(0.REAL 2)=0.REAL 2 by Def1;
A2: D`= {0.REAL 2} by Th30;
A3: for p being Point of (TOP-REAL 2)|D holds f.p<>f.(0.REAL 2)
proof let p be Point of (TOP-REAL 2)|D;
A4:the carrier of (TOP-REAL 2)|D=[#]((TOP-REAL 2)|D) by PRE_TOPC:12;
A5:[#]((TOP-REAL 2)|D)=D by PRE_TOPC:def 10;
then A6:p in the carrier of TOP-REAL 2 & not p in {0.REAL 2}
by A4,XBOOLE_0:def 4;
reconsider q=p as Point of TOP-REAL 2 by A4,A5,XBOOLE_0:def 4;
A7:not p=0.REAL 2 by A6,TARSKI:def 1;
per cases;
suppose A8:not(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then A9:Sq_Circ.q=|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|
by A7,Def1;
A10:q`1<=q`2 & -q`2<=q`1 or q`1>=q`2 & q`1<=-q`2 by A8,JGRAPH_2:23;
A11:now assume A12:q`2=0;
then q`1=0 by A10;
hence contradiction by A7,A12,EUCLID:57,58;
end;
set q9=|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|;
A13:q9`1=q`1/sqrt(1+(q`1/q`2)^2) & q9`2=q`2/sqrt(1+(q`1/q`2)^2)
by EUCLID:56;
1+(q`1/q`2)^2>0 by Lm1;
then A14:sqrt(1+(q`1/q`2)^2)>0 by SQUARE_1:93;
now assume q9=0.REAL 2;
then 0 *sqrt(1+(q`1/q`2)^2)=q`2/sqrt(1+(q`1/q`2)^2)*sqrt(1+(q`1/q`2)^2)
by A13,EUCLID:56,58;
hence contradiction by A11,A14,XCMPLX_1:88;
end;
hence thesis by A9,Def1;
suppose A15:q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1;
then A16:Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|
by A7,Def1;
A17:now assume A18:q`1=0;
then q`2=0 by A15;
hence contradiction by A7,A18,EUCLID:57,58;
end;
set q9=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|;
A19:q9`1=q`1/sqrt(1+(q`2/q`1)^2) & q9`2=q`2/sqrt(1+(q`2/q`1)^2)
by EUCLID:56;
1+(q`2/q`1)^2>0 by Lm1;
then A20:sqrt(1+(q`2/q`1)^2)>0 by SQUARE_1:93;
now assume q9=0.REAL 2;
then 0 *sqrt(1+(q`2/q`1)^2)=q`1/sqrt(1+(q`2/q`1)^2)*sqrt(1+(q`2/q`1)^2)
by A19,EUCLID:56,58;
hence contradiction by A17,A20,XCMPLX_1:88;
end;
hence thesis by A16,Def1;
end;
A21:ex h being map of (TOP-REAL 2)|D,(TOP-REAL 2)|D
st h=Sq_Circ|D & h is continuous by A2,Th29;
for V being Subset of TOP-REAL 2 st f.(0.REAL 2) in V & V is open
ex W being Subset of TOP-REAL 2 st 0.REAL 2 in W
& W is open & f.:W c= V
proof let V be Subset of (TOP-REAL 2);
assume A22:f.(0.REAL 2) in V & V is open;
A23:the carrier of TOP-REAL 2=REAL 2 by EUCLID:25;
A24:Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then reconsider u0=0.REAL 2 as Point of Euclid 2 by EUCLID:25;
consider r being real number such that A25:r>0 & Ball(u0,r) c= V
by A1,A22,Lm2,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
reconsider W1=Ball(u0,r) as Subset of TOP-REAL 2
by A23,A24;
A26:u0 in W1 by A25,GOBOARD6:4;
A27:W1 is open by GOBOARD6:6;
f.:W1 c= W1
proof let z be set;assume z in f.:W1;
then consider y being set such that
A28: y in dom f & y in W1 & z=f.y by FUNCT_1:def 12;
reconsider q=y as Point of TOP-REAL 2 by A28;
reconsider qy=q as Point of Euclid 2 by A24,EUCLID:25;
z in rng f by A28,FUNCT_1:def 5;
then reconsider qz=z as Point of TOP-REAL 2;
reconsider pz=qz as Point of Euclid 2 by A24,EUCLID:25;
dist(u0,qy)<r by A28,METRIC_1:12;
then |.(0.REAL 2) - q.|<r by JGRAPH_1:45;
then sqrt((((0.REAL 2) - q)`1)^2+(((0.REAL 2) - q)`2)^2)<r by JGRAPH_1:
47;
then sqrt(((0.REAL 2)`1 - q`1)^2+(((0.REAL 2) - q)`2)^2)<r
by TOPREAL3:8;
then sqrt(((0.REAL 2)`1 - q`1)^2+((0.REAL 2)`2 - q`2)^2)<r
by TOPREAL3:8;
then sqrt((- q`1)^2+(0 - q`2)^2)<r by JGRAPH_2:11,XCMPLX_1:150;
then sqrt((- q`1)^2+(- q`2)^2)<r by XCMPLX_1:150;
then sqrt((q`1)^2+(- q`2)^2)<r by SQUARE_1:61;
then A29:sqrt((q`1)^2+(q`2)^2)<r by SQUARE_1:61;
per cases;
suppose q=0.REAL 2;
hence thesis by A28,Def1;
suppose q<>0.REAL 2 &
(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then A30:Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)
]|
by Def1;
A31:((0.REAL 2) - qz)`1=(0.REAL 2)`1-qz`1 by TOPREAL3:8
.= -qz`1 by JGRAPH_2:11,XCMPLX_1:150;
A32:((0.REAL 2) - qz)`2=(0.REAL 2)`2-qz`2 by TOPREAL3:8
.= -qz`2 by JGRAPH_2:11,XCMPLX_1:150;
(q`2/q`1)^2 >=0 by SQUARE_1:72;
then 1+(q`2/q`1)^2>=1+0 by REAL_1:55;
then A33:sqrt(1+(q`2/q`1)^2)>=1 by Th8;
then (sqrt(1+(q`2/q`1)^2))^2>=sqrt(1+(q`2/q`1)^2) by JGRAPH_2:2;
then A34:1<=(sqrt(1+(q`2/q`1)^2))^2 by A33,AXIOMS:22;
A35:(qz`1)^2=(q`1/sqrt(1+(q`2/q`1)^2))^2 by A28,A30,EUCLID:56
.=(q`1)^2/(sqrt(1+(q`2/q`1)^2))^2 by SQUARE_1:69;
A36:(qz`1)^2>=0 by SQUARE_1:72;
(q`1)^2>=0 by SQUARE_1:72;
then A37:(qz`1)^2<=(q`1)^2/1 by A34,A35,REAL_2:201;
A38:(qz`2)^2=(q`2/sqrt(1+(q`2/q`1)^2))^2 by A28,A30,EUCLID:56
.=(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2 by SQUARE_1:69;
A39:(qz`2)^2>=0 by SQUARE_1:72;
(q`2)^2>=0 by SQUARE_1:72;
then A40:(qz`2)^2<=(q`2)^2/1 by A34,A38,REAL_2:201;
A41:sqrt((((0.REAL 2) - qz)`1)^2+(((0.REAL 2) - qz)`2)^2)
=sqrt((qz`1)^2+(-qz`2)^2) by A31,A32,SQUARE_1:61
.=sqrt((qz`1)^2+(qz`2)^2) by SQUARE_1:61;
A42:(qz`1)^2+(qz`2)^2<=(q`1)^2+(q`2)^2 by A37,A40,REAL_1:55;
0+0<= (qz`1)^2+(qz`2)^2 by A36,A39,REAL_1:55;
then sqrt((qz`1)^2+(qz`2)^2) <= sqrt((q`1)^2+(q`2)^2)
by A42,SQUARE_1:94;
then sqrt((((0.REAL 2) - qz)`1)^2+(((0.REAL 2) - qz)`2)^2)<r
by A29,A41,AXIOMS:22;
then |.(0.REAL 2) - qz.|<r by JGRAPH_1:47;
then dist(u0,pz)<r by JGRAPH_1:45;
hence thesis by METRIC_1:12;
suppose q<>0.REAL 2 &
not (q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then A43:Sq_Circ.q=|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)
]|
by Def1;
A44:((0.REAL 2) - qz)`1=(0.REAL 2)`1-qz`1 by TOPREAL3:8
.= -qz`1 by JGRAPH_2:11,XCMPLX_1:150;
A45:((0.REAL 2) - qz)`2=(0.REAL 2)`2-qz`2 by TOPREAL3:8
.= -qz`2 by JGRAPH_2:11,XCMPLX_1:150;
(q`1/q`2)^2 >=0 by SQUARE_1:72;
then 1+(q`1/q`2)^2>=1+0 by REAL_1:55;
then A46:sqrt(1+(q`1/q`2)^2)>=1 by Th8;
then (sqrt(1+(q`1/q`2)^2))^2>=sqrt(1+(q`1/q`2)^2) by JGRAPH_2:2;
then A47:1<=(sqrt(1+(q`1/q`2)^2))^2 by A46,AXIOMS:22;
A48:(qz`1)^2=(q`1/sqrt(1+(q`1/q`2)^2))^2 by A28,A43,EUCLID:56
.=(q`1)^2/(sqrt(1+(q`1/q`2)^2))^2 by SQUARE_1:69;
A49:(qz`1)^2>=0 by SQUARE_1:72;
(q`1)^2>=0 by SQUARE_1:72;
then A50:(qz`1)^2<=(q`1)^2/1 by A47,A48,REAL_2:201;
A51:(qz`2)^2=(q`2/sqrt(1+(q`1/q`2)^2))^2 by A28,A43,EUCLID:56
.=(q`2)^2/(sqrt(1+(q`1/q`2)^2))^2 by SQUARE_1:69;
A52:(qz`2)^2>=0 by SQUARE_1:72;
(q`2)^2>=0 by SQUARE_1:72;
then A53: (qz`2)^2<=(q`2)^2/1 by A47,A51,REAL_2:201;
A54:sqrt((((0.REAL 2) - qz)`1)^2+(((0.REAL 2) - qz)`2)^2)
=sqrt((qz`1)^2+(-qz`2)^2) by A44,A45,SQUARE_1:61
.=sqrt((qz`1)^2+(qz`2)^2) by SQUARE_1:61;
A55:(qz`1)^2+(qz`2)^2<=(q`1)^2+(q`2)^2 by A50,A53,REAL_1:55;
0+0<= (qz`1)^2+(qz`2)^2 by A49,A52,REAL_1:55;
then sqrt((qz`1)^2+(qz`2)^2) <= sqrt((q`1)^2+(q`2)^2)
by A55,SQUARE_1:94;
then sqrt((((0.REAL 2) - qz)`1)^2+(((0.REAL 2) - qz)`2)^2)<r
by A29,A54,AXIOMS:22;
then |.(0.REAL 2) - qz.|<r by JGRAPH_1:47;
then dist(u0,pz)<r by JGRAPH_1:45;
hence thesis by METRIC_1:12;
end;
then f.:W1 c= V by A25,XBOOLE_1:1;
hence ex W being Subset of TOP-REAL 2 st 0.REAL 2 in W
& W is open & f.:W c= V by A26,A27;
end;
then f is continuous by A1,A2,A3,A21,Th13;
hence thesis;
end;
theorem Th32: Sq_Circ is one-to-one
proof
let x1,x2 be set;
assume A1: x1 in dom Sq_Circ & x2 in dom Sq_Circ & Sq_Circ.x1=Sq_Circ.x2;
then reconsider p1=x1 as Point of TOP-REAL 2;
reconsider p2=x2 as Point of TOP-REAL 2 by A1;
set q=p1,p=p2;
per cases;
suppose A2:q=0.REAL 2;
then A3:Sq_Circ.q=0.REAL 2 by Def1;
now per cases;
case p=0.REAL 2;
hence x1=x2 by A2;
case A4:p<>0.REAL 2 &
(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1);
then Sq_Circ.p=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|
by Def1;
then A5:p`1/sqrt(1+(p`2/p`1)^2)=0 & p`2/sqrt(1+(p`2/p`1)^2)=0
by A1,A3,EUCLID:56,JGRAPH_2:11;
(p`2/p`1)^2 >=0 by SQUARE_1:72;
then 1+(p`2/p`1)^2>=1+0 by REAL_1:55;
then sqrt(1+(p`2/p`1)^2)>=1 by Th8;
then A6:sqrt(1+(p`2/p`1)^2)>0 by AXIOMS:22;
then A7:p`1= 0 *sqrt(1+(p`2/p`1)^2) by A5,XCMPLX_1:88 .=0;
p`2= 0 *sqrt(1+(p`2/p`1)^2) by A5,A6,XCMPLX_1:88 .=0;
hence contradiction by A4,A7,EUCLID:57,58;
case A8:p<>0.REAL 2 &
not (p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1);
then Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|
by Def1;
then A9:p`1/sqrt(1+(p`1/p`2)^2)=0 & p`2/sqrt(1+(p`1/p`2)^2)=0
by A1,A3,EUCLID:56,JGRAPH_2:11;
(p`1/p`2)^2 >=0 by SQUARE_1:72;
then 1+(p`1/p`2)^2>=1+0 by REAL_1:55;
then sqrt(1+(p`1/p`2)^2)>=1 by Th8;
then A10:sqrt(1+(p`1/p`2)^2)>0 by AXIOMS:22;
then A11:p`1= 0 *sqrt(1+(p`1/p`2)^2) by A9,XCMPLX_1:88 .=0;
p`2= 0 *sqrt(1+(p`1/p`2)^2) by A9,A10,XCMPLX_1:88 .=0;
hence contradiction by A8,A11;
end;
hence x1=x2;
suppose A12:q<>0.REAL 2 &
(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then A13:Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|
by Def1;
A14: (|[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;
A15:1+(q`2/q`1)^2>0 by Lm1;
then A16:sqrt(1+(q`2/q`1)^2)>0 by SQUARE_1:93;
now per cases;
case p=0.REAL 2;
then Sq_Circ.p=0.REAL 2 by Def1;
then A17:q`1/sqrt(1+(q`2/q`1)^2)=0 & q`2/sqrt(1+(q`2/q`1)^2)=0
by A1,A13,EUCLID:56,JGRAPH_2:11;
(q`2/q`1)^2 >=0 by SQUARE_1:72;
then 1+(q`2/q`1)^2>=1+0 by REAL_1:55;
then sqrt(1+(q`2/q`1)^2)>=1 by Th8;
then A18:sqrt(1+(q`2/q`1)^2)>0 by AXIOMS:22;
then A19:q`1= 0 *sqrt(1+(q`2/q`1)^2) by A17,XCMPLX_1:88 .=0;
q`2= 0 *sqrt(1+(q`2/q`1)^2) by A17,A18,XCMPLX_1:88 .=0;
hence contradiction by A12,A19,EUCLID:57,58;
case A20:p<>0.REAL 2 &
(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1);
then A21:Sq_Circ.p=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|
by Def1;
then A22:p`1/sqrt(1+(p`2/p`1)^2)=q`1/sqrt(1+(q`2/q`1)^2) &
p`2/sqrt(1+(p`2/p`1)^2)=q`2/sqrt(1+(q`2/q`1)^2)
by A1,A13,A14,EUCLID:56;
A23:1+(p`2/p`1)^2>0 by Lm1;
then A24:sqrt(1+(p`2/p`1)^2)>0 by SQUARE_1:93;
(p`1)^2/(sqrt(1+(p`2/p`1)^2))^2=(q`1/sqrt(1+(q`2/q`1)^2))^2
by A22,SQUARE_1:69;
then (p`1)^2/(sqrt(1+(p`2/p`1)^2))^2=(q`1)^2/(sqrt(1+(q`2/q`1)^2))^2
by SQUARE_1:69;
then (p`1)^2/(1+(p`2/p`1)^2)=(q`1)^2/(sqrt(1+(q`2/q`1)^2))^2
by A23,SQUARE_1:def 4;
then A25:(p`1)^2/(1+(p`2/p`1)^2)=(q`1)^2/(1+(q`2/q`1)^2)
by A15,SQUARE_1:def 4;
(p`2)^2/(sqrt(1+(p`2/p`1)^2))^2=(q`2/sqrt(1+(q`2/q`1)^2))^2
by A22,SQUARE_1:69;
then (p`2)^2/(sqrt(1+(p`2/p`1)^2))^2=(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by SQUARE_1:69;
then (p`2)^2/(1+(p`2/p`1)^2)=(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by A23,SQUARE_1:def 4;
then A26:(p`2)^2/(1+(p`2/p`1)^2)=(q`2)^2/(1+(q`2/q`1)^2)
by A15,SQUARE_1:def 4;
now assume
A27:p`1=0;
then p`2=0 by A20;
hence contradiction by A20,A27,EUCLID:57,58;
end;
then A28:(p`1)^2>0 by SQUARE_1:74;
(p`1)^2/(1+(p`2/p`1)^2)/(p`1)^2=(q`1)^2/(p`1)^2/(1+(q`2/q`1)^2)
by A25,XCMPLX_1:48;
then (p`1)^2/(p`1)^2/(1+(p`2/p`1)^2)=(q`1)^2/(p`1)^2/(1+(q`2/q`1)^2)
by XCMPLX_1:48;
then 1/(1+(p`2/p`1)^2)=(q`1)^2/(p`1)^2/(1+(q`2/q`1)^2)
by A28,XCMPLX_1:60;
then A29:1/(1+(p`2/p`1)^2)*(1+(q`2/q`1)^2)=(q`1)^2/(p`1)^2
by A15,XCMPLX_1:88;
now assume
A30:q`1=0;
then q`2=0 by A12;
hence contradiction by A12,A30,EUCLID:57,58;
end;
then A31:(q`1)^2>0 by SQUARE_1:74;
now per cases;
case A32:p`2=0;
then (q`2)^2=0 by A15,A26,SQUARE_1:60,XCMPLX_1:50;
then A33:q`2=0 by SQUARE_1:73;
then p=|[q`1,0]|by A1,A13,A21,A32,EUCLID:57,SQUARE_1:60,83;
hence x1=x2 by A33,EUCLID:57;
case p`2<>0;
then A34:(p`2)^2>0 by SQUARE_1:74;
(p`2)^2/(1+(p`2/p`1)^2)/(p`2)^2=(q`2)^2/(p`2)^2/(1+(q`2/q`1)^2)
by A26,XCMPLX_1:48;
then (p`2)^2/(p`2)^2/(1+(p`2/p`1)^2)=(q`2)^2/(p`2)^2/(1+(q`2/q`1)^2)
by XCMPLX_1:48;
then 1/(1+(p`2/p`1)^2)=(q`2)^2/(p`2)^2/(1+(q`2/q`1)^2)
by A34,XCMPLX_1:60;
then 1/(1+(p`2/p`1)^2)*(1+(q`2/q`1)^2)=(q`2)^2/(p`2)^2
by A15,XCMPLX_1:88;
then (q`1)^2/(q`1)^2/(p`1)^2=(q`2)^2/(p`2)^2/(q`1)^2
by A29,XCMPLX_1:48;
then 1/(p`1)^2=(q`2)^2/(p`2)^2/(q`1)^2 by A31,XCMPLX_1:60;
then 1/(p`1)^2*(p`2)^2=(p`2)^2*((q`2)^2/(p`2)^2)/(q`1)^2
by XCMPLX_1:75;
then 1/(p`1)^2*(p`2)^2=(q`2)^2/(q`1)^2 by A34,XCMPLX_1:88;
then (p`2)^2/(p`1)^2=(q`2)^2/(q`1)^2 by XCMPLX_1:100;
then (p`2/p`1)^2=(q`2)^2/(q`1)^2 by SQUARE_1:69;
then A35:(1+(p`2/p`1)^2)=(1+(q`2/q`1)^2) by SQUARE_1:69;
then p`1=q`1/sqrt(1+(q`2/q`1)^2)*sqrt(1+(q`2/q`1)^2)
by A22,A24,XCMPLX_1:88;
then A36:p`1=q`1 by A16,XCMPLX_1:88;
p`2=q`2/sqrt(1+(q`2/q`1)^2)*sqrt(1+(q`2/q`1)^2)
by A22,A24,A35,XCMPLX_1:88;
then p`2=q`2 by A16,XCMPLX_1:88;
then p=|[q`1,q`2]|by A36,EUCLID:57;
hence x1=x2 by EUCLID:57;
end;
hence x1=x2;
case A37:p<>0.REAL 2 &
not (p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1);
then A38: p<>0.REAL 2 & p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2
by JGRAPH_2:23;
(|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|)`1
= p`1/sqrt(1+(p`1/p`2)^2) &
(|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|)`2
= p`2/sqrt(1+(p`1/p`2)^2) by EUCLID:56;
then A39:p`1/sqrt(1+(p`1/p`2)^2)=q`1/sqrt(1+(q`2/q`1)^2) &
p`2/sqrt(1+(p`1/p`2)^2)=q`2/sqrt(1+(q`2/q`1)^2)
by A1,A13,A14,A37,Def1;
A40:1+(p`1/p`2)^2>0 by Lm1;
then A41:sqrt(1+(p`1/p`2)^2)>0 by SQUARE_1:93;
(p`1)^2/(sqrt(1+(p`1/p`2)^2))^2=(q`1/sqrt(1+(q`2/q`1)^2))^2
by A39,SQUARE_1:69;
then (p`1)^2/(sqrt(1+(p`1/p`2)^2))^2=(q`1)^2/(sqrt(1+(q`2/q`1)^2))^2
by SQUARE_1:69;
then (p`1)^2/(1+(p`1/p`2)^2)=(q`1)^2/(sqrt(1+(q`2/q`1)^2))^2
by A40,SQUARE_1:def 4;
then A42:(p`1)^2/(1+(p`1/p`2)^2)=(q`1)^2/(1+(q`2/q`1)^2)
by A15,SQUARE_1:def 4;
(p`2)^2/(sqrt(1+(p`1/p`2)^2))^2=(q`2/sqrt(1+(q`2/q`1)^2))^2
by A39,SQUARE_1:69;
then (p`2)^2/(sqrt(1+(p`1/p`2)^2))^2=(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by SQUARE_1:69;
then (p`2)^2/(1+(p`1/p`2)^2)=(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by A40,SQUARE_1:def 4;
then A43:(p`2)^2/(1+(p`1/p`2)^2)=(q`2)^2/(1+(q`2/q`1)^2)
by A15,SQUARE_1:def 4;
p`2<>0 by A37,A38;
then A44:(p`2)^2>0 by SQUARE_1:74;
(p`2)^2/(1+(p`1/p`2)^2)/(p`2)^2=(q`2)^2/(p`2)^2/(1+(q`2/q`1)^2)
by A43,XCMPLX_1:48;
then (p`2)^2/(p`2)^2/(1+(p`1/p`2)^2)=(q`2)^2/(p`2)^2/(1+(q`2/q`1)^2)
by XCMPLX_1:48;
then 1/(1+(p`1/p`2)^2)=(q`2)^2/(p`2)^2/(1+(q`2/q`1)^2)
by A44,XCMPLX_1:60;
then A45:1/(1+(p`1/p`2)^2)*(1+(q`2/q`1)^2)=(q`2)^2/(p`2)^2
by A15,XCMPLX_1:88;
A46:now assume
A47:q`1=0;
then q`2=0 by A12;
hence contradiction by A12,A47,EUCLID:57,58;
end;
then A48:(q`1)^2>0 by SQUARE_1:74;
now per cases;
case p`1=0;
then (q`1)^2=0 by A15,A42,SQUARE_1:60,XCMPLX_1:50;
then A49:q`1=0 by SQUARE_1:73;
then q`2=0 by A12;
hence contradiction by A12,A49,EUCLID:57,58;
case A50:p`1<>0;
then A51:(p`1)^2>0 by SQUARE_1:74;
(p`1)^2/(1+(p`1/p`2)^2)/(p`1)^2=(q`1)^2/(p`1)^2/(1+(q`2/q`1)^2)
by A42,XCMPLX_1:48;
then (p`1)^2/(p`1)^2/(1+(p`1/p`2)^2)=(q`1)^2/(p`1)^2/(1+(q`2/q`1)^2)
by XCMPLX_1:48;
then 1/(1+(p`1/p`2)^2)=(q`1)^2/(p`1)^2/(1+(q`2/q`1)^2)
by A51,XCMPLX_1:60;
then 1/(1+(p`1/p`2)^2)*(1+(q`2/q`1)^2)=(q`1)^2/(p`1)^2
by A15,XCMPLX_1:88;
then (q`1)^2/(q`1)^2/(p`1)^2=(q`2)^2/(p`2)^2/(q`1)^2 by A45,XCMPLX_1:
48;
then 1/(p`1)^2=(q`2)^2/(p`2)^2/(q`1)^2 by A48,XCMPLX_1:60;
then 1/(p`1)^2*(p`2)^2=(p`2)^2*((q`2)^2/(p`2)^2)/(q`1)^2
by XCMPLX_1:75;
then 1/(p`1)^2*(p`2)^2=(q`2)^2/(q`1)^2 by A44,XCMPLX_1:88;
then (p`2)^2/(p`1)^2=(q`2)^2/(q`1)^2 by XCMPLX_1:100;
then (p`2/p`1)^2=(q`2)^2/(q`1)^2 by SQUARE_1:69;
then A52:(p`2/p`1)^2=(q`2/q`1)^2 by SQUARE_1:69;
set a=q`2/q`1;
A53:p`2/p`1*p`1=a*p`1 or p`2/p`1*p`1=(-a)*p`1 by A52,Th1;
A54:now per cases by A50,A53,XCMPLX_1:88;
case A55: p`2=a*p`1;
now per cases by A50;
case p`1>0;
then p`1/p`1<= a*p`1/p`1 & (-(a*p`1))/p`1<=p`1/p`1 or
p`1/p`1>=(a*p`1)/p`1 & p`1/p`1<=(-(a*p`1))/p`1
by A38,A55,REAL_1:73;
then A56:1<= a*p`1/p`1 & (-(a*p`1))/p`1<=1 or
1>=(a*p`1)/p`1 & 1<=(-(a*p`1))/p`1 by A50,XCMPLX_1:60;
(a*p`1)/p`1=a by A50,XCMPLX_1:90;
hence 1<=a & -a<=1 or 1>=a & 1<=-a by A56,XCMPLX_1:188;
case p`1<0;
then p`1/p`1>= a*p`1/p`1 & (-(a*p`1))/p`1>=p`1/p`1 or
p`1/p`1<=(a*p`1)/p`1 & p`1/p`1>=(-(a*p`1))/p`1
by A38,A55,REAL_1:74;
then A57:1>= a*p`1/p`1 & (-(a*p`1))/p`1>=1 or
1<=(a*p`1)/p`1 & 1>=(-(a*p`1))/p`1 by A50,XCMPLX_1:60;
(a*p`1)/p`1=a by A50,XCMPLX_1:90;
hence 1<=a & -a<=1 or 1>=a & 1<=-a by A57,XCMPLX_1:188;
end;
then 1<=a & -a<=1 or 1>=a & -1>=--a by REAL_1:50;
hence 1<=a or -1>=a;
case A58: p`2=(-a)*p`1;
now per cases by A50;
case p`1>0;
then p`1/p`1<= (-a)*p`1/p`1 & (-((-a)*p`1))/p`1<=p`1/p`1 or
p`1/p`1>=((-a)*p`1)/p`1 & p`1/p`1<=(-((-a)*p`1))/p`1
by A38,A58,REAL_1:73;
then A59:1<= (-a)*p`1/p`1 & (-((-a)*p`1))/p`1<=1 or
1>=((-a)*p`1)/p`1 & 1<=(-((-a)*p`1))/p`1 by A50,XCMPLX_1:60;
A60:((-a)*p`1)/p`1=(-a) by A50,XCMPLX_1:90;
1<= (-a) & -(((-a)*p`1)/p`1)<=1 or
1>=(-a) & 1<=-(((-a)*p`1)/p`1) by A50,A59,XCMPLX_1:90,188;
hence 1<=a & -a<=1 or 1>=a & 1<=-a by A60;
case p`1<0;
then p`1/p`1>= (-a)*p`1/p`1 & (-((-a)*p`1))/p`1>=p`1/p`1 or
p`1/p`1<=((-a)*p`1)/p`1 & p`1/p`1>=(-((-a)*p`1))/p`1
by A38,A58,REAL_1:74;
then A61:1>= (-a)*p`1/p`1 & (-((-a)*p`1))/p`1>=1 or
1<=((-a)*p`1)/p`1 & 1>=(-((-a)*p`1))/p`1 by A50,XCMPLX_1:60;
A62:((-a)*p`1)/p`1=(-a) by A50,XCMPLX_1:90;
1>= (-a) & -(((-a)*p`1)/p`1)>=1 or
1<=(-a) & 1>=-(((-a)*p`1)/p`1) by A50,A61,XCMPLX_1:90,188;
hence 1<=a & -a<=1 or 1>=a & 1<=-a by A62;
end;
then 1<=a & -a<=1 or 1>=a & -1>=--a by REAL_1:50;
hence 1<=a or -1>=a;
end;
A63:q`1*a<=q`1 & -q`1<=q`1*a or q`1*a>=q`1 & q`1*a<=-q`1
by A12,A46,XCMPLX_1:88;
A64:now per cases by A46;
case A65:q`1>0;
then a*q`1/q`1<=q`1/q`1 & (-q`1)/q`1<=a*q`1/q`1
or a*q`1/q`1>=q`1/q`1 & a*q`1/q`1<=(-q`1)/q`1 by A63,REAL_1:73;
then A66:a<=q`1/q`1 & (-q`1)/q`1<=a
or a>=q`1/q`1 & a<=(-q`1)/q`1 by A65,XCMPLX_1:90;
q`1/q`1=1 by A65,XCMPLX_1:60;
hence a<=1 & -1<=a or a>=1 & a<=-1 by A66,XCMPLX_1:188;
case A67:q`1<0;
then A68:a*q`1/q`1>=q`1/q`1 & (-q`1)/q`1>=a*q`1/q`1
or a*q`1/q`1<=q`1/q`1 & a*q`1/q`1>=(-q`1)/q`1 by A63,REAL_1:74;
A69:q`1/q`1=1 by A67,XCMPLX_1:60;
(-q`1)/q`1=-1 by A67,XCMPLX_1:198;
hence a<=1 & -1<=a or a>=1 & a<=-1 by A67,A68,A69,XCMPLX_1:90
;
end;
A70: now per cases by A54,A64,AXIOMS:21,22;
case a=1;
then (p`2)^2/(p`1)^2=1 by A52,SQUARE_1:59,69;
then A71:(p`2)^2=(p`1)^2 by XCMPLX_1:58;
(p`1/p`2)^2=(p`1)^2/(p`2)^2 by SQUARE_1:69;
hence (p`1/p`2)^2=(q`2/q`1)^2 by A52,A71,SQUARE_1:69;
case a=-1; then a^2=1 by SQUARE_1:59,61;
then (p`2)^2/(p`1)^2=1 by A52,SQUARE_1:69;
then A72:(p`2)^2=(p`1)^2 by XCMPLX_1:58;
(p`1/p`2)^2=(p`1)^2/(p`2)^2 by SQUARE_1:69;
hence (p`1/p`2)^2=(q`2/q`1)^2 by A52,A72,SQUARE_1:69;
end;
then p`1=q`1/sqrt(1+(q`2/q`1)^2)*sqrt(1+(q`2/q`1)^2)
by A39,A41,XCMPLX_1:88;
then A73:p`1=q`1 by A16,XCMPLX_1:88;
p`2=q`2/sqrt(1+(q`2/q`1)^2)*sqrt(1+(q`2/q`1)^2)
by A39,A41,A70,XCMPLX_1:88;
then p`2=q`2 by A16,XCMPLX_1:88;
then p=|[q`1,q`2]| by A73,EUCLID:57;
hence x1=x2 by EUCLID:57;
end;
hence x1=x2;
end;
hence x1=x2;
suppose A74:q<>0.REAL 2 &
not (q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then A75:Sq_Circ.q=|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|
by Def1;
A76: (|[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;
A77:1+(q`1/q`2)^2>0 by Lm1;
then A78:sqrt(1+(q`1/q`2)^2)>0 by SQUARE_1:93;
A79: (q`1<=q`2 & -q`2<=q`1 or q`1>=q`2 & q`1<=-q`2)
by A74,JGRAPH_2:23;
now per cases;
case p=0.REAL 2;
then Sq_Circ.p=0.REAL 2 by Def1;
then A80:q`1/sqrt(1+(q`1/q`2)^2)=0 & q`2/sqrt(1+(q`1/q`2)^2)=0
by A1,A75,EUCLID:56,JGRAPH_2:11;
(q`1/q`2)^2 >=0 by SQUARE_1:72;
then 1+(q`1/q`2)^2>=1+0 by REAL_1:55;
then sqrt(1+(q`1/q`2)^2)>=1 by Th8;
then A81:sqrt(1+(q`1/q`2)^2)>0 by AXIOMS:22;
then A82:q`1= 0 *sqrt(1+(q`1/q`2)^2) by A80,XCMPLX_1:88 .=0;
q`2= 0 *sqrt(1+(q`1/q`2)^2) by A80,A81,XCMPLX_1:88 .=0;
hence contradiction by A74,A82;
case A83:p<>0.REAL 2 &
(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1);
then Sq_Circ.p=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|
by Def1;
then A84:p`1/sqrt(1+(p`2/p`1)^2)=q`1/sqrt(1+(q`1/q`2)^2) &
p`2/sqrt(1+(p`2/p`1)^2)=q`2/sqrt(1+(q`1/q`2)^2)
by A1,A75,A76,EUCLID:56;
A85:1+(p`2/p`1)^2>0 by Lm1;
then A86:sqrt(1+(p`2/p`1)^2)>0 by SQUARE_1:93;
(p`1)^2/(sqrt(1+(p`2/p`1)^2))^2=(q`1/sqrt(1+(q`1/q`2)^2))^2
by A84,SQUARE_1:69;
then (p`1)^2/(sqrt(1+(p`2/p`1)^2))^2=(q`1)^2/(sqrt(1+(q`1/q`2)^2))^2
by SQUARE_1:69;
then (p`1)^2/(1+(p`2/p`1)^2)=(q`1)^2/(sqrt(1+(q`1/q`2)^2))^2
by A85,SQUARE_1:def 4;
then A87:(p`1)^2/(1+(p`2/p`1)^2)=(q`1)^2/(1+(q`1/q`2)^2)
by A77,SQUARE_1:def 4;
(p`2)^2/(sqrt(1+(p`2/p`1)^2))^2=(q`2/sqrt(1+(q`1/q`2)^2))^2
by A84,SQUARE_1:69;
then (p`2)^2/(sqrt(1+(p`2/p`1)^2))^2=(q`2)^2/(sqrt(1+(q`1/q`2)^2))^2
by SQUARE_1:69;
then (p`2)^2/(1+(p`2/p`1)^2)=(q`2)^2/(sqrt(1+(q`1/q`2)^2))^2
by A85,SQUARE_1:def 4;
then A88:(p`2)^2/(1+(p`2/p`1)^2)=(q`2)^2/(1+(q`1/q`2)^2)
by A77,SQUARE_1:def 4;
now assume
A89:p`1=0;
then p`2=0 by A83;
hence contradiction by A83,A89,EUCLID:57,58;
end;
then A90:(p`1)^2>0 by SQUARE_1:74;
(p`1)^2/(1+(p`2/p`1)^2)/(p`1)^2=(q`1)^2/(p`1)^2/(1+(q`1/q`2)^2)
by A87,XCMPLX_1:48;
then (p`1)^2/(p`1)^2/(1+(p`2/p`1)^2)=(q`1)^2/(p`1)^2/(1+(q`1/q`2)^2)
by XCMPLX_1:48;
then 1/(1+(p`2/p`1)^2)=(q`1)^2/(p`1)^2/(1+(q`1/q`2)^2)
by A90,XCMPLX_1:60;
then A91:1/(1+(p`2/p`1)^2)*(1+(q`1/q`2)^2)=(q`1)^2/(p`1)^2 by A77,XCMPLX_1:
88
;
A92: q`2<>0 by A74,A79;
then A93:(q`2)^2>0 by SQUARE_1:74;
now per cases;
case p`2=0;
then (q`2)^2=0 by A77,A88,SQUARE_1:60,XCMPLX_1:50;
then q`2=0 by SQUARE_1:73;
hence contradiction by A74,A79;
case A94:p`2<>0;
then A95:(p`2)^2>0 by SQUARE_1:74;
(p`2)^2/(1+(p`2/p`1)^2)/(p`2)^2=(q`2)^2/(p`2)^2/(1+(q`1/q`2)^2)
by A88,XCMPLX_1:48;
then (p`2)^2/(p`2)^2/(1+(p`2/p`1)^2)=(q`2)^2/(p`2)^2/(1+(q`1/q`2)^2)
by XCMPLX_1:48;
then 1/(1+(p`2/p`1)^2)=(q`2)^2/(p`2)^2/(1+(q`1/q`2)^2)
by A95,XCMPLX_1:60;
then 1/(1+(p`2/p`1)^2)*(1+(q`1/q`2)^2)=(q`2)^2/(p`2)^2
by A77,XCMPLX_1:88;
then (q`2)^2/(q`2)^2/(p`2)^2=(q`1)^2/(p`1)^2/(q`2)^2
by A91,XCMPLX_1:48;
then 1/(p`2)^2=(q`1)^2/(p`1)^2/(q`2)^2 by A93,XCMPLX_1:60;
then 1/(p`2)^2*(p`1)^2=(p`1)^2*((q`1)^2/(p`1)^2)/(q`2)^2
by XCMPLX_1:75;
then 1/(p`2)^2*(p`1)^2=(q`1)^2/(q`2)^2 by A90,XCMPLX_1:88;
then (p`1)^2/(p`2)^2=(q`1)^2/(q`2)^2 by XCMPLX_1:100;
then (p`1/p`2)^2=(q`1)^2/(q`2)^2 by SQUARE_1:69;
then A96:(p`1/p`2)^2=(q`1/q`2)^2 by SQUARE_1:69;
then A97:p`1/p`2=q`1/q`2 or p`1/p`2=-q`1/q`2 by Th1;
set a=q`1/q`2;
A98:now per cases by A94,A97,XCMPLX_1:88;
case A99: p`1=a*p`2;
now per cases by A94;
case p`2>0;
then p`2/p`2<= a*p`2/p`2 & (-(a*p`2))/p`2<=p`2/p`2 or
p`2/p`2>=(a*p`2)/p`2 & p`2/p`2<=(-(a*p`2))/p`2
by A83,A99,REAL_1:73;
then A100:1<= a*p`2/p`2 & (-(a*p`2))/p`2<=1 or
1>=(a*p`2)/p`2 & 1<=(-(a*p`2))/p`2 by A94,XCMPLX_1:60;
(a*p`2)/p`2=a by A94,XCMPLX_1:90;
hence 1<=a & -a<=1 or 1>=a & 1<=-a by A100,XCMPLX_1:188;
case p`2<0;
then p`2/p`2>= a*p`2/p`2 & (-(a*p`2))/p`2>=p`2/p`2 or
p`2/p`2<=(a*p`2)/p`2 & p`2/p`2>=(-(a*p`2))/p`2
by A83,A99,REAL_1:74;
then A101:1>= a*p`2/p`2 & (-(a*p`2))/p`2>=1 or
1<=(a*p`2)/p`2 & 1>=(-(a*p`2))/p`2 by A94,XCMPLX_1:60;
(a*p`2)/p`2=a by A94,XCMPLX_1:90;
hence 1<=a & -a<=1 or 1>=a & 1<=-a by A101,XCMPLX_1:188;
end;
then 1<=a & -a<=1 or 1>=a & -1>=--a by REAL_1:50;
hence 1<=a or -1>=a;
case A102: p`1=(-a)*p`2;
now per cases by A94;
case p`2>0;
then p`2/p`2<= (-a)*p`2/p`2 & (-((-a)*p`2))/p`2<=p`2/p`2 or
p`2/p`2>=((-a)*p`2)/p`2 & p`2/p`2<=(-((-a)*p`2))/p`2
by A83,A102,REAL_1:73;
then A103:1<= (-a)*p`2/p`2 & (-((-a)*p`2))/p`2<=1 or
1>=((-a)*p`2)/p`2 & 1<=(-((-a)*p`2))/p`2 by A94,XCMPLX_1:60;
A104:((-a)*p`2)/p`2=(-a) by A94,XCMPLX_1:90;
1<= (-a) & -(((-a)*p`2)/p`2)<=1 or
1>=(-a) & 1<=-(((-a)*p`2)/p`2) by A94,A103,XCMPLX_1:90,188;
hence 1<=a & -a<=1 or 1>=a & 1<=-a by A104;
case p`2<0;
then p`2/p`2>= (-a)*p`2/p`2 & (-((-a)*p`2))/p`2>=p`2/p`2 or
p`2/p`2<=((-a)*p`2)/p`2 & p`2/p`2>=(-((-a)*p`2))/p`2
by A83,A102,REAL_1:74;
then A105:1>= (-a)*p`2/p`2 & (-((-a)*p`2))/p`2>=1 or
1<=((-a)*p`2)/p`2 & 1>=(-((-a)*p`2))/p`2 by A94,XCMPLX_1:60;
A106:((-a)*p`2)/p`2=(-a) by A94,XCMPLX_1:90;
1>= -a & -(((-a)*p`2)/p`2)>=1 or
1<=-a & 1>=-(((-a)*p`2)/p`2) by A94,A105,XCMPLX_1:90,188;
hence 1<=a & -a<=1 or 1>=a & 1<=-a by A106;
end;
then 1<=a & -a<=1 or 1>=a & -1>=--a by REAL_1:50;
hence 1<=a or -1>=a;
end;
A107:q`2*a<=q`2 & -q`2<=q`2*a or q`2*a>=q`2 & q`2*a<=-q`2
by A79,A92,XCMPLX_1:88;
A108:now per cases by A92;
case A109:q`2>0;
then A110:a*q`2/q`2<=q`2/q`2 & (-q`2)/q`2<=a*q`2/q`2
or a*q`2/q`2>=q`2/q`2 & a*q`2/q`2<=(-q`2)/q`2 by A107,REAL_1:73;
A111:q`2/q`2=1 by A109,XCMPLX_1:60;
(-q`2)/q`2=-1 by A109,XCMPLX_1:198;
hence a<=1 & -1<=a or a>=1 & a<=-1 by A109,A110,A111,XCMPLX_1:90;
case A112:q`2<0;
then a*q`2/q`2>=q`2/q`2 & (-q`2)/q`2>=a*q`2/q`2
or a*q`2/q`2<=q`2/q`2 & a*q`2/q`2>=(-q`2)/q`2 by A107,REAL_1:74;
then a>=q`2/q`2 & (-q`2)/q`2>=a
or a<=q`2/q`2 & a>=(-q`2)/q`2 by A112,XCMPLX_1:90;
hence a<=1 & -1<=a or a>=1 & a<=-1 by A112,XCMPLX_1:60,198;
end;
A113: now per cases by A98,A108,AXIOMS:21,22;
case a=1;
then (p`1)^2/(p`2)^2=1 by A96,SQUARE_1:59,69;
then A114:(p`1)^2=(p`2)^2 by XCMPLX_1:58;
(p`2/p`1)^2=(p`2)^2/(p`1)^2 by SQUARE_1:69;
hence (p`2/p`1)^2=(q`1/q`2)^2 by A96,A114,SQUARE_1:69;
case a=-1; then a^2=1 by SQUARE_1:59,61;
then (p`1)^2/(p`2)^2=1 by A96,SQUARE_1:69;
then A115:(p`1)^2=(p`2)^2 by XCMPLX_1:58;
(p`2/p`1)^2=(p`2)^2/(p`1)^2 by SQUARE_1:69;
hence (p`2/p`1)^2=(q`1/q`2)^2 by A96,A115,SQUARE_1:69;
end;
then p`2=q`2/sqrt(1+(q`1/q`2)^2)*sqrt(1+(q`1/q`2)^2)
by A84,A86,XCMPLX_1:88;
then A116:p`2=q`2 by A78,XCMPLX_1:88;
p`1=q`1/sqrt(1+(q`1/q`2)^2)*sqrt(1+(q`1/q`2)^2)
by A84,A86,A113,XCMPLX_1:88;
then p`1=q`1 by A78,XCMPLX_1:88;
then p=|[q`1,q`2]|by A116,EUCLID:57;
hence x1=x2 by EUCLID:57;
end;
hence x1=x2;
case A117:p<>0.REAL 2 &
not (p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1);
then A118: (p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) by JGRAPH_2:
23;
A119:Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|
by A117,Def1;
then A120:p`2/sqrt(1+(p`1/p`2)^2)=q`2/sqrt(1+(q`1/q`2)^2) &
p`1/sqrt(1+(p`1/p`2)^2)=q`1/sqrt(1+(q`1/q`2)^2)
by A1,A75,A76,EUCLID:56;
A121:1+(p`1/p`2)^2>0 by Lm1;
then A122:sqrt(1+(p`1/p`2)^2)>0 by SQUARE_1:93;
(p`2)^2/(sqrt(1+(p`1/p`2)^2))^2=(q`2/sqrt(1+(q`1/q`2)^2))^2
by A120,SQUARE_1:69;
then (p`2)^2/(sqrt(1+(p`1/p`2)^2))^2=(q`2)^2/(sqrt(1+(q`1/q`2)^2))^2
by SQUARE_1:69;
then (p`2)^2/(1+(p`1/p`2)^2)=(q`2)^2/(sqrt(1+(q`1/q`2)^2))^2
by A121,SQUARE_1:def 4;
then A123:(p`2)^2/(1+(p`1/p`2)^2)=(q`2)^2/(1+(q`1/q`2)^2)
by A77,SQUARE_1:def 4;
(p`1)^2/(sqrt(1+(p`1/p`2)^2))^2=(q`1/sqrt(1+(q`1/q`2)^2))^2
by A120,SQUARE_1:69;
then (p`1)^2/(sqrt(1+(p`1/p`2)^2))^2=(q`1)^2/(sqrt(1+(q`1/q`2)^2))^2
by SQUARE_1:69;
then (p`1)^2/(1+(p`1/p`2)^2)=(q`1)^2/(sqrt(1+(q`1/q`2)^2))^2
by A121,SQUARE_1:def 4;
then A124:(p`1)^2/(1+(p`1/p`2)^2)=(q`1)^2/(1+(q`1/q`2)^2)
by A77,SQUARE_1:def 4;
p`2<>0 by A117,A118;
then A125:(p`2)^2>0 by SQUARE_1:74;
(p`2)^2/(1+(p`1/p`2)^2)/(p`2)^2=(q`2)^2/(p`2)^2/(1+(q`1/q`2)^2)
by A123,XCMPLX_1:48;
then (p`2)^2/(p`2)^2/(1+(p`1/p`2)^2)=(q`2)^2/(p`2)^2/(1+(q`1/q`2)^2)
by XCMPLX_1:48;
then 1/(1+(p`1/p`2)^2)=(q`2)^2/(p`2)^2/(1+(q`1/q`2)^2)
by A125,XCMPLX_1:60;
then A126:1/(1+(p`1/p`2)^2)*(1+(q`1/q`2)^2)=(q`2)^2/(p`2)^2
by A77,XCMPLX_1:88;
q`2<>0 by A74,A79;
then A127:(q`2)^2>0 by SQUARE_1:74;
now per cases;
case A128:p`1=0;
then (q`1)^2=0 by A77,A124,SQUARE_1:60,XCMPLX_1:50;
then A129:q`1=0 by SQUARE_1:73;
then p=|[0,q`2]|by A1,A75,A119,A128,EUCLID:57,SQUARE_1:60,83;
hence x1=x2 by A129,EUCLID:57;
case p`1<>0;
then A130:(p`1)^2>0 by SQUARE_1:74;
(p`1)^2/(1+(p`1/p`2)^2)/(p`1)^2=(q`1)^2/(p`1)^2/(1+(q`1/q`2)^2)
by A124,XCMPLX_1:48;
then (p`1)^2/(p`1)^2/(1+(p`1/p`2)^2)=(q`1)^2/(p`1)^2/(1+(q`1/q`2)^2)
by XCMPLX_1:48;
then 1/(1+(p`1/p`2)^2)=(q`1)^2/(p`1)^2/(1+(q`1/q`2)^2)
by A130,XCMPLX_1:60;
then 1/(1+(p`1/p`2)^2)*(1+(q`1/q`2)^2)=(q`1)^2/(p`1)^2
by A77,XCMPLX_1:88;
then (q`2)^2/(q`2)^2/(p`2)^2=(q`1)^2/(p`1)^2/(q`2)^2
by A126,XCMPLX_1:48;
then 1/(p`2)^2=(q`1)^2/(p`1)^2/(q`2)^2 by A127,XCMPLX_1:60;
then 1/(p`2)^2*(p`1)^2=(p`1)^2*((q`1)^2/(p`1)^2)/(q`2)^2
by XCMPLX_1:75;
then 1/(p`2)^2*(p`1)^2=(q`1)^2/(q`2)^2 by A130,XCMPLX_1:88;
then (p`1)^2/(p`2)^2=(q`1)^2/(q`2)^2 by XCMPLX_1:100;
then (p`1/p`2)^2=(q`1)^2/(q`2)^2 by SQUARE_1:69;
then A131:(1+(p`1/p`2)^2)=(1+(q`1/q`2)^2) by SQUARE_1:69;
then p`2=q`2/sqrt(1+(q`1/q`2)^2)*sqrt(1+(q`1/q`2)^2)
by A120,A122,XCMPLX_1:88;
then A132:p`2=q`2 by A78,XCMPLX_1:88;
p`1=q`1/sqrt(1+(q`1/q`2)^2)*sqrt(1+(q`1/q`2)^2)
by A120,A122,A131,XCMPLX_1:88;
then p`1=q`1 by A78,XCMPLX_1:88;
then p=|[q`1,q`2]|by A132,EUCLID:57;
hence x1=x2 by EUCLID:57;
end;
hence x1=x2;
end;
hence x1=x2;
end;
definition
cluster Sq_Circ -> one-to-one;
coherence by Th32;
end;
theorem Th33: for Kb,Cb being Subset of TOP-REAL 2 st
Kb={q: -1=q`1 & -1<=q`2 & q`2<=1 or q`1=1 & -1<=q`2 & q`2<=1
or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1<=q`1 & q`1<=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={q: -1=q`1 & -1<=q`2 & q`2<=1 or q`1=1 & -1<=q`2 & q`2<=1
or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1<=q`1 & q`1<=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 & -1<=q`2 & q`2<=1 or q`1=1 & -1<=q`2 & q`2<=1
or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1<=q`1 & q`1<=1)
by A1,A2;
now per cases;
case q=0.REAL 2;
hence contradiction by A3,JGRAPH_2:11;
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 Def1;
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) &
(|[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;
A7:1+(q`2)^2>0 by Lm1;
now per cases by A3;
case -1=q`1 & -1<=q`2 & q`2<=1;
then A8: |.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|^2
=((-1)/sqrt(1+(q`2/(-1))^2))^2+(q`2/sqrt(1+(q`2/(-1))^2))^2
by A6,JGRAPH_1:46
.=(-1)^2/(sqrt(1+(q`2/(-1))^2))^2+(q`2/sqrt(1+(q`2/(-1))^2))^2
by SQUARE_1:69
.=(-1)^2/(sqrt(1+(q`2/(-1))^2))^2+(q`2)^2/(sqrt(1+(q`2/(-1))^2))^2
by SQUARE_1:69
.=1/(sqrt(1+(q`2/(-1))^2))^2+(q`2)^2/(sqrt(1+(q`2/(-1))^2))^2
by SQUARE_1:59,61
.=1/(sqrt(1+(-q`2)^2))^2+(q`2)^2/(sqrt(1+(q`2/(-1))^2))^2
by XCMPLX_1:194
.=1/(sqrt(1+(-q`2)^2))^2+(q`2)^2/(sqrt(1+(-q`2)^2))^2 by XCMPLX_1:194
.=1/(sqrt(1+(q`2)^2))^2+(q`2)^2/(sqrt(1+(-q`2)^2))^2 by SQUARE_1:61
.=1/(sqrt(1+(q`2)^2))^2+(q`2)^2/(sqrt(1+(q`2)^2))^2 by SQUARE_1:61
.=1/(1+(q`2)^2)+(q`2)^2/(sqrt(1+(q`2)^2))^2 by A7,SQUARE_1:def 4
.=1/(1+(q`2)^2)+(q`2)^2/(1+(q`2)^2) by A7,SQUARE_1:def 4
.=(1+(q`2)^2)/(1+(q`2)^2) by XCMPLX_1:63
.=1 by A7,XCMPLX_1:60;
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 A8,SQUARE_1:83,89;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|=1
by A2,A3,A5;
case q`1=1 & -1<=q`2 & q`2<=1;
then A9: |.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|^2
=(1/sqrt(1+(q`2/(1))^2))^2+(q`2/sqrt(1+(q`2/(1))^2))^2
by A6,JGRAPH_1:46
.=1^2/(sqrt(1+(q`2/(1))^2))^2+(q`2/sqrt(1+(q`2/(1))^2))^2
by SQUARE_1:69
.=1/(sqrt(1+(q`2/(1))^2))^2+(q`2)^2/(sqrt(1+(q`2/(1))^2))^2
by SQUARE_1:59,69
.=1/(1+(q`2)^2)+(q`2)^2/(sqrt(1+(q`2)^2))^2
by A7,SQUARE_1:def 4
.=1/(1+(q`2)^2)+(q`2)^2/(1+(q`2)^2) by A7,SQUARE_1:def 4
.=(1+(q`2)^2)/(1+(q`2)^2) by XCMPLX_1:63
.=1 by A7,XCMPLX_1:60;
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 A9,SQUARE_1:83,89;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|=1
by A2,A3,A5;
case A10: -1=q`2 & -1<=q`1 & q`1<=1;
then (-1<=q`1 & q`1>=1 or -1>=q`1 & 1>=q`1) by A4,REAL_1:50;
then q`1=1 or q`1=-1 by A10,AXIOMS:21;
then A11:(q`1)^2=1 by SQUARE_1:59,61;
A12: |.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|^2
=((q`1)/sqrt(1+((-1)/(q`1))^2))^2+((-1)/sqrt(1+((-1)/(q`1))^2))^2
by A6,A10,JGRAPH_1:46
.=((q`1)/sqrt(1+((-1)/(q`1))^2))^2+(-1)^2/(sqrt(1+((-1)/(q`1))^2))^2
by SQUARE_1:69
.=(q`1)^2/(sqrt(1+((-1)/(q`1))^2))^2+(-1)^2/(sqrt(1+((-1)/(q`1))^2))^2
by SQUARE_1:69
.=(q`1)^2/(sqrt(1+((-1)/(q`1))^2))^2+1/(sqrt(1+((-1)/(q`1))^2))^2
by SQUARE_1:59,61
.=(q`1)^2/(sqrt(1+(-1)^2/(q`1)^2))^2+1/(sqrt(1+((-1)/(q`1))^2))^2
by SQUARE_1:69
.=(q`1)^2/(sqrt(1+(-1)^2/(q`1)^2))^2+1/(sqrt(1+(-1)^2/(q`1)^2))^2
by SQUARE_1:69
.=(q`1)^2/(sqrt(1+(1)^2/(q`1)^2))^2+1/(sqrt(1+(-1)^2/(q`1)^2))^2
by SQUARE_1:61
.=1/(sqrt(1+1/1))^2+1/(sqrt(1+1/1))^2 by A11,SQUARE_1:59,61
.=1/2+1/(sqrt(2))^2 by SQUARE_1:def 4
.=1/2+1/2 by SQUARE_1:def 4
.=1;
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 A12,SQUARE_1:83,89;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|=1
by A2,A3,A5;
case A13: 1=q`2 & -1<=q`1 & q`1<=1;
then (1<=q`1 & q`1>=-1 or 1>=q`1 & -1>=q`1) by A4,REAL_2:109;
then q`1=1 or q`1=-1 by A13,AXIOMS:21;
then A14:(q`1)^2=1 by SQUARE_1:59,61;
A15: |.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|^2
=((q`1)/sqrt(1+((1)/(q`1))^2))^2+((1)/sqrt(1+((1)/(q`1))^2))^2
by A6,A13,JGRAPH_1:46
.=((q`1)/sqrt(1+((1)/(q`1))^2))^2+(1)^2/(sqrt(1+((1)/(q`1))^2))^2
by SQUARE_1:69
.=(q`1)^2/(sqrt(1+((1)/(q`1))^2))^2+1/(sqrt(1+((1)/(q`1))^2))^2
by SQUARE_1:59,69
.=(q`1)^2/(sqrt(1+(1)^2/(q`1)^2))^2+1/(sqrt(1+((1)/(q`1))^2))^2
by SQUARE_1:69
.=1/(sqrt(1+1/1))^2+1/(sqrt(1+1/1))^2 by A14,SQUARE_1:59,69
.=1/2+1/(sqrt(2))^2 by SQUARE_1:def 4
.=1/2+1/2 by SQUARE_1:def 4
.=1;
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,SQUARE_1:83,89;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|=1
by A2,A3,A5;
end;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|=1;
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 Def1;
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;
A19:1+(q`1)^2>0 by Lm1;
now per cases by A3;
case -1=q`2 & -1<=q`1 & q`1<=1;
then A20: |.(|[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/(-1))^2))^2+((-1)/sqrt(1+(q`1/(-1))^2))^2
by A18,JGRAPH_1:46
.=(-1)^2/(sqrt(1+(q`1/(-1))^2))^2+(q`1/sqrt(1+(q`1/(-1))^2))^2
by SQUARE_1:69
.=(-1)^2/(sqrt(1+(q`1/(-1))^2))^2+(q`1)^2/(sqrt(1+(q`1/(-1))^2))^2
by SQUARE_1:69
.=1/(sqrt(1+(q`1/(-1))^2))^2+(q`1)^2/(sqrt(1+(q`1/(-1))^2))^2
by SQUARE_1:59,61
.=1/(sqrt(1+(-q`1)^2))^2+(q`1)^2/(sqrt(1+(q`1/(-1))^2))^2
by XCMPLX_1:194
.=1/(sqrt(1+(-q`1)^2))^2+(q`1)^2/(sqrt(1+(-q`1)^2))^2 by XCMPLX_1:194
.=1/(sqrt(1+(q`1)^2))^2+(q`1)^2/(sqrt(1+(-q`1)^2))^2 by SQUARE_1:61
.=1/(sqrt(1+(q`1)^2))^2+(q`1)^2/(sqrt(1+(q`1)^2))^2 by SQUARE_1:61
.=1/(1+(q`1)^2)+(q`1)^2/(sqrt(1+(q`1)^2))^2 by A19,SQUARE_1:def 4
.=1/(1+(q`1)^2)+(q`1)^2/(1+(q`1)^2) by A19,SQUARE_1:def 4
.=(1+(q`1)^2)/(1+(q`1)^2) by XCMPLX_1:63
.=1 by A19,XCMPLX_1:60;
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 A20,SQUARE_1:83,89;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|=1
by A2,A3,A17;
case q`2=1 & -1<=q`1 & q`1<=1;