Copyright (c) 1998 Association of Mizar Users
environ
vocabulary GRAPH_1, FINSEQ_1, ORDERS_1, SQUARE_1, ABSVALUE, ARYTM_1, GRAPH_4,
FUNCT_1, FINSEQ_4, BOOLE, FUNCT_3, RELAT_1, FINSET_1, CARD_1, EUCLID,
TOPREAL1, GOBOARD5, PRE_TOPC, TARSKI, MCART_1, GOBOARD1, GOBOARD4,
COMPLEX1, METRIC_1, RLVECT_1, RVSUM_1, PCOMPS_1, COMPTS_1, WEIERSTR,
NAT_1, ARYTM_3, BORSUK_1, TOPS_2, ORDINAL2, RCOMP_1, TBSP_1, SUBSET_1,
PSCOMP_1, LATTICES, JGRAPH_1, ARYTM;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0,
REAL_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSET_1, CARD_1,
NAT_1, GRAPH_1, STRUCT_0, BINARITH, GRAPH_2, FINSEQ_4, GRAPH_4, TOPREAL1,
GOBOARD5, PRE_TOPC, GOBOARD1, GOBOARD4, TOPMETR, PCOMPS_1, COMPTS_1,
WEIERSTR, TOPS_2, METRIC_1, TBSP_1, RCOMP_1, ABSVALUE, SQUARE_1,
PSCOMP_1, RVSUM_1, TOPRNS_1, EUCLID, FUNCT_3;
constructors REAL_1, BINARITH, GRAPH_2, GRAPH_4, GOBOARD5, GOBOARD4, WEIERSTR,
TOPS_2, TBSP_1, RCOMP_1, ABSVALUE, SQUARE_1, PSCOMP_1, FUNCT_3, FINSEQ_4,
TOPRNS_1, GOBOARD1, JORDAN7;
clusters STRUCT_0, RELSET_1, GRAPH_4, EUCLID, PRE_TOPC, BORSUK_1, XREAL_0,
FINSEQ_1, METRIC_1, ARYTM_3, MEMBERED;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
theorems AXIOMS, TARSKI, FUNCT_1, FINSEQ_1, NAT_1, JORDAN3, ZFMISC_1, REAL_1,
REAL_2, SPPOL_1, FINSEQ_4, CARD_1, FINSET_1, GRAPH_1, GRAPH_2, BINARITH,
FUNCT_3, RELAT_1, GRAPH_4, FINSEQ_3, TOPREAL1, GOBOARD1, GOBOARD5,
GOBOARD4, TOPREAL3, SQUARE_1, EUCLID, JORDAN7, UNIFORM1, WEIERSTR,
JORDAN5A, TOPS_2, PRE_TOPC, TBSP_1, HEINE, COMPTS_1, TOPMETR, PSCOMP_1,
TOPREAL5, BORSUK_1, RCOMP_1, ABSVALUE, METRIC_1, RVSUM_1, FINSEQ_2,
FUNCT_2, GROUP_4, SCMFSA_7, JORDAN6, XBOOLE_0, XBOOLE_1, TOPRNS_1,
JORDAN1, XCMPLX_0, XCMPLX_1;
schemes FINSEQ_1;
begin :: GRAPHS BY CARTESIAN PRODUCT
reserve x,y for set;
reserve G for Graph;
reserve vs,vs' for FinSequence of the Vertices of G;
reserve IT for oriented Chain of G;
reserve n,m,k,i,j for Nat;
reserve r,r1,r2 for Real;
canceled;
theorem Th2: sqrt(r1^2+r2^2)<=abs(r1)+abs(r2)
proof
A1: r1^2>=0 by SQUARE_1:72;
r2^2>=0 by SQUARE_1:72;
then r1^2+r2^2>=0+0 by A1,REAL_1:55;
then A2:(sqrt(r1^2+r2^2))^2=r1^2+r2^2 by SQUARE_1:def 4;
A3:(abs(r1)+abs(r2))^2=(abs(r1))^2+2*(abs(r1))*(abs(r2))+(abs(r2))^2
by SQUARE_1:63;
(abs(r1))^2=r1^2 by SQUARE_1:62;
then A4:(abs(r1)+abs(r2))^2 - (sqrt(r1^2+r2^2))^2=
r1^2+2*(abs(r1))*(abs(r2))+r2^2-(r1^2+r2^2) by A2,A3,SQUARE_1:62
.=2*(abs(r1))*(abs(r2))+r1^2+r2^2-r1^2-r2^2 by XCMPLX_1:36
.=2*(abs(r1))*(abs(r2))+r2^2+r1^2-r1^2-r2^2 by XCMPLX_1:1
.=2*(abs(r1))*(abs(r2))+r2^2-r2^2 by XCMPLX_1:26
.=2*(abs(r1))*(abs(r2)) by XCMPLX_1:26;
A5:abs(r1)>=0 by ABSVALUE:5;
then A6: 2*abs(r1)>=0 by SQUARE_1:19;
A7:abs(r2)>=0 by ABSVALUE:5;
then 2*abs(r1)*abs(r2)>=0 by A6,SQUARE_1:19;
then A8:(abs(r1)+abs(r2))^2>= (sqrt(r1^2+r2^2))^2 by A4,REAL_2:105;
(sqrt(r1^2+r2^2))^2>=0 by SQUARE_1:72;
then A9:sqrt((abs(r1)+abs(r2))^2)>=sqrt((sqrt(r1^2+r2^2))^2) by A8,SQUARE_1:
94;
abs(r1)+abs(r2)>=0+0 by A5,A7,REAL_1:55;
hence thesis by A2,A9,SQUARE_1:89;
end;
theorem Th3: abs(r1)<=sqrt(r1^2+r2^2) & abs(r2)<=sqrt(r1^2+r2^2)
proof
A1: r1^2>=0 by SQUARE_1:72;
A2:r2^2>=0 by SQUARE_1:72;
then r1^2+0<= r1^2+r2^2 by AXIOMS:24;
then sqrt(r1^2)<= sqrt(r1^2+r2^2) by A1,SQUARE_1:94;
hence abs(r1)<= sqrt(r1^2+r2^2) by SQUARE_1:91;
0+r2^2<= r1^2+r2^2 by A1,REAL_1:55;
then sqrt(r2^2)<= sqrt(r1^2+r2^2) by A2,SQUARE_1:94;
hence thesis by SQUARE_1:91;
end;
theorem Th4: for vs st IT is Simple & vs is_oriented_vertex_seq_of IT
holds for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs
proof let vs;assume A1:IT is Simple & vs is_oriented_vertex_seq_of IT;
then consider vs' such that A2: vs' is_oriented_vertex_seq_of IT &
(for n,m st 1<=n & n<m & m<=len vs' & vs'.n=vs'.m holds n=1 & m=len vs')
by GRAPH_4:def 7;
A3:len vs = len IT + 1 &
for n st 1<=n & n<=len IT holds IT.n orientedly_joins vs/.n, vs/.(n+1)
by A1,GRAPH_4:def 5;
per cases;
suppose IT<> {};
then vs=vs' by A1,A2,GRAPH_4:11;
hence thesis by A2;
suppose IT= {}; then len IT=0 by FINSEQ_1:25;
hence thesis by A3,AXIOMS:22;
end;
definition let X be set;
func PGraph(X) -> MultiGraphStruct equals
:Def1: MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#);
coherence;
end;
theorem Th5:for X being non empty set holds PGraph(X) is Graph
proof let X be non empty set;
PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#) by Def1;
hence thesis by GRAPH_1:def 1;
end;
theorem Th6:for X being set holds the Vertices of PGraph(X)=X
proof let X be set;
PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#) by Def1;
hence thesis;
end;
definition let f be FinSequence;
func PairF(f) -> FinSequence means
:Def2: len it=len f-'1 &
for i being Nat st 1<=i & i<len f holds it.i=[f.i,f.(i+1)];
existence
proof
deffunc F(Nat)=[f.$1,f.($1+1)];
ex p being FinSequence st len p = len f-'1
& for k being Nat st k in Seg (len f-'1) holds p.k=F(k)
from SeqLambda;
then consider p being FinSequence such that A1: len p = len f-'1
& for k being Nat st k in Seg (len f-'1) holds p.k=[f.k,f.(k+1)];
for i being Nat st 1<=i & i<len f holds p.i=[f.i,f.(i+1)]
proof let i be Nat;assume A2:1<=i & i<len f;
then len f>1 by AXIOMS:22;
then A3:len f-1=len f-'1 by SCMFSA_7:3;
i+1<=len f by A2,NAT_1:38;
then i+1-1<=len f-1 by REAL_1:49;
then i<=len f-'1 by A3,XCMPLX_1:26;
then i in Seg (len f-'1) by A2,FINSEQ_1:3;
hence thesis by A1;
end;
hence thesis by A1;
end;
uniqueness
proof let g1,g2 be FinSequence;
assume A4:(len g1=len f-'1 &
for i being Nat st 1<=i & i<len f holds g1.i=[f.i,f.(i+1)])&
(len g2=len f-'1 &
for i being Nat st 1<=i & i<len f holds g2.i=[f.i,f.(i+1)]);
per cases;
suppose A5:len f>=1;
for j being Nat st 1<=j & j<=len g1 holds g1.j=g2.j
proof let j be Nat;assume A6:1<=j & j<=len g1;
len f<len f+1 by NAT_1:38;
then len f-1<len f by REAL_1:84;
then len g1<len f by A4,A5,SCMFSA_7:3;
then A7:j<len f by A6,AXIOMS:22;
then g1.j=[f.j,f.(j+1)] by A4,A6;
hence thesis by A4,A6,A7;
end;
hence thesis by A4,FINSEQ_1:18;
suppose len f<1; then len f+1<=1 by NAT_1:38;
then len f+1-1<=1-1 by REAL_1:49;
then len f<=0 by XCMPLX_1:26; then A8:len f=0 by NAT_1:18; 0-1<0;
then A9:len g1=0 & len g2=0 by A4,A8,BINARITH:def 3;
then g1= {} by FINSEQ_1:25;
hence thesis by A9,FINSEQ_1:25;
end;
end;
reserve X for non empty set;
definition let X be non empty set;
cluster PGraph(X) -> Graph-like;
coherence by Th5;
end;
theorem Th7:for f being FinSequence of X
holds f is FinSequence of the Vertices of PGraph(X)
proof let f be FinSequence of X;
PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#) by Def1;
hence thesis;
end;
theorem Th8:for f being FinSequence of X
holds PairF(f) is FinSequence of the Edges of PGraph(X)
proof let f be FinSequence of X;
A1:rng PairF(f) c= [:X,X:]
proof let y be set;assume y in rng PairF(f);
then consider x being set such that
A2:x in dom PairF(f) & y=(PairF(f)).x by FUNCT_1:def 5;
A3:x in Seg len PairF(f) by A2,FINSEQ_1:def 3;
reconsider n=x as Nat by A2;
A4:1<=n & n<=len PairF(f) by A3,FINSEQ_1:3;
A5:len PairF(f)=len f-'1 by Def2;
then 1<=len f-'1 by A4,AXIOMS:22;
then A6:len f-'1=len f-1 by JORDAN3:1;
len f-'1<len f-'1+1 by NAT_1:38;
then len f-'1<len f by A6,XCMPLX_1:27;
then A7:n<len f by A4,A5,AXIOMS:22;
then A8:(PairF(f)).n =[f.n,f.(n+1)] by A4,Def2;
A9:rng f c= X by FINSEQ_1:def 4;
n in dom f by A4,A7,FINSEQ_3:27;
then A10: f.n in rng f by FUNCT_1:def 5;
A11:1<n+1 by A4,NAT_1:38;
n+1<=len f by A7,NAT_1:38;
then n+1 in dom f by A11,FINSEQ_3:27;
then f.(n+1) in rng f by FUNCT_1:def 5;
hence y in [:X,X:] by A2,A8,A9,A10,ZFMISC_1:def 2;
end;
PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#) by Def1;
hence thesis by A1,FINSEQ_1:def 4;
end;
definition let X be non empty set,f be FinSequence of X;
redefine func PairF(f) -> FinSequence of the Edges of PGraph(X);
coherence by Th8;
end;
theorem Th9:for n being Nat,f being FinSequence of X
st 1 <= n & n <= len PairF(f) holds
(PairF(f)).n in the Edges of PGraph(X)
proof let n be Nat,f be FinSequence of X;
assume A1:1 <= n & n <= len PairF(f);
A2:len PairF(f)=len f-'1 by Def2;
then 1<=len f-'1 by A1,AXIOMS:22;
then A3:len f-'1=len f-1 by JORDAN3:1;
len f-'1<len f-'1+1 by NAT_1:38;
then len f-'1<len f by A3,XCMPLX_1:27;
then A4:n<len f by A1,A2,AXIOMS:22;
then A5:(PairF(f)).n =[f.n,f.(n+1)] by A1,Def2;
A6:rng f c= X by FINSEQ_1:def 4;
n in dom f by A1,A4,FINSEQ_3:27;
then A7:f.n in rng f by FUNCT_1:def 5;
A8:1<n+1 by A1,NAT_1:38;
n+1<=len f by A4,NAT_1:38;
then n+1 in dom f by A8,FINSEQ_3:27;
then A9:f.(n+1) in rng f by FUNCT_1:def 5;
PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#) by Def1;
hence thesis by A5,A6,A7,A9,ZFMISC_1:def 2;
end;
theorem Th10:for f being FinSequence of X holds
PairF(f) is oriented Chain of PGraph(X)
proof let f be FinSequence of X;
A1: now per cases;
case len f>=1;
then len f-1+1=len f-'1+1 by SCMFSA_7:3;
then len f=len f-'1+1 by XCMPLX_1:27;
then A2:len f = len PairF(f) + 1 by Def2;
A3:for n st 1 <= n & n <= len f holds f.n in the Vertices of PGraph(X)
proof let n;assume
A4:1 <= n & n <= len f;
A5:rng f c= X by FINSEQ_1:def 4;
n in dom f by A4,FINSEQ_3:27;
then A6: f.n in rng f by FUNCT_1:def 5;
PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#) by Def1;
hence thesis by A5,A6;
end;
for n st 1 <= n & n <= len PairF(f)
ex x', y' being Element of the Vertices of PGraph(X) st
x' = f.n & y' = f.(n+1) & (PairF(f)).n joins x', y'
proof let n;assume A7:1 <= n & n <= len PairF(f);
A8:len PairF(f)=len f-'1 by Def2;
then 1<=len f-'1 by A7,AXIOMS:22;
then A9:len f-'1=len f-1 by JORDAN3:1;
len f-'1<len f-'1+1 by NAT_1:38;
then len f-'1<len f by A9,XCMPLX_1:27;
then A10:n<len f by A7,A8,AXIOMS:22;
A11:rng f c= X by FINSEQ_1:def 4;
n in dom f by A7,A10,FINSEQ_3:27;
then A12: f.n in rng f by FUNCT_1:def 5;
A13:1<n+1 by A7,NAT_1:38;
n+1<=len f by A10,NAT_1:38;
then n+1 in dom f by A13,FINSEQ_3:27;
then A14: f.(n+1) in rng f by FUNCT_1:def 5;
A15:PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#) by Def1;
then reconsider a=f.n,b=f.(n+1) as Element of the Vertices of PGraph(X
)
by A11,A12,A14;
A16:(pr1(X,X)).([f.n,f.(n+1)])=f.n by A11,A12,A14,FUNCT_3:def 5;
(pr2(X,X)).([f.n,f.(n+1)])=f.(n+1)
by A11,A12,A14,FUNCT_3:def 6;
then ((the Source of PGraph(X)).((PairF(f)).n) = a
& (the Target of PGraph(X)).((PairF(f)).n) = b)
by A7,A10,A15,A16,Def2;
then (PairF(f)).n joins a, b by GRAPH_1:def 9;
hence thesis;
end;
then (for n st 1 <= n & n <= len PairF(f) holds
(PairF(f)).n in the Edges of PGraph(X)) &
ex p being FinSequence st
len p = len PairF(f) + 1 &
(for n st 1 <= n & n <= len p holds p.n in the Vertices of PGraph(X)) &
for n st 1 <= n & n <= len PairF(f)
ex x', y' being Element of the Vertices of PGraph(X) st
x' = p.n & y' = p.(n+1) & (PairF(f)).n joins x', y' by A2,A3,Th9;
hence PairF(f) is Chain of PGraph(X) by GRAPH_1:def 11;
case len f<1;
then len f+1<=1 by NAT_1:38;
then len f+1-1<=1-1 by REAL_1:49;
then len f<=0 by XCMPLX_1:26; then A17:len f=0 by NAT_1:18; 0-1<0;
then len f-'1=0 by A17,BINARITH:def 3;
then len PairF(f)=0 by Def2;
then PairF(f)= {} by FINSEQ_1:25;
hence PairF(f) is oriented Chain of PGraph(X) by GRAPH_1:14;
end;
for n st 1 <= n & n < len PairF(f) holds
(the Source of PGraph(X)).((PairF(f)).(n+1))
= (the Target of PGraph(X)).((PairF(f)).n)
proof let n;assume A18:1 <= n & n < len PairF(f);
then A19:n+1<=len PairF(f) by NAT_1:38;
A20:len PairF(f)=len f-'1 by Def2;
then 1<=len f-'1 by A18,AXIOMS:22;
then A21:len f-'1=len f-1 by JORDAN3:1;
len f-'1<len f-'1+1 by NAT_1:38;
then A22:len f-'1<len f by A21,XCMPLX_1:27;
then A23:n<len f by A18,A20,AXIOMS:22;
A24:n+1<len f by A19,A20,A22,AXIOMS:22;
A25:rng f c= X by FINSEQ_1:def 4;
n in dom f by A18,A23,FINSEQ_3:27;
then A26: f.n in rng f by FUNCT_1:def 5;
A27:1<n+1 by A18,NAT_1:38;
n+1<=len f by A23,NAT_1:38;
then n+1 in dom f by A27,FINSEQ_3:27;
then A28: f.(n+1) in rng f by FUNCT_1:def 5;
A29:PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#)
by Def1;
then reconsider a=f.n,b=f.(n+1) as Element of the Vertices of PGraph(X)
by A25,A26,A28;
A30:(pr1(X,X)).([f.n,f.(n+1)])=f.n by A25,A26,A28,FUNCT_3:def 5;
(pr2(X,X)).([f.n,f.(n+1)])=f.(n+1) by A25,A26,A28,FUNCT_3:def 6;
then A31:((the Source of PGraph(X)).((PairF(f)).n) = a
& (the Target of PGraph(X)).((PairF(f)).n) = b)
by A18,A23,A29,A30,Def2;
A32:rng f c= X by FINSEQ_1:def 4;
n+1 in dom f by A24,A27,FINSEQ_3:27;
then A33: f.(n+1) in rng f by FUNCT_1:def 5;
A34:1<n+1+1 by A27,NAT_1:38;
n+1+1<=len f by A24,NAT_1:38;
then n+1+1 in dom f by A34,FINSEQ_3:27;
then A35: f.(n+1+1) in rng f by FUNCT_1:def 5;
A36:PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#) by Def1;
(pr1(X,X)).([f.(n+1),f.((n+1)+1)])=f.(n+1)
by A32,A33,A35,FUNCT_3:def 5;
hence thesis by A24,A27,A31,A36,Def2;
end;
hence thesis by A1,GRAPH_1:def 12;
end;
definition let X be non empty set,f be FinSequence of X;
redefine func PairF(f) -> oriented Chain of PGraph(X);
coherence by Th10;
end;
theorem Th11:for f being FinSequence of X,
f1 being FinSequence of the Vertices of PGraph(X) st len f>=1 & f=f1 holds
f1 is_oriented_vertex_seq_of PairF(f)
proof let f be FinSequence of X,
f1 be FinSequence of the Vertices of PGraph(X);
assume A1:len f>=1 & f=f1;
then len f-'1=len f-1 by SCMFSA_7:3;
then len f-1+1=len PairF(f)+1 by Def2;
then A2:len f1=len PairF(f)+1 by A1,XCMPLX_1:27;
for n st 1<=n & n<=len PairF(f) holds
((PairF(f)).n) orientedly_joins f1/.n, f1/.(n+1)
proof let n;assume A3: 1<=n & n<=len PairF(f);
A4:len PairF(f)=len f-'1 by Def2;
then 1<=len f-'1 by A3,AXIOMS:22;
then A5:len f-'1=len f-1 by JORDAN3:1;
len f-'1<len f-'1+1 by NAT_1:38;
then len f-'1<len f by A5,XCMPLX_1:27;
then A6:n<len f by A3,A4,AXIOMS:22;
A7:rng f c= X by FINSEQ_1:def 4;
A8:n in dom f by A3,A6,FINSEQ_3:27;
then A9: f.n in rng f by FUNCT_1:def 5;
A10:1<n+1 by A3,NAT_1:38;
n+1<=len f by A6,NAT_1:38;
then A11:n+1 in dom f by A10,FINSEQ_3:27;
then A12: f.(n+1) in rng f by FUNCT_1:def 5;
A13:PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#)
by Def1;
A14:f1/.n=f1.n by A1,A8,FINSEQ_4:def 4;
A15:f1/.(n+1)=f1.(n+1) by A1,A11,FINSEQ_4:def 4;
A16:(pr1(X,X)).([f.n,f.(n+1)])=f.n by A7,A9,A12,FUNCT_3:def 5;
(pr2(X,X)).([f.n,f.(n+1)])=f.(n+1) by A7,A9,A12,FUNCT_3:def 6;
then (the Source of PGraph(X)).((PairF(f)).n) = f1/.n
& (the Target of PGraph(X)).((PairF(f)).n) = f1/.(n+1)
by A1,A3,A6,A13,A14,A15,A16,Def2;
hence thesis by GRAPH_4:def 1;
end;
hence thesis by A2,GRAPH_4:def 5;
end;
begin :: SHORTCUTS OF FINITE SEQUENCES IN PLANE
definition let X be non empty set,f,g be FinSequence of X;
pred g is_Shortcut_of f means
:Def3: f.1=g.1 & f.len f=g.len g &
ex fc being FinSubsequence of PairF(f),fvs being FinSubsequence of f,
sc being oriented simple Chain of PGraph(X),
g1 being FinSequence of the Vertices of PGraph(X)
st Seq fc = sc & Seq fvs = g & g1=g
& g1 is_oriented_vertex_seq_of sc;
end;
theorem Th12:for f,g being FinSequence of X st g is_Shortcut_of f holds
1<=len g & len g <= len f
proof let f,g be FinSequence of X;assume
g is_Shortcut_of f;
then consider fc being FinSubsequence of PairF(f),fvs being FinSubsequence of
f,
sc being oriented simple Chain of PGraph(X),
g1 being FinSequence of the Vertices of PGraph(X)
such that A1:Seq fc = sc & Seq fvs = g & g1=g
& g1 is_oriented_vertex_seq_of sc by Def3;
A2:len g1 = len sc + 1 by A1,GRAPH_4:def 5;
fvs c= f by GRAPH_2:def 5;
then A3:dom fvs c= dom f by RELAT_1:25;
A4:g=fvs*Sgm(dom fvs) by A1,FINSEQ_1:def 14;
rng Sgm(dom fvs) c= dom fvs by FINSEQ_1:71;
then A5:dom g=dom (Sgm(dom fvs)) by A4,RELAT_1:46;
A6:Seg len f is finite set;
then dom f is finite set by FINSEQ_1:def 3;
then reconsider dfvs=dom fvs as finite set by A3,FINSET_1:13;
reconsider df=dom f as finite set by A6,FINSEQ_1:def 3;
A7:dom fvs c=Seg len f by A3,FINSEQ_1:def 3;
A8:len g=len Sgm(dom fvs) by A5,FINSEQ_3:31
.=card dfvs by A7,FINSEQ_3:44;
card df=card (Seg len f) by FINSEQ_1:def 3 .=len f by FINSEQ_1:78;
hence thesis by A1,A2,A3,A8,CARD_1:80,NAT_1:37;
end;
theorem Th13:for f being FinSequence of X st len f>=1 holds
ex g being FinSequence of X st g is_Shortcut_of f
proof let f be FinSequence of X;assume A1: len f>=1;
reconsider f1=f as FinSequence of the Vertices of PGraph(X) by Th7;
f1 is_oriented_vertex_seq_of PairF(f) by A1,Th11;
then consider fc being FinSubsequence of PairF(f),
fvs being FinSubsequence of f1, sc being oriented simple Chain of PGraph(X),
vs1 being FinSequence of the Vertices of PGraph(X)
such that A2: Seq fc = sc & Seq fvs = vs1
& vs1 is_oriented_vertex_seq_of sc &
f1.1 = vs1.1 & f1.len f1 = vs1.len vs1 by GRAPH_4:23;
A3:PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#)
by Def1;
then reconsider g1=vs1 as FinSequence of X;
g1 is_Shortcut_of f by A2,A3,Def3;
hence thesis;
end;
theorem Th14:for f,g being FinSequence of X st
g is_Shortcut_of f holds rng PairF(g) c= rng PairF(f)
proof let f,g be FinSequence of X;assume
g is_Shortcut_of f;
then consider fc being FinSubsequence of PairF(f),
fvs being FinSubsequence of f,
sc being oriented simple Chain of PGraph(X),
g1 being FinSequence of the Vertices of PGraph(X)
such that
A1:Seq fc = sc & Seq fvs = g & g1=g & g1 is_oriented_vertex_seq_of sc
by Def3;
let y be set;assume y in rng PairF(g);
then consider x being set such that
A2: x in dom PairF(g) & y=(PairF(g)).x by FUNCT_1:def 5;
A3:x in Seg len PairF(g) by A2,FINSEQ_1:def 3;
reconsider n=x as Nat by A2;
A4:1<=n & n<=len PairF(g) by A3,FINSEQ_1:3;
A5:len PairF(g)=len g-'1 by Def2;
1<=len PairF(g) by A4,AXIOMS:22;
then A6:len g-'1=len g-1 by A5,JORDAN3:1;
len g<len g+1 by NAT_1:38;
then len g-1<len g by REAL_1:84;
then A7:n<len g by A4,A5,A6,AXIOMS:22;
then A8:(PairF(g)).x=[g.n,g.(n+1)] by A4,Def2;
A9:n+1<=len g by A7,NAT_1:38;
A10:fc* Sgm(dom fc)=sc by A1,FINSEQ_1:def 14;
rng Sgm(dom fc) = dom fc by FINSEQ_1:71;
then A11:rng fc = rng sc by A10,RELAT_1:47;
fc c= PairF(f) by GRAPH_2:def 5;
then A12:rng sc c= rng PairF(f) by A11,RELAT_1:25;
n+1<=len sc+1 by A1,A9,GRAPH_4:def 5;
then A13:n<=len sc by REAL_1:53;
then A14: (sc.n) orientedly_joins g1/.n, g1/.(n+1) by A1,A4,GRAPH_4:def 5;
n in dom sc by A4,A13,FINSEQ_3:27;
then sc.n in rng sc by FUNCT_1:def 5;
then consider z being set such that
A15: z in dom PairF(f) & (PairF(f)).z=sc.n by A12,FUNCT_1:def 5;
A16:z in Seg len PairF(f) by A15,FINSEQ_1:def 3;
reconsider m=z as Nat by A15;
A17: 1<=m & m<=len PairF(f) by A16,FINSEQ_1:3;
then A18:1<=m & m<=len f -'1 by Def2;
then 1<=len f-'1 by AXIOMS:22;
then A19:len f-'1=len f-1 by JORDAN3:1;
len f<len f+1 by NAT_1:38;
then len f-1<len f by REAL_1:84;
then A20:1<=m & m<len f by A18,A19,AXIOMS:22;
then A21:[f.m,f.(m+1)]=sc.n by A15,Def2;
m in dom f by A20,FINSEQ_3:27;
then A22:f.m in rng f by FUNCT_1:def 5;
A23:1<m+1 by A17,NAT_1:38;
m+1<=len f by A20,NAT_1:38;
then m+1 in dom f by A23,FINSEQ_3:27;
then A24:f.(m+1) in rng f by FUNCT_1:def 5;
A25: rng f c= X by FINSEQ_1:def 4;
A26:PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#)
by Def1;
then A27:(the Source of PGraph(X)).(sc.n)= f.m by A21,A22,A24,A25,FUNCT_3:
def 5;
(the Target of PGraph(X)).(sc.n)= f.(m+1) by A21,A22,A24,A25,A26,FUNCT_3:
def 6;
then A28:g1/.n=f.m & g1/.(n+1)=f.(m+1) by A14,A27,GRAPH_4:def 1;
1<=n+1 & n+1<=len g1 by A1,A4,A7,NAT_1:38;
then g.n=f.m & g.(n+1)=f.(m+1) by A1,A4,A7,A28,FINSEQ_4:24;
hence thesis by A2,A8,A15,A21,FUNCT_1:def 5;
end;
theorem Th15:for f,g being FinSequence of X st f.1<>f.len f &
g is_Shortcut_of f holds g is one-to-one & rng PairF(g) c= rng PairF(f)
& g.1=f.1 & g.len g=f.len f
proof let f,g be FinSequence of X;
assume A1:f.1<>f.len f & g is_Shortcut_of f;
then A2: f.1=g.1 & f.len f=g.len g &
ex fc being FinSubsequence of PairF(f),fvs being FinSubsequence of f,
sc being oriented simple Chain of PGraph(X),
g1 being FinSequence of the Vertices of PGraph(X)
st Seq fc = sc & Seq fvs = g & g1=g
& g1 is_oriented_vertex_seq_of sc by Def3;
consider fc being FinSubsequence of PairF(f),
fvs being FinSubsequence of f,
sc being oriented simple Chain of PGraph(X),
g1 being FinSequence of the Vertices of PGraph(X)
such that
A3:Seq fc = sc & Seq fvs = g & g1=g & g1 is_oriented_vertex_seq_of sc
by A1,Def3;
sc is Simple by GRAPH_4:20;
then consider vs being FinSequence of the Vertices of PGraph(X)
such that A4: vs is_oriented_vertex_seq_of sc &
(for n,m being Nat st 1<=n & n<m & m<=len vs & vs.n=vs.m
holds n=1 & m=len vs) by GRAPH_4:def 7;
A5:len g1 = len sc + 1 &
for n st 1<=n & n<=len sc holds sc.n orientedly_joins g1/.n,g1/.(n+1)
by A3,GRAPH_4:def 5;
then 1<=len g1 by NAT_1:29;
then 1<len g1 by A1,A2,A3,REAL_1:def 5;
then len sc>=1 by A5,NAT_1:38;
then len sc>0 by AXIOMS:22;
then sc<> {} by FINSEQ_1:25;
then A6:g1=vs by A3,A4,GRAPH_4:11;
for x,y being set st x in dom g & y in dom g & g.x=g.y holds x=y
proof let x,y be set;assume
A7: x in dom g & y in dom g & g.x=g.y;
then A8:x in Seg len g by FINSEQ_1:def 3;
reconsider i1=x as Nat by A7;
A9:y in Seg len g by A7,FINSEQ_1:def 3;
reconsider i2=y as Nat by A7;
A10:1<=i1 & i1<=len g by A8,FINSEQ_1:3;
A11:1<=i2 & i2<=len g by A9,FINSEQ_1:3;
now assume A12:x<>y;
per cases;
suppose i1<=i2;
then i1<i2 by A12,REAL_1:def 5;
then i1=1 & i2=len g by A3,A4,A6,A7,A10,A11;
hence contradiction by A1,A2,A7;
suppose i1>i2;
then i2=1 & i1=len g by A3,A4,A6,A7,A10,A11;
hence contradiction by A1,A2,A7;
end;
hence x=y;
end;
hence g is one-to-one by FUNCT_1:def 8;
thus rng PairF(g) c= rng PairF(f) by A1,Th14;
thus thesis by A1,Def3;
end;
definition let n; let IT be FinSequence of TOP-REAL n;
attr IT is nodic means
:Def4: for i,j st LSeg(IT,i) meets LSeg(IT,j)
holds LSeg(IT,i) /\ LSeg(IT,j)={IT.i}
&(IT.i=IT.j or IT.i=IT.(j+1)) or
LSeg(IT,i) /\ LSeg(IT,j)={IT.(i+1)}
&(IT.(i+1)=IT.j or IT.(i+1)=IT.(j+1)) or
LSeg(IT,i)=LSeg(IT,j);
end;
theorem for f being FinSequence of TOP-REAL 2 st f is s.n.c.
holds f is s.c.c.
proof let f be FinSequence of TOP-REAL 2;
assume f is s.n.c.;
then for i,j st i+1 < j & (i > 1 & j < len f or j+1 < len f)
holds LSeg(f,i) misses LSeg(f,j) by TOPREAL1:def 9;
hence thesis by GOBOARD5:def 4;
end;
theorem Th17:for f being FinSequence of TOP-REAL 2 st f is s.c.c. &
LSeg(f,1) misses LSeg(f,len f -'1) holds f is s.n.c.
proof let f be FinSequence of TOP-REAL 2;
assume A1:f is s.c.c. & LSeg(f,1) misses LSeg(f,len f -'1);
for i,j st i+1 < j holds LSeg(f,i) misses LSeg(f,j)
proof let i,j;assume A2:i+1 < j;
per cases;
suppose len f<>0; then len f>0 by NAT_1:19;
then A3: len f>=0+1 by NAT_1:38;
now per cases;
case A4:1<=i & j+1<=len f;
then A5:j<len f by NAT_1:38;
now per cases;
case A6:i=1 & j+1=len f;
then j=len f-1 by XCMPLX_1:26;
then LSeg(f,i) misses LSeg(f,j) by A1,A3,A6,SCMFSA_7:3;
hence LSeg(f,i) /\ LSeg(f,j) = {} by XBOOLE_0:def 7;
case not(i=1 & j+1=len f);
then i>1 or j+1<len f by A4,REAL_1:def 5;
then LSeg(f,i) misses LSeg(f,j) by A1,A2,A5,GOBOARD5:def 4;
hence LSeg(f,i) /\ LSeg(f,j) = {} by XBOOLE_0:def 7;
end;
hence LSeg(f,i) /\ LSeg(f,j) = {};
case A7:not (1<=i & j+1<=len f);
now per cases by A7;
case 1>i;
then LSeg(f,i)={} by TOPREAL1:def 5;
hence LSeg(f,i) /\ LSeg(f,j) = {};
case j+1>len f;
then LSeg(f,j)={} by TOPREAL1:def 5;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
hence thesis by XBOOLE_0:def 7;
suppose A8:len f=0;
now per cases;
case i>=1; then i>len f by A8,AXIOMS:22;
then i+1>len f by NAT_1:38;
then LSeg(f,i)={} by TOPREAL1:def 5;
hence LSeg(f,i) /\ LSeg(f,j) = {};
case i<1;
then LSeg(f,i)={} by TOPREAL1:def 5;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
hence thesis by XBOOLE_0:def 7;
end;
hence thesis by TOPREAL1:def 9;
end;
theorem Th18: for f being FinSequence of TOP-REAL 2 st
f is nodic & PairF(f) is Simple holds f is s.c.c.
proof let f be FinSequence of TOP-REAL 2;
assume A1:f is nodic & PairF(f) is Simple;
reconsider f1=f as
FinSequence of the Vertices of PGraph(the carrier of TOP-REAL 2) by Th6;
per cases;
suppose len f>=1;
then A2:f1 is_oriented_vertex_seq_of PairF(f) by Th11;
for i,j st i+1 < j & (i > 1 & j < len f or j+1 < len f)
holds LSeg(f,i) misses LSeg(f,j)
proof let i,j;assume A3:i+1 < j & (i > 1 & j < len f or j+1 < len f);
per cases;
suppose A4:i>=1;
A5:i<j by A3,NAT_1:38;
A6:i+1<j+1 by A3,NAT_1:38;
A7:1<=j by A4,A5,AXIOMS:22;
A8:j<len f by A3,NAT_1:38;
then A9: i+1<len f by A3,AXIOMS:22;
A10:i<j+1 by A5,NAT_1:38;
A11: j+1<=len f by A3,NAT_1:38;
then A12:i<len f by A10,AXIOMS:22;
A13:1<i+1 by A4,NAT_1:38;
A14:1<j+1 by A7,NAT_1:38;
now assume A15:LSeg(f,i) meets LSeg(f,j);
now per cases by A1,A15,Def4;
case A16:LSeg(f,i) /\ LSeg(f,j)={f.i}
&(f.i=f.j or f.i=f.(j+1))& LSeg(f,i)<>LSeg(f,j);
now per cases by A16;
case f.i=f.j;
hence contradiction by A1,A2,A4,A5,A8,Th4;
case f.i=f.(j+1);
hence contradiction by A1,A2,A3,A4,A10,A11,Th4;
end;
hence contradiction;
case A17:LSeg(f,i) /\ LSeg(f,j)={f.(i+1)}
&(f.(i+1)=f.j or f.(i+1)=f.(j+1))&LSeg(f,i)<>LSeg(f,j);
now per cases by A17;
case f.(i+1)=f.j;
hence contradiction by A1,A2,A3,A8,A13,Th4;
case f.(i+1)=f.(j+1);
hence contradiction by A1,A2,A6,A11,A13,Th4;
end;
hence contradiction;
case LSeg(f,i)=LSeg(f,j);
then LSeg(f/.i,f/.(i+1))=LSeg(f,j) by A4,A9,TOPREAL1:def 5;
then A18: LSeg(f/.i,f/.(i+1))=LSeg(f/.j,f/.(j+1))
by A7,A11,TOPREAL1:def 5;
A19:f/.i=f.i by A4,A12,FINSEQ_4:24;
A20:f/.(i+1)=f.(i+1) by A9,A13,FINSEQ_4:24;
A21:f/.j=f.j by A7,A8,FINSEQ_4:24;
A22:f/.(j+1)=f.(j+1) by A11,A14,FINSEQ_4:24;
now per cases by A18,A19,A20,A21,A22,SPPOL_1:25;
case f.i=f.j & f.(i+1)=f.(j+1);
hence contradiction by A1,A2,A6,A11,A13,Th4;
case f.i=f.(j+1) & f.(i+1)=f.j;
hence contradiction by A1,A2,A3,A8,A13,Th4;
end;
hence contradiction;
end;
hence contradiction;
end;
hence thesis;
suppose i<1;
then LSeg(f,i)={} by TOPREAL1:def 5;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis by XBOOLE_0:def 7;
end;
hence thesis by GOBOARD5:def 4;
suppose A23:len f<1;
for i,j st i+1 < j & (i > 1 & j < len f or j+1 < len f)
holds LSeg(f,i) misses LSeg(f,j)
proof let i,j;assume i+1 < j & (i > 1 & j < len f or j+1 < len f);
per cases;
suppose i>=1; then i>len f by A23,AXIOMS:22;
then i+1>len f by NAT_1:38;
then LSeg(f,i)={} by TOPREAL1:def 5;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis by XBOOLE_0:def 7;
suppose i<1;
then LSeg(f,i)={} by TOPREAL1:def 5;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis by XBOOLE_0:def 7;
end;
hence thesis by GOBOARD5:def 4;
end;
theorem Th19:for f being FinSequence of TOP-REAL 2 st
f is nodic & PairF(f) is Simple & f.1<>f.len f holds f is s.n.c.
proof let f be FinSequence of TOP-REAL 2;
assume A1:f is nodic & PairF(f) is Simple & f.1<>f.len f;
then A2:f is s.c.c. by Th18;
reconsider f1=f as
FinSequence of the Vertices of PGraph(the carrier of TOP-REAL 2) by Th6;
A3:len f-'1<=len f by JORDAN3:7;
per cases;
suppose A4:len f-'1>2;
then A5:len f-'1>1 by AXIOMS:22;
then A6:1<len f by JORDAN3:7;
len f>=1 by A5,JORDAN3:7;
then A7:f1 is_oriented_vertex_seq_of PairF(f) by Th11;
A8:1+1<len f by A4,JORDAN3:7;
A9:len f-'1=len f-1 by A5,JORDAN3:1;
then A10:(len f-'1)+1=len f by XCMPLX_1:27;
now assume
A11: LSeg(f,1) meets LSeg(f,len f-'1);
now per cases by A1,A11,Def4;
case LSeg(f,1) /\ LSeg(f,(len f-'1))={f.1}
&(f.1=f.(len f-'1) or f.1=f.((len f-'1)+1));
hence contradiction by A1,A3,A5,A7,A9,Th4,XCMPLX_1:27;
case A12:LSeg(f,1) /\ LSeg(f,(len f-'1))={f.(1+1)}
&(f.(1+1)=f.(len f-'1) or f.(1+1)=f.((len f-'1)+1));
now per cases by A12;
case f.(1+1)=f.(len f-'1);
hence contradiction by A1,A3,A4,A7,Th4;
case f.(1+1)=f.((len f-'1)+1);
hence contradiction by A1,A7,A8,A10,Th4;
end;
hence contradiction;
case A13:LSeg(f,1)=LSeg(f,(len f-'1));
A14:1+1<(len f-'1)+1 by A5,REAL_1:53;
A15:(len f-'1)<len f by A10,NAT_1:38;
A16:1<(len f-'1)+1 by A6,A9,XCMPLX_1:27;
A17: (len f-'1)+1<=len f by A9,XCMPLX_1:27;
A18:1<len f by A5,JORDAN3:7;
LSeg(f/.1,f/.(1+1))=LSeg(f,(len f-'1))
by A8,A13,TOPREAL1:def 5;
then A19: LSeg(f/.1,f/.(1+1))=LSeg(f/.(len f-'1),f/.((len f-'1)+1))
by A5,A17,TOPREAL1:def 5;
A20:f/.1=f.1 by A18,FINSEQ_4:24;
A21:f/.(1+1)=f.(1+1) by A8,FINSEQ_4:24;
A22:f/.(len f-'1)=f.(len f-'1) by A5,A15,FINSEQ_4:24;
A23:f/.((len f-'1)+1)=f.((len f-'1)+1) by A16,A17,FINSEQ_4:24;
now per cases by A19,A20,A21,A22,A23,SPPOL_1:25;
case f.1=f.(len f-'1) & f.(1+1)=f.((len f-'1)+1);
hence contradiction by A1,A7,A14,A17,Th4;
case f.1=f.((len f-'1)+1) & f.(1+1)=f.(len f-'1);
hence contradiction by A1,A9,XCMPLX_1:27;
end;
hence contradiction;
end;
hence contradiction;
end;
hence thesis by A2,Th17;
suppose A24:len f-'1<=2;
for i,j st i+1 < j holds LSeg(f,i) misses LSeg(f,j)
proof let i,j;assume A25:i+1 < j;
per cases;
suppose A26:1<=i & j+1<=len f;
i+1+1<j+1 by A25,REAL_1:53;
then A27:i+1+1<len f by A26,AXIOMS:22;
1<i+1 by A26,NAT_1:38;
then 1+1<i+1+1 by REAL_1:67;
then 1+1+1<=i+1+1 by NAT_1:38;
then 1+1+1<len f by A27,AXIOMS:22;
then A28: 1+1+1-1<len f-1 by REAL_1:54;
then 1<len f-1 by AXIOMS:22;
hence thesis by A24,A28,JORDAN3:1;
suppose A29:1>i or j+1>len f;
now per cases by A29;
case 1>i;
then LSeg(f,i)={} by TOPREAL1:def 5;
hence LSeg(f,i) /\ LSeg(f,j) = {};
case j+1>len f;
then LSeg(f,j)={} by TOPREAL1:def 5;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
hence thesis by XBOOLE_0:def 7;
end;
hence thesis by TOPREAL1:def 9;
end;
theorem Th20:for p1,p2,p3 being Point of TOP-REAL n st
(ex x being set st x<>p2 & x in LSeg(p1,p2)/\ LSeg(p2,p3)) holds
p1 in LSeg(p2,p3) or p3 in LSeg(p1,p2)
proof let p1,p2,p3 be Point of TOP-REAL n;
given x being set such that
A1:x<>p2 & x in LSeg(p1,p2)/\ LSeg(p2,p3);
A2:x in LSeg(p1,p2) & x in LSeg(p2,p3) by A1,XBOOLE_0:def 3;
reconsider p=x as Point of TOP-REAL n by A1;
p in { (1-r1)*p1 + r1*p2 : 0 <= r1 & r1 <= 1 } by A2,TOPREAL1:def 4;
then consider r1 such that
A3:p=(1-r1)*p1 + r1*p2 &( 0 <= r1 & r1 <= 1 );
p in { (1-r2)*p2 + r2*p3 : 0 <= r2 & r2 <= 1 } by A2,TOPREAL1:def 4;
then consider r2 such that
A4:p=(1-r2)*p2 + r2*p3 &( 0 <= r2 & r2 <= 1 );
per cases;
suppose A5:r1>=1-r2;
now per cases;
case A6:r2<>0;
r2*p3=(1-r1)*p1 + r1*p2-(1-r2)*p2 by A3,A4,EUCLID:52;
then r2*p3=(1-r1)*p1 + (r1*p2-(1-r2)*p2) by EUCLID:49;
then r2"*(r2*p3)=r2"*((1-r1)*p1 + (r1-(1-r2))*p2) by EUCLID:54;
then (r2"*r2)*p3=r2"*((1-r1)*p1 + (r1-(1-r2))*p2) by EUCLID:34;
then 1*p3=r2"*((1-r1)*p1 + (r1-(1-r2))*p2) by A6,XCMPLX_0:def 7;
then A7: p3=r2"*((1-r1)*p1 + (r1-(1-r2))*p2) by EUCLID:33
.=r2"*((1-r1)*p1) +r2"*((r1-(1-r2))*p2) by EUCLID:36
.=(r2"*(1-r1))*p1 +r2"*((r1-(1-r2))*p2) by EUCLID:34
.=(r2"*(1-r1))*p1 +(r2"*(r1-(1-r2)))*p2 by EUCLID:34;
r2"*(1-r1) +r2"*(r1-(1-r2))=r2"*(1-r1+(r1-(1-r2))) by XCMPLX_1:8
.=r2"*(1-r1+r1-(1-r2)) by XCMPLX_1:29 .=r2"*(1-(1-r2)) by XCMPLX_1:27
.=r2"*(1-1+r2) by XCMPLX_1:37 .=1 by A6,XCMPLX_0:def 7;
then A8:r2"*(1-r1)=1-r2"*(r1-(1-r2)) by XCMPLX_1:26;
A9:(r1-(1-r2))>=0 by A5,SQUARE_1:12;
A10:r2">0 by A4,A6,REAL_1:72;
then A11:0<=r2"*(r1-(1-r2)) by A9,REAL_2:121;
r1<=1+0 by A3;
then r1-1<=0 by REAL_1:86;
then r1-1+r2<=0+r2 by AXIOMS:24;
then (r1-(1-r2))<=r2 by XCMPLX_1:37;
then r2"*(r1-(1-r2))<=r2"*r2 by A10,AXIOMS:25;
then r2"*(r1-(1-r2))<=1 by A6,XCMPLX_0:def 7;
then p3 in {(1-r)*p1+r*p2:0<=r & r<=1} by A7,A8,A11;
hence p1 in LSeg(p2,p3) or p3 in LSeg(p1,p2) by TOPREAL1:def 4;
case r2=0; then p=1*p2+0.REAL n by A4,EUCLID:33;
then p=p2+0.REAL n by EUCLID:33;
hence p1 in LSeg(p2,p3) or p3 in LSeg(p1,p2) by A1,EUCLID:31;
end;
hence thesis;
suppose A12:r1<1-r2;
set s1=1-r2;
set s2=1-r1;
A13:1-s1=1-1+r2 by XCMPLX_1:37 .=r2;
A14:1-s2=1-1+r1 by XCMPLX_1:37 .=r1;
A15: 0+s1<=1-s1+s1 by A4,A13,AXIOMS:24;
1-s2+s2<=1+s2 by A3,A14,AXIOMS:24;
then 1<=1+s2 by XCMPLX_1:27;
then A16: 1-1<=s2 by REAL_1:86;
now per cases;
case A17:s2<>0;
s2*p1=(1-s1)*p3 + s1*p2-(1-s2)*p2 by A3,A4,A13,A14,EUCLID:52
.=(1-s1)*p3 + (s1*p2-(1-s2)*p2) by EUCLID:49
.=(1-s1)*p3 + (s1-(1-s2))*p2 by EUCLID:54;
then (s2"*s2)*p1=s2"*((1-s1)*p3 + (s1-(1-s2))*p2) by EUCLID:34;
then 1*p1=s2"*((1-s1)*p3 + (s1-(1-s2))*p2) by A17,XCMPLX_0:def 7;
then p1=s2"*((1-s1)*p3 + (s1-(1-s2))*p2) by EUCLID:33
.=s2"*((1-s1)*p3) +s2"*((s1-(1-s2))*p2) by EUCLID:36
.=(s2"*(1-s1))*p3 +s2"*((s1-(1-s2))*p2) by EUCLID:34;
then A18:p1=(s2"*(1-s1))*p3 +(s2"*(s1-(1-s2)))*p2 by EUCLID:34;
s2"*(1-s1) +s2"*(s1-(1-s2))=s2"*(1-s1+(s1-(1-s2))) by XCMPLX_1:8
.=s2"*(1-s1+s1-(1-s2)) by XCMPLX_1:29 .=s2"*(1-(1-s2)) by XCMPLX_1:27
.=s2"*(1-1+s2) by XCMPLX_1:37 .=1 by A17,XCMPLX_0:def 7;
then A19:s2"*(1-s1)=1-s2"*(s1-(1-s2)) by XCMPLX_1:26;
A20:(s1-(1-s2))>=0 by A12,A14,SQUARE_1:12;
A21:s2">0 by A16,A17,REAL_1:72;
then A22:0<=s2"*(s1-(1-s2)) by A20,REAL_2:121;
s1<=1+0 by A15,XCMPLX_1:27;
then s1-1<=0 by REAL_1:86;
then s1-1+s2<=0+s2 by AXIOMS:24;
then (s1-(1-s2))<=s2 by XCMPLX_1:37;
then s2"*(s1-(1-s2))<=s2"*s2 by A21,AXIOMS:25;
then s2"*(s1-(1-s2))<=1 by A17,XCMPLX_0:def 7;
then p1 in {(1-r)*p3+r*p2:0<=r & r<=1} by A18,A19,A22;
hence p1 in LSeg(p2,p3) or p3 in LSeg(p1,p2) by TOPREAL1:def 4;
case s2=0; then p=1*p2+0.REAL n by A3,A14,EUCLID:33;
then p=p2+0.REAL n by EUCLID:33;
hence p1 in LSeg(p2,p3) or p3 in LSeg(p1,p2) by A1,EUCLID:31;
end;
hence thesis;
end;
theorem Th21:for f being FinSequence of TOP-REAL 2 st f is s.n.c. &
LSeg(f,1) /\ LSeg(f,1+1) c= {f/.(1+1)} &
LSeg(f,len f-'2) /\ LSeg(f,len f-'1) c= {f/.(len f-'1)} holds
f is unfolded
proof let f be FinSequence of TOP-REAL 2;
assume A1: f is s.n.c. &
LSeg(f,1) /\ LSeg(f,1+1) c= {f/.(1+1)} &
LSeg(f,len f-'2) /\ LSeg(f,len f-'1) c= {f/.(len f-'1)};
for i st 1 <= i & i + 2 <= len f
holds LSeg(f,i) /\ LSeg(f,i+1) = {f/.(i+1)}
proof let i;assume A2:1 <= i & i + 2 <= len f;
A3:i+1+1=i+(1+1) by XCMPLX_1:1 .=i+2;
A4: 1<i+1 by A2,NAT_1:38;
A5:i+1<len f by A2,A3,NAT_1:38;
then A6:i<len f by NAT_1:38;
A7:1<i+1+1 by A4,NAT_1:38;
A8:LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A2,A5,TOPREAL1:def 5;
A9:LSeg(f,i+1)=LSeg(f/.(i+1),f/.(i+1+1))
by A2,A3,A4,TOPREAL1:def 5;
A10:f/.(i+1) in LSeg(f/.i,f/.(i+1)) by TOPREAL1:6;
f/.(i+1) in LSeg(f/.(i+1),f/.(i+1+1)) by TOPREAL1:6;
then f/.(i+1) in LSeg(f,i) /\ LSeg(f,i+1) by A8,A9,A10,XBOOLE_0:def 3;
then A11:{f/.(i+1)} c= LSeg(f,i) /\ LSeg(f,i+1) by ZFMISC_1:37;
per cases;
suppose i=1;
hence thesis by A1,A11,XBOOLE_0:def 10;
suppose A12:i<>1;
now per cases;
case A13:i+2=len f;
then A14:i=len f-2 by XCMPLX_1:26;
then A15:len f-2=len f-'2 by A2,JORDAN3:1;
A16:i+1=len f-1 by A3,A13,XCMPLX_1:26;
then len f-1=len f-'1 by A4,JORDAN3:1;
hence LSeg(f,i) /\ LSeg(f,i+1) = {f/.(i+1)}
by A1,A11,A14,A15,A16,XBOOLE_0:def 10;
case i+2<>len f;
then i+2<len f by A2,REAL_1:def 5;
then A17:i+1+1+1<=len f by A3,NAT_1:38;
1<i by A2,A12,REAL_1:def 5;
then 1+1<=i by NAT_1:38;
then A18: 1+1-1<=i-1 by REAL_1:49;
now assume A19:LSeg(f,i) /\ LSeg(f,i+1)<>{f/.(i+1)};
A20:f/.(i+1) in LSeg(f,i+1) by A9,TOPREAL1:6;
f/.(i+1) in LSeg(f,i) by A8,TOPREAL1:6;
then f/.(i+1) in LSeg(f,i) /\ LSeg(f,i+1) by A20,XBOOLE_0:def 3;
then {f/.(i+1)} c= LSeg(f,i) /\ LSeg(f,i+1) by ZFMISC_1:37;
then not LSeg(f,i) /\ LSeg(f,i+1) c= {f/.(i+1)}
by A19,XBOOLE_0:def 10;
then consider x being set such that
A21: x in LSeg(f,i) /\ LSeg(f,i+1) & not x in {f/.(i+1)} by TARSKI:def 3;
A22:x<>f/.(i+1) by A21,TARSKI:def 1;
A23:LSeg(f,i+1+1)=LSeg(f/.(i+1+1),f/.(i+1+1+1))
by A7,A17,TOPREAL1:def 5;
now per cases by A8,A9,A21,A22,Th20;
case A24: f/.i in LSeg(f/.(i+1),f/.(i+1+1));
A25:i-'1=i-1 by A2,SCMFSA_7:3;
then A26:i-'1+1=i by XCMPLX_1:27;
then i-'1+1<i+1 by NAT_1:38;
then LSeg(f,i-'1) misses LSeg(f,i+1) by A1,TOPREAL1:def 9;
then A27:LSeg(f,i-'1)/\ LSeg(f,i+1)={} by XBOOLE_0:def 7;
LSeg(f,i-'1)=LSeg(f/.(i-'1),f/.(i-'1+1))
by A6,A18,A25,A26,TOPREAL1:def 5;
then f/.i in LSeg(f,i-'1) by A26,TOPREAL1:6;
hence contradiction by A9,A24,A27,XBOOLE_0:def 3;
case A28: f/.(i+1+1) in LSeg(f/.i,f/.(i+1));
i+1<i+1+1 by NAT_1:38;
then LSeg(f,i) misses LSeg(f,i+1+1) by A1,TOPREAL1:def 9;
then A29:LSeg(f,i)/\ LSeg(f,i+1+1)={} by XBOOLE_0:def 7;
f/.(i+1+1) in LSeg(f,i+1+1) by A23,TOPREAL1:6;
hence contradiction by A8,A28,A29,XBOOLE_0:def 3;
end;
hence contradiction;
end;
hence LSeg(f,i) /\ LSeg(f,i+1) = {f/.(i+1)};
end;
hence thesis;
end;
hence thesis by TOPREAL1:def 8;
end;
theorem Th22:for f being FinSequence of X holds
PairF(f) is Simple & f.1<>f.len f implies f is one-to-one & len f<>1
proof let f be FinSequence of X;
thus PairF(f) is Simple & f.1<>f.len f implies f is one-to-one & len f<>1
proof assume A1:PairF(f) is Simple & f.1<>f.len f;
then consider vs being FinSequence of the Vertices of PGraph(X) such that
A2:vs is_oriented_vertex_seq_of PairF(f) &
(for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs)
by GRAPH_4:def 7;
reconsider f1=f as FinSequence of the Vertices of PGraph(X) by Th7;
now per cases;
case A3:len f>=1;
now per cases by A3,REAL_1:def 5;
case A4: len f>1;
A5: f1 is_oriented_vertex_seq_of PairF(f) by A3,Th11;
then len f1=len PairF(f)+1 by GRAPH_4:def 5;
then 1-1<len PairF(f)+1-1 by A4,REAL_1:54;
then 1-1<len PairF(f) by XCMPLX_1:26;
then PairF(f) <> {} by FINSEQ_1:25;
then A6:vs = f1 by A2,A5,GRAPH_4:11;
for x,y st x in dom f & y in dom f & f.x=f.y holds x=y
proof let x,y;assume A7:x in dom f & y in dom f & f.x=f.y;
A8:dom f=Seg len f by FINSEQ_1:def 3;
reconsider i=x,j=y as Nat by A7;
A9:1<=i & i<=len f by A7,A8,FINSEQ_1:3;
A10:1<=j & j<=len f by A7,A8,FINSEQ_1:3;
now assume A11:i<>j;
now per cases by A11,REAL_1:def 5;
case i<j; then i=1 & j=len f by A2,A6,A7,A9,A10;
hence contradiction by A1,A7;
case j<i; then j=1 & i=len f by A2,A6,A7,A9,A10;
hence contradiction by A1,A7;
end;
hence contradiction;
end;
hence thesis;
end;
hence f is one-to-one by FUNCT_1:def 8;
case len f=1;
hence f is one-to-one by A1;
end;
hence f is one-to-one;
case len f<1; then len f+1<=1 by NAT_1:38;
then len f+1-1<=1-1 by REAL_1:49; then len f<=1-1 by XCMPLX_1:26;
then len f=0 by NAT_1:18;
then for x,y st x in dom f & y in dom f & f.x=f.y holds x=y by FINSEQ_1:4,
def 3;
hence f is one-to-one by FUNCT_1:def 8;
end;
hence thesis by A1;
end;
end;
theorem for f being FinSequence of X holds
f is one-to-one & len f>1 implies PairF(f) is Simple & f.1<>f.len f
proof let f be FinSequence of X;
assume A1:f is one-to-one & len f>1;
then A2:1 in dom f by FINSEQ_3:27;
A3: len f in dom f by A1,FINSEQ_3:27;
reconsider f1=f as FinSequence of the Vertices of PGraph(X) by Th7;
A4: f1 is_oriented_vertex_seq_of PairF(f) by A1,Th11;
for i,j st 1<=i & i<j & j<=len f1 & f1.i=f1.j holds i=1 & j=len f1
proof let i,j;assume A5:1<=i & i<j & j<=len f1 & f1.i=f1.j;
then A6:i<len f by AXIOMS:22;
1<j by A5,AXIOMS:22;
then A7: j in Seg len f by A5,FINSEQ_1:3;
i in Seg len f by A5,A6,FINSEQ_1:3;
then i in dom f & j in dom f by A7,FINSEQ_1:def 3;
hence thesis by A1,A5,FUNCT_1:def 8;
end;
hence thesis by A1,A2,A3,A4,FUNCT_1:def 8,GRAPH_4:def 7;
end;
theorem for f being FinSequence of TOP-REAL 2 st
f is nodic & PairF(f) is Simple & f.1<>f.len f holds f is unfolded
proof let f be FinSequence of TOP-REAL 2;
assume A1:f is nodic & PairF(f) is Simple & f.1<>f.len f;
then A2:f is s.n.c. by Th19;
per cases;
suppose A3:2<len f;
then A4:2+1<=len f by NAT_1:38;
A5:1+1<=len f by A3;
A6:LSeg(f,1)=LSeg(f/.1,f/.(1+1)) by A3,TOPREAL1:def 5;
A7:LSeg(f,2)=LSeg(f/.2,f/.(2+1)) by A4,TOPREAL1:def 5;
A8:f is one-to-one by A1,Th22;
A9:1<len f by A3,AXIOMS:22;
then A10:1 in dom f by FINSEQ_3:27;
A11:2 in dom f by A3,FINSEQ_3:27;
A12:f.1=f/.1 by A9,FINSEQ_4:24;
A13:2+1 in dom f by A4,FINSEQ_3:27;
A14:f.2=f/.2 by A3,FINSEQ_4:24;
then A15:f.2 in LSeg(f,1) by A5,TOPREAL1:27;
A16:now assume A17:LSeg(f,1)=LSeg(f,2);
now per cases by A6,A7,A17,SPPOL_1:25;
case A18:f/.1=f/.2 & f/.(1+1)=f/.(2+1);
A19:f.1=f/.1 by A9,FINSEQ_4:24;
f.2=f/.2 by A3,FINSEQ_4:24;
hence contradiction by A8,A10,A11,A18,A19,FUNCT_1:def 8;
case A20:f/.1=f/.(2+1) & f/.(1+1)=f/.2;
f.(2+1)=f/.(2+1) by A4,FINSEQ_4:24;
hence contradiction by A8,A10,A12,A13,A20,FUNCT_1:def 8;
end;
hence contradiction;
end;
f.2 in LSeg(f,2) by A4,A14,TOPREAL1:27;
then LSeg(f,1)/\ LSeg(f,2)<>{} by A15,XBOOLE_0:def 3;
then LSeg(f,1) meets LSeg(f,2) by XBOOLE_0:def 7;
then LSeg(f,1) /\ LSeg(f,2)={f.1} &(f.1=f.2 or f.1=f.(2+1)) or
LSeg(f,1) /\ LSeg(f,2)={f.(1+1)} &(f.(1+1)=f.2 or f.(1+1)=f.(2+1))
by A1,A16,Def4;
then A21:LSeg(f,1) /\ LSeg(f,1+1) c= {f/.(1+1)}
by A3,A8,A10,A13,FINSEQ_4:24,FUNCT_1:def 8;
A22:1+1-1<=len f-1 by A3,REAL_1:49;
A23:2+1-2<=len f-2 by A4,REAL_1:49;
A24:len f-1=len f-'1 by A9,SCMFSA_7:3;
then A25:len f-'1+1=len f by XCMPLX_1:27;
A26:len f-'2=len f-2 by A3,SCMFSA_7:3;
then A27:len f-'2+1=len f-(1+1-1) by XCMPLX_1:37;
len f<len f+1 by NAT_1:38;
then A28:len f-1<len f by REAL_1:84;
then len f-1-1<len f-1 by REAL_1:54;
then A29:len f-(1+1)<len f-1 by XCMPLX_1:36;
then A30:len f-2<len f by A28,AXIOMS:22;
A31:len f-'2<len f by A26,A28,A29,AXIOMS:22;
then A32:(len f-'2)+1<=len f by NAT_1:38;
then A33:LSeg(f,(len f-'2))=LSeg(f/.(len f-'2),f/.((len f-'2)+1))
by A23,A26,TOPREAL1:def 5;
A34:LSeg(f,(len f-'1))=LSeg(f/.(len f-'1),f/.((len f-'1)+1))
by A22,A24,A25,TOPREAL1:def 5;
A35:f.(len f-'2)=f/.(len f-'2) by A23,A26,A31,FINSEQ_4:24;
A36:f.(len f-'2)=f/.(len f-'2) by A23,A26,A30,FINSEQ_4:24;
A37:now assume A38:LSeg(f,(len f-'2))=LSeg(f,(len f-'1));
A39:(len f-'2) in dom f by A23,A26,A31,FINSEQ_3:27;
A40:(len f-'1) in dom f by A22,A24,A28,FINSEQ_3:27;
now per cases by A33,A34,A38,SPPOL_1:25;
case A41:f/.(len f-'2)=f/.(len f-'1)
& f/.((len f-'2)+1)=f/.((len f-'1)+1);
f.(len f-'1)=f/.(len f-'1) by A22,A24,A28,FINSEQ_4:24;
hence contradiction by A8,A24,A26,A29,A35,A39,A40,A41,FUNCT_1:def 8;
case A42:f/.(len f-'2)=f/.((len f-'1)+1)
& f/.((len f-'2)+1)=f/.(len f-'1);
(len f-'1)+1 in Seg len f by A9,A25,FINSEQ_1:3;
then A43:(len f-'1)+1 in dom f by FINSEQ_1:def 3;
f.((len f-'1)+1)=f/.((len f-'1)+1) by A9,A25,FINSEQ_4:24;
hence contradiction
by A8,A25,A26,A28,A29,A36,A39,A42,A43,FUNCT_1:def 8;
end;
hence contradiction;
end;
A44:f.(len f-'1)=f/.(len f-'1) by A22,A24,A28,FINSEQ_4:24;
then A45:f.(len f-'1) in LSeg(f,(len f-'2))
by A23,A24,A26,A27,A32,TOPREAL1:27;
f.(len f-'1) in LSeg(f,(len f-'1)) by A22,A24,A25,A44,TOPREAL1:27;
then LSeg(f,(len f-'2))/\ LSeg(f,(len f-'1))<>{} by A45,XBOOLE_0:def 3;
then LSeg(f,(len f-'2)) meets LSeg(f,(len f-'1)) by XBOOLE_0:def 7;
then A46:LSeg(f,(len f-'2)) /\ LSeg(f,(len f-'1))={f.(len f-'2)}
&(f.(len f-'2)=f.(len f-'1) or f.(len f-'2)=f.((len f-'1)+1)) or
LSeg(f,(len f-'2)) /\ LSeg(f,(len f-'1))={f.((len f-'2)+1)}
&(f.((len f-'2)+1)=f.(len f-'1) or f.((len f-'2)+1)=f.((len f-'1)+1))
by A1,A37,Def4;
A47:len f-'2 in dom f by A23,A26,A31,FINSEQ_3:27;
len f-'1+1 in dom f by A9,A25,FINSEQ_3:27;
then LSeg(f,len f-'2) /\ LSeg(f,len f-'1) c= {f/.(len f-'1)}
by A8,A22,A24,A25,A26,A27,A28,A29,A46,A47,FINSEQ_4:24,FUNCT_1:def 8;
hence thesis by A2,A21,Th21;
suppose A48:len f<=2;
for i st 1 <= i & i + 2 <= len f
holds LSeg(f,i) /\ LSeg(f,i+1) = {f/.(i+1)}
proof let i;assume A49:1 <= i & i + 2 <= len f;
then i+2<=2 by A48,AXIOMS:22;
then i<=2-2 by REAL_1:84;
hence thesis by A49,AXIOMS:22;
end;
hence thesis by TOPREAL1:def 8;
end;
theorem Th25: for f,g being FinSequence of TOP-REAL 2,i st
g is_Shortcut_of f & 1 <= i & i+1 <= len g holds
ex k1 being Nat st 1<=k1 & k1+1<=len f & f/.k1=g/.i &
f/.(k1+1)=g/.(i+1)
& f.k1=g.i & f.(k1+1)=g.(i+1)
proof let f,g be FinSequence of TOP-REAL 2,i;assume that
A1:g is_Shortcut_of f and
A2:1 <= i & i+1 <= len g;
A3:i<=len g by A2,NAT_1:38;
A4:1<=i+1 by A2,NAT_1:38;
A5: rng PairF(g) c= rng PairF(f) by A1,Th14;
A6:i<len g by A2,NAT_1:38;
then A7:(PairF(g)).i=[g.i,g.(i+1)] by A2,Def2;
A8:len PairF(g)=len g -'1 by Def2;
A9:i<=len g-1 by A2,REAL_1:84;
then 1<=len g-1 by A2,AXIOMS:22;
then len g-'1=len g-1 by JORDAN3:1;
then i in dom (PairF(g)) by A2,A8,A9,FINSEQ_3:27;
then [ g.i,g.(i+1) ] in rng PairF(g) by A7,FUNCT_1:def 5;
then consider x such that
A10:x in dom PairF(f) & (PairF(f)).x=[g.i,g.(i+1)] by A5,FUNCT_1:def 5;
A11:x in Seg len PairF(f) by A10,FINSEQ_1:def 3;
reconsider k=x as Nat by A10;
A12:1<=k & k<=len PairF(f) by A11,FINSEQ_1:3;
A13:len PairF(f)=len f-'1 by Def2;
A14:1<len g by A2,A6,AXIOMS:22;
len g<=len f by A1,Th12;
then 1<=len f by A14,AXIOMS:22;
then len f-'1=len f-1 by SCMFSA_7:3;
then k+1<=len f-1+1 by A12,A13,AXIOMS:24;
then A15:k+1<=len f by XCMPLX_1:27;
then A16:k<len f by NAT_1:38;
then [ g.i,g.(i+1)]=[ f.k,f.(k+1) ] by A10,A12,Def2;
then A17:g.i=f.k & g.(i+1)=f.(k+1) by ZFMISC_1:33;
A18:1<k+1 by A12,NAT_1:38;
A19:g/.i=g.i by A2,A3,FINSEQ_4:24;
A20:g/.(i+1)=g.(i+1) by A2,A4,FINSEQ_4:24;
A21:f/.k=f.k by A12,A16,FINSEQ_4:24;
f/.(k+1)=f.(k+1) by A15,A18,FINSEQ_4:24;
hence thesis by A12,A15,A17,A19,A20,A21;
end;
theorem Th26: for f,g being FinSequence of TOP-REAL 2 st
g is_Shortcut_of f holds rng g c= rng f
proof let f,g be FinSequence of TOP-REAL 2;
assume A1: g is_Shortcut_of f;
let x;assume x in rng g;
then consider z being set such that
A2:z in dom g & x=g.z by FUNCT_1:def 5;
A3:z in Seg len g by A2,FINSEQ_1:def 3;
reconsider i=z as Nat by A2;
A4:1<=i & i<=len g by A3,FINSEQ_1:3;
per cases;
suppose i<len g; then i+1<=len g by NAT_1:38;
then consider k1 being Nat such that
A5:1<=k1 & k1+1<=len f & f/.k1=g/.i
& f/.(k1+1)=g/.(i+1) & f.k1=g.i & f.(k1+1)=g.(i+1) by A1,A4,Th25;
k1<len f by A5,NAT_1:38;
then k1 in dom f by A5,FINSEQ_3:27;
hence x in rng f by A2,A5,FUNCT_1:def 5;
suppose i>=len g; then A6:i=len g by A4,AXIOMS:21;
now per cases;
case A7:1<i; then 1-1<i-1 by REAL_1:54;
then 0<i-'1 by A7,SCMFSA_7:3;
then A8:0+1<=i-'1 by NAT_1:38;
i-'1=i-1 by A7,SCMFSA_7:3;
then A9:i-'1+1=len g by A6,XCMPLX_1:27;
then consider k1 being Nat such that
A10:1<=k1 & k1+1<=len f & f/.k1=g/.(i-'1)
& f/.(k1+1)=g/.(i-'1+1) & f.k1=g.(i-'1)
& f.(k1+1)=g.(i-'1+1) by A1,A8,Th25;
1<k1+1 by A10,NAT_1:38;
then k1+1 in dom f by A10,FINSEQ_3:27;
hence x in rng f by A2,A6,A9,A10,FUNCT_1:def 5;
case 1>=i;
then A11:i=1 by A4,AXIOMS:21;
A12:f.1=g.1 by A1,Def3;
len g<=len f by A1,Th12;
then 1 in dom f by A6,A11,FINSEQ_3:27;
hence x in rng f by A2,A11,A12,FUNCT_1:def 5;
end;
hence thesis;
end;
theorem Th27: for f,g being FinSequence of TOP-REAL 2 st
g is_Shortcut_of f holds L~g c= L~f
proof let f,g be FinSequence of TOP-REAL 2;
assume A1: g is_Shortcut_of f;
let x be set;assume x in L~g;
then x in union { LSeg(g,i) : 1 <= i & i+1 <= len g } by TOPREAL1:def 6;
then consider y such that A2:x in y & y in
{ LSeg(g,i) : 1 <= i & i+1 <= len g }
by TARSKI:def 4;
consider i such that A3: y=LSeg(g,i) &(1<=i & i+1<=len g) by A2;
A4:x in LSeg(g/.i,g/.(i+1)) by A2,A3,TOPREAL1:def 5;
consider k1 being Nat such that
A5: 1<=k1 & k1+1<=len f & f/.k1=g/.i & f/.(k1+1)=g/.(i+1)
& f.k1=g.i & f.(k1+1)=g.(i+1) by A1,A3,Th25;
A6:x in LSeg(f,k1) by A4,A5,TOPREAL1:def 5;
LSeg(f,k1) in {LSeg(f,k):1<=k & k+1<=len f} by A5;
then x in union { LSeg(f,k) : 1 <= k & k+1 <= len f } by A6,TARSKI:def 4;
hence thesis by TOPREAL1:def 6;
end;
theorem Th28: for f,g being FinSequence of TOP-REAL 2 st f is special
& g is_Shortcut_of f holds g is special
proof let f,g be FinSequence of TOP-REAL 2;assume
A1:f is special & g is_Shortcut_of f;
for i st 1 <= i & i+1 <= len g holds
(g/.i)`1 = (g/.(i+1))`1 or (g/.i)`2 = (g/.(i+1))`2
proof let i;assume
A2:1 <= i & i+1 <= len g;
then A3:i<=len g by NAT_1:38;
A4:1<=i+1 by A2,NAT_1:38;
A5: rng PairF(g) c= rng PairF(f) by A1,Th14;
A6:i<len g by A2,NAT_1:38;
then A7:(PairF(g)).i=[g.i,g.(i+1)] by A2,Def2;
A8:len PairF(g)=len g -'1 by Def2;
A9:i<=len g-1 by A2,REAL_1:84;
then 1<=len g-1 by A2,AXIOMS:22;
then len g-'1=len g-1 by JORDAN3:1;
then i in dom PairF(g) by A2,A8,A9,FINSEQ_3:27;
then [ (g.i),(g.(i+1)) ] in rng PairF(g) by A7,FUNCT_1:def 5;
then consider x such that
A10:x in dom PairF(f) & (PairF(f)).x=[g.i,g.(i+1)] by A5,FUNCT_1:def 5;
A11:x in Seg len PairF(f) by A10,FINSEQ_1:def 3;
reconsider k=x as Nat by A10;
A12:1<=k & k<=len PairF(f) by A11,FINSEQ_1:3;
A13:len PairF(f)=len f-'1 by Def2;
A14:1<len g by A2,A6,AXIOMS:22;
len g<=len f by A1,Th12;
then 1<=len f by A14,AXIOMS:22;
then len f-'1=len f-1 by SCMFSA_7:3;
then k+1<=len f-1+1 by A12,A13,AXIOMS:24;
then A15:k+1<=len f by XCMPLX_1:27;
then A16:k<len f by NAT_1:38;
then (PairF(f)).k=[f.k,f.(k+1)] by A12,Def2;
then A17:g.i=f.k & g.(i+1)=f.(k+1) by A10,ZFMISC_1:33;
A18:1<k+1 by A12,NAT_1:38;
A19:g/.i=g.i by A2,A3,FINSEQ_4:24;
A20:g/.(i+1)=g.(i+1) by A2,A4,FINSEQ_4:24;
A21:f/.k=f.k by A12,A16,FINSEQ_4:24;
f/.(k+1)=f.(k+1) by A15,A18,FINSEQ_4:24;
hence thesis by A1,A12,A15,A17,A19,A20,A21,TOPREAL1:def 7;
end;
hence thesis by TOPREAL1:def 7;
end;
theorem Th29:for f being FinSequence of TOP-REAL 2 st f is special & 2<=len f
& f.1 <> f.len f holds ex g being FinSequence of TOP-REAL 2 st
2<=len g & g is special & g is one-to-one & L~g c= L~f & f.1=g.1
& f.len f=g.len g & rng g c= rng f
proof let f be FinSequence of TOP-REAL 2;assume
A1:f is special & 2<=len f & f.1 <> f.len f; then 1<=len f by AXIOMS:22;
then consider g being FinSequence of TOP-REAL 2 such that
A2:g is_Shortcut_of f by Th13;
A3:g is one-to-one & rng PairF(g) c= rng PairF(f)
& g.1=f.1 & g.len g=f.len f by A1,A2,Th15;
A4:g is special by A1,A2,Th28;
A5:L~g c= L~f by A2,Th27;
A6: rng g c= rng f by A2,Th26;
1<=len g by A2,Th12;
then 1<len g by A1,A3,REAL_1:def 5;
then 1+1<=len g by NAT_1:38;
hence thesis by A3,A4,A5,A6;
end;
:: Goboard Theorem for general special sequences
theorem Th30:for f1,f2 being FinSequence of TOP-REAL 2 st
f1 is special & f2 is special & 2<=len f1 & 2<=len f2 & f1.1<>f1.len f1
& f2.1<>f2.len f2 &
X_axis(f1) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
X_axis(f2) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
Y_axis(f1) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) &
Y_axis(f2) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) holds
L~f1 meets L~f2
proof let f1,f2 be FinSequence of TOP-REAL 2;
assume A1:f1 is special & f2 is special & 2<=len f1
& 2<=len f2 & f1.1<>f1.len f1
& f2.1<>f2.len f2 &
X_axis(f1) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
X_axis(f2) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
Y_axis(f1) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) &
Y_axis(f2) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2);
then consider g1 being FinSequence of TOP-REAL 2 such that
A2: 2<=len g1 & g1 is special & g1 is one-to-one & L~g1 c= L~f1 & f1.1=g1.1
& f1.len f1=g1.len g1 & rng g1 c= rng f1 by Th29;
consider g2 being FinSequence of TOP-REAL 2 such that
A3: 2<=len g2 & g2 is special & g2 is one-to-one & L~g2 c= L~f2 & f2.1=g2.1
& f2.len f2=g2.len g2 & rng g2 c= rng f2 by A1,Th29;
for i st i in dom X_axis(g1) holds (X_axis(g1)).1 <= X_axis(g1).i
& X_axis(g1).i <= (X_axis(g1)).(len g1)
proof let i;assume A4:i in dom X_axis(g1);
A5:len (X_axis(f1)) = len f1 &
for j st j in dom X_axis(f1) holds (X_axis(f1)).j = (f1/.j)`1
by GOBOARD1:def 3;
A6:len (X_axis(g1)) = len g1 &
for j st j in dom X_axis(g1) holds (X_axis(g1)).j = (g1/.j)`1
by GOBOARD1:def 3;
A7:1<=len g1 by A2,AXIOMS:22;
then A8:1 in dom X_axis(g1) by A6,FINSEQ_3:27;
A9:g1/.1=g1.1 by A7,FINSEQ_4:24;
A10:1<=len f1 by A1,AXIOMS:22;
then A11:g1/.1=f1/.1 by A2,A9,FINSEQ_4:24;
g1/.len g1=g1.(len g1) by A7,FINSEQ_4:24;
then A12:g1/.len g1=f1/.len f1 by A2,A10,FINSEQ_4:24;
A13:1 in dom X_axis(f1) by A5,A10,FINSEQ_3:27;
i in Seg len g1 by A4,A6,FINSEQ_1:def 3;
then A14:i in dom g1 by FINSEQ_1:def 3; then g1.i in rng g1 by FUNCT_1:def
5;
then consider y being set such that
A15:y in dom f1 & g1.i=f1.y by A2,FUNCT_1:def 5;
reconsider j=y as Nat by A15;
f1.j=f1/.j by A15,FINSEQ_4:def 4;
then A16:j in dom f1 & g1/.i=f1/.j by A14,A15,FINSEQ_4:def 4;
j in Seg len f1 by A15,FINSEQ_1:def 3;
then A17:j in dom (X_axis(f1)) by A5,FINSEQ_1:def 3;
then A18:(X_axis(f1)).1 <= X_axis(f1).j
& X_axis(f1).j <= (X_axis(f1)).(len f1) by A1,GOBOARD4:def 1;
A19:X_axis(f1).j =(f1/.j)`1 by A17,GOBOARD1:def 3;
len f1 in Seg len f1 by A10,FINSEQ_1:3;
then len f1 in dom (X_axis(f1)) by A5,FINSEQ_1:def 3;
then A20:(g1/.1)`1<=(g1/.i)`1 & (g1/.i)`1<=(g1/.len g1)`1
by A11,A12,A13,A16,A18,A19,GOBOARD1:def 3;
A21:X_axis(g1).i = (g1/.i)`1 by A4,GOBOARD1:def 3;
len g1 in Seg len g1 by A7,FINSEQ_1:3;
then len g1 in dom (X_axis(g1)) by A6,FINSEQ_1:def 3;
hence thesis by A8,A20,A21,GOBOARD1:def 3;
end;
then A22:X_axis(g1) lies_between (X_axis(g1)).1, (X_axis(g1)).(len g1)
by GOBOARD4:def 1;
for i st i in dom X_axis(g2) holds (X_axis(g1)).1 <= X_axis(g2).i
& X_axis(g2).i <= (X_axis(g1)).(len g1)
proof let i;assume A23:i in dom X_axis(g2);
A24:len (X_axis(f2)) = len f2 &
for j st j in dom X_axis(f2) holds (X_axis(f2)).j = (f2/.j)`1
by GOBOARD1:def 3;
A25:len (X_axis(f1)) = len f1 &
for j st j in dom X_axis(f1) holds (X_axis(f1)).j = (f1/.j)`1
by GOBOARD1:def 3;
A26:len (X_axis(g2)) = len g2 &
for j st j in dom X_axis(g2) holds (X_axis(g2)).j = (g2/.j)`1
by GOBOARD1:def 3;
A27:len (X_axis(g1)) = len g1 &
for j st j in dom X_axis(g1) holds (X_axis(g1)).j = (g1/.j)`1
by GOBOARD1:def 3;
A28:1<=len g1 by A2,AXIOMS:22; then 1 in Seg len g1 by FINSEQ_1:3;
then A29:1 in dom (X_axis(g1)) by A27,FINSEQ_1:def 3;
A30:g1/.1=g1.1 by A28,FINSEQ_4:24;
A31:1<=len f1 by A1,AXIOMS:22;
then A32:g1/.1=f1/.1 by A2,A30,FINSEQ_4:24;
g1/.len g1=g1.(len g1) by A28,FINSEQ_4:24;
then A33:g1/.len g1=f1/.len f1 by A2,A31,FINSEQ_4:24;
1 in Seg len f1 by A31,FINSEQ_1:3;
then A34:1 in dom (X_axis(f1)) by A25,FINSEQ_1:def 3;
i in Seg len g2 by A23,A26,FINSEQ_1:def 3;
then A35:i in dom g2 by FINSEQ_1:def 3; then g2.i in rng g2 by FUNCT_1:def
5;
then consider y being set such that
A36:y in dom f2 & g2.i=f2.y by A3,FUNCT_1:def 5;
reconsider j=y as Nat by A36;
f2.j=f2/.j by A36,FINSEQ_4:def 4;
then A37:j in dom f2 & g2/.i=f2/.j by A35,A36,FINSEQ_4:def 4;
j in Seg len f2 by A36,FINSEQ_1:def 3;
then A38:j in dom (X_axis(f2)) by A24,FINSEQ_1:def 3;
then A39:(X_axis(f1)).1 <= X_axis(f2).j
& X_axis(f2).j <= (X_axis(f1)).(len f1) by A1,GOBOARD4:def 1;
A40:X_axis(f2).j =(f2/.j)`1 by A38,GOBOARD1:def 3;
len f1 in Seg len f1 by A31,FINSEQ_1:3;
then len f1 in dom (X_axis(f1)) by A25,FINSEQ_1:def 3;
then A41:(g1/.1)`1<=(g2/.i)`1 & (g2/.i)`1<=(g1/.len g1)`1
by A32,A33,A34,A37,A39,A40,GOBOARD1:def 3;
A42:X_axis(g2).i =(g2/.i)`1 by A23,GOBOARD1:def 3;
len g1 in Seg len g1 by A28,FINSEQ_1:3;
then len g1 in dom (X_axis(g1)) by A27,FINSEQ_1:def 3;
hence thesis by A29,A41,A42,GOBOARD1:def 3;
end;
then A43:X_axis(g2) lies_between (X_axis(g1)).1, (X_axis(g1)).(len g1)
by GOBOARD4:def 1;
for i st i in dom Y_axis(g1) holds (Y_axis(g2)).1 <= Y_axis(g1).i
& Y_axis(g1).i <= (Y_axis(g2)).(len g2)
proof let i;assume A44:i in dom Y_axis(g1);
A45:len (Y_axis(f1)) = len f1 &
for j st j in dom Y_axis(f1) holds (Y_axis(f1)).j = (f1/.j)`2
by GOBOARD1:def 4;
A46:len (Y_axis(f2)) = len f2 &
for j st j in dom Y_axis(f2) holds (Y_axis(f2)).j = (f2/.j)`2
by GOBOARD1:def 4;
A47:len (Y_axis(g1)) = len g1 &
for j st j in dom Y_axis(g1) holds (Y_axis(g1)).j = (g1/.j)`2
by GOBOARD1:def 4;
A48:len (Y_axis(g2)) = len g2 &
for j st j in dom Y_axis(g2) holds (Y_axis(g2)).j = (g2/.j)`2
by GOBOARD1:def 4;
A49:1<=len g2 by A3,AXIOMS:22; then 1 in Seg len g2 by FINSEQ_1:3;
then A50:1 in dom (Y_axis(g2)) by A48,FINSEQ_1:def 3;
A51:g2/.1=g2.1 by A49,FINSEQ_4:24;
A52:1<=len f2 by A1,AXIOMS:22;
then A53:g2/.1=f2/.1 by A3,A51,FINSEQ_4:24;
g2/.len g2=g2.(len g2) by A49,FINSEQ_4:24;
then A54:g2/.len g2=f2/.len f2 by A3,A52,FINSEQ_4:24;
1 in Seg len f2 by A52,FINSEQ_1:3;
then A55:1 in dom (Y_axis(f2)) by A46,FINSEQ_1:def 3;
i in Seg len g1 by A44,A47,FINSEQ_1:def 3;
then A56:i in dom g1 by FINSEQ_1:def 3; then g1.i in rng g1 by FUNCT_1:def
5;
then consider y being set such that
A57:y in dom f1 & g1.i=f1.y by A2,FUNCT_1:def 5;
reconsider j=y as Nat by A57;
f1.j=f1/.j by A57,FINSEQ_4:def 4;
then A58:j in dom f1 & g1/.i=f1/.j by A56,A57,FINSEQ_4:def 4;
j in Seg len f1 by A57,FINSEQ_1:def 3;
then A59:j in dom (Y_axis(f1)) by A45,FINSEQ_1:def 3;
then A60:(Y_axis(f2)).1 <= Y_axis(f1).j
& Y_axis(f1).j <= (Y_axis(f2)).(len f2) by A1,GOBOARD4:def 1;
A61:Y_axis(f1).j =(f1/.j)`2 by A59,GOBOARD1:def 4;
len f2 in Seg len f2 by A52,FINSEQ_1:3;
then len f2 in dom (Y_axis(f2)) by A46,FINSEQ_1:def 3;
then A62:(g2/.1)`2<=(g1/.i)`2 & (g1/.i)`2<=(g2/.len g2)`2
by A53,A54,A55,A58,A60,A61,GOBOARD1:def 4;
A63:Y_axis(g1).i = (g1/.i)`2 by A44,GOBOARD1:def 4;
len g2 in Seg len g2 by A49,FINSEQ_1:3;
then len g2 in dom (Y_axis(g2)) by A48,FINSEQ_1:def 3;
hence thesis by A50,A62,A63,GOBOARD1:def 4;
end;
then A64:Y_axis(g1) lies_between (Y_axis(g2)).1, (Y_axis(g2)).(len g2)
by GOBOARD4:def 1;
for i st i in dom Y_axis(g2) holds (Y_axis(g2)).1 <= Y_axis(g2).i
& Y_axis(g2).i <= (Y_axis(g2)).(len g2)
proof let i;assume A65:i in dom Y_axis(g2);
A66:len (Y_axis(f2)) = len f2 &
for j st j in dom Y_axis(f2) holds (Y_axis(f2)).j = (f2/.j)`2
by GOBOARD1:def 4;
A67:len (Y_axis(g2)) = len g2 &
for j st j in dom Y_axis(g2) holds (Y_axis(g2)).j = (g2/.j)`2
by GOBOARD1:def 4;
A68:1<=len g2 by A3,AXIOMS:22; then 1 in Seg len g2 by FINSEQ_1:3;
then A69:1 in dom (Y_axis(g2)) by A67,FINSEQ_1:def 3;
A70:g2/.1=g2.1 by A68,FINSEQ_4:24;
A71:1<=len f2 by A1,AXIOMS:22;
then A72:g2/.1=f2/.1 by A3,A70,FINSEQ_4:24;
g2/.len g2=g2.(len g2) by A68,FINSEQ_4:24;
then A73:g2/.len g2=f2/.len f2 by A3,A71,FINSEQ_4:24;
1 in Seg len f2 by A71,FINSEQ_1:3;
then A74:1 in dom (Y_axis(f2)) by A66,FINSEQ_1:def 3;
i in Seg len g2 by A65,A67,FINSEQ_1:def 3;
then A75:i in dom g2 by FINSEQ_1:def 3; then g2.i in rng g2 by FUNCT_1:def
5;
then consider y being set such that
A76:y in dom f2 & g2.i=f2.y by A3,FUNCT_1:def 5;
reconsider j=y as Nat by A76;
f2.j=f2/.j by A76,FINSEQ_4:def 4;
then A77:j in dom f2 & g2/.i=f2/.j by A75,A76,FINSEQ_4:def 4;
j in Seg len f2 by A76,FINSEQ_1:def 3;
then A78:j in dom (Y_axis(f2)) by A66,FINSEQ_1:def 3;
then A79:(Y_axis(f2)).1 <= Y_axis(f2).j
& Y_axis(f2).j <= (Y_axis(f2)).(len f2) by A1,GOBOARD4:def 1;
A80:Y_axis(f2).j =(f2/.j)`2 by A78,GOBOARD1:def 4;
len f2 in Seg len f2 by A71,FINSEQ_1:3;
then len f2 in dom (Y_axis(f2)) by A66,FINSEQ_1:def 3;
then A81:(g2/.1)`2<=(g2/.i)`2 & (g2/.i)`2<=(g2/.len g2)`2
by A72,A73,A74,A77,A79,A80,GOBOARD1:def 4;
A82:Y_axis(g2).i =(g2/.i)`2 by A65,GOBOARD1:def 4;
len g2 in Seg len (Y_axis(g2)) by A67,A68,FINSEQ_1:3;
then len g2 in dom (Y_axis(g2)) by FINSEQ_1:def 3;
hence thesis by A69,A81,A82,GOBOARD1:def 4;
end;
then A83:Y_axis(g2) lies_between (Y_axis(g2)).1, (Y_axis(g2)).(len g2)
by GOBOARD4:def 1;
A84:for k being Nat st k in dom g1 & k+1 in dom g1 holds g1/.k <> g1/.(k+1)
proof let k be Nat;assume A85:k in dom g1 & k+1 in dom g1;
k<k+1 by NAT_1:38;
then A86:g1.k<>g1.(k+1) by A2,A85,FUNCT_1:def 8;
g1.k=g1/.k by A85,FINSEQ_4:def 4;
hence thesis by A85,A86,FINSEQ_4:def 4;
end;
for k being Nat st k in dom g2 & k+1 in dom g2 holds g2/.k <> g2/.(k+1)
proof let k be Nat;assume A87:k in dom g2 & k+1 in dom g2;
k<k+1 by NAT_1:38;
then A88:g2.k<>g2.(k+1) by A3,A87,FUNCT_1:def 8;
g2.k=g2/.k by A87,FINSEQ_4:def 4;
hence thesis by A87,A88,FINSEQ_4:def 4;
end;
then L~g1 meets L~g2 by A2,A3,A22,A43,A64,A83,A84,GOBOARD4:4;
then A89: L~g1 /\ L~g2 <> {} by XBOOLE_0:def 7;
L~g1 /\ L~g2 c= L~f1 /\ L~f2 by A2,A3,XBOOLE_1:27;
then L~f1 /\ L~f2 <> {} by A89,XBOOLE_1:3;
hence thesis by XBOOLE_0:def 7;
end;
begin :: NORM OF POINTS IN TOPREAL n
theorem Th31: for a,b,r1,r2 being Real
st a<=r1 & r1<=b & a<=r2 & r2<=b holds
abs(r1-r2)<=b-a
proof let a,b,r1,r2 be Real;
assume A1:a<=r1 & r1<=b & a<=r2 & r2<=b;
per cases;
suppose r1-r2>=0;
then A2:abs(r1-r2)=r1-r2 by ABSVALUE:def 1;
A3:r1-r2<=b-r2 by A1,REAL_1:49;
b-r2<=b-a by A1,REAL_2:106;
hence thesis by A2,A3,AXIOMS:22;
suppose r1-r2<0;
then A4:abs(r1-r2)=-(r1-r2) by ABSVALUE:def 1 .=r2-r1 by XCMPLX_1:143;
A5:r2-r1<=b-r1 by A1,REAL_1:49;
b-r1<=b-a by A1,REAL_2:106;
hence thesis by A4,A5,AXIOMS:22;
end;
definition let n;let p be Point of TOP-REAL n;
redefine func |. p .| means
:Def5: for w being Element of REAL n st p=w holds it=|.w.|;
compatibility
proof let r be Real;
thus r = |. p .| implies for w being Element of REAL n st p=w holds r=|.w.|
by TOPRNS_1:def 6;
reconsider y = p as Element of REAL n by EUCLID:25;
assume for w being Element of REAL n st p=w holds r=|.w.|;
then r=|.y.|;
hence r = |. p .| by TOPRNS_1:def 6;
end;
end;
reserve p,p1,p2 for Point of TOP-REAL n;
canceled 13;
theorem Th45: for x1,x2 being Point of Euclid n st x1=p1 & x2=p2 holds
|.p1 - p2.| = dist(x1,x2)
proof let x1,x2 be Point of Euclid n;
assume A1:x1=p1 & x2=p2;
Euclid n= MetrStruct(#REAL n,Pitag_dist n#) by EUCLID:def 7;
then reconsider x1'=x1,x2'=x2 as Element of REAL n;
p1-p2=x1'-x2' by A1,EUCLID:def 13;
then |.p1-p2.|=|.x1'-x2'.| by Def5;
then A2:(Pitag_dist n).(x1',x2')=|.p1-p2.| by EUCLID:def 6;
Euclid n = MetrStruct(#REAL n,Pitag_dist n#) by EUCLID:def 7;
hence thesis by A2,METRIC_1:def 1;
end;
theorem Th46: for p being Point of TOP-REAL 2 holds
(|.p.|)^2 = (p`1)^2+(p`2)^2
proof let p be Point of TOP-REAL 2;
reconsider w=p as Element of REAL 2 by EUCLID:25;
A1:|.p.|=|.w.| by Def5;
A2:|.w.| = sqrt Sum sqr w by EUCLID:def 5;
0 <= Sum sqr w by RVSUM_1:116;
then A3: (|.p.|)^2=Sum sqr w by A1,A2,SQUARE_1:def 4;
A4: p`1=w.1 by EUCLID:def 14;
A5: p`2=w.2 by EUCLID:def 15;
A6:len sqr w =2 by FINSEQ_2:109;
A7:(sqr w).1=(p`1)^2 by A4,RVSUM_1:78;
(sqr w).2=(p`2)^2 by A5,RVSUM_1:78;
then sqr w=<*(p`1)^2,(p`2)^2*> by A6,A7,FINSEQ_1:61;
hence thesis by A3,RVSUM_1:107;
end;
theorem Th47: for p being Point of TOP-REAL 2 holds
|.p.| = sqrt((p`1)^2+(p`2)^2)
proof let p be Point of TOP-REAL 2;
A1:(|.p.|)^2= (p`1)^2+(p`2)^2 by Th46;
|.p.| >=0 by TOPRNS_1:26;
hence thesis by A1,SQUARE_1:89;
end;
theorem Th48: for p being Point of TOP-REAL 2 holds |.p.|<=abs(p`1)+abs(p`2)
proof let p be Point of TOP-REAL 2;
A1:(|.p.|)^2= (p`1)^2+(p`2)^2 by Th46;
|.p.| >=0 by TOPRNS_1:26;
then sqrt((p`1)^2+(p`2)^2)=|.p.| by A1,SQUARE_1:89;
hence thesis by Th2;
end;
theorem Th49: for p1,p2 being Point of TOP-REAL 2 holds
|.p1-p2.|<=abs(p1`1-p2`1)+abs(p1`2-p2`2)
proof let p1,p2 be Point of TOP-REAL 2;
p1`1-p2`1=(p1-p2)`1 & p1`2-p2`2=(p1-p2)`2 by TOPREAL3:8;
hence thesis by Th48;
end;
theorem Th50: for p being Point of TOP-REAL 2 holds
abs(p`1)<=|.p.| & abs(p`2)<=|.p.|
proof let p be Point of TOP-REAL 2;
|.p.| = sqrt((p`1)^2+(p`2)^2) by Th47;
hence thesis by Th3;
end;
theorem Th51: for p1,p2 being Point of TOP-REAL 2 holds
abs(p1`1-p2`1)<=|.p1-p2.| & abs(p1`2-p2`2)<=|.p1-p2.|
proof let p1,p2 be Point of TOP-REAL 2;
p1`1-p2`1=(p1-p2)`1 & p1`2-p2`2=(p1-p2)`2 by TOPREAL3:8;
hence thesis by Th50;
end;
theorem Th52: p in LSeg(p1,p2) implies ex r st
0<=r & r<=1 & p=(1-r)*p1+r*p2
proof assume p in LSeg(p1,p2);
then p in { (1-r)*p1 + r*p2 : 0 <= r & r <= 1 } by TOPREAL1:def 4;
then consider r1 such that
A1: p=(1-r1)*p1 + r1*p2 &( 0 <= r1 & r1 <= 1);
thus thesis by A1;
end;
theorem Th53: p in LSeg(p1,p2) implies
|.p-p1.|<=|.p1-p2.| & |.p-p2.|<=|.p1-p2.|
proof assume A1:p in LSeg(p1,p2);
then consider r such that
A2: 0<=r & r<=1 & p=(1-r)*p1+r*p2 by Th52;
p-p1= (1-r)*p1+r*p2+-p1 by A2,EUCLID:45
.= (1-r)*p1+-p1+r*p2 by EUCLID:30
.=(1-r)*p1-p1+r*p2 by EUCLID:45
.=(1-r)*p1-1*p1+r*p2 by EUCLID:33
.=(1-r-1)*p1+r*p2 by EUCLID:54
.=(1+-r-1)*p1+r*p2 by XCMPLX_0:def 8
.=(-r)*p1+r*p2 by XCMPLX_1:26
.=r*p2+-r*p1 by EUCLID:44
.=r*p2+r*(-p1) by EUCLID:44
.=r*(p2+(-p1)) by EUCLID:36
.=r*(p2-p1) by EUCLID:45;
then |.p-p1.|=abs(r)*|.p2-p1.| by TOPRNS_1:8
.=abs(r)*|.p1-p2.| by TOPRNS_1:28 .=r*|.p1-p2.| by A2,ABSVALUE:def 1;
then A3:|.p1-p2.|- |.p-p1.|=1*|.p1-p2.|-r*|.p1-p2.|.=(1-r)*|.p1-p2.|
by XCMPLX_1:40;
A4:0<=1-r by A2,SQUARE_1:12;
|.p1-p2.|>=0 by TOPRNS_1:26;
then A5:|.p1-p2.|- |.p-p1.|>=0 by A3,A4,SQUARE_1:19;
consider r such that
A6: 0<=r & r<=1 & p=(1-r)*p2+r*p1 by A1,Th52;
p-p2= (1-r)*p2+r*p1+-p2 by A6,EUCLID:45
.= (1-r)*p2+-p2+r*p1 by EUCLID:30
.=(1-r)*p2-p2+r*p1 by EUCLID:45
.=(1-r)*p2-1*p2+r*p1 by EUCLID:33
.=(1-r-1)*p2+r*p1 by EUCLID:54
.=(1+-r-1)*p2+r*p1 by XCMPLX_0:def 8
.=(-r)*p2+r*p1 by XCMPLX_1:26
.=r*p1+-r*p2 by EUCLID:44
.=r*p1+r*(-p2) by EUCLID:44
.=r*(p1+(-p2)) by EUCLID:36
.=r*(p1-p2) by EUCLID:45;
then |.p-p2.|=abs(r)*|.p1-p2.| by TOPRNS_1:8
.=r*|.p1-p2.| by A6,ABSVALUE:def 1;
then A7:|.p1-p2.|- |.p-p2.|=1*|.p1-p2.|-r*|.p1-p2.|.=(1-r)*|.p1-p2.|
by XCMPLX_1:40;
A8:0<=1-r by A6,SQUARE_1:12;
|.p1-p2.|>=0 by TOPRNS_1:26;
then |.p1-p2.|- |.p-p2.|>=0 by A7,A8,SQUARE_1:19;
hence thesis by A5,REAL_2:105;
end;
begin :: EXTENDED GOBOARD THEOREM AND FASHODA MEET THEOREM
reserve M for non empty MetrSpace;
theorem Th54: for P,Q being Subset of TopSpaceMetr(M) st
P <> {} & P is compact & Q <> {} & Q is compact holds
min_dist_min(P,Q)>=0
proof let P,Q be Subset of TopSpaceMetr(M);
assume P <> {} & P is compact & Q <> {} & Q is compact;
then consider x1,x2 being Point of M such that
A1:x1 in P & x2 in Q &
dist(x1,x2) = min_dist_min(P,Q) by WEIERSTR:36;
thus thesis by A1,METRIC_1:5;
end;
theorem Th55: for P,Q being Subset of TopSpaceMetr(M) st
P <> {} & P is compact & Q <> {} & Q is compact holds
P misses Q iff min_dist_min(P,Q)>0
proof let P,Q be Subset of TopSpaceMetr(M);
assume A1:P <> {} & P is compact & Q <> {} & Q is compact;
then consider x1,x2 being Point of M such that
A2:x1 in P & x2 in Q &
dist(x1,x2) = min_dist_min(P,Q) by WEIERSTR:36;
A3: the distance of M is discerning by METRIC_1:def 8;
A4: now assume not min_dist_min(P,Q)>0;
then dist(x1,x2)=0 by A1,A2,Th54;
then (the distance of M).(x1,x2)=0 by METRIC_1:def 1;
then x1=x2 by A3,METRIC_1:def 4;
hence P /\ Q <> {} by A2,XBOOLE_0:def 3;
end;
now assume A5:P /\ Q <>{};
consider p being Element of P /\ Q;
A6:p in P & p in Q by A5,XBOOLE_0:def 3;
then reconsider p'=p as Element of TopSpaceMetr(M);
reconsider q=p' as Point of M by TOPMETR:16;
the distance of M is Reflexive by METRIC_1:def 7;
then (the distance of M).(q,q)=0 by METRIC_1:def 3;
then dist(q,q)=0 by METRIC_1:def 1;
hence not min_dist_min(P,Q)>0 by A1,A6,WEIERSTR:40;
end;
hence thesis by A4,XBOOLE_0:def 7;
end;
:: Approximation of finite sequence by special finite sequence
theorem Th56: for f being FinSequence of TOP-REAL 2,a,c,d being Real st
1<=len f & X_axis(f) lies_between (X_axis(f)).1, (X_axis(f)).(len f) &
Y_axis(f) lies_between c, d & a>0 &
(for i st 1<=i & i+1<=len f holds
|. f/.i-f/.(i+1) .|<a)
holds
ex g being FinSequence of TOP-REAL 2 st g is special &
g.1=f.1 & g.len g=f.len f & len g>=len f &
X_axis(g) lies_between (X_axis(f)).1, (X_axis(f)).(len f) &
Y_axis(g) lies_between c, d &
(for j st j in dom g holds ex k st k in dom f & |. g/.j - f/.k .|<a)&
(for j st 1<=j & j+1<=len g holds |. g/.j - g/.(j+1) .|<a)
proof let f be FinSequence of TOP-REAL 2,a,c,d be Real;
assume A1:1<=len f &
X_axis(f) lies_between (X_axis(f)).1, (X_axis(f)).(len f) &
Y_axis(f) lies_between c, d & a>0 &
(for i st 1<=i & i+1<=len f holds |. f/.i-f/.(i+1) .|<a);
defpred P[set,set] means
(for j st $1=2*j or $1=2*j -'1 holds
($1 =2*j implies $2=|[(f/.j)`1,(f/.(j+1))`2]|)
&($1 =2*j-'1 implies $2=f/.j));
A2: for k st k in Seg (2*(len f)-'1)
ex x st P[k,x]
proof let k;assume
A3: k in Seg (2*(len f)-'1);
then A4:1<=k & k<=(2*(len f)-'1) by FINSEQ_1:3;
per cases by GROUP_4:100;
suppose A5:k mod 2=0;
consider i such that
A6: k=2*i+ (k mod 2) & k mod 2<2 by NAT_1:def 2;
for j st k=2*j or k=2*j -'1 holds
(k =2*j implies |[(f/.i)`1,(f/.(i+1))`2]|
=|[(f/.j)`1,(f/.(j+1))`2]|)
&(k =2*j-'1 implies |[(f/.i)`1,(f/.(i+1))`2]|=f/.j)
proof let j;assume A7:k=2*j or k=2*j -'1;
per cases by A7;
suppose k=2*j;
then i=2*j/2 by A5,A6,XCMPLX_1:90;
then A8: i=j by XCMPLX_1:90;
now assume
A9:k=2*j-'1; then k=2*j-1 by A4,JORDAN3:1;
then A10:k=2*j-2*1+2-1 by XCMPLX_1:27 .=2*(j-1)+(1+1)-1 by
XCMPLX_1:40
.=2*(j-1)+1+1-1 by XCMPLX_1:1
.=2*(j-1)+1 by XCMPLX_1:26;
now assume A11:j=0;
0-1<0; then 0-'1=0 by BINARITH:def 3;
hence contradiction by A3,A9,A11,FINSEQ_1:3;
end; then j>0 by NAT_1:19; then j>=0+1 by NAT_1:38;
then k= 2*(j-'1)+1 & 1<=2 by A10,SCMFSA_7:3;
hence contradiction by A5,NAT_1:def 2;
end;
hence thesis by A8;
suppose A12:k=2*j-'1; then k=2*j-1 by A4,JORDAN3:1;
then A13:k=2*j-2*1+2-1 by XCMPLX_1:27 .=2*(j-1)+(1+1)-1 by XCMPLX_1:
40
.=2*(j-1)+1+1-1 by XCMPLX_1:1
.=2*(j-1)+1 by XCMPLX_1:26;
now assume A14:j=0;
0-1<0; then 0-'1=0 by BINARITH:def 3;
hence contradiction by A3,A12,A14,FINSEQ_1:3;
end; then j>0 by NAT_1:19; then j>=0+1 by NAT_1:38;
then k= 2*(j-'1)+1 & 1<=2 by A13,SCMFSA_7:3;
hence thesis by A5,NAT_1:def 2;
end;
hence thesis;
suppose A15:k mod 2=1;
consider i such that
A16: k=2*i+ (k mod 2) & k mod 2<2 by NAT_1:def 2;
for j st k=2*j or k=2*j -'1 holds
(k =2*j implies f/.(i+1)=|[(f/.j)`1,(f/.(j+1))`2]|)
&(k =2*j-'1 implies f/.(i+1)=f/.j)
proof let j;assume A17:k=2*j or k=2*j -'1;
per cases by A17;
suppose k=2*j-'1;
then A18:k=2*j-1 by A4,JORDAN3:1;
A19:now assume
k=2*j-'1;
then k=2*j-1 by A4,JORDAN3:1;
then k=2*j-2*1+2-1 by XCMPLX_1:27 .=2*(j-1)+(1+1)-1 by XCMPLX_1:40
.=2*(j-1)+1+1-1 by XCMPLX_1:1
.=2*(j-1)+1 by XCMPLX_1:26;
then 2*(j-1)=2*i+1-1 by A15,A16,XCMPLX_1:26;
then 2*(j-1)/2=2*i/2 by XCMPLX_1:26;
then (j-1)=2*i/2 by XCMPLX_1:90;
then j-1+1=i+1 by XCMPLX_1:90;
hence f/.(i+1)=f/.j by XCMPLX_1:27;
end;
now assume k=2*j;
then k-k=1 by A18,XCMPLX_1:18;
hence contradiction by XCMPLX_1:14;
end;
hence thesis by A19;
suppose k=2*j;
then 2*j-2*i=1 by A15,A16,XCMPLX_1:26;
then A20:2*(j-i)=1 by XCMPLX_1:40;
then j-i>=0 by SQUARE_1:24;
then A21:j-i=j-'i by BINARITH:def 3;
j-i=0 or j-i>0 by A20,SQUARE_1:24;
then j-i>=0+1 by A20,A21,NAT_1:38;
then 2*(j-i)>=2*1 by AXIOMS:25;
hence thesis by A20;
end;
hence thesis;
end;
A22:for k being Nat,y1,y2 being set st k in Seg (2*(len f)-'1) &
P[k,y1] & P[k,y2] holds y1=y2
proof let k be Nat,y1,y2 be set;
assume A23: k in Seg (2*(len f)-'1) &
(for j st k=2*j or k=2*j -'1 holds
(k =2*j implies y1=|[(f/.j)`1,(f/.(j+1))`2]|)
&(k =2*j-'1 implies y1=f/.j))&
(for j st k=2*j or k=2*j -'1 holds
(k =2*j implies y2=|[(f/.j)`1,(f/.(j+1))`2]|)
&(k =2*j-'1 implies y2=f/.j));
per cases by GROUP_4:100;
suppose A24:k mod 2=0;
consider i such that
A25: k=2*i+ (k mod 2) & k mod 2<2 by NAT_1:def 2;
y1=|[(f/.i)`1,(f/.(i+1))`2]| by A23,A24,A25;
hence thesis by A23,A24,A25;
suppose A26:k mod 2=1;
consider i such that
A27: k=2*i+ (k mod 2) & k mod 2<2 by NAT_1:def 2;
k=2*i+2*1-(1+1)+1 by A26,A27,XCMPLX_1:26
.=2*(i+1)-(1+1)+1 by XCMPLX_1:8
.=2*(i+1)+1-(1+1) by XCMPLX_1:29
.=2*(i+1)+1-1-1 by XCMPLX_1:36;
then A28:k=2*(i+1)-1 by XCMPLX_1:26;
1<=1+i by NAT_1:37;
then 2*1<=2*(i+1) by AXIOMS:25;
then 1<=2*(i+1) by AXIOMS:22;
then A29:2*(i+1)-'1= 2*(i+1)-1 by SCMFSA_7:3;
then y1=f/.(i+1) by A23,A28;
hence thesis by A23,A28,A29;
end;
ex p being FinSequence st dom p = Seg (2*(len f)-'1)
& for k st k in Seg (2*(len f)-'1) holds
P[k,p.k] from SeqEx(A22,A2);
then consider p being FinSequence such that
A30: dom p = Seg (2*(len f)-'1)
& for k st k in Seg (2*(len f)-'1) holds
(for j st k=2*j or k=2*j -'1 holds
(k =2*j implies p.k=|[(f/.j)`1,(f/.(j+1))`2]|)
&(k =2*j-'1 implies p.k=f/.j));
A31:len p=(2*(len f)-'1) by A30,FINSEQ_1:def 3;
rng p c= the carrier of TOP-REAL 2
proof let y;assume y in rng p;
then consider x such that
A32:x in dom p & y=p.x by FUNCT_1:def 5;
A33:x in Seg len p by A32,FINSEQ_1:def 3;
reconsider i=x as Nat by A32;
A34:1 <= i & i <= len p by A33,FINSEQ_1:3;
per cases by GROUP_4:100;
suppose A35:i mod 2=0;
consider j such that
A36: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
p.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A32,A35,A36;
hence thesis by A32;
suppose A37:i mod 2=1;
consider j such that
A38: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
i=2*j+1+1-1 by A37,A38,XCMPLX_1:26
.=2*j+(1+1)-1 by XCMPLX_1:1
.=2*j+2*1-1;
then A39:i=2*(j+1)-1 by XCMPLX_1:8;
then 2*(j+1)-'1 =2*(j+1)-1 by A34,JORDAN3:1;
then p.i=f/.(j+1) by A30,A32,A39;
hence thesis by A32;
end;
then reconsider g1=p as FinSequence of TOP-REAL 2 by FINSEQ_1:def 4;
for i st 1 <= i & i+1 <= len g1 holds
(g1/.i)`1 = (g1/.(i+1))`1 or (g1/.i)`2 = (g1/.(i+1))`2
proof let i;assume A40:1 <= i & i+1 <= len g1;
then A41:i<len g1 by NAT_1:38;
A42:1<i+1 by A40,NAT_1:38;
then A43:i+1 in Seg len g1 by A40,FINSEQ_1:3;
A44: i in Seg (2*(len f)-'1) by A31,A40,A41,FINSEQ_1:3;
A45:g1.i=g1/.i by A40,A41,FINSEQ_4:24;
A46:g1.(i+1)=g1/.(i+1) by A40,A42,FINSEQ_4:24;
per cases by GROUP_4:100;
suppose A47:i mod 2=0;
consider j such that
A48: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
A49:g1.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A44,A47,A48;
i+1=2*j+1+1-1 by A47,A48,XCMPLX_1:26
.=2*j+(1+1)-1 by XCMPLX_1:1
.=2*j+2*1-1;
then A50:i+1=2*(j+1)-1 by XCMPLX_1:8;
1<=1+i by NAT_1:29;
then 2*(j+1)-'1 =2*(j+1)-1 by A50,JORDAN3:1;
then g1.(i+1)=f/.(j+1) by A30,A31,A43,A50;
hence thesis by A45,A46,A49,EUCLID:56;
suppose A51:i mod 2=1;
consider j such that
A52: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
i=2*j+1+1-1 by A51,A52,XCMPLX_1:26
.=2*j+(1+1)-1 by XCMPLX_1:1
.=2*j+2*1-1;
then A53:i=2*(j+1)-1 by XCMPLX_1:8;
then 2*(j+1)-'1 =2*(j+1)-1 by A40,JORDAN3:1;
then A54: g1.i=f/.(j+1) by A30,A44,A53;
i+1=2*j+(1+1) by A51,A52,XCMPLX_1:1
.=2*j+2*1
.=2*(j+1) by XCMPLX_1:8;
then g1.(i+1)=|[(f/.(j+1))`1,(f/.(j+1+1))`2]| by A30,A31,A43;
hence thesis by A45,A46,A54,EUCLID:56;
end;
then A55:g1 is special by TOPREAL1:def 7;
A56:f.len f=f/.len f by A1,FINSEQ_4:24;
A57: 2*(len f)>=2*1 by A1,AXIOMS:25;
then 2*(len f)>=1 by AXIOMS:22;
then A58:2*(len f)-'1= 2*(len f)-1 by SCMFSA_7:3;
A59:2*(len f)-1>= 1+1-1 by A57,REAL_1:49;
then A60: 1 in Seg (2*(len f)-'1) by A58,FINSEQ_1:3;
2*1-'1=1+1-'1 .=1 by BINARITH:39;
then p.1=f/.1 by A30,A60;
then A61:g1.1=f.1 by A1,FINSEQ_4:24;
(2*(len f)-'1) in Seg (2*(len f)-'1) by A58,A59,FINSEQ_1:3;
then A62:g1.len g1=f.len f by A30,A31,A56;
len f + len f>=len f+1 by A1,AXIOMS:24;
then 2*(len f)>=len f +1 by XCMPLX_1:11;
then 2*(len f)-1>=len f +1-1 by REAL_1:49;
then A63:len g1>=len f by A31,A58,XCMPLX_1:26;
for i st i in dom (X_axis(g1)) holds (X_axis(f)).1 <= (X_axis(g1)).i
& (X_axis(g1)).i <= (X_axis(f)).(len f)
proof let i;assume
A64:i in dom (X_axis(g1));
then A65: i in Seg len (X_axis(g1)) by FINSEQ_1:def 3;
then i in Seg len g1 by GOBOARD1:def 3;
then A66: 1<=i & i<=len g1 by FINSEQ_1:3;
A67:i in Seg len g1 by A65,GOBOARD1:def 3;
A68:(X_axis(g1)).i = (g1/.i)`1 by A64,GOBOARD1:def 3;
A69:len (X_axis(f))=len f by GOBOARD1:def 3;
A70:g1/.i=(g1.i) by A66,FINSEQ_4:24;
per cases by GROUP_4:100;
suppose A71:i mod 2=0;
consider j such that
A72: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
g1.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A31,A67,A71,A72;
then A73:(g1/.i)`1=(f/.j)`1 by A70,EUCLID:56;
j<>0 by A65,A71,A72,FINSEQ_1:3;
then j>0 by NAT_1:19;
then A74: j>=0+1 by NAT_1:38;
2*j+1<=2*(len f)-1+1 by A31,A58,A66,A71,A72,AXIOMS:24;
then 2*j+1<=2*(len f) by XCMPLX_1:27;
then 2*j<2*(len f) by NAT_1:38;
then 2*j/2<2*(len f)/2 by REAL_1:73;
then j<2*(len f)/2 by XCMPLX_1:90;
then j<len f by XCMPLX_1:90;
then j in Seg len f by A74,FINSEQ_1:3;
then A75:j in dom (X_axis(f)) by A69,FINSEQ_1:def 3;
then (X_axis(f)).j = (f/.j)`1 by GOBOARD1:def 3;
hence thesis by A1,A68,A73,A75,GOBOARD4:def 1;
suppose A76:i mod 2=1;
consider j such that
A77: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
i=2*j+1+1-1 by A76,A77,XCMPLX_1:26;
then i=2*j+(1+1)-1 by XCMPLX_1:1;
then i=2*j+2*1-1;
then A78:i=2*(j+1)-1 by XCMPLX_1:8;
then 2*(j+1)-'1 =2*(j+1)-1 by A66,JORDAN3:1;
then A79:(g1/.i)`1=(f/.(j+1))`1 by A30,A31,A67,A70,A78;
A80:1<=j+1 by NAT_1:29;
2*j+1<=2*(len f)-1+1 by A31,A58,A66,A76,A77,NAT_1:38;
then 2*j+1<=2*(len f) by XCMPLX_1:27;
then 2*j<2*(len f) by NAT_1:38;
then 2*j/2<2*(len f)/2 by REAL_1:73;
then j<2*(len f)/2 by XCMPLX_1:90;
then j<len f by XCMPLX_1:90;
then j+1<=len f by NAT_1:38;
then j+1 in Seg len f by A80,FINSEQ_1:3;
then A81:j+1 in dom (X_axis(f)) by A69,FINSEQ_1:def 3;
then (X_axis(f)).(j+1) = (f/.(j+1))`1 by GOBOARD1:def 3;
hence thesis by A1,A68,A79,A81,GOBOARD4:def 1;
end;
then A82:X_axis(g1) lies_between (X_axis(f)).1, (X_axis(f)).(len f)
by GOBOARD4:def 1;
for i st i in dom (Y_axis(g1)) holds
c <= (Y_axis(g1)).i & (Y_axis(g1)).i <= d
proof let i;assume
A83:i in dom (Y_axis(g1));
then A84: i in Seg len (Y_axis(g1)) by FINSEQ_1:def 3;
then i in Seg len g1 by GOBOARD1:def 4;
then A85: 1<=i & i<=len g1 by FINSEQ_1:3;
A86:i in Seg len g1 by A84,GOBOARD1:def 4;
A87:(Y_axis(g1)).i = (g1/.i)`2 by A83,GOBOARD1:def 4;
A88:len (Y_axis(f))=len f by GOBOARD1:def 4;
A89:g1/.i=(g1.i) by A85,FINSEQ_4:24;
per cases by GROUP_4:100;
suppose A90:i mod 2=0;
consider j such that
A91: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
g1.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A31,A86,A90,A91;
then A92:(g1/.i)`2=(f/.(j+1))`2 by A89,EUCLID:56;
A93:1<=j+1 by NAT_1:29;
2*j+1<=2*(len f)-1+1 by A31,A58,A85,A90,A91,AXIOMS:24;
then 2*j+1<=2*(len f) by XCMPLX_1:27;
then 2*j<2*(len f) by NAT_1:38;
then 2*j/2<2*(len f)/2 by REAL_1:73;
then j<2*(len f)/2 by XCMPLX_1:90;
then j<len f by XCMPLX_1:90;
then j+1<=len f by NAT_1:38;
then j+1 in Seg len f by A93,FINSEQ_1:3;
then A94:j+1 in dom (Y_axis(f)) by A88,FINSEQ_1:def 3;
then (Y_axis(f)).(j+1) = (f/.(j+1))`2 by GOBOARD1:def 4;
hence thesis by A1,A87,A92,A94,GOBOARD4:def 1;
suppose A95:i mod 2=1;
consider j such that
A96: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
i=2*j+1+1-1 by A95,A96,XCMPLX_1:26;
then i=2*j+(1+1)-1 by XCMPLX_1:1;
then i=2*j+2*1-1;
then A97:i=2*(j+1)-1 by XCMPLX_1:8;
then 2*(j+1)-'1 =2*(j+1)-1 by A85,JORDAN3:1;
then A98:(g1/.i)`2=(f/.(j+1))`2 by A30,A31,A86,A89,A97;
A99:1<=j+1 by NAT_1:29;
2*j+1<=2*(len f)-1+1 by A31,A58,A85,A95,A96,NAT_1:38;
then 2*j+1<=2*(len f) by XCMPLX_1:27;
then 2*j<2*(len f) by NAT_1:38;
then 2*j/2<2*(len f)/2 by REAL_1:73;
then j<2*(len f)/2 by XCMPLX_1:90;
then j<len f by XCMPLX_1:90;
then j+1<=len f by NAT_1:38;
then j+1 in Seg len f by A99,FINSEQ_1:3;
then A100:j+1 in dom (Y_axis(f)) by A88,FINSEQ_1:def 3;
then (Y_axis(f)).(j+1) = (f/.(j+1))`2 by GOBOARD1:def 4;
hence thesis by A1,A87,A98,A100,GOBOARD4:def 1;
end;
then A101:Y_axis(g1) lies_between c, d by GOBOARD4:def 1;
A102:for i st i in dom g1 holds
ex k st k in dom f & |. g1/.i - f/.k .| < a
proof let i;assume A103:i in dom g1;
then A104: i in Seg len g1 by FINSEQ_1:def 3;
then A105:1<=i & i<=len g1 by FINSEQ_1:3;
then A106:g1.i=g1/.i by FINSEQ_4:24;
per cases by GROUP_4:100;
suppose A107:i mod 2=0;
consider j such that
A108: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
A109:g1.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A103,A107,A108;
then A110:(g1/.i)`1=(f/.j)`1 by A106,EUCLID:56;
A111:(g1/.i)`2=(f/.(j+1))`2 by A106,A109,EUCLID:56;
A112:g1/.i-f/.j=|[(g1/.i)`1-(f/.j)`1,(g1/.i)`2-(
(f/.j))`2]| by EUCLID:65
.=|[0,(g1/.i)`2-(f/.j)`2]| by A110,XCMPLX_1:14;
then (g1/.i-f/.j)`2=(g1/.i)`2-(f/.j)`2 by EUCLID:56;
then |.g1/.i-f/.j.|=
sqrt(((g1/.i-f/.j)`1)^2+((g1/.i)`2-(f/.j)`2)^2)
by Th47
.= sqrt(0+(((f/.(j+1))`2-(f/.j)`2))^2) by A111,A112,EUCLID:56,SQUARE_1
:60
.= sqrt((((f/.(j+1))`2-(f/.j)`2))^2);
then |.g1/.i-f/.j.|=abs((f/.(j+1))`2-(f/.j)`2) by SQUARE_1:91
.=abs((f/.j)`2 -(f/.(j+1))`2) by UNIFORM1:13;
then A113:|.g1/.i-f/.j.|
<=|.f/.j-f/.(j+1).| by Th51;
j<>0 by A104,A107,A108,FINSEQ_1:3;
then j>0 by NAT_1:19;
then A114: j>=0+1 by NAT_1:38;
2*j+1<=2*(len f)-1+1 by A31,A58,A105,A107,A108,AXIOMS:24;
then 2*j+1<=2*(len f) by XCMPLX_1:27;
then 2*j<2*(len f) by NAT_1:38;
then 2*j/2<2*(len f)/2 by REAL_1:73;
then j<2*(len f)/2 by XCMPLX_1:90;
then A115: j<len f by XCMPLX_1:90;
then j+1<=len f by NAT_1:38;
then |. f/.j-f/.(j+1) .|<a by A1,A114;
then A116: |. g1/.i - f/.j .|<a by A113,AXIOMS:22;
j in dom f by A114,A115,FINSEQ_3:27;
hence thesis by A116;
suppose A117:i mod 2=1;
consider j such that
A118: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
i=2*j+1+1-1 by A117,A118,XCMPLX_1:26
.=2*j+(1+1)-1 by XCMPLX_1:1
.=2*j+2*1-1;
then A119:i=2*(j+1)-1 by XCMPLX_1:8;
then 2*(j+1)-'1 =2*(j+1)-1 by A105,JORDAN3:1;
then g1.i=f/.(j+1) by A30,A103,A119;
then A120:|.g1/.i-f/.(j+1).|=|.0.REAL 2.| by A106,EUCLID:46
.=0 by TOPRNS_1:24;
2*j+1+1<=2*(len f)-1+1 by A31,A58,A105,A117,A118,AXIOMS:24;
then 2*j+1+1<=2*(len f) by XCMPLX_1:27;
then 2*j+1<2*(len f) by NAT_1:38;
then 2*j<2*(len f) by NAT_1:38;
then 2*j/2<2*(len f)/2 by REAL_1:73;
then j<2*(len f)/2 by XCMPLX_1:90;
then j<len f by XCMPLX_1:90;
then A121: j+1<=len f by NAT_1:38;
1<=j+1 by NAT_1:29;
then j+1 in dom f by A121,FINSEQ_3:27;
hence thesis by A1,A120;
end;
for i st 1<=i & i+1<=len g1 holds |. g1/.i - g1/.(i+1) .|<a
proof let i;assume A122:1<=i & i+1<=len g1;
then i<=len g1 by NAT_1:38;
then A123:i in Seg len g1 by A122,FINSEQ_1:3;
A124:1<=i & i<=len g1 by A122,NAT_1:38;
A125:1<=i+1 by NAT_1:29;
then A126: i+1 in Seg (2*(len f)-'1) by A31,A122,FINSEQ_1:3;
A127:g1.(i+1)=g1/.(i+1) by A122,A125,FINSEQ_4:24;
A128:g1.i=g1/.i by A124,FINSEQ_4:24;
per cases by GROUP_4:100;
suppose A129:i mod 2=0;
consider j such that
A130: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
A131:g1.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A31,A123,A129,A130;
i+1=2*j+1+1-1 by A129,A130,XCMPLX_1:26
.=2*j+(1+1)-1 by XCMPLX_1:1
.=2*j+2*1-1;
then A132:i+1=2*(j+1)-1 by XCMPLX_1:8;
1<=1+i by NAT_1:29;
then 2*(j+1)-'1 =2*(j+1)-1 by A132,JORDAN3:1;
then A133:g1.(i+1)=f/.(j+1) by A30,A126,A132;
A134:(g1/.i)`1=(f/.j)`1 by A128,A131,EUCLID:56;
A135:(g1/.i)`2=(f/.(j+1))`2 by A128,A131,EUCLID:56;
A136:(g1/.(i+1))`1=(f/.(j+1))`1 by A122,A125,A133,FINSEQ_4:24;
A137:(g1/.(i+1))`2=(f/.(j+1))`2 by A122,A125,A133,FINSEQ_4:24;
A138:g1/.i-g1/.(i+1)
=|[(g1/.i)`1-(g1/.(i+1))`1,(g1/.i)`2-(g1/.(i+1))`2]|
by EUCLID:65
.=|[(f/.j)`1-(f/.(j+1))`1,0]|
by A134,A135,A136,A137,XCMPLX_1:14;
then A139:(g1/.i-g1/.(i+1))`1=(f/.j)`1-(f/.(j+1))`1 by EUCLID:56;
|.g1/.i-g1/.(i+1).|=
sqrt((((g1/.i-g1/.(i+1))`1))^2+(((g1/.i-g1/.(i+1))`2))^2)
by Th47
.= sqrt((((f/.j)`1-(f/.(j+1))`1))^2+0) by A138,A139,EUCLID:56,SQUARE_1
:60
.= sqrt((((f/.j)`1-(f/.(j+1))`1))^2);
then |.g1/.i-g1/.(i+1).|=abs((f/.j)`1-(f/.(j+1))`1)
by SQUARE_1:91;
then A140:|.g1/.i-g1/.(i+1).|
<=|.f/.j-f/.(j+1).| by Th51;
j<>0 by A122,A129,A130;
then j>0 by NAT_1:19;
then A141: j>=0+1 by NAT_1:38;
2*j+1<=2*(len f)-1+1 by A31,A58,A122,A129,A130,NAT_1:38;
then 2*j+1<=2*(len f) by XCMPLX_1:27;
then 2*j<2*(len f) by NAT_1:38;
then 2*j/2<2*(len f)/2 by REAL_1:73;
then j<2*(len f)/2 by XCMPLX_1:90;
then j<len f by XCMPLX_1:90;
then j+1<=len f by NAT_1:38;
then |. f/.j-f/.(j+1) .|<a by A1,A141;
hence thesis by A140,AXIOMS:22;
suppose A142:i mod 2=1;
consider j such that
A143: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
i=2*j+1+1-1 by A142,A143,XCMPLX_1:26;
then i=2*j+(1+1)-1 by XCMPLX_1:1;
then i=2*j+2*1-1;
then A144:i=2*(j+1)-1 by XCMPLX_1:8;
then A145: 2*(j+1)-'1 =2*(j+1)-1 by A122,JORDAN3:1;
i+1=2*j+(1+1) by A142,A143,XCMPLX_1:1
.=2*j+2*1;
then A146:i+1=2*(j+1) by XCMPLX_1:8;
then A147:g1/.(i+1)=|[(f/.(j+1))`1,(f/.(j+1+1))`2]| by A30,A126,A127;
then A148:(g1/.(i+1))`1=(f/.(j+1))`1 by EUCLID:56;
A149:(g1/.(i+1))`2=(f/.(j+1+1))`2 by A147,EUCLID:56;
A150:(g1/.i)`1=(f/.(j+1))`1 by A30,A31,A123,A128,A144,A145;
A151:(g1/.i)`2=(f/.(j+1))`2 by A30,A31,A123,A128,A144,A145;
A152:g1/.i-g1/.(i+1)
=|[(g1/.i)`1-(g1/.(i+1))`1,(g1/.i)`2-(g1/.(i+1))`2]| by EUCLID:65
.=|[0,(f/.(j+1))`2-(f/.(j+1+1))`2]|
by A148,A149,A150,A151,XCMPLX_1:14;
then A153:(g1/.i-g1/.(i+1))`1=0 by EUCLID:56;
|.g1/.i-g1/.(i+1).|=
sqrt((((g1/.i-g1/.(i+1))`1))^2+(((g1/.i-
g1/.(i+1))`2))^2) by Th47
.= sqrt((((f/.(j+1))`2-(f/.(j+1+1))`2))^2) by A152,A153,EUCLID:56,
SQUARE_1:60;
then |.g1/.i-g1/.(i+1).|=abs((f/.(j+1))`2-(f/.(j+1+1))`2)
by SQUARE_1:91;
then A154:|.g1/.i-g1/.(i+1).|
<=|.f/.(j+1)-f/.(j+1+1).| by Th51;
A155: j+1>=1 by NAT_1:29;
2*(j+1)+1<=2*(len f)-1+1 by A31,A58,A122,A146,AXIOMS:24;
then 2*(j+1)+1<=2*(len f) by XCMPLX_1:27;
then 2*(j+1)<2*(len f) by NAT_1:38;
then 2*(j+1)/2<2*(len f)/2 by REAL_1:73;
then (j+1)<2*(len f)/2 by XCMPLX_1:90;
then (j+1)<len f by XCMPLX_1:90;
then (j+1)+1<=len f by NAT_1:38;
then |. f/.(j+1)-f/.(j+1+1) .|<a by A1,A155;
hence thesis by A154,AXIOMS:22;
end;
hence thesis by A55,A61,A62,A63,A82,A101,A102;
end;
theorem Th57: for f being FinSequence of TOP-REAL 2,a,c,d being Real st
1<=len f &
Y_axis(f) lies_between (Y_axis(f)).1, (Y_axis(f)).(len f) &
X_axis(f) lies_between c, d & a>0 &
(for i st 1<=i & i+1<=len f holds |. (f/.i)-(f/.(i+1)) .|<a)
holds
ex g being FinSequence of TOP-REAL 2 st g is special &
g.1=f.1 & g.len g=f.len f & len g>=len f &
Y_axis(g) lies_between (Y_axis(f)).1, (Y_axis(f)).(len f) &
X_axis(g) lies_between c, d &
(for j st j in dom g holds ex k st k in dom f & |. g/.j - f/.k .| < a)&
(for j st 1<=j & j+1<=len g holds |. g/.j - g/.(j+1) .|<a)
proof let f be FinSequence of TOP-REAL 2,a,c,d be Real;
assume A1:1<=len f &
Y_axis(f) lies_between (Y_axis(f)).1, (Y_axis(f)).(len f) &
X_axis(f) lies_between c, d & a>0 &
(for i st 1<=i & i+1<=len f holds |. f/.i-f/.(i+1) .|<a);
defpred P[set,set] means
(for j st $1=2*j or $1=2*j -'1 holds
($1 =2*j implies $2=|[(f/.j)`1,(f/.(j+1))`2]|)
&($1 =2*j-'1 implies $2=f/.j));
A2: for k st k in Seg (2*(len f)-'1) ex x st P[k,x]
proof let k;assume
A3: k in Seg (2*(len f)-'1);
then A4:1<=k & k<=2*(len f)-'1 by FINSEQ_1:3;
per cases by GROUP_4:100;
suppose A5:k mod 2=0;
consider i such that
A6: k=2*i+ (k mod 2) & k mod 2<2 by NAT_1:def 2;
for j st k=2*j or k=2*j -'1 holds
(k =2*j implies |[(f/.i)`1,(f/.(i+1))`2]|
=|[(f/.j)`1,(f/.(j+1))`2]|)
&(k =2*j-'1 implies |[(f/.i)`1,(f/.(i+1))`2]|=f/.j)
proof let j;assume A7:k=2*j or k=2*j -'1;
per cases by A7;
suppose k=2*j;
then i=2*j/2 by A5,A6,XCMPLX_1:90;
then A8: i=j by XCMPLX_1:90;
now assume
A9:k=2*j-'1; then k=2*j-1 by A4,JORDAN3:1;
then A10:k=2*j-2*1+2-1 by XCMPLX_1:27 .=2*(j-1)+(1+1)-1 by
XCMPLX_1:40
.=2*(j-1)+1+1-1 by XCMPLX_1:1
.=2*(j-1)+1 by XCMPLX_1:26;
now assume A11:j=0;
0-1<0; then 0-'1=0 by BINARITH:def 3;
hence contradiction by A3,A9,A11,FINSEQ_1:3;
end; then j>0 by NAT_1:19; then j>=0+1 by NAT_1:38;
then k= 2*(j-'1)+1 & 1<=2 by A10,SCMFSA_7:3;
hence contradiction by A5,NAT_1:def 2;
end;
hence thesis by A8;
suppose A12:
k=2*j-'1; then k=2*j-1 by A4,JORDAN3:1;
then A13:k=2*j-2*1+2-1 by XCMPLX_1:27 .=2*(j-1)+(1+1)-1 by XCMPLX_1:
40
.=2*(j-1)+1+1-1 by XCMPLX_1:1
.=2*(j-1)+1 by XCMPLX_1:26;
now assume A14:j=0;
0-1<0; then 0-'1=0 by BINARITH:def 3;
hence contradiction by A3,A12,A14,FINSEQ_1:3;
end; then j>0 by NAT_1:19; then j>=0+1 by NAT_1:38;
then j-'1=j-1 by SCMFSA_7:3;
hence thesis by A5,A13,NAT_1:def 2;
end;
hence thesis;
suppose A15:k mod 2=1;
consider i such that
A16: k=2*i+ (k mod 2) & k mod 2<2 by NAT_1:def 2;
for j st k=2*j or k=2*j -'1 holds
(k =2*j implies f/.(i+1)=|[(f/.j)`1,(f/.(j+1))`2]|)
&(k =2*j-'1 implies f/.(i+1)=f/.j)
proof let j;assume A17:k=2*j or k=2*j -'1;
per cases by A17;
suppose k=2*j-'1;
then A18:k=2*j-1 by A4,JORDAN3:1;
A19:now assume
k=2*j-'1;
then k=2*j-1 by A4,JORDAN3:1;
then k=2*j-2*1+2-1 by XCMPLX_1:27 .=2*(j-1)+(1+1)-1 by XCMPLX_1:40
.=2*(j-1)+1+1-1 by XCMPLX_1:1
.=2*(j-1)+1 by XCMPLX_1:26;
then 2*(j-1)=2*i+1-1 by A15,A16,XCMPLX_1:26;
then 2*(j-1)/2=2*i/2 by XCMPLX_1:26;
then (j-1)=2*i/2 by XCMPLX_1:90;
then (j-1)=i by XCMPLX_1:90;
hence f/.(i+1)=f/.j by XCMPLX_1:27;
end;
now assume k=2*j;
then k-k=1 by A18,XCMPLX_1:18;
hence contradiction by XCMPLX_1:14;
end;
hence thesis by A19;
suppose k=2*j;
then 2*j-2*i=1 by A15,A16,XCMPLX_1:26;
then A20:2*(j-i)=1 by XCMPLX_1:40;
then j-i>=0 by SQUARE_1:24;
then A21:j-i=j-'i by BINARITH:def 3;
j-i=0 or j-i>0 by A20,SQUARE_1:24;
then j-i>=0+1 by A20,A21,NAT_1:38;
then 2*(j-i)>=2*1 by AXIOMS:25;
hence thesis by A20;
end;
hence thesis;
end;
A22:for k being Nat,y1,y2 being set st k in Seg (2*(len f)-'1) &
P[k,y1] & P[k,y2] holds y1=y2
proof let k be Nat,y1,y2 be set;
assume A23: k in Seg (2*(len f)-'1) &
(for j st k=2*j or k=2*j -'1 holds
(k =2*j implies y1=|[(f/.j)`1,(f/.(j+1))`2]|)
&(k =2*j-'1 implies y1=f/.j))&
(for j st k=2*j or k=2*j -'1 holds
(k =2*j implies y2=|[(f/.j)`1,(f/.(j+1))`2]|)
&(k =2*j-'1 implies y2=f/.j));
per cases by GROUP_4:100;
suppose A24:k mod 2=0;
consider i such that
A25: k=2*i+ (k mod 2) & k mod 2<2 by NAT_1:def 2;
y1=|[(f/.i)`1,(f/.(i+1))`2]| by A23,A24,A25;
hence thesis by A23,A24,A25;
suppose A26:k mod 2=1;
consider i such that
A27: k=2*i+ (k mod 2) & k mod 2<2 by NAT_1:def 2;
A28: k=2*i+2*1-(1+1)+1 by A26,A27,XCMPLX_1:26
.=2*(i+1)-(1+1)+1 by XCMPLX_1:8
.=2*(i+1)+1-(1+1) by XCMPLX_1:29
.=2*(i+1)+1-1-1 by XCMPLX_1:36
.=2*(i+1)-1 by XCMPLX_1:26;
1<=1+i by NAT_1:37;
then 2*1<=2*(i+1) by AXIOMS:25;
then 1<=2*(i+1) by AXIOMS:22;
then A29:2*(i+1)-'1= 2*(i+1)-1 by SCMFSA_7:3;
then y1=f/.(i+1) by A23,A28;
hence thesis by A23,A28,A29;
end;
ex p being FinSequence st dom p = Seg (2*(len f)-'1)
& for k st k in Seg (2*(len f)-'1) holds P[k,p.k] from SeqEx(A22,A2);
then consider p being FinSequence such that
A30: dom p = Seg (2*(len f)-'1)
& for k st k in Seg (2*(len f)-'1) holds
(for j st k=2*j or k=2*j -'1 holds
(k =2*j implies p.k=|[(f/.j)`1,(f/.(j+1))`2]|)
&(k =2*j-'1 implies p.k=f/.j));
A31:len p=(2*(len f)-'1) by A30,FINSEQ_1:def 3;
rng p c= the carrier of TOP-REAL 2
proof let y;assume y in rng p;
then consider x such that
A32:x in dom p & y=p.x by FUNCT_1:def 5;
A33:x in Seg len p by A32,FINSEQ_1:def 3;
reconsider i=x as Nat by A32;
A34:1 <= i & i <= len p by A33,FINSEQ_1:3;
per cases by GROUP_4:100;
suppose A35:i mod 2=0;
consider j such that
A36: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
p.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A32,A35,A36;
hence thesis by A32;
suppose A37:i mod 2=1;
consider j such that
A38: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
A39: i=2*j+1+1-1 by A37,A38,XCMPLX_1:26
.=2*j+(1+1)-1 by XCMPLX_1:1
.=2*j+2*1-1
.=2*(j+1)-1 by XCMPLX_1:8;
then 2*(j+1)-1=2*(j+1)-'1 by A34,JORDAN3:1;
then p.i=f/.(j+1) by A30,A32,A39;
hence thesis by A32;
end;
then reconsider g1=p as FinSequence of TOP-REAL 2 by FINSEQ_1:def 4;
for i st 1 <= i & i+1 <= len g1 holds
(g1/.i)`1 = (g1/.(i+1))`1 or (g1/.i)`2 = (g1/.(i+1))`2
proof let i;assume A40:1 <= i & i+1 <= len g1;
then A41:i<len g1 by NAT_1:38;
A42:1<i+1 by A40,NAT_1:38;
then A43:i+1 in Seg len g1 by A40,FINSEQ_1:3;
A44: i in Seg (2*(len f)-'1) by A31,A40,A41,FINSEQ_1:3;
A45:g1.i=g1/.i by A40,A41,FINSEQ_4:24;
A46:g1/.(i+1)=g1.(i+1) by A40,A42,FINSEQ_4:24;
per cases by GROUP_4:100;
suppose A47:i mod 2=0;
consider j such that
A48: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
A49:g1/.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A44,A45,A47,A48;
A50: i+1=2*j+1+1-1 by A47,A48,XCMPLX_1:26
.=2*j+(1+1)-1 by XCMPLX_1:1
.=2*j+2*1-1
.=2*(j+1)-1 by XCMPLX_1:8;
1<=1+i by NAT_1:29;
then 2*(j+1)-'1 =2*(j+1)-1 by A50,JORDAN3:1;
then g1/.(i+1)=f/.(j+1) by A30,A31,A43,A46,A50;
hence thesis by A49,EUCLID:56;
suppose A51:i mod 2=1;
consider j such that
A52: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
i=2*j+1+1-1 by A51,A52,XCMPLX_1:26;
then i=2*j+(1+1)-1 by XCMPLX_1:1;
then i=2*j+2*1-1;
then A53:i=2*(j+1)-1 by XCMPLX_1:8;
then 2*(j+1)-'1 =2*(j+1)-1 by A40,JORDAN3:1;
then A54:g1/.i=f/.(j+1) by A30,A44,A45,A53;
i+1=2*j+(1+1) by A51,A52,XCMPLX_1:1
.=2*j+2*1
.=2*(j+1) by XCMPLX_1:8;
then g1/.(i+1)=|[(f/.(j+1))`1,(f/.(j+1+1))`2]| by A30,A31,A43,A46;
hence thesis by A54,EUCLID:56;
end;
then A55:g1 is special by TOPREAL1:def 7;
A56: 2*(len f)>=2*1 by A1,AXIOMS:25;
then 2*(len f)>=1 by AXIOMS:22;
then A57:2*(len f)-'1= 2*(len f)-1 by SCMFSA_7:3;
A58:2*(len f)-1>= 1+1-1 by A56,REAL_1:49;
then A59: 1 in Seg (2*(len f)-'1) by A57,FINSEQ_1:3;
2*1-'1=1+1-'1 .=1 by BINARITH:39;
then p.1=f/.1 by A30,A59;
then A60:g1.1=f.1 by A1,FINSEQ_4:24;
(2*(len f)-'1) in Seg (2*(len f)-'1) by A57,A58,FINSEQ_1:3;
then p.(2*(len f)-'1)=f/.len f by A30;
then A61:g1.len g1=f.len f by A1,A31,FINSEQ_4:24;
len f + len f>=len f+1 by A1,AXIOMS:24;
then 2*(len f)>=len f +1 by XCMPLX_1:11;
then 2*(len f)-1>=len f +1-1 by REAL_1:49;
then A62:len g1>=len f by A31,A57,XCMPLX_1:26;
for i st i in dom (Y_axis(g1)) holds (Y_axis(f)).1 <= (Y_axis(g1)).i
& (Y_axis(g1)).i <= (Y_axis(f)).(len f)
proof let i;assume
A63:i in dom (Y_axis(g1));
then A64: i in Seg len (Y_axis(g1)) by FINSEQ_1:def 3;
then i in Seg len g1 by GOBOARD1:def 4;
then A65: 1<=i & i<=len g1 by FINSEQ_1:3;
A66:i in Seg len g1 by A64,GOBOARD1:def 4;
A67:(Y_axis(g1)).i = (g1/.i)`2 by A63,GOBOARD1:def 4;
A68:len (Y_axis(f))=len f by GOBOARD1:def 4;
A69:g1/.i=(g1.i) by A65,FINSEQ_4:24;
per cases by GROUP_4:100;
suppose A70:i mod 2=0;
consider j such that
A71: i=2*j+ (i mod 2) & (i mod 2)<2 by NAT_1:def 2;
g1/.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A31,A66,A69,A70,A71;
then A72:(g1/.i)`2=(f/.(j+1))`2 by EUCLID:56;
A73:1<=j+1 by NAT_1:29;
2*j+1<=2*(len f)-1+1 by A31,A57,A65,A70,A71,AXIOMS:24;
then 2*j+1<=2*(len f) by XCMPLX_1:27;
then 2*j<2*(len f) by NAT_1:38;
then 2*j/2<2*(len f)/2 by REAL_1:73;
then j<2*(len f)/2 by XCMPLX_1:90;
then j<len f by XCMPLX_1:90;
then j+1<=len f by NAT_1:38;
then j+1 in Seg len f by A73,FINSEQ_1:3;
then A74:j+1 in dom (Y_axis(f)) by A68,FINSEQ_1:def 3;
then (Y_axis(f)).(j+1) = (f/.(j+1))`2 by GOBOARD1:def 4;
hence thesis by A1,A67,A72,A74,GOBOARD4:def 1;
suppose A75:i mod 2=1;
consider j such that
A76: i=2*j+ (i mod 2) & (i mod 2)<2 by NAT_1:def 2;
i=2*j+1+1-1 by A75,A76,XCMPLX_1:26
.=2*j+(1+1)-1 by XCMPLX_1:1
.=2*j+2*1-1;
then A77:i=2*(j+1)-1 by XCMPLX_1:8;
then 2*(j+1)-'1 =2*(j+1)-1 by A65,JORDAN3:1;
then A78:(g1/.i)`2=(f/.(j+1))`2 by A30,A31,A66,A69,A77;
A79:1<=j+1 by NAT_1:29;
2*j+1<=2*(len f)-1+1 by A31,A57,A65,A75,A76,NAT_1:38;
then 2*j+1<=2*(len f) by XCMPLX_1:27;
then 2*j<2*(len f) by NAT_1:38;
then 2*j/2<2*(len f)/2 by REAL_1:73;
then j<2*(len f)/2 by XCMPLX_1:90;
then j<len f by XCMPLX_1:90;
then j+1<=len f by NAT_1:38;
then j+1 in Seg len f by A79,FINSEQ_1:3;
then A80:j+1 in dom (Y_axis(f)) by A68,FINSEQ_1:def 3;
then (Y_axis(f)).(j+1) = (f/.(j+1))`2 by GOBOARD1:def 4;
hence thesis by A1,A67,A78,A80,GOBOARD4:def 1;
end;
then A81:Y_axis(g1) lies_between (Y_axis(f)).1, (Y_axis(f)).(len f)
by GOBOARD4:def 1;
for i st i in dom (X_axis(g1)) holds
c <= (X_axis(g1)).i & (X_axis(g1)).i <= d
proof let i;assume
A82:i in dom (X_axis(g1));
then A83: i in Seg len (X_axis(g1)) by FINSEQ_1:def 3;
then A84:i in Seg len g1 by GOBOARD1:def 3;
then A85: 1<=i & i<=len g1 by FINSEQ_1:3;
A86:(X_axis(g1)).i = (g1/.i)`1 by A82,GOBOARD1:def 3;
A87:len (X_axis(f))=len f by GOBOARD1:def 3;
A88:g1/.i=(g1.i) by A85,FINSEQ_4:24;
per cases by GROUP_4:100;
suppose A89:i mod 2=0;
consider j such that
A90: i=2*j+ (i mod 2) & (i mod 2)<2 by NAT_1:def 2;
g1/.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A31,A84,A88,A89,A90;
then A91:(g1/.i)`1=(f/.j)`1 by EUCLID:56;
j<>0 by A83,A89,A90,FINSEQ_1:3;
then j>0 by NAT_1:19;
then A92: j>=0+1 by NAT_1:38;
2*j+1<=2*(len f)-1+1 by A31,A57,A85,A89,A90,AXIOMS:24;
then 2*j+1<=2*(len f) by XCMPLX_1:27;
then 2*j<2*(len f) by NAT_1:38;
then 2*j/2<2*(len f)/2 by REAL_1:73;
then j<2*(len f)/2 by XCMPLX_1:90;
then j<len f by XCMPLX_1:90;
then j in Seg len f by A92,FINSEQ_1:3;
then A93:j in dom (X_axis(f)) by A87,FINSEQ_1:def 3;
then (X_axis(f)).j = (f/.j)`1 by GOBOARD1:def 3;
hence thesis by A1,A86,A91,A93,GOBOARD4:def 1;
suppose A94:i mod 2=1;
consider j such that
A95: i=2*j+ (i mod 2) & (i mod 2)<2 by NAT_1:def 2;
i=2*j+1+1-1 by A94,A95,XCMPLX_1:26;
then i=2*j+(1+1)-1 by XCMPLX_1:1;
then i=2*j+2*1-1;
then A96:i=2*(j+1)-1 by XCMPLX_1:8;
then 2*(j+1)-'1 =2*(j+1)-1 by A85,JORDAN3:1;
then A97:(g1/.i)`1=(f/.(j+1))`1 by A30,A31,A84,A88,A96;
A98:1<=j+1 by NAT_1:29;
2*j+1<=2*(len f)-1+1 by A31,A57,A85,A94,A95,NAT_1:38;
then 2*j+1<=2*(len f) by XCMPLX_1:27;
then 2*j<2*(len f) by NAT_1:38;
then 2*j/2<2*(len f)/2 by REAL_1:73;
then j<2*(len f)/2 by XCMPLX_1:90;
then j<len f by XCMPLX_1:90;
then j+1<=len f by NAT_1:38;
then j+1 in Seg len f by A98,FINSEQ_1:3;
then A99:j+1 in dom (X_axis(f)) by A87,FINSEQ_1:def 3;
then (X_axis(f)).(j+1) = (f/.(j+1))`1 by GOBOARD1:def 3;
hence thesis by A1,A86,A97,A99,GOBOARD4:def 1;
end;
then A100:X_axis(g1) lies_between c, d by GOBOARD4:def 1;
A101:for i st i in dom g1 holds
ex k st k in dom f & |. g1/.i - f/.k .| < a
proof let i;assume
A102: i in dom g1;
then A103:1<=i & i<=len g1 by FINSEQ_3:27;
then A104:g1.i=g1/.i by FINSEQ_4:24;
per cases by GROUP_4:100;
suppose A105:i mod 2=0;
consider j such that
A106: i=2*j+ (i mod 2) & (i mod 2)<2 by NAT_1:def 2;
A107:g1/.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A102,A104,A105,A106;
then A108:(g1/.i)`1=(f/.j)`1 by EUCLID:56;
A109:g1/.i-f/.j
=|[(g1/.i)`1-(f/.j)`1,(g1/.i)`2-(f/.j)`2]| by EUCLID:65
.=|[0,(g1/.i)`2-(f/.j)`2]| by A108,XCMPLX_1:14;
then A110:(g1/.i-f/.j)`1=0 by EUCLID:56;
(g1/.i-f/.j)`2=(g1/.i)`2-(f/.j)`2 by A109,EUCLID:56;
then |.g1/.i-f/.j.|=
sqrt((((g1/.i-f/.j)`1))^2+(((g1/.i)`2-(f/.j)`2))^2)
by Th47
.= sqrt((((f/.(j+1))`2-(f/.j)`2))^2) by A107,A110,EUCLID:56,SQUARE_1:
60;
then |.g1/.i-f/.j.|=abs((f/.(j+1))`2-(f/.j)`2) by SQUARE_1:91
.=abs((f/.j)`2 -(f/.(j+1))`2) by UNIFORM1:13;
then A111:|.g1/.i-f/.j.|
<=|.f/.j-f/.(j+1).| by Th51;
j<>0 by A102,A105,A106,FINSEQ_3:27;
then j>0 by NAT_1:19;
then A112: j>=0+1 by NAT_1:38;
2*j+1<=2*(len f)-1+1 by A31,A57,A103,A105,A106,AXIOMS:24;
then 2*j+1<=2*(len f) by XCMPLX_1:27;
then 2*j<2*(len f) by NAT_1:38;
then 2*j/2<2*(len f)/2 by REAL_1:73;
then j<2*(len f)/2 by XCMPLX_1:90;
then A113: j<len f by XCMPLX_1:90;
then j+1<=len f by NAT_1:38;
then |. f/.j-f/.(j+1) .|<a by A1,A112;
then A114: |. g1/.i - f/.j .|<a by A111,AXIOMS:22;
j in dom f by A112,A113,FINSEQ_3:27;
hence thesis by A114;
suppose A115:i mod 2=1;
consider j such that
A116: i=2*j+ (i mod 2) & (i mod 2)<2 by NAT_1:def 2;
i=2*j+1+1-1 by A115,A116,XCMPLX_1:26;
then i=2*j+(1+1)-1 by XCMPLX_1:1;
then i=2*j+2*1-1;
then A117:i=2*(j+1)-1 by XCMPLX_1:8;
then 2*(j+1)-'1 =2*(j+1)-1 by A103,JORDAN3:1;
then g1/.i=f/.(j+1) by A30,A102,A104,A117;
then A118:|.g1/.i-f/.(j+1).|=|.0.REAL 2.| by EUCLID:46 .=0 by TOPRNS_1:
24;
2*j+1+1<=2*(len f)-1+1 by A31,A57,A103,A115,A116,AXIOMS:24;
then 2*j+1+1<=2*(len f) by XCMPLX_1:27;
then 2*j+1<2*(len f) by NAT_1:38;
then 2*j<2*(len f) by NAT_1:38;
then 2*j/2<2*(len f)/2 by REAL_1:73;
then j<2*(len f)/2 by XCMPLX_1:90;
then j<len f by XCMPLX_1:90;
then A119: j+1<=len f by NAT_1:38;
1<=j+1 by NAT_1:29;
then j+1 in dom f by A119,FINSEQ_3:27;
hence thesis by A1,A118;
end;
for i st 1<=i & i+1<=len g1 holds |. g1/.i - g1/.(i+1) .|<a
proof let i;assume A120:1<=i & i+1<=len g1;
then i<=len g1 by NAT_1:38;
then A121:i in Seg len g1 by A120,FINSEQ_1:3;
A122:1<=i & i<=len g1 by A120,NAT_1:38;
A123:1<=i+1 by NAT_1:29;
then A124: i+1 in Seg (2*(len f)-'1) by A31,A120,FINSEQ_1:3;
A125:g1.(i+1)=g1/.(i+1) by A120,A123,FINSEQ_4:24;
A126:g1.i=g1/.i by A122,FINSEQ_4:24;
per cases by GROUP_4:100;
suppose A127:i mod 2=0;
consider j such that
A128: i=2*j+ (i mod 2) & (i mod 2)<2 by NAT_1:def 2;
A129:g1/.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A31,A121,A126,A127,A128;
i+1=2*j+1+1-1 by A127,A128,XCMPLX_1:26
.=2*j+(1+1)-1 by XCMPLX_1:1
.=2*j+2*1-1;
then A130:i+1=2*(j+1)-1 by XCMPLX_1:8;
1<=1+i by NAT_1:29;
then 2*(j+1)-'1 =2*(j+1)-1 by A130,JORDAN3:1;
then A131:g1/.(i+1)=f/.(j+1) by A30,A124,A125,A130;
A132:(g1/.i)`1=(f/.j)`1 by A129,EUCLID:56;
A133:(g1/.i)`2=(f/.(j+1))`2 by A129,EUCLID:56;
A134:g1/.i-g1/.(i+1)
=|[(g1/.i)`1-(g1/.(i+1))`1,(g1/.i)`2-(g1/.(i+1))`2]|
by EUCLID:65
.=|[(f/.j)`1-(f/.(j+1))`1,0]|
by A131,A132,A133,XCMPLX_1:14;
then A135:(g1/.i-g1/.(i+1))`1=(f/.j)`1-(f/.(j+1))`1 by EUCLID:56;
(g1/.i-g1/.(i+1))`2=0 by A134,EUCLID:56;
then |.g1/.i-g1/.(i+1).|= sqrt((((f/.j)`1-(f/.(j+1))`1))^2+0) by A135,
Th47,SQUARE_1:60
.= sqrt((((f/.j)`1-(f/.(j+1))`1))^2);
then |.g1/.i-g1/.(i+1).|=abs((f/.j)`1-(f/.(j+1))`1)
by SQUARE_1:91;
then A136:|.g1/.i-g1/.(i+1).|<=|.f/.j-f/.(j+1).| by Th51;
j<>0 by A120,A127,A128;
then j>0 by NAT_1:19;
then A137: j>=0+1 by NAT_1:38;
2*j+1<=2*(len f)-1+1 by A31,A57,A120,A127,A128,NAT_1:38;
then 2*j+1<=2*(len f) by XCMPLX_1:27;
then 2*j<2*(len f) by NAT_1:38;
then 2*j/2<2*(len f)/2 by REAL_1:73;
then j<2*(len f)/2 by XCMPLX_1:90;
then j<len f by XCMPLX_1:90;
then j+1<=len f by NAT_1:38;
then |. f/.j-f/.(j+1) .|<a by A1,A137;
hence thesis by A136,AXIOMS:22;
suppose A138:i mod 2=1;
consider j such that
A139: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
i=2*j+1+1-1 by A138,A139,XCMPLX_1:26
.=2*j+(1+1)-1 by XCMPLX_1:1
.=2*j+2*1-1;
then A140:i=2*(j+1)-1 by XCMPLX_1:8;
then 2*(j+1)-'1 =2*(j+1)-1 by A120,JORDAN3:1;
then A141:g1/.i=f/.(j+1) by A30,A31,A121,A126,A140;
i+1=2*j+(1+1) by A138,A139,XCMPLX_1:1
.=2*j+2*1;
then A142:i+1=2*(j+1) by XCMPLX_1:8;
then A143:g1/.(i+1)=|[(f/.(j+1))`1,(f/.(j+1+1))`2]| by A30,A124,A125;
then A144:(g1/.(i+1))`1=(f/.(j+1))`1 by EUCLID:56;
A145:(g1/.(i+1))`2=(f/.(j+1+1))`2 by A143,EUCLID:56;
A146:g1/.i-g1/.(i+1)
=|[(g1/.i)`1-(g1/.(i+1))`1,(g1/.i)`2-(g1/.(i+1))`2]|
by EUCLID:65
.=|[0,(f/.(j+1))`2-(f/.(j+1+1))`2]|
by A141,A144,A145,XCMPLX_1:14;
then A147:(g1/.i-g1/.(i+1))`1=0 by EUCLID:56;
(g1/.i-g1/.(i+1))`2=(f/.(j+1))`2-(f/.(j+1+1))`2
by A146,EUCLID:56;
then |.g1/.i-g1/.(i+1).|= sqrt(0+(((f/.(j+1))`2-(f/.(j+1+1))`2))^2)
by A147,Th47,SQUARE_1:60
.= sqrt((((f/.(j+1))`2-(f/.(j+1+1))`2))^2);
then |.g1/.i-g1/.(i+1).|=abs((f/.(j+1))`2-(f/.(j+1+1))`2)
by SQUARE_1:91;
then A148:|.g1/.i-g1/.(i+1).|
<=|.f/.(j+1)-f/.(j+1+1).| by Th51;
A149: j+1>=1 by NAT_1:29;
2*(j+1)+1<=2*(len f)-1+1 by A31,A57,A120,A142,AXIOMS:24;
then 2*(j+1)+1<=2*(len f) by XCMPLX_1:27;
then 2*(j+1)<2*(len f) by NAT_1:38;
then 2*(j+1)/2<2*(len f)/2 by REAL_1:73;
then (j+1)<2*(len f)/2 by XCMPLX_1:90;
then (j+1)<len f by XCMPLX_1:90;
then (j+1)+1<=len f by NAT_1:38;
then |. f/.(j+1)-f/.(j+1+1) .|<a by A1,A149;
hence thesis by A148,AXIOMS:22;
end;
hence thesis by A55,A60,A61,A62,A81,A100,A101;
end;
canceled;
theorem Th59:
for f being FinSequence of TOP-REAL 2 st 1 <=len f
holds len X_axis(f)=len f &
X_axis(f).1=(f/.1)`1 & X_axis(f).len f=(f/.len f)`1
proof let f be FinSequence of TOP-REAL 2;
assume A1:1 <=len f;
then A2: 1 in Seg len f by FINSEQ_1:3;
A3: len (X_axis(f)) = len f &
for k st k in dom (X_axis(f)) holds (X_axis(f)).k = (f/.k)`1
by GOBOARD1:def 3;
then A4: 1 in dom (X_axis(f)) by A2,FINSEQ_1:def 3;
len f in Seg len f by A1,FINSEQ_1:3;
then len f in dom (X_axis(f)) by A3,FINSEQ_1:def 3;
hence thesis by A4,GOBOARD1:def 3;
end;
theorem Th60:
for f being FinSequence of TOP-REAL 2 st 1 <=len f
holds len Y_axis(f)=len f &
Y_axis(f).1=(f/.1)`2 & Y_axis(f).len f=(f/.len f)`2
proof let f be FinSequence of TOP-REAL 2;
assume A1:1 <=len f;
then A2: 1 in Seg len f by FINSEQ_1:3;
A3: len (Y_axis(f)) = len f &
for k st k in dom (Y_axis(f)) holds (Y_axis(f)).k = (f/.k)`2
by GOBOARD1:def 4;
then A4: 1 in dom (Y_axis(f)) by A2,FINSEQ_1:def 3;
len f in Seg len f by A1,FINSEQ_1:3;
then len f in dom (Y_axis(f)) by A3,FINSEQ_1:def 3;
hence thesis by A4,GOBOARD1:def 4;
end;
theorem Th61:
for f being FinSequence of TOP-REAL 2 st i in dom f
holds X_axis(f).i=(f/.i)`1 & Y_axis(f).i=(f/.i)`2
proof let f be FinSequence of TOP-REAL 2;
assume
A1: i in dom f;
len (X_axis(f)) = len f by GOBOARD1:def 3;
then i in dom (X_axis(f)) by A1,FINSEQ_3:31;
hence (X_axis(f)).i = (f/.i)`1 by GOBOARD1:def 3;
len (Y_axis(f)) = len f by GOBOARD1:def 4;
then i in dom Y_axis f by A1,FINSEQ_3:31;
hence thesis by GOBOARD1:def 4;
end;
:: Goboard Theorem in continuous case
theorem Th62:for P,Q being non empty Subset of TOP-REAL 2,
p1,p2,q1,q2 being Point of TOP-REAL 2 st
P is_an_arc_of p1,p2 & Q is_an_arc_of q1,q2 &
(for p being Point of TOP-REAL 2 st p in P holds p1`1<=p`1 & p`1<= p2`1) &
(for p being Point of TOP-REAL 2 st p in Q holds p1`1<=p`1 & p`1<= p2`1) &
(for p being Point of TOP-REAL 2 st p in P holds q1`2<=p`2 & p`2<= q2`2) &
(for p being Point of TOP-REAL 2 st p in Q holds q1`2<=p`2 & p`2<= q2`2)
holds P meets Q
proof let P,Q be non empty Subset of TOP-REAL 2,
p1,p2,q1,q2 be Point of TOP-REAL 2;
assume that A1:P is_an_arc_of p1,p2 & Q is_an_arc_of q1,q2 and
A2:(for p being Point of TOP-REAL 2 st p in P holds p1`1<=p`1 & p`1<= p2`1)
and
A3:(for p being Point of TOP-REAL 2 st p in Q holds p1`1<=p`1 & p`1<= p2`1)
and
A4:(for p being Point of TOP-REAL 2 st p in P holds q1`2<=p`2 & p`2<= q2`2)
and
A5:(for p being Point of TOP-REAL 2 st p in Q holds q1`2<=p`2 & p`2<= q2`2);
A6:p1<>p2 by A1,JORDAN6:49;
A7:q1<>q2 by A1,JORDAN6:49;
consider f being map of I[01], (TOP-REAL 2)|P such that
A8:f is_homeomorphism & f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 2;
consider g being map of I[01], (TOP-REAL 2)|Q such that
A9:g is_homeomorphism & g.0 = q1 & g.1 = q2 by A1,TOPREAL1:def 2;
consider f1 being map of I[01],TOP-REAL 2 such that
A10: f=f1 & f1 is continuous & f1 is one-to-one by A8,JORDAN7:15;
consider g1 being map of I[01],TOP-REAL 2 such that
A11: g=g1 & g1 is continuous & g1 is one-to-one by A9,JORDAN7:15;
A12:TOP-REAL 2=TopSpaceMetr(Euclid 2) by EUCLID:def 8;
A13: Euclid 2= MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
reconsider P'=P,Q'=Q as Subset of TopSpaceMetr(Euclid 2)
by A12;
A14:P' <> {} & P' is compact & Q' <> {}
& Q' is compact by A1,A12,JORDAN5A:1;
assume P /\ Q= {};
then P misses Q by XBOOLE_0:def 7;
then A15:min_dist_min(P',Q')>0 by A14,Th55;
set e=min_dist_min(P',Q')/5;
A16:e*5=min_dist_min(P',Q') by XCMPLX_1:88;
A17: e>0/5 by A15,REAL_1:73;
then consider h being FinSequence of REAL such that
A18: h.1=0 & h.len h=1 & 5<=len h & rng h c= the carrier of I[01]
& h is increasing
&(for i being Nat,R being Subset of I[01],
W being Subset of Euclid 2
st 1<=i & i<len h & R=[.h/.i,h/.(i+1).] & W=f1.:(R) holds
diameter(W)<e) by A8,A10,UNIFORM1:15;
deffunc F(Nat)=f1.(h.$1);
ex h1' being FinSequence st len h1'=len h &
for i st i in Seg len h holds h1'.i=F(i) from SeqLambda;
then consider h1' being FinSequence such that
A19:len h1'=len h &
for i st i in Seg len h holds h1'.i=f1.(h.i);
rng h1' c= the carrier of TOP-REAL 2
proof let y;assume y in rng h1';
then consider x such that
A20:x in dom h1' & y=h1'.x by FUNCT_1:def 5;
A21:dom h1'=Seg len h1' by FINSEQ_1:def 3;
reconsider i=x as Nat by A20;
A22: h1'.i=f1.(h.i) by A19,A20,A21;
i in dom h by A19,A20,A21,FINSEQ_1:def 3;
then A23:h.i in rng h by FUNCT_1:def 5;
dom f1= [#](I[01]) by A8,A10,TOPS_2:def 5
.=the carrier of I[01] by PRE_TOPC:12;
then A24:h1'.i in rng f by A10,A18,A22,A23,FUNCT_1:def 5;
rng f=[#]((TOP-REAL 2)|P) by A8,TOPS_2:def 5
.=P by PRE_TOPC:def 10;
hence thesis by A20,A24;
end;
then reconsider h1=h1' as FinSequence of TOP-REAL 2 by FINSEQ_1:def 4;
A25: dom h=Seg len h by FINSEQ_1:def 3;
A26:the carrier of TOP-REAL 2=the carrier of Euclid 2 by TOPREAL3:13;
A27:for i st 1<=i & i+1<=len h1 holds |.h1/.i-h1/.(i+1).|<e
proof let i;assume A28:1<=i & i+1<=len h1;
then A29:i<len h1 by NAT_1:38;
A30:1<i+1 by A28,NAT_1:38;
then A31:i+1 in Seg len h by A19,A28,FINSEQ_1:3;
A32: i in Seg len h by A19,A28,A29,FINSEQ_1:3;
then A33:h1'.i=f1.(h.i) by A19;
then A34:h1/.i=f1.(h.i) by A28,A29,FINSEQ_4:24;
A35:h1'.(i+1)=f1.(h.(i+1)) by A19,A31;
then A36:h1/.(i+1)=f1.(h.(i+1)) by A28,A30,FINSEQ_4:24;
A37:i in dom h by A19,A28,A29,FINSEQ_3:27;
then A38:h.i in rng h by FUNCT_1:def 5;
A39: dom f1= [#](I[01]) by A8,A10,TOPS_2:def 5
.=the carrier of I[01] by PRE_TOPC:12;
then A40:h1'.i in rng f by A10,A18,A33,A38,FUNCT_1:def 5;
A41:rng f=[#]((TOP-REAL 2)|P) by A8,TOPS_2:def 5
.=P by PRE_TOPC:def 10;
then A42:f1.(h.i) is Element of TOP-REAL 2 by A19,A32,
A40;
i+1 in dom h by A19,A28,A30,FINSEQ_3:27;
then h.(i+1) in rng h by FUNCT_1:def 5;
then h1'.(i+1) in rng f by A10,A18,A35,A39,FUNCT_1:def 5;
then A43:f1.(h.(i+1)) is Element of TOP-REAL 2 by A19,
A31,A41;
A44:h.i=h/.i by A19,A28,A29,FINSEQ_4:24;
A45:i+1 in dom h by A19,A28,A30,FINSEQ_3:27;
then A46:h.(i+1) in rng h by FUNCT_1:def 5;
A47:h.(i+1)=h/.(i+1) by A19,A28,A30,FINSEQ_4:24;
i<i+1 by NAT_1:38;
then A48:0<=h/.i & h/.i <= h/.(i+1) & h/.(i+1)<=1
by A18,A37,A38,A44,A45,A46,A47,BORSUK_1:83,GOBOARD1:def 1,TOPREAL5
:1;
reconsider W1=P as Subset of Euclid 2 by A26;
reconsider Pa=P as Subset of TOP-REAL 2;
A49:Pa is compact by A1,JORDAN5A:1;
reconsider Pa as non empty Subset of TOP-REAL 2;
reconsider R=[.h/.i,h/.(i+1).] as Subset of I[01]
by A18,A38,A44,A46,A47,BORSUK_1:83,RCOMP_1:16;
reconsider w1=f1.(h.i),w2=f1.(h.(i+1)) as Point of Euclid 2
by A42,A43,TOPREAL3:13;
A50: h.i in R by A44,A48,TOPREAL5:1;
h.(i+1) in R by A47,A48,TOPREAL5:1;
then A51:w1 in f1.:R & w2 in f1.:R by A39,A50,FUNCT_1:def 12;
reconsider W=f1.:R as Subset of Euclid 2 by A26;
A52:dom f1=[#](I[01]) & rng f1=P
by A8,A10,A41,TOPS_2:def 5;
[#](I[01])=[.0,1.] by BORSUK_1:83,PRE_TOPC:12;
then P=f1.:([.0,1.]) by A52,RELAT_1:146;
then A53:W c= W1 by BORSUK_1:83,RELAT_1:156;
p1 in Pa by A1,TOPREAL1:4;
then A54: W-bound Pa <= p1`1 & p1`1 <= E-bound Pa &
S-bound Pa <= p1`2 & p1`2 <= N-bound Pa by A49,PSCOMP_1:71;
set r1=((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa))+1;
(W-bound Pa)<=(E-bound Pa) by A54,AXIOMS:22;
then A55:0<=((E-bound Pa) - (W-bound Pa)) by SQUARE_1:12;
(S-bound Pa)<=(N-bound Pa) by A54,AXIOMS:22;
then 0<=((N-bound Pa) - (S-bound Pa)) by SQUARE_1:12;
then A56:((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa))
>=0+0 by A55,REAL_1:55;
A57: r1> ((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa))
by REAL_1:69;
for x,y being Point of Euclid 2
st x in W1 & y in W1 holds dist(x,y)<=r1
proof let x,y be Point of Euclid 2;
assume A58: x in W1 & y in W1;
then reconsider pw1=x,pw2=y as Point of TOP-REAL 2;
A59:dist(x,y)=|.pw1-pw2.| by Th45;
A60:|.pw1-pw2.|<=abs(pw1`1-pw2`1)+abs(pw1`2-pw2`2) by Th49;
A61:W-bound Pa <= pw1`1 & pw1`1 <= E-bound Pa &
S-bound Pa <= pw1`2 & pw1`2 <= N-bound Pa
by A49,A58,PSCOMP_1:71;
A62:W-bound Pa <= pw2`1 & pw2`1 <= E-bound Pa &
S-bound Pa <= pw2`2 & pw2`2 <= N-bound Pa
by A49,A58,PSCOMP_1:71;
then A63:abs(pw1`1-pw2`1)<=(E-bound Pa) - (W-bound Pa) by A61,Th31;
abs(pw1`2-pw2`2)<=(N-bound Pa) - (S-bound Pa) by A61,A62,Th31;
then A64:abs(pw1`1-pw2`1)+abs(pw1`2-pw2`2)
<=((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa))
by A63,REAL_1:55;
((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa))
<= ((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa))
+1 by REAL_1:69;
then abs(pw1`1-pw2`1)+abs(pw1`2-pw2`2)<=r1 by A64,AXIOMS:22;
hence thesis by A59,A60,AXIOMS:22;
end;
then W1 is bounded by A56,A57,TBSP_1:def 9;
then A65:W is bounded by A53,TBSP_1:21;
A66: diameter(W)<e by A18,A19,A28,A29;
dist(w1,w2)<=diameter(W) by A51,A65,TBSP_1:def 10;
then dist(w1,w2)<e by A66,AXIOMS:22;
hence thesis by A34,A36,Th45;
end;
A67:len h1>=1 by A18,A19,AXIOMS:22;
consider hb being FinSequence of REAL
such that
A68: hb.1=0 & hb.len hb=1 & 5<=len hb & rng hb c= the carrier of I[01]
& hb is increasing
&(for i being Nat,R being Subset of I[01],
W being Subset of Euclid 2
st 1<=i & i<len hb & R=[.hb/.i,hb/.(i+1).] & W=g1.:(R) holds
diameter(W)<e) by A9,A11,A17,UNIFORM1:15;
A69: 1<=len hb by A68,AXIOMS:22;
then A70:1 in dom hb by FINSEQ_3:27;
A71:len hb in dom hb by A69,FINSEQ_3:27;
deffunc F(Nat)=g1.(hb.$1);
ex h2' being FinSequence st len h2'=len hb &
for i st i in Seg len hb holds h2'.i=F(i) from SeqLambda;
then consider h2' being FinSequence such that
A72:len h2'=len hb &
for i st i in Seg len hb holds h2'.i=g1.(hb.i);
rng h2' c= the carrier of TOP-REAL 2
proof let y;assume y in rng h2';
then consider x such that
A73:x in dom h2' & y=h2'.x by FUNCT_1:def 5;
A74:dom h2'=Seg len h2' by FINSEQ_1:def 3;
reconsider i=x as Nat by A73;
A75: h2'.i=g1.(hb.i) by A72,A73,A74;
i in dom hb by A72,A73,A74,FINSEQ_1:def 3;
then A76:hb.i in rng hb by FUNCT_1:def 5;
dom g1= [#](I[01]) by A9,A11,TOPS_2:def 5
.=the carrier of I[01] by PRE_TOPC:12;
then A77:h2'.i in rng g by A11,A68,A75,A76,FUNCT_1:def 5;
rng g=[#]((TOP-REAL 2)|Q) by A9,TOPS_2:def 5
.=Q by PRE_TOPC:def 10;
hence thesis by A73,A77;
end;
then reconsider h2=h2' as FinSequence of TOP-REAL 2 by FINSEQ_1:def 4;
A78:dom hb=Seg len hb by FINSEQ_1:def 3;
A79: for i st i in dom hb holds h2/.i=g1.(hb.i)
proof let i;assume
A80: i in dom hb;
then A81:h2.i=g1.(hb.i) by A72,A78;
1<=i & i<=len hb by A78,A80,FINSEQ_1:3;
hence thesis by A72,A81,FINSEQ_4:24;
end;
A82:len h2>=1 by A68,A72,AXIOMS:22;
A83:for i st i in dom h1 holds
(h1/.1)`1<=(h1/.i)`1 & (h1/.i)`1<=(h1/.len h1)`1
proof let i;assume A84:i in dom h1;
then A85: i in Seg len h by A19,FINSEQ_1:def 3;
then A86:i in dom h by FINSEQ_1:def 3;
h1.i=f1.(h.i) by A19,A85;
then A87:h1/.i=f1.(h.i) by A84,FINSEQ_4:def 4;
1 in dom h by A19,A67,FINSEQ_3:27;
then h1.1=f1.(h.1) by A19,A25;
then A88:h1/.1=f1.(h.1) by A67,FINSEQ_4:24;
len h in dom h by A19,A67,FINSEQ_3:27;
then h1.len h1=f1.(h.len h) by A19,A25;
then A89:h1/.len h1=f1.(h.len h) by A67,FINSEQ_4:24;
A90:h.i in rng h by A86,FUNCT_1:def 5;
dom f1= [#](I[01]) by A8,A10,TOPS_2:def 5
.=the carrier of I[01] by PRE_TOPC:12;
then A91:h1/.i in rng f by A10,A18,A87,A90,FUNCT_1:def 5;
rng f=[#]((TOP-REAL 2)|P) by A8,TOPS_2:def 5
.=P by PRE_TOPC:def 10;
hence thesis by A2,A8,A10,A18,A88,A89,A91;
end;
A92: for i st i in dom (X_axis(h1)) holds
(X_axis(h1)).1<=(X_axis(h1)).i & (X_axis(h1)).i<=(X_axis(h1)).(len h1)
proof let i;assume i in dom (X_axis(h1));
then i in Seg len (X_axis(h1)) by FINSEQ_1:def 3;
then i in Seg len h1 by A67,Th59;
then A93:i in dom h1 by FINSEQ_1:def 3;
then A94:(X_axis(h1)).i = (h1/.i)`1 by Th61;
A95:(X_axis(h1)).1=(h1/.1)`1 by A67,Th59;
(X_axis(h1)).len h1=(h1/.len h1)`1 by A67,Th59;
hence thesis by A83,A93,A94,A95;
end;
A96:for i st i in dom h1 holds
q1`2<=(h1/.i)`2 & (h1/.i)`2<=q2`2
proof let i;assume A97:i in dom h1;
then A98: i in Seg len h1 by FINSEQ_1:def 3;
then A99:i in dom h by A19,FINSEQ_1:def 3;
h1.i=f1.(h.i) by A19,A98;
then A100:h1/.i=f1.(h.i) by A97,FINSEQ_4:def 4;
A101:h.i in rng h by A99,FUNCT_1:def 5;
dom f1= [#](I[01]) by A8,A10,TOPS_2:def 5
.=the carrier of I[01] by PRE_TOPC:12;
then A102:h1/.i in rng f by A10,A18,A100,A101,FUNCT_1:def 5;
rng f=[#]((TOP-REAL 2)|P) by A8,TOPS_2:def 5
.=P by PRE_TOPC:def 10;
hence thesis by A4,A102;
end;
for i st i in dom (Y_axis(h1)) holds
q1`2<=(Y_axis(h1)).i & (Y_axis(h1)).i<=q2`2
proof let i;assume i in dom (Y_axis(h1));
then i in Seg len (Y_axis(h1)) by FINSEQ_1:def 3;
then i in Seg len h1 by A67,Th60;
then A103:i in dom h1 by FINSEQ_1:def 3;
then (Y_axis(h1)).i = (h1/.i)`2 by Th61;
hence thesis by A96,A103;
end;
then A104:X_axis(h1) lies_between (X_axis(h1)).1, (X_axis(h1)).(len h1) &
Y_axis(h1) lies_between q1`2,q2`2 by A92,GOBOARD4:def 1;
A105:for i st i in dom h2 holds
(h2/.1)`2<=(h2/.i)`2 & (h2/.i)`2<=(h2/.len h2)`2
proof let i;assume i in dom h2;
then i in Seg len h2 by FINSEQ_1:def 3;
then A106:i in dom hb by A72,FINSEQ_1:def 3;
then A107:h2/.i=g1.(hb.i) by A79;
1 in Seg len hb by A72,A82,FINSEQ_1:3;
then 1 in dom hb by FINSEQ_1:def 3;
then A108:h2/.1=g1.(hb.1) by A79;
len hb in Seg len hb by A72,A82,FINSEQ_1:3;
then len hb in dom hb by FINSEQ_1:def 3;
then A109:h2/.len h2=g1.(hb.len hb) by A72,A79;
A110:hb.i in rng hb by A106,FUNCT_1:def 5;
dom g1= [#](I[01]) by A9,A11,TOPS_2:def 5
.=the carrier of I[01] by PRE_TOPC:12;
then A111:h2/.i in rng g by A11,A68,A107,A110,FUNCT_1:def 5;
rng g=[#]((TOP-REAL 2)|Q) by A9,TOPS_2:def 5
.=Q by PRE_TOPC:def 10;
hence thesis by A5,A9,A11,A68,A108,A109,A111;
end;
A112: for i st i in dom (Y_axis(h2)) holds
(Y_axis(h2)).1<=(Y_axis(h2)).i & (Y_axis(h2)).i <=(Y_axis(h2)).(len h2)
proof let i;assume i in dom (Y_axis(h2));
then i in Seg len (Y_axis(h2)) by FINSEQ_1:def 3;
then i in Seg len h2 by A82,Th60;
then A113:i in dom h2 by FINSEQ_1:def 3;
then A114:(Y_axis(h2)).i = (h2/.i)`2 by Th61;
A115:(Y_axis(h2)).1=(h2/.1)`2 by A82,Th60;
(Y_axis(h2)).len h2=(h2/.len h2)`2 by A82,Th60;
hence thesis by A105,A113,A114,A115;
end;
A116:for i st i in dom h2 holds
p1`1<=(h2/.i)`1 & (h2/.i)`1<=p2`1
proof let i;assume i in dom h2;
then i in Seg len h2 by FINSEQ_1:def 3;
then A117:i in dom hb by A72,FINSEQ_1:def 3;
then A118:h2/.i=g1.(hb.i) by A79;
A119:hb.i in rng hb by A117,FUNCT_1:def 5;
dom g1= [#](I[01]) by A9,A11,TOPS_2:def 5
.=the carrier of I[01] by PRE_TOPC:12;
then A120:h2/.i in rng g by A11,A68,A118,A119,FUNCT_1:def 5;
rng g=[#]((TOP-REAL 2)|Q) by A9,TOPS_2:def 5
.=Q by PRE_TOPC:def 10;
hence thesis by A3,A120;
end;
for i st i in dom (X_axis(h2)) holds
p1`1<= (X_axis(h2)).i & (X_axis(h2)).i<=p2`1
proof let i;assume i in dom (X_axis(h2));
then i in Seg len (X_axis(h2)) by FINSEQ_1:def 3;
then i in Seg len h2 by A82,Th59;
then A121:i in dom h2 by FINSEQ_1:def 3;
then (X_axis(h2)).i = (h2/.i)`1 by Th61;
hence thesis by A116,A121;
end;
then A122:X_axis(h2) lies_between p1`1, p2`1 &
Y_axis(h2) lies_between (Y_axis(h2)).1, (Y_axis(h2)).(len h2)
by A112,GOBOARD4:def 1;
A123:for i st 1<=i & i+1<=len h2 holds
|. (h2/.i)-(h2/.(i+1)) .|<e
proof let i;assume A124:1<=i & i+1<=len h2;
then A125:i<len h2 by NAT_1:38;
A126:1<i+1 by A124,NAT_1:38;
then A127:i+1 in Seg len hb by A72,A124,FINSEQ_1:3;
i in Seg len hb by A72,A124,A125,FINSEQ_1:3;
then A128:h2'.i=g1.(hb.i) by A72;
then A129:h2/.i=g1.(hb.i) by A124,A125,FINSEQ_4:24;
A130:h2'.(i+1)=g1.(hb.(i+1)) by A72,A127;
h2.(i+1)=h2/.(i+1) by A124,A126,FINSEQ_4:24;
then A131:h2/.(i+1)=g1.(hb.(i+1)) by A72,A127;
i in Seg len hb by A72,A124,A125,FINSEQ_1:3;
then A132:i in dom hb by FINSEQ_1:def 3;
then A133:hb.i in rng hb by FUNCT_1:def 5;
A134: dom g1= [#](I[01]) by A9,A11,TOPS_2:def 5
.=the carrier of I[01] by PRE_TOPC:12;
then A135:h2'.i in rng g by A11,A68,A128,A133,FUNCT_1:def 5;
A136:rng g=[#]((TOP-REAL 2)|Q) by A9,TOPS_2:def 5
.=Q by PRE_TOPC:def 10;
i+1 in Seg len hb by A72,A124,A126,FINSEQ_1:3;
then i+1 in dom hb by FINSEQ_1:def 3;
then hb.(i+1) in rng hb by FUNCT_1:def 5;
then h2'.(i+1) in rng g by A11,A68,A130,A134,FUNCT_1:def 5;
then A137:g1.(hb.(i+1)) is Element of TOP-REAL 2 by A72,A127,
A136;
A138:hb.i=hb/.i by A72,A124,A125,FINSEQ_4:24;
i+1 in Seg len hb by A72,A124,A126,FINSEQ_1:3;
then A139:i+1 in dom hb by FINSEQ_1:def 3;
then A140:hb.(i+1) in rng hb by FUNCT_1:def 5;
A141:hb.(i+1)=hb/.(i+1) by A72,A124,A126,FINSEQ_4:24;
i<i+1 by NAT_1:38;
then A142:0<=hb/.i & hb/.i <= hb/.(i+1) & hb/.(i+1)<=1
by A68,A132,A133,A138,A139,A140,A141,BORSUK_1:83,GOBOARD1:def 1,
TOPREAL5:1;
reconsider W1=Q as Subset of Euclid 2 by A26;
reconsider Qa=Q as Subset of TOP-REAL 2;
A143:Qa is compact by A1,JORDAN5A:1;
reconsider Qa as non empty Subset of TOP-REAL 2;
reconsider R=[.hb/.i,hb/.(i+1).] as Subset of I[01]
by A68,A133,A138,A140,A141,BORSUK_1:83,
RCOMP_1:16;
reconsider w1=g1.(hb.i),w2=g1.(hb.(i+1)) as Point of Euclid 2
by A128,A135,A136,A137,TOPREAL3:13;
A144: hb.i in R by A138,A142,TOPREAL5:1;
hb.(i+1) in R by A141,A142,TOPREAL5:1;
then A145:w1 in g1.:(R) & w2 in g1.:(R) by A134,A144,FUNCT_1:def 12;
reconsider W=g1.:(R) as Subset of Euclid 2 by A26;
A146:dom g1=[#](I[01]) & rng g1=Q by A9,A11,A136,TOPS_2:def 5;
[#](I[01])=[.0,1.] by BORSUK_1:83,PRE_TOPC:12;
then Q=g1.:([.0,1.]) by A146,RELAT_1:146;
then A147:W c= W1 by BORSUK_1:83,RELAT_1:156;
q1 in Qa by A1,TOPREAL1:4;
then A148: W-bound Qa <= q1`1 & q1`1 <= E-bound Qa &
S-bound Qa <= q1`2 & q1`2 <= N-bound Qa by A143,PSCOMP_1:71;
set r1=
((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa))+1;
(W-bound Qa)<=(E-bound Qa) by A148,AXIOMS:22;
then A149:0<=((E-bound Qa) - (W-bound Qa)) by SQUARE_1:12;
(S-bound Qa)<=(N-bound Qa) by A148,AXIOMS:22;
then 0<=((N-bound Qa) - (S-bound Qa)) by SQUARE_1:12;
then A150:((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa))
>=0+0 by A149,REAL_1:55;
A151: r1> ((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa))
by REAL_1:69;
for x,y being Point of Euclid 2
st x in W1 & y in W1 holds dist(x,y)<=r1
proof let x,y be Point of Euclid 2;
assume A152: x in W1 & y in W1;
then reconsider pw1=x,pw2=y as Point of TOP-REAL 2;
A153:dist(x,y)=|.pw1-pw2.| by Th45;
A154:|.pw1-pw2.|<=abs(pw1`1-pw2`1)+abs(pw1`2-pw2`2) by Th49;
A155:W-bound Qa <= pw1`1 & pw1`1 <= E-bound Qa &
S-bound Qa <= pw1`2 & pw1`2 <= N-bound Qa
by A143,A152,PSCOMP_1:71;
A156:W-bound Qa <= pw2`1 & pw2`1 <= E-bound Qa &
S-bound Qa <= pw2`2 & pw2`2 <= N-bound Qa
by A143,A152,PSCOMP_1:71;
then A157:abs(pw1`1-pw2`1)<=(E-bound Qa) - (W-bound Qa) by A155,Th31
;
abs(pw1`2-pw2`2)<=(N-bound Qa) - (S-bound Qa) by A155,A156,Th31;
then A158:abs(pw1`1-pw2`1)+abs(pw1`2-pw2`2)
<=((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa))
by A157,REAL_1:55;
((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa))
<=
((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa))
+1 by REAL_1:69;
then abs(pw1`1-pw2`1)+abs(pw1`2-pw2`2)<=r1 by A158,AXIOMS:22;
hence thesis by A153,A154,AXIOMS:22;
end;
then W1 is bounded by A150,A151,TBSP_1:def 9;
then A159:W is bounded by A147,TBSP_1:21;
A160: diameter(W)<e by A68,A72,A124,A125;
dist(w1,w2)<=diameter(W) by A145,A159,TBSP_1:def 10;
then dist(w1,w2)<e by A160,AXIOMS:22;
hence thesis by A129,A131,Th45;
end;
consider f2 being FinSequence of TOP-REAL 2 such that
A161: f2 is special &
f2.1=h1.1 & f2.len f2=h1.len h1 & len f2>=len h1 &
X_axis(f2) lies_between (X_axis(h1)).1, (X_axis(h1)).(len h1) &
Y_axis(f2) lies_between q1`2,q2`2 &
(for j st j in dom f2 holds
ex k st k in dom h1 & |.(f2/.j - h1/.k).|<e)
&(for j st 1<=j & j+1<=len f2 holds |.f2/.j - f2/.(j+1).|<e)
by A17,A27,A67,A104,Th56;
A162:len f2>=1 by A67,A161,AXIOMS:22;
consider g2 being FinSequence of TOP-REAL 2 such that
A163: g2 is special &
g2.1=h2.1 & g2.len g2=h2.len h2 & len g2>=len h2 &
Y_axis(g2) lies_between (Y_axis(h2)).1, (Y_axis(h2)).(len h2) &
X_axis(g2) lies_between p1`1,p2`1 &
(for j st j in dom g2 holds
ex k st k in dom h2 & |.((g2/.j) - h2/.k).|<e)&
(for j st 1<=j & j+1<=len g2 holds |.(g2/.j) - g2/.(j+1).|<e)
by A17,A82,A122,A123,Th57;
A164:len g2>=1 by A82,A163,AXIOMS:22;
A165:1 in dom h by A19,A67,FINSEQ_3:27;
A166:len h in dom h by A19,A67,FINSEQ_3:27;
A167: h1.1=f1.(h.1) by A19,A25,A165;
A168:h1.1=h1/.1 by A67,FINSEQ_4:24;
A169:h1.len h1=h1/.len h1 by A67,FINSEQ_4:24;
A170:f2.1=f2/.1 by A162,FINSEQ_4:24;
A171:f2.len f2=f2/.len f2 by A162,FINSEQ_4:24;
A172:X_axis(f2).1=p1`1 by A8,A10,A18,A161,A162,A167,A170,Th59;
(h1/.len h1)=p2 by A8,A10,A18,A19,A25,A166,A169;
then A173:X_axis(f2).len f2=p2`1 by A161,A162,A169,A171,Th59;
A174:(h2/.1)=q1 by A9,A11,A68,A70,A79;
A175:h2.1=h2/.1 by A69,A72,FINSEQ_4:24;
A176:h2.len h2=h2/.len h2 by A69,A72,FINSEQ_4:24;
g2/.1=g2.1 by A164,FINSEQ_4:24;
then A177:Y_axis(g2).1=q1`2 by A163,A164,A174,A175,Th60;
A178:g2/.len g2=g2.len g2 by A164,FINSEQ_4:24;
(g2.len g2)=q2 by A9,A11,A68,A71,A72,A79,A163,A176;
then A179:Y_axis(g2).len g2=q2`2 by A164,A178,Th60;
A180:(X_axis(f2)).1=(h1/.1)`1 by A161,A162,A168,A170,Th59
.=(X_axis(h1)).1 by A67,Th59;
A181:X_axis(f2).len f2=(h1/.len h1)`1 by A161,A162,A169,A171,Th59
.=X_axis(h1).len h1 by A67,Th59;
g2.1=g2/.1 by A164,FINSEQ_4:24;
then A182:(Y_axis(g2)).1=(h2/.1)`2 by A163,A164,A175,Th60
.=(Y_axis(h2)).1 by A82,Th60;
g2.len g2=g2/.len g2 by A164,FINSEQ_4:24;
then A183: Y_axis(g2).len g2=(h2/.len h2)`2 by A163,A164,A176,Th60
.=Y_axis(h2).len h2 by A82,Th60;
5<=len f2 by A18,A19,A161,AXIOMS:22;
then A184:2<=len f2 by AXIOMS:22;
5<=len g2 by A68,A72,A163,AXIOMS:22;
then A185:2<=len g2 by AXIOMS:22;
A186:1<=len h by A18,AXIOMS:22;
then 1 in dom h by FINSEQ_3:27;
then A187:h1/.1=f1.(h.1) by A19,A25,A168;
len h in dom h by A186,FINSEQ_3:27;
then A188: f2/.1<>f2/.len f2 by A6,A8,A10,A18,A19,A25,A161,A168,A170,A171,
A187;
A189:1<=len hb by A68,AXIOMS:22;
then 1 in dom hb by FINSEQ_3:27;
then A190:h2/.1=g1.(hb.1) by A79;
len hb in dom hb by A189,FINSEQ_3:27;
then g2.1<>g2.len g2 by A7,A9,A11,A68,A72,A79,A163,A175,A176,A190;
then L~f2 meets L~g2 by A161,A163,A170,A171,A172,A173,A177,A179,A180,A181,
A182,A183,A184,A185,A188,Th30;
then consider s being set such that
A191:s in L~f2 & s in L~g2 by XBOOLE_0:3;
reconsider ps=s as Point of TOP-REAL 2 by A191;
ps in union{ LSeg(f2,i) : 1 <= i & i+1 <= len f2 }
by A191,TOPREAL1:def 6;
then consider x such that
A192: ps in x & x in
{ LSeg(f2,i) : 1 <= i & i+1 <= len f2 } by TARSKI:def 4;
consider i such that
A193: x=LSeg(f2,i) &(1 <= i & i+1 <= len f2) by A192;
A194:LSeg(f2,i)=LSeg(f2/.i,f2/.(i+1)) by A193,TOPREAL1:def 5;
i<len f2 by A193,NAT_1:38;
then i in dom f2 by A193,FINSEQ_3:27;
then consider k such that
A195: k in dom h1 & |.f2/.i - h1/.k.|<e by A161;
A196:|.ps-f2/.i.|<=|.f2/.i-f2/.(i+1).| by A192,A193,A194,Th53;
|.f2/.i-f2/.(i+1).|<e by A161,A193;
then A197:|.ps-f2/.i.|<e by A196,AXIOMS:22;
A198:|.ps-h1/.k.|<=|.ps-f2/.i.|+|.f2/.i-h1/.k.| by TOPRNS_1:35;
|.ps-f2/.i.|+|.f2/.i-h1/.k.|<e+e by A195,A197,REAL_1:67;
then A199:|.ps-h1/.k.|<e+e by A198,AXIOMS:22;
A200:k in Seg len h1 by A195,FINSEQ_1:def 3;
then A201:k in dom h by A19,FINSEQ_1:def 3;
1<=k & k<=len h1 by A200,FINSEQ_1:3;
then h1.k=h1/.k by FINSEQ_4:24;
then A202:h1/.k=f1.(h.k) by A19,A200;
A203:h.k in rng h by A201,FUNCT_1:def 5;
A204: dom f1= [#](I[01]) by A8,A10,TOPS_2:def 5
.=the carrier of I[01] by PRE_TOPC:12;
rng f=[#]((TOP-REAL 2)|P) by A8,TOPS_2:def 5
.=P by PRE_TOPC:def 10;
then A205: h1/.k in P by A10,A18,A202,A203,A204,FUNCT_1:def 5;
reconsider p11=h1/.k as Point of TOP-REAL 2;
A206: |.(p11-ps).|<e+e by A199,TOPRNS_1:28;
ps in union{ LSeg(g2,j) : 1 <= j & j+1 <=
len g2 } by A191,TOPREAL1:def 6;
then consider y such that
A207: ps in y &
y in { LSeg(g2,j) : 1 <= j & j+1 <= len g2 } by TARSKI:def 4;
consider j such that
A208:y=LSeg(g2,j) &(1 <= j & j+1 <= len g2) by A207;
A209: LSeg(g2,j)=LSeg((g2/.j),g2/.(j+1)) &
ps in LSeg(g2,j) & y=LSeg(g2,j) &(1 <= j & j+1 <= len g2)
by A207,A208,TOPREAL1:def 5;
j<len g2 &
LSeg(g2,j)=LSeg((g2/.j),g2/.(j+1)) &
ps in LSeg(g2,j) & y=LSeg(g2,j) &(1 <= j & j+1 <= len g2)
by A207,A208,NAT_1:38,TOPREAL1:def 5;
then j in Seg len g2 by FINSEQ_1:3;
then j in dom g2 by FINSEQ_1:def 3;
then consider k' being Nat such that
A210: k' in dom h2 & |.((g2/.j) - h2/.k').|<e by A163;
A211:|.ps-(g2/.j).|<=|.(g2/.j)-g2/.(j+1).| by A209,Th53;
|.(g2/.j)-g2/.(j+1).|<e by A163,A208;
then A212:|.ps-(g2/.j).|<e by A211,AXIOMS:22;
A213:|.ps-h2/.k'.|<=|.ps-(g2/.j).|+|.(g2/.j)-h2/.k'.| by TOPRNS_1:35;
|.ps-(g2/.j).|+|.(g2/.j)-(h2/.k').|<e+e by A210,A212,REAL_1:67;
then A214:|.ps-(h2/.k').|<e+e by A213,AXIOMS:22;
k' in Seg len h2 by A210,FINSEQ_1:def 3;
then k' in dom hb by A72,FINSEQ_1:def 3;
then A215:hb.k' in rng hb &
h2/.k'=g1.(hb.k') & k' in dom hb by A79,FUNCT_1:def 5;
dom g1= [#](I[01]) by A9,A11,TOPS_2:def 5
.=the carrier of I[01] by PRE_TOPC:12;
then A216:Q<>{}(TOP-REAL 2) &
h2/.k' in rng g & hb.k' in dom g1 by A11,A68,A215,FUNCT_1:def 5;
A217: rng g=[#]((TOP-REAL 2)|Q) by A9,TOPS_2:def 5
.=Q by PRE_TOPC:def 10;
reconsider q11=h2/.k' as Point of TOP-REAL 2;
reconsider x1=p11,x2=q11 as Point of Euclid 2 by A13,EUCLID:25;
min_dist_min(P',Q')<=dist(x1,x2) by A14,A205,A216,A217,WEIERSTR:40;
then A218:|.(p11-q11).|<= |.(p11-ps).|+|.(ps-q11).|
& min_dist_min(P',Q')<=|.(p11-q11).| by Th45,TOPRNS_1:35;
|.(p11-ps).|+|.(ps-q11).| <e+e+(e+e) by A206,A214,REAL_1:67;
then |.(p11-q11).|<e+e+(e+e) by A218,AXIOMS:22;
then |.(p11-q11).|<e+e+e+e by XCMPLX_1:1;
then |.(p11-q11).|<4*e by XCMPLX_1:13;
then min_dist_min(P',Q')<4*e by A218,AXIOMS:22;
then 4*e-5*e>0 by A16,SQUARE_1:11;
then (4-5)*e>0 by XCMPLX_1:40; then (4-5)*e/e>0 by A17,REAL_2:127;
then 4-5>0 by A17,XCMPLX_1:90;
hence contradiction;
end;
reserve X,Y for non empty TopSpace;
theorem Th63:for f being map of X,Y,
P being non empty Subset of Y,
f1 being map of X,Y|P st f=f1 & f is continuous holds
f1 is continuous
proof let f be map of X,Y,
P be non empty Subset of Y,
f1 be map of X,Y|P;
assume A1:f=f1 & f is continuous;
A2:rng f1 c= the carrier of (Y|P);
for P1 being Subset of (Y|P) st
P1 is open holds f1"P1 is open
proof let P1 be Subset of (Y|P);
assume P1 is open;
then P1 in the topology of (Y|P) by PRE_TOPC:def 5;
then consider Q being Subset of Y such that
A3: Q in the topology of Y &
P1 = Q /\ [#](Y|P) by PRE_TOPC:def 9;
reconsider Q as Subset of Y;
Q is open by A3,PRE_TOPC:def 5;
then A4:f"Q is open by A1,TOPS_2:55;
A5: [#](Y|P)=P by PRE_TOPC:def 10;
A6:f"Q=f1"(rng f1 /\ Q) by A1,RELAT_1:168;
Q /\ [#](Y|P) c= Q by XBOOLE_1:17;
then A7:f1"P1 c= f"Q by A1,A3,RELAT_1:178;
rng f1 c= P by A2,A5,PRE_TOPC:12;
then rng f1 /\ Q c= P /\ Q by XBOOLE_1:26;
then f1"(rng f1 /\ Q) c= f1"P1 by A3,A5,RELAT_1:178;
hence thesis by A4,A6,A7,XBOOLE_0:def 10;
end;
hence thesis by TOPS_2:55;
end;
theorem Th64:for f being map of X,Y,
P being non empty Subset of Y
st X is compact & Y is_T2 &
f is continuous one-to-one & P=rng f holds
ex f1 being map of X,(Y|P) st f=f1 & f1 is_homeomorphism
proof let f be map of X,Y,P be non empty Subset of Y such that
A1: X is compact and
A2: Y is_T2 and
A3: f is continuous one-to-one and
A4: P=rng f;
A5:f is Function of dom f,rng f by FUNCT_2:3;
A6:the carrier of (Y|P)=P by JORDAN1:1;
A7:dom f=the carrier of X by FUNCT_2:def 1;
then reconsider f2=f as map of X,(Y|P) by A4,A5,A6;
A8:dom f2=[#]X by A7,PRE_TOPC:12;
A9: rng f2=[#](Y|P) by A4,PRE_TOPC:def 10;
A10:Y|P is_T2 by A2,TOPMETR:3;
f2 is continuous by A3,Th63;
then f2 is_homeomorphism by A1,A3,A8,A9,A10,COMPTS_1:26;
hence thesis;
end;
:: Fashoda Meet Theorem
theorem for f,g being map of I[01],TOP-REAL 2,a,b,c,d being real number,
O,I being Point of I[01] st O=0 & I=1 &
f is continuous one-to-one &
g is continuous one-to-one &
(f.O)`1=a & (f.I)`1=b &
(g.O)`2=c & (g.I)`2=d &
(for r being Point of I[01] holds
a <=(f.r)`1 & (f.r)`1<=b & a <=(g.r)`1 & (g.r)`1<=b &
c <=(f.r)`2 & (f.r)`2<=d & c <=(g.r)`2 & (g.r)`2<=d)
holds rng f meets rng g
proof let f,g be map of I[01],TOP-REAL 2,a,b,c,d be real number,
O,I be Point of I[01];
assume A1: O=0 & I=1 &
f is continuous one-to-one & g is continuous one-to-one &
(f.O)`1=a & (f.I)`1=b & (g.O)`2=c & (g.I)`2=d &
(for r being Point of I[01] holds
a<=(f.r)`1 & (f.r)`1<=b & a<=(g.r)`1 & (g.r)`1<=b &
c <=(f.r)`2 & (f.r)`2<=d & c <=(g.r)`2 & (g.r)`2<=d);
A2:dom f= the carrier of I[01] by FUNCT_2:def 1
.=[#](I[01]) by PRE_TOPC:12;
A3:[#](I[01]) =[.0,1.] by BORSUK_1:83,PRE_TOPC:12;
then 0 in dom f by A2,TOPREAL5:1;
then reconsider P=rng f as non empty Subset of TOP-REAL 2
by FUNCT_1:12;
dom g= the carrier of I[01] by FUNCT_2:def 1
.=[#](I[01]) by PRE_TOPC:12;
then 0 in dom g by A3,TOPREAL5:1;
then reconsider Q=rng g as non empty Subset of TOP-REAL 2
by FUNCT_1:12;
A4:I[01] is compact by HEINE:11,TOPMETR:27;
A5:TOP-REAL 2 is_T2 by SPPOL_1:26;
then consider f1 being map of I[01],((TOP-REAL 2)|P) such that
A6: f=f1 & f1 is_homeomorphism by A1,A4,Th64;
consider g1 being map of I[01],((TOP-REAL 2)|Q) such that
A7:g=g1 & g1 is_homeomorphism by A1,A4,A5,Th64;
A8:dom f1= [#](I[01]) by A6,TOPS_2:def 5;
reconsider p1=f1.O as Point of TOP-REAL 2 by A1,A6;
reconsider p2=f1.I as Point of TOP-REAL 2 by A1,A6;
A9:dom g1= [#](I[01]) by A7,TOPS_2:def 5;
reconsider q1=g1.O as Point of TOP-REAL 2 by A1,A7;
reconsider q2=g1.I as Point of TOP-REAL 2 by A1,A7;
A10:P is_an_arc_of p1,p2 by A1,A6,TOPREAL1:def 2;
A11:Q is_an_arc_of q1,q2 by A1,A7,TOPREAL1:def 2;
A12:for p being Point of TOP-REAL 2 st p in P holds p1`1<=p`1 & p`1<= p2`1
proof let p be Point of TOP-REAL 2;
assume p in P; then consider x such that
A13:x in dom f1 & p=f1.x by A6,FUNCT_1:def 5;
reconsider r=x as Point of I[01] by A8,A13;
p=f.r by A6,A13;
hence thesis by A1,A6;
end;
A14:(for p being Point of TOP-REAL 2
st p in Q holds p1`1<=p`1 & p`1<= p2`1)
proof let p be Point of TOP-REAL 2;
assume p in Q; then consider x such that
A15:x in dom g1 & p=g1.x by A7,FUNCT_1:def 5;
reconsider r=x as Point of I[01] by A9,A15;
p=g.r by A7,A15;
hence thesis by A1,A6;
end;
A16:for p being Point of TOP-REAL 2 st p in P holds
q1`2<=p`2 & p`2<= q2`2
proof let p be Point of TOP-REAL 2;
assume p in P; then consider x such that
A17:x in dom f1 & p=f1.x by A6,FUNCT_1:def 5;
reconsider r=x as Point of I[01] by A8,A17;
p=f.r by A6,A17;
hence thesis by A1,A7;
end;
for p being Point of TOP-REAL 2 st p in Q holds q1`2<=p`2 & p`2<= q2`2
proof let p be Point of TOP-REAL 2;
assume p in Q; then consider x such that
A18:x in dom g1 & p=g1.x by A7,FUNCT_1:def 5;
reconsider r=x as Point of I[01] by A9,A18;
p=g.r by A7,A18;
hence thesis by A1,A7;
end;
hence thesis by A10,A11,A12,A14,A16,Th62;
end;