Copyright (c) 2002 Association of Mizar Users
environ
vocabulary FUNCT_1, BOOLE, ABSVALUE, EUCLID, PRE_TOPC, JORDAN2C, SQUARE_1,
RELAT_1, SUBSET_1, ARYTM_3, METRIC_1, RCOMP_1, FUNCT_4, FUNCT_5, TOPMETR,
COMPTS_1, JGRAPH_4, ORDINAL2, TOPS_2, ARYTM_1, CARD_3, COMPLEX1, MCART_1,
PARTFUN1, PCOMPS_1, LATTICES, ARYTM;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, XREAL_0, REAL_1,
ABSVALUE, RELAT_1, FUNCT_1, FUNCT_2, NAT_1, STRUCT_0, PARTFUN1, TOPMETR,
PCOMPS_1, EUCLID, COMPTS_1, TOPS_2, METRIC_1, SQUARE_1, TBSP_1, RCOMP_1,
PSCOMP_1, PRE_TOPC, JGRAPH_1, JORDAN2C, FUNCT_4;
constructors REAL_1, TOPS_2, TBSP_1, RCOMP_1, PSCOMP_1, JORDAN2C, COMPTS_1,
TOPGRP_1, TOPMETR, WELLFND1, TOPRNS_1, MEMBERED;
clusters XREAL_0, STRUCT_0, RELSET_1, EUCLID, PRE_TOPC, SQUARE_1, PSCOMP_1,
METRIC_1, TOPREAL6, BORSUK_2, JORDAN6, MEMBERED, ZFMISC_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
theorems TARSKI, AXIOMS, RELAT_1, SUBSET_1, FUNCT_1, FUNCT_2, FUNCT_4, TOPS_1,
TOPS_2, PARTFUN1, PRE_TOPC, FRECHET, TOPMETR, JORDAN6, EUCLID, RELSET_1,
REAL_1, REAL_2, JGRAPH_1, SQUARE_1, PSCOMP_1, METRIC_1, JGRAPH_2,
GOBOARD6, GOBOARD9, TBSP_1, TOPREAL3, TOPREAL5, TOPREAL6, JGRAPH_3,
ABSVALUE, JORDAN2C, TSEP_1, EXTENS_1, XREAL_0, JORDAN1, XBOOLE_0,
XBOOLE_1, TOPRNS_1, SEQ_2, XCMPLX_0, XCMPLX_1;
schemes FUNCT_2, DOMAIN_1, JGRAPH_2, COMPLSP1, SUPINF_2, JGRAPH_3;
begin :: Preliminaries
reserve x,a for real number;
reserve p,q for Point of TOP-REAL 2;
Lm1:p <> 0.REAL 2 implies |.p.| > 0
proof
assume p <> 0.REAL 2;
then |.p.| <> 0 by TOPRNS_1:25;
hence thesis by TOPRNS_1:26;
end;
canceled;
theorem Th2: 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:132;
A3: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<=x+a by A3,AXIOMS:22;
then x<a+0 & x+a>0 by A2,AXIOMS:22,REAL_1:84;
then x<a & x>0-a by REAL_1:84;
hence -a<x & x<a by XCMPLX_1:150;
end;
theorem Th3: for sn being real number st -1<sn & sn<1 holds 1+sn>0 & 1-sn>0
proof let sn be real number;
assume A1: -1<sn & sn<1;
then -1+1<sn+1 by REAL_1:67;
hence 1+sn>0;
thus 1-sn>0 by A1,SQUARE_1:11;
end;
theorem Th4: for a being real number st a^2<=1 holds -1<=a & a<=1
proof let a be real number;assume a^2<=1;
then a^2-1^2<=1^2-1^2 by REAL_1:49,SQUARE_1:59;
then a^2-1^2<=0 by XCMPLX_1:14;
then (a-1)*(a+1)<=0 by SQUARE_1:67;
hence -1<=a & a<=1 by JGRAPH_3:4;
end;
theorem Th5: for a being real number st a^2<1 holds -1<a & a<1
proof let a be real number;assume a^2<1;
then a^2-1^2<1^2-1^2 by REAL_1:54,SQUARE_1:59;
then a^2-1^2<0 by XCMPLX_1:14;
then (a-1)*(a+1)<0 by SQUARE_1:67;
hence -1<a & a<1 by Th2;
end;
theorem Th6:
for X being non empty TopStruct,
g being map of X,R^1, B being Subset of X,
a being real number st g is continuous &
B = {p where p is Point of X: pi(g,p) > a } holds B is open
proof let X be non empty TopStruct,g be map of X,R^1,B be Subset of X,
a be real number;
assume A1: g is continuous & B={p where p is Point of X:pi(g,p) > a };
{r where r is Real: r>a} c= the carrier of R^1
proof let x be set;assume x in {r where r is Real: r>a};
then consider r being Real such that
A2: r=x & r>a;
thus x in the carrier of R^1 by A2,TOPMETR:24;
end;
then reconsider D={r where r is Real: r>a} as Subset of R^1;
A3: D is open by TOPREAL5:7;
A4: B c= g"D
proof let x be set;assume
x in B;
then consider p being Point of X such that
A5: p=x & pi(g,p) > a by A1;
A6: dom g=the carrier of X by FUNCT_2:def 1;
A7: pi(g,p) is Real by XREAL_0:def 1;
pi(g,p)=g.p by JORDAN2C:def 10;
then x in dom g & g.x in D by A5,A6,A7;
hence x in g"D by FUNCT_1:def 13;
end;
g"D c= B
proof let x be set;assume
A8: x in g"D;
then x in dom g & g.x in D by FUNCT_1:def 13;
then consider r being Real such that
A9: r=g.x & r>a;
reconsider p=x as Point of X by A8;
pi(g,p)=g.p by JORDAN2C:def 10;
hence x in B by A1,A9;
end;
then B=g"D by A4,XBOOLE_0:def 10;
hence B is open by A1,A3,TOPS_2:55;
end;
theorem Th7:
for X being non empty TopStruct,
g being map of X,R^1,B being Subset of X,
a being Real st g is continuous &
B={p where p is Point of X: pi(g,p) < a } holds B is open
proof let X be non empty TopStruct,g be map of X,R^1,
B be Subset of X,a be Real;
assume A1: g is continuous & B={p where p is Point of X: pi(g,p) < a };
{r where r is Real: r<a} c= the carrier of R^1
proof let x be set;assume x in {r where r is Real: r<a};
then consider r being Real such that
A2: r=x & r<a;
thus x in the carrier of R^1 by A2,TOPMETR:24;
end;
then reconsider D={r where r is Real: r<a} as Subset of R^1;
A3: D is open by TOPREAL5:8;
A4: B c= g"D
proof let x be set;assume
x in B;
then consider p being Point of X such that
A5: p=x & pi(g,p) < a by A1;
A6: dom g=the carrier of X by FUNCT_2:def 1;
A7: pi(g,p) is Real by XREAL_0:def 1;
pi(g,p)=g.p by JORDAN2C:def 10;
then x in dom g & g.x in D by A5,A6,A7;
hence x in g"D by FUNCT_1:def 13;
end;
g"D c= B
proof let x be set;assume
A8: x in g"D;
then x in dom g & g.x in D by FUNCT_1:def 13;
then consider r being Real such that
A9: r=g.x & r<a;
reconsider p=x as Point of X by A8;
pi(g,p)=g.p by JORDAN2C:def 10;
hence x in B by A1,A9;
end;
then B=g"D by A4,XBOOLE_0:def 10;
hence B is open by A1,A3,TOPS_2:55;
end;
theorem Th8: for f being map of TOP-REAL 2,TOP-REAL 2 st
f is continuous one-to-one & rng f=[#](TOP-REAL 2) &
(for p2 being Point of TOP-REAL 2
ex K being non empty compact Subset of TOP-REAL 2 st K = f.:K &
(ex V2 being Subset of TOP-REAL 2 st
p2 in V2 & V2 is open & V2 c= K & f.p2 in V2))
holds f is_homeomorphism
proof let f be map of TOP-REAL 2,TOP-REAL 2;
assume A1: f is continuous one-to-one & rng f=[#](TOP-REAL 2)
& (for p2 being Point of TOP-REAL 2
ex K being non empty compact Subset of TOP-REAL 2 st K = f.:K &
(ex V2 being Subset of TOP-REAL 2 st
p2 in V2 & V2 is open & V2 c= K & f.p2 in V2));
A2: dom f=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then A3: dom f=[#](TOP-REAL 2) by PRE_TOPC:12;
rng f=the carrier of TOP-REAL 2 by A1,PRE_TOPC:12;
then (f qua Function)" is Function of the carrier of TOP-REAL 2,
the carrier of TOP-REAL 2 by A1,FUNCT_2:31;
then reconsider g=(f qua Function)"
as map of TOP-REAL 2,TOP-REAL 2 ;
for p being Point of TOP-REAL 2, V being Subset of
TOP-REAL 2 st g.p in V & V is open ex W being Subset of TOP-REAL 2 st
p in W & W is open & g.:W c= V
proof let p be Point of TOP-REAL 2, V be Subset of TOP-REAL 2;
assume A4: g.p in V & V is open;
consider K being non empty compact Subset of TOP-REAL 2 such that
A5: K = f.:K & (ex V2 being Subset of TOP-REAL 2 st
g.p in V2 & V2 is open & V2 c= K & f.(g.p) in V2) by A1;
consider V2 being Subset of TOP-REAL 2 such that
A6: g.p in V2 & V2 is open & V2 c= K & f.(g.p) in V2 by A5;
p in the carrier of TOP-REAL 2;
then p in rng f by A1,PRE_TOPC:12;
then A7: g.p in V2 & V2 is open & V2 c= K & p in V2 by A1,A6,FUNCT_1:57;
A8: dom (f|K)=dom f /\ K by FUNCT_1:68
.=(the carrier of TOP-REAL 2)/\ K by FUNCT_2:def 1
.=K by XBOOLE_1:28
.=the carrier of ((TOP-REAL 2)|K) by JORDAN1:1;
rng (f|K) c= rng f by FUNCT_1:76;
then rng (f|K) c= the carrier of TOP-REAL 2 by XBOOLE_1:1;
then f|K is Function of the carrier of (TOP-REAL 2)|K,
the carrier of (TOP-REAL 2) by A8,FUNCT_2:4;
then reconsider h=f|K as map of (TOP-REAL 2)|K,(TOP-REAL 2)
;
A9: h is continuous by A1,TOPMETR:10;
A10: h is one-to-one by A1,FUNCT_1:84;
A11: dom (f|K)=dom f /\ K by RELAT_1:90 .=K by A2,XBOOLE_1:28;
A12:K=(f|K).:K by A5,EXTENS_1:1 .=rng (f|K)
by A11,RELAT_1:146;
then consider f1 being map of (TOP-REAL 2)|K,(TOP-REAL 2)|K such that
A13: h=f1 & f1 is_homeomorphism by A9,A10,JGRAPH_1:64;
A14: rng f1=[#]((TOP-REAL 2)|K) by A13,TOPS_2:def 5;
A15: the carrier of ((TOP-REAL 2)|K)=K by JORDAN1:1;
V /\ V2 /\ K c= K by XBOOLE_1:17;
then reconsider R=V /\ V2 /\ K as Subset of (TOP-REAL 2)|K
by A15;
A16: V /\ V2 is open by A4,A6,TOPS_1:38;
R=V /\ V2 /\ [#]((TOP-REAL 2)|K) by PRE_TOPC:def 10;
then A17: R is open by A16,TOPS_2:32;
A18: g.p in V /\ V2 by A4,A6,XBOOLE_0:def 3;
A19: f1.((f1 qua Function)".p)=p by A7,A10,A12,A13,FUNCT_1:57;
A20: f1.(g.p)=f.(g.p) by A6,A13,FUNCT_1:72.=p
by A1,A2,A3,FUNCT_1:57;
A21: dom f1=dom f /\ K by A13,FUNCT_1:68 .=K
by A2,XBOOLE_1:28;
A22: rng ((f1 qua Function)")=dom f1 by A10,A13,FUNCT_1:55;
rng f1=dom ((f1 qua Function)") by A10,A13,FUNCT_1:55;
then ((f1 qua Function)").p in rng ((f1 qua Function)")
by A7,A12,A13,FUNCT_1:12;
then A23: ((f1 qua Function)").p=g.p by A5,A10,A13,A19,A20,A21,A22,FUNCT_1
:def 8;
reconsider q=p as Point of ((TOP-REAL 2)|K) by A7,JORDAN1:1;
A24: ((f1 qua Function)").p in R by A6,A18,A23,XBOOLE_0:def 3;
A25: dom ((f1 qua Function)")=rng f1 by A10,A13,FUNCT_1:54;
A26: rng ((f1 qua Function)")=dom f1 by A10,A13,FUNCT_1:55;
A27: dom f1=the carrier of (TOP-REAL 2)|K by FUNCT_2:def 1;
the carrier of (TOP-REAL 2)|K=[#]((TOP-REAL 2)|K)
by PRE_TOPC:12;
then A28: the carrier of (TOP-REAL 2)|K=K by PRE_TOPC:def 10;
A29: rng f1 = the carrier of (TOP-REAL 2)|K by A14,PRE_TOPC:12;
then (f1 qua Function)" is Function of the carrier of (TOP-REAL 2)|K,
the carrier of (TOP-REAL 2)|K
by A21,A25,A26,A28,FUNCT_2:4;
then reconsider g1=(f1 qua Function)"
as map of (TOP-REAL 2)|K,(TOP-REAL 2)|K ;
g1=f1" by A10,A13,A14,TOPS_2:def 4;
then g1 is continuous by A13,TOPS_2:def 5;
then consider W3 being Subset of (TOP-REAL 2)|K such that
A30: q in W3 & W3 is open & ((f1 qua Function)").:W3 c= R
by A17,A24,JGRAPH_2:20;
A31: ((f qua Function)").:W3 c= R
proof let y be set;assume y in ((f qua Function)").:W3;
then consider x being set such that
A32: x in dom ((f qua Function)") & x in W3 & y=((f qua Function)").x
by FUNCT_1:def 12;
x in rng f by A1,A32,FUNCT_1:55;
then A33: y in dom f & f.y=x by A1,A32,FUNCT_1:54;
A34: dom ((f1 qua Function)")=the carrier of (TOP-REAL 2)|K by A10,A13,
A29,FUNCT_1:55;
the carrier of (TOP-REAL 2)|K=K by JORDAN1:1;
then consider z2 being set such that
A35: z2 in dom f & z2 in K & f.y=f.z2 by A5,A32,A33,FUNCT_1:def 12;
A36: y in K by A1,A33,A35,FUNCT_1:def 8;
then A37: y in the carrier of ((TOP-REAL 2)|K) by JORDAN1:1;
f1.y=x by A13,A33,A36,FUNCT_1:72;
then x in dom ((f1 qua Function)") & y=((f1 qua Function)").x
by A10,A13,A27,A32,A34,A37,FUNCT_1:54;
then y in ((f1 qua Function)").:W3 by A32,FUNCT_1:def 12;
hence y in R by A30;
end;
consider W5 being Subset of TOP-REAL 2 such that
A38: W5 is open & W3=W5 /\ [#]((TOP-REAL 2)|K) by A30,TOPS_2:32;
reconsider W4=W5 /\ V2 as Subset of TOP-REAL 2;
p in W5 by A30,A38,XBOOLE_0:def 3;
then A39: p in W4 by A7,XBOOLE_0:def 3;
A40: W4 is open by A6,A38,TOPS_1:38;
W4=W5 /\ (V2 /\ K) by A6,XBOOLE_1:28
.=W5 /\ K /\ V2 by XBOOLE_1:16
.=W3 /\ V2 by A38,PRE_TOPC:def 10;
then A41: g.:W4 c= (g).:W3 /\ (g).:V2 by RELAT_1:154;
g.:W3 /\ (g).:V2 c= (g).:W3 by XBOOLE_1:17;
then g.:W4 c= g.:W3 by A41,XBOOLE_1:1;
then A42: (g).:W4 c= R by A31,XBOOLE_1:1;
R=V /\ (V2 /\ K) by XBOOLE_1:16;
then R c= V by XBOOLE_1:17;
then g.:W4 c= V by A42,XBOOLE_1:1;
hence ex W being Subset of TOP-REAL 2 st
p in W & W is open & g.:W c= V by A39,A40;
end;
then A43: g is continuous by JGRAPH_2:20;
g=f" by A1,TOPS_2:def 4;
hence f is_homeomorphism by A1,A3,A43,TOPS_2:def 5;
end;
theorem Th9: for X being non empty TopSpace,
f1,f2 being map of X,R^1,a,b being real number st f1 is continuous &
f2 is continuous & b<>0 & (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-a)/b) & g is continuous
proof let X be non empty TopSpace,
f1,f2 be map of X,R^1,a,b be real number;
assume A1:f1 is continuous & f2 is continuous & b<>0 &
(for q being Point of X holds f2.q<>0);
consider g1 being map of X,R^1
such that A2: for p being Point of X
holds g1.p=b & g1 is continuous by JGRAPH_2:30;
consider g2 being map of X,R^1
such that A3: for p being Point of X
holds g2.p=a & g2 is continuous by JGRAPH_2:30;
consider g3 being map of X,R^1
such that A4: (for p being Point of X,r1,r0 being real number st
f1.p=r1 & f2.p=r0 holds g3.p=r1/r0) & g3 is continuous
by A1,JGRAPH_2:37;
consider g4 being map of X,R^1
such that A5: (for p being Point of X,r1,r0 being real number st
g3.p=r1 & g2.p=r0 holds g4.p=r1-r0) & g4 is continuous
by A3,A4,JGRAPH_2:31;
for q being Point of X holds g1.q<>0 by A1,A2;
then consider g5 being map of X,R^1
such that A6: (for p being Point of X,r1,r0 being real number st
g4.p=r1 & g1.p=r0 holds g5.p=r1/r0) & g5 is continuous
by A2,A5,JGRAPH_2:37;
for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g5.p=(r1/r2-a)/b
proof let p be Point of X,r1,r2 be real number;
assume A7:f1.p=r1 & f2.p=r2;
A8: g1.p=b by A2;
A9: g2.p=a by A3;
set r8=r1/r2;
g3.p=r8 by A4,A7;
then g4.p=r8-a by A5,A9;
hence g5.p=(r1/r2-a)/b by A6,A8;
end;
hence thesis by A6;
end;
theorem Th10: for X being non empty TopSpace,
f1,f2 being map of X,R^1,a,b being Real st f1 is continuous &
f2 is continuous & b<>0 & (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 st
f1.p=r1 & f2.p=r2 holds g.p=r2*((r1/r2-a)/b)) & g is continuous
proof let X be non empty TopSpace,
f1,f2 be map of X,R^1,a,b be Real;
assume A1:f1 is continuous & f2 is continuous & b<>0 &
(for q being Point of X holds f2.q<>0);
consider g1 being map of X,R^1
such that A2: for p being Point of X
holds g1.p=b & g1 is continuous by JGRAPH_2:30;
consider g2 being map of X,R^1
such that A3: for p being Point of X
holds g2.p=a & g2 is continuous by JGRAPH_2:30;
consider g3 being map of X,R^1
such that A4: (for p being Point of X,r1,r0 being real number st
f1.p=r1 & f2.p=r0 holds g3.p=r1/r0) & g3 is continuous
by A1,JGRAPH_2:37;
consider g4 being map of X,R^1
such that A5: (for p being Point of X,r1,r0 being real number st
g3.p=r1 & g2.p=r0 holds g4.p=r1-r0) & g4 is continuous
by A3,A4,JGRAPH_2:31;
for q being Point of X holds g1.q<>0 by A1,A2;
then consider g5 being map of X,R^1
such that A6: (for p being Point of X,r1,r0 being real number st
g4.p=r1 & g1.p=r0 holds g5.p=r1/r0) & g5 is continuous
by A2,A5,JGRAPH_2:37;
consider g6 being map of X,R^1
such that A7: (for p being Point of X,r1,r0 being real number st
f2.p=r1 & g5.p=r0 holds g6.p=r1*r0) & g6 is continuous
by A1,A6,JGRAPH_2:35;
for p being Point of X,r1,r2 being Real st
f1.p=r1 & f2.p=r2 holds g6.p=r2*((r1/r2-a)/b)
proof let p be Point of X,r1,r2 be Real;
assume A8:f1.p=r1 & f2.p=r2;
A9: g1.p=b by A2;
A10: g2.p=a by A3;
reconsider r8=r1/r2 as Real;
g3.p=r8 by A4,A8;
then g4.p=r8-a by A5,A10;
then g5.p=(r1/r2-a)/b by A6,A9;
hence g6.p=r2*((r1/r2-a)/b) by A7,A8;
end;
hence thesis by A7;
end;
theorem Th11:
for X being non empty TopSpace,
f1 being map of X,R^1 st f1 is continuous
holds ex g being map of X,R^1
st (for p being Point of X,r1 being real number st f1.p=r1 holds g.p=r1^2) &
g is continuous
proof let X be non empty TopSpace,
f1 being map of X,R^1;
assume f1 is continuous;
then consider g1 being map of X,R^1
such that A1:(for p being Point of X,r1 being real number st
f1.p=r1 holds g1.p=r1*r1) & g1 is continuous by JGRAPH_2:32;
for p being Point of X,r1 being real number st
f1.p=r1 holds g1.p=r1^2
proof let p be Point of X,r1 be real number;
assume f1.p=r1;
then g1.p=r1*r1 by A1;
hence thesis by SQUARE_1:def 3;
end;
hence thesis by A1;
end;
theorem Th12:
for X being non empty TopSpace,
f1 being map of X,R^1 st f1 is continuous
holds ex g being map of X,R^1
st (for p being Point of X,r1 being real number st
f1.p=r1 holds g.p=abs(r1)) & g is continuous
proof let X be non empty TopSpace,
f1 be map of X,R^1;
assume f1 is continuous;
then consider g1 being map of X,R^1 such that
A1: (for p being Point of X,r1 being real number st
f1.p=r1 holds g1.p=r1^2) & g1 is continuous by Th11;
for q being Point of X ex r being real number st g1.q=r & r>=0
proof let q be Point of X;
reconsider r11=f1.q as Real by TOPMETR:24;
A2: g1.q=r11^2 by A1;
r11^2>=0 by SQUARE_1:72;
hence ex r being real number st g1.q=r & r>=0 by A2;
end;
then consider g2 being map of X,R^1 such that
A3: (for p being Point of X,r1 being real number st
g1.p=r1 holds g2.p=sqrt(r1)) & g2 is continuous by A1,JGRAPH_3:15;
for p being Point of X,r1 being real number st
f1.p=r1 holds g2.p=abs(r1)
proof let p be Point of X,r1 be real number;
assume f1.p=r1;
then g1.p=r1^2 by A1;
then g2.p=sqrt(r1^2) by A3 .=abs(r1) by SQUARE_1:91;
hence g2.p=abs(r1);
end;
hence thesis by A3;
end;
theorem Th13:
for X being non empty TopSpace,
f1 being map of X,R^1 st f1 is continuous
holds ex g being map of X,R^1
st (for p being Point of X,r1 being real number st
f1.p=r1 holds g.p=-r1) & g is continuous
proof let X be non empty TopSpace,
f1 be map of X,R^1;
assume A1: f1 is continuous;
consider g1 being map of X,R^1 such that
A2: (for p being Point of X holds g1.p=0) & g1 is continuous
by JGRAPH_2:30;
consider g2 being map of X,R^1
such that A3: (for p being Point of X,r1,r2 being real number st
g1.p=r1 & f1.p=r2 holds g2.p=r1-r2) & g2 is continuous
by A1,A2,JGRAPH_2:31;
for p being Point of X,r1 being real number st
f1.p=r1 holds g2.p=-r1
proof let p be Point of X,r1 be real number;
assume A4: f1.p=r1;
g1.p=0 by A2;
then g2.p=0-r1 by A3,A4;
hence g2.p=-r1 by XCMPLX_1:150;
end;
hence thesis by A3;
end;
theorem Th14: for X being non empty TopSpace,
f1,f2 being map of X,R^1,a,b being real number st f1 is continuous &
f2 is continuous & b<>0 & (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(abs(1-((r1/r2-a)/b)^2))))
& g is continuous
proof let X be non empty TopSpace,
f1,f2 be map of X,R^1,a,b being real number;
assume A1: f1 is continuous & f2 is continuous & b<>0 &
(for q being Point of X holds f2.q<>0);
then consider g1 being map of X,R^1 such that
A2: (for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g1.p=(r1/r2-a)/b) & g1 is continuous
by Th9;
consider g2 being map of X,R^1 such that
A3: (for p being Point of X,s being real number st
g1.p=s holds g2.p=s^2) & g2 is continuous by A2,Th11;
consider g0 being map of X,R^1 such that
A4: (for p being Point of X
holds g0.p=1)& g0 is continuous by JGRAPH_2:30;
consider g3 being map of X,R^1 such that
A5: (for p being Point of X,s,t being real number st
g0.p=s & g2.p=t holds g3.p=s-t)
& g3 is continuous by A3,A4,JGRAPH_2:31;
consider g4 being map of X,R^1 such that
A6: (for p being Point of X,s being real number st
g3.p=s holds g4.p=abs s)
& g4 is continuous by A5,Th12;
for q being Point of X ex r being real number st g4.q=r & r>=0
proof let q be Point of X;
reconsider s=g3.q as Real by TOPMETR:24;
A7: g4.q=abs s by A6;
abs s>=0 by ABSVALUE:5;
hence ex r being real number st g4.q=r & r>=0 by A7;
end;
then consider g5 being map of X,R^1 such that
A8: (for p being Point of X,s being real number st
g4.p=s holds g5.p=sqrt(s))
& g5 is continuous by A6,JGRAPH_3:15;
consider g6 being map of X,R^1 such that
A9: (for p being Point of X,s being real number st
g5.p=s holds g6.p=-s) & g6 is continuous by A8,Th13;
consider g7 being map of X,R^1
such that A10: (for p being Point of X,r1,r0 being real number st
f2.p=r1 & g6.p=r0 holds g7.p=r1*r0) & g7 is continuous
by A1,A9,JGRAPH_2:35;
for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g7.p= r2*(-sqrt(abs(1-((r1/r2-a)/b)^2)))
proof let p be Point of X,r1,r2 be real number;
assume A11: f1.p=r1 & f2.p=r2;
A12: g0.p=1 by A4;
g1.p=(r1/r2-a)/b by A2,A11;
then g2.p=((r1/r2-a)/b)^2 by A3;
then g3.p=1-((r1/r2-a)/b)^2 by A5,A12;
then g4.p= abs(1-((r1/r2-a)/b)^2) by A6;
then g5.p=sqrt(abs(1-((r1/r2-a)/b)^2)) by A8;
then g6.p= -sqrt(abs(1-((r1/r2-a)/b)^2)) by A9;
hence g7.p=r2*(-sqrt(abs(1-((r1/r2-a)/b)^2))) by A10,A11;
end;
hence thesis by A10;
end;
theorem Th15: for X being non empty TopSpace,
f1,f2 being map of X,R^1,a,b being real number st
f1 is continuous &
f2 is continuous & b<>0 & (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(abs(1-((r1/r2-a)/b)^2))))
& g is continuous
proof let X be non empty TopSpace,
f1,f2 be map of X,R^1,a,b being real number;
assume A1: f1 is continuous &
f2 is continuous & b<>0 & (for q being Point of X holds f2.q<>0);
then consider g1 being map of X,R^1 such that
A2: (for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g1.p=(r1/r2-a)/b) & g1 is continuous
by Th9;
consider g2 being map of X,R^1 such that
A3: (for p being Point of X,s being real number st
g1.p=s holds g2.p=s^2) & g2 is continuous by A2,Th11;
consider g0 being map of X,R^1 such that
A4: (for p being Point of X
holds g0.p=1)& g0 is continuous by JGRAPH_2:30;
consider g3 being map of X,R^1 such that
A5: (for p being Point of X,s,t being real number st
g0.p=s & g2.p=t holds g3.p=s-t)
& g3 is continuous by A3,A4,JGRAPH_2:31;
consider g4 being map of X,R^1 such that
A6: (for p being Point of X,s being real number st
g3.p=s holds g4.p=abs s)
& g4 is continuous by A5,Th12;
for q being Point of X ex r being real number st g4.q=r & r>=0
proof let q be Point of X;
reconsider s=g3.q as Real by TOPMETR:24;
A7: g4.q=abs s by A6;
abs s>=0 by ABSVALUE:5;
hence ex r being real number st g4.q=r & r>=0 by A7;
end;
then consider g5 being map of X,R^1 such that
A8: (for p being Point of X,s being real number st
g4.p=s holds g5.p=sqrt(s))
& g5 is continuous by A6,JGRAPH_3:15;
consider g7 being map of X,R^1
such that A9: (for p being Point of X,r1,r0 being real number st
f2.p=r1 & g5.p=r0 holds g7.p=r1*r0) & g7 is continuous
by A1,A8,JGRAPH_2:35;
for p being Point of X,r1,r2 being real number st
f1.p=r1 & f2.p=r2 holds g7.p= r2*( sqrt(abs(1-((r1/r2-a)/b)^2)))
proof let p be Point of X,r1,r2 be real number;
assume A10: f1.p=r1 & f2.p=r2;
A11: g0.p=1 by A4;
g1.p=(r1/r2-a)/b by A2,A10;
then g2.p=((r1/r2-a)/b)^2 by A3;
then g3.p=1-((r1/r2-a)/b)^2 by A5,A11;
then g4.p= abs(1-((r1/r2-a)/b)^2) by A6;
then g5.p=sqrt(abs(1-((r1/r2-a)/b)^2)) by A8;
hence g7.p=r2*( sqrt(abs(1-((r1/r2-a)/b)^2))) by A9,A10;
end;
hence thesis by A9;
end;
definition let n be Nat;
func n NormF -> Function of the carrier of TOP-REAL n, the carrier of R^1
means
:Def1: for q being Point of TOP-REAL n holds
it.q=|.q.|;
existence
proof
deffunc F(Point of TOP-REAL n)=|.$1.|;
A1: for x being Element of TOP-REAL n holds
F(x) in the carrier of R^1 by TOPMETR:24;
thus ex IT being Function of the carrier of TOP-REAL n, the carrier of R^1
st for q being Point of TOP-REAL n holds
IT.q = F(q) from FunctR_ealEx(A1);
end;
uniqueness
proof
deffunc F(Point of TOP-REAL n)=|.$1.|;
thus
for f,g being Function of the carrier of TOP-REAL n, the carrier of R^1
st (for q being Point of TOP-REAL n holds f.q=F(q)) &
(for q being Point of TOP-REAL n holds g.q=F(q))
holds f=g from FuncDefUniq;
end;
end;
theorem Th16: for n being Nat holds
dom (n NormF)=the carrier of TOP-REAL n & dom (n NormF)=REAL n
proof let n be Nat;
thus dom (n NormF)=the carrier of TOP-REAL n by FUNCT_2:def 1;
hence thesis by EUCLID:25;
end;
canceled 2;
theorem Th19:for n being Nat,f being map of TOP-REAL n,R^1 st f=n NormF
holds f is continuous
proof let n be Nat,f be map of TOP-REAL n,R^1;
assume A1: f=n NormF;
for p being Point of TOP-REAL n,V being Subset of R^1
st f.p in V & V is open holds
ex W being Subset of TOP-REAL n st p in W & W is open & f.:W c= V
proof let p be Point of TOP-REAL n,V be Subset of R^1;
assume A2: f.p in V & V is open;
reconsider v=p as Point of Euclid n by TOPREAL3:13;
reconsider u=f.p as Point of RealSpace by METRIC_1:def 14,TOPMETR:24;
reconsider u'=f.p as Real by TOPMETR:24;
A3: f.p=|.p.| by A1,Def1;
consider r being real number such that
A4: r>0 & Ball(u,r) c= V by A2,TOPMETR:22,def 7;
reconsider r as Real by XREAL_0:def 1;
A5: Ball(v,r)={q where q is Point of TOP-REAL n:
|. p-q .| < r} by JGRAPH_2:10;
defpred P[Point of TOP-REAL n] means |. p-$1 .| < r;
{q where q is Point of TOP-REAL n: P[q]}
is Subset of TOP-REAL n from SubsetD;
then reconsider W1=Ball(v,r) as Subset of TOP-REAL n by A5;
A6: v in W1 by A4,GOBOARD6:4;
A7: W1 is open by GOBOARD6:6;
f.:W1 c= Ball(u,r)
proof let y be set;assume y in f.:W1;
then consider x being set such that
A8: x in dom f & x in W1 & y=f.x by FUNCT_1:def 12;
reconsider q=x as Point of TOP-REAL n by A8;
consider q1 being Point of TOP-REAL n such that
A9: q=q1 & |. p-q1 .| < r by A5,A8;
A10: f.x=|.q.| by A1,Def1;
A11: Ball(u,r)=].u'-r,u'+r.[ by A4,FRECHET:7;
abs(|.p.|-(|.q.|))<= |. p-q .| by JORDAN2C:11;
then abs(u'-(|.q.|))<r by A3,A9,AXIOMS:22;
then A12: -r < u'-(|.q.|) & u'-(|.q.|)<r by SEQ_2:9;
then A13: u'-(u'-(|.q.|))>u'-r by REAL_1:92;
u'>|.q.|+-r by A12,REAL_1:86;
then u' --r > |.q.| +-r--r by REAL_1:54;
then u' +--r > |.q.| +-r--r by XCMPLX_0:def 8;
then u'-r<|.q.| & |.q.|<u'+r by A13,XCMPLX_1:18,26;
hence y in Ball(u,r) by A8,A10,A11,JORDAN6:45;
end;
then f.:W1 c= V by A4,XBOOLE_1:1;
hence thesis by A6,A7;
end;
hence f is continuous by JGRAPH_2:20;
end;
theorem Th20: for n being Nat,K0 being Subset of TOP-REAL n,
f being map of (TOP-REAL n)|K0,R^1 st
(for p being Point of (TOP-REAL n)|K0 holds
f.p=(n NormF).p) holds f is continuous
proof let n be Nat,K0 be Subset of TOP-REAL n,
f be map of (TOP-REAL n)|K0,R^1;
assume A1: (for p being Point of (TOP-REAL n)|K0 holds f.p=(n NormF).p);
A2:dom f= the carrier of (TOP-REAL n)|K0 by FUNCT_2:def 1;
A3: the carrier of (TOP-REAL n)|K0=K0 by JORDAN1:1;
(the carrier of TOP-REAL n)/\K0=K0 by XBOOLE_1:28;
then A4:dom f=dom (n NormF) /\ K0 by A2,A3,Th16;
A5:for x being set st x in dom f holds f.x=(n NormF).x by A1,A2;
reconsider g=(n NormF) as map of TOP-REAL n,R^1 ;
A6:f=g|K0 by A4,A5,FUNCT_1:68;
g is continuous by Th19;
hence f is continuous by A6,TOPMETR:10;
end;
theorem Th21: for n being Nat,p being Point of Euclid n,r being Real,
B being Subset of TOP-REAL n st B=cl_Ball(p,r)
holds B is Bounded & B is closed
proof let n be Nat,p be Point of Euclid n,r be Real,
B be Subset of TOP-REAL n;
assume A1: B=cl_Ball(p,r);
A2: TOP-REAL n=TopSpaceMetr(Euclid n) by EUCLID:def 8;
A3: cl_Ball(p,r) c= Ball(p,r+1)
proof let x be set;assume A4: x in cl_Ball(p,r);
then reconsider q=x as Point of Euclid n;
A5: dist(p,q)<=r by A4,METRIC_1:13;
r<r+1 by REAL_1:69;
then dist(p,q)<r+1 by A5,AXIOMS:22;
hence x in Ball(p,r+1) by METRIC_1:12;
end;
Ball(p,r+1) is bounded by TBSP_1:19;
then cl_Ball(p,r) is bounded by A3,TBSP_1:21;
hence B is Bounded by A1,JORDAN2C:def 2;
thus B is closed by A1,A2,TOPREAL6:65;
end;
theorem Th22: for p being Point of Euclid 2,r being Real,
B being Subset of TOP-REAL 2 st B=cl_Ball(p,r)
holds B is compact
proof let p be Point of Euclid 2,r be Real,
B be Subset of TOP-REAL 2;
assume B=cl_Ball(p,r);
then B is Bounded & B is closed by Th21;
hence B is compact by TOPREAL6:88;
end;
begin :: Fan Morphism for West
definition let s be real number, q be Point of TOP-REAL 2;
func FanW(s,q) -> Point of TOP-REAL 2 equals
:Def2: |.q.|*|[-sqrt(1-((q`2/|.q.|-s)/(1-s))^2),
(q`2/|.q.|-s)/(1-s)]| if q`2/|.q.|>=s & q`1<0,
|.q.|*|[-sqrt(1-((q`2/|.q.|-s)/(1+s))^2),
(q`2/|.q.|-s)/(1+s)]| if q`2/|.q.|<s & q`1<0
otherwise q;
correctness;
end;
definition let s be real number;
func s-FanMorphW -> Function of the carrier of TOP-REAL 2,
the carrier of TOP-REAL 2 means
:Def3: for q being Point of TOP-REAL 2 holds
it.q=FanW(s,q);
existence
proof
deffunc F(Point of TOP-REAL 2)=FanW(s,$1);
thus ex IT being Function of the carrier of TOP-REAL 2,
the carrier of TOP-REAL 2 st
for q being Point of TOP-REAL 2 holds
IT.q=F(q) from LambdaD;
end;
uniqueness
proof
deffunc F(Point of TOP-REAL 2)=FanW(s,$1);
thus for f,g being Function of the carrier of TOP-REAL 2,
the carrier of TOP-REAL 2 st
(for q being Point of TOP-REAL 2 holds f.q=F(q)) &
(for q being Point of TOP-REAL 2 holds g.q=F(q)) holds f=g
from FuncDefUniq;
end;
end;
theorem Th23: for sn being real number holds
(q`2/|.q.|>=sn & q`1<0 implies
sn-FanMorphW.q= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)),
|.q.|* ((q`2/|.q.|-sn)/(1-sn))]|) &
(q`1>=0 implies sn-FanMorphW.q=q)
proof let sn be real number;
A1: sn-FanMorphW.q=FanW(sn,q) by Def3;
hereby assume q`2/|.q.|>=sn & q`1<0;
then FanW(sn,q)= |.q.|*|[-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2),
(q`2/|.q.|-sn)/(1-sn)]| by Def2
.= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)),
|.q.|* ((q`2/|.q.|-sn)/(1-sn))]| by EUCLID:62;
hence sn-FanMorphW.q= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)),
|.q.|* ((q`2/|.q.|-sn)/(1-sn))]| by Def3;
end;
assume q`1>=0; hence thesis by A1,Def2;
end;
theorem Th24: for sn being Real holds
(q`2/|.q.|<=sn & q`1<0 implies
sn-FanMorphW.q= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)),
|.q.|*((q`2/|.q.|-sn)/(1+sn))]|)
proof let sn be Real;
assume A1: q`2/|.q.|<=sn & q`1<0;
now per cases by A1,REAL_1:def 5;
case q`2/|.q.|<sn;
then FanW(sn,q)= |.q.|*|[-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2),
(q`2/|.q.|-sn)/(1+sn)]| by A1,Def2
.= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)),
|.q.|* ((q`2/|.q.|-sn)/(1+sn))]| by EUCLID:62;
hence sn-FanMorphW.q= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)),
|.q.|*((q`2/|.q.|-sn)/(1+sn))]| by Def3;
case A2: q`2/|.q.|=sn;
then A3: q`2/|.q.|-sn=0 by XCMPLX_1:14;
then (q`2/|.q.|-sn)/(1-sn)=0;
hence sn-FanMorphW.q= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)),
|.q.|*((q`2/|.q.|-sn)/(1+sn))]| by A1,A2,A3,Th23;
end;
hence thesis;
end;
theorem Th25: for sn being Real st -1<sn & sn<1 holds
(q`2/|.q.|>=sn & q`1<=0 & q<>0.REAL 2 implies
sn-FanMorphW.q= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)),
|.q.|* ((q`2/|.q.|-sn)/(1-sn))]|) &
(q`2/|.q.|<=sn & q`1<=0 & q<>0.REAL 2 implies
sn-FanMorphW.q= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)),
|.q.|*((q`2/|.q.|-sn)/(1+sn))]|)
proof let sn be Real;
assume A1: -1<sn & sn<1;
now per cases;
case A2: q`2/|.q.|>=sn & q`1<=0 & q<>0.REAL 2;
now per cases;
case A3: q`1<0;
then FanW(sn,q)= |.q.|*|[-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2),
(q`2/|.q.|-sn)/(1-sn)]| by A2,Def2
.= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)),
|.q.|* ((q`2/|.q.|-sn)/(1-sn))]| by EUCLID:62;
hence thesis by A3,Def3,Th24;
case A4: q`1>=0;
then A5: sn-FanMorphW.q=q by Th23;
A6: (|.q.|)^2 =(q`1)^2+(q`2)^2 by JGRAPH_3:10;
A7: |.q.|<>0 by A2,TOPRNS_1:25;
then A8: |.q.|^2>0 by SQUARE_1:74;
A9: q`1=0 by A2,A4;
|.q.|>=0 by TOPRNS_1:26;
then A10: sqrt((|.q.|)^2)=|.q.| by SQUARE_1:89;
A11: 1-sn>0 by A1,Th3;
A12: |.q.|>0 by A2,Lm1;
(q`2)^2/|.q.|^2=1^2 by A6,A8,A9,SQUARE_1:59,60,XCMPLX_1:60;
then ((q`2)/|.q.|)^2=1^2 by SQUARE_1:69;
then A13: sqrt(((q`2)/|.q.|)^2)=1 by SQUARE_1:89;
now assume q`2<0;
then q`2/|.q.|<0 by A12,REAL_2:128;
then -((q`2)/|.q.|)=1 by A13,SQUARE_1:90;
hence contradiction by A1,A2;
end;
then A14: |.q.|=q`2 by A6,A9,A10,SQUARE_1:60,89;
then 1=q`2/|.q.| by A7,XCMPLX_1:60;
then (q`2/|.q.|-sn)/(1-sn)=1 by A11,XCMPLX_1:60;
hence thesis by A1,A5,A7,A9,A14,EUCLID:57,SQUARE_1:59,82,XCMPLX_1:60;
end;
hence thesis;
case A15: q`2/|.q.|<=sn & q`1<=0 & q<>0.REAL 2;
now per cases;
case q`1<0;
hence thesis by Th23,Th24;
case A16: q`1>=0;
A17: (|.q.|)^2 =(q`1)^2+(q`2)^2 by JGRAPH_3:10;
A18: |.q.|<>0 by A15,TOPRNS_1:25;
A19: q`1=0 by A15,A16;
A20: |.q.|>0 by A15,Lm1;
A21: 1+sn>0 by A1,Th3;
1-sn>0 by A1,Th3;
then 1-sn+sn>0+sn by REAL_1:53;
then 1>sn by XCMPLX_1:27;
then 1>q`2/|.q.| by A15,AXIOMS:22;
then (1)*(|.q.|)>q`2/|.q.|*(|.q.|) by A20,REAL_1:70;
then A22: (|.q.|)>q`2 by A18,XCMPLX_1:88;
then A23: |.q.|=-q`2 by A17,A19,JGRAPH_3:1,SQUARE_1:60;
A24: q`2= -(|.q.|) by A17,A19,A22,JGRAPH_3:1,SQUARE_1:60;
then -1=q`2/|.q.| by A18,XCMPLX_1:198;
then (q`2/|.q.|-sn)/(1+sn)
=(-(1+sn))/(1+sn) by XCMPLX_1:161 .=-1 by A21,XCMPLX_1:198;
then |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)),
|.q.|* ((q`2/|.q.|-sn)/(1+sn))]|
=|[ |.q.|*(-sqrt(1-1)),|.q.|*(-1)]| by SQUARE_1:59,61
.=|[ |.q.|*(0),-(|.q.|)]| by SQUARE_1:82,XCMPLX_1:180
.=q by A19,A23,EUCLID:57;
hence thesis by A1,A16,A18,A24,Th23,XCMPLX_1:198;
end;
hence thesis;
case q`1>0 or q=0.REAL 2;
hence thesis;
end;
hence thesis;
end;
Lm2: for K being non empty Subset of TOP-REAL 2 holds
proj1|K is continuous map of (TOP-REAL 2)|K,R^1 &
for q being Point of (TOP-REAL 2)|K holds (proj1|K).q=proj1.q
proof
let K be non empty Subset of TOP-REAL 2;
A1: the carrier of (TOP-REAL 2)|K=K by JORDAN1:1;
proj1|K is Function of K,the carrier of R^1 by FUNCT_2:38,TOPMETR:24;
then reconsider g2=proj1|K as map of (TOP-REAL 2)|K,R^1 by A1;
for q being Point of (TOP-REAL 2)|K holds g2.q=proj1.q
proof let q be Point of (TOP-REAL 2)|K;
A2:q in the carrier of (TOP-REAL 2)|K;
dom proj1=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then q in dom proj1 /\ K by A1,A2,XBOOLE_0:def 3;
hence g2.q=proj1.q by FUNCT_1:71;
end;
hence thesis by JGRAPH_2:39;
end;
Lm3: for K being non empty Subset of TOP-REAL 2 holds
proj2|K is continuous map of (TOP-REAL 2)|K,R^1 &
for q being Point of (TOP-REAL 2)|K holds (proj2|K).q=proj2.q
proof
let K be non empty Subset of TOP-REAL 2;
A1: the carrier of (TOP-REAL 2)|K=K by JORDAN1:1;
proj2|K is Function of K,the carrier of R^1 by FUNCT_2:38,TOPMETR:24;
then reconsider g2=proj2|K as map of (TOP-REAL 2)|K,R^1 by A1;
for q being Point of (TOP-REAL 2)|K holds g2.q=proj2.q
proof let q be Point of (TOP-REAL 2)|K;
A2:q in the carrier of (TOP-REAL 2)|K;
dom proj2=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then q in dom proj2 /\ K by A1,A2,XBOOLE_0:def 3;
hence g2.q=proj2.q by FUNCT_1:71;
end;
hence thesis by JGRAPH_2:40;
end;
Lm4: dom (2 NormF)=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
Lm5: for K being non empty Subset of TOP-REAL 2 holds
(2 NormF)|K is continuous map of (TOP-REAL 2)|K,R^1 &
(for q being Point of (TOP-REAL 2)|K holds ((2 NormF)|K).q=(2 NormF).q)
proof
let K1 be non empty Subset of TOP-REAL 2;
A1:the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
(2 NormF)|K1 is Function of K1,the carrier of R^1 by FUNCT_2:38;
then reconsider g1=(2 NormF)|K1 as map of (TOP-REAL 2)|K1,R^1 by A1;
for q being Point of (TOP-REAL 2)|K1 holds g1.q=(2 NormF).q
proof let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1;
then q in dom (2 NormF) /\ K1 by A1,Lm4,XBOOLE_0:def 3;
hence g1.q=(2 NormF).q by FUNCT_1:71;
end;
hence thesis by Th20;
end;
Lm6:
for K1 be non empty Subset of TOP-REAL 2,
g1 be map of (TOP-REAL 2)|K1,R^1 st g1=(2 NormF)|K1 &
(for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q<>0.REAL 2) holds
for q being Point of (TOP-REAL 2)|K1 holds g1.q<>0
proof
let K1 be non empty Subset of TOP-REAL 2,
g1 be map of (TOP-REAL 2)|K1,R^1;
A1: the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
assume A2: g1=(2 NormF)|K1 & (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q<>0.REAL 2);
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 A1;
A3: g1.q=(2 NormF).q by A2,Lm5 .= |.q2.| by Def1;
now assume |.q2.|=0; then q2=0.REAL 2 by TOPRNS_1:25;
hence contradiction by A2;
end;
hence g1.q<>0 by A3;
end;
theorem Th26:
for sn being Real,K1 being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K1,R^1 st -1<sn & sn<1 &
(for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1
holds f.p=|.p.|* ((p`2/|.p.|-sn)/(1-sn)))
& (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`1<=0 & q<>0.REAL 2) holds
f is continuous
proof
let sn be Real,K1 be non empty Subset of TOP-REAL 2,
f be map of (TOP-REAL 2)|K1,R^1;
assume A1: -1<sn & sn<1 &
(for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1
holds f.p=|.p.|* ((p`2/|.p.|-sn)/(1-sn)))
& (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`1<=0 & q<>0.REAL 2);
set a=sn, b=(1-sn);
A2: b>0 by A1,Th3;
reconsider g2=proj2|K1 as continuous map of (TOP-REAL 2)|K1,R^1 by Lm3;
reconsider g1=(2 NormF)|K1 as continuous map of (TOP-REAL 2)|K1,R^1
by Lm5;
for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q<>0.REAL 2 by A1;
then for q being Point of (TOP-REAL 2)|K1 holds g1.q<>0 by Lm6;
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 st g2.q=r1 & g1.q=r2
holds g3.q=r2*((r1/r2-a)/b)) & g3 is continuous by A2,Th10;
A4:dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then A5: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
A6: x in dom f;
then x in K1 by A4,A5,JORDAN1:1;
then reconsider r=x as Point of TOP-REAL 2;
reconsider s=x as Point of (TOP-REAL 2)|K1 by A6,FUNCT_2:def 1;
A7:f.r=(|.r.|)* ((r`2/|.r.|-sn)/(1-sn)) by A1,A4,A5,A6;
A8:g2.s=proj2.s by Lm3;
A9:g1.s=(2 NormF).s by Lm5;
A10:proj2.r=r`2 by PSCOMP_1:def 29;
(2 NormF).r=|.r.| by Def1;
hence f.x=g3.x by A3,A7,A8,A9,A10;
end;
hence f is continuous by A3,A5,FUNCT_1:9;
end;
theorem Th27:
for sn being Real,K1 being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K1,R^1 st -1<sn & sn<1 &
(for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1
holds f.p=|.p.|* ((p`2/|.p.|-sn)/(1+sn)))
& (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`1<=0 & q<>0.REAL 2) holds
f is continuous
proof
let sn be Real,K1 be non empty Subset of TOP-REAL 2,
f be map of (TOP-REAL 2)|K1,R^1;
assume A1:
-1<sn & sn<1 &
(for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1
holds f.p=|.p.|* ((p`2/|.p.|-sn)/(1+sn)))
& (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`1<=0 & q<>0.REAL 2);
set a=sn, b=(1+sn);
A2: 1+sn>0 by A1,Th3;
reconsider g2=proj2|K1 as continuous map of (TOP-REAL 2)|K1,R^1 by Lm3;
reconsider g1=(2 NormF)|K1 as continuous map of (TOP-REAL 2)|K1,R^1
by Lm5;
for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q<>0.REAL 2 by A1;
then for q being Point of (TOP-REAL 2)|K1 holds g1.q<>0 by Lm6;
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 st g2.q=r1 & g1.q=r2
holds g3.q=r2*((r1/r2-a)/b)) & g3 is continuous by A2,Th10;
A4:dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then A5: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
A6: x in dom f; then A7: x in dom g3 by A4,FUNCT_2:def 1;
then x in K1 by A4,JORDAN1:1;
then reconsider r=x as Point of (TOP-REAL 2);
reconsider s=x as Point of (TOP-REAL 2)|K1 by A6,FUNCT_2:def 1;
A8:f.r=(|.r.|)* ((r`2/|.r.|-sn)/(1+sn)) by A1,A4,A7;
A9:g2.s=proj2.s by Lm3;
A10:g1.s=(2 NormF).s by Lm5;
A11:proj2.r=r`2 by PSCOMP_1:def 29;
(2 NormF).r=|.r.| by Def1;
hence f.x=g3.x by A3,A8,A9,A10,A11;
end;
hence f is continuous by A3,A5,FUNCT_1:9;
end;
theorem Th28:
for sn being Real,K1 being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K1,R^1 st -1<sn & sn<1 &
(for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1
holds f.p=|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2)))
& (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds
q`1<=0 & q`2/|.q.|>=sn & q<>0.REAL 2) holds
f is continuous
proof
let sn be Real,K1 be non empty Subset of TOP-REAL 2,
f be map of (TOP-REAL 2)|K1,R^1;
assume A1: -1<sn & sn<1 &
(for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1
holds f.p=|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2)))
& (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds
q`1<=0 & q`2/|.q.|>=sn & q<>0.REAL 2);
set a=sn, b=(1-sn);
A2: b>0 by A1,Th3;
reconsider g2=proj2|K1 as continuous map of (TOP-REAL 2)|K1,R^1 by Lm3;
reconsider g1=(2 NormF)|K1 as continuous map of (TOP-REAL 2)|K1,R^1
by Lm5;
for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q<>0.REAL 2 by A1;
then for q being Point of (TOP-REAL 2)|K1 holds g1.q<>0 by Lm6;
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(abs(1-((r1/r2-a)/b)^2))))
& g3 is continuous by A2,Th14;
A4:dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then A5: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
A6: x in dom f;
then x in K1 by A4,A5,JORDAN1:1;
then reconsider r=x as Point of (TOP-REAL 2);
reconsider s=x as Point of (TOP-REAL 2)|K1 by A6,FUNCT_2:def 1;
A7: now assume |.r.|=0; then r=0.REAL 2 by TOPRNS_1:25;
hence contradiction by A1,A4,A5,A6;
end;
A8: |.r.|>=0 by TOPRNS_1:26;
|.r.|^2=(r`1)^2+(r`2)^2 by JGRAPH_3:10;
then |.r.|^2 -(r`2)^2 =(r`1)^2 by XCMPLX_1:26;
then (r`2)^2 -(|.r.|)^2 =-(r`1)^2 by XCMPLX_1:143;
then A9: ((r`2) -(|.r.|))*((r`2)+|.r.|) =-(r`1)^2 by SQUARE_1:67;
(r`1)^2>=0 by SQUARE_1:72;
then -(r`1)^2 <=0 by REAL_1:66;
then -(|.r.|)<=r`2 & r`2<= |.r.| by A8,A9,JGRAPH_3:4;
then r`2/|.r.| <= |.r.|/|.r.| by A7,A8,REAL_1:73;
then r`2/|.r.|<=1 by A7,XCMPLX_1:60;
then A10: r`2/|.r.|-sn<=(1-sn) by REAL_1:49;
A11: now assume (1-sn)^2=0;
then 1-sn+sn=0+sn by SQUARE_1:73;
hence contradiction by A1,XCMPLX_1:27;
end;
A12: 1-sn>0 by A1,Th3;
A13: (1-sn)^2>=0 by SQUARE_1:72;
sn<=r`2/(|.r.|) by A1,A4,A5,A6;
then sn-r`2/|.r.|<=0 by REAL_2:106;
then -(sn- r`2/|.r.|)>=-(1-sn) by A12,REAL_1:50;
then -(1-sn)<= r`2/|.r.|-sn by XCMPLX_1:143;
then (r`2/|.r.|-sn)^2<=(1-sn)^2 by A10,JGRAPH_2:7;
then (r`2/|.r.|-sn)^2/(1-sn)^2<=(1-sn)^2/(1-sn)^2 by A11,A13,REAL_1:73;
then (r`2/|.r.|-sn)^2/(1-sn)^2<=1 by A11,XCMPLX_1:60;
then ((r`2/|.r.|-sn)/(1-sn))^2<=1 by SQUARE_1:69;
then 1-((r`2/|.r.|-sn)/(1-sn))^2>=0 by SQUARE_1:12;
then abs(1-((r`2/|.r.|-sn)/(1-sn))^2)
=1-((r`2/|.r.|-sn)/(1-sn))^2 by ABSVALUE:def 1;
then A14:f.r=(|.r.|)*(-sqrt(abs(1-((r`2/|.r.|-sn)/(1-sn))^2))) by A1,A4,A5
,A6;
A15:g2.s=proj2.s by Lm3;
A16:g1.s=(2 NormF).s by Lm5;
A17:proj2.r=r`2 by PSCOMP_1:def 29;
(2 NormF).r=|.r.| by Def1;
hence f.x=g3.x by A3,A14,A15,A16,A17;
end;
hence f is continuous by A3,A5,FUNCT_1:9;
end;
theorem Th29:
for sn being Real,K1 being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K1,R^1 st -1<sn & sn<1 &
(for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1
holds f.p=|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2)))
& (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds
q`1<=0 & q`2/|.q.|<=sn & q<>0.REAL 2) holds
f is continuous
proof
let sn be Real,K1 be non empty Subset of TOP-REAL 2,
f be map of (TOP-REAL 2)|K1,R^1;
assume A1: -1<sn & sn<1 &
(for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1
holds f.p=|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2)))
& (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds
q`1<=0 & q`2/|.q.|<=sn & q<>0.REAL 2);
set a=sn, b=(1+sn);
A2: 1+sn>0 by A1,Th3;
reconsider g2=proj2|K1 as continuous map of (TOP-REAL 2)|K1,R^1 by Lm3;
reconsider g1=(2 NormF)|K1 as continuous map of (TOP-REAL 2)|K1,R^1
by Lm5;
for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q<>0.REAL 2 by A1;
then for q being Point of (TOP-REAL 2)|K1 holds g1.q<>0 by Lm6;
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(abs(1-((r1/r2-a)/b)^2))))
& g3 is continuous by A2,Th14;
A4:dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then A5: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
A6:x in dom f;
then x in K1 by A4,A5,JORDAN1:1;
then reconsider r=x as Point of (TOP-REAL 2);
reconsider s=x as Point of (TOP-REAL 2)|K1 by A6,FUNCT_2:def 1;
A7: now assume |.r.|=0; then r=0.REAL 2 by TOPRNS_1:25;
hence contradiction by A1,A4,A5,A6;
end;
A8: |.r.|>=0 by TOPRNS_1:26;
|.r.|^2=(r`1)^2+(r`2)^2 by JGRAPH_3:10;
then |.r.|^2 -(r`2)^2 =(r`1)^2 by XCMPLX_1:26;
then (r`2)^2 -(|.r.|)^2 =-(r`1)^2 by XCMPLX_1:143;
then A9: ((r`2) -(|.r.|))*((r`2)+|.r.|) =-(r`1)^2 by SQUARE_1:67;
(r`1)^2>=0 by SQUARE_1:72;
then -(r`1)^2 <=0 by REAL_1:66;
then -(|.r.|)<=r`2 & r`2<= |.r.| by A8,A9,JGRAPH_3:4;
then r`2/|.r.| >= (-(|.r.|))/|.r.| by A7,A8,REAL_1:73;
then r`2/|.r.|>= -1 by A7,XCMPLX_1:198;
then r`2/|.r.|-sn>=-1-sn by REAL_1:49;
then A10: r`2/|.r.|-sn>=-(1+sn) by XCMPLX_1:161;
A11: (1+sn)^2>0 by A2,SQUARE_1:74;
sn>=r`2/(|.r.|) by A1,A4,A5,A6;
then sn-r`2/|.r.|>=0 by SQUARE_1:12;
then -(sn-r`2/|.r.|)<=-0 by REAL_1:50;
then r`2/|.r.|-sn<=-0 by XCMPLX_1:143;
then r`2/|.r.|-sn<=1+sn by A2,AXIOMS:22;
then (r`2/|.r.|-sn)^2<=(1+sn)^2 by A10,JGRAPH_2:7;
then (r`2/|.r.|-sn)^2/(1+sn)^2<=(1+sn)^2/(1+sn)^2 by A11,REAL_1:73;
then (r`2/|.r.|-sn)^2/(1+sn)^2<=1 by A11,XCMPLX_1:60;
then ((r`2/|.r.|-sn)/(1+sn))^2<=1 by SQUARE_1:69;
then 1-((r`2/|.r.|-sn)/(1+sn))^2>=0 by SQUARE_1:12;
then abs(1-((r`2/|.r.|-sn)/(1+sn))^2)
=1-((r`2/|.r.|-sn)/(1+sn))^2 by ABSVALUE:def 1;
then A12:f.r=(|.r.|)*(-sqrt(abs(1-((r`2/|.r.|-sn)/(1+sn))^2))) by A1,A4,A5
,A6;
A13:g2.s=proj2.s by Lm3;
A14:g1.s=(2 NormF).s by Lm5;
A15:proj2.r=r`2 by PSCOMP_1:def 29;
(2 NormF).r=|.r.| by Def1;
hence f.x=g3.x by A3,A12,A13,A14,A15;
end;
hence f is continuous by A3,A5,FUNCT_1:9;
end;
theorem Th30: for sn being Real,
K0,B0 being Subset of TOP-REAL 2,f being
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0
st -1<sn & sn<1 & f=(sn-FanMorphW)|K0 &
B0={q where q is Point of TOP-REAL 2: q`1<=0 & q<>0.REAL 2}
& K0={p: p`2/|.p.|>=sn & p`1<=0 & p<>0.REAL 2}
holds f is continuous
proof let sn be Real,K0,B0 be Subset of TOP-REAL 2,f be
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0;
assume A1: -1<sn & sn<1 & f=(sn-FanMorphW)|K0 &
B0={q where q is Point of TOP-REAL 2: q`1<=0 & q<>0.REAL 2} &
K0={p: p`2/|.p.|>=sn & p`1<=0 & p<>0.REAL 2};
set cn=sqrt(1-sn^2);
set p0=|[-cn,sn]|;
A2: p0`2=sn by EUCLID:56;
A3: p0`1=-cn by EUCLID:56;
sn^2<1^2 by A1,JGRAPH_2:8;
then A4: 1-sn^2>0 by SQUARE_1:11,59;
A5: now assume p0=0.REAL 2;
then --cn=-0 by EUCLID:56,JGRAPH_2:11;
hence contradiction by A4,SQUARE_1:93;
end;
--cn>0 by A4,SQUARE_1:93;
then A6: p0`1<0 by A3,REAL_1:66;
A7: |.p0.|=sqrt((-cn)^2+sn^2) by A2,A3,JGRAPH_3:10
.=sqrt((cn)^2+sn^2) by SQUARE_1:61;
cn^2=1-sn^2 by A4,SQUARE_1:def 4;
then |.p0.|=1 by A7,SQUARE_1:83,XCMPLX_1:27;
then p0`2/|.p0.|=sn by EUCLID:56;
then A8: p0 in K0 by A1,A5,A6;
then reconsider K1=K0 as non empty Subset of TOP-REAL 2;
A9: K0 c= B0
proof let x be set;assume x in K0;
then consider p8 being Point of TOP-REAL 2 such that
A10: x=p8 & (p8`2/|.p8.|>=sn & p8`1<=0 & p8<>0.REAL 2) by A1;
thus x in B0 by A1,A10;
end;
A11:dom ((proj2)*((sn-FanMorphW)|K1)) c= dom ((sn-FanMorphW)|K1)
by RELAT_1:44;
dom ((sn-FanMorphW)|K1) c= dom ((proj2)*((sn-FanMorphW)|K1))
proof let x be set;assume A12:x in dom ((sn-FanMorphW)|K1);
then A13:x in dom (sn-FanMorphW) /\ K1 by FUNCT_1:68;
A14:((sn-FanMorphW)|K1).x=(sn-FanMorphW).x by A12,FUNCT_1:68;
A15: dom proj2 = (the carrier of TOP-REAL 2) by FUNCT_2:def 1;
x in dom (sn-FanMorphW) by A13,XBOOLE_0:def 3;
then (sn-FanMorphW).x in rng (sn-FanMorphW) by FUNCT_1:12;
hence x in dom ((proj2)*((sn-FanMorphW)|K1)) by A12,A14,A15,FUNCT_1:21;
end;
then A16:dom ((proj2)*((sn-FanMorphW)|K1))
=dom ((sn-FanMorphW)|K1) by A11,XBOOLE_0:def 10
.=dom (sn-FanMorphW) /\ 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;
A17:rng ((proj2)*((sn-FanMorphW)|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)*((sn-FanMorphW)|K1)) c= the carrier of R^1 by A17,XBOOLE_1:1
;
then (proj2)*((sn-FanMorphW)|K1) is Function of the carrier of (TOP-REAL 2)|K1
,
the carrier of R^1 by A16,FUNCT_2:4;
then reconsider g2=(proj2)*((sn-FanMorphW)|K1) as map of (TOP-REAL 2)|K1,R^1
;
A18:dom ((proj1)*((sn-FanMorphW)|K1))
c= dom ((sn-FanMorphW)|K1) by RELAT_1:44;
dom ((sn-FanMorphW)|K1) c= dom ((proj1)*((sn-FanMorphW)|K1))
proof let x be set;assume A19:x in dom ((sn-FanMorphW)|K1);
then A20:x in dom (sn-FanMorphW) /\ K1 by FUNCT_1:68;
A21:((sn-FanMorphW)|K1).x=(sn-FanMorphW).x by A19,FUNCT_1:68;
A22: dom proj1 = (the carrier of TOP-REAL 2) by FUNCT_2:def 1;
x in dom (sn-FanMorphW) by A20,XBOOLE_0:def 3;
then (sn-FanMorphW).x in rng (sn-FanMorphW) by FUNCT_1:12;
hence x in dom ((proj1)*((sn-FanMorphW)|K1)) by A19,A21,A22,FUNCT_1:21;
end;
then A23:dom ((proj1)*((sn-FanMorphW)|K1))
=dom ((sn-FanMorphW)|K1) by A18,XBOOLE_0:def 10
.=dom (sn-FanMorphW) /\ 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;
A24:rng ((proj1)*((sn-FanMorphW)|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)*((sn-FanMorphW)|K1)) c= the carrier of R^1 by A24,XBOOLE_1:1
;
then (proj1)*((sn-FanMorphW)|K1) is Function of the carrier of (TOP-REAL 2)|K1
,
the carrier of R^1 by A23,FUNCT_2:4;
then reconsider g1=(proj1)*((sn-FanMorphW)|K1) as map of (TOP-REAL 2)|K1,R^1
;
A25: for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`1<=0 & q<>0.REAL 2
proof let q be Point of TOP-REAL 2;
assume A26: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
A27: q=p3 & (p3`2/|.p3.|>=sn & p3`1<=0 & p3<>0.REAL 2) by A1,A26;
thus q`1<=0 & q<>0.REAL 2 by A27;
end;
for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds g2.p=|.p.|* ((p`2/|.p.|-sn)/(1-sn))
proof let p be Point of TOP-REAL 2;
assume A28: p in the carrier of (TOP-REAL 2)|K1;
A29:dom ((sn-FanMorphW)|K1)=dom (sn-FanMorphW) /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2))/\ K1 by FUNCT_2:def 1
.=K1 by XBOOLE_1:28;
A30:the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
then consider p3 being Point of TOP-REAL 2 such that
A31: p=p3 & (p3`2/|.p3.|>=sn & p3`1<=0 & p3<>0.REAL 2) by A1,A28;
A32:(sn-FanMorphW).p
=|[|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2)),
|.p.|* ((p`2/|.p.|-sn)/(1-sn))]| by A1,A31,Th25;
((sn-FanMorphW)|K1).p=(sn-FanMorphW).p by A28,A30,FUNCT_1:72;
then g2.p=(proj2).(|[|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2)),
|.p.|* ((p`2/|.p.|-sn)/(1-sn))]|)
by A28,A29,A30,A32,FUNCT_1:23
.=(|[|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2)),
|.p.|* ((p`2/|.p.|-sn)/(1-sn))]|)`2 by PSCOMP_1:def 29
.=|.p.|* ((p`2/|.p.|-sn)/(1-sn)) by EUCLID:56;
hence g2.p=|.p.|* ((p`2/|.p.|-sn)/(1-sn));
end;
then consider f2 being map of (TOP-REAL 2)|K1,R^1 such that
A33:for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f2.p=|.p.|* ((p`2/|.p.|-sn)/(1-sn));
A34:f2 is continuous by A1,A25,A33,Th26;
for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds g1.p=|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2))
proof let p be Point of TOP-REAL 2;
assume A35: p in the carrier of (TOP-REAL 2)|K1;
A36:dom ((sn-FanMorphW)|K1)=dom (sn-FanMorphW) /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2))/\ K1 by FUNCT_2:def 1
.=K1 by XBOOLE_1:28;
A37:the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
then consider p3 being Point of TOP-REAL 2 such that
A38: p=p3 & (p3`2/|.p3.|>=sn & p3`1<=0 & p3<>0.REAL 2) by A1,A35;
A39:(sn-FanMorphW).p=|[|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2)),
|.p.|* ((p`2/|.p.|-sn)/(1-sn))]| by A1,A38,Th25;
((sn-FanMorphW)|K1).p=(sn-FanMorphW).p by A35,A37,FUNCT_1:72;
then g1.p=(proj1).(|[|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2)),
|.p.|* ((p`2/|.p.|-sn)/(1-sn))]|)
by A35,A36,A37,A39,FUNCT_1:23
.=(|[|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2)),
|.p.|* ((p`2/|.p.|-sn)/(1-sn)) ]|)`1 by PSCOMP_1:def 28
.= |.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2)) by EUCLID:56;
hence g1.p=|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2));
end;
then consider f1 being map of (TOP-REAL 2)|K1,R^1 such that
A40:for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f1.p=|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2));
for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`1<=0 & q`2/|.q.|>=sn & q<>0.REAL 2
proof let q be Point of TOP-REAL 2;
assume A41: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
A42: q=p3 & (p3`2/|.p3.|>=sn & p3`1<=0 & p3<>0.REAL 2) by A1,A41;
thus thesis by A42;
end;
then A43:f1 is continuous by A1,A40,Th28;
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 A44: |[x,y]| in K1 & r=f1.(|[x,y]|) & s=f2.(|[x,y]|);
set p99=|[x,y]|;
A45:the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
consider p3 being Point of TOP-REAL 2 such that
A46: p99=p3 & (p3`2/|.p3.|>=sn & p3`1<=0 & p3<>0.REAL 2) by A1,A44;
A47:f1.p99=|.p99.|*(-sqrt(1-((p99`2/|.p99.|-sn)/(1-sn))^2))
by A40,A44,A45;
((sn-FanMorphW)|K0).(|[x,y]|)=((sn-FanMorphW)).(|[x,y]|) by A44,FUNCT_1:
72
.= |[|.p99.|*(-sqrt(1-((p99`2/|.p99.|-sn)/(1-sn))^2)),
|.p99.|* ((p99`2/|.p99.|-sn)/(1-sn))]| by A1,A46,Th25
.=|[r,s]| by A33,A44,A45,A47;
hence f.(|[x,y]|)=|[r,s]| by A1;
end;
hence f is continuous by A8,A9,A34,A43,JGRAPH_2:45;
end;
theorem Th31: for sn being Real,
K0,B0 being Subset of TOP-REAL 2,f being
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0
st -1<sn & sn<1 & f=(sn-FanMorphW)|K0 &
B0={q where q is Point of TOP-REAL 2: q`1<=0 & q<>0.REAL 2}
& K0={p: p`2/|.p.|<=sn & p`1<=0 & p<>0.REAL 2}
holds f is continuous
proof let sn be Real,K0,B0 be Subset of TOP-REAL 2,f be
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0;
assume A1: -1<sn & sn<1 & f=(sn-FanMorphW)|K0 &
B0={q where q is Point of TOP-REAL 2: q`1<=0 & q<>0.REAL 2} &
K0={p: p`2/|.p.|<=sn & p`1<=0 & p<>0.REAL 2};
set cn=sqrt(1-sn^2);
set p0=|[-cn,sn]|;
A2: p0`2=sn by EUCLID:56;
A3: p0`1=-cn by EUCLID:56;
sn^2<1^2 by A1,JGRAPH_2:8;
then A4: 1-sn^2>0 by SQUARE_1:11,59;
A5: now assume p0=0.REAL 2;
then --cn=-0 by EUCLID:56,JGRAPH_2:11;
hence contradiction by A4,SQUARE_1:93;
end;
--cn>0 by A4,SQUARE_1:93;
then A6: p0`1<0 by A3,REAL_1:66;
A7: |.p0.|=sqrt((-cn)^2+sn^2) by A2,A3,JGRAPH_3:10
.=sqrt((cn)^2+sn^2) by SQUARE_1:61;
cn^2=1-sn^2 by A4,SQUARE_1:def 4;
then |.p0.|=1 by A7,SQUARE_1:83,XCMPLX_1:27;
then p0`2/|.p0.|=sn by EUCLID:56;
then A8: p0 in K0 by A1,A5,A6;
then reconsider K1=K0 as non empty Subset of TOP-REAL 2;
A9: K0 c= B0
proof let x be set;assume x in K0;
then consider p8 being Point of TOP-REAL 2 such that
A10: x=p8 & (
p8`2/|.p8.|<=sn & p8`1<=0 & p8<>0.REAL 2) by A1;
thus x in B0 by A1,A10;
end;
A11:dom ((proj2)*((sn-FanMorphW)|K1)) c= dom ((sn-FanMorphW)|K1)
by RELAT_1:44;
dom ((sn-FanMorphW)|K1) c= dom ((proj2)*((sn-FanMorphW)|K1))
proof let x be set;assume A12:x in dom ((sn-FanMorphW)|K1);
then A13:x in dom (sn-FanMorphW) /\ K1 by FUNCT_1:68;
A14:((sn-FanMorphW)|K1).x=(sn-FanMorphW).x by A12,FUNCT_1:68;
A15: dom proj2 = (the carrier of TOP-REAL 2) by FUNCT_2:def 1;
x in dom (sn-FanMorphW) by A13,XBOOLE_0:def 3;
then (sn-FanMorphW).x in rng (sn-FanMorphW) by FUNCT_1:12;
hence x in dom ((proj2)*((sn-FanMorphW)|K1)) by A12,A14,A15,FUNCT_1:21;
end;
then A16:dom ((proj2)*((sn-FanMorphW)|K1))
=dom ((sn-FanMorphW)|K1) by A11,XBOOLE_0:def 10
.=dom (sn-FanMorphW) /\ 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;
A17:rng ((proj2)*((sn-FanMorphW)|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)*((sn-FanMorphW)|K1)) c= the carrier of R^1 by A17,XBOOLE_1:1
;
then (proj2)*((sn-FanMorphW)|K1) is Function of the carrier of (TOP-REAL 2)|K1
,
the carrier of R^1 by A16,FUNCT_2:4;
then reconsider g2=(proj2)*((sn-FanMorphW)|K1) as map of (TOP-REAL 2)|K1,R^1
;
A18:dom ((proj1)*((sn-FanMorphW)|K1))
c= dom ((sn-FanMorphW)|K1) by RELAT_1:44;
dom ((sn-FanMorphW)|K1) c= dom ((proj1)*((sn-FanMorphW)|K1))
proof let x be set;assume A19:x in dom ((sn-FanMorphW)|K1);
then A20:x in dom (sn-FanMorphW) /\ K1 by FUNCT_1:68;
A21:((sn-FanMorphW)|K1).x=(sn-FanMorphW).x by A19,FUNCT_1:68;
A22: dom proj1 = (the carrier of TOP-REAL 2) by FUNCT_2:def 1;
x in dom (sn-FanMorphW) by A20,XBOOLE_0:def 3;
then (sn-FanMorphW).x in rng (sn-FanMorphW) by FUNCT_1:12;
hence x in dom ((proj1)*((sn-FanMorphW)|K1)) by A19,A21,A22,FUNCT_1:21;
end;
then A23:dom ((proj1)*((sn-FanMorphW)|K1))
=dom ((sn-FanMorphW)|K1) by A18,XBOOLE_0:def 10
.=dom (sn-FanMorphW) /\ 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;
A24:rng ((proj1)*((sn-FanMorphW)|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)*((sn-FanMorphW)|K1)) c= the carrier of R^1 by A24,XBOOLE_1:1
;
then (proj1)*((sn-FanMorphW)|K1) is Function of the carrier of (TOP-REAL 2)|K1
,
the carrier of R^1 by A23,FUNCT_2:4;
then reconsider g1=(proj1)*((sn-FanMorphW)|K1) as map of (TOP-REAL 2)|K1,R^1
;
A25: for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`1<=0 & q<>0.REAL 2
proof let q be Point of TOP-REAL 2;
assume A26: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
A27: q=p3 & (p3`2/|.p3.|<=sn & p3`1<=0 & p3<>0.REAL 2) by A1,A26;
thus q`1<=0 & q<>0.REAL 2 by A27;
end;
for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds g2.p=|.p.|* ((p`2/|.p.|-sn)/(1+sn))
proof let p be Point of TOP-REAL 2;
assume A28: p in the carrier of (TOP-REAL 2)|K1;
A29:dom ((sn-FanMorphW)|K1)=dom (sn-FanMorphW) /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2))/\ K1 by FUNCT_2:def 1
.=K1 by XBOOLE_1:28;
A30:the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
then consider p3 being Point of TOP-REAL 2 such that
A31: p=p3 & (p3`2/|.p3.|<=sn & p3`1<=0 & p3<>0.REAL 2) by A1,A28;
A32:(sn-FanMorphW).p
=|[|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2)),
|.p.|* ((p`2/|.p.|-sn)/(1+sn))]| by A1,A31,Th25;
((sn-FanMorphW)|K1).p=(sn-FanMorphW).p by A28,A30,FUNCT_1:72;
then g2.p=(proj2).(|[|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2)),
|.p.|* ((p`2/|.p.|-sn)/(1+sn))]|)
by A28,A29,A30,A32,FUNCT_1:23
.=(|[|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2)),
|.p.|* ((p`2/|.p.|-sn)/(1+sn))]|)`2 by PSCOMP_1:def 29
.=|.p.|* ((p`2/|.p.|-sn)/(1+sn)) by EUCLID:56;
hence g2.p=|.p.|* ((p`2/|.p.|-sn)/(1+sn));
end;
then consider f2 being map of (TOP-REAL 2)|K1,R^1 such that
A33:for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f2.p=|.p.|* ((p`2/|.p.|-sn)/(1+sn));
A34:f2 is continuous by A1,A25,A33,Th27;
for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds g1.p=|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2))
proof let p be Point of TOP-REAL 2;
assume A35: p in the carrier of (TOP-REAL 2)|K1;
A36:dom ((sn-FanMorphW)|K1)=dom (sn-FanMorphW) /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2))/\ K1 by FUNCT_2:def 1
.=K1 by XBOOLE_1:28;
A37:the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
then consider p3 being Point of TOP-REAL 2 such that
A38: p=p3 & (p3`2/|.p3.|<=sn & p3`1<=0 & p3<>0.REAL 2) by A1,A35;
A39:(sn-FanMorphW).p=|[|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2)),
|.p.|* ((p`2/|.p.|-sn)/(1+sn))]| by A1,A38,Th25;
((sn-FanMorphW)|K1).p=(sn-FanMorphW).p by A35,A37,FUNCT_1:72;
then g1.p=(proj1).(|[|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2)),
|.p.|* ((p`2/|.p.|-sn)/(1+sn))]|)
by A35,A36,A37,A39,FUNCT_1:23
.=(|[|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2)),
|.p.|* ((p`2/|.p.|-sn)/(1+sn)) ]|)`1 by PSCOMP_1:def 28
.= |.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2)) by EUCLID:56;
hence g1.p=|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2));
end;
then consider f1 being map of (TOP-REAL 2)|K1,R^1 such that
A40:for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds f1.p=|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2));
for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`1<=0 & q`2/|.q.|<=sn & q<>0.REAL 2
proof let q be Point of TOP-REAL 2;
assume A41: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
A42: q=p3 & (p3`2/|.p3.|<=sn & p3`1<=0 & p3<>0.REAL 2) by A1,A41;
thus thesis by A42;
end;
then A43:f1 is continuous by A1,A40,Th29;
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 A44: |[x,y]| in K1 & r=f1.(|[x,y]|) & s=f2.(|[x,y]|);
set p99=|[x,y]|;
A45:the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
consider p3 being Point of TOP-REAL 2 such that
A46: p99=p3 & (p3`2/|.p3.|<=sn & p3`1<=0 & p3<>0.REAL 2) by A1,A44;
A47:f1.p99=|.p99.|*(-sqrt(1-((p99`2/|.p99.|-sn)/(1+sn))^2))
by A40,A44,A45;
((sn-FanMorphW)|K0).(|[x,y]|)=((sn-FanMorphW)).(|[x,y]|) by A44,FUNCT_1:
72
.= |[|.p99.|*(-sqrt(1-((p99`2/|.p99.|-sn)/(1+sn))^2)),
|.p99.|* ((p99`2/|.p99.|-sn)/(1+sn))]| by A1,A46,Th25
.=|[r,s]| by A33,A44,A45,A47;
hence f.(|[x,y]|)=|[r,s]| by A1;
end;
hence f is continuous by A8,A9,A34,A43,JGRAPH_2:45;
end;
Lm7: for sn being Real, K1 being Subset of TOP-REAL 2
st K1={p7 where p7 is Point of TOP-REAL 2:p7`2>=sn*|.p7.|}
holds K1 is closed
proof let sn be Real, K1 be Subset of TOP-REAL 2;
defpred P[Point of TOP-REAL 2] means ($1`2>=sn*|.$1.|);
assume K1={p: p`2>=(sn)*(|.p.|)};
then A1:K1={p7 where p7 is Point of TOP-REAL 2:P[p7]};
A2: K1`={p7 where p7 is Point of TOP-REAL 2:not P[p7]} from TopCompl(A1);
set K10=[#](TOP-REAL 2);
reconsider g1=proj2|K10 as continuous map of (TOP-REAL 2)|K10,R^1 by Lm3;
reconsider g0=(2 NormF)|K10 as continuous map of (TOP-REAL 2)|K10,R^1
by Lm5;
consider g2 being map of (TOP-REAL 2)|K10,R^1 such that
A3: (for q being Point of
(TOP-REAL 2)|K10,r1 being real number st g0.q=r1
holds g2.q=sn*r1) & g2 is continuous by JGRAPH_2:33;
consider g3 being map of (TOP-REAL 2)|K10,R^1 such that
A4: (for q being Point of
(TOP-REAL 2)|K10,r1,r2 being real number st g2.q=r1 & g1.q=r2
holds g3.q=r1-r2) & g3 is continuous by A3,JGRAPH_2:31;
A5: (TOP-REAL 2)|K10=TOP-REAL 2 by TSEP_1:3;
A6: for p being Point of TOP-REAL 2 holds g3.p=sn*|.p.|-p`2
proof let p be Point of TOP-REAL 2;
g0.p=(2 NormF).p by A5,Lm5 .=|.p.| by Def1;
then A7: g2.p=sn*|.p.| by A3,A5;
g1.p=proj2.p by A5,Lm3 .=p`2 by PSCOMP_1:def 29;
hence g3.p=sn*|.p.|-p`2 by A4,A5,A7;
end;
reconsider g=g3 as map of TOP-REAL 2,R^1 by A5;
A8: {p7 where p7 is Point of TOP-REAL 2: pi(g,p7)>0} c= K1`
proof let x be set;assume x in
{p7 where p7 is Point of TOP-REAL 2: pi(g,p7)>0};
then consider p7 being Point of TOP-REAL 2 such that
A9: p7=x & pi(g,p7)>0;
pi(g,p7)=g.p7 by JORDAN2C:def 10
.=sn*|.p7.|-p7`2 by A6;
then sn*|.p7.| - p7`2+p7`2>0+p7`2 by A9,REAL_1:67;
then sn*|.p7.| >0+p7`2 by XCMPLX_1:27;
hence x in K1` by A2,A9;
end;
K1` c= {p7 where p7 is Point of TOP-REAL 2:pi(g,p7)>0}
proof let x be set;assume x in K1`;
then consider p9 being Point of TOP-REAL 2 such that
A10: x=p9 & p9`2<sn*|.p9.| by A2;
A11: sn*|.p9.| - p9`2>0 by A10,SQUARE_1:11;
pi(g,p9)=g.p9 by JORDAN2C:def 10
.=sn*|.p9.|-p9`2 by A6;
hence x in {p7 where p7 is Point of TOP-REAL 2:
pi(g,p7)>0} by A10,A11;
end;
then K1`={p7 where p7 is Point of TOP-REAL 2:pi(g,p7)>0} by A8,XBOOLE_0:def
10;
then K1` is open by A4,A5,Th6;
hence thesis by TOPS_1:29;
end;
Lm8: for sn being Real, K1 being Subset of TOP-REAL 2
st K1={p7 where p7 is Point of TOP-REAL 2:p7`1>=sn*|.p7.|}
holds K1 is closed
proof let sn be Real, K1 be Subset of TOP-REAL 2;
defpred P[Point of TOP-REAL 2] means ($1`1>=sn*|.$1.|);
assume K1={p: p`1>=(sn)*(|.p.|)};
then A1:K1={p7 where p7 is Point of TOP-REAL 2:P[p7]};
A2: K1`={p7 where p7 is Point of TOP-REAL 2:not P[p7]} from TopCompl(A1);
set K10=[#](TOP-REAL 2);
reconsider g1=proj1|K10 as continuous map of (TOP-REAL 2)|K10,R^1 by Lm2;
reconsider g0=(2 NormF)|K10 as continuous map of (TOP-REAL 2)|K10,R^1
by Lm5;
consider g2 being map of (TOP-REAL 2)|K10,R^1 such that
A3: (for q being Point of
(TOP-REAL 2)|K10,r1 being real number st g0.q=r1
holds g2.q=sn*r1) & g2 is continuous by JGRAPH_2:33;
consider g3 being map of (TOP-REAL 2)|K10,R^1 such that
A4: (for q being Point of
(TOP-REAL 2)|K10,r1,r2 being real number st g2.q=r1 & g1.q=r2
holds g3.q=r1-r2) & g3 is continuous by A3,JGRAPH_2:31;
A5: (TOP-REAL 2)|K10=TOP-REAL 2 by TSEP_1:3;
A6: for p being Point of TOP-REAL 2 holds g3.p=sn*|.p.|-p`1
proof let p be Point of TOP-REAL 2;
g0.p=(2 NormF).p by A5,Lm5 .=|.p.| by Def1;
then A7: g2.p=sn*|.p.| by A3,A5;
g1.p=proj1.p by A5,Lm2 .=p`1 by PSCOMP_1:def 28;
hence g3.p=sn*|.p.|-p`1 by A4,A5,A7;
end;
reconsider g=g3 as map of TOP-REAL 2,R^1 by A5;
A8: {p7 where p7 is Point of TOP-REAL 2: pi(g,p7)>0} c= K1`
proof let x be set;assume x in
{p7 where p7 is Point of TOP-REAL 2: pi(g,p7)>0};
then consider p7 being Point of TOP-REAL 2 such that
A9: p7=x & pi(g,p7)>0;
pi(g,p7)=g.p7 by JORDAN2C:def 10
.=sn*|.p7.|-p7`1 by A6;
then sn*|.p7.| - p7`1+p7`1>0+p7`1 by A9,REAL_1:67;
then sn*|.p7.| >0+p7`1 by XCMPLX_1:27;
hence x in K1` by A2,A9;
end;
K1` c= {p7 where p7 is Point of TOP-REAL 2:pi(g,p7)>0}
proof let x be set;assume x in K1`;
then consider p9 being Point of TOP-REAL 2 such that
A10: x=p9 & p9`1<sn*|.p9.| by A2;
A11: sn*|.p9.| - p9`1>0 by A10,SQUARE_1:11;
pi(g,p9)=g.p9 by JORDAN2C:def 10
.=sn*|.p9.|-p9`1 by A6;
hence x in {p7 where p7 is Point of TOP-REAL 2: pi(g,p7)>0} by A10,A11;
end;
then K1`={p7 where p7 is Point of TOP-REAL 2:pi(g,p7)>0} by A8,XBOOLE_0:def
10;
then K1` is open by A4,A5,Th6;
hence thesis by TOPS_1:29;
end;
TopInter2 { P,Q[set] } : { p: P[p] & Q[p] } =
{ p1 where p1 is Point of TOP-REAL 2 : P[p1] } /\
{ p2 where p2 is Point of TOP-REAL 2 : Q[p2] }
proof
set K0 = { p: P[p] & Q[p] };
set K1 = { p7 where p7 is Point of TOP-REAL 2 : P[p7]};
set B0 = { p1 where p1 is Point of TOP-REAL 2 : Q[p1]};
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];
consider p6 being Point of TOP-REAL 2 such that
A4: p6=x & Q[p6] by A2;
thus x in K0 by A3,A4;
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
A5: x=p & P[p] & Q[p];
x in K1 & x in B0 by A5;
hence x in K1 /\ B0 by XBOOLE_0:def 3;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th32: for sn being Real, K03 being Subset of TOP-REAL 2
st K03={p: p`2>=(sn)*(|.p.|) & p`1<=0}
holds K03 is closed
proof
let sn be Real, K003 be Subset of TOP-REAL 2;
defpred P[Point of TOP-REAL 2] means ($1`2>=sn*|.$1.|);
assume A1: K003={p: p`2>=(sn)*(|.p.|) & p`1<=0};
reconsider K1={p7 where p7 is Point of TOP-REAL 2:P[p7]}
as Subset of TOP-REAL 2 from TopSubset;
A2: K1 is closed by Lm7;
defpred Q[Point of TOP-REAL 2] means $1`1<=0;
reconsider KX={p where p is Point of TOP-REAL 2: Q[p]}
as Subset of TOP-REAL 2 from TopSubset;
A3: KX is closed by JORDAN6:6;
{p : P[p] & Q[p]}
= {p7 where p7 is Point of TOP-REAL 2:P[p7]} /\
{p1 where p1 is Point of TOP-REAL 2: Q[p1]} from TopInter2;
hence thesis by A1,A2,A3,TOPS_1:35;
end;
Lm9: for sn being Real, K1 being Subset of TOP-REAL 2
st K1={p7 where p7 is Point of TOP-REAL 2:p7`2<=sn*|.p7.|}
holds K1 is closed
proof let sn be Real, K1 be Subset of TOP-REAL 2;
defpred P[Point of TOP-REAL 2] means ($1`2<=sn*|.$1.|);
assume K1={p: p`2<=(sn)*(|.p.|)};
then A1:K1={p7 where p7 is Point of TOP-REAL 2:P[p7]};
A2:K1`={p7 where p7 is Point of TOP-REAL 2:not P[p7]} from TopCompl(A1);
set K10=[#](TOP-REAL 2);
reconsider g1=proj2|K10 as continuous map of (TOP-REAL 2)|K10,R^1 by Lm3;
reconsider g0=(2 NormF)|K10 as continuous map of (TOP-REAL 2)|K10,R^1
by Lm5;
consider g2 being map of (TOP-REAL 2)|K10,R^1 such that
A3: (for q being Point of
(TOP-REAL 2)|K10,r1 being real number st g0.q=r1
holds g2.q=sn*r1) & g2 is continuous by JGRAPH_2:33;
consider g3 being map of (TOP-REAL 2)|K10,R^1 such that
A4: (for q being Point of
(TOP-REAL 2)|K10,r1,r2 being real number st g2.q=r1 & g1.q=r2
holds g3.q=r1-r2) & g3 is continuous by A3,JGRAPH_2:31;
A5: (TOP-REAL 2)|K10=TOP-REAL 2 by TSEP_1:3;
A6: for p being Point of TOP-REAL 2 holds g3.p=sn*|.p.|-p`2
proof let p be Point of TOP-REAL 2;
g0.p=(2 NormF).p by A5,Lm5 .=|.p.| by Def1;
then A7: g2.p=sn*|.p.| by A3,A5;
g1.p=proj2.p by A5,Lm3 .=p`2 by PSCOMP_1:def 29;
hence g3.p=sn*|.p.|-p`2 by A4,A5,A7;
end;
reconsider g=g3 as map of TOP-REAL 2,R^1 by A5;
A8: {p7 where p7 is Point of TOP-REAL 2: pi(g,p7)<0} c= K1`
proof let x be set;assume x in
{p7 where p7 is Point of TOP-REAL 2: pi(g,p7)<0};
then consider p7 being Point of TOP-REAL 2 such that
A9: p7=x & pi(g,p7)<0;
pi(g,p7)=g.p7 by JORDAN2C:def 10
.=sn*|.p7.|-p7`2 by A6;
then sn*|.p7.| - p7`2+p7`2<0+p7`2 by A9,REAL_1:67;
then sn*|.p7.| <0+p7`2 by XCMPLX_1:27;
hence x in K1` by A2,A9;
end;
K1` c= {p7 where p7 is Point of TOP-REAL 2:pi(g,p7)<0}
proof let x be set;assume x in K1`;
then consider p9 being Point of TOP-REAL 2 such that
A10: x=p9 & p9`2>sn*|.p9.| by A2;
A11: sn*|.p9.| - p9`2<0 by A10,REAL_2:105;
pi(g,p9)=g.p9 by JORDAN2C:def 10
.=sn*|.p9.|-p9`2 by A6;
hence x in {p7 where p7 is Point of TOP-REAL 2:
pi(g,p7)<0} by A10,A11;
end;
then K1`={p7 where p7 is Point of TOP-REAL 2:pi(g,p7)<0} by A8,XBOOLE_0:def
10;
then K1` is open by A4,A5,Th7;
hence thesis by TOPS_1:29;
end;
Lm10: for sn being Real, K1 being Subset of TOP-REAL 2
st K1={p7 where p7 is Point of TOP-REAL 2:p7`1<=sn*|.p7.|}
holds K1 is closed
proof let sn be Real, K1 be Subset of TOP-REAL 2;
defpred P[Point of TOP-REAL 2] means ($1`1<=sn*|.$1.|);
assume K1={p: p`1<=(sn)*(|.p.|)};
then A1:K1={p7 where p7 is Point of TOP-REAL 2:P[p7]};
A2:K1`={p7 where p7 is Point of TOP-REAL 2:not P[p7]} from TopCompl(A1);
set K10=[#](TOP-REAL 2);
reconsider g1=proj1|K10 as continuous map of (TOP-REAL 2)|K10,R^1 by Lm2;
reconsider g0=(2 NormF)|K10 as continuous map of (TOP-REAL 2)|K10,R^1
by Lm5;
consider g2 being map of (TOP-REAL 2)|K10,R^1 such that
A3: (for q being Point of
(TOP-REAL 2)|K10,r1 being real number st g0.q=r1
holds g2.q=sn*r1) & g2 is continuous by JGRAPH_2:33;
consider g3 being map of (TOP-REAL 2)|K10,R^1 such that
A4: (for q being Point of
(TOP-REAL 2)|K10,r1,r2 being real number st g2.q=r1 & g1.q=r2
holds g3.q=r1-r2) & g3 is continuous by A3,JGRAPH_2:31;
A5: (TOP-REAL 2)|K10=TOP-REAL 2 by TSEP_1:3;
A6: for p being Point of TOP-REAL 2 holds g3.p=sn*|.p.|-p`1
proof let p be Point of TOP-REAL 2;
g0.p=(2 NormF).p by A5,Lm5 .=|.p.| by Def1;
then A7: g2.p=sn*|.p.| by A3,A5;
g1.p=proj1.p by A5,Lm2 .=p`1 by PSCOMP_1:def 28;
hence g3.p=sn*|.p.|-p`1 by A4,A5,A7;
end;
reconsider g=g3 as map of TOP-REAL 2,R^1 by A5;
A8: {p7 where p7 is Point of TOP-REAL 2: pi(g,p7)<0} c= K1`
proof let x be set;assume x in
{p7 where p7 is Point of TOP-REAL 2: pi(g,p7)<0};
then consider p7 being Point of TOP-REAL 2 such that
A9: p7=x & pi(g,p7)<0;
pi(g,p7)=g.p7 by JORDAN2C:def 10
.=sn*|.p7.|-p7`1 by A6;
then sn*|.p7.| - p7`1+p7`1<0+p7`1 by A9,REAL_1:67;
then sn*|.p7.| <0+p7`1 by XCMPLX_1:27;
hence x in K1` by A2,A9;
end;
K1` c= {p7 where p7 is Point of TOP-REAL 2:pi(g,p7)<0}
proof let x be set;assume x in K1`;
then consider p9 being Point of TOP-REAL 2 such that
A10: x=p9 & p9`1>sn*|.p9.| by A2;
A11: sn*|.p9.| - p9`1<0 by A10,REAL_2:105;
pi(g,p9)=g.p9 by JORDAN2C:def 10
.=sn*|.p9.|-p9`1 by A6;
hence x in {p7 where p7 is Point of TOP-REAL 2: pi(g,p7)<0} by A10,A11;
end;
then K1`={p7 where p7 is Point of TOP-REAL 2:pi(g,p7)<0} by A8,XBOOLE_0:def
10;
then K1` is open by A4,A5,Th7;
hence thesis by TOPS_1:29;
end;
theorem Th33: for sn being Real, K03 being Subset of TOP-REAL 2
st K03={p: p`2<=(sn)*(|.p.|) & p`1<=0}
holds K03 is closed
proof let sn be Real, K003 be Subset of TOP-REAL 2;
defpred P[Point of TOP-REAL 2] means ($1`2<=sn*|.$1.|);
defpred Q[Point of TOP-REAL 2] means $1`1<=0;
assume A1: K003={p: P[p] & Q[p]};
reconsider K1={p7 where p7 is Point of TOP-REAL 2:P[p7]}
as Subset of TOP-REAL 2 from TopSubset;
A2: K1 is closed by Lm9;
reconsider KX={p where p is Point of TOP-REAL 2: Q[p]}
as Subset of TOP-REAL 2 from TopSubset;
A3: KX is closed by JORDAN6:6;
{p : P[p] & Q[p]}
= {p7 where p7 is Point of TOP-REAL 2:P[p7]} /\
{p1 where p1 is Point of TOP-REAL 2: Q[p1]} from TopInter2;
hence thesis by A1,A2,A3,TOPS_1:35;
end;
theorem Th34: for sn being Real,
K0,B0 being Subset of TOP-REAL 2,f being
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0
st -1<sn & sn<1 & f=(sn-FanMorphW)|K0 &
B0=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p: p`1<=0 & p<>0.REAL 2}
holds f is continuous
proof let sn be Real,K0,B0 be Subset of TOP-REAL 2,f be
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0;
assume A1: -1<sn & sn<1 & f=(sn-FanMorphW)|K0 &
B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`1<=0 & p<>0.REAL 2};
set cn=sqrt(1-sn^2);
set p0=|[-cn,sn]|;
A2: p0`2=sn by EUCLID:56;
A3: p0`1=-cn by EUCLID:56;
sn^2<1 by A1,JGRAPH_2:8,SQUARE_1:59;
then A4: 1-sn^2>0 by SQUARE_1:11;
A5: now assume p0=0.REAL 2;
then --cn=-0 by EUCLID:56,JGRAPH_2:11;
hence contradiction by A4,SQUARE_1:93;
end;
--cn>0 by A4,SQUARE_1:93;
then A6: p0`1<0 by A3,REAL_1:66;
A7: |.p0.|=sqrt((-cn)^2+sn^2) by A2,A3,JGRAPH_3:10
.=sqrt((cn)^2+sn^2) by SQUARE_1:61;
cn^2=1-sn^2 by A4,SQUARE_1:def 4;
then |.p0.|=1 by A7,SQUARE_1:83,XCMPLX_1:27;
then A8: p0`2/|.p0.|=sn by EUCLID:56;
p0 in K0 by A1,A5,A6;
then reconsider K1=K0 as non empty Subset of TOP-REAL 2;
p0 in the carrier of TOP-REAL 2 & not p0 in {0.REAL 2}
by A5,TARSKI:def 1;
then reconsider D=B0 as non empty Subset of TOP-REAL 2 by A1,XBOOLE_0:def 4;
A9: p0 in {p: p`2/|.p.|>=sn & p`1<=0 & p<>0.REAL 2} by A5,A6,A8;
defpred P[Point of TOP-REAL 2] means
$1`2/|.$1.|>=sn & $1`1<=0 & $1<>0.REAL 2;
A10: {p: P[p]}
is Subset of TOP-REAL 2 from SubsetD;
A11: the carrier of ((TOP-REAL 2)|K1)=K1 by JORDAN1:1;
A12: {p: p`2/|.p.|>=sn & p`1<=0 & p<>0.REAL 2} c= K1
proof let x be set;assume x in
{p: p`2/|.p.|>=sn & p`1<=0 & p<>0.REAL 2};
then consider p such that
A13:p=x & p`2/|.p.|>=sn & p`1<=0 & p<>0.REAL 2;
thus x in K1 by A1,A13;
end;
then reconsider K00={p: p`2/|.p.|>=sn & p`1<=0 & p<>0.REAL 2}
as non empty Subset of ((TOP-REAL 2)|K1)
by A9,A11;
reconsider K001={p: p`2/|.p.|>=sn & p`1<=0 & p<>0.REAL 2}
as non empty Subset of (TOP-REAL 2)
by A9,A10;
defpred P[Point of TOP-REAL 2] means $1`2>=(sn)*(|.$1.|) & $1`1<=0;
{p: P[p]} is Subset of
TOP-REAL 2 from SubsetD;
then reconsider K003={p: p`2>=(sn)*(|.p.|) & p`1<=0}
as Subset of (TOP-REAL 2);
A14: p0 in {p: p`2/|.p.|<=sn & p`1<=0 & p<>0.REAL 2} by A5,A6,A8;
A15: {p: p`2/|.p.|<=sn & p`1<=0 & p<>0.REAL 2} c= K1
proof let x be set;assume x in
{p: p`2/|.p.|<=sn & p`1<=0 & p<>0.REAL 2};
then consider p such that
A16: p=x & p`2/|.p.|<=sn & p`1<=0 & p<>0.REAL 2;
thus x in K1 by A1,A16;
end;
then reconsider K11={p: p`2/|.p.|<=sn & p`1<=0 & p<>0.REAL 2}
as non empty Subset of ((TOP-REAL 2)|K1)
by A11,A14;
A17: p0 in {p: p`2/|.p.|<=sn & p`1<=0 & p<>0.REAL 2} by A5,A6,A8;
defpred P[Point of TOP-REAL 2] means
$1`2/|.$1.|<=sn & $1`1<=0 & $1<>0.REAL 2;
{p: P[p]} is Subset of
TOP-REAL 2 from SubsetD;
then reconsider K111={p: p`2/|.p.|<=sn & p`1<=0 & p<>0.REAL 2}
as non empty Subset of (TOP-REAL 2)
by A17;
defpred P[Point of TOP-REAL 2] means $1`2<=(sn)*(|.$1.|) & $1`1<=0;
{p: P[p]} is Subset of
TOP-REAL 2 from SubsetD;
then reconsider K004={p: p`2<=(sn)*(|.p.|) & p`1<=0}
as Subset of (TOP-REAL 2);
the carrier of (TOP-REAL 2)|B0=the carrier of (TOP-REAL 2)|D;
then A18: dom f=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1
.=K1 by JORDAN1:1;
then A19: dom (f|K00)=K00 by A12,RELAT_1:91
.= the carrier of ((TOP-REAL 2)|K1)|K00 by JORDAN1:1;
A20: the carrier of (TOP-REAL 2)|D=D by JORDAN1:1;
rng (f|K00) c= rng f by RELAT_1:99;
then rng (f|K00) c=D by A20,XBOOLE_1:1;
then f|K00 is Function of the carrier of ((TOP-REAL 2)|K1)|K00,
the carrier of (TOP-REAL 2)|D by A19,A20,FUNCT_2:4;
then reconsider f1=f|K00 as map of ((TOP-REAL 2)|K1)|K00,(TOP-REAL 2)|D
;
A21: dom f1=the carrier of ((TOP-REAL 2)|K1)|K00 by FUNCT_2:def 1
.=K00 by JORDAN1:1;
A22: dom (sn-FanMorphW)=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then A23: dom ((sn-FanMorphW)|K001)=K001 by RELAT_1:91
.= the carrier of (TOP-REAL 2)|K001 by JORDAN1:1;
A24: the carrier of (TOP-REAL 2)|K1 = K1 by JORDAN1:1;
rng ((sn-FanMorphW)|K001) c= K1
proof let y be set;assume y in rng ((sn-FanMorphW)|K001);
then consider x being set such that
A25: x in dom ((sn-FanMorphW)|K001) & y=((sn-FanMorphW)|K001).x
by FUNCT_1:def 5;
A26: dom ((sn-FanMorphW)|K001)=(dom (sn-FanMorphW))/\ K001 by FUNCT_1:68
.=(the carrier of TOP-REAL 2)/\ K001 by FUNCT_2:def 1
.=K001 by XBOOLE_1:28;
then reconsider q=x as Point of TOP-REAL 2 by A25;
A27: y=(sn-FanMorphW).q by A25,FUNCT_1:70;
consider p2 being Point of TOP-REAL 2 such that
A28: p2=q & p2`2/|.p2.|>=sn & p2`1<=0 & p2<>0.REAL 2 by A25,A26;
A29: sn-FanMorphW.q= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)),
|.q.|* ((q`2/|.q.|-sn)/(1-sn))]| by A1,A28,Th25;
set q4= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)),
|.q.|* ((q`2/|.q.|-sn)/(1-sn))]|;
A30: |.q.|>=0 by TOPRNS_1:26;
|.q.|<>0 by A28,TOPRNS_1:25;
then A31: (|.q.|)^2>0 by SQUARE_1:74;
A32: 1-sn>0 by A1,Th3;
A33: q4`1= |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2))&
q4`2= |.q.|* ((q`2/|.q.|-sn)/(1-sn))
by EUCLID:56;
A34: (q`2/|.q.|-sn)>= 0 by A28,SQUARE_1:12;
0<=(q`1)^2 by SQUARE_1:72;
then 0+(q`2)^2<=(q`1)^2+(q`2)^2 by REAL_1:55;
then (q`2)^2 <= (|.q.|)^2 by JGRAPH_3:10;
then (q`2)^2/(|.q.|)^2 <= (|.q.|)^2/(|.q.|)^2 by A31,REAL_1:73;
then (q`2)^2/(|.q.|)^2 <= 1 by A31,XCMPLX_1:60;
then ((q`2)/|.q.|)^2 <= 1 by SQUARE_1:69;
then 1>=q`2/|.q.| by Th4;
then A35: 1-sn>=q`2/|.q.|-sn by REAL_1:49;
A36: -(1-sn)<= -0 by A32,REAL_1:50;
-(1-sn)<= -( q`2/|.q.|-sn) by A35,REAL_1:50;
then (-(1-sn))/(1-sn)<=(-( q`2/|.q.|-sn))/(1-sn)
by A32,REAL_1:73;
then A37: -1<=(-( q`2/|.q.|-sn))/(1-sn)
by A32,XCMPLX_1:198;
--(1-sn)>= -(q`2/|.q.|-sn) by A34,A36,REAL_1:50;
then (-(q`2/|.q.|-sn))/(1-sn)<=1 by A32,REAL_2:117;
then ((-(q`2/|.q.|-sn))/(1-sn))^2<=1 by A37,JGRAPH_2:7,SQUARE_1:59;
then A38: 1-((-(q`2/|.q.|-sn))/(1-sn))^2>=0 by SQUARE_1:12;
then 1-(-((q`2/|.q.|-sn))/(1-sn))^2>=0 by XCMPLX_1:188;
then A39: 1-((q`2/|.q.|-sn)/(1-sn))^2>=0 by SQUARE_1:61;
sqrt(1-((-(q`2/|.q.|-sn))/(1-sn))^2)>=0 by A38,SQUARE_1:def 4;
then sqrt(1-(-(q`2/|.q.|-sn))^2/(1-sn)^2)>=0 by SQUARE_1:69;
then sqrt(1-(q`2/|.q.|-sn)^2/(1-sn)^2)>=0 by SQUARE_1:61;
then sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)>=0 by SQUARE_1:69;
then A40: -sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)<= -0 by REAL_1:50;
A41: (q4`1)^2= (|.q.|)^2*(-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2))^2
by A33,SQUARE_1:68
.= (|.q.|)^2*(sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2))^2
by SQUARE_1:61
.= (|.q.|)^2*(1-((q`2/|.q.|-sn)/(1-sn))^2) by A39,SQUARE_1:def 4;
A42: (q4`2)^2= (|.q.|)^2*((q`2/|.q.|-sn)/(1-sn))^2
by A33,SQUARE_1:68;
(|.q4.|)^2=(q4`1)^2+(q4`2)^2 by JGRAPH_3:10
.=(|.q.|)^2*(1-((q`2/|.q.|-sn)/(1-sn))^2
+((q`2/|.q.|-sn)/(1-sn))^2) by A41,A42,XCMPLX_1:8
.=(|.q.|)^2*1 by XCMPLX_1:27 .=(|.q.|)^2;
then q4`1<=0 & q4<>0.REAL 2 by A30,A31,A33,A40,SQUARE_1:23,60,TOPRNS_1:24
;
hence y in K1 by A1,A27,A29;
end;
then (sn-FanMorphW)|K001 is Function of the carrier of (TOP-REAL 2)|K001,
the carrier of (TOP-REAL 2)|K1 by A23,A24,FUNCT_2:4;
then reconsider f3=(sn-FanMorphW)|K001
as map of (TOP-REAL 2)|K001,(TOP-REAL 2)|K1 ;
A43: dom (f|K11)=K11 by A15,A18,RELAT_1:91
.= the carrier of ((TOP-REAL 2)|K1)|K11 by JORDAN1:1;
A44: the carrier of (TOP-REAL 2)|D=D by JORDAN1:1;
rng (f|K11) c= rng f by RELAT_1:99;
then rng (f|K11) c=D by A44,XBOOLE_1:1;
then f|K11 is Function of the carrier of ((TOP-REAL 2)|K1)|K11,
the carrier of (TOP-REAL 2)|D by A43,A44,FUNCT_2:4;
then reconsider f2=f|K11 as map of ((TOP-REAL 2)|K1)|K11,(TOP-REAL 2)|D
;
A45: dom f2=the carrier of ((TOP-REAL 2)|K1)|K11 by FUNCT_2:def 1
.=K11 by JORDAN1:1;
A46: dom ((sn-FanMorphW)|K111)=K111 by A22,RELAT_1:91
.= the carrier of (TOP-REAL 2)|K111 by JORDAN1:1;
A47: the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
rng ((sn-FanMorphW)|K111) c= K1
proof let y be set;assume y in rng ((sn-FanMorphW)|K111);
then consider x being set such that
A48: x in dom ((sn-FanMorphW)|K111) & y=((sn-FanMorphW)|K111).x
by FUNCT_1:def 5;
A49: dom ((sn-FanMorphW)|K111)=(dom (sn-FanMorphW))/\ K111 by FUNCT_1:68
.=(the carrier of TOP-REAL 2)/\ K111 by FUNCT_2:def 1
.=K111 by XBOOLE_1:28;
then reconsider q=x as Point of TOP-REAL 2 by A48;
A50: y=(sn-FanMorphW).q by A48,FUNCT_1:70;
consider p2 being Point of TOP-REAL 2 such that
A51: p2=q & p2`2/|.p2.|<=sn & p2`1<=0 & p2<>0.REAL 2 by A48,A49;
A52: sn-FanMorphW.q= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)),
|.q.|* ((q`2/|.q.|-sn)/(1+sn))]| by A1,A51,Th25;
set q4= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)),
|.q.|* ((q`2/|.q.|-sn)/(1+sn))]|;
A53: |.q.|>=0 by TOPRNS_1:26;
|.q.|<>0 by A51,TOPRNS_1:25;
then A54: (|.q.|)^2>0 by SQUARE_1:74;
A55: 1+sn>0 by A1,Th3;
A56: q4`1= |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2))&
q4`2= |.q.|* ((q`2/|.q.|-sn)/(1+sn))
by EUCLID:56;
A57: (q`2/|.q.|-sn)<=0 by A51,REAL_2:106;
A58: (|.q.|)^2 =(q`1)^2+(q`2)^2 by JGRAPH_3:10;
0<=(q`1)^2 by SQUARE_1:72;
then 0+(q`2)^2<=(q`1)^2+(q`2)^2 by REAL_1:55;
then (q`2)^2/(|.q.|)^2 <= (|.q.|)^2/(|.q.|)^2 by A54,A58,REAL_1:73;
then (q`2)^2/(|.q.|)^2 <= 1 by A54,XCMPLX_1:60;
then ((q`2)/|.q.|)^2 <= 1 by SQUARE_1:69;
then -1<=q`2/|.q.| by Th4;
then -1-sn<=q`2/|.q.|-sn by REAL_1:49;
then A59: -(1+sn)<=q`2/|.q.|-sn by XCMPLX_1:161;
(1+sn)/(1+sn)>=(q`2/|.q.|-sn)/(1+sn) by A55,A57,REAL_1:73;
then A60: 1>=(q`2/|.q.|-sn)/(1+sn) by A55,XCMPLX_1:60;
(-(1+sn))/(1+sn)<=(( q`2/|.q.|-sn))/(1+sn)
by A55,A59,REAL_1:73;
then -1<=(( q`2/|.q.|-sn))/(1+sn)
by A55,XCMPLX_1:198;
then (((q`2/|.q.|-sn))/(1+sn))^2<=1^2 by A60,JGRAPH_2:7;
then A61: 1-((q`2/|.q.|-sn)/(1+sn))^2>=0 by SQUARE_1:12,59;
then 1-(-((q`2/|.q.|-sn)/(1+sn)))^2>=0 by SQUARE_1:61;
then 1-((-(q`2/|.q.|-sn))/(1+sn))^2>=0 by XCMPLX_1:188;
then sqrt(1-((-(q`2/|.q.|-sn))/(1+sn))^2)>=0 by SQUARE_1:def 4;
then sqrt(1-(-(q`2/|.q.|-sn))^2/(1+sn)^2)>=0 by SQUARE_1:69;
then sqrt(1-(q`2/|.q.|-sn)^2/(1+sn)^2)>=0 by SQUARE_1:61;
then sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)>=0 by SQUARE_1:69;
then -sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)<= -0 by REAL_1:50;
then A62: q4`1<= 0 by A53,A56,SQUARE_1:23;
A63: (q4`1)^2= (|.q.|)^2*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2))^2
by A56,SQUARE_1:68
.= (|.q.|)^2*(sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2))^2
by SQUARE_1:61
.= (|.q.|)^2*(1-((q`2/|.q.|-sn)/(1+sn))^2) by A61,SQUARE_1:def 4;
A64: (q4`2)^2= (|.q.|)^2*((q`2/|.q.|-sn)/(1+sn))^2
by A56,SQUARE_1:68;
(|.q4.|)^2=(q4`1)^2+(q4`2)^2 by JGRAPH_3:10
.=(|.q.|)^2*(1-((q`2/|.q.|-sn)/(1+sn))^2
+((q`2/|.q.|-sn)/(1+sn))^2) by A63,A64,XCMPLX_1:8
.=(|.q.|)^2*1 by XCMPLX_1:27 .=(|.q.|)^2;
then q4<>0.REAL 2 by A54,SQUARE_1:60,TOPRNS_1:24;
hence y in K1 by A1,A50,A52,A62;
end;
then (sn-FanMorphW)|K111 is Function of the carrier of (TOP-REAL 2)|K111,
the carrier of (TOP-REAL 2)|K1 by A46,A47,FUNCT_2:4;
then reconsider f4=(sn-FanMorphW)|K111
as map of (TOP-REAL 2)|K111,(TOP-REAL 2)|K1 ;
set T1= ((TOP-REAL 2)|K1)|K00,T2=((TOP-REAL 2)|K1)|K11;
A65: [#](((TOP-REAL 2)|K1)|K00)=K00 by PRE_TOPC:def 10;
A66: [#](((TOP-REAL 2)|K1)|K11)=K11 by PRE_TOPC:def 10;
A67: [#]((TOP-REAL 2)|K1)=K1 by PRE_TOPC:def 10;
A68: K00 \/ K11 c= K1
proof let x be set;assume
A69: x in K00 \/ K11;
now per cases by A69,XBOOLE_0:def 2;
case x in K00;
then consider p8 being Point of TOP-REAL 2 such that
A70: p8=x & p8`2/|.p8.|>=sn & p8`1<=0 & p8<>0.REAL 2;
thus x in K1 by A1,A70;
case x in K11;
then consider p8 being Point of TOP-REAL 2 such that
A71: p8=x & p8`2/|.p8.|<=sn & p8`1<=0 & p8<>0.REAL 2;
thus x in K1 by A1,A71;
end;
hence x in K1;
end;
A72: K1 c= K00 \/ K11
proof let x be set;assume x in K1;
then consider p such that
A73: p=x & (p`1<=0 & p<>0.REAL 2) by A1;
now per cases;
case p`2/|.p.|>=sn;
then x in K00 by A73;
hence x in K00 \/ K11 by XBOOLE_0:def 2;
case p`2/|.p.|<sn;
then x in K11 by A73;
hence x in K00 \/ K11 by XBOOLE_0:def 2;
end;
hence x in K00 \/ K11;
end;
then A74: [#](((TOP-REAL 2)|K1)|K00) \/ [#](((TOP-REAL 2)|K1)|K11)
=[#]((TOP-REAL 2)|K1) by A65,A66,A67,A68,XBOOLE_0:def 10;
A75: K003 is closed by Th32;
A76: K003 /\ K1 c= K00
proof let x be set;assume x in K003 /\ K1;
then A77: x in K003 & x in K1 by XBOOLE_0:def 3;
then consider q1 being Point of TOP-REAL 2 such that
A78: q1=x & q1`2>=(sn)*(|.q1.|) & q1`1<=0;
consider q2 being Point of TOP-REAL 2 such that
A79: q2=x & q2`1<=0 & q2<>0.REAL 2 by A1,A77;
A80: |.q2.|<>0 by A79,TOPRNS_1:25;
|.q1.|>0 by A78,A79,Lm1;
then q1`2/|.q1.|>=(sn)*(|.q1.|)/|.q1.| by A78,REAL_1:73;
then q1`2/|.q1.|>=(sn) by A78,A79,A80,XCMPLX_1:90;
hence x in K00 by A78,A79;
end;
K00 c= K003 /\ K1
proof let x be set;assume x in K00;
then consider p such that
A81: p=x & (p`2/|.p.|>=sn & p`1<=0 & p<>0.REAL 2);
A82: |.p.|<>0 by A81,TOPRNS_1:25;
|.p.|>=0 by TOPRNS_1:26;
then p`2/|.p.|*|.p.|>=(sn)*(|.p.|) by A81,AXIOMS:25;
then p`2>=(sn)*(|.p.|) by A82,XCMPLX_1:88;
then A83: x in K003 by A81;
x in K1 by A1,A81;
hence x in K003 /\ K1 by A83,XBOOLE_0:def 3;
end;
then K00=K003 /\ [#]((TOP-REAL 2)|K1) by A67,A76,XBOOLE_0:def 10;
then A84: K00 is closed by A75,PRE_TOPC:43;
A85: K004 is closed by Th33;
A86: K004 /\ K1 c= K11
proof let x be set;assume x in K004 /\ K1;
then A87: x in K004 & x in K1 by XBOOLE_0:def 3;
then consider q1 being Point of TOP-REAL 2 such that
A88: q1=x & q1`2<=(sn)*(|.q1.|) & q1`1<=0;
consider q2 being Point of TOP-REAL 2 such that
A89: q2=x & q2`1<=0 & q2<>0.REAL 2 by A1,A87;
A90: |.q2.|<>0 by A89,TOPRNS_1:25;
|.q1.|>0 by A88,A89,Lm1;
then q1`2/|.q1.|<=(sn)*(|.q1.|)/|.q1.| by A88,REAL_1:73;
then q1`2/|.q1.|<=(sn) by A88,A89,A90,XCMPLX_1:90;
hence x in K11 by A88,A89;
end;
K11 c= K004 /\ K1
proof let x be set;assume x in K11;
then consider p such that
A91: p=x & (p`2/|.p.|<=sn & p`1<=0 & p<>0.REAL 2);
A92: |.p.|<>0 by A91,TOPRNS_1:25;
|.p.|>=0 by TOPRNS_1:26;
then p`2/|.p.|*|.p.|<=(sn)*(|.p.|) by A91,AXIOMS:25;
then p`2<=(sn)*(|.p.|) by A92,XCMPLX_1:88;
then A93: x in K004 by A91;
x in K1 by A1,A91;
hence x in K004 /\ K1 by A93,XBOOLE_0:def 3;
end;
then K11=K004 /\ [#]((TOP-REAL 2)|K1) by A67,A86,XBOOLE_0:def 10;
then A94: K11 is closed by A85,PRE_TOPC:43;
A95: ((TOP-REAL 2)|K1)|K00=(TOP-REAL 2)|K001 by GOBOARD9:4;
K1 c= D
proof let x be set;assume x in K1;
then consider p6 being Point of TOP-REAL 2 such that
A96: p6=x & p6`1<=0 & p6<>0.REAL 2 by A1;
x in the carrier of TOP-REAL 2 & not x in {0.REAL 2} by A96,TARSKI:def 1
;
hence x in D by A1,XBOOLE_0:def 4;
end;
then D=K1 \/ D by XBOOLE_1:12;
then A97: (TOP-REAL 2)|K1 is SubSpace of (TOP-REAL 2)|D by TOPMETR:5;
the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
then A98: f1= f3 by A1,FUNCT_1:82;
f3 is continuous by A1,Th30;
then A99: f1 is continuous by A95,A97,A98,TOPMETR:7;
A100: ((TOP-REAL 2)|K1)|K11=(TOP-REAL 2)|K111 by GOBOARD9:4;
the carrier of (TOP-REAL 2)|K1=K1 by JORDAN1:1;
then A101: f2= f4 by A1,FUNCT_1:82;
f4 is continuous by A1,Th31;
then A102: f2 is continuous by A97,A100,A101,TOPMETR:7;
A103: D<>{};
A104: the carrier of (TOP-REAL 2)|B0=B0 by JORDAN1:1;
for p being set st p in ([#]T1)/\([#]T2) holds f1.p = f2.p
proof let p be set;
assume p in ([#]T1)/\([#]T2);
then A105: p in K00 & p in K11 by A65,A66,XBOOLE_0:def 3;
hence f1.p=f.p by FUNCT_1:72 .=f2.p by A105,FUNCT_1:72;
end;
then consider h being map of (TOP-REAL 2)|K1,(TOP-REAL 2)|D
such that
A106: h=f1+*f2 & h is continuous by A65,A66,A74,A84,A94,A99,A102,JGRAPH_2:9;
A107: dom h=the carrier of ((TOP-REAL 2)|K1) by FUNCT_2:def 1;
A108: the carrier of ((TOP-REAL 2)|K1)=K0 by JORDAN1:1;
A109: K0=the carrier of ((TOP-REAL 2)|K0) by JORDAN1:1
.=dom f by A103,A104,FUNCT_2:def 1;
for y being set st y in dom h holds h.y=f.y
proof let y be set;assume
A110: y in dom h;
now per cases by A72,A107,A108,A110,XBOOLE_0:def 2;
case A111: y in K00 & not y in K11;
then y in dom f1 \/ dom f2 by A21,XBOOLE_0:def 2;
hence h.y=f1.y by A45,A106,A111,FUNCT_4:def 1 .=f.y by A111,FUNCT_1:72;
case A112: y in K11;
then y in dom f1 \/ dom f2 by A45,XBOOLE_0:def 2;
hence h.y=f2.y by A45,A106,A112,FUNCT_4:def 1 .=f.y by A112,FUNCT_1:72;
end;
hence h.y=f.y;
end;
hence thesis by A106,A107,A108,A109,FUNCT_1:9;
end;
theorem Th35: for sn being Real,
K0,B0 being Subset of TOP-REAL 2,f being
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0
st -1<sn & sn<1 & f=(sn-FanMorphW)|K0 &
B0=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p: p`1>=0 & p<>0.REAL 2}
holds f is continuous
proof let sn be Real,K0,B0 be Subset of TOP-REAL 2,f be
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0;
assume A1: -1<sn & sn<1 & f=(sn-FanMorphW)|K0 &
B0=(the carrier of TOP-REAL 2)\ {0.REAL 2} &
K0={p: p`1>=0 & p<>0.REAL 2};
set cn=sqrt(1-sn^2);
set p0=|[cn,-sn]|;
A2: p0`1=cn by EUCLID:56;
sn^2<1^2 by A1,JGRAPH_2:8;
then A3: 1-sn^2>0 by SQUARE_1:11,59;
then A4: p0<>0.REAL 2 by A2,JGRAPH_2:11,SQUARE_1:93;
p0`1>0 by A2,A3,SQUARE_1:93;
then p0 in K0 by A1,JGRAPH_2:11;
then reconsider K1=K0 as non empty Subset of TOP-REAL 2;
p0 in the carrier of TOP-REAL 2 & not p0 in {0.REAL 2}
by A4,TARSKI:def 1;
then reconsider D=B0 as non empty Subset of TOP-REAL 2 by A1,XBOOLE_0:def 4;
A5: K1 c= D
proof let x be set;assume x in K1;
then consider p2 being Point of TOP-REAL 2 such that
A6: p2=x & p2`1>=0 & p2<>0.REAL 2 by A1;
not p2 in {0.REAL 2} by A6,TARSKI:def 1;
hence x in D by A1,A6,XBOOLE_0:def 4;
end;
for p being Point of (TOP-REAL 2)|K1,V being Subset of (TOP-REAL 2)|D
st f.p in V & V is open holds
ex W being Subset of (TOP-REAL 2)|K1 st
p in W & W is open & f.:W c= V
proof let p be Point of (TOP-REAL 2)|K1,V be Subset of (TOP-REAL 2)|D;
assume A7: f.p in V & V is open;
then consider V2 being Subset of TOP-REAL 2 such that
A8: V2 is open & V2 /\ [#]((TOP-REAL 2)|D)=V by TOPS_2:32;
A9: p in the carrier of (TOP-REAL 2)|K1;
A10: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1) by PRE_TOPC:12;
A11: [#]((TOP-REAL 2)|K1)=K1 by PRE_TOPC:def 10;
V2 /\ [#]((TOP-REAL 2)|K1) c= the carrier of (TOP-REAL 2)|K1
proof let x be set;assume x in V2 /\ [#]((TOP-REAL 2)|K1);
then x in [#]((TOP-REAL 2)|K1) by XBOOLE_0:def 3;
hence x in the carrier of (TOP-REAL 2)|K1;
end;
then reconsider W2=V2 /\ [#]((TOP-REAL 2)|K1) as Subset of (TOP-REAL 2)|
K1
;
A12: W2 is open by A8,TOPS_2:32;
A13: f.p=(sn-FanMorphW).p by A1,A10,A11,FUNCT_1:72;
consider q being Point of TOP-REAL 2 such that
A14: q=p & q`1>=0 & q <>0.REAL 2 by A1,A9,A10,A11;
(sn-FanMorphW).q=q by A14,Th23;
then p in V2 & p in [#]((TOP-REAL 2)|D) by A7,A8,A13,A14,XBOOLE_0:def 3;
then A15: p in W2 by A10,XBOOLE_0:def 3;
f.:W2 c= V
proof let y be set;assume y in f.:W2;
then consider x being set such that
A16: x in dom f & x in W2 & y=f.x by FUNCT_1:def 12;
f is Function of the carrier of (TOP-REAL 2)|K1,
the carrier of (TOP-REAL 2)|D;
then dom f= K1 by A10,A11,FUNCT_2:def 1;
then consider p4 being Point of TOP-REAL 2 such that
A17: x=p4 & p4`1>=0 & p4<>0.REAL 2 by A1,A16;
A18: f.p4=(sn-FanMorphW).p4 by A1,A10,A11,A16,A17,FUNCT_1:72
.=p4 by A17,Th23;
A19: p4 in V2 & p4 in [#]((TOP-REAL 2)|K1) by A16,A17,XBOOLE_0:def 3
;
then p4 in D by A5,A11;
then p4 in [#]((TOP-REAL 2)|D) by PRE_TOPC:def 10;
hence y in V by A8,A16,A17,A18,A19,XBOOLE_0:def 3;
end;
hence ex W being Subset of (TOP-REAL 2)|K1 st
p in W & W is open & f.:W c= V by A12,A15;
end;
hence f is continuous by JGRAPH_2:20;
end;
theorem Th36:
for B0 being Subset of TOP-REAL 2,
K0 being Subset of (TOP-REAL 2)|B0
st B0=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p: p`1<=0 & p<>0.REAL 2} holds K0 is closed
proof
defpred P[Point of TOP-REAL 2] means $1`1<=0;
set I1 = {p: P[p] & p<>0.REAL 2};
set J0 = (the carrier of TOP-REAL 2) \ {0.REAL 2};
let B0 be Subset of TOP-REAL 2,K0 be Subset of (TOP-REAL 2)|B0;
assume A1: B0=J0 & K0=I1;
reconsider K1={p7 where p7 is Point of TOP-REAL 2:P[p7]}
as Subset of TOP-REAL 2 from TopSubset;
A2:K1 is closed by JORDAN6:6;
I1 = {p7 where p7 is Point of TOP-REAL 2 : P[p7]} /\ J0
from TopInter;
then K0=K1 /\ [#]((TOP-REAL 2)|B0) by A1,PRE_TOPC:def 10;
hence K0 is closed by A2,PRE_TOPC:43;
end;
theorem Th37: for sn being Real,
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 -1<sn & sn<1 & f=(sn-FanMorphW)|K0 &
B0=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p: p`1<=0 & p<>0.REAL 2}
holds f is continuous
proof let sn be Real,
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);
defpred P[Point of TOP-REAL 2] means $1`1<=0 & $1<>0.REAL 2;
assume A1: -1<sn & sn<1 & f=(sn-FanMorphW)|K0 &
B0=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p: p`1<=0 & p<>0.REAL 2 };
reconsider K1={p: P[p] } as Subset of TOP-REAL 2
from TopSubset;
K0 c= B0
proof let x be set;assume x in K0;
then consider p8 being Point of TOP-REAL 2 such that
A2: x=p8 & (p8`1<=0 & p8<>0.REAL 2) by A1;
not x in {0.REAL 2} by A2,TARSKI:def 1;
hence x in B0 by A1,A2,XBOOLE_0:def 4;
end;
then ((TOP-REAL 2)|B0)|K0=(TOP-REAL 2)|K1 by A1,JORDAN6:47;
hence f is continuous by A1,Th34;
end;
theorem Th38:
for B0 being Subset of TOP-REAL 2,
K0 being Subset of (TOP-REAL 2)|B0
st B0=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p: p`1>=0 & p<>0.REAL 2} holds K0 is closed
proof
defpred P[Point of TOP-REAL 2] means $1`1>=0;
set I1 = {p: P[p] & p<>0.REAL 2};
set J0 = (the carrier of TOP-REAL 2) \ {0.REAL 2};
let B0 be Subset of TOP-REAL 2,K0 be Subset of (TOP-REAL 2)|B0;
assume A1: B0=J0 & K0=I1;
reconsider K1={p7 where p7 is Point of TOP-REAL 2:P[p7]}
as Subset of TOP-REAL 2 from TopSubset;
A2:K1 is closed by JORDAN6:5;
I1 = {p7 where p7 is Point of TOP-REAL 2 : P[p7]} /\ J0
from TopInter;
then K0=K1 /\ [#]((TOP-REAL 2)|B0) by A1,PRE_TOPC:def 10;
hence K0 is closed by A2,PRE_TOPC:43;
end;
theorem Th39: for sn being Real,
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 -1<sn & sn<1 & f=(sn-FanMorphW)|K0 &
B0=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p: p`1>=0 & p<>0.REAL 2}
holds f is continuous
proof let sn be Real,
B0 be Subset of TOP-REAL 2,K0 be Subset of
(TOP-REAL 2)|B0,f be map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0);
assume A1: -1<sn & sn<1 & f=(sn-FanMorphW)|K0 &
B0=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p: p`1>=0 & 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;
K0 c= B0
proof let x be set;assume x in K0;
then consider p8 being Point of TOP-REAL 2 such that
A2: x=p8 & (p8`1>=0 & p8<>0.REAL 2) by A1;
not x in {0.REAL 2} by A2,TARSKI:def 1;
hence x in B0 by A1,A2,XBOOLE_0:def 4;
end;
then ((TOP-REAL 2)|B0)|K0=(TOP-REAL 2)|K1 by JORDAN6:47;
hence thesis by A1,Th35;
end;
theorem Th40: for sn being Real,p being Point of TOP-REAL 2
holds |.(sn-FanMorphW).p.|=|.p.|
proof let sn be Real,p be Point of TOP-REAL 2;
set z=(sn-FanMorphW).p;
reconsider q=p as Point of TOP-REAL 2;
reconsider qz=z as Point of TOP-REAL 2;
A1: |.q.|>=0 by TOPRNS_1:26;
now per cases;
case A2: q`2/|.q.|>=sn & q`1<0;
then (sn-FanMorphW).q= |[
|.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)),
|.q.|* ((q`2/|.q.|-sn)/(1-sn))]| by Th23;
then A3: qz`1= |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2))&
qz`2= |.q.|* ((q`2/|.q.|-sn)/(1-sn)) by EUCLID:56;
|.q.|<>0 by A2,JGRAPH_2:11,TOPRNS_1:25;
then A4: (|.q.|)^2>0 by SQUARE_1:74;
A5: (q`2/|.q.|-sn)>=0 by A2,SQUARE_1:12;
A6: (|.q.|)^2 =(q`1)^2+(q`2)^2 by JGRAPH_3:10;
0<=(q`1)^2 by SQUARE_1:72;
then 0+(q`2)^2<=(q`1)^2+(q`2)^2 by REAL_1:55;
then (q`2)^2/(|.q.|)^2 <= (|.q.|)^2/(|.q.|)^2 by A4,A6,REAL_1:73;
then (q`2)^2/(|.q.|)^2 <= 1 by A4,XCMPLX_1:60;
then ((q`2)/|.q.|)^2 <= 1 by SQUARE_1:69;
then 1>=q`2/|.q.| by Th4;
then A7: 1-sn>=q`2/|.q.|-sn by REAL_1:49;
now per cases;
case A8: 1-sn=0;
A9:((q`2/|.q.|-sn)/(1-sn))=(q`2/|.q.|-sn)*(1-sn)" by XCMPLX_0:def 9
.= (q`2/|.q.|-sn)*0 by A8,XCMPLX_0:def 7 .=0;
then -sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)=-1 by SQUARE_1:60,83;
then (sn-FanMorphW).q= |[|.q.|*(-1),|.q.|*0]| by A2,A9,Th23
.=|[-(|.q.|),0]| by XCMPLX_1:180;
then ((sn-FanMorphW).q)`1=-(|.q.|) & ((sn-FanMorphW).q)`2=0
by EUCLID:56;
then |.(sn-FanMorphW).p.|=sqrt((-(|.q.|))^2+0) by JGRAPH_3:10,
SQUARE_1:60
.=sqrt((|.q.|)^2) by SQUARE_1:61
.=|.q.| by A1,SQUARE_1:89;
hence |.(sn-FanMorphW).p.|=|.p.|;
case A10: 1-sn<>0;
now per cases by A10;
case A11: 1-sn>0;
then A12: -(1-sn)<= -0 by REAL_1:50;
-(1-sn)<= -( q`2/|.q.|-sn) by A7,REAL_1:50;
then (-(1-sn))/(1-sn)<=(-( q`2/|.q.|-sn))/(1-sn)
by A11,REAL_1:73;
then A13: -1<=(-( q`2/|.q.|-sn))/(1-sn)
by A11,XCMPLX_1:198;
--(1-sn)>= -(q`2/|.q.|-sn) by A5,A12,REAL_1:50;
then (-(q`2/|.q.|-sn))/(1-sn)<=1 by A11,REAL_2:117;
then ((-(q`2/|.q.|-sn))/(1-sn))^2<=1^2 by A13,JGRAPH_2:7;
then 1-((-(q`2/|.q.|-sn))/(1-sn))^2>=0 by SQUARE_1:12,59;
then 1-(-((q`2/|.q.|-sn))/(1-sn))^2>=0 by XCMPLX_1:188;
then A14: 1-((q`2/|.q.|-sn)/(1-sn))^2>=0 by SQUARE_1:61;
A15: (qz`1)^2= (|.q.|)^2*(-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2))^2
by A3,SQUARE_1:68
.= (|.q.|)^2*(sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2))^2
by SQUARE_1:61
.= (|.q.|)^2*(1-((q`2/|.q.|-sn)/(1-sn))^2)
by A14,SQUARE_1:def 4;
A16: (qz`2)^2= (|.q.|)^2*((q`2/|.q.|-sn)/(1-sn))^2
by A3,SQUARE_1:68;
(|.qz.|)^2=(qz`1)^2+(qz`2)^2 by JGRAPH_3:10
.=(|.q.|)^2*(1-((q`2/|.q.|-sn)/(1-sn))^2
+((q`2/|.q.|-sn)/(1-sn))^2) by A15,A16,XCMPLX_1:8
.=(|.q.|)^2*1 by XCMPLX_1:27 .=(|.q.|)^2;
then A17: sqrt((|.qz.|)^2)=|.q.| by A1,SQUARE_1:89;
|.qz.|>=0 by TOPRNS_1:26;
hence |.(sn-FanMorphW).p.|=|.p.| by A17,SQUARE_1:89;
case A18: 1-sn<0;
A19: q`2/|.q.|-sn>=0 by A2,SQUARE_1:12;
0<(q`1)^2 by A2,SQUARE_1:74;
then 0+(q`2)^2<(q`1)^2+(q`2)^2 by REAL_1:67;
then (q`2)^2/(|.q.|)^2 < (|.q.|)^2/(|.q.|)^2 by A4,A6,REAL_1:73;
then (q`2)^2/(|.q.|)^2 < 1 by A4,XCMPLX_1:60;
then ((q`2)/|.q.|)^2 < 1 by SQUARE_1:69;
then 1 > q`2/|.p.| by Th5;
then q`2/|.q.|-sn<1-sn by REAL_1:54;
hence |.(sn-FanMorphW).p.|=|.p.| by A18,A19,AXIOMS:22;
end;
hence |.(sn-FanMorphW).p.|=|.p.|;
end;
hence |.(sn-FanMorphW).p.|=|.p.|;
case A20: q`2/|.q.|<sn & q`1<0;
then A21:(sn-FanMorphW).q= |[
|.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)),
|.q.|* ((q`2/|.q.|-sn)/(1+sn))]| by Th24;
then A22: qz`1= |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2))&
qz`2= |.q.|* ((q`2/|.q.|-sn)/(1+sn))
by EUCLID:56;
|.q.|<>0 by A20,JGRAPH_2:11,TOPRNS_1:25;
then A23: (|.q.|)^2>0 by SQUARE_1:74;
A24: (q`2/|.q.|-sn)<0 by A20,REAL_2:105;
A25: (|.q.|)^2 =(q`1)^2+(q`2)^2 by JGRAPH_3:10;
0<=(q`1)^2 by SQUARE_1:72;
then 0+(q`2)^2<=(q`1)^2+(q`2)^2 by REAL_1:55;
then (q`2)^2/(|.q.|)^2 <= (|.q.|)^2/(|.q.|)^2 by A23,A25,REAL_1:73;
then (q`2)^2/(|.q.|)^2 <= 1 by A23,XCMPLX_1:60;
then ((q`2)/|.q.|)^2 <= 1 by SQUARE_1:69;
then -1<=q`2/|.q.| by Th4;
then A26: -1-sn<=q`2/|.q.|-sn by REAL_1:49;
now per cases;
case A27: 1+sn=0;
((q`2/|.q.|-sn)/(1+sn))=(q`2/|.q.|-sn)*(1+sn)" by XCMPLX_0:def 9
.= (q`2/|.q.|-sn)*0 by A27,XCMPLX_0:def 7 .=0;
then (sn-FanMorphW).q=|[-(|.q.|),0]| by A21,SQUARE_1:60,83,XCMPLX_1
:180;
then ((sn-FanMorphW).q)`1=-(|.q.|) & ((sn-FanMorphW).q)`2=0
by EUCLID:56;
then |.(sn-FanMorphW).p.|=sqrt((-(|.q.|))^2+0) by JGRAPH_3:10,
SQUARE_1:60
.=sqrt((|.q.|)^2) by SQUARE_1:61
.=|.q.| by A1,SQUARE_1:89;
hence |.(sn-FanMorphW).p.|=|.p.|;
case A28: 1+sn<>0;
now per cases by A28;
case A29: 1+sn>0;
-(1+sn)<= ( q`2/|.q.|-sn) by A26,XCMPLX_1:161;
then (-(1+sn))/(1+sn)<=(( q`2/|.q.|-sn))/(1+sn)
by A29,REAL_1:73;
then A30: -1<=(( q`2/|.q.|-sn))/(1+sn) by A29,XCMPLX_1:198;
(1+sn)>= (q`2/|.q.|-sn) by A24,A29,AXIOMS:22;
then ((q`2/|.q.|-sn))/(1+sn)<=1 by A29,REAL_2:117;
then (((q`2/|.q.|-sn))/(1+sn))^2<=1 by A30,JGRAPH_2:7,SQUARE_1:59
;
then A31: 1-(((q`2/|.q.|-sn))/(1+sn))^2>=0 by SQUARE_1:12;
A32: (qz`1)^2= (|.q.|)^2*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2))^2
by A22,SQUARE_1:68
.= (|.q.|)^2*(sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2))^2
by SQUARE_1:61
.= (|.q.|)^2*(1-((q`2/|.q.|-sn)/(1+sn))^2)
by A31,SQUARE_1:def 4;
A33: (qz`2)^2= (|.q.|)^2*((q`2/|.q.|-sn)/(1+sn))^2
by A22,SQUARE_1:68;
(|.qz.|)^2=(qz`1)^2+(qz`2)^2 by JGRAPH_3:10
.=(|.q.|)^2*(1-((q`2/|.q.|-sn)/(1+sn))^2
+((q`2/|.q.|-sn)/(1+sn))^2) by A32,A33,XCMPLX_1:8
.=(|.q.|)^2*1 by XCMPLX_1:27 .=(|.q.|)^2;
then A34: sqrt((|.qz.|)^2)=|.q.| by A1,SQUARE_1:89;
|.qz.|>=0 by TOPRNS_1:26;
hence |.(sn-FanMorphW).p.|=|.p.| by A34,SQUARE_1:89;
case 1+sn<0;
then A35: -(1+sn)>-0 by REAL_1:50;
0<(q`1)^2 by A20,SQUARE_1:74;
then 0+(q`2)^2<(q`1)^2+(q`2)^2 by REAL_1:67;
then (q`2)^2/(|.q.|)^2 < (|.q.|)^2/(|.q.|)^2 by A23,A25,REAL_1:73
;
then (q`2)^2/(|.q.|)^2 < 1 by A23,XCMPLX_1:60;
then ((q`2)/|.q.|)^2 < 1 by SQUARE_1:69;
then -1 < q`2/|.p.| by Th5;
then q`2/|.q.|-sn>-1-sn by REAL_1:54;
then q`2/|.q.|-sn>-(1+sn) by XCMPLX_1:161;
hence |.(sn-FanMorphW).p.|=|.p.| by A24,A35,AXIOMS:22;
end;
hence |.(sn-FanMorphW).p.|=|.p.|;
end;
hence |.(sn-FanMorphW).p.|=|.p.|;
case q`1>=0;
hence |.(sn-FanMorphW).p.|=|.p.| by Th23;
end;
hence |.(sn-FanMorphW).p.|=|.p.|;
end;
theorem Th41: for sn being Real,x,K0 being set
st -1<sn & sn<1 & x in K0 & K0={p: p`1<=0 & p<>0.REAL 2}
holds (sn-FanMorphW).x in K0
proof let sn be Real,x,K0 be set;
assume A1: -1<sn & sn<1 & x in K0 & K0={p: p`1<=0 & p<>0.REAL 2};
then consider p such that
A2: p=x & p`1<=0 & p<>0.REAL 2;
A3:now assume |.p.|<=0;
then |.p.|=0 by TOPRNS_1:26;
hence contradiction by A2,TOPRNS_1:25;
end;
then A4: (|.p.|)^2>0 by SQUARE_1:74;
now per cases;
case A5: p`2/|.p.|<=sn;
then A6: (sn-FanMorphW).p= |[ |.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2)),
|.p.|*((p`2/|.p.|-sn)/(1+sn))]| by A1,A2,Th25;
reconsider p9= (sn-FanMorphW).p as Point of TOP-REAL 2;
A7: p9`1=|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2)) by A6,EUCLID:56;
A8: 1+sn>0 by A1,Th3;
A9: (|.p.|)^2 =(p`1)^2+(p`2)^2 by JGRAPH_3:10;
now per cases;
case p`1=0;
hence (sn-FanMorphW).x in K0 by A1,A2,Th23;
case p`1<>0;
then 0<(p`1)^2 by SQUARE_1:74;
then 0+(p`2)^2<(p`1)^2+(p`2)^2 by REAL_1:67;
then (p`2)^2/(|.p.|)^2 < (|.p.|)^2/(|.p.|)^2 by A4,A9,REAL_1:73;
then (p`2)^2/(|.p.|)^2 < 1 by A4,XCMPLX_1:60;
then A10: ((p`2)/|.p.|)^2 < 1 by SQUARE_1:69;
p`2/|.p.|-sn<=0 by A5,REAL_2:106;
then A11: (p`2/|.p.|-sn)/(1+sn)<(1+sn)/(1+sn) by A8,REAL_1:73;
-1 < p`2/|.p.| by A10,Th5;
then -1-sn< p`2/|.p.|-sn by REAL_1:54;
then -(1+sn)<p`2/|.p.|-sn by XCMPLX_1:161;
then (-1)*(1+sn)< p`2/|.p.|-sn by XCMPLX_1:180;
then (-1)*(1+sn)/(1+sn)< (p`2/|.p.|-sn)/(1+sn)
by A8,REAL_1:73;
then -1< (p`2/|.p.|-sn)/(1+sn) & (p`2/|.p.|-sn)/(1+sn)<1
by A8,A11,XCMPLX_1:60,90;
then 1^2> ((p`2/|.p.|-sn)/(1+sn))^2 by JGRAPH_2:8;
then 1-((p`2/|.p.|-sn)/(1+sn))^2>0 by SQUARE_1:11,59;
then --sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2)>0 by SQUARE_1:93;
then -sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2)<0 by REAL_1:66;
then |.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2))<0
by A3,SQUARE_1:24;
hence (sn-FanMorphW).x in K0 by A1,A2,A7,JGRAPH_2:11;
end;
hence (sn-FanMorphW).x in K0;
case A12: p`2/|.p.|>sn;
then A13: (sn-FanMorphW).p= |[ |.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2)),
|.p.|*((p`2/|.p.|-sn)/(1-sn))]| by A1,A2,Th25;
reconsider p9= (sn-FanMorphW).p as Point of TOP-REAL 2;
A14: p9`1=|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2)) by A13,EUCLID:56;
A15: 1-sn>0 by A1,Th3;
A16: (|.p.|)^2 =(p`1)^2+(p`2)^2 by JGRAPH_3:10;
now per cases;
case p`1=0;
hence (sn-FanMorphW).x in K0 by A1,A2,Th23;
case p`1<>0;
then 0<(p`1)^2 by SQUARE_1:74;
then 0+(p`2)^2<(p`1)^2+(p`2)^2 by REAL_1:67;
then (p`2)^2/(|.p.|)^2 < (|.p.|)^2/(|.p.|)^2 by A4,A16,REAL_1:73;
then (p`2)^2/(|.p.|)^2 < 1 by A4,XCMPLX_1:60;
then ((p`2)/|.p.|)^2 < 1 by SQUARE_1:69;
then p`2/|.p.|<1 by Th5;
then (p`2/|.p.|-sn)<1-sn by REAL_1:54;
then A17: (p`2/|.p.|-sn)/(1-sn)<(1-sn)/(1-sn) by A15,REAL_1:73;
-(1-sn)< -0 by A15,REAL_1:50;
then A18: -(1-sn)<sn-sn by XCMPLX_1:14;
p`2/|.p.|-sn>=sn-sn by A12,REAL_1:49;
then -(1-sn)<p`2/|.p.|-sn by A18,AXIOMS:22;
then (-1)*(1-sn)< p`2/|.p.|-sn by XCMPLX_1:180;
then (-1)*(1-sn)/(1-sn)< (p`2/|.p.|-sn)/(1-sn)
by A15,REAL_1:73;
then -1< (p`2/|.p.|-sn)/(1-sn) & (p`2/|.p.|-sn)/(1-sn)<1
by A15,A17,XCMPLX_1:60,90;
then 1> ((p`2/|.p.|-sn)/(1-sn))^2 by JGRAPH_2:8,SQUARE_1:59;
then 1-((p`2/|.p.|-sn)/(1-sn))^2>0 by SQUARE_1:11;
then --sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2)>0 by SQUARE_1:93;
then -sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2)<0 by REAL_1:66;
then p9`1<0 by A3,A14,SQUARE_1:24;
hence (sn-FanMorphW).x in K0 by A1,A2,JGRAPH_2:11;
end;
hence (sn-FanMorphW).x in K0;
end;
hence (sn-FanMorphW).x in K0;
end;
theorem Th42: for sn being Real,x,K0 being set
st -1<sn & sn<1 & x in K0 & K0={p: p`1>=0 & p<>0.REAL 2}
holds (sn-FanMorphW).x in K0
proof let sn be Real,x,K0 be set;
assume A1: -1<sn & sn<1 & x in K0 &
K0={p: p`1>=0 & p<>0.REAL 2};
then consider p such that
A2: p=x & p`1>=0 & p<>0.REAL 2;
thus (sn-FanMorphW).x in K0 by A1,A2,Th23;
end;
InclSub { D() -> non empty Subset of TOP-REAL 2, P[set] } :
{ p : P[p] & p<>0.REAL 2 } c= the carrier of (TOP-REAL 2)|D()
provided
A1: D() = (the carrier of TOP-REAL 2) \ {0.REAL 2}
proof
let x be set;
A2:D()` = {0.REAL 2} by A1,JGRAPH_3:30;
assume x in {p: P[p] & p<>0.REAL 2};
then consider p such that A3: x=p & P[p] & p<>0.REAL 2;
now assume not x in D();
then x in (the carrier of TOP-REAL 2) \ D() by A3,XBOOLE_0:def 4;
then x in D()` by SUBSET_1:def 5;
hence contradiction by A2,A3,TARSKI:def 1;
end;
hence thesis by JORDAN1:1;
end;
theorem Th43:for sn being Real,
D being non empty Subset of TOP-REAL 2
st -1<sn & sn<1 & D`={0.REAL 2} holds
ex h being map of (TOP-REAL 2)|D,(TOP-REAL 2)|D
st h=(sn-FanMorphW)|D & h is continuous
proof let sn be Real,D be non empty Subset of TOP-REAL 2;
assume A1: -1<sn & sn<1 & D`={0.REAL 2};
reconsider B0= {0.REAL 2} as Subset of TOP-REAL 2;
A2: D =(B0)` by A1
.=((the carrier of TOP-REAL 2)\ {0.REAL 2}) by SUBSET_1:def 5;
defpred P[Point of TOP-REAL 2] means $1`1<=0;
A3:{p: P[p] & p<>0.REAL 2} c= the carrier of (TOP-REAL 2)|D
from InclSub(A2);
(|[0,1]|)`1=0 & (|[0,1]|)`2=1 by EUCLID:56;
then |[0,1]| in {p where p is Point of TOP-REAL 2:
p`1<=0 & p<>0.REAL 2} by JGRAPH_2:11;
then reconsider K0={p:p`1<=0 & p<>0.REAL 2}
as non empty Subset of (TOP-REAL 2)|D by A3;
defpred P[Point of TOP-REAL 2] means $1`1>=0;
A4:{p: P[p] & p<>0.REAL 2} c= the carrier of (TOP-REAL 2)|D
from InclSub(A2);
set Y1=|[0,1]|;
Y1`1=0 & Y1`2=1 by EUCLID:56;
then Y1 in {p where p is Point of TOP-REAL 2:
p`1>=0 & p<>0.REAL 2} by JGRAPH_2:11;
then reconsider K1={p: p`1>=0 & p<>0.REAL 2}
as non empty Subset of (TOP-REAL 2)|D by A4;
A5:the carrier of ((TOP-REAL 2)|D) =D by JORDAN1:1;
A6: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
A7: p8=z & p8`1<=0 & p8<>0.REAL 2;
thus z in (the carrier of TOP-REAL 2) by A7;
end;
A8:dom ((sn-FanMorphW)|K0)= dom ((sn-FanMorphW)) /\ K0 by FUNCT_1:68
.=((the carrier of TOP-REAL 2)) /\ K0 by FUNCT_2:def 1
.=K0 by A6,XBOOLE_1:28;
A9: K0 =the carrier of ((TOP-REAL 2)|D)|K0 by JORDAN1:1;
rng ((sn-FanMorphW)|K0) c= the carrier of ((TOP-REAL 2)|D)|K0
proof let y be set;assume y in rng ((sn-FanMorphW)|K0);
then consider x being set such that
A10:x in dom ((sn-FanMorphW)|K0)
& y=((sn-FanMorphW)|K0).x by FUNCT_1:def 5;
x in (dom (sn-FanMorphW)) /\ K0 by A10,FUNCT_1:68;
then A11:x in K0 by XBOOLE_0:def 3;
K0 c= the carrier of TOP-REAL 2 by A5,XBOOLE_1:1;
then reconsider p=x as Point of TOP-REAL 2 by A11;
(sn-FanMorphW).p=y by A10,A11,FUNCT_1:72;
then y in K0 by A1,A11,Th41;
hence y in the carrier of ((TOP-REAL 2)|D)|K0 by JORDAN1:1;
end;
then rng ((sn-FanMorphW)|K0)c= the carrier of ((TOP-REAL 2)|D)
by A9,XBOOLE_1:1;
then (sn-FanMorphW)|K0 is Function of the carrier of ((TOP-REAL 2)|D)|K0,
the carrier of ((TOP-REAL 2)|D) by A8,A9,FUNCT_2:4;
then reconsider f=(sn-FanMorphW)|K0 as map of ((TOP-REAL 2)|D)|K0,
((TOP-REAL 2)|D) ;
A12: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
A13: p8=z & p8`1>=0 & p8<>0.REAL 2;
thus z in (the carrier of TOP-REAL 2) by A13;
end;
A14:dom ((sn-FanMorphW)|K1)= dom ((sn-FanMorphW)) /\ K1 by FUNCT_1:68
.=((the carrier of TOP-REAL 2)) /\ K1 by FUNCT_2:def 1
.=K1 by A12,XBOOLE_1:28;
A15: K1=the carrier of ((TOP-REAL 2)|D)|K1 by JORDAN1:1;
rng ((sn-FanMorphW)|K1) c= the carrier of ((TOP-REAL 2)|D)|K1
proof let y be set;assume y in rng ((sn-FanMorphW)|K1);
then consider x being set such that
A16:x in dom ((sn-FanMorphW)|K1)
& y=((sn-FanMorphW)|K1).x by FUNCT_1:def 5;
x in (dom (sn-FanMorphW)) /\ K1 by A16,FUNCT_1:68;
then A17:x in K1 by XBOOLE_0:def 3;
K1 c= the carrier of TOP-REAL 2 by A5,XBOOLE_1:1;
then reconsider p=x as Point of TOP-REAL 2 by A17;
(sn-FanMorphW).p=y by A16,A17,FUNCT_1:72;
then y in K1 by A1,A17,Th42;
hence y in the carrier of ((TOP-REAL 2)|D)|K1 by JORDAN1:1;
end;
then rng ((sn-FanMorphW)|K1)c= the carrier of ((TOP-REAL 2)|D)
by A15,XBOOLE_1:1;
then (sn-FanMorphW)|K1 is Function of the carrier of ((TOP-REAL 2)|D)|K1,
the carrier of ((TOP-REAL 2)|D) by A14,A15,FUNCT_2:4;
then reconsider g=(sn-FanMorphW)|K1 as map of ((TOP-REAL 2)|D)|K1,
((TOP-REAL 2)|D) ;
A18:K0=[#](((TOP-REAL 2)|D)|K0) by PRE_TOPC:def 10;
A19:K1=[#](((TOP-REAL 2)|D)|K1) by PRE_TOPC:def 10;
A20:D= [#]((TOP-REAL 2)|D) by PRE_TOPC:def 10;
A21:K0 \/ K1 c= D
proof let x be set;assume A22:x in K0 \/ K1;
now per cases by A22,XBOOLE_0:def 2;
case x in K0;
then consider p such that A23:p=x &
p`1<=0 & p<>0.REAL 2;
thus
x in the carrier of TOP-REAL 2 & not x=0.REAL 2 by A23;
case x in K1;
then consider p such that A24:p=x &
p`1>=0 & p<>0.REAL 2;
thus x in the carrier of TOP-REAL 2 & not x=0.REAL 2 by A24;
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 A25: x in D;
then A26: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 A25;
px`1<=0 & px<>0.REAL 2 or
px`1>=0 & px<>0.REAL 2 by A26,TARSKI:def 1;
then x in K0 or x in K1;
hence x in K0 \/ K1 by XBOOLE_0:def 2;
end;
then A27:([#](((TOP-REAL 2)|D)|K0)) \/ ([#](((TOP-REAL 2)|D)|K1))
= [#]((TOP-REAL 2)|D) by A18,A19,A20,A21,XBOOLE_0:def 10;
A28: f is continuous & K0 is closed by A1,A2,Th36,Th37;
A29: g is continuous & K1 is closed by A1,A2,Th38,Th39;
A30: 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 A31:x in K0 & x in K1 by A18,A19,XBOOLE_0:def 3;
then f.x=(sn-FanMorphW).x by FUNCT_1:72;
hence f.x = g.x by A31,FUNCT_1:72;
end;
then consider h being map of (TOP-REAL 2)|D,(TOP-REAL 2)|D
such that A32: h= f+*g & h is continuous
by A18,A19,A27,A28,A29,JGRAPH_2:9;
A33:dom h=the carrier of ((TOP-REAL 2)|D) by FUNCT_2:def 1;
A34:the carrier of ((TOP-REAL 2)|D)=D by JORDAN1:1;
A35:the carrier of ((TOP-REAL 2)|D) =
((the carrier of TOP-REAL 2)\ {0.REAL 2}) by A2,JORDAN1:1;
dom (sn-FanMorphW)=(the carrier of (TOP-REAL 2))
by FUNCT_2:def 1;
then A36:dom ((sn-FanMorphW)|D)=(the carrier of (TOP-REAL 2))/\ D
by FUNCT_1:68
.=the carrier of ((TOP-REAL 2)|D) by A34,XBOOLE_1:28;
A37:dom f=K0 by A9,FUNCT_2:def 1;
A38:K0=[#](((TOP-REAL 2)|D)|K0) by PRE_TOPC:def 10;
A39:dom g=K1 by A15,FUNCT_2:def 1;
K1=[#](((TOP-REAL 2)|D)|K1) by PRE_TOPC:def 10;
then A40: f tolerates g by A30,A37,A38,A39,PARTFUN1:def 6;
for x being set st x in dom h holds h.x=((sn-FanMorphW)|D).x
proof let x be set;assume A41: x in dom h;
then x in (the carrier of TOP-REAL 2) & not x in {0.REAL 2}
by A33,A35,XBOOLE_0:def 4;
then A42:x <>0.REAL 2 by TARSKI:def 1;
reconsider p=x as Point of TOP-REAL 2 by A33,A35,A41,XBOOLE_0:def 4;
A43: x in D`` by A33,A41,JORDAN1:1;
now per cases;
case A44:x in K0;
A45:(sn-FanMorphW)|D.p=(sn-FanMorphW).p by A43,FUNCT_1:72
.=f.p by A44,FUNCT_1:72;
h.p=(g+*f).p by A32,A40,FUNCT_4:35
.=f.p by A37,A44,FUNCT_4:14;
hence h.x=(sn-FanMorphW)|D.x by A45;
case not x in K0;
then not (p`1<=0) by A42;
then A46:x in K1 by A42;
(sn-FanMorphW)|D.p=(sn-FanMorphW).p by A43,FUNCT_1:72
.=g.p by A46,FUNCT_1:72;
hence h.x=(sn-FanMorphW)|D.x by A32,A39,A46,FUNCT_4:14;
end;
hence h.x=(sn-FanMorphW)|D.x;
end;
then f+*g=(sn-FanMorphW)|D by A32,A33,A36,FUNCT_1:9;
hence thesis by A18,A19,A27,A28,A29,A30,JGRAPH_2:9;
end;
theorem Th44: for sn being Real
st -1<sn & sn<1 holds
ex h being map of (TOP-REAL 2),(TOP-REAL 2)
st h=(sn-FanMorphW) & h is continuous
proof let sn be Real;
assume A1: -1<sn & sn<1;
reconsider f=(sn-FanMorphW) 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 XB