-p`1 by XREAL_1:24;
assume
A2: p<>0.TOP-REAL 2;
hereby
assume
A3: p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2;
now
per cases by A3;
case
A4: p`1<=p`2 & -p`2<=p`1;
now
assume
A5: p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1;
A6: now
per cases by A5;
case
p`2<=p`1 & -p`1<=p`2;
hence p`1=p`2 or p`1=-p`2 by A4,XXREAL_0:1;
end;
case
p`2>=p`1 & p`2<=-p`1;
then -p`2>=--p`1 by XREAL_1:24;
hence p`1=p`2 or p`1=-p`2 by A4,XXREAL_0:1;
end;
end;
now
per cases by A6;
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 A2,A5,Def1;
end;
case
A7: p`1=-p`2;
then p`1<>0 & -p`1=p`2 by A2,EUCLID:53,54;
then
A8: p`2/p`1=-1 by XCMPLX_1:197;
p`2<>0 by A2,A7,EUCLID:53,54;
then p`1/p`2=-1 by A7,XCMPLX_1:197;
hence
Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)
]| by A2,A5,A8,Def1;
end;
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
A2,Def1;
end;
case
A9: p`1>=p`2 & p`1<=-p`2;
now
assume
A10: p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1;
A11: now
per cases by A10;
case
p`2<=p`1 & -p`1<=p`2;
then --p`1>=-p`2 by XREAL_1:24;
hence p`1=p`2 or p`1=-p`2 by A9,XXREAL_0:1;
end;
case
p`2>=p`1 & p`2<=-p`1;
hence p`1=p`2 or p`1=-p`2 by A9,XXREAL_0:1;
end;
end;
now
per cases by A11;
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 A2,A10,Def1;
end;
case
A12: p`1=-p`2;
then p`1<>0 & -p`1=p`2 by A2,EUCLID:53,54;
then
A13: p`2/p`1=-1 by XCMPLX_1:197;
p`2<>0 by A2,A12,EUCLID:53,54;
then p`1/p`2=-1 by A12,XCMPLX_1:197;
hence
Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)
]| by A2,A10,A13,Def1;
end;
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
A2,Def1;
end;
end;
hence Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|;
end;
A14: -p`2>p`1 implies --p`2<-p`1 by XREAL_1:24;
assume not(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2);
hence thesis by A2,A1,A14,Def1;
end;
theorem Th5:
for X being non empty TopSpace, f1 being Function of X,R^1 st f1
is continuous & (for q being Point of X ex r being Real st f1.q=r & r>=0
) holds ex g being Function of X,R^1 st (for p being Point of X,r1 being Real
st f1.p=r1 holds g.p=sqrt(r1)) & g is continuous
proof
let X being non empty TopSpace,f1 be Function of X,R^1;
assume that
A1: f1 is continuous and
A2: for q being Point of X ex r being Real st f1.q=r & r>=0;
defpred P[set,set] means (for r11 being Real st f1.$1=r11 holds $2=
sqrt(r11));
A3: for x being Element of X ex y being Element of REAL st P[x,y]
proof
let x be Element of X;
reconsider r1=f1.x as Element of REAL by TOPMETR:17;
reconsider y = sqrt(r1) as Element of REAL by XREAL_0:def 1;
take y;
thus 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 FUNCT_2:sch 3(A3);
then consider f being Function of the carrier of X,REAL such that
A4: for x2 being Element of X holds for r11 being Real st f1.x2=
r11 holds f.x2=sqrt(r11);
reconsider g0=f as Function of X,R^1 by TOPMETR:17;
for p being Point of X,V being Subset of R^1 st g0.p in V & V is open
holds ex W being Subset of X st p in W & W is open & g0.:W c= V
proof
let p be Point of X,V be Subset of R^1;
reconsider r=g0.p as Real;
reconsider r1=f1.p as Real;
assume g0.p in V & V is open;
then consider r01 being Real such that
A5: r01>0 and
A6: ].r-r01,r+r01.[ c= V by FRECHET:8;
set r0=min(r01,1);
A7: r0>0 by A5,XXREAL_0:21;
A8: r0>0 by A5,XXREAL_0:21;
r0<=r01 by XXREAL_0:17;
then r-r01<=r-r0 & r+r0<=r+r01 by XREAL_1:6,10;
then ].r-r0,r+r0.[ c= ].r-r01,r+r01.[ by XXREAL_1:46;
then
A9: ].r-r0,r+r0.[ c= V by A6;
A10: ex r8 being Real st f1.p=r8 & r8>=0 by A2;
A11: r=sqrt(r1) by A4;
then
A12: r1=r^2 by A10,SQUARE_1:def 2;
A13: r>=0 by A10,A11,SQUARE_1:17,26;
then
A14: 2*r*r0+r0^2>0+0 by A8,SQUARE_1:12,XREAL_1:8;
per cases;
suppose
A15: r-r0>0;
set r4=r0*(r-r0);
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1 by TOPMETR:17;
A16: r1 -p`1 by XREAL_1:24;
assume
A2: p<>0.TOP-REAL 2;
hereby
assume
A3: p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2;
now
per cases by A3;
case
A4: p`1<=p`2 & -p`2<=p`1;
now
assume
A5: p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1;
A6: now
per cases by A5;
case
p`2<=p`1 & -p`1<=p`2;
hence p`1=p`2 or p`1=-p`2 by A4,XXREAL_0:1;
end;
case
p`2>=p`1 & p`2<=-p`1;
then -p`2>=--p`1 by XREAL_1:24;
hence p`1=p`2 or p`1=-p`2 by A4,XXREAL_0:1;
end;
end;
now
per cases by A6;
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 A2,A5,Th28;
end;
case
p`1=-p`2;
then p`1<>0 & -p`1=p`2 by A2,EUCLID:53,54;
then p`1/p`2=-1 & p`2/p`1=-1 by XCMPLX_1:197,198;
hence
(Sq_Circ").p=|[p`1*sqrt(1+(p`1/p`2)^2),p`2*sqrt(1+(p`1/p`2)
^2) ]| by A2,A5,Th28;
end;
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 Th28;
end;
case
A7: p`1>=p`2 & p`1<=-p`2;
now
assume
A8: p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1;
A9: now
per cases by A8;
case
p`2<=p`1 & -p`1<=p`2;
then --p`1>=-p`2 by XREAL_1:24;
hence p`1=p`2 or p`1=-p`2 by A7,XXREAL_0:1;
end;
case
p`2>=p`1 & p`2<=-p`1;
hence p`1=p`2 or p`1=-p`2 by A7,XXREAL_0:1;
end;
end;
now
per cases by A9;
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 A2,A8,Th28;
end;
case
A10: p`1=-p`2;
then p`1<>0 & -p`1=p`2 by A2,EUCLID:53,54;
then
A11: p`2/p`1=-1 by XCMPLX_1:197;
p`2<>0 by A2,A10,EUCLID:53,54;
then p`1/p`2=-1 by A10,XCMPLX_1:197;
hence
(Sq_Circ").p=|[p`1*sqrt(1+(p`1/p`2)^2),p`2*sqrt(1+(p`1/p`2)
^2) ]| by A2,A8,A11,Th28;
end;
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 Th28;
end;
end;
hence (Sq_Circ").p=|[p`1*sqrt(1+(p`1/p`2)^2),p`2*sqrt(1+(p`1/p`2)^2)]|;
end;
A12: -p`2>p`1 implies --p`2<-p`1 by XREAL_1:24;
assume not(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2);
hence thesis by A2,A1,A12,Th28;
end;
theorem Th31:
for X being non empty TopSpace, f1,f2 being Function of X,R^1 st
f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0)
holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real
st f1.p=r1 & f2.p=r2 holds g.p=r1*sqrt(1+(r1/r2)^2)) & g is continuous
proof
let X be non empty TopSpace, f1,f2 be Function of X,R^1;
assume that
A1: f1 is continuous and
A2: f2 is continuous & for q being Point of X holds f2.q<>0;
consider g2 being Function of X,R^1 such that
A3: for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2
holds g2.p=sqrt(1+(r1/r2)^2) and
A4: g2 is continuous by A1,A2,Th8;
consider g3 being Function of X,R^1 such that
A5: for p being Point of X,r1,r0 being Real st f1.p=r1 & g2.p=r0
holds g3.p=r1*r0 and
A6: g3 is continuous by A1,A4,JGRAPH_2:25;
for p being Point of X,r1,r2 being Real 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;
assume that
A7: f1.p=r1 and
A8: f2.p=r2;
g2.p=sqrt(1+(r1/r2)^2) by A3,A7,A8;
hence thesis by A5,A7;
end;
hence thesis by A6;
end;
theorem Th32:
for X being non empty TopSpace, f1,f2 being Function of X,R^1 st
f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0) ex
g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st
f1.p=r1 & f2.p=r2 holds g.p=r2*sqrt(1+(r1/r2)^2)) & g is continuous
proof
let X be non empty TopSpace, f1,f2 be Function of X,R^1;
assume that
A1: f1 is continuous and
A2: f2 is continuous and
A3: for q being Point of X holds f2.q<>0;
consider g2 being Function of X,R^1 such that
A4: for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2
holds g2.p=sqrt(1+(r1/r2)^2) and
A5: g2 is continuous by A1,A2,A3,Th8;
consider g3 being Function of X,R^1 such that
A6: for p being Point of X,r2,r0 being Real st f2.p=r2 & g2.p=r0
holds g3.p=r2*r0 and
A7: g3 is continuous by A2,A5,JGRAPH_2:25;
for p being Point of X,r1,r2 being Real 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;
assume that
A8: f1.p=r1 and
A9: f2.p=r2;
g2.p=sqrt(1+(r1/r2)^2) by A4,A8,A9;
hence thesis by A6,A9;
end;
hence thesis by A7;
end;
theorem Th33:
for K1 being non empty Subset of TOP-REAL 2, f being Function of
(TOP-REAL 2)|K1,R^1 st (for p being Point of TOP-REAL 2 st p in the carrier of
(TOP-REAL 2)|K1 holds f.p=p`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 Function of (TOP-REAL 2)|K1,
R^1;
reconsider g1=proj1|K1 as continuous Function of (TOP-REAL 2)|K1,R^1 by Lm7;
reconsider g2=proj2|K1 as continuous Function of (TOP-REAL 2)|K1,R^1 by Lm5;
assume that
A1: for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|
K1 holds f.p=p`1*sqrt(1+(p`2/p`1)^2) and
A2: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)
|K1 holds q`1<>0;
A3: the carrier of (TOP-REAL 2)|K1=K1 by PRE_TOPC:8;
for q being Point of (TOP-REAL 2)|K1 holds g1.q<>0
proof
let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1;
then reconsider q2=q as Point of TOP-REAL 2 by A3;
g1.q=proj1.q by Lm6
.=q2`1 by PSCOMP_1:def 5;
hence thesis by A2;
end;
then consider g3 being Function of (TOP-REAL 2)|K1,R^1 such that
A4: for q being Point of (TOP-REAL 2)|K1,r1,r2 being Real st g2.q
=r1 & g1.q=r2 holds g3.q=r2*sqrt(1+(r1/r2)^2) and
A5: g3 is continuous by Th32;
A6: now
let x be object;
assume
A7: x in dom f;
then reconsider s=x as Point of (TOP-REAL 2)|K1;
x in the carrier of (TOP-REAL 2)|K1 by A7;
then x in K1 by PRE_TOPC:8;
then reconsider r=x as Point of (TOP-REAL 2);
A8: proj2.r=r`2 & proj1.r=r`1 by PSCOMP_1:def 5,def 6;
A9: g2.s=proj2.s & g1.s=proj1.s by Lm4,Lm6;
f.r=r`1*sqrt(1+(r`2/r`1)^2) by A1,A7;
hence f.x=g3.x by A4,A9,A8;
end;
dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then dom f=dom g3 by FUNCT_2:def 1;
hence thesis by A5,A6,FUNCT_1:2;
end;
theorem Th34:
for K1 being non empty Subset of TOP-REAL 2, f being Function of
(TOP-REAL 2)|K1,R^1 st (for p being Point of TOP-REAL 2 st p in the carrier of
(TOP-REAL 2)|K1 holds f.p=p`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 Function of (TOP-REAL 2)|K1,
R^1;
reconsider g1=proj1|K1 as continuous Function of (TOP-REAL 2)|K1,R^1 by Lm7;
reconsider g2=proj2|K1 as continuous Function of (TOP-REAL 2)|K1,R^1 by Lm5;
assume that
A1: for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|
K1 holds f.p=p`2*sqrt(1+(p`2/p`1)^2) and
A2: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)
|K1 holds q`1<>0;
A3: the carrier of (TOP-REAL 2)|K1=K1 by PRE_TOPC:8;
for q being Point of (TOP-REAL 2)|K1 holds g1.q<>0
proof
let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1;
then reconsider q2=q as Point of TOP-REAL 2 by A3;
g1.q=proj1.q by Lm6
.=q2`1 by PSCOMP_1:def 5;
hence thesis by A2;
end;
then consider g3 being Function of (TOP-REAL 2)|K1,R^1 such that
A4: for q being Point of (TOP-REAL 2)|K1,r1,r2 being Real st g2.q
=r1 & g1.q=r2 holds g3.q=r1*sqrt(1+(r1/r2)^2) and
A5: g3 is continuous by Th31;
A6: now
let x be object;
assume
A7: x in dom f;
then reconsider s=x as Point of (TOP-REAL 2)|K1;
x in the carrier of (TOP-REAL 2)|K1 by A7;
then x in K1 by PRE_TOPC:8;
then reconsider r=x as Point of (TOP-REAL 2);
A8: proj2.r=r`2 & proj1.r=r`1 by PSCOMP_1:def 5,def 6;
A9: g2.s=proj2.s & g1.s=proj1.s by Lm4,Lm6;
f.r=r`2*sqrt(1+(r`2/r`1)^2) by A1,A7;
hence f.x=g3.x by A4,A9,A8;
end;
dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then dom f=dom g3 by FUNCT_2:def 1;
hence thesis by A5,A6,FUNCT_1:2;
end;
theorem Th35:
for K1 being non empty Subset of TOP-REAL 2, f being Function of
(TOP-REAL 2)|K1,R^1 st (for p being Point of TOP-REAL 2 st p in the carrier of
(TOP-REAL 2)|K1 holds f.p=p`2*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 Function of (TOP-REAL 2)|K1,
R^1;
reconsider g1=proj1|K1 as continuous Function of (TOP-REAL 2)|K1,R^1 by Lm7;
reconsider g2=proj2|K1 as continuous Function of (TOP-REAL 2)|K1,R^1 by Lm5;
assume that
A1: for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|
K1 holds f.p=p`2*sqrt(1+(p`1/p`2)^2) and
A2: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)
|K1 holds q`2<>0;
A3: the carrier of (TOP-REAL 2)|K1=K1 by PRE_TOPC:8;
for q being Point of (TOP-REAL 2)|K1 holds g2.q<>0
proof
let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1;
then reconsider q2=q as Point of TOP-REAL 2 by A3;
g2.q=proj2.q by Lm4
.=q2`2 by PSCOMP_1:def 6;
hence thesis by A2;
end;
then consider g3 being Function of (TOP-REAL 2)|K1,R^1 such that
A4: for q being Point of (TOP-REAL 2)|K1,r1,r2 being Real st g1.q
=r1 & g2.q=r2 holds g3.q=r2*sqrt(1+(r1/r2)^2) and
A5: g3 is continuous by Th32;
A6: now
let x be object;
assume
A7: x in dom f;
then reconsider s=x as Point of (TOP-REAL 2)|K1;
x in the carrier of (TOP-REAL 2)|K1 by A7;
then x in K1 by PRE_TOPC:8;
then reconsider r=x as Point of (TOP-REAL 2);
A8: proj2.r=r`2 & proj1.r=r`1 by PSCOMP_1:def 5,def 6;
A9: g2.s=proj2.s & g1.s=proj1.s by Lm4,Lm6;
f.r=r`2*sqrt(1+(r`1/r`2)^2) by A1,A7;
hence f.x=g3.x by A4,A9,A8;
end;
dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then dom f=dom g3 by FUNCT_2:def 1;
hence thesis by A5,A6,FUNCT_1:2;
end;
theorem Th36:
for K1 being non empty Subset of TOP-REAL 2, f being Function of
(TOP-REAL 2)|K1,R^1 st (for p being Point of TOP-REAL 2 st p in the carrier of
(TOP-REAL 2)|K1 holds f.p=p`1*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 Function of (TOP-REAL 2)|K1,
R^1;
reconsider g1=proj1|K1 as continuous Function of (TOP-REAL 2)|K1,R^1 by Lm7;
reconsider g2=proj2|K1 as continuous Function of (TOP-REAL 2)|K1,R^1 by Lm5;
assume that
A1: for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|
K1 holds f.p=p`1*sqrt(1+(p`1/p`2)^2) and
A2: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)
|K1 holds q`2<>0;
A3: the carrier of (TOP-REAL 2)|K1=K1 by PRE_TOPC:8;
for q being Point of (TOP-REAL 2)|K1 holds g2.q<>0
proof
let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1;
then reconsider q2=q as Point of TOP-REAL 2 by A3;
g2.q=proj2.q by Lm4
.=q2`2 by PSCOMP_1:def 6;
hence thesis by A2;
end;
then consider g3 being Function of (TOP-REAL 2)|K1,R^1 such that
A4: for q being Point of (TOP-REAL 2)|K1,r1,r2 being Real st g1.q
=r1 & g2.q=r2 holds g3.q=r1*sqrt(1+(r1/r2)^2) and
A5: g3 is continuous by Th31;
A6: now
let x be object;
assume
A7: x in dom f;
then reconsider s=x as Point of (TOP-REAL 2)|K1;
x in the carrier of (TOP-REAL 2)|K1 by A7;
then x in K1 by PRE_TOPC:8;
then reconsider r=x as Point of (TOP-REAL 2);
A8: proj2.r=r`2 & proj1.r=r`1 by PSCOMP_1:def 5,def 6;
A9: g2.s=proj2.s & g1.s=proj1.s by Lm4,Lm6;
f.r=r`1*sqrt(1+(r`1/r`2)^2) by A1,A7;
hence f.x=g3.x by A4,A9,A8;
end;
dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then dom f=dom g3 by FUNCT_2:def 1;
hence thesis by A5,A6,FUNCT_1:2;
end;
Lm17: for K1 being non empty Subset of TOP-REAL 2 holds (proj2)*((Sq_Circ")|K1
) is Function of (TOP-REAL 2)|K1,R^1
proof
let K1 be non empty Subset of TOP-REAL 2;
A1: rng ((proj2)*((Sq_Circ")|K1)) c= rng (proj2) by RELAT_1:26;
A2: dom ((Sq_Circ")|K1) c= dom ((proj2)*((Sq_Circ")|K1))
proof
let x be object;
A3: rng (Sq_Circ") c= the carrier of TOP-REAL 2 by Th29,RELAT_1:def 19;
assume
A4: x in dom ((Sq_Circ")|K1);
then x in dom (Sq_Circ") /\ K1 by RELAT_1:61;
then x in dom (Sq_Circ") by XBOOLE_0:def 4;
then
A5: (Sq_Circ").x in rng (Sq_Circ") by FUNCT_1:3;
((Sq_Circ")|K1).x=(Sq_Circ").x by A4,FUNCT_1:47;
hence thesis by A4,A5,A3,Lm3,FUNCT_1:11;
end;
dom ((proj2)*((Sq_Circ")|K1)) c= dom ((Sq_Circ")|K1) by RELAT_1:25;
then dom ((proj2)*((Sq_Circ")|K1))=dom ((Sq_Circ")|K1) by A2
.=dom (Sq_Circ") /\ K1 by RELAT_1:61
.=(the carrier of TOP-REAL 2)/\ K1 by Th29,FUNCT_2:def 1
.=K1 by XBOOLE_1:28
.=the carrier of (TOP-REAL 2)|K1 by PRE_TOPC:8;
hence thesis by A1,FUNCT_2:2,TOPMETR:17,XBOOLE_1:1;
end;
Lm18: for K1 being non empty Subset of TOP-REAL 2 holds (proj1)*((Sq_Circ")|K1
) is Function of (TOP-REAL 2)|K1,R^1
proof
let K1 be non empty Subset of TOP-REAL 2;
A1: rng ((proj1)*((Sq_Circ")|K1)) c= rng (proj1) by RELAT_1:26;
A2: dom ((Sq_Circ")|K1) c= dom ((proj1)*((Sq_Circ")|K1))
proof
let x be object;
A3: rng (Sq_Circ") c= the carrier of TOP-REAL 2 by Th29,RELAT_1:def 19;
assume
A4: x in dom ((Sq_Circ")|K1);
then x in dom (Sq_Circ") /\ K1 by RELAT_1:61;
then x in dom (Sq_Circ") by XBOOLE_0:def 4;
then
A5: (Sq_Circ").x in rng (Sq_Circ") by FUNCT_1:3;
((Sq_Circ")|K1).x=(Sq_Circ").x by A4,FUNCT_1:47;
hence thesis by A4,A5,A3,Lm2,FUNCT_1:11;
end;
dom ((proj1)*((Sq_Circ")|K1)) c= dom ((Sq_Circ")|K1) by RELAT_1:25;
then dom ((proj1)*((Sq_Circ")|K1)) =dom ((Sq_Circ")|K1) by A2
.=dom (Sq_Circ") /\ K1 by RELAT_1:61
.=((the carrier of TOP-REAL 2))/\ K1 by Th29,FUNCT_2:def 1
.=K1 by XBOOLE_1:28
.=the carrier of (TOP-REAL 2)|K1 by PRE_TOPC:8;
hence thesis by A1,FUNCT_2:2,TOPMETR:17,XBOOLE_1:1;
end;
theorem Th37:
for K0,B0 being Subset of TOP-REAL 2,f being Function of (
TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=(Sq_Circ")|K0 & B0=NonZero TOP-REAL 2 & K0=
{p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2} holds f is
continuous
proof
let K0,B0 be Subset of TOP-REAL 2,f be Function of (TOP-REAL 2)|K0,(TOP-REAL
2)|B0;
assume
A1: f=(Sq_Circ")|K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`2<=p`1 & -p`1<=p
`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2};
then 1.REAL 2 in K0 by Lm9,Lm10;
then reconsider K1=K0 as non empty Subset of TOP-REAL 2;
reconsider g1=(proj1)*((Sq_Circ")|K1) as Function of (TOP-REAL 2)|K1,R^1 by
Lm18;
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
A2: dom ((Sq_Circ")|K1)=dom (Sq_Circ") /\ K1 by RELAT_1:61
.=((the carrier of TOP-REAL 2))/\ K1 by Th29,FUNCT_2:def 1
.=K1 by XBOOLE_1:28;
let p be Point of TOP-REAL 2;
A3: the carrier of (TOP-REAL 2)|K1=K1 by PRE_TOPC:8;
assume
A4: p in the carrier of (TOP-REAL 2)|K1;
then ex p3 being Point of TOP-REAL 2 st p=p3 &( p3`2<=p3`1 & - p3`1<=p3`2
or p3`2>=p3`1 & p3`2<=-p3`1)& p3<>0.TOP-REAL 2 by A1,A3;
then
A5: (Sq_Circ").p=|[p`1*sqrt(1+(p`2/p`1)^2), p`2*sqrt(1+(p`2/p`1)^2)]| by Th28;
((Sq_Circ")|K1).p=(Sq_Circ").p by A4,A3,FUNCT_1:49;
then g1.p=(proj1).(|[p`1*sqrt(1+(p`2/p`1)^2), p`2*sqrt(1+(p`2/p`1)^2)]|)
by A4,A2,A3,A5,FUNCT_1:13
.=(|[p`1*sqrt(1+(p`2/p`1)^2), p`2*sqrt(1+(p`2/p`1)^2)]|)`1 by
PSCOMP_1:def 5
.=p`1*sqrt(1+(p`2/p`1)^2) by EUCLID:52;
hence thesis;
end;
then consider f1 being Function of (TOP-REAL 2)|K1,R^1 such that
A6: 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);
reconsider g2=(proj2)*((Sq_Circ")|K1) as Function of (TOP-REAL 2)|K1,R^1 by
Lm17;
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
A7: dom ((Sq_Circ")|K1)=dom (Sq_Circ") /\ K1 by RELAT_1:61
.=((the carrier of TOP-REAL 2))/\ K1 by Th29,FUNCT_2:def 1
.=K1 by XBOOLE_1:28;
let p be Point of TOP-REAL 2;
A8: the carrier of (TOP-REAL 2)|K1=K1 by PRE_TOPC:8;
assume
A9: p in the carrier of (TOP-REAL 2)|K1;
then ex p3 being Point of TOP-REAL 2 st p=p3 &( p3`2<=p3`1 & - p3`1<=p3`2
or p3`2>=p3`1 & p3`2<=-p3`1)& p3<>0.TOP-REAL 2 by A1,A8;
then
A10: (Sq_Circ").p =|[p`1*sqrt(1+(p`2/p`1)^2),p`2*sqrt(1+(p`2/p`1)^2)]| by Th28;
((Sq_Circ")|K1).p=(Sq_Circ").p by A9,A8,FUNCT_1:49;
then
g2.p=(proj2).(|[p`1*sqrt(1+(p`2/p`1)^2),p`2*sqrt(1+(p`2/p`1)^2)]|) by A9,A7
,A8,A10,FUNCT_1:13
.=(|[p`1*sqrt(1+(p`2/p`1)^2), p`2*sqrt(1+(p`2/p`1)^2)]|)`2 by
PSCOMP_1:def 6
.=p`2*sqrt(1+(p`2/p`1)^2) by EUCLID:52;
hence thesis;
end;
then consider f2 being Function of (TOP-REAL 2)|K1,R^1 such that
A11: 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);
A12: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1
holds q`1<>0
proof
let q be Point of TOP-REAL 2;
A13: the carrier of (TOP-REAL 2)|K1=K1 by PRE_TOPC:8;
assume q in the carrier of (TOP-REAL 2)|K1;
then
A14: ex p3 being Point of TOP-REAL 2 st q=p3 &( p3`2<=p3`1 & - p3`1<=p3`2 or
p3`2>=p3`1 & p3`2<=-p3`1)& p3<>0.TOP-REAL 2 by A1,A13;
now
assume
A15: q`1=0;
then q`2=0 by A14;
hence contradiction by A14,A15,EUCLID:53,54;
end;
hence thesis;
end;
then
A16: f1 is continuous by A6,Th33;
A17: now
let x,y,r,s be Real;
assume that
A18: |[x,y]| in K1 and
A19: r=f1.(|[x,y]|) & s=f2.(|[x,y]|);
set p99=|[x,y]|;
A20: ex p3 being Point of TOP-REAL 2 st p99=p3 &( p3`2<=p3`1 & -p3`1<=p3`2
or p3`2>=p3`1 & p3`2<=-p3`1)& p3<>0.TOP-REAL 2 by A1,A18;
A21: the carrier of (TOP-REAL 2)|K1=K1 by PRE_TOPC:8;
then
A22: f1.p99=p99`1*sqrt(1+(p99`2/p99`1)^2) by A6,A18;
((Sq_Circ")|K0).(|[x,y]|)=((Sq_Circ")).(|[x,y]|) by A18,FUNCT_1:49
.= |[p99`1*sqrt(1+(p99`2/p99`1)^2), p99`2*sqrt(1+(p99`2/p99`1)^2)]| by
A20,Th28
.=|[r,s]| by A11,A18,A19,A21,A22;
hence f.(|[x,y]|)=|[r,s]| by A1;
end;
f2 is continuous by A12,A11,Th34;
hence thesis by A1,A16,A17,Lm13,JGRAPH_2:35;
end;
theorem Th38:
for K0,B0 being Subset of TOP-REAL 2,f being Function of (
TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=(Sq_Circ")|K0 & B0=NonZero TOP-REAL 2 & K0=
{p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2} holds f is
continuous
proof
let K0,B0 be Subset of TOP-REAL 2,f be Function of (TOP-REAL 2)|K0,(TOP-REAL
2)|B0;
assume
A1: f=(Sq_Circ")|K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`1<=p`2 & -p`2<=p
`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2};
then 1.REAL 2 in K0 by Lm14,Lm15;
then reconsider K1=K0 as non empty Subset of TOP-REAL 2;
reconsider g1=(proj2)*((Sq_Circ")|K1) as Function of (TOP-REAL 2)|K1,R^1 by
Lm17;
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
A2: dom ((Sq_Circ")|K1)=dom (Sq_Circ") /\ K1 by RELAT_1:61
.=((the carrier of TOP-REAL 2))/\ K1 by Th29,FUNCT_2:def 1
.=K1 by XBOOLE_1:28;
let p be Point of TOP-REAL 2;
A3: the carrier of (TOP-REAL 2)|K1=K1 by PRE_TOPC:8;
assume
A4: p in the carrier of (TOP-REAL 2)|K1;
then ex p3 being Point of TOP-REAL 2 st p=p3 &( p3`1<=p3`2 & - p3`2<=p3`1
or p3`1>=p3`2 & p3`1<=-p3`2)& p3<>0.TOP-REAL 2 by A1,A3;
then
A5: (Sq_Circ").p=|[p`1*sqrt(1+(p`1/p`2)^2), p`2*sqrt(1+(p`1/p`2)^2)]| by Th30;
((Sq_Circ")|K1).p=(Sq_Circ").p by A4,A3,FUNCT_1:49;
then
g1.p=(proj2).(|[p`1*sqrt(1+(p`1/p`2)^2),p`2*sqrt(1+(p`1/p`2)^2)]|) by A4,A2
,A3,A5,FUNCT_1:13
.=(|[p`1*sqrt(1+(p`1/p`2)^2), p`2*sqrt(1+(p`1/p`2)^2)]|)`2 by
PSCOMP_1:def 6
.=p`2*sqrt(1+(p`1/p`2)^2) by EUCLID:52;
hence thesis;
end;
then consider f1 being Function of (TOP-REAL 2)|K1,R^1 such that
A6: 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);
reconsider g2=(proj1)*((Sq_Circ")|K1) as Function of (TOP-REAL 2)|K1,R^1 by
Lm18;
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
A7: dom ((Sq_Circ")|K1)=dom (Sq_Circ") /\ K1 by RELAT_1:61
.=((the carrier of TOP-REAL 2))/\ K1 by Th29,FUNCT_2:def 1
.=K1 by XBOOLE_1:28;
let p be Point of TOP-REAL 2;
A8: the carrier of (TOP-REAL 2)|K1=K1 by PRE_TOPC:8;
assume
A9: p in the carrier of (TOP-REAL 2)|K1;
then ex p3 being Point of TOP-REAL 2 st p=p3 &( p3`1<=p3`2 & - p3`2<=p3`1
or p3`1>=p3`2 & p3`1<=-p3`2)& p3<>0.TOP-REAL 2 by A1,A8;
then
A10: (Sq_Circ").p=|[p`1*sqrt(1+(p`1/p`2)^2), p`2*sqrt(1+(p`1/p`2)^2)]| by Th30;
((Sq_Circ")|K1).p=(Sq_Circ").p by A9,A8,FUNCT_1:49;
then
g2.p=(proj1).(|[p`1*sqrt(1+(p`1/p`2)^2),p`2*sqrt(1+(p`1/p`2)^2)]|) by A9,A7
,A8,A10,FUNCT_1:13
.=(|[p`1*sqrt(1+(p`1/p`2)^2), p`2*sqrt(1+(p`1/p`2)^2)]|)`1 by
PSCOMP_1:def 5
.=p`1*sqrt(1+(p`1/p`2)^2) by EUCLID:52;
hence thesis;
end;
then consider f2 being Function of (TOP-REAL 2)|K1,R^1 such that
A11: 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);
A12: 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;
A13: the carrier of (TOP-REAL 2)|K1=K1 by PRE_TOPC:8;
assume q in the carrier of (TOP-REAL 2)|K1;
then
A14: ex p3 being Point of TOP-REAL 2 st q=p3 &( p3`1<=p3`2 & - p3`2<=p3`1 or
p3`1>=p3`2 & p3`1<=-p3`2)& p3<>0.TOP-REAL 2 by A1,A13;
now
assume
A15: q`2=0;
then q`1=0 by A14;
hence contradiction by A14,A15,EUCLID:53,54;
end;
hence thesis;
end;
then
A16: f1 is continuous by A6,Th35;
A17: for x,y,s,r being Real st |[x,y]| in K1 & s=f2.(|[x,y]|) & r=f1.
(|[x,y]|) holds f.(|[x,y]|)=|[s,r]|
proof
let x,y,s,r be Real;
assume that
A18: |[x,y]| in K1 and
A19: s=f2.(|[x,y]|) & r=f1.(|[x,y]|);
set p99=|[x,y]|;
A20: ex p3 being Point of TOP-REAL 2 st p99=p3 &( p3`1<=p3`2 & -p3`2<=p3`1
or p3`1>=p3`2 & p3`1<=-p3`2)& p3<>0.TOP-REAL 2 by A1,A18;
A21: the carrier of (TOP-REAL 2)|K1=K1 by PRE_TOPC:8;
then
A22: f1.p99=p99`2*sqrt(1+(p99`1/p99`2)^2) by A6,A18;
((Sq_Circ")|K0).(|[x,y]|)=((Sq_Circ")).(|[x,y]|) by A18,FUNCT_1:49
.= |[p99`1*sqrt(1+(p99`1/p99`2)^2), p99`2*sqrt(1+(p99`1/p99`2)^2)]| by
A20,Th30
.=|[s,r]| by A11,A18,A19,A21,A22;
hence thesis by A1;
end;
f2 is continuous by A12,A11,Th36;
hence thesis by A1,A16,A17,Lm13,JGRAPH_2:35;
end;
theorem Th39:
for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2
)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=(Sq_Circ")
|K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p
`1) & p<>0.TOP-REAL 2} holds f is continuous & K0 is closed
proof
reconsider K5={p7 where p7 is Point of TOP-REAL 2:p7`2<=-p7`1 } as closed
Subset of TOP-REAL 2 by JGRAPH_2:47;
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:46;
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:47;
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:46;
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);
set b0 = NonZero TOP-REAL 2;
defpred P0[Point of TOP-REAL 2] means ($1`2<=$1`1 & -$1`1<=$1`2 or $1`2>=$1
`1 & $1`2<=-$1`1);
let B0 be Subset of TOP-REAL 2,K0 be Subset of (TOP-REAL 2)|B0,f being
Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0);
set k0 = {p:P0[p] & p<>0.TOP-REAL 2};
assume that
A1: f=(Sq_Circ")|K0 and
A2: B0=b0 & K0=k0;
the carrier of (TOP-REAL 2)|B0 = B0 by PRE_TOPC:8;
then reconsider K1=K0 as Subset of TOP-REAL 2 by XBOOLE_1:1;
k0 c= NonZero TOP-REAL 2 from TopIncl;
then
A3: ((TOP-REAL 2)|B0)|K0=(TOP-REAL 2)|K1 by A2,PRE_TOPC:7;
reconsider K1={p7 where p7 is Point of TOP-REAL 2: P[p7]} as Subset of
TOP-REAL 2 from JGRAPH_2:sch 1;
A4: K2 /\ K3 \/ K4 /\ K5 c= K1
proof
let x be object;
assume
A5: x in K2 /\ K3 \/ K4 /\ K5;
per cases by A5,XBOOLE_0:def 3;
suppose
A6: x in K2 /\ K3;
then x in K3 by XBOOLE_0:def 4;
then
A7: ex p8 being Point of TOP-REAL 2 st p8=x & -p8`1<=p8`2;
x in K2 by A6,XBOOLE_0:def 4;
then ex p7 being Point of TOP-REAL 2 st p7=x & p7`2<=(p7`1);
hence thesis by A7;
end;
suppose
A8: x in K4 /\ K5;
then x in K5 by XBOOLE_0:def 4;
then
A9: ex p8 being Point of TOP-REAL 2 st p8=x & p8`2<= -p8`1;
x in K4 by A8,XBOOLE_0:def 4;
then ex p7 being Point of TOP-REAL 2 st p7=x & p7`2>=(p7`1);
hence thesis by A9;
end;
end;
A10: K2 /\ K3 is closed & K4 /\ K5 is closed by TOPS_1:8;
K1 c= K2 /\ K3 \/ K4 /\ K5
proof
let x be object;
assume x in K1;
then ex p being Point of TOP-REAL 2 st p=x &( p`2<=p`1 & -p`1 <=p`2 or p`2
>=p`1 & p`2<=-p`1);
then x in K2 & x in K3 or x in K4 & x in K5;
then x in K2 /\ K3 or x in K4 /\ K5 by XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 3;
end;
then K1=K2 /\ K3 \/ K4 /\ K5 by A4;
then
A11: K1 is closed by A10,TOPS_1:9;
k0={p7 where p7 is Point of TOP-REAL 2:P0[p7]} /\ b0 from TopInter;
then K0=K1 /\ [#]((TOP-REAL 2)|B0) by A2,PRE_TOPC:def 5;
hence thesis by A1,A2,A3,A11,Th37,PRE_TOPC:13;
end;
theorem Th40:
for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2
)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=(Sq_Circ")
|K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p
`2) & p<>0.TOP-REAL 2} holds f is continuous & K0 is closed
proof
reconsider K5={p7 where p7 is Point of TOP-REAL 2:p7`1<=-p7`2 } as closed
Subset of TOP-REAL 2 by JGRAPH_2:48;
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:46;
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:48;
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:46;
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);
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);
let B0 be Subset of TOP-REAL 2,K0 be Subset of (TOP-REAL 2)|B0,f being
Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0);
set k0 = {p:P0[p] & p<>0.TOP-REAL 2}, b0=NonZero TOP-REAL 2;
assume that
A1: f=(Sq_Circ")|K0 and
A2: B0=b0 & K0=k0;
the carrier of (TOP-REAL 2)|B0= B0 by PRE_TOPC:8;
then reconsider K1=K0 as Subset of TOP-REAL 2 by XBOOLE_1:1;
{p:P[p] & p<>0.TOP-REAL 2} c= NonZero TOP-REAL 2 from TopIncl;
then
A3: ((TOP-REAL 2)|B0)|K0=(TOP-REAL 2)|K1 by A2,PRE_TOPC:7;
set k1 = {p7 where p7 is Point of TOP-REAL 2: P0[p7]};
A4: K2 /\ K3 is closed & K4 /\ K5 is closed by TOPS_1:8;
reconsider K1=k1 as Subset of TOP-REAL 2 from JGRAPH_2:sch 1;
A5: K2 /\ K3 \/ K4 /\ K5 c= K1
proof
let x be object;
assume
A6: x in K2 /\ K3 \/ K4 /\ K5;
per cases by A6,XBOOLE_0:def 3;
suppose
A7: x in K2 /\ K3;
then x in K3 by XBOOLE_0:def 4;
then
A8: ex p8 being Point of TOP-REAL 2 st p8=x & -p8`2<=p8`1;
x in K2 by A7,XBOOLE_0:def 4;
then ex p7 being Point of TOP-REAL 2 st p7=x & p7`1<=(p7`2);
hence thesis by A8;
end;
suppose
A9: x in K4 /\ K5;
then x in K5 by XBOOLE_0:def 4;
then
A10: ex p8 being Point of TOP-REAL 2 st p8=x & p8`1<= -p8`2;
x in K4 by A9,XBOOLE_0:def 4;
then ex p7 being Point of TOP-REAL 2 st p7=x & p7`1>=(p7`2);
hence thesis by A10;
end;
end;
K1 c= K2 /\ K3 \/ K4 /\ K5
proof
let x be object;
assume x in K1;
then ex p being Point of TOP-REAL 2 st p=x &( p`1<=p`2 & -p`2 <=p`1 or p`1
>=p`2 & p`1<=-p`2);
then x in K2 & x in K3 or x in K4 & x in K5;
then x in K2 /\ K3 or x in K4 /\ K5 by XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 3;
end;
then K1=K2 /\ K3 \/ K4 /\ K5 by A5;
then
A11: K1 is closed by A4,TOPS_1:9;
k0=k1 /\ b0 from TopInter;
then K0=K1 /\ [#]((TOP-REAL 2)|B0) by A2,PRE_TOPC:def 5;
hence thesis by A1,A2,A3,A11,Th38,PRE_TOPC:13;
end;
theorem Th41:
for D being non empty Subset of TOP-REAL 2 st D`={0.TOP-REAL 2}
holds ex h being Function of (TOP-REAL 2)|D,(TOP-REAL 2)|D st h=(Sq_Circ")|D &
h is continuous
proof
set Y1=|[-1,1]|;
set B0 = {0.TOP-REAL 2};
let D be non empty Subset of TOP-REAL 2;
A1: the carrier of ((TOP-REAL 2)|D) = D by PRE_TOPC:8;
dom (Sq_Circ")=(the carrier of (TOP-REAL 2)) by Th29,FUNCT_2:def 1;
then
A2: dom ((Sq_Circ")|D)=(the carrier of (TOP-REAL 2))/\ D by RELAT_1:61
.=the carrier of ((TOP-REAL 2)|D) by A1,XBOOLE_1:28;
assume
A3: D`={0.TOP-REAL 2};
then
A4: D = (B0)` .=(NonZero TOP-REAL 2) by SUBSET_1:def 4;
A5: {p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2} c=
the carrier of (TOP-REAL 2)|D
proof
let x be object;
assume
x in {p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0. TOP-REAL 2};
then
A6: ex p st x=p &( p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p `1)& p<>0.
TOP-REAL 2;
now
assume not x in D;
then x in (the carrier of TOP-REAL 2) \ D by A6,XBOOLE_0:def 5;
then x in D` by SUBSET_1:def 4;
hence contradiction by A3,A6,TARSKI:def 1;
end;
hence thesis by PRE_TOPC:8;
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.TOP-REAL 2} by Lm9,Lm10;
then reconsider K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.
TOP-REAL 2} as non empty Subset of (TOP-REAL 2)|D by A5;
A7: K0=the carrier of ((TOP-REAL 2)|D)|K0 by PRE_TOPC:8;
A8: {p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2} c=
the carrier of (TOP-REAL 2)|D
proof
let x be object;
assume
x in {p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0. TOP-REAL 2};
then
A9: ex p st x=p &( p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p `2)& p<>0.
TOP-REAL 2;
now
assume not x in D;
then x in (the carrier of TOP-REAL 2) \ D by A9,XBOOLE_0:def 5;
then x in D` by SUBSET_1:def 4;
hence contradiction by A3,A9,TARSKI:def 1;
end;
hence thesis by PRE_TOPC:8;
end;
Y1`1=-1 & Y1`2=1 by EUCLID:52;
then
Y1 in {p where p is Point of TOP-REAL 2: (p`1<=p`2 & -p`2<=p`1 or p`1>=
p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2} by JGRAPH_2:3;
then reconsider K1={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.
TOP-REAL 2} as non empty Subset of (TOP-REAL 2)|D by A8;
A10: K1=the carrier of ((TOP-REAL 2)|D)|K1 by PRE_TOPC:8;
A11: D c= K0 \/ K1
proof
let x be object;
assume
A12: x in D;
then reconsider px=x as Point of TOP-REAL 2;
not x in {0.TOP-REAL 2} by A4,A12,XBOOLE_0:def 5;
then (px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1) & px<>0.
TOP-REAL 2 or (px`1<=px`2 & -px`2<=px`1 or px`1>=px`2 & px`1<=-px`2) & px<>0.
TOP-REAL 2 by TARSKI:def 1,XREAL_1:26;
then x in K0 or x in K1;
hence thesis by XBOOLE_0:def 3;
end;
A13: the carrier of ((TOP-REAL 2)|D)=[#](((TOP-REAL 2)|D))
.=(NonZero TOP-REAL 2) by A4,PRE_TOPC:def 5;
A14: K0 c= the carrier of TOP-REAL 2
proof
let z be object;
assume z in K0;
then ex p8 being Point of TOP-REAL 2 st p8=z &( p8`2<=p8`1 & - p8`1<=p8`2
or p8`2>=p8`1 & p8`2<=-p8`1)& p8<>0.TOP-REAL 2;
hence thesis;
end;
A15: rng ((Sq_Circ")|K0) c= the carrier of ((TOP-REAL 2)|D)|K0
proof
reconsider K00=K0 as Subset of TOP-REAL 2 by A14;
let y be object;
A16: 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;
A17: the carrier of (TOP-REAL 2)|K00=K0 by PRE_TOPC:8;
assume q in the carrier of (TOP-REAL 2)|K00;
then
A18: ex p3 being Point of TOP-REAL 2 st q=p3 &( p3`2<=p3`1 & - p3`1<=p3`2
or p3`2>=p3`1 & p3`2<=-p3`1)& p3<>0.TOP-REAL 2 by A17;
now
assume
A19: q`1=0;
then q`2=0 by A18;
hence contradiction by A18,A19,EUCLID:53,54;
end;
hence thesis;
end;
assume y in rng ((Sq_Circ")|K0);
then consider x being object such that
A20: x in dom ((Sq_Circ")|K0) and
A21: y=((Sq_Circ")|K0).x by FUNCT_1:def 3;
A22: x in (dom (Sq_Circ")) /\ K0 by A20,RELAT_1:61;
then
A23: x in K0 by XBOOLE_0:def 4;
then reconsider p=x as Point of TOP-REAL 2 by A14;
K00=the carrier of ((TOP-REAL 2)|K00) by PRE_TOPC:8;
then p in the carrier of ((TOP-REAL 2)|K00) by A22,XBOOLE_0:def 4;
then
A24: p`1<>0 by A16;
set p9=|[p`1*sqrt(1+(p`2/p`1)^2),p`2*sqrt(1+(p`2/p`1)^2)]|;
A25: p9`1=p`1*sqrt(1+(p`2/p`1)^2) & p9`2=p`2*sqrt(1+(p`2/p`1)^2) by EUCLID:52;
A26: ex px being Point of TOP-REAL 2 st x=px &( px`2<=px`1 & - px`1<=px`2
or px`2>=px`1 & px`2<=-px`1)& px<>0.TOP-REAL 2 by A23;
then
A27: (Sq_Circ").p=|[p`1*sqrt(1+(p`2/p`1)^2), p`2*sqrt(1+(p`2/p`1)^2)]| by Th28;
A28: sqrt(1+(p`2/p`1)^2)>0 by Lm1,SQUARE_1:25;
then
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 A26,
XREAL_1:64;
then
A29: 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));
A30: p9`1=p`1*sqrt(1+(p`2/p`1)^2) by EUCLID:52;
A31: now
assume p9=0.TOP-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 A30,EUCLID:52,54;
hence contradiction by A24,A28,XCMPLX_1:89;
end;
(Sq_Circ").p=y by A21,A23,FUNCT_1:49;
then y in K0 by A31,A27,A29,A25;
hence thesis by PRE_TOPC:8;
end;
dom ((Sq_Circ")|K0)= dom ((Sq_Circ")) /\ K0 by RELAT_1:61
.=((the carrier of TOP-REAL 2)) /\ K0 by Th29,FUNCT_2:def 1
.=K0 by A14,XBOOLE_1:28;
then reconsider
f=(Sq_Circ")|K0 as Function of ((TOP-REAL 2)|D)|K0, (TOP-REAL 2)|
D by A7,A15,FUNCT_2:2,XBOOLE_1:1;
A32: K1=[#](((TOP-REAL 2)|D)|K1) by PRE_TOPC:def 5;
A33: K1 c= the carrier of TOP-REAL 2
proof
let z be object;
assume z in K1;
then ex p8 being Point of TOP-REAL 2 st p8=z &( p8`1<=p8`2 & - p8`2<=p8`1
or p8`1>=p8`2 & p8`1<=-p8`2)& p8<>0.TOP-REAL 2;
hence thesis;
end;
A34: rng ((Sq_Circ")|K1) c= the carrier of ((TOP-REAL 2)|D)|K1
proof
reconsider K10=K1 as Subset of TOP-REAL 2 by A33;
let y be object;
A35: 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;
A36: the carrier of (TOP-REAL 2)|K10=K1 by PRE_TOPC:8;
assume q in the carrier of (TOP-REAL 2)|K10;
then
A37: ex p3 being Point of TOP-REAL 2 st q=p3 &( p3`1<=p3`2 & - p3`2<=p3`1
or p3`1>=p3`2 & p3`1<=-p3`2)& p3<>0.TOP-REAL 2 by A36;
now
assume
A38: q`2=0;
then q`1=0 by A37;
hence contradiction by A37,A38,EUCLID:53,54;
end;
hence thesis;
end;
assume y in rng ((Sq_Circ")|K1);
then consider x being object such that
A39: x in dom ((Sq_Circ")|K1) and
A40: y=((Sq_Circ")|K1).x by FUNCT_1:def 3;
A41: x in (dom (Sq_Circ")) /\ K1 by A39,RELAT_1:61;
then
A42: x in K1 by XBOOLE_0:def 4;
then reconsider p=x as Point of TOP-REAL 2 by A33;
K10=the carrier of ((TOP-REAL 2)|K10) by PRE_TOPC:8;
then p in the carrier of ((TOP-REAL 2)|K10) by A41,XBOOLE_0:def 4;
then
A43: p`2<>0 by A35;
set p9=|[p`1*sqrt(1+(p`1/p`2)^2),p`2*sqrt(1+(p`1/p`2)^2)]|;
A44: p9`2=p`2*sqrt(1+(p`1/p`2)^2) & p9`1=p`1*sqrt(1+(p`1/p`2)^2) by EUCLID:52;
A45: ex px being Point of TOP-REAL 2 st x=px &( px`1<=px`2 & - px`2<=px`1
or px`1>=px`2 & px`1<=-px`2)& px<>0.TOP-REAL 2 by A42;
then
A46: (Sq_Circ").p=|[p`1*sqrt(1+(p`1/p`2)^2), p`2*sqrt(1+(p`1/p`2)^2)]| by Th30;
A47: sqrt(1+(p`1/p`2)^2)>0 by Lm1,SQUARE_1:25;
then
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 A45,
XREAL_1:64;
then
A48: 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));
A49: p9`2=p`2*sqrt(1+(p`1/p`2)^2) by EUCLID:52;
A50: now
assume p9=0.TOP-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 A49,EUCLID:52,54;
hence contradiction by A43,A47,XCMPLX_1:89;
end;
(Sq_Circ").p=y by A40,A42,FUNCT_1:49;
then y in K1 by A50,A46,A48,A44;
hence thesis by PRE_TOPC:8;
end;
dom ((Sq_Circ")|K1)= dom ((Sq_Circ")) /\ K1 by RELAT_1:61
.=((the carrier of TOP-REAL 2)) /\ K1 by Th29,FUNCT_2:def 1
.=K1 by A33,XBOOLE_1:28;
then reconsider
g=(Sq_Circ")|K1 as Function of ((TOP-REAL 2)|D)|K1, ((TOP-REAL 2)
|D) by A10,A34,FUNCT_2:2,XBOOLE_1:1;
A51: dom g=K1 by A10,FUNCT_2:def 1;
g=(Sq_Circ")|K1;
then
A52: K1 is closed by A4,Th40;
A53: K0=[#](((TOP-REAL 2)|D)|K0) by PRE_TOPC:def 5;
A54: now
let x be object;
assume
A55: x in ([#]((((TOP-REAL 2)|D)|K0))) /\ ([#] ((((TOP-REAL 2)|D)|K1) ));
then x in K0 by A53,XBOOLE_0:def 4;
then f.x=(Sq_Circ").x by FUNCT_1:49;
hence f.x = g.x by A32,A55,FUNCT_1:49;
end;
f=(Sq_Circ")|K0;
then
A56: K0 is closed by A4,Th39;
A57: dom f=K0 by A7,FUNCT_2:def 1;
D= [#]((TOP-REAL 2)|D) by PRE_TOPC:def 5;
then
A58: ([#](((TOP-REAL 2)|D)|K0)) \/ [#](((TOP-REAL 2)|D)|K1) = [#]((TOP-REAL
2)|D) by A53,A32,A11;
A59: f is continuous & g is continuous by A4,Th39,Th40;
then consider h being Function of (TOP-REAL 2)|D,(TOP-REAL 2)|D such that
A60: h= f+*g and
h is continuous by A53,A32,A58,A56,A52,A54,JGRAPH_2:1;
K0=[#](((TOP-REAL 2)|D)|K0) & K1=[#](((TOP-REAL 2)|D)|K1) by PRE_TOPC:def 5;
then
A61: f tolerates g by A54,A57,A51,PARTFUN1:def 4;
A62: for x being object st x in dom h holds h.x=((Sq_Circ")|D).x
proof
let x be object;
assume
A63: x in dom h;
then reconsider p=x as Point of TOP-REAL 2 by A13,XBOOLE_0:def 5;
not x in {0.TOP-REAL 2} by A13,A63,XBOOLE_0:def 5;
then
A64: x <>0.TOP-REAL 2 by TARSKI:def 1;
x in (the carrier of TOP-REAL 2)\D` by A3,A13,A63;
then
A65: x in D`` by SUBSET_1:def 4;
per cases;
suppose
A66: x in K0;
A67: (Sq_Circ")|D.p=(Sq_Circ").p by A65,FUNCT_1:49
.=f.p by A66,FUNCT_1:49;
h.p=(g+*f).p by A60,A61,FUNCT_4:34
.=f.p by A57,A66,FUNCT_4:13;
hence thesis by A67;
end;
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 A64;
then p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2 by XREAL_1:26;
then
A68: x in K1 by A64;
(Sq_Circ")|D.p=(Sq_Circ").p by A65,FUNCT_1:49
.=g.p by A68,FUNCT_1:49;
hence thesis by A60,A51,A68,FUNCT_4:13;
end;
end;
dom h=the carrier of ((TOP-REAL 2)|D) by FUNCT_2:def 1;
then f+*g=(Sq_Circ")|D by A60,A2,A62;
hence thesis by A53,A32,A58,A56,A59,A52,A54,JGRAPH_2:1;
end;
theorem Th42:
ex h being Function of TOP-REAL 2,TOP-REAL 2 st h=Sq_Circ" & h is continuous
proof
reconsider f=(Sq_Circ") as Function of (TOP-REAL 2),(TOP-REAL 2) by Th29;
reconsider D=NonZero TOP-REAL 2 as non empty Subset of TOP-REAL 2 by
JGRAPH_2:9;
A1: f.(0.TOP-REAL 2)=0.TOP-REAL 2 by Th28;
A2: for p being Point of (TOP-REAL 2)|D holds f.p<>f.(0.TOP-REAL 2)
proof
let p be Point of (TOP-REAL 2)|D;
A3: [#]((TOP-REAL 2)|D)=D by PRE_TOPC:def 5;
then reconsider q=p as Point of TOP-REAL 2 by XBOOLE_0:def 5;
not p in {0.TOP-REAL 2} by A3,XBOOLE_0:def 5;
then
A4: not p=0.TOP-REAL 2 by TARSKI:def 1;
per cases;
suppose
A5: not(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then A6: q`2<>0;
set q9=|[q`1*sqrt(1+(q`1/q`2)^2),q`2*sqrt(1+(q`1/q`2)^2)]|;
A7: q9`2=q`2*sqrt(1+(q`1/q`2)^2) by EUCLID:52;
A8: sqrt(1+(q`1/q`2)^2)>0 by Lm1,SQUARE_1:25;
now
assume q9=0.TOP-REAL 2;
then 0 *q`2=q`2*sqrt(1+(q`1/q`2)^2) by A7,EUCLID:52,54;
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 );
hence contradiction by A6,A8,XCMPLX_1:89;
end;
hence thesis by A1,A5,Th28;
end;
suppose
A9: q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1;
A10: now
assume
A11: q`1=0;
then q`2=0 by A9;
hence contradiction by A4,A11,EUCLID:53,54;
end;
set q9=|[q`1*sqrt(1+(q`2/q`1)^2),q`2*sqrt(1+(q`2/q`1)^2)]|;
A12: q9`1=q`1*sqrt(1+(q`2/q`1)^2) by EUCLID:52;
A13: sqrt(1+(q`2/q`1)^2)>0 by Lm1,SQUARE_1:25;
now
assume q9=0.TOP-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 A12,EUCLID:52,54;
hence contradiction by A10,A13,XCMPLX_1:89;
end;
hence thesis by A1,A4,A9,Th28;
end;
end;
A14: for V being Subset of TOP-REAL 2 st f.(0.TOP-REAL 2) in V & V is open
ex W being Subset of TOP-REAL 2 st 0.TOP-REAL 2 in W & W is open & f.:W c= V
proof
reconsider u0=0.TOP-REAL 2 as Point of Euclid 2 by EUCLID:67;
let V be Subset of TOP-REAL 2;
reconsider VV=V as Subset of TopSpaceMetr Euclid 2 by Lm16;
assume that
A15: f.(0.TOP-REAL 2) in V and
A16: V is open;
VV is open by A16,Lm16,PRE_TOPC:30;
then consider r being Real such that
A17: r>0 and
A18: Ball(u0,r) c= V by A1,A15,TOPMETR:15;
reconsider r as Real;
reconsider W1=Ball(u0,r), V1=Ball(u0,r/sqrt(2)) as Subset of TOP-REAL 2 by
EUCLID:67;
A19: f.:V1 c= W1
proof
let z be object;
A20: sqrt(2)>0 by SQUARE_1:25;
assume z in f.:V1;
then consider y being object such that
A21: y in dom f and
A22: y in V1 and
A23: z=f.y by FUNCT_1:def 6;
z in rng f by A21,A23,FUNCT_1:def 3;
then reconsider qz=z as Point of TOP-REAL 2;
reconsider pz=qz as Point of Euclid 2 by EUCLID:67;
reconsider q=y as Point of TOP-REAL 2 by A21;
reconsider qy=q as Point of Euclid 2 by EUCLID:67;
A24: (q`1)^2 >=0 by XREAL_1:63;
A25: (q`2)^2>=0 by XREAL_1:63;
dist(u0,qy)=0 & (qz`2)^2>=0 by XREAL_1:63;
then
A41: sqrt((qz`1)^2+(qz`2)^2) <= sqrt((q`1)^2*2+(q`2)^2*2) by A40,SQUARE_1:26
;
A42: ((0.TOP-REAL 2) - qz)`2=(0.TOP-REAL 2)`2-qz`2 by TOPREAL3:3
.= -qz`2 by JGRAPH_2:3;
((0.TOP-REAL 2) - qz)`1=(0.TOP-REAL 2)`1-qz`1 by TOPREAL3:3
.= -qz`1 by JGRAPH_2:3;
then sqrt((((0.TOP-REAL 2) - qz)`1)^2+(((0.TOP-REAL 2) - qz)`2)^2)

0 by Lm1;
then
A51: (sqrt(1+(q`1/q`2)^2))^2=1+(q`1/q`2)^2 by SQUARE_1:def 2;
A52: (q`1)^2*(1+(q`1/q`2)^2)<=(q`1)^2*2 by A24,A49,XREAL_1:64;
A53: (Sq_Circ").q=|[q`1*sqrt(1+(q`1/q`2)^2),q`2*sqrt(1+(q`1/q`2 ) ^2)
]| by A43,Th28;
then qz`1=q`1*sqrt(1+(q`1/q`2)^2) by A23,EUCLID:52;
then
A54: (qz`1)^2<=(q`1)^2*2 by A52,A51,SQUARE_1:9;
qz`2=q`2*sqrt(1+(q`1/q`2)^2) by A23,A53,EUCLID:52;
then (qz`2)^2<=(q`2)^2*2 by A50,A51,SQUARE_1:9;
then
A55: (qz`2)^2+(qz`1)^2<=(q`2)^2*2+(q`1)^2*2 by A54,XREAL_1:7;
(qz`2)^2>=0 & (qz`1)^2>=0 by XREAL_1:63;
then
A56: sqrt((qz`2)^2+(qz`1)^2) <= sqrt((q`2)^2*2+(q`1)^2*2) by A55,SQUARE_1:26
;
A57: ((0.TOP-REAL 2) - qz)`2=(0.TOP-REAL 2)`2-qz`2 by TOPREAL3:3
.= -qz`2 by JGRAPH_2:3;
((0.TOP-REAL 2) - qz)`1=(0.TOP-REAL 2)`1-qz`1 by TOPREAL3:3
.= -qz`1 by JGRAPH_2:3;
then sqrt((((0.TOP-REAL 2) - qz)`2)^2+(((0.TOP-REAL 2) - qz)`1)^2)