{} & C<>{} holds ex g being Function of X,Z st g is continuous & g=h*f; reserve p,q for Point of TOP-REAL 2; definition func Out_In_Sq -> Function of NonZero TOP-REAL 2, NonZero TOP-REAL 2 means :: JGRAPH_2:def 1 for p being Point of TOP-REAL 2 st p<>0.TOP-REAL 2 holds ((p`2<=p`1 & -p `1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies it.p=|[1/p`1,p`2/p`1/p`1]|) & (not(p`2 <=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies it.p=|[p`1/p`2/p`2,1/p`2]|); end; theorem :: JGRAPH_2:13 for p being Point of TOP-REAL 2 st not(p`2<=p`1 & -p`1<=p`2 or p `2>=p`1 & p`2<=-p`1) holds p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2; theorem :: JGRAPH_2:14 for p being Point of TOP-REAL 2 st p<>0.TOP-REAL 2 holds ((p`1<= p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2)implies Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2 ]|) & (not (p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) implies Out_In_Sq.p= |[1/p`1,p`2/p`1/p`1]|); theorem :: JGRAPH_2:15 for D being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL 2 )|D st K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2} holds rng (Out_In_Sq|K0) c= the carrier of ((TOP-REAL 2)|D)|K0; theorem :: JGRAPH_2:16 for D being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL 2 )|D st K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2} holds rng (Out_In_Sq|K0) c= the carrier of ((TOP-REAL 2)|D)|K0; theorem :: JGRAPH_2:17 for K0a being set,D being non empty Subset of TOP-REAL 2 st K0a= {p where p is Point of TOP-REAL 2: (p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p `1) & p<>0.TOP-REAL 2} & D`={0.TOP-REAL 2} holds K0a is non empty Subset of ( TOP-REAL 2)|D & K0a is non empty Subset of TOP-REAL 2; theorem :: JGRAPH_2:18 for K0a being set,D being non empty Subset of TOP-REAL 2 st K0a= {p where p is Point of TOP-REAL 2: (p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p `2) & p<>0.TOP-REAL 2} & D`={0.TOP-REAL 2} holds K0a is non empty Subset of ( TOP-REAL 2)|D & K0a is non empty Subset of TOP-REAL 2; theorem :: JGRAPH_2:19 for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r1+r2 ) & g is continuous; theorem :: JGRAPH_2:20 for X being non empty TopSpace, a being Real holds ex g being Function of X,R^1 st (for p being Point of X holds g.p=a) & g is continuous; theorem :: JGRAPH_2:21 for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r1-r2 ) & g is continuous; theorem :: JGRAPH_2:22 for X being non empty TopSpace, f1 being Function of X,R^1 st f1 is continuous ex g being Function of X,R^1 st (for p being Point of X,r1 being Real st f1.p=r1 holds g.p=r1*r1) & g is continuous; theorem :: JGRAPH_2:23 for X being non empty TopSpace, f1 being Function of X,R^1,a being Real st f1 is continuous holds ex g being Function of X,R^1 st ( for p being Point of X,r1 being Real st f1.p=r1 holds g.p=a*r1) & g is continuous; theorem :: JGRAPH_2:24 for X being non empty TopSpace, f1 being Function of X,R^1,a being Real st f1 is continuous holds ex g being Function of X,R^1 st ( for p being Point of X,r1 being Real st f1.p=r1 holds g.p=r1+a) & g is continuous; theorem :: JGRAPH_2:25 for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r1*r2 ) & g is continuous; theorem :: JGRAPH_2:26 for X being non empty TopSpace, f1 being Function of X,R^1 st f1 is continuous & (for q being Point of X holds f1.q<>0) holds ex g being Function of X,R^1 st (for p being Point of X,r1 being Real st f1.p=r1 holds g.p=1/r1) & g is continuous; theorem :: JGRAPH_2:27 for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0) holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r1/r2) & g is continuous; theorem :: JGRAPH_2:28 for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0) holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r1/r2/r2) & g is continuous; theorem :: JGRAPH_2:29 for K0 being Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K0,R^1 st (for p being Point of (TOP-REAL 2)|K0 holds f.p=proj1.p) holds f is continuous; theorem :: JGRAPH_2:30 for K0 being Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K0,R^1 st (for p being Point of (TOP-REAL 2)|K0 holds f.p=proj2.p) holds f is continuous; theorem :: JGRAPH_2:31 for K1 being non empty Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K1,R^1 st (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=1/p`1) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1<>0 ) holds f is continuous; theorem :: JGRAPH_2:32 for K1 being non empty Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K1,R^1 st (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=1/p`2) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2<>0 ) holds f is continuous; theorem :: JGRAPH_2:33 for K1 being non empty Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K1,R^1 st (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=p`2/p`1/p`1) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1<>0 ) holds f is continuous; theorem :: JGRAPH_2:34 for K1 being non empty Subset of TOP-REAL 2, f being Function of (TOP-REAL 2)|K1,R^1 st (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=p`1/p`2/p`2) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2<>0 ) holds f is continuous; theorem :: JGRAPH_2:35 for K0,B0 being Subset of TOP-REAL 2, f being Function of ( TOP-REAL 2)|K0,(TOP-REAL 2)|B0, f1,f2 being Function of (TOP-REAL 2)|K0,R^1 st f1 is continuous & f2 is continuous & K0<>{} & B0<>{} & (for x,y,r,s being Real st |[x,y]| in K0 & r=f1.(|[x,y]|) & s=f2.(|[x,y]|) holds f.(|[x,y]|)=|[r ,s]|) holds f is continuous; theorem :: JGRAPH_2:36 for K0,B0 being Subset of TOP-REAL 2,f being Function of ( TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=Out_In_Sq|K0 & B0=NonZero TOP-REAL 2 & K0={ p: (p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2} holds f is continuous; theorem :: JGRAPH_2:37 for K0,B0 being Subset of TOP-REAL 2,f being Function of ( TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=Out_In_Sq|K0 & B0=NonZero TOP-REAL 2 & K0={ p: (p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2} holds f is continuous; scheme :: JGRAPH_2:sch 1 TopSubset { P[set] } : { p where p is Point of TOP-REAL 2 : P[p] } is Subset of TOP-REAL 2; scheme :: JGRAPH_2:sch 2 TopCompl { P[set], K() -> Subset of TOP-REAL 2 } : K()` = { p where p is Point of TOP-REAL 2 : not P[p] } provided K() = { p where p is Point of TOP-REAL 2 : P[p] }; scheme :: JGRAPH_2:sch 3 ClosedSubset { F,G(Point of TOP-REAL 2) -> Real } : {p where p is Point of TOP-REAL 2 : F(p) <= G(p) } is closed Subset of TOP-REAL 2 provided for p,q being Point of TOP-REAL 2 holds F(p-q) = F(p) - F(q) & G(p-q ) = G(p) - G(q) and for p,q being Point of TOP-REAL 2 holds (|. (p-q).|)^2 = (F(p-q))^2+ (G(p-q))^2; theorem :: JGRAPH_2:38 for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2 )|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=Out_In_Sq| K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p `1) & p<>0.TOP-REAL 2} holds f is continuous & K0 is closed; theorem :: JGRAPH_2:39 for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2 )|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=Out_In_Sq| K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p `2) & p<>0.TOP-REAL 2} holds f is continuous & K0 is closed; theorem :: JGRAPH_2:40 for D being non empty Subset of TOP-REAL 2 st D`={0.TOP-REAL 2} holds ex h being Function of (TOP-REAL 2)|D,(TOP-REAL 2)|D st h=Out_In_Sq & h is continuous; theorem :: JGRAPH_2:41 for B,K0,Kb being Subset of TOP-REAL 2 st B={0.TOP-REAL 2} & K0= {p: -10.TOP-REAL 2 holds not f.t in K0 \/ Kb) &(for r being Point of TOP-REAL 2 st not r in K0 \/ Kb holds f.r in K0) & for s being Point of TOP-REAL 2 st s in Kb holds f.s=s; theorem :: JGRAPH_2:42 for f,g being Function of I[01],TOP-REAL 2, K0 being Subset of TOP-REAL 2, O,I being Point of I[01] st O=0 & I=1 & f is continuous one-to-one & g is continuous one-to-one & K0={p: -1

Function of TOP-REAL 2,TOP-REAL 2 means :: JGRAPH_2:def 2 for t being Point of TOP-REAL 2 holds it.t=|[A*(t`1)+B,C*(t`2)+D]|; end; registration let a,b,c,d be Real; cluster AffineMap(a,b,c,d) -> continuous; end; theorem :: JGRAPH_2:44 for A,B,C,D being Real st A>0 & C>0 holds AffineMap(A,B,C ,D) is one-to-one; theorem :: JGRAPH_2:45 for f,g being Function of I[01],TOP-REAL 2,a,b,c,d being Real , O,I being Point of I[01] st O=0 & I=1 & f is continuous one-to-one & g is continuous one-to-one & (f.O)`1=a & (f.I)`1=b & c <=(f.O)`2 & (f.O)`2<=d & c <= (f.I)`2 & (f.I)`2<=d & (g.O)`2=c & (g.I)`2=d & a<=(g.O)`1 & (g.O)`1<=b & a<=(g. I)`1 & (g.I)`1<=b & a < b & c < d & not (ex r being Point of I[01] st a<(f.r)`1 & (f.r)`1