:: Fashoda Meet Theorem for Rectangles
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received January 3, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, PRE_TOPC, EUCLID, ARYTM_3, MCART_1, XXREAL_0, RLTOPSP1,
ARYTM_1, REAL_1, CARD_1, RELAT_1, SUBSET_1, TOPREAL1, FUNCT_1, BORSUK_1,
ORDINAL2, TOPS_2, JORDAN3, JGRAPH_6, PSCOMP_1, JORDAN17, JGRAPH_2,
STRUCT_0, FUNCT_2, VALUED_1, TARSKI, XBOOLE_0;
notations XBOOLE_0, ORDINAL1, NUMBERS, XCMPLX_0, TARSKI, TOPS_2, RLVECT_1,
RLTOPSP1, EUCLID, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SUBSET_1,
STRUCT_0, TOPMETR, PRE_TOPC, JORDAN6, JORDAN17, JGRAPH_2, XREAL_0,
TOPREAL1, PSCOMP_1, REAL_1, JGRAPH_6, XXREAL_0;
constructors REAL_1, RCOMP_1, TOPS_2, TOPMETR, TOPREAL1, SPPOL_2, PSCOMP_1,
JORDAN6, JGRAPH_2, JORDAN17, JGRAPH_6, BINOP_2;
registrations XBOOLE_0, RELSET_1, FUNCT_2, XREAL_0, MEMBERED, STRUCT_0,
BORSUK_1, EUCLID, JGRAPH_2;
requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
definitions TARSKI;
equalities STRUCT_0, RLTOPSP1;
theorems XBOOLE_0, FUNCT_1, FUNCT_2, TOPS_2, PRE_TOPC, EUCLID, JGRAPH_2,
BORSUK_1, TOPREAL1, JORDAN7, JORDAN17, XCMPLX_1, JGRAPH_6, JORDAN1K,
XREAL_1, XXREAL_0, XXREAL_1;
begin
theorem Th1:
for a,b,d being Real,p being Point of TOP-REAL 2 st a **0 by A1,XREAL_1:50;
p`1-a <=b-a by A4,XREAL_1:9;
then w<=(b-a)/(b-a) by A5,XREAL_1:72;
then
A6: w<=1 by A5,XCMPLX_1:60;
p`1-a>=0 by A3,XREAL_1:48;
then
A7: 0<=w by A5,XREAL_1:136;
(1-w)*(|[a,d]|)+w*(|[b,d]|) =|[(1-w)*a,(1-w)*d]|+w*(|[b,d]|) by EUCLID:58
.=|[(1-w)*a,(1-w)*d]|+(|[w*b,w*d]|) by EUCLID:58
.=|[(1-w)*a+w*b,(1-w)*d+w*d]| by EUCLID:56
.= |[a+w*(b-a),d]|
.= |[a+(p`1-a),d]| by A5,XCMPLX_1:87
.= p by A2,EUCLID:53;
hence thesis by A7,A6;
end;
theorem Th2:
for n being Element of NAT, P being Subset of TOP-REAL n, p1,p2
being Point of TOP-REAL n st P is_an_arc_of p1,p2 holds ex f being Function of
I[01],TOP-REAL n st f is continuous one-to-one & rng f=P & f.0=p1 & f.1=p2
proof
let n be Element of NAT,P be Subset of TOP-REAL n, p1,p2 be Point of
TOP-REAL n;
assume
A1: P is_an_arc_of p1,p2;
then consider f2 being Function of I[01], (TOP-REAL n)|P such that
A2: f2 is being_homeomorphism and
A3: f2.0 = p1 and
A4: f2.1 = p2 by TOPREAL1:def 1;
p1 in P by A1,TOPREAL1:1;
then consider g being Function of I[01],TOP-REAL n such that
A5: f2=g and
A6: g is continuous and
A7: g is one-to-one by A2,JORDAN7:15;
rng g =[#]((TOP-REAL n)|P) by A2,A5,TOPS_2:def 5
.=P by PRE_TOPC:def 5;
hence thesis by A3,A4,A5,A6,A7;
end;
theorem Th3:
for p1,p2 being Point of TOP-REAL 2, b,c,d being Real st
p1`1****=p2`2 by A6,A7,XXREAL_0:2;
then
A8: p2 in LSeg(|[b,d]|,|[b,c]|) by A2,A4,A5,JGRAPH_6:2;
p1`2>= c by A5,A6,XXREAL_0:2;
then p1 in LSeg(|[b,d]|,|[b,c]|) by A2,A3,A7,JGRAPH_6:2;
hence thesis by A1,A2,A6,A8,JGRAPH_6:61;
end;
theorem Th11:
for p1,p2 being Point of TOP-REAL 2, a,b,c,d being Real
st a****p2`1 by A6,A7,XXREAL_0:2;
then
A8: p2 in LSeg(|[b,c]|,|[a,c]|) by A1,A4,A5,Th1;
W-min K=|[a,c]| by A1,A2,JGRAPH_6:46;
then
A9: (W-min(K))`1=a by EUCLID:52;
p1`1>a by A5,A6,XXREAL_0:2;
then p1 in LSeg(|[b,c]|,|[a,c]|) by A1,A3,A7,Th1;
hence thesis by A1,A2,A5,A6,A8,A9,JGRAPH_6:62;
end;
theorem Th13:
for p1,p2 being Point of TOP-REAL 2, a,b,c,d being Real
st a**** c by A10,A11,XXREAL_0:2;
c p3`1 & p4`2
<> p2`2 & p4`2 <=p1`2 & p1`2<=p2`2 & p1`1<=p2`1 & p2`1<=p3`1 & p4`2 <=p3`2 & p3
`2<=p2`2 & p1`1 p3`1 and
A2: p4`2 <> p2`2 and
A3: p4`2 <=p1`2 and
A4: p1`2<=p2`2 and
A5: p1`1<=p2`1 and
A6: p2`1<=p3`1 and
A7: p4`2 <=p3`2 and
A8: p3`2<=p2`2 and
A9: p1`1 =p2`2 & p2`2>p3`2 & p3`2>p4`2 & p4`2>= c holds p1,p2,p3,p4
are_in_this_order_on rectangle(a,b,c,d)
proof
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d being Real;
set K=rectangle(a,b,c,d);
assume that
A1: a****=p2`2 and
A10: p2`2>p3`2 and
A11: p3`2>p4`2 and
A12: p4`2>= c;
A13: p3`2p4`2 by A10,A11,XXREAL_0:2;
then
A14: p2`2> c by A12,XXREAL_0:2;
c =p2`2 & p2`2>p3`2 & p3`2>=c & a=p2`2 and
A10: p2`2>p3`2 and
A11: p3`2>=c and
A12: a c by A10,A11,XXREAL_0:2;
then
LE p1,p2,K & LE p2,p3,K & LE p3,p4,K or LE p2,p3,K & LE p3,p4,K & LE p4
,p1,K or LE p3,p4,K & LE p4,p1,K & LE p1,p2,K or LE p4,p1,K & LE p1,p2,K & LE
p2,p3,K by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,Th5,Th10,Th11;
hence thesis by JORDAN17:def 1;
end;
theorem Th32:
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real
st a****a by A11,A12,XXREAL_0:2;
then
LE p1,p2,K & LE p2,p3,K & LE p3,p4,K or LE p2,p3,K & LE p3,p4,K & LE p4
,p1,K or LE p3,p4,K & LE p4,p1,K & LE p1,p2,K or LE p4,p1,K & LE p1,p2,K & LE
p2,p3,K by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,Th5,Th11,Th12;
hence thesis by JORDAN17:def 1;
end;
theorem Th33:
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real
st a****p4`1 by A10,A11,XXREAL_0:2;
then
A14: p2`1> a by A9,XXREAL_0:2;
a p1`1 by A8,A9,XXREAL_0:2;
then
A14: p3`1>a by A7,XXREAL_0:2;
p2`1<=b by A9,A10,XXREAL_0:2;
then
LE p1,p2,K & LE p2,p3,K & LE p3,p4,K or LE p2,p3,K & LE p3,p4,K & LE p4
,p1,K or LE p3,p4,K & LE p4,p1,K & LE p1,p2,K or LE p4,p1,K & LE p1,p2,K & LE
p2,p3,K by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,Th7,Th9;
hence thesis by JORDAN17:def 1;
end;
theorem Th37:
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real
st a**** c by A10,A11,XXREAL_0:2;
a a by A10,A11,XXREAL_0:2;
a =p2`2 & p2`2>p3`2 & p3`2>p4`2 & p4`2>= c holds p1,p2,p3,p4
are_in_this_order_on rectangle(a,b,c,d)
proof
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d being Real;
set K=rectangle(a,b,c,d);
assume that
A1: a****=p2`2 and
A10: p2`2>p3`2 and
A11: p3`2>p4`2 and
A12: p4`2>= c;
A13: p3`2> c by A11,A12,XXREAL_0:2;
p2`2>p4`2 by A10,A11,XXREAL_0:2;
then
A14: p2`2> c by A12,XXREAL_0:2;
d>p3`2 by A9,A10,XXREAL_0:2;
then
LE p1,p2,K & LE p2,p3,K & LE p3,p4,K or LE p2,p3,K & LE p3,p4,K & LE p4
,p1,K or LE p3,p4,K & LE p4,p1,K & LE p1,p2,K or LE p4,p1,K & LE p1,p2,K & LE
p2,p3,K by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A14,A13,Th8,Th10;
hence thesis by JORDAN17:def 1;
end;
theorem Th41:
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real
st a****=p2`2 & p2`2>p3`2 & p3`2>= c & a =p2`2 and
A10: p2`2>p3`2 and
A11: p3`2>= c and
A12: a p3`2 by A9,A10,XXREAL_0:2;
p2`2> c by A10,A11,XXREAL_0:2;
then
LE p1,p2,K & LE p2,p3,K & LE p3,p4,K or LE p2,p3,K & LE p3,p4,K & LE p4
,p1,K or LE p3,p4,K & LE p4,p1,K & LE p1,p2,K or LE p4,p1,K & LE p1,p2,K & LE
p2,p3,K by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,Th8,Th10,Th11;
hence thesis by JORDAN17:def 1;
end;
theorem Th42:
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real
st a****p4`1 by A10,A11,XXREAL_0:2;
then
A14: p2`1> a by A9,XXREAL_0:2;
a =p1`2 & p1`2>p2
`2 & p2`2>p3`2 & p3`2>p4`2 & p4`2>= c holds p1,p2,p3,p4 are_in_this_order_on
rectangle(a,b,c,d)
proof
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d being Real;
set K=rectangle(a,b,c,d);
assume that
A1: a****=p1`2 and
A8: p1`2>p2`2 and
A9: p2`2>p3`2 and
A10: p3`2>p4`2 and
A11: p4`2>= c;
A12: p3`2> c by A10,A11,XXREAL_0:2;
p2`2>p4`2 by A9,A10,XXREAL_0:2;
then
A13: p2`2> c by A11,XXREAL_0:2;
A14: d >p2`2 by A7,A8,XXREAL_0:2;
then d >p3`2 by A9,XXREAL_0:2;
then
LE p1,p2,K & LE p2,p3,K & LE p3,p4,K or LE p2,p3,K & LE p3,p4,K & LE p4
,p1,K or LE p3,p4,K & LE p4,p1,K & LE p1,p2,K or LE p4,p1,K & LE p1,p2,K & LE
p2,p3,K by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A13,A14,A12,Th10;
hence thesis by JORDAN17:def 1;
end;
theorem Th45:
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real
st a****=p1`2 & p1`2>p2
`2 & p2`2>p3`2 & p3`2>= c & a=p1`2 and
A8: p1`2>p2`2 and
A9: p2`2>p3`2 and
A10: p3`2>= c and
A11: a c by A9,A10,XXREAL_0:2;
A14: d >p2`2 by A7,A8,XXREAL_0:2;
then d >p3`2 by A9,XXREAL_0:2;
then
LE p1,p2,K & LE p2,p3,K & LE p3,p4,K or LE p2,p3,K & LE p3,p4,K & LE p4
,p1,K or LE p3,p4,K & LE p4,p1,K & LE p1,p2,K or LE p4,p1,K & LE p1,p2,K & LE
p2,p3,K by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,Th10,Th11;
hence thesis by JORDAN17:def 1;
end;
theorem Th46:
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real
st a****=p1`2 & p1`2>
p2`2 & p2`2>= c & b>=p3`1 & p3`1>p4`1 & p4`1>a holds p1,p2,p3,p4
are_in_this_order_on rectangle(a,b,c,d)
proof
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d being Real;
set K=rectangle(a,b,c,d);
assume that
A1: a****=p1`2 and
A8: p1`2>p2`2 and
A9: p2`2>= c and
A10: b>=p3`1 and
A11: p3`1>p4`1 and
A12: p4`1>a;
A13: p3`1>a by A11,A12,XXREAL_0:2;
d >p2`2 by A7,A8,XXREAL_0:2;
then
LE p1,p2,K & LE p2,p3,K & LE p3,p4,K or LE p2,p3,K & LE p3,p4,K & LE p4
,p1,K or LE p3,p4,K & LE p4,p1,K & LE p1,p2,K or LE p4,p1,K & LE p1,p2,K & LE
p2,p3,K by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,Th10,Th11,Th12;
hence thesis by JORDAN17:def 1;
end;
theorem Th47:
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real
st a****=p2`1 & p2`1>p3`1 & p3`1>p4`1 & p4`1> a holds p1,p2,p3,p4
are_in_this_order_on rectangle(a,b,c,d)
proof
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d being Real;
set K=rectangle(a,b,c,d);
assume that
A1: a****=p2`1 and
A10: p2`1>p3`1 and
A11: p3`1>p4`1 and
A12: p4`1> a;
A13: p3`1>a by A11,A12,XXREAL_0:2;
p2`1>p4`1 by A10,A11,XXREAL_0:2;
then
A14: p2`1>a by A12,XXREAL_0:2;
b>p3`1 by A9,A10,XXREAL_0:2;
then
LE p1,p2,K & LE p2,p3,K & LE p3,p4,K or LE p2,p3,K & LE p3,p4,K & LE p4
,p1,K or LE p3,p4,K & LE p4,p1,K & LE p1,p2,K or LE p4,p1,K & LE p1,p2,K & LE
p2,p3,K by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A14,A13,Th11,Th12;
hence thesis by JORDAN17:def 1;
end;
theorem Th48:
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real
st a****=p1`1 & p1`1
>p2`1 & p2`1>p3`1 & p3`1>p4`1 & p4`1> a holds p1,p2,p3,p4 are_in_this_order_on
rectangle(a,b,c,d)
proof
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d being Real;
set K=rectangle(a,b,c,d);
assume that
A1: a****=p1`1 and
A8: p1`1>p2`1 and
A9: p2`1>p3`1 and
A10: p3`1>p4`1 and
A11: p4`1> a;
A12: p3`1>a by A10,A11,XXREAL_0:2;
p2`1>p4`1 by A9,A10,XXREAL_0:2;
then
A13: p2`1>a by A11,XXREAL_0:2;
A14: b>p2`1 by A7,A8,XXREAL_0:2;
then b >p3`1 by A9,XXREAL_0:2;
then
LE p1,p2,K & LE p2,p3,K & LE p3,p4,K or LE p2,p3,K & LE p3,p4,K & LE p4
,p1,K or LE p3,p4,K & LE p4,p1,K & LE p1,p2,K or LE p4,p1,K & LE p1,p2,K & LE
p2,p3,K by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A13,A14,A12,Th12;
hence thesis by JORDAN17:def 1;
end;
theorem Th49:
for A,B,C,D being Real, h,g being Function of TOP-REAL 2,
TOP-REAL 2 st A>0 & C>0 & h=AffineMap(A,B,C,D) & g=AffineMap(1/A,-B/A,1/C,-D/C)
holds g=h" & h=g"
proof
let A,B,C,D being Real, h,g being Function of TOP-REAL 2,TOP-REAL 2;
assume that
A1: A>0 and
A2: C>0 and
A3: h=AffineMap(A,B,C,D) and
A4: g=AffineMap(1/A,-B/A,1/C,-D/C);
A5: h is one-to-one by A1,A2,A3,JGRAPH_2:44;
A6: for x,y being object st x in dom h & y in dom g holds h.x = y iff g.y = x
proof
let x,y be object;
assume that
A7: x in dom h and
A8: y in dom g;
reconsider py=y as Point of TOP-REAL 2 by A8;
reconsider px=x as Point of TOP-REAL 2 by A7;
A9: h.x=y implies g.y=x
proof
assume
A10: h.x=y;
A11: (h.px)= |[A*(px`1)+B,C*(px`2)+D]| by A3,JGRAPH_2:def 2;
then py`1=A*(px`1)+B by A10,EUCLID:52;
then
A12: (1/A)*(py`1)+-B/A =(1/A*A)*px`1+(1/A)*B +-B/A
.=1*px`1+(1/A)*B +-B/A by A1,XCMPLX_1:106
.=px`1+B/A+-B/A by XCMPLX_1:99
.=px`1;
py`2=C*(px`2)+D by A10,A11,EUCLID:52;
then
A13: (1/C)*(py`2)+-D/C =(1/C*C)*px`2+(1/C)*D +-D/C
.=1*px`2+(1/C)*D +-D/C by A2,XCMPLX_1:106
.=px`2+D/C+-D/C by XCMPLX_1:99
.=px`2;
(g.py)= |[(1/A)*(py`1)+-B/A,(1/C)*(py`2)+-D/C]| by A4,JGRAPH_2:def 2;
hence thesis by A12,A13,EUCLID:53;
end;
g.y=x implies h.x=y
proof
assume
A14: g.y=x;
A15: (g.py)= |[1/A*(py`1)+-B/A,1/C*(py`2)+-D/C]| by A4,JGRAPH_2:def 2;
then px`1=1/A*(py`1)+-B/A by A14,EUCLID:52;
then
A16: (A)*(px`1)+B =(A*(1/A))*(py`1)+(A)*(-B/A) +B
.=1*py`1+(A)*(-B/A) +B by A1,XCMPLX_1:106
.=py`1+A*((-B)/A)+B by XCMPLX_1:187
.=py`1+(-B)+B by A1,XCMPLX_1:87
.=py`1;
px`2=1/C*(py`2)+-D/C by A14,A15,EUCLID:52;
then
A17: (C)*(px`2)+D =(C*(1/C))*(py`2)+(C)*(-D/C) +D
.=1*(py`2)+(C)*(-D/C) +D by A2,XCMPLX_1:106
.=py`2+C*((-D)/C)+D by XCMPLX_1:187
.=py`2+(-D)+D by A2,XCMPLX_1:87
.=py`2;
(h.px)= |[(A)*(px`1)+B,(C)*(px`2)+D]| by A3,JGRAPH_2:def 2;
hence thesis by A16,A17,EUCLID:53;
end;
hence thesis by A9;
end;
A18: dom g=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
reconsider RD=D as Real;
reconsider RC=C as Real;
reconsider RB=B as Real;
reconsider RA=A as Real;
A19: g= AffineMap(1/RA,-RB/RA,1/RC,-RD/RC) by A4;
h= AffineMap(RA,RB,RC,RD) by A3;
then h is onto by A1,A2,JORDAN1K:36;
then
A20: rng h=the carrier of TOP-REAL 2 by FUNCT_2:def 3;
A21: 1/C>0 by A2,XREAL_1:139;
1/A>0 by A1,XREAL_1:139;
then g is onto by A21,A19,JORDAN1K:36;
then
A22: rng g=the carrier of TOP-REAL 2 by FUNCT_2:def 3;
dom h=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then g = h" by A5,A18,A20,A22,A6,FUNCT_1:38;
hence thesis by A5,FUNCT_1:43;
end;
theorem Th50:
for A,B,C,D being Real, h being Function of TOP-REAL 2,
TOP-REAL 2 st A>0 & C >0 & h=AffineMap(A,B,C,D) holds h is being_homeomorphism
& for p1,p2 being Point of TOP-REAL 2 st p1`10 and
A2: C >0 and
A3: h=AffineMap(A,B,C,D);
A4: h is one-to-one by A1,A2,A3,JGRAPH_2:44;
set g=AffineMap(1/A,-B/A,1/C,-D/C);
A5: g=h" by A1,A2,A3,Th49;
A6: for p1,p2 being Point of TOP-REAL 2 st p1`10 & C >0 & h=AffineMap(A,B,C,D) holds h is being_homeomorphism
& for p1,p2 being Point of TOP-REAL 2 st p1`20 and
A2: C >0 and
A3: h=AffineMap(A,B,C,D);
A4: h is one-to-one by A1,A2,A3,JGRAPH_2:44;
set g=AffineMap(1/A,-B/A,1/C,-D/C);
A5: g=h" by A1,A2,A3,Th49;
A6: for p1,p2 being Point of TOP-REAL 2 st p1`20 by A1,XREAL_1:50;
then
A11: A >0 by XREAL_1:139;
(-1-B)/A =(-1+(b+a)/(b-a))/(2/(b-a))
.=((-1)*(b-a)+(b+a))/(b-a)/(2/(b-a)) by A10,XCMPLX_1:113
.= (a+a)/(b-a)/2*(b-a) by XCMPLX_1:82
.= ((b-a)*((a+a)/(b-a)))/2
.=(a+a)/2 by A10,XCMPLX_1:87
.= a;
then A*((-1-B)/A) <= A*((f.t0)`1) by A11,A8,XREAL_1:64;
then -1-B <= A*((f.t0)`1) by A11,XCMPLX_1:87;
then -1-B+B <= A*((f.t0)`1)+B by XREAL_1:6;
then
A12: -1 <=p0`1 by A6,A9,A7,EUCLID:52;
A13: d-c >0 by A2,XREAL_1:50;
then
A14: C >0 by XREAL_1:139;
(1-B)/A =(1+(b+a)/(b-a))/(2/(b-a))
.=((1)*(b-a)+(b+a))/(b-a)/(2/(b-a)) by A10,XCMPLX_1:113
.= (b+b)/(b-a)/2*(b-a) by XCMPLX_1:82
.= ((b-a)*((b+b)/(b-a)))/2
.=(b+b)/2 by A10,XCMPLX_1:87
.= b;
then A*((1-B)/A) >= A*((f.t0)`1) by A11,A8,XREAL_1:64;
then 1-B >= A*((f.t0)`1) by A11,XCMPLX_1:87;
then 1-B+B >= A*((f.t0)`1)+B by XREAL_1:6;
then
A15: p0`1<=1 by A6,A9,A7,EUCLID:52;
(1-D)/C =(1+(d+c)/(d-c))/(2/(d-c))
.=((1)*(d-c)+(d+c))/(d-c)/(2/(d-c)) by A13,XCMPLX_1:113
.= (d+d)/(d-c)/2*(d-c) by XCMPLX_1:82
.= ((d-c)*((d+d)/(d-c)))/2
.=(d+d)/2 by A13,XCMPLX_1:87
.= d;
then C*((1-D)/C) >= C*((f.t0)`2) by A14,A8,XREAL_1:64;
then 1-D >= C*((f.t0)`2) by A14,XCMPLX_1:87;
then 1-D+D >= C*((f.t0)`2)+D by XREAL_1:6;
then
A16: p0`2<=1 by A6,A9,A7,EUCLID:52;
(-1-D)/C =(-1+(d+c)/(d-c))/(2/(d-c))
.=((-1)*(d-c)+(d+c))/(d-c)/(2/(d-c)) by A13,XCMPLX_1:113
.= (c+c)/(d-c)/2*(d-c) by XCMPLX_1:82
.= ((d-c)*((c+c)/(d-c)))/2
.=(c+c)/2 by A13,XCMPLX_1:87
.= c;
then C*((-1-D)/C) <= C*((f.t0)`2) by A14,A8,XREAL_1:64;
then -1-D <= C*((f.t0)`2) by A14,XCMPLX_1:87;
then -1-D+D <= C*((f.t0)`2)+D by XREAL_1:6;
then -1 <=p0`2 by A6,A9,A7,EUCLID:52;
then x in {p2 where p2 is Point of TOP-REAL 2: -1 <=p2`1 & p2`1<= 1 & -1 <=
p2`2 & p2`2<= 1} by A16,A12,A15;
hence thesis by JGRAPH_6:def 2;
end;
theorem Th53:
for a,b,c,d being Real, h being Function of TOP-REAL 2,
TOP-REAL 2,f being Function of I[01],TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A5: C >0 by XREAL_1:139;
b-a>0 by A1,XREAL_1:50;
then A >0 by XREAL_1:139;
then h is being_homeomorphism by A3,A5,Th51;
then h is one-to-one by TOPS_2:def 5;
hence thesis by A3,A4,FUNCT_1:24;
end;
theorem Th54:
for a,b,c,d being Real, h being Function of TOP-REAL 2,
TOP-REAL 2,f being Function of I[01],TOP-REAL 2, O being Point of I[01] st a****0 by A1,XREAL_1:50;
dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A5: ((h*f).O)=(h.(f.O)) by FUNCT_1:13;
A6: (h.(f.O))= |[A*((f.O)`1)+B,C*((f.O)`2)+D]| by A2,JGRAPH_2:def 2;
A*((f.O)`1)+B = (2*a)/(b-a)+ -(b+a)/(b-a) by A3,XCMPLX_1:74
.= (2*a)/(b-a)+ (-(b+a))/(b-a) by XCMPLX_1:187
.=(2*a+-(b+a))/(b-a) by XCMPLX_1:62
.=(-(b-a))/(b-a)
.= -1 by A4,XCMPLX_1:197;
hence thesis by A5,A6,EUCLID:52;
end;
theorem Th55:
for a,b,c,d being Real, h being Function of TOP-REAL 2,
TOP-REAL 2,f being Function of I[01],TOP-REAL 2, I being Point of I[01] st c 0 by A1,XREAL_1:50;
dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A5: ((h*f).I)=(h.(f.I)) by FUNCT_1:13;
A6: (h.(f.I))= |[A*((f.I)`1)+B,C*((f.I)`2)+D]| by A2,JGRAPH_2:def 2;
C*((f.I)`2)+D = (2*d)/(d-c)+ -(d+c)/(d-c) by A3,XCMPLX_1:74
.= (2*d)/(d-c)+ (-(d+c))/(d-c) by XCMPLX_1:187
.=(2*d+-(d+c))/(d-c) by XCMPLX_1:62
.= 1 by A4,XCMPLX_1:60;
hence thesis by A5,A6,EUCLID:52;
end;
theorem Th56:
for a,b,c,d being Real, h being Function of TOP-REAL 2,
TOP-REAL 2,f being Function of I[01],TOP-REAL 2, I being Point of I[01] st a****0 by A1,XREAL_1:50;
dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A5: ((h*f).I)=(h.(f.I)) by FUNCT_1:13;
A6: (h.(f.I))= |[A*((f.I)`1)+B,C*((f.I)`2)+D]| by A2,JGRAPH_2:def 2;
A*((f.I)`1)+B = (2*b)/(b-a)+ -(b+a)/(b-a) by A3,XCMPLX_1:74
.= (2*b)/(b-a)+ (-(b+a))/(b-a) by XCMPLX_1:187
.=(b+b+-(b+a))/(b-a) by XCMPLX_1:62
.= 1 by A4,XCMPLX_1:60;
hence thesis by A5,A6,EUCLID:52;
end;
theorem Th57:
for a,b,c,d being Real, h being Function of TOP-REAL 2,
TOP-REAL 2,f being Function of I[01],TOP-REAL 2, I being Point of I[01] st c 0 by A1,XREAL_1:50;
dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A5: ((h*f).I)=(h.(f.I)) by FUNCT_1:13;
A6: (h.(f.I))= |[A*((f.I)`1)+B,C*((f.I)`2)+D]| by A2,JGRAPH_2:def 2;
C*((f.I)`2)+D = (2*c)/(d-c)+ -(d+c)/(d-c) by A3,XCMPLX_1:74
.= (2*c)/(d-c)+ (-(d+c))/(d-c) by XCMPLX_1:187
.=(c+c+-(d+c))/(d-c) by XCMPLX_1:62
.=(-(d-c))/(d-c)
.= -1 by A4,XCMPLX_1:197;
hence thesis by A5,A6,EUCLID:52;
end;
theorem Th58:
for a,b,c,d being Real, h being Function of TOP-REAL 2,
TOP-REAL 2,f being Function of I[01],TOP-REAL 2, O,I being Point of I[01] st c
0 by A1,XREAL_1:50;
then
A8: C >0 by XREAL_1:139;
(-1-D)/C =(-1+(d+c)/(d-c))/(2/(d-c))
.=((-1)*(d-c)+(d+c))/(d-c)/(2/(d-c)) by A7,XCMPLX_1:113
.= (c+c)/(d-c)/2*(d-c) by XCMPLX_1:82
.= ((d-c)*((c+c)/(d-c)))/2
.=(c+c)/2 by A7,XCMPLX_1:87
.= c;
then C*((-1-D)/C) <= C*((f.O)`2) by A3,A8,XREAL_1:64;
then -1-D <= C*((f.O)`2) by A8,XCMPLX_1:87;
then
A9: -1-D+D <= C*((f.O)`2)+D by XREAL_1:6;
A10: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A11: ((h*f).O)=(h.(f.O)) by FUNCT_1:13;
A12: ((h*f).I)=(h.(f.I)) by A10,FUNCT_1:13;
(1-D)/C =(1+(d+c)/(d-c))/(2/(d-c))
.=((1)*(d-c)+(d+c))/(d-c)/(2/(d-c)) by A7,XCMPLX_1:113
.= (d+d)/(d-c)/2*(d-c) by XCMPLX_1:82
.= ((d-c)*((d+d)/(d-c)))/2
.=(d+d)/2 by A7,XCMPLX_1:87
.= d;
then C*((1- D)/C) >= C*((f.I)`2) by A5,A8,XREAL_1:64;
then 1-D >= C*((f.I)`2) by A8,XCMPLX_1:87;
then
A13: 1-D+D >= C*((f.I)`2)+D by XREAL_1:6;
A14: (h.(f.I))= |[A*((f.I)`1)+B,C*((f.I)`2)+D]| by A2,JGRAPH_2:def 2;
C*((f.O)`2)< C*((f.I)`2) by A4,A8,XREAL_1:68;
then C*((f.O)`2)+D < C*((f.I)`2)+D by XREAL_1:8;
then C*((f.O)`2)+D < ((h*f).I)`2 by A12,A14,EUCLID:52;
hence thesis by A11,A12,A6,A14,A9,A13,EUCLID:52;
end;
theorem Th59:
for a,b,c,d being Real, h being Function of TOP-REAL 2,
TOP-REAL 2,f being Function of I[01],TOP-REAL 2, O,I being Point of I[01] st a<
b & c 0 by A2,XREAL_1:50;
then
A10: C >0 by XREAL_1:139;
then C*d >= C*((f.O)`2) by A5,XREAL_1:64;
then
A11: C*d+D >= C*((f.O)`2)+D by XREAL_1:6;
(-1-D)/C =(-1+(d+c)/(d-c))/(2/(d-c))
.=((-1)*(d-c)+(d+c))/(d-c)/(2/(d-c)) by A9,XCMPLX_1:113
.= (c+c)/(d-c)/2*(d-c) by XCMPLX_1:82
.= ((d-c)*((c+c)/(d-c)))/2
.=(c+c)/2 by A9,XCMPLX_1:87
.= c;
then C*((-1-D)/C) <= C*((f.O)`2) by A4,A10,XREAL_1:64;
then -1-D <= C*((f.O)`2) by A10,XCMPLX_1:87;
then
A12: -1-D+D <= C*((f.O)`2)+D by XREAL_1:6;
A13: C*(d)+D = (2*d)/(d-c)+ -(d+c)/(d-c) by XCMPLX_1:74
.= (2*d)/(d-c)+ (-(d+c))/(d-c) by XCMPLX_1:187
.=(2*d+-(d+c))/(d-c) by XCMPLX_1:62
.= 1 by A9,XCMPLX_1:60;
A14: (h.(f.I))= |[A*((f.I)`1)+B,C*((f.I)`2)+D]| by A3,JGRAPH_2:def 2;
A15: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A16: ((h*f).I)=(h.(f.I)) by FUNCT_1:13;
A17: b-a>0 by A1,XREAL_1:50;
then
A18: A >0 by XREAL_1:139;
then A*b >= A*((f.I)`1) by A7,XREAL_1:64;
then
A19: A*b+B >= A*((f.I)`1)+B by XREAL_1:6;
A*a<=A*((f.I)`1) by A6,A18,XREAL_1:64;
then
A20: A*a+B <= A*((f.I)`1)+B by XREAL_1:7;
A21: A*b+B = (2*b)/(b-a)+ -(b+a)/(b-a) by XCMPLX_1:74
.= (2*b)/(b-a)+ (-(b+a))/(b-a) by XCMPLX_1:187
.=(2*b+-(b+a))/(b-a) by XCMPLX_1:62
.= 1 by A17,XCMPLX_1:60;
A22: A*a+B = (2*a)/(b-a)+ -(b+a)/(b-a) by XCMPLX_1:74
.= (2*a)/(b-a)+ (-(b+a))/(b-a) by XCMPLX_1:187
.=(2*a+-(b+a))/(b-a) by XCMPLX_1:62
.=(-(b-a))/(b-a)
.= -1 by A17,XCMPLX_1:197;
((h*f).O)=(h.(f.O)) by A15,FUNCT_1:13;
hence thesis by A16,A8,A14,A22,A21,A13,A12,A11,A19,A20,EUCLID:52;
end;
theorem Th60:
for a,b,c,d being Real, h being Function of TOP-REAL 2,
TOP-REAL 2,f being Function of I[01],TOP-REAL 2, O,I being Point of I[01] st c
0 by A1,XREAL_1:50;
then
A9: C >0 by XREAL_1:139;
then C*d >= C*((f.O)`2) by A4,XREAL_1:64;
then
A10: C*d+D >= C*((f.O)`2)+D by XREAL_1:6;
(-1-D)/C =(-1+(d+c)/(d-c))/(2/(d-c))
.=((-1)*(d-c)+(d+c))/(d-c)/(2/(d-c)) by A8,XCMPLX_1:113
.= (d-c)*((c+c)/(d-c)/2) by XCMPLX_1:82
.= ((d-c)*((c+c)/(d-c)))/2
.=(c+c)/2 by A8,XCMPLX_1:87
.= c;
then C*((-1-D)/C) <= C*((f.O)`2) by A3,A9,XREAL_1:64;
then -1-D <= C*((f.O)`2) by A9,XCMPLX_1:87;
then
A11: -1-D+D <= C*((f.O)`2)+D by XREAL_1:6;
C*c <=C*((f.I)`2) by A5,A9,XREAL_1:64;
then
A12: C*c+D <= C*((f.I)`2)+D by XREAL_1:7;
A13: (h.(f.I))= |[A*((f.I)`1)+B,C*((f.I)`2)+D]| by A2,JGRAPH_2:def 2;
A14: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A15: ((h*f).I)=(h.(f.I)) by FUNCT_1:13;
C*d >= C*((f.I)`2) by A6,A9,XREAL_1:64;
then
A16: C*d+D >= C*((f.I)`2)+D by XREAL_1:6;
A17: C*d+D = (2*d)/(d-c)+ -(d+c)/(d-c) by XCMPLX_1:74
.= (2*d)/(d-c)+ (-(d+c))/(d-c) by XCMPLX_1:187
.=(d+d+-(d+c))/(d-c) by XCMPLX_1:62
.= 1 by A8,XCMPLX_1:60;
A18: C*c+D = (2*c)/(d-c)+ -(d+c)/(d-c) by XCMPLX_1:74
.= (2*c)/(d-c)+ (-(d+c))/(d-c) by XCMPLX_1:187
.=(c+c+-(d+c))/(d-c) by XCMPLX_1:62
.=(-(d-c))/(d-c)
.= -1 by A8,XCMPLX_1:197;
((h*f).O)=(h.(f.O)) by A14,FUNCT_1:13;
hence thesis by A15,A7,A13,A18,A17,A11,A10,A16,A12,EUCLID:52;
end;
theorem Th61:
for a,b,c,d being Real, h being Function of TOP-REAL 2,
TOP-REAL 2,f being Function of I[01],TOP-REAL 2, O,I being Point of I[01] st a<
b & c 0 by A2,XREAL_1:50;
then
A10: C >0 by XREAL_1:139;
then C*d >= C*((f.O)`2) by A5,XREAL_1:64;
then
A11: C*d+D >= C*((f.O)`2)+D by XREAL_1:6;
(-1-D)/C =(-1+(d+c)/(d-c))/(2/(d-c))
.=((-1)*(d-c)+(d+c))/(d-c)/(2/(d-c)) by A9,XCMPLX_1:113
.= (d-c)*((c+c)/(d-c)/2) by XCMPLX_1:82
.= ((d-c)*((c+c)/(d-c)))/2
.=(c+c)/2 by A9,XCMPLX_1:87
.= c;
then C*((-1-D)/C) <= C*((f.O)`2) by A4,A10,XREAL_1:64;
then -1-D <= C*((f.O)`2) by A10,XCMPLX_1:87;
then
A12: -1-D+D <= C*((f.O)`2)+D by XREAL_1:6;
A13: C*d+D = (2*d)/(d-c)+ -(d+c)/(d-c) by XCMPLX_1:74
.= (2*d)/(d-c)+ (-(d+c))/(d-c) by XCMPLX_1:187
.=(d+d+-(d+c))/(d-c) by XCMPLX_1:62
.= 1 by A9,XCMPLX_1:60;
A14: (h.(f.I))= |[A*((f.I)`1)+B,C*((f.I)`2)+D]| by A3,JGRAPH_2:def 2;
A15: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A16: ((h*f).I)=(h.(f.I)) by FUNCT_1:13;
A17: b-a>0 by A1,XREAL_1:50;
then
A18: A >0 by XREAL_1:139;
then A*b >= A*((f.I)`1) by A7,XREAL_1:64;
then
A19: A*b+B >= A*((f.I)`1)+B by XREAL_1:6;
A*a0 by A1,XREAL_1:50;
then
A8: A >0 by XREAL_1:139;
(1-B)/A =(1+(b+a)/(b-a))/(2/(b-a))
.=((1)*(b-a)+(b+a))/(b-a)/(2/(b-a)) by A7,XCMPLX_1:113
.= (b-a)*((b+b)/(b-a)/2) by XCMPLX_1:82
.= ((b-a)*((b+b)/(b-a)))/2
.=(b+b)/2 by A7,XCMPLX_1:87
.= b;
then A*((1- B)/A) >= A*((f.I)`1) by A5,A8,XREAL_1:64;
then 1-B >= A*((f.I)`1) by A8,XCMPLX_1:87;
then
A9: 1-B+B >= A*((f.I)`1)+B by XREAL_1:6;
A10: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A11: ((h*f).O)=(h.(f.O)) by FUNCT_1:13;
A12: ((h*f).I)=(h.(f.I)) by A10,FUNCT_1:13;
(-1-B)/A =(-1+(b+a)/(b-a))/(2/(b-a))
.=((-1)*(b-a)+(b+a))/(b-a)/(2/(b-a)) by A7,XCMPLX_1:113
.= (b-a)*((a+a)/(b-a)/2) by XCMPLX_1:82
.= ((b-a)*((a+a)/(b-a)))/2
.=(a+a)/2 by A7,XCMPLX_1:87
.= a;
then A*((-1-B)/A) <= A*((f.O)`1) by A3,A8,XREAL_1:64;
then -1-B <= A*((f.O)`1) by A8,XCMPLX_1:87;
then
A13: -1-B+B <= A*((f.O)`1)+B by XREAL_1:6;
A14: (h.(f.I))= |[A*((f.I)`1)+B,C*((f.I)`2)+D]| by A2,JGRAPH_2:def 2;
A*((f.O)`1)< A*((f.I)`1) by A4,A8,XREAL_1:68;
then A*((f.O)`1)+B < A*((f.I)`1)+B by XREAL_1:8;
then A*((f.O)`1)+B < ((h*f).I)`1 by A12,A14,EUCLID:52;
hence thesis by A11,A12,A6,A14,A13,A9,EUCLID:52;
end;
theorem Th63:
for a,b,c,d being Real, h being Function of TOP-REAL 2,
TOP-REAL 2,f being Function of I[01],TOP-REAL 2, O,I being Point of I[01] st a<
b & c 0 by A1,XREAL_1:50;
then
A10: A >0 by XREAL_1:139;
(-1-B)/A =(-1+(b+a)/(b-a))/(2/(b-a))
.=((-1)*(b-a)+(b+a))/(b-a)/(2/(b-a)) by A9,XCMPLX_1:113
.= (b-a)*((a+a)/(b-a)/2) by XCMPLX_1:82
.= ((b-a)*((a+a)/(b-a)))/2
.=(a+a)/2 by A9,XCMPLX_1:87
.= a;
then A*((-1-B)/A) <= A*((f.O)`1) by A4,A10,XREAL_1:64;
then -1-B <= A*((f.O)`1) by A10,XCMPLX_1:87;
then
A11: -1-B+B <= A*((f.O)`1)+B by XREAL_1:6;
A12: d-c >0 by A2,XREAL_1:50;
then
A13: C >0 by XREAL_1:139;
(-1-D)/C =(-1+(d+c)/(d-c))/(2/(d-c))
.=((-1)*(d-c)+(d+c))/(d-c)/(2/(d-c)) by A12,XCMPLX_1:113
.= (d-c)*((c+c)/(d-c)/2) by XCMPLX_1:82
.= ((d-c)*((c+c)/(d-c)))/2
.=(c+c)/2 by A12,XCMPLX_1:87
.= c;
then C*((-1-D)/C) <= C*((f.I)`2) by A6,A13,XREAL_1:64;
then -1-D <= C*((f.I)`2) by A13,XCMPLX_1:87;
then
A14: -1-D+D <= C*((f.I)`2)+D by XREAL_1:6;
A15: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A16: ((h*f).I)=(h.(f.I)) by FUNCT_1:13;
(1-B)/A =(1+(b+a)/(b-a))/(2/(b-a))
.=((1)*(b-a)+(b+a))/(b-a)/(2/(b-a)) by A9,XCMPLX_1:113
.= (b-a)*((b+b)/(b-a)/2) by XCMPLX_1:82
.= ((b-a)*((b+b)/(b-a)))/2
.=(b+b)/2 by A9,XCMPLX_1:87
.= b;
then A*((1- B)/A) >= A*((f.O)`1) by A5,A10,XREAL_1:64;
then 1-B >= A*((f.O)`1) by A10,XCMPLX_1:87;
then
A17: 1-B+B >= A*((f.O)`1)+B by XREAL_1:6;
A18: (h.(f.I))= |[A*((f.I)`1)+B,C*((f.I)`2)+D]| by A3,JGRAPH_2:def 2;
(1-D)/C =(1+(d+c)/(d-c))/(2/(d-c))
.=((1)*(d-c)+(d+c))/(d-c)/(2/(d-c)) by A12,XCMPLX_1:113
.= (d-c)*((d+d)/(d-c)/2) by XCMPLX_1:82
.= ((d-c)*((d+d)/(d-c)))/2
.=(d+d)/2 by A12,XCMPLX_1:87
.= d;
then C*((1- D)/C) >= C*((f.I)`2) by A7,A13,XREAL_1:64;
then 1-D >= C*((f.I)`2) by A13,XCMPLX_1:87;
then
A19: 1-D+D >= C*((f.I)`2)+D by XREAL_1:6;
((h*f).O)=(h.(f.O)) by A15,FUNCT_1:13;
hence thesis by A16,A8,A18,A11,A17,A19,A14,EUCLID:52;
end;
theorem Th64:
for a,b,c,d being Real, h being Function of TOP-REAL 2,
TOP-REAL 2,f being Function of I[01],TOP-REAL 2, O,I being Point of I[01] st a<
b & h=AffineMap(2/(b-a),-(b+a)/(b-a),2/(d-c),-(d+c)/(d-c)) & a <=(f.O)`1 & (f.O
)`1<=b & a <(f.I)`1 & (f.I)`1<=b holds -1 <=((h*f).O)`1 & ((h*f).O)`1<=1 & -1<(
(h*f).I)`1 & ((h*f).I)`1<=1
proof
let a,b,c,d be Real, h be Function of TOP-REAL 2,TOP-REAL 2,f be
Function of I[01],TOP-REAL 2, O,I be Point of I[01];
set A=2/(b-a), B=-(b+a)/(b-a), C = 2/(d-c), D=-(d+c)/(d-c);
assume that
A1: a****0 by A1,XREAL_1:50;
then
A8: A >0 by XREAL_1:139;
A9: (1-B)/A =(1+(b+a)/(b-a))/(2/(b-a))
.=((1)*(b-a)+(b+a))/(b-a)/(2/(b-a)) by A7,XCMPLX_1:113
.= (b-a)*((b+b)/(b-a)/2) by XCMPLX_1:82
.= ((b-a)*((b+b)/(b-a)))/2
.=(b+b)/2 by A7,XCMPLX_1:87
.= b;
then A*((1- B)/A) >= A*((f.O)`1) by A4,A8,XREAL_1:64;
then 1-B >= A*((f.O)`1) by A8,XCMPLX_1:87;
then
A10: 1-B+B >= A*((f.O)`1)+B by XREAL_1:6;
A*((1- B)/A) >= A*((f.I)`1) by A6,A8,A9,XREAL_1:64;
then 1-B >= A*((f.I)`1) by A8,XCMPLX_1:87;
then
A11: 1-B+B >= A*((f.I)`1)+B by XREAL_1:6;
A12: (h.(f.I))= |[A*((f.I)`1)+B,C*((f.I)`2)+D]| by A2,JGRAPH_2:def 2;
A13: (h.(f.O))= |[A*((f.O)`1)+B,C*((f.O)`2)+D]| by A2,JGRAPH_2:def 2;
A14: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A15: ((h*f).I)=(h.(f.I)) by FUNCT_1:13;
A16: (-1-B)/A =(-1+(b+a)/(b-a))/(2/(b-a))
.=((-1)*(b-a)+(b+a))/(b-a)/(2/(b-a)) by A7,XCMPLX_1:113
.= (b-a)*((a+a)/(b-a)/2) by XCMPLX_1:82
.= ((b-a)*((a+a)/(b-a)))/2
.=(a+a)/2 by A7,XCMPLX_1:87
.= a;
then A*((-1-B)/A) <= A*((f.O)`1) by A3,A8,XREAL_1:64;
then -1-B <= A*((f.O)`1) by A8,XCMPLX_1:87;
then
A17: -1-B+B <= A*((f.O)`1)+B by XREAL_1:6;
A*((-1-B)/A) < A*((f.I)`1) by A5,A8,A16,XREAL_1:68;
then -1-B < A*((f.I)`1) by A8,XCMPLX_1:87;
then
A18: -1-B+B < A*((f.I)`1)+B by XREAL_1:8;
((h*f).O)=(h.(f.O)) by A14,FUNCT_1:13;
hence thesis by A15,A13,A12,A17,A10,A11,A18,EUCLID:52;
end;
theorem Th65:
for a,b,c,d being Real, h being Function of TOP-REAL 2,
TOP-REAL 2,f being Function of I[01],TOP-REAL 2, O,I being Point of I[01] st c
=(f.O)`2 & (f.
O)`2>(f.I)`2 & (f.I)`2>= c holds 1 >=((h*f).O)`2 & ((h*f).O)`2>((h*f).I)`2 & ((
h*f).I)`2>= -1
proof
let a,b,c,d be Real, h be Function of TOP-REAL 2,TOP-REAL 2,f be
Function of I[01],TOP-REAL 2, O,I be Point of I[01];
set A=2/(b-a), B=-(b+a)/(b-a), C = 2/(d-c), D=-(d+c)/(d-c);
assume that
A1: c =(f.O)`2 and
A4: (f.O)`2>(f.I)`2 and
A5: (f.I)`2>= c;
A6: (h.(f.O))= |[A*((f.O)`1)+B,C*((f.O)`2)+D]| by A2,JGRAPH_2:def 2;
A7: d-c >0 by A1,XREAL_1:50;
then
A8: C >0 by XREAL_1:139;
(-1-D)/C =(-1+(d+c)/(d-c))/(2/(d-c))
.=((-1)*(d-c)+(d+c))/(d-c)/(2/(d-c)) by A7,XCMPLX_1:113
.= (d-c)*((c+c)/(d-c)/2) by XCMPLX_1:82
.= ((d-c)*((c+c)/(d-c)))/2
.=(c+c)/2 by A7,XCMPLX_1:87
.= c;
then C*((-1- D)/C) <= C*((f.I)`2) by A5,A8,XREAL_1:64;
then -1-D <= C*((f.I)`2) by A8,XCMPLX_1:87;
then
A9: -1-D+D <= C*((f.I)`2)+D by XREAL_1:6;
A10: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A11: ((h*f).O)=(h.(f.O)) by FUNCT_1:13;
A12: ((h*f).I)=(h.(f.I)) by A10,FUNCT_1:13;
(1-D)/C =(1+(d+c)/(d-c))/(2/(d-c))
.=((1)*(d-c)+(d+c))/(d-c)/(2/(d-c)) by A7,XCMPLX_1:113
.= (d-c)*((d+d)/(d-c)/2) by XCMPLX_1:82
.= ((d-c)*((d+d)/(d-c)))/2
.=(d+d)/2 by A7,XCMPLX_1:87
.= d;
then C*((1-D)/C) >= C*((f.O)`2) by A3,A8,XREAL_1:64;
then 1-D >= C*((f.O)`2) by A8,XCMPLX_1:87;
then
A13: 1-D+D >= C*((f.O)`2)+D by XREAL_1:6;
A14: (h.(f.I))= |[A*((f.I)`1)+B,C*((f.I)`2)+D]| by A2,JGRAPH_2:def 2;
C*((f.O)`2)> C*((f.I)`2) by A4,A8,XREAL_1:68;
then C*((f.O)`2)+D > C*((f.I)`2)+D by XREAL_1:8;
then C*((f.O)`2)+D > ((h*f).I)`2 by A12,A14,EUCLID:52;
hence thesis by A11,A12,A6,A14,A13,A9,EUCLID:52;
end;
theorem Th66:
for a,b,c,d being Real, h being Function of TOP-REAL 2,
TOP-REAL 2,f being Function of I[01],TOP-REAL 2, O,I being Point of I[01] st a<
b & c 0 by A1,XREAL_1:50;
then
A10: A >0 by XREAL_1:139;
(-1-B)/A =(-1+(b+a)/(b-a))/(2/(b-a))
.=((-1)*(b-a)+(b+a))/(b-a)/(2/(b-a)) by A9,XCMPLX_1:113
.= (b-a)*((a+a)/(b-a)/2) by XCMPLX_1:82
.= ((b-a)*((a+a)/(b-a)))/2
.=(a+a)/2 by A9,XCMPLX_1:87
.= a;
then A*((-1-B)/A) < A*((f.I)`1) by A6,A10,XREAL_1:68;
then -1-B < A*((f.I)`1) by A10,XCMPLX_1:87;
then
A11: -1-B+B < A*((f.I)`1)+B by XREAL_1:8;
A12: d-c >0 by A2,XREAL_1:50;
then
A13: C >0 by XREAL_1:139;
(-1-D)/C =(-1+(d+c)/(d-c))/(2/(d-c))
.=((-1)*(d-c)+(d+c))/(d-c)/(2/(d-c)) by A12,XCMPLX_1:113
.= (d-c)*((c+c)/(d-c)/2) by XCMPLX_1:82
.= ((d-c)*((c+c)/(d-c)))/2
.=(c+c)/2 by A12,XCMPLX_1:87
.= c;
then C*((-1-D)/C) <= C*((f.O)`2) by A4,A13,XREAL_1:64;
then -1-D <= C*((f.O)`2) by A13,XCMPLX_1:87;
then
A14: -1-D+D <= C*((f.O)`2)+D by XREAL_1:6;
A15: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A16: ((h*f).I)=(h.(f.I)) by FUNCT_1:13;
(1-B)/A =(1+(b+a)/(b-a))/(2/(b-a))
.=((1)*(b-a)+(b+a))/(b-a)/(2/(b-a)) by A9,XCMPLX_1:113
.= (b-a)*((b+b)/(b-a)/2) by XCMPLX_1:82
.= ((b-a)*((b+b)/(b-a)))/2
.=(b+b)/2 by A9,XCMPLX_1:87
.= b;
then A*((1- B)/A) >= A*((f.I)`1) by A7,A10,XREAL_1:64;
then 1-B >= A*((f.I)`1) by A10,XCMPLX_1:87;
then
A17: 1-B+B >= A*((f.I)`1)+B by XREAL_1:6;
A18: (h.(f.I))= |[A*((f.I)`1)+B,C*((f.I)`2)+D]| by A3,JGRAPH_2:def 2;
(1-D)/C =(1+(d+c)/(d-c))/(2/(d-c))
.=((1)*(d-c)+(d+c))/(d-c)/(2/(d-c)) by A12,XCMPLX_1:113
.= (d-c)*((d+d)/(d-c)/2) by XCMPLX_1:82
.= ((d-c)*((d+d)/(d-c)))/2
.=(d+d)/2 by A12,XCMPLX_1:87
.= d;
then C*((1- D)/C) >= C*((f.O)`2) by A5,A13,XREAL_1:64;
then 1-D >= C*((f.O)`2) by A13,XCMPLX_1:87;
then
A19: 1-D+D >= C*((f.O)`2)+D by XREAL_1:6;
((h*f).O)=(h.(f.O)) by A15,FUNCT_1:13;
hence thesis by A16,A8,A18,A14,A19,A17,A11,EUCLID:52;
end;
theorem Th67:
for a,b,c,d being Real, h being Function of TOP-REAL 2,
TOP-REAL 2,f being Function of I[01],TOP-REAL 2, O,I being Point of I[01] st a<
b & h=AffineMap(2/(b-a),-(b+a)/(b-a),2/(d-c),-(d+c)/(d-c)) & a <(f.I)`1 & (f.I)
`1 <(f.O)`1 & (f.O)`1<=b holds -1<((h*f).I)`1 & ((h*f).I)`1<((h*f).O)`1 & ((h*f
).O)`1<=1
proof
let a,b,c,d be Real, h be Function of TOP-REAL 2,TOP-REAL 2,f be
Function of I[01],TOP-REAL 2, O,I be Point of I[01];
set A=2/(b-a), B=-(b+a)/(b-a), C = 2/(d-c), D=-(d+c)/(d-c);
assume that
A1: a****0 by A1,XREAL_1:50;
then
A8: A >0 by XREAL_1:139;
(1-B)/A =(1+(b+a)/(b-a))/(2/(b-a))
.=((1)*(b-a)+(b+a))/(b-a)/(2/(b-a)) by A7,XCMPLX_1:113
.= (b-a)*((b+b)/(b-a)/2) by XCMPLX_1:82
.= ((b-a)*((b+b)/(b-a)))/2
.=(b+b)/2 by A7,XCMPLX_1:87
.= b;
then A*((1- B)/A) >= A*((f.O)`1) by A5,A8,XREAL_1:64;
then 1-B >= A*((f.O)`1) by A8,XCMPLX_1:87;
then
A9: 1-B+B >= A*((f.O)`1)+B by XREAL_1:6;
A10: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A11: ((h*f).O)=(h.(f.O)) by FUNCT_1:13;
A12: ((h*f).I)=(h.(f.I)) by A10,FUNCT_1:13;
(-1-B)/A =(-1+(b+a)/(b-a))/(2/(b-a))
.=((-1)*(b-a)+(b+a))/(b-a)/(2/(b-a)) by A7,XCMPLX_1:113
.= (b-a)*((a+a)/(b-a)/2) by XCMPLX_1:82
.= ((b-a)*((a+a)/(b-a)))/2
.=(a+a)/2 by A7,XCMPLX_1:87
.= a;
then A*((-1-B)/A) < A*((f.I)`1) by A3,A8,XREAL_1:68;
then -1-B < A*((f.I)`1) by A8,XCMPLX_1:87;
then
A13: -1-B+B < A*((f.I)`1)+B by XREAL_1:8;
A14: (h.(f.I))= |[A*((f.I)`1)+B,C*((f.I)`2)+D]| by A2,JGRAPH_2:def 2;
A*((f.O)`1)> A*((f.I)`1) by A4,A8,XREAL_1:68;
then A*((f.O)`1)+B > A*((f.I)`1)+B by XREAL_1:8;
then A*((f.O)`1)+B > ((h*f).I)`1 by A12,A14,EUCLID:52;
hence thesis by A11,A12,A6,A14,A9,A13,EUCLID:52;
end;
theorem Th68:
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real
, f,g being Function of I[01],TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A30: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A31: f2 is continuous one-to-one by A1,A2,A16,Th53;
A32: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A18,Th52;
A33: ((f2).I)`1= -1 by A1,A5,A13,Th54;
A34: (f.I)`1=a by A5,A13;
A35: p3`20 by A1,XREAL_1:50;
then
A40: A >0 by XREAL_1:139;
then
A41: (h.p1)`2<(h.p2)`2 by A8,A30,Th51;
A42: (h.p3)`2<(h.p4)`2 by A10,A40,A30,Th51;
A43: (h.p2)`2<(h.p3)`2 by A9,A40,A30,Th51;
h.p1=f2.O by A12,A38,FUNCT_1:13;
then f2.O,g2.O,f2.I,g2.I are_in_this_order_on rectangle(-1,1,-1,1) by A41,A43
,A42,A28,A39,A29,A37,A33,A36,A26,A25,A23,Th14;
then rng f2 meets rng g2 by A31,A32,A20,A24,JGRAPH_6:79;
then
A44: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A45: z2 in dom g2 and
A46: x=g2.z2 by FUNCT_1:def 3;
A47: x=h.(g.z2) by A27,A45,A46,FUNCT_1:13;
h is being_homeomorphism by A40,A30,Th51;
then
A48: h is one-to-one by TOPS_2:def 5;
x in rng f2 by A44,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A38,A49,FUNCT_1:def 3;
A52: g.z2 in rng g by A27,A45,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A45,FUNCT_2:5;
then
A53: g.z2 in dom h by FUNCT_2:def 1;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A54: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A38,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A47,A54,A53,A48,FUNCT_1:def 4;
hence thesis by A51,A52,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A29: C >0 by XREAL_1:139;
b-a>0 by A1,XREAL_1:50;
then
A30: A >0 by XREAL_1:139;
then
A31: (h.p1)`2<(h.p2)`2 by A8,A29,Th51;
(f.O)`1=a by A3,A13;
then
A32: ((f2).I)`2<=1 by A2,A7,A10,A13,A14,A21,Th58;
h is being_homeomorphism by A30,A29,Th51;
then
A33: h is one-to-one by TOPS_2:def 5;
A34: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A35: ((f2).I)`1= -1 by A1,A5,A14,Th54;
A36: ((f2).O)`1= -1 by A1,A3,A13,Th54;
A37: f2 is continuous one-to-one by A1,A2,A17,Th53;
A38: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A39: (h.p2)`2<(h.p3)`2 by A9,A30,A29,Th51;
A40: ((g2).I)`1<=1 by A1,A2,A6,A11,A12,A16,Th59;
A41: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A42: h.p2=g2.O by A15,FUNCT_1:13;
h.p1=f2.O by A13,A27,FUNCT_1:13;
then rng f2 meets rng g2 by A31,A39,A42,A28,A37,A36,A35,A25,A32,A34,A26,A24
,A23,A22,A40,A38,Th15,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A41,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A41,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A27,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A27,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A33,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A29: C >0 by XREAL_1:139;
b-a>0 by A1,XREAL_1:50;
then
A30: A >0 by XREAL_1:139;
then
A31: (h.p1)`2<(h.p2)`2 by A8,A29,Th51;
(f.O)`1=a by A3,A13;
then
A32: ((f2).I)`2<=1 by A2,A7,A10,A13,A14,A21,Th58;
h is being_homeomorphism by A30,A29,Th51;
then
A33: h is one-to-one by TOPS_2:def 5;
A34: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A35: ((f2).I)`1= -1 by A1,A5,A14,Th54;
A36: ((f2).O)`1= -1 by A1,A3,A13,Th54;
A37: f2 is continuous one-to-one by A1,A2,A17,Th53;
A38: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A39: (h.p2)`2<(h.p3)`2 by A9,A30,A29,Th51;
A40: ((g2).I)`2<=1 by A2,A11,A12,A16,Th60;
A41: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A42: h.p2=g2.O by A15,FUNCT_1:13;
h.p1=f2.O by A13,A27,FUNCT_1:13;
then rng f2 meets rng g2 by A31,A39,A42,A28,A37,A36,A35,A25,A32,A34,A26,A24
,A23,A22,A40,A38,Th16,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A41,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A41,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A27,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A27,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A33,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A29: C >0 by XREAL_1:139;
b-a>0 by A1,XREAL_1:50;
then
A30: A >0 by XREAL_1:139;
then
A31: (h.p1)`2<(h.p2)`2 by A8,A29,Th51;
(f.O)`1=a by A3,A13;
then
A32: ((f2).I)`2<=1 by A2,A7,A10,A13,A14,A21,Th58;
h is being_homeomorphism by A30,A29,Th51;
then
A33: h is one-to-one by TOPS_2:def 5;
A34: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A35: ((f2).I)`1= -1 by A1,A5,A14,Th54;
A36: ((f2).O)`1= -1 by A1,A3,A13,Th54;
A37: f2 is continuous one-to-one by A1,A2,A17,Th53;
A38: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A39: (h.p2)`2<(h.p3)`2 by A9,A30,A29,Th51;
A40: ((g2).I)`1<=1 by A1,A2,A6,A11,A12,A16,Th61;
A41: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A42: h.p2=g2.O by A15,FUNCT_1:13;
h.p1=f2.O by A13,A27,FUNCT_1:13;
then rng f2 meets rng g2 by A31,A39,A42,A28,A37,A36,A35,A25,A32,A34,A26,A24
,A23,A22,A40,A38,Th17,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A41,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A41,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A27,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A27,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A33,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A25: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A26: f2 is continuous one-to-one by A1,A2,A17,Th53;
p3`1****0 by A1,XREAL_1:50;
then
A34: A >0 by XREAL_1:139;
then
A35: (h.p1)`2<(h.p2)`2 by A8,A25,Th51;
a{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A39,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A39,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A32,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A32,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A37,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A28: C >0 by XREAL_1:139;
reconsider g2= h*g as Function of I[01],TOP-REAL 2;
A29: -1<=((g2).I)`2 by A2,A12,A13,A17,Th60;
A30: ((g2).O)`1= -1 by A1,A4,A16,Th54;
A31: g2 is continuous one-to-one by A1,A2,A19,Th53;
c 0 by A1,XREAL_1:50;
then
A36: A >0 by XREAL_1:139;
then
A37: (h.p1)`2<(h.p2)`2 by A8,A28,Th51;
p1`2<=d by A8,A9,XXREAL_0:2;
then
A38: -1 <=((f2).O)`2 by A1,A2,A3,A7,A14,Th59;
h is being_homeomorphism by A36,A28,Th51;
then
A39: h is one-to-one by TOPS_2:def 5;
A40: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A21,Th52;
A41: ((g2).I)`1= 1 by A1,A6,A17,Th56;
A42: dom f=the carrier of I[01] by FUNCT_2:def 1;
then h.p1=f2.O by A14,FUNCT_1:13;
then rng f2 meets rng g2 by A37,A35,A24,A26,A25,A38,A22,A23,A27,A31,A30,A41
,A32,A29,A33,A40,Th19,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A34,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A34,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A42,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A42,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A39,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A28: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A29: -1<=((f2).I)`1 by A1,A2,A5,A10,A11,A15,Th59;
A30: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A31: ((f2).I)`2= 1 by A2,A5,A15,Th55;
p1`2<=d by A8,A9,XXREAL_0:2;
then
A32: -1 <=((f2).O)`2 by A1,A2,A3,A7,A14,Th59;
A33: ((f2).O)`1= -1 by A1,A3,A14,Th54;
A34: f2 is continuous one-to-one by A1,A2,A18,Th53;
A35: ((f2).I)`1<=1 by A1,A2,A5,A10,A11,A15,Th59;
set x = the Element of rng f2 /\ rng g2;
A36: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A37: h.p2=g2.O by A16,FUNCT_1:13;
A38: (g.I)`2= c by A6,A17;
c 0 by A1,XREAL_1:50;
then
A40: A >0 by XREAL_1:139;
then
A41: (h.p1)`2<(h.p2)`2 by A8,A28,Th51;
A42: dom f=the carrier of I[01] by FUNCT_2:def 1;
then h.p1=f2.O by A14,FUNCT_1:13;
then rng f2 meets rng g2 by A41,A37,A34,A33,A31,A32,A29,A35,A30,A24,A26,A25
,A39,A22,A23,A27,Th20,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A36,A44,A45,FUNCT_1:13;
h is being_homeomorphism by A40,A28,Th51;
then
A47: h is one-to-one by TOPS_2:def 5;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A48: z1 in dom f2 and
A49: x=f2.z1 by FUNCT_1:def 3;
A50: f.z1 in rng f by A42,A48,FUNCT_1:def 3;
A51: g.z2 in rng g by A36,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A52: g.z2 in dom h by FUNCT_2:def 1;
f.z1 in the carrier of TOP-REAL 2 by A48,FUNCT_2:5;
then
A53: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A42,A48,A49,FUNCT_1:13;
then f.z1=g.z2 by A46,A53,A52,A47,FUNCT_1:def 4;
hence thesis by A50,A51,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a**** c by A10,A11,XXREAL_0:2;
then
A26: ((f2).I)`2<=1 by A2,A12,A14,Th60;
d-c >0 by A2,XREAL_1:50;
then
A27: C >0 by XREAL_1:139;
A28: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A29: ((g2).I)`1= 1 by A1,A6,A16,Th56;
A30: ((g2).O)`1= -1 by A1,A4,A15,Th54;
A31: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A32: h.p2=g2.O by A15,FUNCT_1:13;
p1`2<=d by A8,A9,XXREAL_0:2;
then
A33: -1 <=((f2).O)`2 by A2,A7,A13,Th60;
A34: ((f2).O)`1= -1 by A1,A3,A13,Th54;
set x = the Element of rng f2 /\ rng g2;
A35: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A36: h.p3=f2.I by A14,FUNCT_1:13;
b-a>0 by A1,XREAL_1:50;
then
A37: A >0 by XREAL_1:139;
then
A38: (h.p1)`2<(h.p2)`2 by A8,A27,Th51;
d>=p4`2 by A11,A12,XXREAL_0:2;
then
A39: -1<=((g2).I)`2 by A2,A10,A16,Th60;
h is being_homeomorphism by A37,A27,Th51;
then
A40: h is one-to-one by TOPS_2:def 5;
A41: (h.p3)`2>(h.p4)`2 by A11,A37,A27,Th51;
A42: h.p4=g2.I by A16,A31,FUNCT_1:13;
h.p1=f2.O by A13,A35,FUNCT_1:13;
then f2.O,g2.O,f2.I,g2.I are_in_this_order_on rectangle(-1,1,-1,1) by A38,A41
,A32,A36,A42,A34,A24,A33,A26,A30,A29,A25,A39,Th21;
then rng f2 meets rng g2 by A22,A23,A21,A28,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A31,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A31,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A35,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A35,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A40,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A28: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A29: -1<=((f2).I)`2 by A2,A10,A11,A15,Th60;
A30: ((f2).O)`1= -1 by A1,A3,A14,Th54;
A31: f2 is continuous one-to-one by A1,A2,A18,Th53;
p1`2<=d by A8,A9,XXREAL_0:2;
then
A32: -1 <=((f2).O)`2 by A2,A7,A14,Th60;
A33: ((f2).I)`2<=1 by A2,A10,A11,A15,Th60;
set x = the Element of rng f2 /\ rng g2;
A34: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A35: h.p2=g2.O by A16,FUNCT_1:13;
A36: (g.I)`2= c by A6,A17;
c 0 by A1,XREAL_1:50;
then
A38: A >0 by XREAL_1:139;
then
A39: (h.p1)`2<(h.p2)`2 by A8,A28,Th51;
A40: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A41: ((f2).I)`1= 1 by A1,A5,A15,Th56;
A42: dom f=the carrier of I[01] by FUNCT_2:def 1;
then h.p1=f2.O by A14,FUNCT_1:13;
then rng f2 meets rng g2 by A39,A35,A31,A30,A41,A32,A29,A33,A40,A24,A26,A25
,A37,A22,A23,A27,Th22,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A34,A44,A45,FUNCT_1:13;
h is being_homeomorphism by A38,A28,Th51;
then
A47: h is one-to-one by TOPS_2:def 5;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A48: z1 in dom f2 and
A49: x=f2.z1 by FUNCT_1:def 3;
A50: f.z1 in rng f by A42,A48,FUNCT_1:def 3;
A51: g.z2 in rng g by A34,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A52: g.z2 in dom h by FUNCT_2:def 1;
f.z1 in the carrier of TOP-REAL 2 by A48,FUNCT_2:5;
then
A53: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A42,A48,A49,FUNCT_1:13;
then f.z1=g.z2 by A46,A53,A52,A47,FUNCT_1:def 4;
hence thesis by A50,A51,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****=p4`1 by A11,A12,XXREAL_0:2;
then
A23: -1<((g2).I)`1 by A1,A2,A6,A10,A16,Th61;
A24: (g.I)`2= c by A6,A16;
c 0 by A2,XREAL_1:50;
then
A26: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A27: f2 is continuous one-to-one by A1,A2,A17,Th53;
A28: p3`1>a by A10,A11,XXREAL_0:2;
then
A29: ((f2).I)`1<=1 by A1,A2,A5,A12,A14,Th61;
A30: (f.I)`2= c by A5,A14;
p1`2<=d by A8,A9,XXREAL_0:2;
then
A31: -1 <=((f2).O)`2 by A1,A2,A7,A12,A13,A14,A28,A30,Th61;
A32: ((f2).O)`1= -1 by A1,A3,A13,Th54;
set x = the Element of rng f2 /\ rng g2;
A33: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A34: h.p3=f2.I by A14,FUNCT_1:13;
A35: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A36: ((g2).I)`2= -1 by A2,A6,A16,Th57;
A37: ((g2).O)`1= -1 by A1,A4,A15,Th54;
A38: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A39: h.p2=g2.O by A15,FUNCT_1:13;
A40: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A41: ((f2).I)`2= -1 by A2,A5,A14,Th57;
b-a>0 by A1,XREAL_1:50;
then
A42: A >0 by XREAL_1:139;
then
A43: (h.p1)`2<(h.p2)`2 by A8,A26,Th51;
A44: (h.p3)`1>(h.p4)`1 by A11,A42,A26,Th50;
A45: h.p4=g2.I by A16,A38,FUNCT_1:13;
h.p1=f2.O by A13,A33,FUNCT_1:13;
then f2.O,g2.O,f2.I,g2.I are_in_this_order_on rectangle(-1,1,-1,1) by A43,A44
,A39,A34,A45,A32,A41,A31,A29,A37,A36,A25,A23,Th23;
then rng f2 meets rng g2 by A27,A40,A21,A35,JGRAPH_6:79;
then
A46: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A47: z2 in dom g2 and
A48: x=g2.z2 by FUNCT_1:def 3;
A49: x=h.(g.z2) by A38,A47,A48,FUNCT_1:13;
h is being_homeomorphism by A42,A26,Th51;
then
A50: h is one-to-one by TOPS_2:def 5;
x in rng f2 by A46,XBOOLE_0:def 4;
then consider z1 being object such that
A51: z1 in dom f2 and
A52: x=f2.z1 by FUNCT_1:def 3;
A53: f.z1 in rng f by A33,A51,FUNCT_1:def 3;
A54: g.z2 in rng g by A38,A47,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A47,FUNCT_2:5;
then
A55: g.z2 in dom h by FUNCT_2:def 1;
f.z1 in the carrier of TOP-REAL 2 by A51,FUNCT_2:5;
then
A56: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A33,A51,A52,FUNCT_1:13;
then f.z1=g.z2 by A49,A56,A55,A50,FUNCT_1:def 4;
hence thesis by A53,A54,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A30: C >0 by XREAL_1:139;
b-a>0 by A1,XREAL_1:50;
then
A31: A >0 by XREAL_1:139;
then
A32: (h.p2)`1<(h.p3)`1 by A10,A30,Th50;
(g.O)`2=d by A4,A15;
then
A33: ((g2).I)`1<=1 by A1,A9,A12,A15,A16,A21,Th62;
h is being_homeomorphism by A31,A30,Th50;
then
A34: h is one-to-one by TOPS_2:def 5;
A35: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A36: (h.p3)`1<(h.p4)`1 by A11,A31,A30,Th50;
A37: ((g2).I)`2= 1 by A2,A6,A16,Th55;
A38: ((g2).O)`2= 1 by A2,A4,A15,Th55;
(g.I)`2=d by A6,A16;
then
A39: -1 <=((g2).O)`1 by A1,A9,A12,A15,A16,A21,Th62;
A40: g2 is continuous one-to-one by A1,A2,A18,Th53;
A41: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A42: h.p4=g2.I by A16,FUNCT_1:13;
h.p2=g2.O by A15,A41,FUNCT_1:13;
then rng f2 meets rng g2 by A32,A36,A29,A42,A24,A23,A26,A22,A27,A25,A40,A38
,A37,A39,A33,A35,Th24,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A41,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A41,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A28,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A28,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A34,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A28: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A29: -1 <=((f2).O)`2 by A1,A2,A3,A7,A8,A14,Th59;
A30: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A31: ((f2).I)`2= 1 by A2,A5,A15,Th55;
a<=p3`1 by A9,A10,XXREAL_0:2;
then
A32: ((f2).I)`1<=1 by A1,A2,A5,A11,A15,Th59;
A33: ((f2).O)`1= -1 by A1,A3,A14,Th54;
A34: f2 is continuous one-to-one by A1,A2,A18,Th53;
A35: ((f2).O)`2<=1 by A1,A2,A3,A7,A8,A14,Th59;
set x = the Element of rng f2 /\ rng g2;
A36: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A37: h.p3=f2.I by A15,FUNCT_1:13;
b-a>0 by A1,XREAL_1:50;
then
A38: A >0 by XREAL_1:139;
then
A39: (h.p2)`1<(h.p3)`1 by A10,A28,Th50;
p2`1{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A42,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A42,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A36,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A36,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A41,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A28: C >0 by XREAL_1:139;
reconsider g2= h*g as Function of I[01],TOP-REAL 2;
A29: -1<((g2).I)`1 by A1,A12,A13,A17,Th64;
A30: ((g2).O)`2= 1 by A2,A4,A16,Th55;
A31: g2 is continuous one-to-one by A1,A2,A19,Th53;
A32: (g.I)`2= c by A6,A17;
p2`1****0 by A1,XREAL_1:50;
then
A37: A >0 by XREAL_1:139;
then
A38: (h.p2)`1<(h.p3)`1 by A10,A28,Th50;
a<=p3`1 by A9,A10,XXREAL_0:2;
then
A39: ((f2).I)`1<=1 by A1,A2,A5,A11,A15,Th59;
h is being_homeomorphism by A37,A28,Th50;
then
A40: h is one-to-one by TOPS_2:def 5;
A41: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A21,Th52;
A42: ((g2).I)`2= -1 by A2,A6,A17,Th57;
A43: dom g=the carrier of I[01] by FUNCT_2:def 1;
then h.p2=g2.O by A16,FUNCT_1:13;
then rng f2 meets rng g2 by A38,A36,A24,A26,A25,A22,A23,A39,A27,A31,A30,A42
,A33,A29,A34,A41,Th26,JGRAPH_6:79;
then
A44: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A45: z2 in dom g2 and
A46: x=g2.z2 by FUNCT_1:def 3;
A47: x=h.(g.z2) by A43,A45,A46,FUNCT_1:13;
A48: g.z2 in rng g by A43,A45,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A45,FUNCT_2:5;
then
A49: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A44,XBOOLE_0:def 4;
then consider z1 being object such that
A50: z1 in dom f2 and
A51: x=f2.z1 by FUNCT_1:def 3;
A52: f.z1 in rng f by A35,A50,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A50,FUNCT_2:5;
then
A53: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A35,A50,A51,FUNCT_1:13;
then f.z1=g.z2 by A47,A53,A49,A40,FUNCT_1:def 4;
hence thesis by A52,A48,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A28: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A29: -1 <=((f2).O)`2 by A2,A7,A8,A14,Th60;
A30: ((f2).O)`1= -1 by A1,A3,A14,Th54;
A31: f2 is continuous one-to-one by A1,A2,A18,Th53;
p3`2 > c by A11,A12,XXREAL_0:2;
then
A32: ((f2).I)`2<=1 by A2,A13,A15,Th60;
A33: ((f2).O)`2<=1 by A2,A7,A8,A14,Th60;
set x = the Element of rng f2 /\ rng g2;
A34: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A35: h.p4=g2.I by A17,FUNCT_1:13;
b-a>0 by A1,XREAL_1:50;
then
A36: A >0 by XREAL_1:139;
then
A37: (h.p4)`2<(h.p3)`2 by A12,A28,Th51;
p4`2{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A34,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A34,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A42,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A42,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A39,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A30: C >0 by XREAL_1:139;
A31: (g.I)`2= c by A6,A18;
then
A32: ((g2).O)`1<=1 by A1,A9,A10,A13,A14,A17,A18,Th64;
A33: ((g2).I)`1<=1 by A1,A13,A14,A18,Th64;
A34: g2 is continuous one-to-one by A1,A2,A20,Th53;
A35: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A22,Th52;
A36: ((g2).I)`2= -1 by A2,A6,A18,Th57;
A37: ((g2).O)`2= 1 by A2,A4,A17,Th55;
A38: ((f2).I)`2<=1 by A2,A11,A12,A16,Th60;
A39: ((f2).I)`1= 1 by A1,A5,A16,Th56;
-1 <=((g2).O)`1 by A1,A9,A10,A13,A14,A17,A18,A31,Th64;
then rng f2 meets rng g2 by A26,A28,A39,A24,A25,A27,A38,A29,A34,A37,A36,A32
,A23,A33,A35,Th28,JGRAPH_6:79;
then
A40: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng f2 by XBOOLE_0:def 4;
then consider z1 being object such that
A41: z1 in dom f2 and
A42: x=f2.z1 by FUNCT_1:def 3;
A43: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A44: f.z1 in rng f by A41,FUNCT_1:def 3;
b-a>0 by A1,XREAL_1:50;
then A >0 by XREAL_1:139;
then h is being_homeomorphism by A30,Th51;
then
A45: h is one-to-one by TOPS_2:def 5;
f.z1 in the carrier of TOP-REAL 2 by A41,FUNCT_2:5;
then
A46: f.z1 in dom h by FUNCT_2:def 1;
x in rng g2 by A40,XBOOLE_0:def 4;
then consider z2 being object such that
A47: z2 in dom g2 and
A48: x=g2.z2 by FUNCT_1:def 3;
A49: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A50: g.z2 in rng g by A47,FUNCT_1:def 3;
A51: x=h.(g.z2) by A49,A47,A48,FUNCT_1:13;
g.z2 in the carrier of TOP-REAL 2 by A47,FUNCT_2:5;
then
A52: g.z2 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A43,A41,A42,FUNCT_1:13;
then f.z1=g.z2 by A51,A46,A52,A45,FUNCT_1:def 4;
hence thesis by A44,A50,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A28: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A29: f2 is continuous one-to-one by A1,A2,A18,Th53;
A30: p3`1 > a by A11,A12,XXREAL_0:2;
then
A31: ((f2).I)`1<=1 by A1,A2,A5,A13,A15,Th61;
A32: (f.I)`2= c by A5,A15;
then
A33: ((f2).O)`2<=1 by A1,A2,A7,A8,A13,A14,A15,A30,Th61;
set x = the Element of rng f2 /\ rng g2;
A34: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A35: h.p4=g2.I by A17,FUNCT_1:13;
A36: ((g2).I)`2= -1 by A2,A6,A17,Th57;
A37: ((g2).O)`2= 1 by A2,A4,A16,Th55;
b-a>0 by A1,XREAL_1:50;
then
A38: A >0 by XREAL_1:139;
then h is being_homeomorphism by A28,Th50;
then
A39: h is one-to-one by TOPS_2:def 5;
A40: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A21,Th52;
A41: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A42: ((f2).I)`2= -1 by A2,A5,A15,Th57;
A43: ((f2).O)`1= -1 by A1,A3,A14,Th54;
A44: dom f=the carrier of I[01] by FUNCT_2:def 1;
then h.p3=f2.I by A15,FUNCT_1:13;
then
A45: ((g2).I)`1< ((f2).I)`1 by A12,A38,A28,A35,Th50;
-1 <=((f2).O)`2 by A1,A2,A7,A8,A13,A14,A15,A30,A32,Th61;
then rng f2 meets rng g2 by A29,A43,A42,A33,A31,A41,A22,A37,A36,A26,A27,A24
,A40,A45,Th29,JGRAPH_6:79;
then
A46: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A47: z2 in dom g2 and
A48: x=g2.z2 by FUNCT_1:def 3;
A49: x=h.(g.z2) by A34,A47,A48,FUNCT_1:13;
A50: g.z2 in rng g by A34,A47,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A47,FUNCT_2:5;
then
A51: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A46,XBOOLE_0:def 4;
then consider z1 being object such that
A52: z1 in dom f2 and
A53: x=f2.z1 by FUNCT_1:def 3;
A54: f.z1 in rng f by A44,A52,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A52,FUNCT_2:5;
then
A55: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A44,A52,A53,FUNCT_1:13;
then f.z1=g.z2 by A49,A55,A51,A39,FUNCT_1:def 4;
hence thesis by A54,A50,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****p4`2 by A10,A11,XXREAL_0:2;
(g.O)`1=b by A4,A15;
then
A22: ((g2).I)`2>= -1 by A2,A9,A12,A15,A16,A21,Th65;
d-c >0 by A2,XREAL_1:50;
then
A23: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A24: ((f2).O)`2<=1 by A2,A7,A8,A13,Th60;
A25: ((f2).O)`1= -1 by A1,A3,A13,Th54;
A26: f2 is continuous one-to-one by A1,A2,A17,Th53;
A27: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A28: ((f2).I)`1= 1 by A1,A5,A14,Th56;
set x = the Element of rng f2 /\ rng g2;
A29: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A30: h.p3=f2.I by A14,FUNCT_1:13;
(g.I)`1= b by A6,A16;
then
A31: 1 >=((g2).O)`2 by A2,A9,A12,A15,A16,A21,Th65;
A32: ((g2).O)`1= 1 by A1,A4,A15,Th56;
A33: g2 is continuous one-to-one by A1,A2,A18,Th53;
A34: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A35: ((g2).I)`1= 1 by A1,A6,A16,Th56;
b-a>0 by A1,XREAL_1:50;
then
A36: A >0 by XREAL_1:139;
then h is being_homeomorphism by A23,Th50;
then
A37: h is one-to-one by TOPS_2:def 5;
A38: dom g=the carrier of I[01] by FUNCT_2:def 1;
then h.p2=g2.O by A15,FUNCT_1:13;
then
A39: ((g2).O)`2> ((f2).I)`2 by A11,A36,A23,A30,Th51;
h.p4=g2.I by A16,A38,FUNCT_1:13;
then
A40: ((g2).I)`2< ((f2).I)`2 by A10,A36,A23,A30,Th51;
-1 <=((f2).O)`2 by A2,A7,A8,A13,Th60;
then rng f2 meets rng g2 by A26,A25,A28,A24,A27,A33,A32,A35,A31,A22,A34,A39
,A40,Th30,JGRAPH_6:79;
then
A41: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A42: z2 in dom g2 and
A43: x=g2.z2 by FUNCT_1:def 3;
A44: x=h.(g.z2) by A38,A42,A43,FUNCT_1:13;
A45: g.z2 in rng g by A38,A42,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A42,FUNCT_2:5;
then
A46: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A41,XBOOLE_0:def 4;
then consider z1 being object such that
A47: z1 in dom f2 and
A48: x=f2.z1 by FUNCT_1:def 3;
A49: f.z1 in rng f by A29,A47,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A47,FUNCT_2:5;
then
A50: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A29,A47,A48,FUNCT_1:13;
then f.z1=g.z2 by A44,A50,A46,A37,FUNCT_1:def 4;
hence thesis by A49,A45,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A24: C >0 by XREAL_1:139;
reconsider g2= h*g as Function of I[01],TOP-REAL 2;
A25: ((g2).I)`1> -1 by A1,A2,A6,A12,A13,A17,Th66;
A26: ((g2).O)`1= 1 by A1,A4,A16,Th56;
A27: g2 is continuous one-to-one by A1,A2,A19,Th53;
p2`2> c by A9,A10,XXREAL_0:2;
then
A28: 1 >=((g2).O)`2 by A1,A2,A4,A11,A16,Th66;
set x = the Element of rng f2 /\ rng g2;
A29: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A30: h.p3=f2.I by A15,FUNCT_1:13;
A31: ((f2).O)`2<=1 by A2,A7,A8,A14,Th60;
A32: f2 is continuous one-to-one by A1,A2,A18,Th53;
b-a>0 by A1,XREAL_1:50;
then
A33: A >0 by XREAL_1:139;
then h is being_homeomorphism by A24,Th50;
then
A34: h is one-to-one by TOPS_2:def 5;
A35: dom g=the carrier of I[01] by FUNCT_2:def 1;
then h.p2=g2.O by A16,FUNCT_1:13;
then
A36: ((g2).O)`2> ((f2).I)`2 by A10,A33,A24,A30,Th51;
p3`2 < d by A10,A11,XXREAL_0:2;
then
A37: -1<=((f2).I)`2 by A2,A9,A15,Th60;
A38: ((f2).I)`1= 1 by A1,A5,A15,Th56;
A39: ((f2).O)`1= -1 by A1,A3,A14,Th54;
A40: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A21,Th52;
A41: ((g2).I)`2= -1 by A2,A6,A17,Th57;
1>=((g2).I)`1 by A1,A2,A6,A12,A13,A17,Th66;
then rng f2 meets rng g2 by A32,A39,A38,A22,A31,A37,A23,A27,A26,A41,A28,A25
,A40,A36,Th31,JGRAPH_6:79;
then
A42: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A43: z2 in dom g2 and
A44: x=g2.z2 by FUNCT_1:def 3;
A45: x=h.(g.z2) by A35,A43,A44,FUNCT_1:13;
A46: g.z2 in rng g by A35,A43,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A43,FUNCT_2:5;
then
A47: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A42,XBOOLE_0:def 4;
then consider z1 being object such that
A48: z1 in dom f2 and
A49: x=f2.z1 by FUNCT_1:def 3;
A50: f.z1 in rng f by A29,A48,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A48,FUNCT_2:5;
then
A51: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A29,A48,A49,FUNCT_1:13;
then f.z1=g.z2 by A45,A51,A47,A34,FUNCT_1:def 4;
hence thesis by A50,A46,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****=((g2).O)`2 by A1,A2,A4,A9,A10,A16,Th66;
p4`1<=b by A12,A13,XXREAL_0:2;
then
A23: ((g2).I)`1> -1 by A1,A2,A6,A11,A17,Th66;
d-c >0 by A2,XREAL_1:50;
then
A24: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A25: f2 is continuous one-to-one by A1,A2,A18,Th53;
A26: p3`1 >a by A11,A12,XXREAL_0:2;
then
A27: ((f2).I)`1<=1 by A1,A2,A5,A13,A15,Th61;
A28: (f.I)`2= c by A5,A15;
then
A29: ((f2).O)`2<=1 by A1,A2,A7,A8,A13,A14,A15,A26,Th61;
set x = the Element of rng f2 /\ rng g2;
A30: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A31: h.p4=g2.I by A17,FUNCT_1:13;
b-a>0 by A1,XREAL_1:50;
then
A32: A >0 by XREAL_1:139;
then h is being_homeomorphism by A24,Th50;
then
A33: h is one-to-one by TOPS_2:def 5;
A34: dom f=the carrier of I[01] by FUNCT_2:def 1;
then h.p3=f2.I by A15,FUNCT_1:13;
then
A35: ((g2).I)`1< ((f2).I)`1 by A12,A32,A24,A31,Th50;
A36: ((g2).O)`2>= -1 by A1,A2,A4,A9,A10,A16,Th66;
A37: g2 is continuous one-to-one by A1,A2,A19,Th53;
A38: ((g2).I)`2= -1 by A2,A6,A17,Th57;
A39: ((g2).O)`1= 1 by A1,A4,A16,Th56;
A40: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A21,Th52;
A41: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A42: ((f2).I)`2= -1 by A2,A5,A15,Th57;
A43: ((f2).O)`1= -1 by A1,A3,A14,Th54;
-1 <=((f2).O)`2 by A1,A2,A7,A8,A13,A14,A15,A26,A28,Th61;
then rng f2 meets rng g2 by A25,A43,A42,A29,A27,A41,A37,A39,A38,A22,A36,A23
,A40,A35,Th32,JGRAPH_6:79;
then
A44: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A45: z2 in dom g2 and
A46: x=g2.z2 by FUNCT_1:def 3;
A47: x=h.(g.z2) by A30,A45,A46,FUNCT_1:13;
A48: g.z2 in rng g by A30,A45,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A45,FUNCT_2:5;
then
A49: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A44,XBOOLE_0:def 4;
then consider z1 being object such that
A50: z1 in dom f2 and
A51: x=f2.z1 by FUNCT_1:def 3;
A52: f.z1 in rng f by A34,A50,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A50,FUNCT_2:5;
then
A53: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A34,A50,A51,FUNCT_1:13;
then f.z1=g.z2 by A47,A53,A49,A33,FUNCT_1:def 4;
hence thesis by A52,A48,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****p4`1 by A10,A11,XXREAL_0:2;
(g.O)`2= c by A4,A15;
then
A22: ((g2).I)`1> -1 by A1,A9,A12,A15,A16,A21,Th67;
d-c >0 by A2,XREAL_1:50;
then
A23: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A24: b>p3`1 by A11,A12,XXREAL_0:2;
(g.I)`2= c by A6,A16;
then
A25: 1 >=((g2).O)`1 by A1,A9,A12,A15,A16,A21,Th67;
A26: ((g2).O)`2= -1 by A2,A4,A15,Th57;
A27: g2 is continuous one-to-one by A1,A2,A18,Th53;
A28: ((f2).O)`1= -1 by A1,A3,A13,Th54;
A29: f2 is continuous one-to-one by A1,A2,A17,Th53;
set x = the Element of rng f2 /\ rng g2;
A30: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A31: h.p3=f2.I by A14,FUNCT_1:13;
A32: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A33: ((g2).I)`2= -1 by A2,A6,A16,Th57;
b-a>0 by A1,XREAL_1:50;
then
A34: A >0 by XREAL_1:139;
then h is being_homeomorphism by A23,Th50;
then
A35: h is one-to-one by TOPS_2:def 5;
A36: (f.I)`2= c by A5,A14;
A37: dom g=the carrier of I[01] by FUNCT_2:def 1;
then h.p2=g2.O by A15,FUNCT_1:13;
then
A38: ((g2).O)`1> ((f2).I)`1 by A11,A34,A23,A31,Th50;
A39: p3`1 >a by A9,A10,XXREAL_0:2;
then
A40: ((f2).O)`2<=1 by A1,A2,A7,A8,A13,A14,A24,A36,Th61;
A41: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A42: ((f2).I)`2= -1 by A2,A5,A14,Th57;
h.p4=g2.I by A16,A37,FUNCT_1:13;
then
A43: ((g2).I)`1< ((f2).I)`1 by A10,A34,A23,A31,Th50;
-1 <=((f2).O)`2 by A1,A2,A7,A8,A13,A14,A39,A24,A36,Th61;
then rng f2 meets rng g2 by A29,A28,A42,A40,A41,A27,A26,A33,A25,A22,A32,A38
,A43,Th33,JGRAPH_6:79;
then
A44: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A45: z2 in dom g2 and
A46: x=g2.z2 by FUNCT_1:def 3;
A47: x=h.(g.z2) by A37,A45,A46,FUNCT_1:13;
A48: g.z2 in rng g by A37,A45,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A45,FUNCT_2:5;
then
A49: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A44,XBOOLE_0:def 4;
then consider z1 being object such that
A50: z1 in dom f2 and
A51: x=f2.z1 by FUNCT_1:def 3;
A52: f.z1 in rng f by A30,A50,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A50,FUNCT_2:5;
then
A53: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A30,A50,A51,FUNCT_1:13;
then f.z1=g.z2 by A47,A53,A49,A35,FUNCT_1:def 4;
hence thesis by A52,A48,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A30: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A31: f2 is continuous one-to-one by A1,A2,A16,Th53;
A32: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A18,Th52;
A33: ((f2).I)`2= 1 by A2,A5,A13,Th55;
A34: (f.I)`2=d by A5,A13;
A35: p3`1****0 by A1,XREAL_1:50;
then
A40: A >0 by XREAL_1:139;
then
A41: (h.p1)`1<(h.p2)`1 by A8,A30,Th50;
A42: (h.p3)`1<(h.p4)`1 by A10,A40,A30,Th50;
A43: (h.p2)`1<(h.p3)`1 by A9,A40,A30,Th50;
h.p1=f2.O by A12,A38,FUNCT_1:13;
then f2.O,g2.O,f2.I,g2.I are_in_this_order_on rectangle(-1,1,-1,1) by A41,A43
,A42,A28,A39,A29,A37,A33,A36,A26,A25,A23,Th34;
then rng f2 meets rng g2 by A31,A32,A20,A24,JGRAPH_6:79;
then
A44: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A45: z2 in dom g2 and
A46: x=g2.z2 by FUNCT_1:def 3;
A47: x=h.(g.z2) by A27,A45,A46,FUNCT_1:13;
h is being_homeomorphism by A40,A30,Th51;
then
A48: h is one-to-one by TOPS_2:def 5;
x in rng f2 by A44,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A38,A49,FUNCT_1:def 3;
A52: g.z2 in rng g by A27,A45,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A45,FUNCT_2:5;
then
A53: g.z2 in dom h by FUNCT_2:def 1;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A54: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A38,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A47,A54,A53,A48,FUNCT_1:def 4;
hence thesis by A51,A52,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A29: C >0 by XREAL_1:139;
b-a>0 by A1,XREAL_1:50;
then
A30: A >0 by XREAL_1:139;
then
A31: (h.p1)`1<(h.p2)`1 by A8,A29,Th50;
(f.O)`2=d by A3,A13;
then
A32: ((f2).I)`1<=1 by A1,A7,A10,A13,A14,A21,Th62;
h is being_homeomorphism by A30,A29,Th50;
then
A33: h is one-to-one by TOPS_2:def 5;
A34: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A35: ((f2).I)`2= 1 by A2,A5,A14,Th55;
A36: ((f2).O)`2= 1 by A2,A3,A13,Th55;
A37: f2 is continuous one-to-one by A1,A2,A17,Th53;
A38: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A39: (h.p2)`1<(h.p3)`1 by A9,A30,A29,Th50;
A40: ((g2).I)`2<=1 by A1,A2,A6,A11,A12,A16,Th63;
A41: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A42: h.p2=g2.O by A15,FUNCT_1:13;
h.p1=f2.O by A13,A27,FUNCT_1:13;
then rng f2 meets rng g2 by A31,A39,A42,A28,A37,A36,A35,A25,A32,A34,A26,A24
,A23,A22,A40,A38,Th35,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A41,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A41,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A27,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A27,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A33,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A29: C >0 by XREAL_1:139;
b-a>0 by A1,XREAL_1:50;
then
A30: A >0 by XREAL_1:139;
then
A31: (h.p1)`1<(h.p2)`1 by A8,A29,Th50;
(f.O)`2=d by A3,A13;
then
A32: ((f2).I)`1<=1 by A1,A7,A10,A13,A14,A21,Th62;
h is being_homeomorphism by A30,A29,Th50;
then
A33: h is one-to-one by TOPS_2:def 5;
A34: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A35: ((f2).I)`2= 1 by A2,A5,A14,Th55;
A36: ((f2).O)`2= 1 by A2,A3,A13,Th55;
A37: f2 is continuous one-to-one by A1,A2,A17,Th53;
A38: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A39: (h.p2)`1<(h.p3)`1 by A9,A30,A29,Th50;
A40: ((g2).I)`1<=1 by A1,A11,A12,A16,Th64;
A41: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A42: h.p2=g2.O by A15,FUNCT_1:13;
h.p1=f2.O by A13,A27,FUNCT_1:13;
then rng f2 meets rng g2 by A31,A39,A42,A28,A37,A36,A35,A25,A32,A34,A26,A24
,A23,A22,A40,A38,Th36,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A41,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A41,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A27,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A27,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A33,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A25: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A26: f2 is continuous one-to-one by A1,A2,A17,Th53;
p3`2> c by A10,A11,XXREAL_0:2;
then
A27: ((f2).I)`2<=1 by A1,A2,A5,A12,A14,Th63;
A28: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A29: ((f2).I)`1= 1 by A1,A5,A14,Th56;
p1`1<=b by A8,A9,XXREAL_0:2;
then
A30: -1 <=((f2).O)`1 by A1,A2,A3,A7,A13,Th63;
A31: ((f2).O)`2= 1 by A2,A3,A13,Th55;
set x = the Element of rng f2 /\ rng g2;
A32: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A33: h.p3=f2.I by A14,FUNCT_1:13;
b-a>0 by A1,XREAL_1:50;
then
A34: A >0 by XREAL_1:139;
then
A35: (h.p1)`1<(h.p2)`1 by A8,A25,Th50;
d>p4`2 by A11,A12,XXREAL_0:2;
then
A36: -1<=((g2).I)`2 by A1,A2,A6,A10,A16,Th63;
h is being_homeomorphism by A34,A25,Th51;
then
A37: h is one-to-one by TOPS_2:def 5;
A38: ((g2).O)`2= 1 by A2,A4,A15,Th55;
A39: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A40: h.p2=g2.O by A15,FUNCT_1:13;
A41: (h.p3)`2>(h.p4)`2 by A11,A34,A25,Th51;
A42: h.p4=g2.I by A16,A39,FUNCT_1:13;
h.p1=f2.O by A13,A32,FUNCT_1:13;
then f2.O,g2.O,f2.I,g2.I are_in_this_order_on rectangle(-1,1,-1,1) by A35,A41
,A40,A33,A42,A31,A29,A30,A27,A38,A24,A22,A36,Th37;
then rng f2 meets rng g2 by A26,A28,A21,A23,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A39,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A39,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A32,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A32,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A37,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A28: C >0 by XREAL_1:139;
reconsider g2= h*g as Function of I[01],TOP-REAL 2;
A29: -1<((g2).I)`1 by A1,A12,A13,A17,Th64;
A30: ((g2).O)`2= 1 by A2,A4,A16,Th55;
A31: g2 is continuous one-to-one by A1,A2,A19,Th53;
a 0 by A1,XREAL_1:50;
then
A36: A >0 by XREAL_1:139;
then
A37: (h.p1)`1<(h.p2)`1 by A8,A28,Th50;
p1`1<=b by A8,A9,XXREAL_0:2;
then
A38: -1 <=((f2).O)`1 by A1,A2,A3,A7,A14,Th63;
h is being_homeomorphism by A36,A28,Th51;
then
A39: h is one-to-one by TOPS_2:def 5;
A40: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A21,Th52;
A41: ((g2).I)`2= -1 by A2,A6,A17,Th57;
A42: dom f=the carrier of I[01] by FUNCT_2:def 1;
then h.p1=f2.O by A14,FUNCT_1:13;
then rng f2 meets rng g2 by A37,A35,A24,A26,A25,A38,A22,A23,A27,A31,A30,A41
,A32,A29,A33,A40,Th38,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A34,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A34,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A42,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A42,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A39,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****0 by A2,XREAL_1:50;
then
A24: C >0 by XREAL_1:139;
reconsider g2= h*g as Function of I[01],TOP-REAL 2;
A25: g2 is continuous one-to-one by A1,A2,A18,Th53;
b>=p4`1 by A11,A12,XXREAL_0:2;
then
A26: -1<((g2).I)`1 by A1,A10,A16,Th64;
A27: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A28: p3`1> a by A10,A11,XXREAL_0:2;
then
A29: ((f2).I)`1<=1 by A1,A12,A14,Th64;
A30: (f.I)`2= c by A5,A14;
p1`1<=b by A8,A9,XXREAL_0:2;
then
A31: -1 <=((f2).O)`1 by A1,A7,A12,A13,A14,A28,A30,Th64;
A32: ((g2).O)`2= 1 by A2,A4,A15,Th55;
A33: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A34: h.p2=g2.O by A15,FUNCT_1:13;
a 0 by A1,XREAL_1:50;
then
A39: A >0 by XREAL_1:139;
then
A40: (h.p1)`1<(h.p2)`1 by A8,A24,Th50;
A41: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A42: (h.p3)`1>(h.p4)`1 by A11,A39,A24,Th50;
A43: h.p4=g2.I by A16,A33,FUNCT_1:13;
h.p1=f2.O by A13,A37,FUNCT_1:13;
then f2.O,g2.O,f2.I,g2.I are_in_this_order_on rectangle(-1,1,-1,1) by A40,A42
,A34,A38,A43,A23,A22,A31,A29,A32,A36,A35,A26,Th39;
then rng f2 meets rng g2 by A21,A41,A25,A27,JGRAPH_6:79;
then
A44: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A45: z2 in dom g2 and
A46: x=g2.z2 by FUNCT_1:def 3;
A47: x=h.(g.z2) by A33,A45,A46,FUNCT_1:13;
h is being_homeomorphism by A39,A24,Th51;
then
A48: h is one-to-one by TOPS_2:def 5;
x in rng f2 by A44,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A37,A49,FUNCT_1:def 3;
A52: g.z2 in rng g by A33,A45,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A45,FUNCT_2:5;
then
A53: g.z2 in dom h by FUNCT_2:def 1;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A54: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A37,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A47,A54,A53,A48,FUNCT_1:def 4;
hence thesis by A51,A52,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****=p2`2 & p2`2>p3`2 & p3`2>p4`2 & p4
`2>= c & f.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 & f is continuous one-to-one & g is
continuous one-to-one & rng f c= closed_inside_of_rectangle(a,b,c,d) & rng g c=
closed_inside_of_rectangle(a,b,c,d) holds rng f meets rng g
proof
reconsider O=0,I=1 as Point of I[01] by BORSUK_1:40,XXREAL_1:1;
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d be Real, f,g be
Function of I[01],TOP-REAL 2;
assume that
A1: a****=p2`2 and
A10: p2`2>p3`2 and
A11: p3`2>p4`2 and
A12: p4`2>= c and
A13: f.0=p1 and
A14: f.1=p3 and
A15: g.0=p2 and
A16: g.1=p4 and
A17: f is continuous one-to-one and
A18: g is continuous one-to-one and
A19: rng f c= closed_inside_of_rectangle(a,b,c,d) and
A20: rng g c= closed_inside_of_rectangle(a,b,c,d);
set A=2/(b-a), B=-(b+a)/(b-a), C = 2/(d-c), D=-(d+c)/(d-c);
set h=AffineMap(A,B,C,D);
reconsider g2= h*g as Function of I[01],TOP-REAL 2;
A21: p2`2>p4`2 by A10,A11,XXREAL_0:2;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A22: -1 <=((f2).O)`1 by A1,A2,A3,A7,A8,A13,Th63;
A23: ((f2).O)`2= 1 by A2,A3,A13,Th55;
A24: f2 is continuous one-to-one by A1,A2,A17,Th53;
A25: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A26: ((f2).I)`1= 1 by A1,A5,A14,Th56;
A27: ((f2).O)`1<=1 by A1,A2,A3,A7,A8,A13,Th63;
set x = the Element of rng f2 /\ rng g2;
A28: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A29: h.p3=f2.I by A14,FUNCT_1:13;
d-c >0 by A2,XREAL_1:50;
then
A30: C >0 by XREAL_1:139;
b-a>0 by A1,XREAL_1:50;
then
A31: A >0 by XREAL_1:139;
then
A32: (h.p2)`2>(h.p3)`2 by A10,A30,Th51;
(g.O)`1=b by A4,A15;
then
A33: ((g2).I)`2>= -1 by A2,A9,A12,A15,A16,A21,Th65;
h is being_homeomorphism by A31,A30,Th51;
then
A34: h is one-to-one by TOPS_2:def 5;
A35: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A36: (h.p3)`2>(h.p4)`2 by A11,A31,A30,Th51;
A37: ((g2).I)`1= 1 by A1,A6,A16,Th56;
A38: ((g2).O)`1= 1 by A1,A4,A15,Th56;
(g.I)`1=b by A6,A16;
then
A39: 1 >=((g2).O)`2 by A2,A9,A12,A15,A16,A21,Th65;
A40: g2 is continuous one-to-one by A1,A2,A18,Th53;
A41: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A42: h.p4=g2.I by A16,FUNCT_1:13;
h.p2=g2.O by A15,A41,FUNCT_1:13;
then rng f2 meets rng g2 by A32,A36,A29,A42,A24,A23,A26,A22,A27,A25,A40,A38
,A37,A39,A33,A35,Th40,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A41,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A41,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A28,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A28,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A34,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****=p2`2 & p2`2>p3`2 & p3`2>p4`2 & p4`2>= c & P
is_an_arc_of p1,p3 & Q is_an_arc_of p2,p4 & P c= closed_inside_of_rectangle(a,b
,c,d) & Q c= closed_inside_of_rectangle(a,b,c,d) holds P meets Q
proof
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d be Real, P,Q be
Subset of TOP-REAL 2;
assume that
A1: a****=p2`2 and
A10: p2`2>p3`2 and
A11: p3`2>p4`2 and
A12: p4`2>= c and
A13: P is_an_arc_of p1,p3 and
A14: Q is_an_arc_of p2,p4 and
A15: P c= closed_inside_of_rectangle(a,b,c,d) and
A16: Q c= closed_inside_of_rectangle(a,b,c,d);
A17: ex g being Function of I[01],TOP-REAL 2 st g is continuous one-to-one
& rng g=Q & g.0=p2 & g.1=p4 by A14,Th2;
ex f being Function of I[01],TOP-REAL 2 st f is continuous one-to-one
& rng f=P & f.0=p1 & f.1=p3 by A13,Th2;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A15,A16,A17,Th120;
end;
theorem Th122:
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real
, f,g being Function of I[01],TOP-REAL 2 st a****=p2`2 & p2`2>p3`2 & p3`2>= c & a <
p4`1 & p4`1<=b & f.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 & f is continuous one-to-one
& g is continuous one-to-one & rng f c= closed_inside_of_rectangle(a,b,c,d) &
rng g c= closed_inside_of_rectangle(a,b,c,d) holds rng f meets rng g
proof
reconsider O=0,I=1 as Point of I[01] by BORSUK_1:40,XXREAL_1:1;
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d be Real, f,g be
Function of I[01],TOP-REAL 2;
assume that
A1: a****=p2`2 and
A10: p2`2>p3`2 and
A11: p3`2>= c and
A12: a 0 by A2,XREAL_1:50;
then
A28: C >0 by XREAL_1:139;
reconsider g2= h*g as Function of I[01],TOP-REAL 2;
A29: -1<((g2).I)`1 by A1,A2,A6,A12,A13,A17,Th66;
A30: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A21,Th52;
A31: ((g2).I)`2= -1 by A2,A6,A17,Th57;
c 0 by A1,XREAL_1:50;
then
A38: A >0 by XREAL_1:139;
then
A39: (h.p2)`2>(h.p3)`2 by A10,A28,Th51;
d>=p3`2 by A9,A10,XXREAL_0:2;
then
A40: -1<=((f2).I)`2 by A1,A2,A5,A11,A15,Th63;
h is being_homeomorphism by A38,A28,Th51;
then
A41: h is one-to-one by TOPS_2:def 5;
A42: dom g=the carrier of I[01] by FUNCT_2:def 1;
then h.p2=g2.O by A16,FUNCT_1:13;
then rng f2 meets rng g2 by A39,A37,A24,A26,A25,A22,A23,A40,A27,A34,A33,A31
,A32,A29,A35,A30,Th41,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A42,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A42,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A36,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A36,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A41,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****=p2`2 & p2`2>p3`2 & p3`2>= c & a =p2`2 and
A10: p2`2>p3`2 and
A11: p3`2>= c and
A12: a 0 by A2,XREAL_1:50;
then
A28: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A29: p3`1 >a by A11,A12,XXREAL_0:2;
then
A30: ((f2).I)`1<=1 by A1,A13,A15,Th64;
A31: ((f2).I)`2= -1 by A2,A5,A15,Th57;
A32: ((f2).O)`2= 1 by A2,A3,A14,Th55;
A33: f2 is continuous one-to-one by A1,A2,A18,Th53;
set x = the Element of rng f2 /\ rng g2;
A34: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A35: h.p4=g2.I by A17,FUNCT_1:13;
b-a>0 by A1,XREAL_1:50;
then
A36: A >0 by XREAL_1:139;
then
A37: (h.p4)`1<(h.p3)`1 by A12,A28,Th50;
p4`1****{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A46: z2 in dom g2 and
A47: x=g2.z2 by FUNCT_1:def 3;
A48: x=h.(g.z2) by A34,A46,A47,FUNCT_1:13;
A49: g.z2 in rng g by A34,A46,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A46,FUNCT_2:5;
then
A50: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A45,XBOOLE_0:def 4;
then consider z1 being object such that
A51: z1 in dom f2 and
A52: x=f2.z1 by FUNCT_1:def 3;
A53: f.z1 in rng f by A44,A51,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A51,FUNCT_2:5;
then
A54: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A44,A51,A52,FUNCT_1:13;
then f.z1=g.z2 by A48,A54,A50,A39,FUNCT_1:def 4;
hence thesis by A53,A49,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****p4`1 by A10,A11,XXREAL_0:2;
(g.O)`2= c by A4,A15;
then
A22: ((g2).I)`1> -1 by A1,A9,A12,A15,A16,A21,Th67;
d-c >0 by A2,XREAL_1:50;
then
A23: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A24: b>p3`1 by A11,A12,XXREAL_0:2;
(g.I)`2= c by A6,A16;
then
A25: 1 >=((g2).O)`1 by A1,A9,A12,A15,A16,A21,Th67;
A26: ((g2).O)`2= -1 by A2,A4,A15,Th57;
A27: g2 is continuous one-to-one by A1,A2,A18,Th53;
A28: ((f2).O)`2= 1 by A2,A3,A13,Th55;
A29: f2 is continuous one-to-one by A1,A2,A17,Th53;
set x = the Element of rng f2 /\ rng g2;
A30: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A31: h.p3=f2.I by A14,FUNCT_1:13;
A32: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A33: ((g2).I)`2= -1 by A2,A6,A16,Th57;
b-a>0 by A1,XREAL_1:50;
then
A34: A >0 by XREAL_1:139;
then h is being_homeomorphism by A23,Th51;
then
A35: h is one-to-one by TOPS_2:def 5;
A36: (f.I)`2= c by A5,A14;
A37: dom g=the carrier of I[01] by FUNCT_2:def 1;
then h.p2=g2.O by A15,FUNCT_1:13;
then
A38: ((g2).O)`1> ((f2).I)`1 by A11,A34,A23,A31,Th50;
A39: p3`1 > a by A9,A10,XXREAL_0:2;
then
A40: ((f2).O)`1<=1 by A1,A7,A8,A13,A14,A24,A36,Th64;
A41: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A42: ((f2).I)`2= -1 by A2,A5,A14,Th57;
h.p4=g2.I by A16,A37,FUNCT_1:13;
then
A43: ((g2).I)`1< ((f2).I)`1 by A10,A34,A23,A31,Th50;
-1 <=((f2).O)`1 by A1,A7,A8,A13,A14,A39,A24,A36,Th64;
then rng f2 meets rng g2 by A29,A28,A42,A40,A41,A27,A26,A33,A25,A22,A32,A38
,A43,Th43,JGRAPH_6:79;
then
A44: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A45: z2 in dom g2 and
A46: x=g2.z2 by FUNCT_1:def 3;
A47: x=h.(g.z2) by A37,A45,A46,FUNCT_1:13;
A48: g.z2 in rng g by A37,A45,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A45,FUNCT_2:5;
then
A49: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A44,XBOOLE_0:def 4;
then consider z1 being object such that
A50: z1 in dom f2 and
A51: x=f2.z1 by FUNCT_1:def 3;
A52: f.z1 in rng f by A30,A50,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A50,FUNCT_2:5;
then
A53: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A30,A50,A51,FUNCT_1:13;
then f.z1=g.z2 by A47,A53,A49,A35,FUNCT_1:def 4;
hence thesis by A52,A48,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****=p1`2 & p1`2>p2`2 & p2`2>p3`2 & p3`2>p4`2 & p4`2>= c & f
.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 & f is continuous one-to-one & g is continuous
one-to-one & rng f c= closed_inside_of_rectangle(a,b,c,d) & rng g c=
closed_inside_of_rectangle(a,b,c,d) holds rng f meets rng g
proof
reconsider O=0,I=1 as Point of I[01] by BORSUK_1:40,XXREAL_1:1;
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d be Real, f,g be
Function of I[01],TOP-REAL 2;
assume that
A1: a****=p1`2 and
A8: p1`2>p2`2 and
A9: p2`2>p3`2 and
A10: p3`2>p4`2 and
A11: p4`2>= c and
A12: f.0=p1 and
A13: f.1=p3 and
A14: g.0=p2 and
A15: g.1=p4 and
A16: f is continuous one-to-one and
A17: g is continuous one-to-one and
A18: rng f c= closed_inside_of_rectangle(a,b,c,d) and
A19: rng g c= closed_inside_of_rectangle(a,b,c,d);
set A=2/(b-a), B=-(b+a)/(b-a), C = 2/(d-c), D=-(d+c)/(d-c);
set h=AffineMap(A,B,C,D);
reconsider g2= h*g as Function of I[01],TOP-REAL 2;
A20: g2 is continuous one-to-one by A1,A2,A17,Th53;
A21: (g.O)`1=b by A4,A14;
A22: d>p2`2 by A7,A8,XXREAL_0:2;
p2`2>p4`2 by A9,A10,XXREAL_0:2;
then
A23: ((g2).I)`2>= -1 by A2,A11,A14,A15,A22,A21,Th65;
A24: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A25: ((g2).I)`1= 1 by A1,A6,A15,Th56;
A26: ((g2).O)`1= 1 by A1,A4,A14,Th56;
A27: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A28: h.p2=g2.O by A14,FUNCT_1:13;
A29: h.p4=g2.I by A15,A27,FUNCT_1:13;
d-c >0 by A2,XREAL_1:50;
then
A30: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A31: f2 is continuous one-to-one by A1,A2,A16,Th53;
A32: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A18,Th52;
A33: ((f2).I)`1= 1 by A1,A5,A13,Th56;
A34: (f.I)`1=b by A5,A13;
A35: p3`2> c by A10,A11,XXREAL_0:2;
p1`2>p3`2 by A8,A9,XXREAL_0:2;
then
A36: 1 >=((f2).O)`2 by A2,A7,A12,A13,A35,A34,Th65;
A37: ((f2).O)`1= 1 by A1,A3,A12,Th56;
set x = the Element of rng f2 /\ rng g2;
A38: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A39: h.p3=f2.I by A13,FUNCT_1:13;
b-a>0 by A1,XREAL_1:50;
then
A40: A >0 by XREAL_1:139;
then
A41: (h.p1)`2>(h.p2)`2 by A8,A30,Th51;
A42: (h.p3)`2>(h.p4)`2 by A10,A40,A30,Th51;
A43: (h.p2)`2>(h.p3)`2 by A9,A40,A30,Th51;
h.p1=f2.O by A12,A38,FUNCT_1:13;
then f2.O,g2.O,f2.I,g2.I are_in_this_order_on rectangle(-1,1,-1,1) by A41,A43
,A42,A28,A39,A29,A37,A33,A36,A26,A25,A23,Th44;
then rng f2 meets rng g2 by A31,A32,A20,A24,JGRAPH_6:79;
then
A44: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A45: z2 in dom g2 and
A46: x=g2.z2 by FUNCT_1:def 3;
A47: x=h.(g.z2) by A27,A45,A46,FUNCT_1:13;
h is being_homeomorphism by A40,A30,Th51;
then
A48: h is one-to-one by TOPS_2:def 5;
x in rng f2 by A44,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A38,A49,FUNCT_1:def 3;
A52: g.z2 in rng g by A27,A45,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A45,FUNCT_2:5;
then
A53: g.z2 in dom h by FUNCT_2:def 1;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A54: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A38,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A47,A54,A53,A48,FUNCT_1:def 4;
hence thesis by A51,A52,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****=p1`2 & p1`2>p2`2 & p2`2>p3`2 & p3`2>p4`2 & p4`2>= c & P is_an_arc_of
p1,p3 & Q is_an_arc_of p2,p4 & P c= closed_inside_of_rectangle(a,b,c,d) & Q c=
closed_inside_of_rectangle(a,b,c,d) holds P meets Q
proof
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d be Real, P,Q be
Subset of TOP-REAL 2;
assume that
A1: a****=p1`2 and
A8: p1`2>p2`2 and
A9: p2`2>p3`2 and
A10: p3`2>p4`2 and
A11: p4`2>= c and
A12: P is_an_arc_of p1,p3 and
A13: Q is_an_arc_of p2,p4 and
A14: P c= closed_inside_of_rectangle(a,b,c,d) and
A15: Q c= closed_inside_of_rectangle(a,b,c,d);
A16: ex g being Function of I[01],TOP-REAL 2 st g is continuous one-to-one
& rng g=Q & g.0=p2 & g.1=p4 by A13,Th2;
ex f being Function of I[01],TOP-REAL 2 st f is continuous one-to-one
& rng f=P & f.0=p1 & f.1=p3 by A12,Th2;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A14,A15,A16,Th128;
end;
theorem Th130:
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real
, f,g being Function of I[01],TOP-REAL 2 st a****=p1`2 & p1`2>p2`2 & p2`2>p3`2 & p3`2>= c & a=p1`2 and
A8: p1`2>p2`2 and
A9: p2`2>p3`2 and
A10: p3`2>= c and
A11: ap3`2 by A8,A9,XXREAL_0:2;
reconsider g2= h*g as Function of I[01],TOP-REAL 2;
A22: -1<((g2).I)`1 by A1,A2,A6,A11,A12,A16,Th66;
A23: ((g2).I)`2= -1 by A2,A6,A16,Th57;
A24: ((g2).O)`1= 1 by A1,A4,A15,Th56;
(f.I)`1=b by A5,A14;
then
A25: 1 >=((f2).O)`2 by A2,A7,A10,A13,A14,A21,Th65;
A26: g2 is continuous one-to-one by A1,A2,A18,Th53;
set x = the Element of rng f2 /\ rng g2;
A27: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A28: h.p3=f2.I by A14,FUNCT_1:13;
d-c >0 by A2,XREAL_1:50;
then
A29: C >0 by XREAL_1:139;
b-a>0 by A1,XREAL_1:50;
then
A30: A >0 by XREAL_1:139;
then
A31: (h.p1)`2>(h.p2)`2 by A8,A29,Th51;
(f.O)`1=b by A3,A13;
then
A32: ((f2).I)`2>= -1 by A2,A7,A10,A13,A14,A21,Th65;
h is being_homeomorphism by A30,A29,Th51;
then
A33: h is one-to-one by TOPS_2:def 5;
A34: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A35: ((f2).I)`1= 1 by A1,A5,A14,Th56;
A36: ((f2).O)`1= 1 by A1,A3,A13,Th56;
A37: f2 is continuous one-to-one by A1,A2,A17,Th53;
A38: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A39: (h.p2)`2>(h.p3)`2 by A9,A30,A29,Th51;
A40: ((g2).I)`1<=1 by A1,A2,A6,A11,A12,A16,Th66;
A41: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A42: h.p2=g2.O by A15,FUNCT_1:13;
h.p1=f2.O by A13,A27,FUNCT_1:13;
then rng f2 meets rng g2 by A31,A39,A42,A28,A37,A36,A35,A25,A32,A34,A26,A24
,A23,A22,A40,A38,Th45,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A41,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A41,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A27,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A27,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A33,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****=p1`2 & p1`2>p2`2 & p2`2>p3`2 & p3`2>= c & a=p1`2 and
A8: p1`2>p2`2 and
A9: p2`2>p3`2 and
A10: p3`2>= c and
A11: a=p1`2 & p1`2>p2`2 & p2`2>= c & b>=p3`1 & p3`1>p4`1 &
p4`1>a & f.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 & f is continuous one-to-one & g is
continuous one-to-one & rng f c= closed_inside_of_rectangle(a,b,c,d) & rng g c=
closed_inside_of_rectangle(a,b,c,d) holds rng f meets rng g
proof
reconsider O=0,I=1 as Point of I[01] by BORSUK_1:40,XXREAL_1:1;
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d be Real, f,g be
Function of I[01],TOP-REAL 2;
assume that
A1: a****=p1`2 and
A8: p1`2>p2`2 and
A9: p2`2>= c and
A10: b>=p3`1 and
A11: p3`1>p4`1 and
A12: p4`1>a and
A13: f.0=p1 and
A14: f.1=p3 and
A15: g.0=p2 and
A16: g.1=p4 and
A17: f is continuous one-to-one and
A18: g is continuous one-to-one and
A19: rng f c= closed_inside_of_rectangle(a,b,c,d) and
A20: rng g c= closed_inside_of_rectangle(a,b,c,d);
set A=2/(b-a), B=-(b+a)/(b-a), C = 2/(d-c), D=-(d+c)/(d-c);
set h=AffineMap(A,B,C,D);
reconsider g2= h*g as Function of I[01],TOP-REAL 2;
A21: g2 is continuous one-to-one by A1,A2,A18,Th53;
d >p2`2 by A7,A8,XXREAL_0:2;
then
A22: -1 <=((g2).O)`2 by A1,A2,A4,A9,A15,Th66;
A23: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A24: ((g2).I)`2= -1 by A2,A6,A16,Th57;
d-c >0 by A2,XREAL_1:50;
then
A25: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A26: f2 is continuous one-to-one by A1,A2,A17,Th53;
p3`1>a by A11,A12,XXREAL_0:2;
then
A27: ((f2).I)`1<=1 by A1,A2,A5,A10,A14,Th66;
A28: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A29: ((f2).I)`2= -1 by A2,A5,A14,Th57;
p1`2>= c by A8,A9,XXREAL_0:2;
then
A30: ((f2).O)`2<=1 by A1,A2,A3,A7,A13,Th66;
A31: ((f2).O)`1= 1 by A1,A3,A13,Th56;
set x = the Element of rng f2 /\ rng g2;
A32: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A33: h.p3=f2.I by A14,FUNCT_1:13;
b-a>0 by A1,XREAL_1:50;
then
A34: A >0 by XREAL_1:139;
then
A35: (h.p1)`2>(h.p2)`2 by A8,A25,Th51;
b>p4`1 by A10,A11,XXREAL_0:2;
then
A36: -1<((g2).I)`1 by A1,A2,A6,A12,A16,Th66;
h is being_homeomorphism by A34,A25,Th51;
then
A37: h is one-to-one by TOPS_2:def 5;
A38: ((g2).O)`1= 1 by A1,A4,A15,Th56;
A39: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A40: h.p2=g2.O by A15,FUNCT_1:13;
A41: (h.p3)`1>(h.p4)`1 by A11,A34,A25,Th50;
A42: h.p4=g2.I by A16,A39,FUNCT_1:13;
h.p1=f2.O by A13,A32,FUNCT_1:13;
then f2.O,g2.O,f2.I,g2.I are_in_this_order_on rectangle(-1,1,-1,1) by A35,A41
,A40,A33,A42,A31,A29,A30,A27,A38,A24,A22,A36,Th46;
then rng f2 meets rng g2 by A26,A28,A21,A23,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A39,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A39,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A32,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A32,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A37,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****=p1`2 & p1`2>p2`2 & p2`2>= c & b>=p3`1 & p3`1>p4`1 & p4`1>a & P
is_an_arc_of p1,p3 & Q is_an_arc_of p2,p4 & P c= closed_inside_of_rectangle(a,b
,c,d) & Q c= closed_inside_of_rectangle(a,b,c,d) holds P meets Q
proof
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d be Real, P,Q be
Subset of TOP-REAL 2;
assume that
A1: a****=p1`2 and
A8: p1`2>p2`2 and
A9: p2`2>= c and
A10: b>=p3`1 and
A11: p3`1>p4`1 and
A12: p4`1>a and
A13: P is_an_arc_of p1,p3 and
A14: Q is_an_arc_of p2,p4 and
A15: P c= closed_inside_of_rectangle(a,b,c,d) and
A16: Q c= closed_inside_of_rectangle(a,b,c,d);
A17: ex g being Function of I[01],TOP-REAL 2 st g is continuous one-to-one
& rng g=Q & g.0=p2 & g.1=p4 by A14,Th2;
ex f being Function of I[01],TOP-REAL 2 st f is continuous one-to-one
& rng f=P & f.0=p1 & f.1=p3 by A13,Th2;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A15,A16,A17,Th132;
end;
theorem Th134:
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real
, f,g being Function of I[01],TOP-REAL 2 st a****=p2`1 & p2`1>p3`1 & p3`1>p4`1 &
p4`1> a & f.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 & f is continuous one-to-one & g is
continuous one-to-one & rng f c= closed_inside_of_rectangle(a,b,c,d) & rng g c=
closed_inside_of_rectangle(a,b,c,d) holds rng f meets rng g
proof
reconsider O=0,I=1 as Point of I[01] by BORSUK_1:40,XXREAL_1:1;
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d be Real, f,g be
Function of I[01],TOP-REAL 2;
assume that
A1: a****=p2`1 and
A10: p2`1>p3`1 and
A11: p3`1>p4`1 and
A12: p4`1> a and
A13: f.0=p1 and
A14: f.1=p3 and
A15: g.0=p2 and
A16: g.1=p4 and
A17: f is continuous one-to-one and
A18: g is continuous one-to-one and
A19: rng f c= closed_inside_of_rectangle(a,b,c,d) and
A20: rng g c= closed_inside_of_rectangle(a,b,c,d);
set A=2/(b-a), B=-(b+a)/(b-a), C = 2/(d-c), D=-(d+c)/(d-c);
set h=AffineMap(A,B,C,D);
reconsider g2= h*g as Function of I[01],TOP-REAL 2;
A21: p2`1>p4`1 by A10,A11,XXREAL_0:2;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A22: -1 <=((f2).O)`2 by A1,A2,A3,A7,A8,A13,Th66;
A23: ((f2).O)`1= 1 by A1,A3,A13,Th56;
A24: f2 is continuous one-to-one by A1,A2,A17,Th53;
A25: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A26: ((f2).I)`2= -1 by A2,A5,A14,Th57;
A27: ((f2).O)`2<=1 by A1,A2,A3,A7,A8,A13,Th66;
set x = the Element of rng f2 /\ rng g2;
A28: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A29: h.p3=f2.I by A14,FUNCT_1:13;
d-c >0 by A2,XREAL_1:50;
then
A30: C >0 by XREAL_1:139;
b-a>0 by A1,XREAL_1:50;
then
A31: A >0 by XREAL_1:139;
then
A32: (h.p2)`1>(h.p3)`1 by A10,A30,Th50;
(g.O)`2= c by A4,A15;
then
A33: ((g2).I)`1> -1 by A1,A9,A12,A15,A16,A21,Th67;
h is being_homeomorphism by A31,A30,Th50;
then
A34: h is one-to-one by TOPS_2:def 5;
A35: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A20,Th52;
A36: (h.p3)`1>(h.p4)`1 by A11,A31,A30,Th50;
A37: ((g2).I)`2= -1 by A2,A6,A16,Th57;
A38: ((g2).O)`2= -1 by A2,A4,A15,Th57;
(g.I)`2= c by A6,A16;
then
A39: 1 >=((g2).O)`1 by A1,A9,A12,A15,A16,A21,Th67;
A40: g2 is continuous one-to-one by A1,A2,A18,Th53;
A41: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A42: h.p4=g2.I by A16,FUNCT_1:13;
h.p2=g2.O by A15,A41,FUNCT_1:13;
then rng f2 meets rng g2 by A32,A36,A29,A42,A24,A23,A26,A22,A27,A25,A40,A38
,A37,A39,A33,A35,Th47,JGRAPH_6:79;
then
A43: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A44: z2 in dom g2 and
A45: x=g2.z2 by FUNCT_1:def 3;
A46: x=h.(g.z2) by A41,A44,A45,FUNCT_1:13;
A47: g.z2 in rng g by A41,A44,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A44,FUNCT_2:5;
then
A48: g.z2 in dom h by FUNCT_2:def 1;
x in rng f2 by A43,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A28,A49,FUNCT_1:def 3;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A52: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A28,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A46,A52,A48,A34,FUNCT_1:def 4;
hence thesis by A51,A47,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****=p2`1 & p2`1>p3`1 & p3`1>p4`1 & p4`1> a & P
is_an_arc_of p1,p3 & Q is_an_arc_of p2,p4 & P c= closed_inside_of_rectangle(a,b
,c,d) & Q c= closed_inside_of_rectangle(a,b,c,d) holds P meets Q
proof
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d be Real, P,Q be
Subset of TOP-REAL 2;
assume that
A1: a****=p2`1 and
A10: p2`1>p3`1 and
A11: p3`1>p4`1 and
A12: p4`1> a and
A13: P is_an_arc_of p1,p3 and
A14: Q is_an_arc_of p2,p4 and
A15: P c= closed_inside_of_rectangle(a,b,c,d) and
A16: Q c= closed_inside_of_rectangle(a,b,c,d);
A17: ex g being Function of I[01],TOP-REAL 2 st g is continuous one-to-one
& rng g=Q & g.0=p2 & g.1=p4 by A14,Th2;
ex f being Function of I[01],TOP-REAL 2 st f is continuous one-to-one
& rng f=P & f.0=p1 & f.1=p3 by A13,Th2;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A15,A16,A17,Th134;
end;
theorem Th136:
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real
, f,g being Function of I[01],TOP-REAL 2 st a****=p1`1 & p1`1>p2`1 & p2`1>p3`1 & p3`1>p4`1 & p4`1> a
& f.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 & f is continuous one-to-one & g is
continuous one-to-one & rng f c= closed_inside_of_rectangle(a,b,c,d) & rng g c=
closed_inside_of_rectangle(a,b,c,d) holds rng f meets rng g
proof
reconsider O=0,I=1 as Point of I[01] by BORSUK_1:40,XXREAL_1:1;
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d be Real, f,g be
Function of I[01],TOP-REAL 2;
assume that
A1: a****=p1`1 and
A8: p1`1>p2`1 and
A9: p2`1>p3`1 and
A10: p3`1>p4`1 and
A11: p4`1> a and
A12: f.0=p1 and
A13: f.1=p3 and
A14: g.0=p2 and
A15: g.1=p4 and
A16: f is continuous one-to-one and
A17: g is continuous one-to-one and
A18: rng f c= closed_inside_of_rectangle(a,b,c,d) and
A19: rng g c= closed_inside_of_rectangle(a,b,c,d);
set A=2/(b-a), B=-(b+a)/(b-a), C = 2/(d-c), D=-(d+c)/(d-c);
set h=AffineMap(A,B,C,D);
reconsider g2= h*g as Function of I[01],TOP-REAL 2;
A20: g2 is continuous one-to-one by A1,A2,A17,Th53;
A21: (g.O)`2= c by A4,A14;
A22: b>p2`1 by A7,A8,XXREAL_0:2;
p2`1>p4`1 by A9,A10,XXREAL_0:2;
then
A23: ((g2).I)`1> -1 by A1,A11,A14,A15,A22,A21,Th67;
A24: rng (g2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A19,Th52;
A25: ((g2).I)`2= -1 by A2,A6,A15,Th57;
A26: ((g2).O)`2= -1 by A2,A4,A14,Th57;
A27: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A28: h.p2=g2.O by A14,FUNCT_1:13;
A29: h.p4=g2.I by A15,A27,FUNCT_1:13;
d-c >0 by A2,XREAL_1:50;
then
A30: C >0 by XREAL_1:139;
reconsider f2= h*f as Function of I[01],TOP-REAL 2;
A31: f2 is continuous one-to-one by A1,A2,A16,Th53;
A32: rng (f2) c= closed_inside_of_rectangle(-1,1,-1,1) by A1,A2,A18,Th52;
A33: ((f2).I)`2= -1 by A2,A5,A13,Th57;
A34: (f.I)`2= c by A5,A13;
A35: p3`1>a by A10,A11,XXREAL_0:2;
p1`1>p3`1 by A8,A9,XXREAL_0:2;
then
A36: 1 >=((f2).O)`1 by A1,A7,A12,A13,A35,A34,Th67;
A37: ((f2).O)`2= -1 by A2,A3,A12,Th57;
set x = the Element of rng f2 /\ rng g2;
A38: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A39: h.p3=f2.I by A13,FUNCT_1:13;
b-a>0 by A1,XREAL_1:50;
then
A40: A >0 by XREAL_1:139;
then
A41: (h.p1)`1>(h.p2)`1 by A8,A30,Th50;
A42: (h.p3)`1>(h.p4)`1 by A10,A40,A30,Th50;
A43: (h.p2)`1>(h.p3)`1 by A9,A40,A30,Th50;
h.p1=f2.O by A12,A38,FUNCT_1:13;
then f2.O,g2.O,f2.I,g2.I are_in_this_order_on rectangle(-1,1,-1,1) by A41,A43
,A42,A28,A39,A29,A37,A33,A36,A26,A25,A23,Th48;
then rng f2 meets rng g2 by A31,A32,A20,A24,JGRAPH_6:79;
then
A44: rng f2 /\ rng g2 <>{} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being object such that
A45: z2 in dom g2 and
A46: x=g2.z2 by FUNCT_1:def 3;
A47: x=h.(g.z2) by A27,A45,A46,FUNCT_1:13;
h is being_homeomorphism by A40,A30,Th51;
then
A48: h is one-to-one by TOPS_2:def 5;
x in rng f2 by A44,XBOOLE_0:def 4;
then consider z1 being object such that
A49: z1 in dom f2 and
A50: x=f2.z1 by FUNCT_1:def 3;
A51: f.z1 in rng f by A38,A49,FUNCT_1:def 3;
A52: g.z2 in rng g by A27,A45,FUNCT_1:def 3;
g.z2 in the carrier of TOP-REAL 2 by A45,FUNCT_2:5;
then
A53: g.z2 in dom h by FUNCT_2:def 1;
f.z1 in the carrier of TOP-REAL 2 by A49,FUNCT_2:5;
then
A54: f.z1 in dom h by FUNCT_2:def 1;
x=h.(f.z1) by A38,A49,A50,FUNCT_1:13;
then f.z1=g.z2 by A47,A54,A53,A48,FUNCT_1:def 4;
hence thesis by A51,A52,XBOOLE_0:3;
end;
theorem
for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real,
P,Q being Subset of TOP-REAL 2 st a****=p1`1 & p1`1>p2`1 & p2`1>p3`1 & p3`1>p4`1 & p4`1> a & P
is_an_arc_of p1,p3 & Q is_an_arc_of p2,p4 & P c= closed_inside_of_rectangle(a,b
,c,d) & Q c= closed_inside_of_rectangle(a,b,c,d) holds P meets Q
proof
let p1,p2,p3,p4 be Point of TOP-REAL 2, a,b,c,d be Real, P,Q be
Subset of TOP-REAL 2;
assume that
A1: a****=p1`1 and
A8: p1`1>p2`1 and
A9: p2`1>p3`1 and
A10: p3`1>p4`1 and
A11: p4`1> a and
A12: P is_an_arc_of p1,p3 and
A13: Q is_an_arc_of p2,p4 and
A14: P c= closed_inside_of_rectangle(a,b,c,d) and
A15: Q c= closed_inside_of_rectangle(a,b,c,d);
A16: ex g being Function of I[01],TOP-REAL 2 st g is continuous one-to-one
& rng g=Q & g.0=p2 & g.1=p4 by A13,Th2;
ex f being Function of I[01],TOP-REAL 2 st f is continuous one-to-one
& rng f=P & f.0=p1 & f.1=p3 by A12,Th2;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A14,A15,A16,Th136;
end;
**