:: Reconstructions of Special Sequences
:: by Yatsuka Nakamura and Roman Matuszewski
::
:: Received December 10, 1996
:: Copyright (c) 1996-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, REAL_1, SUBSET_1, XBOOLE_0, FINSEQ_1, ARYTM_3,
XXREAL_0, ORDINAL4, FUNCT_1, ARYTM_1, RELAT_1, PARTFUN1, FINSEQ_5,
RFINSEQ, CARD_1, TARSKI, EUCLID, TOPREAL1, RLTOPSP1, PRE_TOPC, MCART_1,
SPPOL_2, GROUP_2, SUPINF_2, STRUCT_0, JORDAN3;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, REAL_1, NAT_1, RFINSEQ, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1,
FINSEQ_5, SEQ_4, FINSEQ_6, STRUCT_0, TOPREAL1, PRE_TOPC, RLVECT_1,
RLTOPSP1, EUCLID, SPPOL_2;
constructors REAL_1, SEQ_4, RFINSEQ, NAT_D, FINSEQ_5, TOPREAL1, BINOP_2,
RELSET_1, FINSEQ_6;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1,
MEMBERED, FINSEQ_1, FINSEQ_5, STRUCT_0, EUCLID, SPPOL_2, XXREAL_2,
CARD_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities RLTOPSP1, RLVECT_1;
expansions TARSKI;
theorems TARSKI, TOPREAL1, FINSEQ_1, FINSEQ_4, RFINSEQ, SPPOL_1, FUNCT_1,
NAT_1, TOPREAL3, SPPOL_2, FINSEQ_5, FINSEQ_6, ZFMISC_1, FINSEQ_3,
PARTFUN2, XBOOLE_0, XBOOLE_1, FINSEQ_2, XCMPLX_1, XREAL_1, XXREAL_0,
ORDINAL1, PARTFUN1, CARD_1, XXREAL_2, XREAL_0, NAT_D, RLTOPSP1, RLVECT_1;
begin
reserve r1,r2 for Real;
reserve n,i,i1,i2,j for Nat;
reserve D for non empty set;
reserve f for FinSequence of D;
theorem
for f being FinSequence of TOP-REAL n st 2<=len f holds f.1 in L~f & f
/.1 in L~f & f.len f in L~f & f/.len f in L~f
proof
let f be FinSequence of TOP-REAL n;
assume
A1: 2<=len f;
then
A2: 1+1<=len f;
then
A3: LSeg(f,1) in {LSeg(f,i):1<=i & i+1<=len f};
f/.1 in LSeg(f/.1,f/.(1+1)) by RLTOPSP1:68;
then f/.1 in LSeg(f,1) by A1,TOPREAL1:def 3;
then f/.1 in union{LSeg(f,i):1<=i & i+1<=len f} by A3,TARSKI:def 4;
then
A4: f/.1 in L~f by TOPREAL1:def 4;
A5: len f-'1+1=len f by A2,NAT_D:46,XREAL_1:235;
A6: 1<=len f-'1 by A2,NAT_D:49;
then
A7: LSeg(f,len f-'1) in {LSeg(f,i):1<=i & i+1<=len f} by A5;
f/.len f in LSeg(f/.(len f-'1),f/.(len f-'1+1)) by A5,RLTOPSP1:68;
then f/.len f in LSeg(f,len f-'1) by A6,A5,TOPREAL1:def 3;
then f/.len f in union{LSeg(f,i):1<=i & i+1<=len f} by A7,TARSKI:def 4;
then
A8: f/.len f in L~f by TOPREAL1:def 4;
1<=len f by A2,NAT_D:46;
hence thesis by A4,A8,FINSEQ_4:15;
end;
theorem Th2:
for p1,p2,q1,q2 being Point of TOP-REAL 2 st (p1`1 = p2`1 or p1
`2 = p2`2)& q1 in LSeg(p1,p2) & q2 in LSeg(p1,p2) holds q1`1 = q2`1 or q1`2 =
q2`2
proof
let p1,p2,q1,q2 be Point of TOP-REAL 2;
assume that
A1: p1`1 = p2`1 or p1`2 = p2`2 and
A2: q1 in LSeg(p1,p2) and
A3: q2 in LSeg(p1,p2);
consider r2 such that
A4: q2= (1-r2)*p1 + r2*p2 and
0 <= r2 and
r2 <= 1 by A3;
consider r1 such that
A5: q1= (1-r1)*p1 + r1*p2 and
0 <= r1 and
r1 <= 1 by A2;
q1`1=((1-r1)*p1)`1+(r1*p2)`1 by A5,TOPREAL3:2;
then q1`1=(1-r1)*(p1`1)+(r1*p2)`1 by TOPREAL3:4;
then
A6: q1`1=(1-r1)*(p1`1)+r1*(p2`1) by TOPREAL3:4;
q2`1=((1-r2)*p1)`1+(r2*p2)`1 by A4,TOPREAL3:2;
then q2`1=(1-r2)*(p1`1)+(r2*p2)`1 by TOPREAL3:4;
then
A7: q2`1=(1-r2)*(p1`1)+r2*(p2`1) by TOPREAL3:4;
q1`2=((1-r1)*p1)`2+(r1*p2)`2 by A5,TOPREAL3:2;
then q1`2=(1-r1)*(p1`2)+(r1*p2)`2 by TOPREAL3:4;
then
A8: q1`2=(1-r1)*(p1`2)+r1*(p2`2) by TOPREAL3:4;
q2`2=((1-r2)*p1)`2+(r2*p2)`2 by A4,TOPREAL3:2;
then q2`2=(1-r2)*(p1`2)+(r2*p2)`2 by TOPREAL3:4;
then
A9: q2`2=(1-r2)*(p1`2)+r2*(p2`2) by TOPREAL3:4;
per cases by A1;
suppose
p1`1 = p2`1;
hence thesis by A6,A7;
end;
suppose
p1`2 = p2`2;
hence thesis by A8,A9;
end;
end;
theorem Th3:
for p1,p2,q1,q2 being Point of TOP-REAL 2 st (p1`1 = p2`1 or p1
`2 = p2`2)& LSeg(q1,q2) c= LSeg(p1,p2) holds q1`1 = q2`1 or q1`2 = q2`2
proof
let p1,p2,q1,q2 be Point of TOP-REAL 2;
A1: q2 in LSeg(q1,q2) by RLTOPSP1:68;
q1 in LSeg(q1,q2) by RLTOPSP1:68;
hence thesis by A1,Th2;
end;
theorem Th4:
for f being FinSequence of TOP-REAL 2,n being Element of NAT st
2<=n & f is being_S-Seq holds f|n is being_S-Seq
proof
let f be FinSequence of TOP-REAL 2,n be Element of NAT;
assume that
A1: 2<=n and
A2: f is being_S-Seq;
A3: len f >= 2 by A2,TOPREAL1:def 8;
A4: now
per cases;
case
n<=len f;
hence len (f|n) >= 2 by A1,FINSEQ_1:59;
end;
case
n>len f;
hence len (f|n) >= 2 by A3,FINSEQ_1:58;
end;
end;
reconsider f9=f as s.n.c. special unfolded one-to-one FinSequence of
TOP-REAL 2 by A2;
f9|n is one-to-one;
hence thesis by A4,TOPREAL1:def 8;
end;
theorem Th5:
for f being FinSequence of TOP-REAL 2,n being Element of NAT st
n<=len f & 2<=len f-'n & f is being_S-Seq holds f/^n is being_S-Seq
proof
let f be FinSequence of TOP-REAL 2,n be Element of NAT;
assume that
A1: n<=len f and
A2: 2<=len f-'n and
A3: f is being_S-Seq;
reconsider f9 = f as one-to-one special s.n.c. unfolded FinSequence of
TOP-REAL 2 by A3;
len (f/^n)=len f-n by A1,RFINSEQ:def 1;
then len (f9/^n) >= 2 by A1,A2,XREAL_1:233;
hence thesis by TOPREAL1:def 8;
end;
theorem
for f being FinSequence of TOP-REAL 2,k1,k2 being Element of NAT st f
is being_S-Seq & 1<=k1 & k1<=len f & 1<=k2 & k2<=len f & k1<>k2 holds mid(f,k1,
k2) is being_S-Seq
proof
let f be FinSequence of TOP-REAL 2,k1,k2 be Element of NAT;
assume that
A1: f is being_S-Seq and
A2: 1<=k1 and
A3: k1<=len f and
A4: 1<=k2 and
A5: k2<=len f and
A6: k1<>k2;
per cases;
suppose
A7: k1<=k2;
then k1<k2 by A6,XXREAL_0:1;
then
A8: k1+1<=k2 by NAT_1:13;
then k1+1-k1<=k2-k1 by XREAL_1:9;
then 1<=k2-'k1 by NAT_D:39;
then
A9: 1+1<=k2-'k1+1 by XREAL_1:6;
k1+1<=len f by A5,A8,XXREAL_0:2;
then k1+1-k1<=len f-k1 by XREAL_1:9;
then
A10: 1+1<=len f-k1+1 by XREAL_1:6;
len f-'(k1-'1)= len f-(k1-'1) by A3,NAT_D:50,XREAL_1:233
.=len f-(k1-1) by A2,XREAL_1:233
.=len f-k1+1;
then
A11: f/^(k1-'1) is being_S-Seq by A1,A3,A10,Th5,NAT_D:50;
mid(f,k1,k2)=(f/^(k1-'1))|(k2-'k1+1) by A7,FINSEQ_6:def 3;
hence thesis by A11,A9,Th4;
end;
suppose
A12: k1>k2;
then
A13: k2+1<=k1 by NAT_1:13;
then k2+1-k2<=k1-k2 by XREAL_1:9;
then 1<=k1-'k2 by NAT_D:39;
then
A14: 1+1<=k1-'k2+1 by XREAL_1:6;
k2+1<=len f by A3,A13,XXREAL_0:2;
then k2+1-k2<=len f-k2 by XREAL_1:9;
then
A15: 1+1<=len f-k2+1 by XREAL_1:6;
len f-'(k2-'1)= len f-(k2-'1) by A5,NAT_D:50,XREAL_1:233
.=len f-(k2-1) by A4,XREAL_1:233
.=len f-k2+1;
then f/^(k2-'1) is being_S-Seq by A1,A5,A15,Th5,NAT_D:50;
then
A16: (f/^(k2-'1))|(k1-'k2+1) is S-Sequence_in_R2 by A14,Th4;
mid(f,k1,k2)= Rev ((f/^(k2-'1))|(k1-'k2+1)) by A12,FINSEQ_6:def 3;
hence thesis by A16;
end;
end;
begin
::---------------------------------------------------------:
:: A Concept of Index for Finite Sequences in TOP-REAL 2 :
::---------------------------------------------------------:
definition
let f be FinSequence of TOP-REAL 2,p be Point of TOP-REAL 2;
assume
A1: p in L~f;
func Index(p,f) -> Element of NAT means
:Def1:
ex S being non empty Subset of NAT st it = min S & S = { i: p in LSeg(f,i) };
existence
proof
set S = { i: p in LSeg(f,i) };
A2: S c= NAT
proof
let x be object;
assume x in S;
then ex i st x = i & p in LSeg(f,i);
hence thesis by ORDINAL1:def 12;
end;
consider i2 being Nat such that
1<=i2 and
i2+1<=len f and
A3: p in LSeg(f,i2) by A1,SPPOL_2:13;
i2 in S by A3;
then reconsider S as non empty Subset of NAT by A2;
take min S, S;
thus thesis;
end;
uniqueness;
end;
theorem Th7:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL
2, i being Element of NAT st p in LSeg(f,i) holds Index(p,f) <= i
proof
let f being FinSequence of TOP-REAL 2;
let p being Point of TOP-REAL 2, i0 be Element of NAT;
assume
A1: p in LSeg(f,i0);
LSeg(f,i0) c= L~f by TOPREAL3:19;
then consider S being non empty Subset of NAT such that
A2: Index(p,f) = min S and
A3: S = { i: p in LSeg(f,i) } by A1,Def1;
i0 in S by A1,A3;
hence thesis by A2,XXREAL_2:def 7;
end;
theorem Th8:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL
2 st p in L~f holds 1<=Index(p,f) & Index(p,f) < len f
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume p in L~f;
then consider S being non empty Subset of NAT such that
A1: Index(p,f) = min S and
A2: S = { i: p in LSeg(f,i) } by Def1;
Index(p,f) in S by A1,XXREAL_2:def 7;
then
A3: ex i st i = Index(p,f) & p in LSeg(f,i) by A2;
hence 1 <= Index(p,f) by TOPREAL1:def 3;
Index(p,f) + 1 <= len f by A3,TOPREAL1:def 3;
hence thesis by NAT_1:13;
end;
theorem Th9:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL
2 st p in L~f holds p in LSeg(f,Index(p,f))
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume p in L~f;
then consider S being non empty Subset of NAT such that
A1: Index(p,f) = min S and
A2: S = { i: p in LSeg(f,i) } by Def1;
Index(p,f) in S by A1,XXREAL_2:def 7;
then ex i st i = Index(p,f) & p in LSeg(f,i) by A2;
hence thesis;
end;
theorem Th10:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL
2 st p in LSeg(f,1) holds Index(p,f) = 1
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume
A1: p in LSeg(f,1);
then
A2: Index(p,f) <= 1 by Th7;
LSeg(f,1) c= L~f by TOPREAL3:19;
then Index(p,f) >= 1 by A1,Th8;
hence thesis by A2,XXREAL_0:1;
end;
theorem Th11:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL
2 st len f >= 2 holds Index(f/.1,f) = 1
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume len f >= 2;
then len f >= 1+1;
then f/.1 in LSeg(f,1) by TOPREAL1:21;
hence thesis by Th10;
end;
theorem Th12:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL
2,i1 being Nat st f is being_S-Seq & 1<i1 & i1<=len f & p=f.i1 holds Index(p,f)
+ 1 = i1
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2,i1 be Nat;
assume
A1: f is being_S-Seq;
assume that
A2: 1<i1 and
A3: i1<=len f;
A4: i1 in dom f by A2,A3,FINSEQ_3:25;
assume p=f.i1;
then
A5: p = f/.i1 by A4,PARTFUN1:def 6;
assume
A6: Index(p,f) + 1 <> i1;
consider j being Nat such that
A7: i1 = j+1 by A2,NAT_1:6;
reconsider j as Element of NAT by ORDINAL1:def 12;
A8: 1 + 0 <= j by A2,A7,NAT_1:13;
then
A9: p in LSeg(f,j) by A3,A7,A5,TOPREAL1:21;
then Index(p,f) <= j by Th7;
then Index(p,f) < j by A7,A6,XXREAL_0:1;
then
A10: Index(p,f) + 1 <= j by NAT_1:13;
A11: LSeg(f,j) c= L~f by TOPREAL3:19;
then
A12: p in LSeg(f,Index(p,f)) by A9,Th9;
per cases by A10,XXREAL_0:1;
suppose
A13: Index(p,f) + 1 = j;
then
A14: Index(p,f) + (1+1) <= len f by A3,A7;
1 <= Index(p,f) by A9,A11,Th8;
then LSeg(f,Index(p,f)) /\ LSeg(f,j) = {f/.j} by A1,A13,A14,TOPREAL1:def 6;
then p in {f/.j} by A9,A12,XBOOLE_0:def 4;
then
A15: p = f/.j by TARSKI:def 1;
j < len f by A3,A7,NAT_1:13;
then
A16: j in dom f by A8,FINSEQ_3:25;
j < i1 by A7,NAT_1:13;
hence contradiction by A1,A4,A5,A15,A16,PARTFUN2:10;
end;
suppose
A17: Index(p,f) + 1 < j;
p in LSeg(f,Index(p,f)) /\ LSeg(f,j) by A9,A12,XBOOLE_0:def 4;
then LSeg(f,Index(p,f)) meets LSeg(f,j) by XBOOLE_0:4;
hence contradiction by A1,A17,TOPREAL1:def 7;
end;
end;
theorem Th13:
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
for i1 be Element of NAT st f is s.n.c. & p in LSeg(f,i1) holds i1=Index(p,f)
or i1=Index(p,f)+1
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
let i1 be Element of NAT;
assume that
A1: f is s.n.c. and
A2: p in LSeg(f,i1);
p in L~f by A2,SPPOL_2:17;
then p in LSeg(f,Index(p,f)) by Th9;
then p in LSeg(f,Index(p,f)) /\ LSeg(f,i1) by A2,XBOOLE_0:def 4;
then
A3: LSeg(f,Index(p,f)) meets LSeg(f,i1) by XBOOLE_0:4;
assume
A4: not thesis;
Index(p,f) <= i1 by A2,Th7;
then Index(p,f) < i1 by A4,XXREAL_0:1;
then Index(p,f)+1 <= i1 by NAT_1:13;
then Index(p,f)+1 < i1 by A4,XXREAL_0:1;
hence contradiction by A1,A3,TOPREAL1:def 7;
end;
theorem Th14:
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
for i1 be Element of NAT st f is unfolded s.n.c. & i1+1<=len f & p in LSeg(f,i1
) & p <> f.i1 holds i1=Index(p,f)
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
let i1 be Element of NAT;
assume that
A1: f is unfolded s.n.c. and
A2: i1+1<=len f and
A3: p in LSeg(f,i1);
A4: i1 < len f by A2,NAT_1:13;
A5: 1 <= Index(p,f)+1 by NAT_1:11;
Index(p,f) <= i1 by A3,Th7;
then Index(p,f) < len f by A4,XXREAL_0:2;
then Index(p,f)+1 <= len f by NAT_1:13;
then
A6: Index(p,f) + 1 in dom f by A5,FINSEQ_3:25;
assume
A7: p <> f.i1;
A8: p in L~f by A3,SPPOL_2:17;
then p in LSeg(f,Index(p,f)) by Th9;
then
A9: p in LSeg(f,Index(p,f)) /\ LSeg(f,i1) by A3,XBOOLE_0:def 4;
A10: 1 <= Index(p,f) by A8,Th8;
now
assume
A11: i1 = Index(p,f)+1;
then Index(p,f) + (1+1) <= len f by A2;
then p in {f/.(Index(p,f)+1)} by A1,A9,A10,A11,TOPREAL1:def 6;
then p = f/.(Index(p,f)+1) by TARSKI:def 1;
hence contradiction by A7,A6,A11,PARTFUN1:def 6;
end;
hence thesis by A1,A3,Th13;
end;
definition
let g be FinSequence of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
pred g is_S-Seq_joining p1,p2 means
g is being_S-Seq & g.1 = p1 & g. len g = p2;
end;
theorem Th15:
for g being FinSequence of TOP-REAL 2, p1,p2 being Point of
TOP-REAL 2 st g is_S-Seq_joining p1,p2 holds Rev g is_S-Seq_joining p2,p1
proof
let g be FinSequence of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
assume that
A1: g is being_S-Seq and
A2: g.1=p1 and
A3: g.len g=p2;
thus Rev g is being_S-Seq by A1;
thus (Rev g).1 = p2 by A3,FINSEQ_5:62;
dom g = dom Rev g by FINSEQ_5:57;
hence (Rev g).len Rev g = (Rev g).len g by FINSEQ_3:29
.= p1 by A2,FINSEQ_5:62;
end;
theorem Th16:
for f,g being FinSequence of TOP-REAL 2, p being Point of
TOP-REAL 2,j be Nat st p in L~f & g=<*p*>^mid(f,Index(p,f)+1,len f) & 1<=j & j+
1<=len g holds LSeg(g,j) c= LSeg(f,Index(p,f)+j-'1)
proof
let f,g be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2,j be Nat;
assume that
A1: p in L~f and
A2: g=<*p*>^mid(f,Index(p,f)+1,len f) and
A3: 1<=j and
A4: j+1<=len g;
A5: j<=len g by A4,NAT_1:13;
len g=len <*p*> + len mid(f,Index(p,f)+1,len f) by A2,FINSEQ_1:22;
then
A6: len g=1+len mid(f,Index(p,f)+1,len f) by FINSEQ_1:39;
then
A7: j+1-1<=1+len mid(f,Index(p,f)+1,len f)-1 by A4,XREAL_1:9;
j-'1<=j by NAT_D:35;
then
A8: j-'1<=len mid(f,Index(p,f)+1,len f) by A7,XXREAL_0:2;
1<=Index(p,f)+j by A3,NAT_1:12;
then
A9: 1-1<=Index(p,f)+j-1 by XREAL_1:9;
A10: j-'1=j-1 by A3,XREAL_1:233;
A11: j=1+(j-1) .=len <*p*> +(j-'1) by A10,FINSEQ_1:39;
1 <= Index(p,f) by A1,Th8;
then 1+1 <= Index(p,f)+j by A3,XREAL_1:7;
then 1<=Index(p,f)+j-1 by XREAL_1:19;
then
A12: 1<=Index(p,f)+j-'1 by NAT_D:39;
consider i such that
1<=i and
A13: i+1<=len f and
p in LSeg(f,i) by A1,SPPOL_2:13;
1<=i+1 by NAT_1:12;
then
A14: 1<=len f by A13,XXREAL_0:2;
A15: Index(p,f)<len f by A1,Th8;
then
A16: Index(p,f)+1<=len f by NAT_1:13;
Index(p,f)+1<=len f by A15,NAT_1:13;
then Index(p,f)+1-Index(p,f)<=len f - Index(p,f) by XREAL_1:9;
then
A17: 1-1<=len f - Index(p,f)-1 by XREAL_1:9;
then
A18: len f -'(Index(p,f)+1)=len f -(Index(p,f)+1) by XREAL_0:def 2
.=len f - Index(p,f) -1;
A19: 0+1<=Index(p,f)+1 by NAT_1:13;
then
A20: 1<=len f by A15,NAT_1:13;
Index(p,f)+1<=len f by A15,NAT_1:13;
then
A21: len(mid(f,Index(p,f)+1,len f))=len f -' (Index(p,f)+1)+1 by A14,A19,
FINSEQ_6:118;
A22: len g=(len <*p*>)+ len(mid(f,Index(p,f)+1,len f)) by A2,FINSEQ_1:22
.=1+ len(mid(f,Index(p,f)+1,len f)) by FINSEQ_1:39;
then len g=1+(len f -(Index(p,f)+1)+1) by A17,A21,XREAL_0:def 2
.=1+(len f - Index(p,f));
then j<=len f - Index(p,f) by A4,XREAL_1:6;
then
A23: j+Index(p,f)<=len f - Index(p,f)+Index(p,f) by XREAL_1:6;
then
A24: Index(p,f)+j-'1+1<=len f by A3,NAT_1:12,XREAL_1:235;
A25: 1<=j+1 by A3,NAT_1:13;
then
A26: g/.(j+1)=g.(j+1) by A4,FINSEQ_4:15;
A27: j+1=len <*p*> +(j+1-1) by FINSEQ_1:39
.=len <*p*> +(j+1-'1) by A25,XREAL_1:233;
A28: j+1-'1=j+1-1 by A25,XREAL_1:233;
then j+1-'1 in dom mid(f,Index(p,f)+1,len f) by A3,A7,FINSEQ_3:25;
then g.(j+1) =mid(f,Index(p,f)+1,len f).(j+1-'1) by A2,A27,FINSEQ_1:def 7
.=f.(j+1-'1+(Index(p,f)+1)-'1) by A3,A19,A16,A20,A28,A7,FINSEQ_6:118
.=f.(j+1-'1+1+Index(p,f)-'1)
.=f.(j+1+Index(p,f)-'1) by A25,XREAL_1:235
.=f.(Index(p,f)+j+1-'1)
.=f.(Index(p,f)+j) by NAT_D:34
.=f.(Index(p,f)+j-'1+1) by A3,NAT_1:12,XREAL_1:235;
then
A29: f/.(Index(p,f)+j-'1+1)=g/.(j+1) by A24,A26,FINSEQ_4:15,NAT_1:11;
j+1-1<=1+len mid(f,Index(p,f)+1,len f)-1 by A4,A6,XREAL_1:9;
then j+Index(p,f)<= len f -Index(p,f)+Index(p,f) by A21,A18,XREAL_1:6;
then Index(p,f)+(j-1)+1 <= len f;
then Index(p,f)+j-'1+1 <= len f by A9,XREAL_0:def 2;
then
A30: LSeg(f,Index(p,f)+j-'1) =LSeg(f/.(Index(p,f)+j-'1),f/.(Index(p,f)+j-'1+
1)) by A12,TOPREAL1:def 3;
A31: 1<=len g by A22,NAT_1:11;
now
per cases by A3,XXREAL_0:1;
case
A32: 1<j;
then
A33: j-'1=j-1 by XREAL_1:233;
then
A34: 1<=j-'1 by A32,SPPOL_1:1;
j-1<=1+len mid(f,Index(p,f)+1,len f)-1 by A6,A5,XREAL_1:9;
then j-'1 in dom mid(f,Index(p,f)+1,len f) by A33,A34,FINSEQ_3:25;
then
A35: g.j =mid(f,Index(p,f)+1,len f).(j-'1) by A2,A11,FINSEQ_1:def 7
.=f.(j-'1+(Index(p,f)+1)-'1) by A19,A16,A20,A8,A34,FINSEQ_6:118
.=f.(j-'1+1+Index(p,f)-'1)
.=f.(Index(p,f)+j-'1) by A3,XREAL_1:235;
g/.j=g.j by A3,A5,FINSEQ_4:15;
then
LSeg(f,Index(p,f)+j-'1) =LSeg(g/.j,g/.(j+1)) by A23,A29,A12,A30,A35,
FINSEQ_4:15,NAT_D:50
.=LSeg(g,j) by A3,A4,TOPREAL1:def 3;
hence thesis;
end;
case
A36: 1=j;
then j<=len <*p*> by FINSEQ_1:39;
then j in dom <*p*> by A36,FINSEQ_3:25;
then
A37: g.j =<*p*>.j by A2,FINSEQ_1:def 7
.=p by A36;
A38: f/.(Index(p,f)+j-'1+1) in LSeg(f/.(Index(p,f)+j-'1),f/.(Index(p,f)+
j-'1+1)) by RLTOPSP1:68;
A39: g/.j=g.j by A31,A36,FINSEQ_4:15;
A40: Index(p,f)+j-'1 = Index(p,f) by A36,NAT_D:34;
p in LSeg(f,Index(p,f)) by A1,Th9;
then LSeg(p,g/.(j+1)) c= LSeg(f,Index(p,f)+j-'1) by A29,A30,A38,A40,
TOPREAL1:6;
hence thesis by A3,A4,A37,A39,TOPREAL1:def 3;
end;
end;
hence thesis;
end;
theorem
for f,g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2
st f is being_S-Seq & p in L~f & p<>f.(Index(p,f)+1) & g=<*p*>^mid(f,Index(p,f)
+1,len f) holds g is_S-Seq_joining p,f/.len f
proof
let f,g be FinSequence of TOP-REAL 2,p be Point of TOP-REAL 2;
assume that
A1: f is being_S-Seq and
A2: p in L~f and
A3: p<>f.(Index(p,f)+1) and
A4: g=<*p*>^mid(f,Index(p,f)+1,len f);
len g=len <*p*> + len mid(f,Index(p,f)+1,len f) by A4,FINSEQ_1:22;
then
A5: len g=1+len mid(f,Index(p,f)+1,len f) by FINSEQ_1:39;
consider i such that
1<=i and
A6: i+1<=len f and
p in LSeg(f,i) by A2,SPPOL_2:13;
1<=1+i by NAT_1:12;
then
A7: 1<=len f by A6,XXREAL_0:2;
A8: for j1,j2 be Nat st j1+1 < j2 holds LSeg(g,j1) misses LSeg(g,j2)
proof
let j1,j2 be Nat;
assume
A9: j1+1 < j2;
A10: j1=0 or j1>=0+1 by NAT_1:13;
now
per cases by A10,XXREAL_0:1;
case
j1=0;
then LSeg(g,j1)={} by TOPREAL1:def 3;
then LSeg(g,j1) /\ LSeg(g,j2) = {};
hence thesis by XBOOLE_0:def 7;
end;
case that
A11: j1=1 or j1>1 and
A12: j2+1<=len g;
1<j1+1 by A11,NAT_1:13;
then 1<=j2 by A9,XXREAL_0:2;
then
A13: LSeg(g,j2) c= LSeg(f,Index(p,f)+j2-'1) by A2,A4,A12,Th16;
1<=Index(p,f)+j1 by A2,Th8,NAT_1:12;
then 1-1<=Index(p,f)+j1-1 by XREAL_1:9;
then
A14: Index(p,f)+j1-1=Index(p,f)+j1-'1 by XREAL_0:def 2;
Index(p,f)+(j1+1)<Index(p,f)+j2 by A9,XREAL_1:6;
then Index(p,f)+j1+1-1<Index(p,f)+j2-1 by XREAL_1:9;
then Index(p,f)+j1-'1+1<Index(p,f)+j2-'1 by A14,XREAL_0:def 2;
then LSeg(f,Index(p,f)+j1-'1) misses LSeg(f,Index(p,f)+j2-'1) by A1,
TOPREAL1:def 7;
then
A15: LSeg(f,Index(p,f)+j1-'1) /\ LSeg(f,Index(p,f)+j2-'1) = {} by
XBOOLE_0:def 7;
j2<len g by A12,NAT_1:13;
then j1+1<=len g by A9,XXREAL_0:2;
then LSeg(g,j1) c= LSeg(f,Index(p,f)+j1-'1) by A2,A4,A11,Th16;
then LSeg(g,j1) /\ LSeg(g,j2) = {} by A13,A15,XBOOLE_1:3,27;
hence thesis by XBOOLE_0:def 7;
end;
case
j2+1>len g;
then LSeg(g,j2)={} by TOPREAL1:def 3;
then LSeg(g,j1) /\ LSeg(g,j2) = {};
hence thesis by XBOOLE_0:def 7;
end;
end;
hence thesis;
end;
A16: Index(p,f)<len f by A2,Th8;
then
A17: Index(p,f)+1<=len f by NAT_1:13;
Index(p,f)+1<=len f by A16,NAT_1:13;
then
A18: Index(p,f)+1-Index(p,f)<=len f - Index(p,f) by XREAL_1:9;
then
A19: 1-1<=len f - Index(p,f)-1 by XREAL_1:9;
then
A20: len f -'(Index(p,f)+1)=len f -(Index(p,f)+1) by XREAL_0:def 2
.=len f - Index(p,f) -1;
A21: 0+1<=Index(p,f)+1 by NAT_1:11;
then
A22: len(mid(f,Index(p,f)+1,len f))=len f -' (Index(p,f)+1)+1 by A7,A17,
FINSEQ_6:118;
A23: for j be Nat st 1 <= j & j + 2 <= len g holds LSeg(g,j) /\ LSeg(g,j+1)
= {g/.(j+1)}
proof
let j be Nat;
assume that
A24: 1 <= j and
A25: j + 2 <= len g;
A26: j+2=j+1+1;
then
A27: j+1<=len g by A25,NAT_1:13;
then
A28: LSeg(g,j) c= LSeg(f,Index(p,f)+j-'1) by A2,A4,A24,Th16;
1<=(j+1) by A24,NAT_1:13;
then
LSeg(g,(j+1)) c= LSeg(f,Index(p,f)+(j+1)-'1) by A2,A4,A25,A26,Th16;
then
A29: LSeg(g,j)/\ LSeg(g,(j+1)) c= LSeg(f,Index(p,f)+j-'1)/\ LSeg(f,Index(
p,f)+(j+1)-'1) by A28,XBOOLE_1:27;
A30: 1<=Index(p,f) by A2,Th8;
1 <= Index(p,f) by A2,Th8;
then 1+1 <= Index(p,f)+j by A24,XREAL_1:7;
then 1<=Index(p,f)+j-1 by XREAL_1:19;
then
A31: 1<=Index(p,f)+j-'1 by NAT_D:39;
1<=Index(p,f)+j by A2,Th8,NAT_1:12;
then
A32: 1-1<=Index(p,f)+j-1 by XREAL_1:9;
j+1+1-1<=1+len mid(f,Index(p,f)+1,len f)-1 by A5,A25,XREAL_1:9;
then
A33: j+1+Index(p,f)<= len f -Index(p,f)+Index(p,f) by A22,A20,XREAL_1:6;
then Index(p,f)+j+1 <= len f;
then Index(p,f)+(j-1)+1 <= len f by NAT_D:46;
then
A34: Index(p,f)+j-'1+1 <= len f by A32,XREAL_0:def 2;
Index(p,f)+j-1+(1+1) <= len f by A33;
then Index(p,f)+j-'1+2 <= len f by A32,XREAL_0:def 2;
then
A35: {f/.(Index(p,f)+j-'1+1)} = LSeg(f,Index(p,f)+j-'1)/\ LSeg(f,Index(p,
f)+j-'1+1) by A1,A31,TOPREAL1:def 6;
A36: 1<j+1 by A24,NAT_1:13;
then
A37: g/.(j+1)=g.(j+1) by A27,FINSEQ_4:15;
A38: g/.(j+1) in LSeg(g/.(j+1),g/.(j+1+1)) by RLTOPSP1:68;
g/.(j+1) in LSeg(g/.j,g/.(j+1)) by RLTOPSP1:68;
then
A39: g/.(j+1) in LSeg(g/.j,g/.(j+1)) /\ LSeg(g/.(j+1),g/.(j+1+1)) by A38,
XBOOLE_0:def 4;
A40: LSeg(g,j)=LSeg(g/.j,g/.(j+1)) by A24,A27,TOPREAL1:def 3;
LSeg(g/.(j+1),g/.(j+1+1))=LSeg(g,j+1) by A25,A36,TOPREAL1:def 3;
then
A41: {g/.(j+1)} c= LSeg(g,j) /\ LSeg(g,j+1) by A40,A39,ZFMISC_1:31;
A42: j+1=j+1-1+1 .=j+1-'1+1 by A36,XREAL_1:233;
then
A43: j+1=len <*p*>+(j+1-'1) by FINSEQ_1:39;
A44: j+1-'1<=len mid(f,Index(p,f)+1,len f) by A5,A27,A42,XREAL_1:6;
then j+1-'1 in dom mid(f,Index(p,f)+1,len f) by A24,A42,FINSEQ_3:25;
then g.(j+1) = mid(f,Index(p,f)+1,len f).(j+1-'1) by A4,A43,FINSEQ_1:def 7
.=f.(j+1-'1+(Index(p,f)+1)-'1) by A7,A17,A21,A24,A42,A44,FINSEQ_6:118
.=f.(j+1-'1+1+Index(p,f)-'1)
.=f.(j+1+Index(p,f)-'1) by A36,XREAL_1:235
.=f.(Index(p,f)+j+1-'1)
.=f.(Index(p,f)+j) by NAT_D:34
.=f.(Index(p,f)+j-'1+1) by A30,NAT_1:12,XREAL_1:235;
then
A45: f/.(Index(p,f)+j-'1+1)=g/.(j+1) by A37,A34,FINSEQ_4:15,NAT_1:11;
Index(p,f)+(j+1)-'1 =Index(p,f)+j+1-1 by NAT_1:11,XREAL_1:233
.=Index(p,f)+j-1+1
.=Index(p,f)+j-'1+1 by A30,NAT_1:12,XREAL_1:233;
hence thesis by A29,A35,A45,A41,XBOOLE_0:def 10;
end;
A46: len g=(len <*p*>)+ len(mid(f,Index(p,f)+1,len f)) by A4,FINSEQ_1:22
.=1+ len(mid(f,Index(p,f)+1,len f)) by FINSEQ_1:39;
then
A47: len g=1+(len f -(Index(p,f)+1)+1) by A19,A22,XREAL_0:def 2
.=1+(len f - Index(p,f));
then
A48: len g -'1=len g -1 by A18,XREAL_0:def 2;
then
A49: len g -'1 in dom (mid(f,Index(p,f)+1,len f)) by A18,A22,A47,A20,
FINSEQ_3:25;
A50: len f - Index(p,f)>=0 by A2,Th8,XREAL_1:50;
then
A51: len f -Index(p,f)=len f -' Index(p,f) by XREAL_0:def 2;
then
A52: mid(f,Index(p,f)+1,len f).(len f -' Index(p,f)) =f.(len f -' Index(p,f)
+(Index(p,f)+1)-'1) by A7,A18,A17,A21,A22,A20,FINSEQ_6:118;
A53: len g -'1= len f -' Index(p,f) by A47,A48,XREAL_0:def 2;
for x1,x2 being object st x1 in dom g & x2 in dom g & g.x1=g.x2 holds x1= x2
proof
let x1,x2 be object;
assume that
A54: x1 in dom g and
A55: x2 in dom g and
A56: g.x1=g.x2;
reconsider n1=x1,n2=x2 as Element of NAT by A54,A55;
A57: n1<=len g by A54,FINSEQ_3:25;
A58: 1<=n2 by A55,FINSEQ_3:25;
A59: n2<=len g by A55,FINSEQ_3:25;
A60: 1<=n1 by A54,FINSEQ_3:25;
now
per cases by A60,A58,XXREAL_0:1;
case
n1=1 & n2=1;
hence thesis;
end;
case that
A61: n1=1 and
A62: n2>1;
A63: n2-1<=1+len mid(f,Index(p,f)+1,len f)-1 by A5,A59,XREAL_1:9;
n1<=len <*p*> by A61,FINSEQ_1:39;
then n1 in dom <*p*> by A61,FINSEQ_3:25;
then
A64: g.n1=<*p*>.n1 by A4,FINSEQ_1:def 7;
n2-1>0 by A62,XREAL_1:50;
then
A65: n2-'1=n2-1 by XREAL_0:def 2;
then
A66: len <*p*>+(n2-'1)=1+(n2-1) by FINSEQ_1:39
.=n2;
A67: 1<=n2-'1 by A62,A65,SPPOL_1:1;
then n2-'1 in dom mid(f,Index(p,f)+1,len f) by A65,A63,FINSEQ_3:25;
then g.n2 =mid(f,Index(p,f)+1,len f).(n2-'1) by A4,A66,FINSEQ_1:def 7
.=f.(n2-'1+(Index(p,f)+1)-'1) by A7,A17,A21,A65,A63,A67,FINSEQ_6:118
.=f.(n2+Index(p,f)-'1) by A65;
then
A68: f.(n2+Index(p,f)-'1)=p by A56,A61,A64;
n2 -' 1 <= len f - Index(p,f) by A47,A48,A59,NAT_D:42;
then n2-1 <= len f - Index(p,f) by A62,XREAL_1:233;
then
A69: n2-1+Index(p,f) <= len f - Index(p,f)+ Index(p,f) by XREAL_1:6;
1 + 1 < n2+Index(p,f) by A2,A62,Th8,XREAL_1:8;
then
A70: 1< n2+Index(p,f)-1 by XREAL_1:20;
then n2+Index(p,f)-'1 = n2+Index(p,f)-1 by XREAL_0:def 2;
hence contradiction by A1,A3,A70,A68,A69,Th12;
end;
case that
A71: n1>1 and
A72: n2=1;
A73: n1-1<=1+len mid(f,Index(p,f)+1,len f)-1 by A5,A57,XREAL_1:9;
n2<=len <*p*> by A72,FINSEQ_1:39;
then n2 in dom <*p*> by A72,FINSEQ_3:25;
then
A74: g.n2=<*p*>.n2 by A4,FINSEQ_1:def 7;
n1-1>0 by A71,XREAL_1:50;
then
A75: n1-'1=n1-1 by XREAL_0:def 2;
then
A76: len <*p*>+(n1-'1)=1+(n1-1) by FINSEQ_1:39
.=n1;
A77: 1<=n1-'1 by A71,A75,SPPOL_1:1;
then n1-'1 in dom mid(f,Index(p,f)+1,len f) by A75,A73,FINSEQ_3:25;
then g.n1 =mid(f,Index(p,f)+1,len f).(n1-'1) by A4,A76,FINSEQ_1:def 7
.=f.(n1-'1+(Index(p,f)+1)-'1) by A7,A17,A21,A75,A73,A77,FINSEQ_6:118
.=f.(n1+Index(p,f)-'1) by A75;
then
A78: f.(n1+Index(p,f)-'1)=p by A56,A72,A74;
n1 -' 1 <= len f - Index(p,f) by A47,A48,A57,NAT_D:42;
then n1-1 <= len f - Index(p,f) by A71,XREAL_1:233;
then
A79: n1-1+Index(p,f) <= len f - Index(p,f)+ Index(p,f) by XREAL_1:6;
1 + 1 < n1+Index(p,f) by A2,A71,Th8,XREAL_1:8;
then
A80: 1< n1+Index(p,f)-1 by XREAL_1:20;
then n1+Index(p,f)-'1 = n1+Index(p,f)-1 by XREAL_0:def 2;
hence contradiction by A1,A3,A80,A78,A79,Th12;
end;
case that
A81: n1>1 and
A82: n2>1;
A83: n2-1>0 by A82,XREAL_1:50;
then
A84: n2-'1=n2-1 by XREAL_0:def 2;
then
A85: len <*p*>+(n2-'1)=1+(n2-1) by FINSEQ_1:39
.=n2;
A86: n1-1>0 by A81,XREAL_1:50;
then
A87: n1-'1=n1-1 by XREAL_0:def 2;
then
A88: 0+1<=n1-'1 by A86,NAT_1:13;
then
A89: 1<=n1-1+Index(p,f) by A87,NAT_1:12;
then
A90: n1+Index(p,f)-'1 = n1+Index(p,f)-1 by XREAL_0:def 2;
A91: len <*p*>+(n1-'1)=1+(n1-1) by A87,FINSEQ_1:39
.=n1;
A92: n1-1<=1+len mid(f,Index(p,f)+1,len f)-1 by A5,A57,XREAL_1:9;
then n1-'1 in dom mid(f,Index(p,f)+1,len f) by A87,A88,FINSEQ_3:25;
then
A93: g.n1 =mid(f,Index(p,f)+1,len f).(n1-'1) by A4,A91,FINSEQ_1:def 7
.=f.(n1-'1+(Index(p,f)+1)-'1) by A7,A17,A21,A87,A88,A92,FINSEQ_6:118
.=f.(n1+Index(p,f)-'1) by A87;
n1-'1 <= len f -' Index(p,f) by A53,A57,NAT_D:42;
then n1-'1+Index(p,f)<=len f - Index(p,f)+ Index(p,f) by A51,XREAL_1:6;
then
A94: n1+Index(p,f)-'1 in dom f by A87,A89,A90,FINSEQ_3:25;
A95: 0+1<=n2-'1 by A83,A84,NAT_1:13;
then
A96: 1<=n2-'1 + Index(p,f) by NAT_1:12;
then
A97: n2+Index(p,f)-'1 = n2+Index(p,f)-1 by A84,XREAL_0:def 2;
A98: n2-1<=1+len mid(f,Index(p,f)+1,len f)-1 by A5,A59,XREAL_1:9;
then n2-'1 in dom mid(f,Index(p,f)+1,len f) by A84,A95,FINSEQ_3:25;
then
A99: g.n2 =mid(f,Index(p,f)+1,len f).(n2-'1) by A4,A85,FINSEQ_1:def 7
.=f.(n2-'1+(Index(p,f)+1)-'1) by A7,A17,A21,A84,A95,A98,FINSEQ_6:118
.=f.(n2+Index(p,f)-'1) by A84;
n2-'1 <= len f -' Index(p,f) by A53,A59,NAT_D:42;
then n2-'1+Index(p,f)<=len f - Index(p,f)+ Index(p,f) by A51,XREAL_1:6;
then n2+Index(p,f)-'1 in dom f by A84,A96,A97,FINSEQ_3:25;
then n1+Index(p,f)-'1=n2+Index(p,f)-'1 by A1,A56,A99,A93,A94,
FUNCT_1:def 4;
hence thesis by A97,A90;
end;
end;
hence thesis;
end;
then
A100: g is one-to-one by FUNCT_1:def 4;
A101: len g -1+1>=1+1 by A18,A47,XREAL_1:6;
A102: len f -'(Index(p,f)+1)+1=len f -Index(p,f) by A20;
for j be Nat st 1 <= j & j+1 <= len g holds (g/.j)`1 = (g/.(j+1))`1 or
(g/.j)`2 = (g/.(j+1))`2
proof
1<=Index(p,f) by A2,Th8;
then
A103: 1<Index(p,f)+1 by NAT_1:13;
let j be Nat;
assume that
A104: 1 <= j and
A105: j+1 <= len g;
A106: LSeg(g,j) = LSeg(g/.j,g/.(j+1)) by A104,A105,TOPREAL1:def 3;
j+1-1<=1+len mid(f,Index(p,f)+1,len f)-1 by A5,A105,XREAL_1:9;
then j+1-1<= len f -Index(p,f) by A7,A17,A21,A102,FINSEQ_6:118;
then
A107: j+Index(p,f)<= len f -Index(p,f)+Index(p,f) by XREAL_1:6;
Index(p,f)+1<=Index(p,f)+j by A104,XREAL_1:6;
then 1<Index(p,f)+j by A103,XXREAL_0:2;
then
A108: 1<=Index(p,f)+j-1 by SPPOL_1:1;
then
A109: Index(p,f)+j-1=Index(p,f)+j-'1 by XREAL_0:def 2;
then
A110: LSeg(f,Index(p,f)+j-'1) = LSeg(f/.(Index(p,f)+j-'1),f/.(Index(p,f)+j
-'1+1)) by A108,A107,TOPREAL1:def 3;
A111: (f/.(Index(p,f)+j-'1))`1 = (f/.(Index(p,f)+j-'1+1))`1 or (f/.(Index(
p,f)+j-'1))`2 = (f/.(Index(p,f)+j-'1+1))`2 by A1,A108,A109,A107,TOPREAL1:def 5;
LSeg(g,j) c= LSeg(f,Index(p,f)+j-'1) by A2,A4,A104,A105,Th16;
hence thesis by A106,A110,A111,Th3;
end;
then g is unfolded s.n.c. special by A23,A8,TOPREAL1:def 5,def 6,def 7;
then
A112: g is being_S-Seq by A101,A100,TOPREAL1:def 8;
A113: len f -' Index(p,f)+(Index(p,f)+1) =len f - Index(p,f)+(Index(p,f)+1)
by A50,XREAL_0:def 2
.= len f +1;
1+(len g -'1)=1+(len g -1) by A46,XREAL_0:def 2
.=len g;
then g.len g =g.(len <*p*> + (len g -'1)) by FINSEQ_1:39
.=mid(f,Index(p,f)+1,len f).(len g -'1) by A4,A49,FINSEQ_1:def 7;
then g.len g=f.len f by A47,A48,A52,A113,NAT_D:34;
then
A114: g.len g = f/.len f by A7,FINSEQ_4:15;
g.1 = p by A4,FINSEQ_1:41;
hence thesis by A112,A114;
end;
theorem Th18:
for f,g being FinSequence of TOP-REAL 2, p being Point of
TOP-REAL 2,j be Nat st p in L~f & 1<=j & j+1<=len g & g=mid(f,1,Index(p,f))^<*p
*> holds LSeg(g,j) c= LSeg(f,j)
proof
let f,g be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2,j be Nat;
assume that
A1: p in L~f and
A2: 1<=j and
A3: j+1<=len g and
A4: g=mid(f,1,Index(p,f))^<*p*>;
A5: Index(p,f) < len f by A1,Th8;
A6: 1<=j+1 by NAT_1:11;
A7: 1<=Index(p,f) by A1,Th8;
1<=Index(p,f) by A1,Th8;
then
A8: 1<=len f by A5,XXREAL_0:2;
j<=j+1 by NAT_1:11;
then
A9: j<=len g by A3,XXREAL_0:2;
now
len g=len mid(f,1,Index(p,f)) + len <*p*> by A4,FINSEQ_1:22
.=len mid(f,1,Index(p,f))+1 by FINSEQ_1:39;
then len g=Index(p,f)-'1+1+1 by A5,A8,A7,FINSEQ_6:118;
then
A10: len g=Index(p,f)+1 by A1,Th8,XREAL_1:235;
then
A11: j<=Index(p,f) by A3,XREAL_1:6;
Index(p,f)+1<=len f +1 by A5,XREAL_1:6;
then j+1<=len f +1 by A3,A10,XXREAL_0:2;
then
A12: j+1-1<=len f +1-1 by XREAL_1:9;
A13: len mid(f,1,Index(p,f))=Index(p,f)-'1+1 by A5,A8,A7,FINSEQ_6:118
.=Index(p,f) by A1,Th8,XREAL_1:235;
then
A14: j in dom mid(f,1,Index(p,f)) by A2,A11,FINSEQ_3:25;
A15: g/.j=g.j by A2,A9,FINSEQ_4:15
.=mid(f,1,Index(p,f)).j by A4,A14,FINSEQ_1:def 7
.=f.(j+1-'1) by A2,A5,A8,A7,A11,A13,FINSEQ_6:118
.=f.j by NAT_D:34
.=f/.j by A2,A12,FINSEQ_4:15;
now
per cases;
case
A16: j+1<=Index(p,f);
A17: len mid(f,1,Index(p,f))=Index(p,f)-'1+1 by A5,A8,A7,FINSEQ_6:118
.=Index(p,f) by A1,Th8,XREAL_1:235;
then
A18: j+1 in dom mid(f,1,Index(p,f)) by A6,A16,FINSEQ_3:25;
A19: LSeg(g,j)=LSeg(g/.j,g/.(j+1)) by A2,A3,TOPREAL1:def 3;
A20: j+1<=len f by A5,A16,XXREAL_0:2;
g/.(j+1)=g.(j+1) by A3,FINSEQ_4:15,NAT_1:11
.= mid(f,1,Index(p,f)).(j+1) by A4,A18,FINSEQ_1:def 7
.=f.(j+1+1-'1) by A5,A8,A7,A6,A16,A17,FINSEQ_6:118
.=f.(j+1) by NAT_D:34
.=f/.(j+1) by A20,FINSEQ_4:15,NAT_1:11;
hence thesis by A2,A15,A20,A19,TOPREAL1:def 3;
end;
case
j+1>Index(p,f);
then j>=Index(p,f) by NAT_1:13;
then
A21: j=Index(p,f) by A11,XXREAL_0:1;
then
A22: p in LSeg(f,j) by A1,Th9;
j+1 <= len f by A1,A21,Th8,NAT_1:13;
then
A23: LSeg(f,j)=LSeg(f/.j,f/.(j+1)) by A2,TOPREAL1:def 3;
1<=len <*p*> by FINSEQ_1:40;
then
A24: 1 in dom <*p*> by FINSEQ_3:25;
A25: len mid(f,1,Index(p,f))=Index(p,f)-'1+1 by A5,A8,A7,FINSEQ_6:118
.=Index(p,f) by A1,Th8,XREAL_1:235;
A26: f/.j in LSeg(f/.j,f/.(j+1)) by RLTOPSP1:68;
g/.(j+1)=g.(j+1) by A3,FINSEQ_4:15,NAT_1:11
.=<*p*>.1 by A4,A21,A24,A25,FINSEQ_1:def 7
.=p;
then LSeg(g/.j,g/.(j+1)) c= LSeg(f/.j,f/.(j+1)) by A15,A26,A22,A23,
TOPREAL1:6;
hence thesis by A2,A3,A23,TOPREAL1:def 3;
end;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th19:
for f,g being FinSequence of TOP-REAL 2, p being Point of
TOP-REAL 2 st f is being_S-Seq & p in L~f & p<>f.1 & g=mid(f,1,Index(p,f))^<*p
*> holds g is_S-Seq_joining f/.1,p
proof
let f,g be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume that
A1: f is being_S-Seq and
A2: p in L~f and
A3: p<>f.1 and
A4: g=mid(f,1,Index(p,f))^<*p*>;
A5: Index(p,f)<=len f by A2,Th8;
A6: for j1,j2 be Nat st j1+1 < j2 holds LSeg(g,j1) misses LSeg(g,j2)
proof
let j1,j2 be Nat;
assume
A7: j1+1 < j2;
A8: j1=0 or j1>=0+1 by NAT_1:13;
now
per cases by A8,XXREAL_0:1;
case
j1=0;
then LSeg(g,j1)={} by TOPREAL1:def 3;
then LSeg(g,j1) /\ LSeg(g,j2) = {};
hence thesis by XBOOLE_0:def 7;
end;
case that
A9: j1=1 or j1>1 and
A10: j2+1<=len g;
j2<len g by A10,NAT_1:13;
then j1+1<len g by A7,XXREAL_0:2;
then
A11: LSeg(g,j1) c= LSeg(f,j1) by A2,A4,A9,Th18;
1+1<=j1+1 by A9,XREAL_1:6;
then 2<=j2 by A7,XXREAL_0:2;
then 1<=j2 by XXREAL_0:2;
then
A12: LSeg(g,j2) c= LSeg(f,j2) by A2,A4,A10,Th18;
LSeg(f,j1) misses LSeg(f,j2) by A1,A7,TOPREAL1:def 7;
then LSeg(f,j1) /\ LSeg(f,j2) = {} by XBOOLE_0:def 7;
then LSeg(g,j1) /\ LSeg(g,j2) = {} by A11,A12,XBOOLE_1:3,27;
hence thesis by XBOOLE_0:def 7;
end;
case
j2+1>len g;
then LSeg(g,j2)={} by TOPREAL1:def 3;
then LSeg(g,j1)/\ LSeg(g,j2)={};
hence thesis by XBOOLE_0:def 7;
end;
end;
hence thesis;
end;
A13: for n1,n2 being Element of NAT st 1<=n1 & n1<=len f & 1<=n2 & n2<=len f
& f.n1=f.n2 holds n1=n2
proof
let n1,n2 be Element of NAT;
assume that
A14: 1<=n1 and
A15: n1<=len f and
A16: 1<=n2 and
A17: n2<=len f and
A18: f.n1=f.n2;
A19: n2 in dom f by A16,A17,FINSEQ_3:25;
n1 in dom f by A14,A15,FINSEQ_3:25;
hence thesis by A1,A18,A19,FUNCT_1:def 4;
end;
A20: len g = len mid(f,1,Index(p,f))+ len<*p*> by A4,FINSEQ_1:22
.= len mid(f,1,Index(p,f))+ 1 by FINSEQ_1:39;
consider i such that
1<=i and
A21: i+1<=len f and
p in LSeg(f,i) by A2,SPPOL_2:13;
A22: 1<=Index(p,f) by A2,Th8;
1<=1+i by NAT_1:12;
then
A23: 1<=len f by A21,XXREAL_0:2;
then
A24: len mid(f,1,Index(p,f))=Index(p,f)-'1+1 by A22,A5,FINSEQ_6:118;
then
A25: len mid(f,1,Index(p,f))=Index(p,f) by A2,Th8,XREAL_1:235;
then g.1=mid(f,1,Index(p,f)).1 by A4,A22,FINSEQ_6:109;
then g.1=f.1 by A22,A5,A23,FINSEQ_6:118;
then
A26: g.1=f/.1 by A23,FINSEQ_4:15;
A27: for j be Nat st 1 <= j & j + 2 <= len g holds LSeg(g,j) /\ LSeg(g,j+1)
= {g/.(j+1)}
proof
let j be Nat;
assume that
A28: 1 <= j and
A29: j + 2 <= len g;
A30: j+1<=len g by A29,NAT_D:47;
then LSeg(g,j)=LSeg(g/.j,g/.(j+1)) by A28,TOPREAL1:def 3;
then
A31: g/.(j+1) in LSeg(g,j) by RLTOPSP1:68;
A32: 1<=j+1 by A28,NAT_D:48;
then LSeg(g,j+1)=LSeg(g/.(j+1),g/.(j+1+1)) by A29,TOPREAL1:def 3;
then g/.(j+1) in LSeg(g,j+1) by RLTOPSP1:68;
then g/.(j+1) in LSeg(g,j) /\ LSeg(g,j+1) by A31,XBOOLE_0:def 4;
then
A33: {g/.(j+1)} c= LSeg(g,j) /\ LSeg(g,j+1) by ZFMISC_1:31;
j+1<=len g by A29,NAT_D:47;
then
A34: LSeg(g,j) c= LSeg(f,j) by A2,A4,A28,Th18;
A35: Index(p,f)<=len f by A2,Th8;
A36: j+1+1<=len g by A29;
then LSeg(g,j+1) c= LSeg(f,j+1) by A2,A4,A32,Th18;
then
A37: LSeg(g,j)/\ LSeg(g,j+1) c= LSeg(f,j)/\ LSeg(f,j+1) by A34,XBOOLE_1:27;
A38: g/.(j+1)=g.(j+1) by A32,A30,FINSEQ_4:15;
now
A39: len g=len mid(f,1,Index(p,f))+1 by A4,FINSEQ_2:16;
Index(p,f)<=len f by A2,Th8;
then
A40: len g<=len f +1 by A25,A39,XREAL_1:6;
now
per cases by A40,XXREAL_0:1;
case
len g=len f +1;
hence contradiction by A2,A25,A39,Th8;
end;
case
len g<len f+1;
then len g<=len f by NAT_1:13;
then j+2<=len f by A29,XXREAL_0:2;
then
A41: LSeg(g,j)/\ LSeg(g,j+1) c= {f/.(j+1)} by A1,A28,A37,TOPREAL1:def 6;
A42: j+1<=Index(p,f) by A25,A36,A39,XREAL_1:6;
then j+1<=len f by A35,XXREAL_0:2;
then
A43: f.(j+1)=f/.(j+1) by A32,FINSEQ_4:15;
g.(j+1)=mid(f,1,Index(p,f)).(j+1) by A4,A25,A32,A42,FINSEQ_1:64
.=f.(j+1) by A5,A32,A42,FINSEQ_6:123;
hence thesis by A38,A33,A41,A43,XBOOLE_0:def 10;
end;
end;
hence thesis;
end;
hence thesis;
end;
for j be Nat st 1 <= j & j+1 <= len g holds (g/.j)`1 = (g/.(j+1))`1 or
(g/.j)`2 = (g/.(j+1))`2
proof
A44: Index(p,f)<len f by A2,Th8;
let j be Nat;
assume that
A45: 1 <= j and
A46: j+1 <= len g;
A47: LSeg(g,j) = LSeg(g/.j,g/.(j+1)) by A45,A46,TOPREAL1:def 3;
j+1<=Index(p,f)+1 by A4,A25,A46,FINSEQ_2:16;
then j<=Index(p,f) by XREAL_1:6;
then j<len f by A44,XXREAL_0:2;
then
A48: j+1<=len f by NAT_1:13;
then
A49: LSeg(f,j) = LSeg(f/.j,f/.(j+1)) by A45,TOPREAL1:def 3;
A50: (f/.j)`1 = (f/.(j+1))`1 or (f/.j)`2 = (f/.(j+1))`2 by A1,A45,A48,
TOPREAL1:def 5;
LSeg(g,j) c= LSeg(f,j) by A2,A4,A45,A46,Th18;
hence thesis by A47,A49,A50,Th3;
end;
then
A51: g is unfolded s.n.c. special by A27,A6,TOPREAL1:def 5,def 6,def 7;
1<=len <*p*> by FINSEQ_1:39;
then
A52: 1 in dom <*p*> by FINSEQ_3:25;
for x1,x2 being object st x1 in dom g & x2 in dom g & g.x1=g.x2 holds x1= x2
proof
let x1,x2 be object;
assume that
A53: x1 in dom g and
A54: x2 in dom g and
A55: g.x1=g.x2;
reconsider n1=x1,n2=x2 as Element of NAT by A53,A54;
A56: 1<=n1 by A53,FINSEQ_3:25;
A57: n2<=len g by A54,FINSEQ_3:25;
A58: 1<=n2 by A54,FINSEQ_3:25;
A59: n1<=len g by A53,FINSEQ_3:25;
now
A60: g.len g =<*p*>.1 by A4,A52,A20,FINSEQ_1:def 7
.=p;
now
per cases;
case
A61: n1=len g;
now
assume
A62: n2<>len g;
then n2<len g by A57,XXREAL_0:1;
then
A63: n2<=len mid(f,1,Index(p,f)) by A20,NAT_1:13;
then
A64: n2 <= len f by A5,A25,XXREAL_0:2;
g.n2=mid(f,1,Index(p,f)).n2 by A4,A58,A63,FINSEQ_1:64;
then g.n2=f.(n2+1-'1) by A22,A5,A23,A58,A63,FINSEQ_6:118;
then
A65: p=f.n2 by A55,A60,A61,NAT_D:34;
then 1 < n2 by A3,A58,XXREAL_0:1;
then Index(p,f)+1 = n2 by A1,A65,A64,Th12;
hence contradiction by A2,A24,A20,A62,Th8,XREAL_1:235;
end;
hence thesis by A61;
end;
case
A66: n2=len g;
now
assume
A67: n1<>len g;
then n1<len g by A59,XXREAL_0:1;
then
A68: n1<=len mid(f,1,Index(p,f)) by A20,NAT_1:13;
then
A69: n1 <= len f by A5,A25,XXREAL_0:2;
g.n1=mid(f,1,Index(p,f)).n1 by A4,A56,A68,FINSEQ_1:64;
then g.n1=f.(n1+1-'1) by A22,A5,A23,A56,A68,FINSEQ_6:118;
then
A70: p=f.n1 by A55,A60,A66,NAT_D:34;
then 1 < n1 by A3,A56,XXREAL_0:1;
then Index(p,f)+1 = n1 by A1,A70,A69,Th12;
hence contradiction by A2,A24,A20,A67,Th8,XREAL_1:235;
end;
hence thesis by A66;
end;
case that
A71: n1<>len g and
A72: n2 <> len g;
n1<len g by A59,A71,XXREAL_0:1;
then
A73: n1<=len mid(f,1,Index(p,f)) by A20,NAT_1:13;
then
A74: n1<=len f by A5,A25,XXREAL_0:2;
n2 < len g by A57,A72,XXREAL_0:1;
then
A75: n2<=len mid(f,1,Index(p,f)) by A20,NAT_1:13;
then
A76: g.n2=mid(f,1,Index(p,f)).n2 by A4,A58,FINSEQ_1:64
.=f.n2 by A5,A25,A58,A75,FINSEQ_6:123;
A77: n2<=len f by A5,A25,A75,XXREAL_0:2;
g.n1=mid(f,1,Index(p,f)).n1 by A4,A56,A73,FINSEQ_1:64
.=f.n1 by A5,A25,A56,A73,FINSEQ_6:123;
hence thesis by A13,A55,A56,A58,A74,A77,A76;
end;
end;
hence thesis;
end;
hence thesis;
end;
then
A78: g is one-to-one by FUNCT_1:def 4;
1+1<=len g by A22,A25,A20,XREAL_1:6;
then
A79: g is being_S-Seq by A78,A51,TOPREAL1:def 8;
g.len g = p by A4,A20,FINSEQ_1:42;
hence thesis by A26,A79;
end;
begin
::----------------------------------------------------------------------:
:: Left and Right Cutting Functions for Finite Sequences in TOP-REAL 2 :
::----------------------------------------------------------------------:
definition
let f be FinSequence of TOP-REAL 2,p be Point of TOP-REAL 2;
func L_Cut(f,p) -> FinSequence of TOP-REAL 2 equals
:Def3:
<*p*>^mid(f,Index
(p,f)+1,len f) if p<>f.(Index(p,f)+1) otherwise mid(f,Index(p,f)+1,len f);
correctness;
func R_Cut(f,p) -> FinSequence of TOP-REAL 2 equals
:Def4:
mid(f,1,Index(p,f
))^<*p*> if p<>f.1 otherwise <*p*>;
correctness;
end;
theorem Th20:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL
2 st f is being_S-Seq & p in L~f & p = f.(Index(p,f)+1) & p <> f.len f holds
Index(p,Rev f) + Index(p,f) + 1 = len f
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2 such that
A1: f is being_S-Seq and
A2: p in L~f and
A3: p = f.(Index(p,f)+1) and
A4: p <> f.len f;
A5: len f <= len f + Index(p,f) by NAT_1:11;
len f = len Rev f by FINSEQ_5:def 3;
then
A6: len f - Index(p,f) <= len Rev f by A5,XREAL_1:20;
Index(p,f) <= len f by A2,Th8;
then
A7: len f - Index(p,f) = len f -' Index(p,f) by XREAL_1:233;
Index(p,f) < len f by A2,Th8;
then
A8: Index(p,f)+1 <= len f by NAT_1:13;
then Index(p,f)+1 < len f by A3,A4,XXREAL_0:1;
then
A9: 1 < len f - Index(p,f) by XREAL_1:20;
1 <= Index(p,f)+1 by NAT_1:11;
then Index(p,f)+1 in dom f by A8,FINSEQ_3:25;
then
A10: Index(p,f)+1 in dom Rev f by FINSEQ_5:57;
p = (Rev Rev f).(Index(p,f)+1) by A3
.= (Rev f).(len Rev f - (Index(p,f)+1) + 1) by A10,FINSEQ_5:58
.= (Rev f).(len Rev f - Index(p,f))
.= (Rev f).(len f - Index(p,f)) by FINSEQ_5:def 3;
then Index(p,Rev f) + 1 = len f -' Index(p,f) by A1,A6,A9,A7,Th12;
hence thesis by A7;
end;
theorem Th21:
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
st f is unfolded s.n.c. & p in L~f & p <> f.(Index(p,f)+1) holds Index(p,Rev f)
+ Index(p,f) = len f
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2 such that
A1: f is unfolded s.n.c. and
A2: p in L~f and
A3: p <> f.(Index(p,f)+1);
A4: Index(p,f) < len f by A2,Th8;
then
A5: len f -' Index(p,f) + Index(p,f) = len f by XREAL_1:235;
0+1 <= Index(p,f) by A2,Th8;
then len f + 0 < len f + Index(p,f) by XREAL_1:6;
then len f - Index(p,f) < len f by XREAL_1:19;
then
A6: len f -' Index(p,f) < len f by A4,XREAL_1:233;
A7: Index(p,f) < len f by A2,Th8;
then Index(p,f) + 1 <= len f by NAT_1:13;
then 1<=len f - Index(p,f) by XREAL_1:19;
then 1<=len f -' Index(p,f) by NAT_D:39;
then len f -' Index(p,f) in dom f by A6,FINSEQ_3:25;
then
A8: (Rev f).(len f -' Index(p,f)) = f.(len f - (len f -' Index(p,f)) + 1)
by FINSEQ_5:58
.= f.(len f - (len f - Index(p,f)) + 1) by A7,XREAL_1:233
.= f.(0 + Index(p,f) + 1);
p in LSeg(f,Index(p,f)) by A2,Th9;
then
A9: p in LSeg(Rev f,len f -' Index(p,f)) by A5,SPPOL_2:2;
len f = len Rev f by FINSEQ_5:def 3;
then
A10: len f -' Index(p,f)+1<=len Rev f by A6,NAT_1:13;
Rev f is s.n.c. by A1,SPPOL_2:35;
then len f -' Index(p,f)=Index(p,Rev f) by A1,A3,A9,A10,A8,Th14,SPPOL_2:28;
hence thesis by A7,XREAL_1:235;
end;
theorem Th22:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL
2 st f is being_S-Seq & p in L~f holds L_Cut(Rev f,p) = Rev R_Cut(f,p)
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2 such that
A1: f is being_S-Seq and
A2: p in L~f;
A3: len f = len Rev f by FINSEQ_5:def 3;
A4: p in L~Rev f by A2,SPPOL_2:22;
A5: 1 <= Index(p,f) by A2,Th8;
A6: Rev f is being_S-Seq by A1;
A7: Rev Rev f = f;
A8: Index(p,f) < len f by A2,Th8;
L~f = L~Rev f by SPPOL_2:22;
then Index(p, Rev f) < len Rev f by A2,Th8;
then
A9: Index(p, Rev f) + 1 <= len f by A3,NAT_1:13;
1 <= Index(p, Rev f)+1 by NAT_1:11;
then
A10: Index(p, Rev f)+1 in dom f by A9,FINSEQ_3:25;
A11: 1+1 <= len f by A1,TOPREAL1:def 8;
then
A12: 1 < len f by NAT_1:13;
then
A13: 1 in dom f by FINSEQ_3:25;
A14: len f in dom f by A12,FINSEQ_3:25;
A15: 2 in dom f by A11,FINSEQ_3:25;
A16: dom Rev f = dom f by FINSEQ_5:57;
per cases;
suppose
A17: p = f.len f;
then
A18: p<>f.1 by A1,A12,A13,A14,FUNCT_1:def 4;
A19: p = (Rev f).1 by A17,FINSEQ_5:62;
then
A20: p <> (Rev f).(1+1) by A1,A16,A13,A15,FUNCT_1:def 4;
p = (Rev f)/.1 by A16,A13,A19,PARTFUN1:def 6;
then
A21: Index(p,Rev f) = 1 by A3,A11,Th11;
then Index(p,Rev f) + Index(p,f) = len f by A6,A4,A7,A3,A20,Th21;
then
A22: Index(p,Rev f) = len f - Index(p,f);
thus L_Cut(Rev f,p) = <*p*>^mid(Rev f,Index(p,Rev f)+1,len f) by A3,A21,A20
,Def3
.= <*p*>^mid(Rev f,len f -'Index(p,f)+1,len f) by A8,A22,XREAL_1:233
.= <*p*>^mid(Rev f,len f -'Index(p,f)+1,len f -' 1 + 1) by A12,
XREAL_1:235
.= <*p*>^Rev mid(f,1,Index(p,f)) by A12,A5,A8,FINSEQ_6:113
.= Rev(mid(f,1,Index(p,f))^<*p*>) by FINSEQ_5:63
.= Rev R_Cut(f,p) by A18,Def4;
end;
suppose
A23: p = f.1;
A24: len Rev f-'1+1=len Rev f by A3,A12,XREAL_1:235;
then
A25: (Rev f/^(len Rev f-'1)).1=Rev f.len Rev f by FINSEQ_6:114;
A26: len (Rev f/^(len Rev f-'1))=len Rev f-'(len Rev f-'1) by RFINSEQ:29;
1<=len Rev f-(len Rev f-'1) by A24;
then
A27: 1<=len (Rev f/^(len Rev f-'1)) by A26,NAT_D:39;
len Rev f-'len Rev f+1=len Rev f-len Rev f+1 by XREAL_1:233
.=1;
then
A28: mid(Rev f,len Rev f,len Rev f)=(Rev f/^(len Rev f-'1))|1 by FINSEQ_6:def 3
.=<*(Rev f/^(len Rev f-'1)).1 *> by A27,CARD_1:27,FINSEQ_5:20
.=<*Rev f.len Rev f*> by A25;
A29: p = (Rev f).len f by A23,FINSEQ_5:62;
then Index(p,Rev f) + 1 = len f by A1,A3,A12,Th12;
hence L_Cut(Rev f,p) = <*p*> by A3,A29,A28,Def3
.= Rev <*p*> by FINSEQ_5:60
.= Rev R_Cut(f,p) by A23,Def4;
end;
suppose that
A30: p <> f.1 and
A31: p <> f.len f and
A32: p = f.(Index(p,f)+1);
A33: len f = Index(p,Rev f) + Index(p,f) + 1 by A1,A2,A31,A32,Th20
.= Index(p,f) + (Index(p,Rev f) + 1);
len f = Index(p,Rev f) + Index(p,f) + 1 by A1,A2,A31,A32,Th20
.= Index(p,Rev f) + (Index(p,f) + 1);
then
A34: p = f.(len f - (Index(p, Rev f)+1) + 1) by A32
.= (Rev f).(Index(p, Rev f)+1) by A10,FINSEQ_5:58;
A35: len f -' Index(p,f) = len f - Index(p,f) by A8,XREAL_1:233
.= Index(p,Rev f)+1 by A33;
p <> (Rev f).len f by A30,FINSEQ_5:62;
then
A36: Index(p, Rev f)+1 < len f by A9,A34,XXREAL_0:1;
thus L_Cut(Rev f,p) = mid(Rev f,Index(p,Rev f)+1,len f) by A3,A34,Def3
.= <*p*>^mid(Rev f,len f -' Index(p,f)+1, len f) by A16,A10,A34,A35,A36,
FINSEQ_6:126
.= <*p*>^mid(Rev f,len f -' Index(p,f)+1, len f-'1+1) by A12,XREAL_1:235
.= <*p*>^Rev mid(f,1,Index(p,f)) by A12,A5,A8,FINSEQ_6:113
.= Rev (mid(f,1,Index(p,f))^<*p*>) by FINSEQ_5:63
.= Rev R_Cut(f,p) by A30,Def4;
end;
suppose that
A37: p <> f.1 and
A38: p <> f.(Index(p,f)+1);
A39: p <> (Rev f).len f by A37,FINSEQ_5:62;
A40: now
assume
A41: p = (Rev f).(Index(p, Rev f)+1);
then
A42: len Rev f = Index(p,Rev Rev f) + Index(p,Rev f) + 1 by A1,A4,A3,A39,Th20
.= Index(p,f) + 1 + Index(p,Rev f);
p = f.(len f - (Index(p, Rev f)+1) + 1) by A10,A41,FINSEQ_5:58
.= f.(Index(p,f)+1) by A3,A42;
hence contradiction by A38;
end;
A43: Index(p, f) < len f by A2,Th8;
len f = Index(p,Rev f) + Index(p,f) by A1,A2,A38,Th21;
then Index(p,Rev f) = len f - Index(p,f)
.= len f -' Index(p,f) by A43,XREAL_1:233;
hence
L_Cut(Rev f,p) = <*p*>^mid(Rev f,len f -' Index(p,f)+1, len f) by A3,A40
,Def3
.= <*p*>^mid(Rev f,len f -' Index(p,f)+1, len f-'1+1) by A12,XREAL_1:235
.= <*p*>^Rev mid(f,1,Index(p,f)) by A12,A5,A8,FINSEQ_6:113
.= Rev (mid(f,1,Index(p,f))^<*p*>) by FINSEQ_5:63
.= Rev R_Cut(f,p) by A37,Def4;
end;
end;
theorem Th23:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL
2 st p in L~f holds (L_Cut(f,p)).1=p & for i st 1<i & i<=len L_Cut(f,p) holds (
p = f.(Index(p,f)+1) implies (L_Cut(f,p)).i=f.(Index(p,f)+i)) & (p <> f.(Index(
p,f)+1) implies (L_Cut(f,p)).i=f.(Index(p,f)+i-1))
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume
A1: p in L~f;
then Index(p,f) < len f by Th8;
then
A2: Index(p,f)+1<=len f by NAT_1:13;
A3: f is non empty by A1,CARD_1:27,TOPREAL1:22;
now
per cases;
suppose
A4: p = f.(Index(p,f)+1);
1 in dom f by A3,FINSEQ_5:6;
then
A5: 1 <= len f by FINSEQ_3:25;
Index(p,f) < len f by A1,Th8;
then
A6: Index(p,f)+1 <= len f by NAT_1:13;
A7: 1 <= Index(p,f)+1 by NAT_1:11;
L_Cut(f,p)=mid(f,Index(p,f)+1,len f) by A4,Def3;
hence (L_Cut(f,p)).1 = p by A4,A7,A6,A5,FINSEQ_6:118;
end;
suppose
p<> f.(Index(p,f)+1);
then L_Cut(f,p)=<*p*>^mid(f,Index(p,f)+1,len f) by Def3;
hence (L_Cut(f,p)).1=p by FINSEQ_1:41;
end;
end;
hence (L_Cut(f,p)).1=p;
let i;
assume that
A8: 1<i and
A9: i<=len L_Cut(f,p);
A10: len <*p*><=i by A8,FINSEQ_1:40;
A11: 1<=Index(p,f)+1 by NAT_1:11;
then
A12: 1<=len f by A2,XXREAL_0:2;
then len mid(f,Index(p,f)+1,len f)=len f -'(Index(p,f)+1)+1 by A11,A2,
FINSEQ_6:118;
then
A13: len <*p*>+len mid(f,Index(p,f)+1,len f) =1+(len f -'(Index(p,f)+1)+1)
by FINSEQ_1:40
.=1+(len f -(Index(p,f)+1)+1) by A2,XREAL_1:233
.=(len f -Index(p,f))+1;
A14: (i-'1)+1=i-1+1 by A8,XREAL_1:233
.=i;
A15: 1<=i-1 by A8,SPPOL_1:1;
then
A16: 1<=i-'1 by NAT_D:39;
hereby
assume p = f.(Index(p,f)+1);
then L_Cut(f,p)=mid(f,Index(p,f)+1,len f) by Def3;
hence (L_Cut(f,p)).i = f.(i+(Index(p,f)+1)-'1) by A8,A9,A11,A2,A12,
FINSEQ_6:118
.= f.(i+Index(p,f)+1-'1)
.= f.(Index(p,f)+i) by NAT_D:34;
end;
A17: i <=i+Index(p,f) by NAT_1:11;
assume p <> f.(Index(p,f)+1);
then
A18: L_Cut(f,p)=<*p*>^mid(f,Index(p,f)+1,len f) by Def3;
then i<=len <*p*>+len mid(f,Index(p,f)+1,len f) by A9,FINSEQ_1:22;
then i-1<=len f -Index(p,f)+1-1 by A13,XREAL_1:9;
then
A19: i-'1<=len f -(Index(p,f)+1)+1 by A15,NAT_D:39;
len <*p*><i by A8,FINSEQ_1:39;
then (L_Cut(f,p)).i =mid(f,Index(p,f)+1,len f).(i-len <*p*>) by A9,A18,
FINSEQ_6:108
.=mid(f,Index(p,f)+1,len f).(i-'len <*p*>) by A10,XREAL_1:233
.=mid(f,Index(p,f)+1,len f).(i-'1) by FINSEQ_1:39
.=f.((i-'1)+(Index(p,f)+1)-'1) by A11,A2,A16,A19,FINSEQ_6:122
.=f.(Index(p,f)+i-'1) by A14;
hence thesis by A8,A17,XREAL_1:233,XXREAL_0:2;
end;
theorem Th24:
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
st p in L~f holds R_Cut(f,p).(len R_Cut(f,p)) = p & for i be Element of NAT st
1<=i & i<=Index(p,f) holds R_Cut(f,p).i = f.i
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume
A1: p in L~f;
then
A2: Index(p,f)<len f by Th8;
now
per cases;
suppose
A3: p<>f.1;
A4: len (mid(f,1,Index(p,f))^<*p*>)= len mid(f,1,Index(p,f))+len <*p*>
by FINSEQ_1:22
.= len mid(f,1,Index(p,f))+1 by FINSEQ_1:39;
R_Cut(f,p) = mid(f,1,Index(p,f))^<*p*> by A3,Def4;
hence (R_Cut(f,p)).(len R_Cut(f,p)) = p by A4,FINSEQ_1:42;
end;
suppose
p=f.1;
then
A5: R_Cut(f,p) = <*p*> by Def4;
then len R_Cut(f,p) = 1 by FINSEQ_1:40;
hence (R_Cut(f,p)).(len R_Cut(f,p)) = p by A5;
end;
end;
hence (R_Cut(f,p)).(len R_Cut(f,p)) = p;
A6: 1<=Index(p,f) by A1,Th8;
then len f > 1 by A2,XXREAL_0:2;
then
A7: len mid(f,1,Index(p,f))=Index(p,f)-'1+1 by A6,A2,FINSEQ_6:118
.= Index(p,f) by A1,Th8,XREAL_1:235;
thus for i be Element of NAT st 1<=i & i<=Index(p,f) holds R_Cut(f,p).i=f.i
proof
let i be Element of NAT;
assume that
A8: 1<=i and
A9: i<=Index(p,f);
now
per cases;
case
p<>f.1;
then (R_Cut(f,p)).i=(mid(f,1,Index(p,f))^<*p*>).i by Def4
.= mid(f,1,Index(p,f)).i by A7,A8,A9,FINSEQ_1:64
.=f.i by A2,A8,A9,FINSEQ_6:123;
hence thesis;
end;
case
A10: p=f.1;
A11: len f > 1 by A6,A2,XXREAL_0:2;
then 1 in dom f by FINSEQ_3:25;
then
A12: p = f/.1 by A10,PARTFUN1:def 6;
len f >= 1+1 by A11,NAT_1:13;
then Index(p,f) = 1 by A12,Th11;
then
A13: i = 1 by A8,A9,XXREAL_0:1;
R_Cut(f,p) = <*p*> by A10,Def4;
hence thesis by A10,A13;
end;
end;
hence thesis;
end;
end;
theorem
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st p
in L~f holds ( p<>f.1 implies len R_Cut(f,p)=Index(p,f)+1 ) & ( p=f.1 implies
len R_Cut(f,p)=Index(p,f) )
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume
A1: p in L~f;
then consider i be Nat such that
A2: 1 <= i and
A3: i+1 <= len f and
p in LSeg(f,i) by SPPOL_2:13;
A4: 1<=Index(p,f) by A1,Th8;
A5: Index(p,f)<=len f by A1,Th8;
i<=len f by A3,NAT_D:46;
then
A6: 1<=len f by A2,XXREAL_0:2;
now
per cases;
case
p<>f.1;
then R_Cut(f,p)=mid(f,1,Index(p,f))^<*p*> by Def4;
hence len R_Cut(f,p) = len mid(f,1,Index(p,f))+len <*p*> by FINSEQ_1:22
.= len mid(f,1,Index(p,f))+1 by FINSEQ_1:39
.= Index(p,f)-'1+1+1 by A6,A4,A5,FINSEQ_6:118
.= Index(p,f)+1 by A1,Th8,XREAL_1:235;
end;
case
A7: p=f.1;
len f > i by A3,NAT_1:13;
then len f > 1 by A2,XXREAL_0:2;
then
A8: len f >= 1+1 by NAT_1:13;
1 in dom f by A3,CARD_1:27,FINSEQ_5:6;
then
A9: p = f/.1 by A7,PARTFUN1:def 6;
R_Cut(f,p)=<*p*> by A7,Def4;
hence len R_Cut(f,p)= 1 by FINSEQ_1:39
.= Index(p,f) by A8,A9,Th11;
end;
end;
hence thesis;
end;
theorem Th26:
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
st p in L~f holds ( p=f.(Index(p,f)+1) implies len L_Cut(f,p) = len f-Index(p,f
) ) & ( p<>f.(Index(p,f)+1) implies len L_Cut(f,p) = len f-Index(p,f)+1 )
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume
A1: p in L~f;
then consider i be Nat such that
A2: 1 <= i and
A3: i+1 <= len f and
p in LSeg(f,i) by SPPOL_2:13;
i<=len f by A3,NAT_D:46;
then
A4: 1<=len f by A2,XXREAL_0:2;
1<=Index(p,f) by A1,Th8;
then
A5: 1<Index(p,f)+1 by NAT_1:13;
Index(p,f)<len f by A1,Th8;
then
A6: Index(p,f)+1+0<=len f by NAT_1:13;
then
A7: len f -(Index(p,f)+1) >= 0 by XREAL_1:19;
now
per cases;
case
p<>f.(Index(p,f)+1);
then L_Cut(f,p)=<*p*>^mid(f,Index(p,f)+1,len f) by Def3;
hence len L_Cut(f,p) = 1+len mid(f,Index(p,f)+1,len f) by FINSEQ_5:8
.= len f -'(Index(p,f)+1)+1+1 by A4,A5,A6,FINSEQ_6:118
.= len f -(Index(p,f)+1)+1+1 by A7,XREAL_0:def 2
.= len f-Index(p,f)+1;
end;
case
p=f.(Index(p,f)+1);
then L_Cut(f,p)=mid(f,Index(p,f)+1,len f) by Def3;
hence len L_Cut(f,p) = len f -' (Index(p,f)+1) + 1
by A4,A5,A6,FINSEQ_6:118
.= len f -(Index(p,f)+1)+1 by A7,XREAL_0:def 2
.= len f-Index(p,f);
end;
end;
hence thesis;
end;
definition
let p1,p2,q1,q2 be Point of TOP-REAL 2;
pred LE q1,q2,p1,p2 means
q1 in LSeg(p1,p2) & q2 in LSeg(p1,p2) & for
r1,r2 being Real
st 0<=r1 & r1<=1 & q1=(1-r1)*p1+r1*p2 & 0<=r2 & r2<=1 & q2=(1-
r2)*p1+r2*p2 holds r1<=r2;
end;
definition
let p1,p2,q1,q2 be Point of TOP-REAL 2;
pred LT q1,q2,p1,p2 means
LE q1,q2,p1,p2 & q1<>q2;
end;
theorem
for p1,p2,q1,q2 being Point of TOP-REAL 2 st LE q1,q2,p1,p2 & LE q2,q1
,p1,p2 holds q1=q2
proof
let p1,p2,q1,q2 be Point of TOP-REAL 2;
assume that
A1: LE q1,q2,p1,p2 and
A2: LE q2,q1,p1,p2;
q1 in LSeg(p1,p2) by A1;
then consider r1 such that
A3: q1 = (1-r1)*p1+r1*p2 and
A4: 0<=r1 and
A5: r1<=1;
q2 in LSeg(p1,p2) by A1;
then consider r2 such that
A6: q2 = (1-r2)*p1+r2*p2 and
A7: 0<=r2 and
A8: r2<=1;
A9: r2<=r1 by A2,A3,A4,A5,A6,A8;
r1<=r2 by A1,A3,A5,A6,A7,A8;
then r1=r2 by A9,XXREAL_0:1;
hence thesis by A3,A6;
end;
theorem Th28:
for p1,p2,q1,q2 being Point of TOP-REAL 2 st q1 in LSeg(p1,p2) &
q2 in LSeg(p1,p2) & p1<>p2 holds (LE q1,q2,p1,p2 or LT q2,q1,p1,p2) & not(LE q1
,q2,p1,p2 & LT q2,q1,p1,p2)
proof
let p1,p2,q1,q2 be Point of TOP-REAL 2;
assume that
A1: q1 in LSeg(p1,p2) and
A2: q2 in LSeg(p1,p2) and
A3: p1<>p2;
consider r1 such that
A4: q1= (1-r1)*p1 + r1*p2 and
A5: 0 <= r1 and
A6: r1 <= 1 by A1;
consider r2 such that
A7: q2= (1-r2)*p1 + r2*p2 and
A8: 0 <= r2 and
A9: r2 <= 1 by A2;
A10: now
per cases;
case
A11: r1<=r2;
for s1,s2 being Real
st 0<=s1 & s1<=1 & q1=(1-s1)*p1+s1*p2 & 0<=s2
& s2<=1 & q2=(1-s2)*p1+s2*p2 holds s1<=s2
proof
let s1,s2 be Real;
assume that
0<=s1 and
s1<=1 and
A12: q1=(1-s1)*p1+s1*p2 and
0<=s2 and
s2<=1 and
A13: q2=(1-s2)*p1+s2*p2;
(1-s2)*p1+(s2*p2-s2*p2)=(1-r2)*p1+r2*p2-s2*p2 by A7,A13,RLVECT_1:def 3;
then (1-s2)*p1+(s2*p2-s2*p2)=(1-r2)*p1+(r2*p2-s2*p2) by RLVECT_1:def 3;
then (1-s2)*p1+(0.TOP-REAL 2)=(1-r2)*p1+(r2*p2-s2*p2) by RLVECT_1:5;
then (1-s2)*p1=(1-r2)*p1+(r2*p2-s2*p2) by RLVECT_1:4;
then (1-s2)*p1=(1-r2)*p1+(r2-s2)*p2 by RLVECT_1:35;
then (1-s2)*p1-(1-r2)*p1=(r2-s2)*p2+((1-r2)*p1-(1-r2)*p1) by
RLVECT_1:def 3;
then (1-s2)*p1-(1-r2)*p1=(r2-s2)*p2+(0.TOP-REAL 2) by RLVECT_1:5;
then (1-s2)*p1-(1-r2)*p1=(r2-s2)*p2 by RLVECT_1:4;
then ((1-s2)-(1-r2))*p1=(r2-s2)*p2 by RLVECT_1:35;
then
A14: (r2-s2)=0 or p1=p2 by RLVECT_1:36;
(1-s1)*p1+(s1*p2-s1*p2)=(1-r1)*p1+r1*p2-s1*p2 by A4,A12,RLVECT_1:def 3;
then (1-s1)*p1+(s1*p2-s1*p2)=(1-r1)*p1+(r1*p2-s1*p2) by RLVECT_1:def 3;
then (1-s1)*p1+(0.TOP-REAL 2)=(1-r1)*p1+(r1*p2-s1*p2) by RLVECT_1:5;
then (1-s1)*p1=(1-r1)*p1+(r1*p2-s1*p2) by RLVECT_1:4;
then (1-s1)*p1=(1-r1)*p1+(r1-s1)*p2 by RLVECT_1:35;
then (1-s1)*p1-(1-r1)*p1=(r1-s1)*p2+((1-r1)*p1-(1-r1)*p1) by
RLVECT_1:def 3;
then (1-s1)*p1-(1-r1)*p1=(r1-s1)*p2+(0.TOP-REAL 2) by RLVECT_1:5;
then (1-s1)*p1-(1-r1)*p1=(r1-s1)*p2 by RLVECT_1:4;
then ((1-s1)-(1-r1))*p1=(r1-s1)*p2 by RLVECT_1:35;
then (r1-s1)=0 or p1=p2 by RLVECT_1:36;
hence thesis by A3,A11,A14;
end;
hence LE q1,q2,p1,p2 or LT q2,q1,p1,p2 by A1,A2;
end;
case
A15: r1>r2;
for s2,s1 being Real
st 0<=s2 & s2<=1 & q2=(1-s2)*p1+s2*p2 & 0<=s1
& s1<=1 & q1=(1-s1)*p1+s1*p2 holds s1>=s2
proof
let s2,s1 be Real;
assume that
0<=s2 and
s2<=1 and
A16: q2=(1-s2)*p1+s2*p2 and
0<=s1 and
s1<=1 and
A17: q1=(1-s1)*p1+s1*p2;
(1-s1)*p1+(s1*p2-s1*p2)=(1-r1)*p1+r1*p2-s1*p2 by A4,A17,RLVECT_1:def 3;
then (1-s1)*p1+(s1*p2-s1*p2)=(1-r1)*p1+(r1*p2-s1*p2) by RLVECT_1:def 3;
then (1-s1)*p1+(0.TOP-REAL 2)=(1-r1)*p1+(r1*p2-s1*p2) by RLVECT_1:5;
then (1-s1)*p1=(1-r1)*p1+(r1*p2-s1*p2) by RLVECT_1:4;
then (1-s1)*p1=(1-r1)*p1+(r1-s1)*p2 by RLVECT_1:35;
then (1-s1)*p1-(1-r1)*p1=(r1-s1)*p2+((1-r1)*p1-(1-r1)*p1) by
RLVECT_1:def 3;
then (1-s1)*p1-(1-r1)*p1=(r1-s1)*p2+(0.TOP-REAL 2) by RLVECT_1:5;
then (1-s1)*p1-(1-r1)*p1=(r1-s1)*p2 by RLVECT_1:4;
then ((1-s1)-(1-r1))*p1=(r1-s1)*p2 by RLVECT_1:35;
then
A18: (r1-s1)=0 or p1=p2 by RLVECT_1:36;
(1-s2)*p1+(s2*p2-s2*p2)=(1-r2)*p1+r2*p2-s2*p2 by A7,A16,RLVECT_1:def 3;
then (1-s2)*p1+(s2*p2-s2*p2)=(1-r2)*p1+(r2*p2-s2*p2) by RLVECT_1:def 3;
then (1-s2)*p1+(0.TOP-REAL 2)=(1-r2)*p1+(r2*p2-s2*p2) by RLVECT_1:5;
then (1-s2)*p1=(1-r2)*p1+(r2*p2-s2*p2) by RLVECT_1:4
.=(r2-s2)*p2+(1-r2)*p1 by RLVECT_1:35;
then (1-s2)*p1-(1-r2)*p1=(r2-s2)*p2+((1-r2)*p1-(1-r2)*p1) by
RLVECT_1:def 3;
then (1-s2)*p1-(1-r2)*p1=(r2-s2)*p2+(0.TOP-REAL 2) by RLVECT_1:5;
then (1-s2)*p1-(1-r2)*p1=(r2-s2)*p2 by RLVECT_1:4;
then ((1-s2)-(1-r2))*p1=(r2-s2)*p2 by RLVECT_1:35;
then (r2-s2)=0 or p1=p2 by RLVECT_1:36;
hence thesis by A3,A15,A18;
end;
then
A19: LE q2,q1,p1,p2 by A1,A2;
thus LE q1,q2,p1,p2 or LT q2,q1,p1,p2 by A19;
end;
end;
now
assume that
A20: LE q1,q2,p1,p2 and
A21: LT q2,q1,p1,p2;
LE q2,q1,p1,p2 by A21;
then
A22: r2<=r1 by A4,A5,A6,A7,A9;
r1<=r2 by A4,A6,A7,A8,A9,A20;
then r1=r2 by A22,XXREAL_0:1;
hence contradiction by A4,A7,A21;
end;
hence thesis by A10;
end;
theorem Th29:
for f be FinSequence of TOP-REAL 2 for p,q be Point of TOP-REAL
2 st p in L~f & q in L~f & Index(p,f)<Index(q,f) holds q in L~L_Cut(f,p)
proof
let f be FinSequence of TOP-REAL 2;
let p,q be Point of TOP-REAL 2;
assume that
A1: p in L~f and
A2: q in L~f and
A3: Index(p,f)<Index(q,f);
A4: Index(q,f)<len f by A2,Th8;
then
A5: Index(q,f)-Index(p,f)<=len f -Index(p,f) by XREAL_1:9;
then
A6: Index(q,f)-Index(p,f)+1<=len f -Index(p,f)+1 by XREAL_1:6;
Index(q,f)-Index(p,f)<=len f -Index(p,f)-1+1 by A4,XREAL_1:9;
then
A7: Index(q,f)-'Index(p,f)<=len f - (Index(p,f)+1)+1 by A3,XREAL_1:233;
set i1 = Index(q,f)-'Index(p,f)+1;
A8: 1<=Index(p,f)+1 by NAT_1:11;
A9: Index(p,f)+1<=Index(q,f) by A3,NAT_1:13;
then
A10: Index(p,f)+1-Index(p,f)<=Index(q,f)-Index(p,f) by XREAL_1:9;
then
A11: 1<=Index(q,f)-'Index(p,f) by XREAL_0:def 2;
then
A12: 1<=Index(q,f)-'Index(p,f)+1 by NAT_D:48;
1+1<=Index(q,f)-'Index(p,f)+1 by A11,XREAL_1:6;
then
A13: 1<Index(q,f)-'Index(p,f)+1 by XXREAL_0:2;
then
A14: len <*p*><Index(q,f)-'Index(p,f)+1 by FINSEQ_1:40;
then
A15: len <*p*><Index(q,f)-'Index(p,f)+1+1 by NAT_1:13;
A16: Index(p,f)+1<=len f by A4,A9,XXREAL_0:2;
A17: 1<=Index(q,f) by A2,Th8;
then 1<len f by A4,XXREAL_0:2;
then
len mid(f,Index(p,f)+1,len f) = len f -'(Index(p,f)+1)+1
by A8,A16,FINSEQ_6:118;
then
A18: len <*p*>+len mid(f,Index(p,f)+1,len f) = 1+(len f -'(Index(p,f)+1)+1)
by FINSEQ_1:40
.= 1+(len f -(Index(p,f)+1)+1) by A4,A9,XREAL_1:233,XXREAL_0:2
.= (len f -Index(p,f))+1;
then
A19: Index(q,f)-'Index(p,f)+1<=len <*p*>+len mid(f,Index(p,f)+1,len f) by A3,A6
,XREAL_1:233;
per cases;
suppose
A20: p = f.(Index(p,f)+1);
then
A21: len L_Cut(f,p)=len f -Index(p,f) by A1,Th26;
then len L_Cut(f,p)>=Index(q,f)-'Index(p,f) by A3,A5,XREAL_1:233;
then (L_Cut(f,p))/.(Index(q,f)-'Index(p,f)) = L_Cut(f,p).(Index(q,f)-'
Index(p,f)) by A11,FINSEQ_4:15
.= mid(f,Index(p,f)+1,len f).(Index(q,f)-'Index(p,f)) by A20,Def3
.= f.(Index(p,f)+1+(Index(q,f)-'Index(p,f))-1)
by A11,A8,A16,A7,FINSEQ_6:122
.= f.(Index(p,f)+1+(Index(q,f)-Index(p,f))-1) by A3,XREAL_1:233
.= f.Index(q,f);
then
A22: (L_Cut(f,p))/.(Index(q,f)-'Index(p,f))=f/.Index(q,f) by A2,A4,Th8,
FINSEQ_4:15;
1<=Index(q,f) by A2,Th8;
then
A23: 1<=Index(q,f)+1 by NAT_D:48;
A24: q in LSeg(f,Index(q,f)) by A2,Th9;
A25: Index(q,f)<len f by A2,Th8;
then
A26: Index(q,f)+1<=len f by NAT_1:13;
then
A27: Index(q,f)+1-Index(p,f)<=len f -Index(p,f) by XREAL_1:9;
then Index(q,f)-Index(p,f)+1<=len f -Index(p,f);
then
A28: Index(q,f)-'Index(p,f)+1<=len f - (Index(p,f)+1)+1 by A3,XREAL_1:233;
Index(q,f)+1-Index(p,f)<=len f -Index(p,f) by A26,XREAL_1:9;
then Index(q,f)-Index(p,f)+1<=len f -Index(p,f);
then
A29: i1<=len L_Cut(f,p) by A10,A21,XREAL_0:def 2;
A30: Index(q,f)+1<=len f by A25,NAT_1:13;
Index(q,f)-Index(p,f)+1<=len f -Index(p,f) by A27;
then len L_Cut(f,p)>=Index(q,f)-'Index(p,f)+1 by A3,A21,XREAL_1:233;
then (L_Cut(f,p))/.(Index(q,f)-'Index(p,f)+1) = L_Cut(f,p).(Index(q,f)-'
Index(p,f)+1) by A13,FINSEQ_4:15
.= (mid(f,Index(p,f)+1,len f)).(Index(q,f)-'Index(p,f)+1) by A20,Def3
.= f.(Index(p,f)+1+(Index(q,f)-'Index(p,f)+1)-1) by A12,A8,A16,A28,
FINSEQ_6:122
.= f.(Index(p,f)+1+(Index(q,f)-Index(p,f)+1)-1) by A3,XREAL_1:233
.= f/.(Index(q,f)+1) by A23,A30,FINSEQ_4:15;
then q in LSeg((L_Cut(f,p))/.((Index(q,f)-'Index(p,f))), (L_Cut(f,p))/.((
Index(q,f)-'Index(p,f)+1))) by A17,A22,A26,A24,TOPREAL1:def 3;
hence thesis by A11,A29,SPPOL_2:15;
end;
suppose that
A31: p <> f.(Index(p,f)+1);
A32: len L_Cut(f,p)=len f -Index(p,f)+1 by A1,A31,Th26;
then len L_Cut(f,p)>=Index(q,f)-'Index(p,f)+1 by A3,A6,XREAL_1:233;
then (L_Cut(f,p))/.(Index(q,f)-'Index(p,f)+1) = L_Cut(f,p).(Index(q,f)-'
Index(p,f)+1) by FINSEQ_4:15,NAT_1:11
.= (<*p*>^mid(f,Index(p,f)+1,len f)).(Index(q,f)-'Index(p,f)+1) by A31
,Def3
.= mid(f,Index(p,f)+1,len f).(Index(q,f)-'Index(p,f)+1-len <*p*>) by A14
,A19,FINSEQ_6:108
.= mid(f,Index(p,f)+1,len f).(Index(q,f)-'Index(p,f)+1-1) by FINSEQ_1:40
.= f.(Index(p,f)+1+(Index(q,f)-'Index(p,f))-1)
by A11,A8,A16,A7,FINSEQ_6:122
.= f.(Index(p,f)+1+(Index(q,f)-Index(p,f))-1) by A3,XREAL_1:233
.= f.Index(q,f);
then
A33: (L_Cut(f,p))/.(Index(q,f)-'Index(p,f)+1)=f/.Index(q,f) by A2,A4,Th8,
FINSEQ_4:15;
A34: Index(q,f)<len f by A2,Th8;
then
A35: Index(q,f)+1<=len f by NAT_1:13;
then
A36: Index(q,f)+1-Index(p,f)<=len f -Index(p,f) by XREAL_1:9;
then Index(q,f)-Index(p,f)+1<=len f -Index(p,f);
then
A37: Index(q,f)-'Index(p,f)+1<=len f - (Index(p,f)+1)+1 by A3,XREAL_1:233;
Index(q,f)+1-Index(p,f)<=len f -Index(p,f) by A35,XREAL_1:9;
then Index(q,f)-Index(p,f)+1<=len f -Index(p,f);
then i1<=len f -Index(p,f) by A10,XREAL_0:def 2;
then
A38: i1+1<=len L_Cut(f,p) by A32,XREAL_1:6;
1<=Index(q,f) by A2,Th8;
then
A39: 1<=Index(q,f)+1 by NAT_D:48;
A40: q in LSeg(f,Index(q,f)) by A2,Th9;
A41: Index(q,f)+1<=len f by A34,NAT_1:13;
A42: Index(q,f)-Index(p,f)+1+1<=len f -Index(p,f)+1 by A36,XREAL_1:6;
then
A43: Index(q,f)-'Index(p,f)+1+1<=len <*p*>+len mid(f,Index(p,f)+1,len f)
by A3,A18,XREAL_1:233;
len L_Cut(f,p)>=Index(q,f)-'Index(p,f)+1+1 by A3,A32,A42,XREAL_1:233;
then
(L_Cut(f,p))/.(Index(q,f)-'Index(p,f)+1+1) = L_Cut(f,p).(Index(q,f)-'
Index(p,f)+1+1) by FINSEQ_4:15,NAT_1:11
.= (<*p*>^mid(f,Index(p,f)+1,len f)).(Index(q,f)-'Index(p,f)+1+1) by A31
,Def3
.= mid(f,Index(p,f)+1,len f).(Index(q,f)-'Index(p,f)+1+1-len <*p*>) by
A15,A43,FINSEQ_6:108
.= mid(f,Index(p,f)+1,len f).(Index(q,f)-'Index(p,f)+1+1-1) by
FINSEQ_1:40
.= f.(Index(p,f)+1+(Index(q,f)-'Index(p,f)+1)-1) by A12,A8,A16,A37,
FINSEQ_6:122
.= f.(Index(p,f)+1+(Index(q,f)-Index(p,f)+1)-1) by A3,XREAL_1:233
.= f/.(Index(q,f)+1) by A39,A41,FINSEQ_4:15;
then
q in LSeg((L_Cut(f,p))/.((Index(q,f)-'Index(p,f)+1)), (L_Cut(f,p))/.(
(Index(q,f)-'Index(p,f)+1+1))) by A17,A33,A35,A40,TOPREAL1:def 3;
hence thesis by A38,NAT_1:11,SPPOL_2:15;
end;
end;
theorem Th30:
for p,q,p1,p2 being Point of TOP-REAL 2 st LE p,q,p1,p2 holds q
in LSeg(p,p2) & p in LSeg(p1,q)
proof
let p,q,p1,p2 be Point of TOP-REAL 2;
assume
A1: LE p,q,p1,p2;
then p in LSeg(p1,p2);
then consider s1 being Real such that
A2: p=(1-s1)*p1+s1*p2 and
A3: 0<=s1 and
A4: s1<=1;
q in LSeg(p1,p2) by A1;
then consider s2 being Real such that
A5: q=(1-s2)*p1+s2*p2 and
A6: 0<=s2 and
A7: s2<=1;
A8: s1<=s2 by A1,A2,A4,A5,A6,A7;
A9: 1-s1>=0 by A4,XREAL_1:48;
A10: now
per cases;
case
A11: 1-s1<>0;
set s=(s2-s1)/(1-s1);
A12: (1-s1)*(((1-s2)/(1-s1)))=1-s2 by A11,XCMPLX_1:87;
A13: (1-s1)*(((s2-s1)/(1-s1)))=s2-s1 by A11,XCMPLX_1:87;
(1-(s2-s1)/(1-s1))=(1*(1-s1)-(s2-s1))/(1-s1) by A11,XCMPLX_1:127
.=((1-s1)+s1-s2)/(1-s1);
then
(1-s1)*((1-s)*p+s*p2) =(1-s1)*(((1-s2)/(1-s1))*((1-s1)*p1+s1*p2)) +
(1-s1)*(((s2-s1)/(1-s1))*p2) by A2,RLVECT_1:def 5
.=(1-s1)*(((1-s2)/(1-s1)))*((1-s1)*p1+s1*p2) +(1-s1)*(((s2-s1)/(1-s1
))*p2) by RLVECT_1:def 7
.=(1-s2)*((1-s1)*p1+s1*p2) +(1-s1)*(((s2-s1)/(1-s1)))*p2 by A12,
RLVECT_1:def 7
.=(1-s2)*((1-s1)*p1)+(1-s2)*(s1*p2) +(s2-s1)*p2 by A13,RLVECT_1:def 5
.=(1-s2)*(1-s1)*p1+(1-s2)*(s1*p2) +(s2-s1)*p2 by RLVECT_1:def 7
.=(1-s2)*(1-s1)*p1+(1-s2)*s1*p2 +(s2-s1)*p2 by RLVECT_1:def 7
.=(1-s2)*(1-s1)*p1+((1-s2)*s1*p2 +(s2-s1)*p2) by RLVECT_1:def 3
.=(1-s2)*(1-s1)*p1+(1*s1-s2*s1+(s2-s1))*p2 by RLVECT_1:def 6
.=(1-s1)*((1-s2)*p1)+(1-s1)*s2*p2 by RLVECT_1:def 7
.=(1-s1)*((1-s2)*p1)+(1-s1)*(s2*p2) by RLVECT_1:def 7
.=(1-s1)*q by A5,RLVECT_1:def 5;
then
A14: q=(1-s)*p+s*p2 by A11,RLVECT_1:36;
1-s1>=s2-s1 by A7,XREAL_1:9;
then (1-s1)/(1-s1)>=(s2-s1)/(1-s1) by A9,XREAL_1:72;
then
A15: 1>=s by A11,XCMPLX_1:60;
s2-s1>=0 by A8,XREAL_1:48;
hence q in LSeg(p,p2) by A9,A15,A14;
end;
case
1-s1=0;
then s2=1 by A7,A8,XXREAL_0:1;
then q =0.TOP-REAL 2 + 1*p2 by A5,RLVECT_1:10
.=0.TOP-REAL 2 + p2 by RLVECT_1:def 8
.=p2 by RLVECT_1:4;
hence q in LSeg(p,p2) by RLTOPSP1:68;
end;
end;
now
per cases;
case
A16: s2<>0;
set s=s1/s2;
s2/s2>=s1/s2 by A6,A8,XREAL_1:72;
then
A17: 1>=s by A16,XCMPLX_1:60;
A18: (s2-s1)+s1*(1-s2)=s2*(1-s1);
A19: s2*((s1)/s2)=s1 by A16,XCMPLX_1:87;
A20: s2*(((s2-s1)/s2))=s2-s1 by A16,XCMPLX_1:87;
s2*((1-s)*p1+s*q) =s2*(((1*s2-s1)/s2)*p1 +(s1/s2)*((1-s2)*p1+s2*p2)
) by A5,A16,XCMPLX_1:127
.=s2*(((s2-s1)/s2)*p1) +s2*((s1/s2)*((1-s2)*p1+s2*p2)) by
RLVECT_1:def 5
.=s2*(((s2-s1)/s2))*p1 +s2*((s1/s2)*((1-s2)*p1+s2*p2)) by
RLVECT_1:def 7
.=(s2-s1)*p1 +s2*(s1/s2)*((1-s2)*p1+s2*p2) by A20,RLVECT_1:def 7
.=(s2-s1)*p1 +(s1*((1-s2)*p1)+s1*(s2*p2)) by A19,RLVECT_1:def 5
.=(s2-s1)*p1 +(s1*(1-s2)*p1+s1*(s2*p2)) by RLVECT_1:def 7
.=(s2-s1)*p1 +(s1*(1-s2)*p1+s1*s2*p2) by RLVECT_1:def 7
.=(s2-s1)*p1 +s1*(1-s2)*p1+s1*s2*p2 by RLVECT_1:def 3
.=((s2-s1)+s1*(1-s2))*p1+s1*s2*p2 by RLVECT_1:def 6
.=s2*((1-s1)*p1)+s2*s1*p2 by A18,RLVECT_1:def 7
.=s2*((1-s1)*p1)+s2*(s1*p2) by RLVECT_1:def 7
.=s2*p by A2,RLVECT_1:def 5;
then p=(1-s)*p1+s*q by A16,RLVECT_1:36;
hence p in LSeg(p1,q) by A3,A6,A17;
end;
case
s2=0;
then s1=0 by A1,A2,A3,A4,A5;
then p =1*p1+(0.TOP-REAL 2) by A2,RLVECT_1:10
.=p1+(0.TOP-REAL 2) by RLVECT_1:def 8
.=p1 by RLVECT_1:4;
hence p in LSeg(p1,q) by RLTOPSP1:68;
end;
end;
hence thesis by A10;
end;
theorem Th31:
for f be FinSequence of TOP-REAL 2 for p,q be Point of TOP-REAL
2 st p in L~f & q in L~f & p<>q & Index(p,f) = Index(q,f) & LE p,q,f/.(Index(p,
f)),f/.(Index(p,f)+1) holds q in L~L_Cut(f,p)
proof
let f be FinSequence of TOP-REAL 2;
let p,q be Point of TOP-REAL 2;
assume that
A1: p in L~f and
A2: q in L~f and
A3: p<>q and
A4: Index(p,f)=Index(q,f) and
A5: LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1);
A6: Index(q,f)-'Index(p,f)=Index(q,f)-Index(p,f) by A4,XREAL_1:233
.=0 by A4;
Index(q,f)<len f by A2,Th8;
then
A7: Index(q,f)+1<=len f by NAT_1:13;
A8: now
q in LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) by A5;
then consider r be Real such that
A9: q = (1-r)*f/.(Index(p,f))+r*f/.(Index(p,f)+1) and
A10: 0 <= r and
A11: r <= 1;
A12: p = 1 * p by RLVECT_1:def 8
.= 0.TOP-REAL 2 + 1 * p by RLVECT_1:4
.= (1-1)*f/.(Index(p,f))+1 * p by RLVECT_1:10;
assume
A13: p = f.(Index(p,f)+1);
then p = f/.(Index(p,f)+1) by A4,A7,FINSEQ_4:15,NAT_1:11;
then 1<=r by A5,A9,A10,A12;
then r = 1 by A11,XXREAL_0:1;
hence contradiction by A3,A4,A7,A13,A9,A12,FINSEQ_4:15,NAT_1:11;
end;
then
A14: len L_Cut(f,p)=len f -Index(p,f)+1 by A1,Th26;
1<=Index(q,f) by A2,Th8;
then
A15: 1<=Index(q,f)+1 by NAT_D:48;
1<0+1+1;
then
A16: len <*p*> < Index(q,f)-'Index(p,f)+1+1 by A6,FINSEQ_1:40;
A17: Index(q,f)<len f by A2,Th8;
then
A18: Index(q,f)+1<=len f by NAT_1:13;
then
A19: Index(q,f)+1-Index(p,f)<=len f -Index(p,f) by XREAL_1:9;
then
A20: Index(q,f)-Index(p,f)+1+1<=len f -Index(p,f)+1 by XREAL_1:6;
Index(q,f)-Index(p,f)+1<=len f -Index(p,f) by A19;
then
A21: Index(q,f)-'Index(p,f)+1<=len f - (Index(p,f)+1)+1 by A4,XREAL_1:233;
A22: 1<=Index(p,f)+1 by NAT_1:11;
A23: Index(q,f)<len f by A2,Th8;
then Index(q,f)-Index(p,f)<=len f -Index(p,f) by XREAL_1:9;
then Index(q,f)-Index(p,f)+1<=len f -Index(p,f)+1 by XREAL_1:6;
then
A24: (L_Cut(f,p))/.(Index(q,f)-'Index(p,f)+1) = L_Cut(f,p).(Index(q,f)-'
Index(p,f)+1) by A4,A6,A14,FINSEQ_4:15
.= (<*p*>^mid(f,Index(p,f)+1,len f)).(Index(q,f)-'Index(p,f)+1) by A8,Def3
.= p by A6,FINSEQ_1:41;
set i1=Index(q,f)-'Index(p,f)+1;
A25: Index(q,f)+1<=len f by A17,NAT_1:13;
Index(q,f)+1-Index(p,f)<=len f -Index(p,f) by A18,XREAL_1:9;
then Index(q,f)-Index(p,f)+1<=len f -Index(p,f);
then i1<=len f -Index(p,f) by A4,XREAL_0:def 2;
then
A26: i1+1<=len L_Cut(f,p) by A14,XREAL_1:6;
1<=Index(q,f) by A2,Th8;
then 1<len f by A23,XXREAL_0:2;
then len mid(f,Index(p,f)+1,len f) = len f -'(Index(p,f)+1)+1 by A4,A7,A22,
FINSEQ_6:118;
then
len <*p*> + len mid(f,Index(p,f)+1,len f) = 1+(len f -'(Index(p,f)+1)+1
) by FINSEQ_1:40
.= 1+(len f -(Index(p,f)+1)+1) by A4,A7,XREAL_1:233
.= (len f -Index(p,f))+1;
then
A27: Index(q,f)-'Index(p,f)+1+1<=len <*p*>+len mid(f,Index(p,f)+1,len f) by A4
,A20,XREAL_1:233;
(L_Cut(f,p))/.(Index(q,f)-'Index(p,f)+1+1) = L_Cut(f,p).(Index(q,f)-'
Index(p,f)+1+1) by A4,A6,A14,A20,FINSEQ_4:15
.= (<*p*>^mid(f,Index(p,f)+1,len f)).(Index(q,f)-'Index(p,f)+1+1) by A8
,Def3
.= mid(f,Index(p,f)+1,len f).(Index(q,f)-'Index(p,f)+1+1-len <*p*>) by A16
,A27,FINSEQ_6:108
.= mid(f,Index(p,f)+1,len f).(Index(q,f)-'Index(p,f)+1+1-1) by FINSEQ_1:40
.= f.(Index(p,f)+1+(Index(q,f)-Index(p,f)+1)-1) by A4,A7,A6,A22,A21,
FINSEQ_6:122
.= f/.(Index(q,f)+1) by A15,A25,FINSEQ_4:15;
then q in LSeg((L_Cut(f,p))/.((Index(q,f)-'Index(p,f)+1)), (L_Cut(f,p))/.((
Index(q,f)-'Index(p,f)+1+1))) by A4,A5,A24,Th30;
hence thesis by A6,A26,SPPOL_2:15;
end;
begin
::--------------------------------------------------------:
:: Cutting Both Sides of a Finite Sequence and :
:: a Discussion of Speciality of Sequences in TOP-REAL 2 :
::--------------------------------------------------------:
definition
let f be FinSequence of TOP-REAL 2,p,q be Point of TOP-REAL 2;
func B_Cut(f,p,q) -> FinSequence of TOP-REAL 2 equals
:Def7:
R_Cut(L_Cut(f,p
),q) if p in L~f & q in L~f & Index(p,f)<Index(q,f) or Index(p,f)=Index(q,f) &
LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1) otherwise Rev (R_Cut(L_Cut(f,q),p));
correctness;
end;
theorem Th32:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL
2 st f is being_S-Seq & p in L~f & p<>f.1 holds R_Cut(f,p) is_S-Seq_joining f/.
1,p
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume that
A1: f is being_S-Seq and
A2: p in L~f and
A3: p<>f.1;
R_Cut(f,p)=mid(f,1,Index(p,f))^<*p*> by A3,Def4;
hence thesis by A1,A2,A3,Th19;
end;
theorem Th33:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL
2 st f is being_S-Seq & p in L~f & p<>f.len f holds L_Cut(f,p) is_S-Seq_joining
p,f/.len f
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume that
A1: f is being_S-Seq and
A2: p in L~f and
A3: p<>f.len f;
A4: f <> {} by A2,CARD_1:27,TOPREAL1:22;
A5: Rev f is being_S-Seq by A1;
A6: p in L~Rev f by A2,SPPOL_2:22;
A7: p <> (Rev f).1 by A3,FINSEQ_5:62;
L_Cut(f,p) = L_Cut(Rev Rev f,p)
.= Rev R_Cut(Rev f,p) by A1,A6,Th22;
then L_Cut(f,p) is_S-Seq_joining p,(Rev f)/.1 by A5,A6,A7,Th15,Th32;
hence thesis by A4,FINSEQ_5:65;
end;
theorem Th34:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL
2 st f is being_S-Seq & p in L~f & p<>f.len f holds L_Cut(f,p) is being_S-Seq
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume that
A1: f is being_S-Seq and
A2: p in L~f and
A3: p<>f.len f;
L_Cut(f,p) is_S-Seq_joining p,f/.len f by A1,A2,A3,Th33;
hence thesis;
end;
theorem Th35:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL
2 st f is being_S-Seq & p in L~f & p<>f.1 holds R_Cut(f,p) is being_S-Seq
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume that
A1: f is being_S-Seq and
A2: p in L~f and
A3: p<>f.1;
R_Cut(f,p) is_S-Seq_joining f/.1,p by A1,A2,A3,Th32;
hence thesis;
end;
Lm1: for f being FinSequence of TOP-REAL 2, p,q being Point of TOP-REAL 2 st f
is being_S-Seq & p in L~f & q in L~f & p<>q & (Index(p,f)<Index(q,f) or Index(p
,f)=Index(q,f) & LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1)) holds B_Cut(f,p,q)
is_S-Seq_joining p,q
proof
let f be FinSequence of TOP-REAL 2, p,q be Point of TOP-REAL 2;
assume that
A1: f is being_S-Seq and
A2: p in L~f and
A3: q in L~f and
A4: p<>q;
assume
A5: Index(p,f)<Index(q,f) or Index(p,f)=Index(q,f) & LE p,q,f/.(Index(p,
f)),f/.(Index(p,f)+1);
then
A6: B_Cut(f,p,q)=R_Cut(L_Cut(f,p),q) by A2,A3,Def7;
Index(p,f) < len f by A2,Th8;
then
A7: Index(p,f)+1 <= len f by NAT_1:13;
A8: Index(q,f)<len f by A3,Th8;
1<=Index(q,f) by A3,Th8;
then
A9: 1<len f by A8,XXREAL_0:2;
A10: now
per cases by A5;
case
A11: Index(p,f)<Index(q,f);
assume
A12: p=f.len f;
Index(p,f)+1<=Index(q,f) by A11,NAT_1:13;
then len f <= Index(q,f) by A1,A9,A12,Th12;
hence contradiction by A3,Th8;
end;
case
A13: Index(p,f)=Index(q,f) & LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1 );
A14: now
q in LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) by A13;
then consider r being Real such that
A15: q = (1-r)*f/.(Index(p,f))+r*f/.(Index(p,f)+1) and
A16: 0 <= r and
A17: r <= 1;
A18: p = 1*p by RLVECT_1:def 8
.= 0.TOP-REAL 2 + 1*p by RLVECT_1:4
.= (1-1)*f/.(Index(p,f))+1*p by RLVECT_1:10;
assume
A19: p = f.(Index(p,f)+1);
then p = f/.(Index(p,f)+1) by A7,FINSEQ_4:15,NAT_1:11;
then 1<=r by A13,A15,A16,A18;
then r = 1 by A17,XXREAL_0:1;
hence contradiction by A4,A7,A19,A15,A18,FINSEQ_4:15,NAT_1:11;
end;
assume p=f.len f;
hence contradiction by A1,A9,A14,Th12;
end;
end;
then L_Cut(f,p) is_S-Seq_joining p,f/.len f by A1,A2,Th33;
then
A20: (L_Cut(f,p)).1=p;
now
per cases by A5;
case
Index(p,f)<Index(q,f);
then q in L~(L_Cut(f,p)) by A2,A3,Th29;
hence ex i1 being Nat st 1<=i1 & i1+1<=len L_Cut(f,p) & q in
LSeg(L_Cut(f,p),i1) by SPPOL_2:13;
end;
case
Index(p,f)=Index(q,f) & LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1 );
then q in L~(L_Cut(f,p)) by A2,A3,A4,Th31;
hence ex i1 being Nat st 1<=i1 & i1+1<=len L_Cut(f,p) & q in
LSeg(L_Cut(f,p),i1) by SPPOL_2:13;
end;
end;
then
A21: q in L~L_Cut(f,p) by SPPOL_2:17;
then
A22: Index(q,L_Cut(f,p))<len L_Cut(f,p) by Th8;
1<=Index(q,L_Cut(f,p)) by A21,Th8;
then 1<=len L_Cut(f,p) by A22,XXREAL_0:2;
then p=(L_Cut(f,p))/.(1) by A20,FINSEQ_4:15;
hence thesis by A1,A2,A4,A6,A10,A21,A20,Th32,Th34;
end;
theorem Th36:
for f being FinSequence of TOP-REAL 2, p,q being Point of
TOP-REAL 2 st f is being_S-Seq & p in L~f & q in L~f & p<>q holds B_Cut(f,p,q)
is_S-Seq_joining p,q
proof
let f be FinSequence of TOP-REAL 2, p,q be Point of TOP-REAL 2;
assume that
A1: f is being_S-Seq and
A2: p in L~f and
A3: q in L~f and
A4: p<>q;
per cases;
suppose
Index(p,f)<Index(q,f) or Index(p,f)=Index(q,f) & LE p,q,f/.(Index(
p,f)),f/.(Index(p,f)+1);
hence thesis by A1,A2,A3,A4,Lm1;
end;
suppose
A5: not(Index(p,f)<Index(q,f) or Index(p,f)=Index(q,f) & LE p,q,f/.(
Index(p,f)),f/.(Index(p,f)+1));
A6: now
A7: Index(p,f) < len f by A2,Th8;
then
A8: Index(p,f)+1 <= len f by NAT_1:13;
1 <= Index(p,f)+1 by NAT_1:11;
then
A9: Index(p,f)+1 in dom f by A8,FINSEQ_3:25;
A10: Index(p,f)+0 <> Index(p,f)+1;
A11: 1 <= Index(p,f) by A2,Th8;
then
A12: LSeg(f,Index(p,f)) = LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) by A8,
TOPREAL1:def 3;
then
A13: p in LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) by A2,Th9;
Index(p,f) in dom f by A11,A7,FINSEQ_3:25;
then
A14: f/.(Index(p,f))<>f/.(Index(p,f)+1) by A1,A9,A10,PARTFUN2:10;
assume that
A15: Index(p,f)=Index(q,f) and
A16: not LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1);
q in LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) by A3,A15,A12,Th9;
then LT q,p,f/.(Index(p,f)),f/.(Index(p,f)+1) by A16,A13,A14,Th28;
hence LE q,p,f/.Index(q,f),f/.(Index(q,f)+1) by A15;
end;
A17: Index(q,f) < Index(p,f) or Index(p,f)=Index(q,f) & not LE p,q,f/.(
Index(p,f)),f/.(Index(p,f)+1) by A5,XXREAL_0:1;
B_Cut(f,p,q)=Rev R_Cut(L_Cut(f,q),p) by A5,Def7;
then
A18: Rev B_Cut(f,q,p) = B_Cut(f,p,q) by A2,A3,A17,A6,Def7;
B_Cut(f,q,p) is_S-Seq_joining q,p by A1,A2,A3,A4,A17,A6,Lm1;
hence thesis by A18,Th15;
end;
end;
theorem
for f being FinSequence of TOP-REAL 2, p,q being Point of TOP-REAL 2
st f is being_S-Seq & p in L~f & q in L~f & p<>q holds B_Cut(f,p,q) is
being_S-Seq
proof
let f be FinSequence of TOP-REAL 2, p,q be Point of TOP-REAL 2;
assume that
A1: f is being_S-Seq and
A2: p in L~f and
A3: q in L~f and
A4: p<>q;
B_Cut(f,p,q) is_S-Seq_joining p,q by A1,A2,A3,A4,Th36;
hence thesis;
end;
theorem Th38:
for f,g being FinSequence of TOP-REAL 2 st f.len f=g.1 & f is
being_S-Seq & g is being_S-Seq & L~f /\ L~g={g.1} holds f^mid(g,2,len g) is
being_S-Seq
proof
let f,g be FinSequence of TOP-REAL 2;
assume that
A1: f.len f=g.1 and
A2: f is being_S-Seq and
A3: g is being_S-Seq and
A4: L~f /\ L~g={g.1};
A5: len f >= 2 by A2,TOPREAL1:def 8;
A6: len (f^mid(g,2,len g))=len f + len mid(g,2,len g) by FINSEQ_1:22;
then len f<=len (f^mid(g,2,len g)) by NAT_1:11;
then
A7: len (f^mid(g,2,len g)) >= 2 by A5,XXREAL_0:2;
A8: len g >= 2 by A3,TOPREAL1:def 8;
then
A9: 1<=len g by XXREAL_0:2;
then
A10: len mid(g,2,len g)=len g -'2+1 by A8,FINSEQ_6:118
.=len g -2+1 by A8,XREAL_1:233
.=len g -1;
for x1,x2 being object st x1 in dom (f^mid(g,2,len g)) & x2 in dom (f^mid(
g,2,len g)) & (f^mid(g,2,len g)).x1=(f^mid(g,2,len g)).x2 holds x1=x2
proof
A11: rng g c=L~g by A8,SPPOL_2:18;
A12: rng (f^mid(g,2,len g)) c= the carrier of TOP-REAL 2 by FINSEQ_1:def 4;
let x1,x2 be object;
assume that
A13: x1 in dom (f^mid(g,2,len g)) and
A14: x2 in dom (f^mid(g,2,len g)) and
A15: (f^mid(g,2,len g)).x1=(f^mid(g,2,len g)).x2;
reconsider n1=x1,n2=x2 as Element of NAT by A13,A14;
A16: x2 in Seg len (f^mid(g,2,len g )) by A14,FINSEQ_1:def 3;
then
A17: 1<=n2 by FINSEQ_1:1;
(f^mid(g,2,len g)).x1 in rng (f^mid(g,2,len g)) by A13,FUNCT_1:def 3;
then reconsider q=(f^mid(g,2,len g)).x1 as Point of TOP-REAL 2 by A12;
A18: rng mid(g,2,len g) c= rng g by FINSEQ_6:119;
A19: rng f c= L~f by A5,SPPOL_2:18;
A20: now
A21: now
g|1=g|Seg 1 by FINSEQ_1:def 16;
then
A22: (g|1).1=g.1 by FINSEQ_1:3,FUNCT_1:49;
len (g|1)=1 by A8,FINSEQ_1:59,XXREAL_0:2;
then 1 in dom (g|1) by FINSEQ_3:25;
then
A23: g.1 in rng (g|1) by A22,FUNCT_1:def 3;
A24: 2-'1=2-1 by XREAL_1:233;
assume g.1 in rng mid(g,2,len g);
then
A25: g.1 in rng (g/^1) by A8,A24,FINSEQ_6:117;
rng(g|1) misses rng (g/^1) by A3,FINSEQ_5:34;
hence contradiction by A25,A23,XBOOLE_0:3;
end;
assume that
A26: q in rng f and
A27: q in rng mid(g,2,len g);
q in rng g by A18,A27;
then q in L~f /\ L~g by A19,A11,A26,XBOOLE_0:def 4;
hence contradiction by A4,A27,A21,TARSKI:def 1;
end;
n2<=len (f^mid(g,2,len g)) by A16,FINSEQ_1:1;
then
A28: n2-len f <=len f + len mid(g,2,len g)-len f by A6,XREAL_1:9;
A29: x1 in Seg len (f^mid(g,2,len g)) by A13,FINSEQ_1:def 3;
then n1<=len (f^mid(g,2,len g)) by FINSEQ_1:1;
then
A30: n1-len f <=len f + len mid(g,2,len g)-len f by A6,XREAL_1:9;
A31: 1<=n1 by A29,FINSEQ_1:1;
now
per cases;
case
n1<=len f;
then
A32: n1 in dom f by A31,FINSEQ_3:25;
then
A33: (f^mid(g,2,len g)).x1 =f.n1 by FINSEQ_1:def 7;
now
per cases;
case
n2<=len f;
then
A34: n2 in dom f by A17,FINSEQ_3:25;
then (f^mid(g,2,len g)).x2 =f.n2 by FINSEQ_1:def 7;
hence thesis by A2,A15,A32,A33,A34,FUNCT_1:def 4;
end;
case
A35: n2>len f;
then len f +1<=n2 by NAT_1:13;
then
A36: len f +1 -len f <=n2 - len f by XREAL_1:9;
then
A37: 1<=(n2-'len f) by NAT_D:39;
A38: len f + (n2-'len f)=len f+(n2-len f) by A35,XREAL_1:233
.=n2;
(n2-'len f)<=len mid(g,2,len g) by A28,A36,NAT_D:39;
then
A39: (n2-'len f) in dom mid(g,2,len g) by A37,FINSEQ_3:25;
then
(f^mid(g,2,len g)).(len f +(n2-'len f)) =mid(g,2,len g).(n2-'
len f) by FINSEQ_1:def 7;
hence contradiction by A15,A20,A32,A33,A39,A38,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
case
A40: n1>len f;
then len f +1<=n1 by NAT_1:13;
then
A41: len f +1 -len f <=n1 - len f by XREAL_1:9;
then
A42: 1<=n1-'len f by NAT_D:39;
then
A43: 1<=n1-'len f+1 by NAT_D:48;
n1-'len f<=n1-'len f +2 by NAT_1:11;
then
A44: n1-'len f +2-'1=n1-'len f +2-1 by A42,XREAL_1:233,XXREAL_0:2
.=n1-'len f +((1+1)-1);
A45: len f + (n1-'len f)=len f+(n1-len f) by A40,XREAL_1:233
.=n1;
A46: n1-'len f<=len mid(g,2,len g) by A30,A41,NAT_D:39;
then
A47: n1-'len f in dom mid(g,2,len g) by A42,FINSEQ_3:25;
then
A48: (f^mid(g,2,len g)).(len f +(n1-'len f)) =mid(g,2,len g).(n1-'len
f) by FINSEQ_1:def 7;
n1-'len f+1<=len g -1+1 by A10,A46,XREAL_1:6;
then
A49: n1-'len f+1 in dom g by A43,FINSEQ_3:25;
len f + (n1-'len f)=len f+(n1-len f) by A40,XREAL_1:233
.=n1;
then
A50: (f^mid(g,2,len g)).n1 =g.(n1-'len f+1) by A8,A9,A30,A41,A48,A44,
FINSEQ_6:118;
now
per cases;
case
n2<=len f;
then
A51: n2 in dom f by A17,FINSEQ_3:25;
then (f^mid(g,2,len g)).x2 =f.n2 by FINSEQ_1:def 7;
hence contradiction by A15,A20,A47,A48,A45,A51,FUNCT_1:def 3;
end;
case
A52: n2>len f;
then len f +1<=n2 by NAT_1:13;
then
A53: len f +1 -len f <=n2 - len f by XREAL_1:9;
then
A54: 1<=n2-'len f by NAT_D:39;
then
A55: 1<=n2-'len f+1 by NAT_D:48;
A56: (n2-'len f)<=len mid(g,2,len g) by A28,A53,NAT_D:39;
then n2-'len f+1<=len g -1+1 by A10,XREAL_1:6;
then
A57: n2-'len f+1 in dom g by A55,FINSEQ_3:25;
n2-'len f<=n2-'len f +2 by NAT_1:11;
then
A58: n2-'len f +2-'1=n2-'len f +2-1 by A54,XREAL_1:233,XXREAL_0:2
.=n2-'len f+1;
1<=(n2-'len f) by A53,NAT_D:39;
then (n2-'len f) in dom mid(g,2,len g) by A56,FINSEQ_3:25;
then
A59: (f^mid(g,2,len g)).(len f +(n2-'len f)) =mid(g,2,len g).(n2-'
len f) by FINSEQ_1:def 7;
len f + (n2-'len f)=len f+(n2-len f) by A52,XREAL_1:233
.=n2;
then (f^mid(g,2,len g)).n2 =g.(n2-'len f+1) by A8,A9,A28,A53,A59
,A58,FINSEQ_6:118;
then n1-'len f+1=n2-'len f+1 by A3,A15,A49,A50,A57,FUNCT_1:def 4;
then n1-len f=n2-'len f by A40,XREAL_1:233;
then n1-len f=n2-len f by A52,XREAL_1:233;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then
A60: f^mid(g,2,len g) is one-to-one by FUNCT_1:def 4;
A61: 1<=len f by A5,XXREAL_0:2;
A62: for i,j be Nat st i+1 < j holds LSeg(f^mid(g,2,len g),i) misses LSeg(f
^mid(g,2,len g),j)
proof
let i,j be Nat;
assume
A63: i+1 < j;
now
per cases;
case
A64: j<len f & j+1<=len (f^mid(g,2,len g));
then
A65: i+1<len f by A63,XXREAL_0:2;
then
A66: i<len f by NAT_1:13;
A67: j<=len (f^mid(g,2,len g)) by A64,NAT_D:46;
then
A68: i+1<len (f^mid(g,2,len g)) by A63,XXREAL_0:2;
then
A69: i<=len (f^mid(g,2,len g)) by NAT_D:46;
now
per cases;
case
A70: 1<=i;
then
A71: f/.i=f.i by A66,FINSEQ_4:15;
(f^mid(g,2,len g))/.i=(f^mid(g,2,len g)).i by A69,A70,FINSEQ_4:15;
then
A72: (f^mid(g,2,len g))/.i=f/.i by A66,A70,A71,FINSEQ_1:64;
A73: LSeg((f^mid(g,2,len g))/.i,(f^mid(g,2,len g))/.(i+1)) = LSeg
(f^mid(g,2,len g),i) by A68,A70,TOPREAL1:def 3;
A74: 1<=i+1 by A70,NAT_D:48;
then
A75: f/.(i+1)=f.(i+1) by A65,FINSEQ_4:15;
(f^mid(g,2,len g))/.(i+1)=(f^mid(g,2,len g)).(i+1) by A68,A74,
FINSEQ_4:15;
then LSeg((f^mid(g,2,len g))/.i,(f^mid(g,2,len g))/.(i+ 1)) =LSeg
(f/.i,f/.(i+1)) by A65,A74,A72,A75,FINSEQ_1:64;
then
A76: LSeg(f^mid(g,2,len g),i)=LSeg(f,i) by A65,A70,A73,TOPREAL1:def 3;
A77: 1<j by A63,A74,XXREAL_0:2;
then
A78: f/.j=f.j by A64,FINSEQ_4:15;
(f^mid(g,2,len g))/.j=(f^mid(g,2,len g)).j by A67,A77,FINSEQ_4:15;
then
A79: (f^mid(g,2,len g))/.j=f/.j by A64,A77,A78,FINSEQ_1:64;
A80: 1<=j+1 by A77,NAT_D:48;
then
A81: (f^mid(g,2,len g))/.(j+1)=(f^mid(g,2,len g)).(j+1) by A64,
FINSEQ_4:15;
A82: j+1<=len f by A64,NAT_1:13;
then
A83: LSeg(f,j)=LSeg(f/.j,f/.(j+1)) by A77,TOPREAL1:def 3;
f/.(j+1)=f.(j+1) by A80,A82,FINSEQ_4:15;
then
A84: LSeg((f^mid(g,2,len g))/.j,(f^mid(g,2,len g))/.(j+ 1)) =LSeg
(f/.j,f/.(j+1)) by A80,A82,A79,A81,FINSEQ_1:64;
LSeg((f^mid(g,2,len g))/.j,(f^mid(g,2,len g))/.(j+1)) = LSeg
(f^mid(g,2,len g),j) by A64,A77,TOPREAL1:def 3;
then LSeg(f^mid(g,2,len g),i) misses LSeg(f^mid(g,2,len g),j) by A2
,A63,A76,A84,A83,TOPREAL1:def 7;
hence LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,2,len g),j) = {} by
XBOOLE_0:def 7;
end;
case
i<1;
then LSeg(f^mid(g,2,len g),i)={} by TOPREAL1:def 3;
hence LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,2,len g),j) = {};
end;
end;
hence thesis by XBOOLE_0:def 7;
end;
case
A85: i+1<=len f & len f<=j & j+1<=len (f^mid(g,2,len g));
now
per cases by A63,A85,XXREAL_0:1;
case
A86: i+1<len f & len f<=j;
len f<=len f+len mid(g,2,len g) by NAT_1:11;
then
A87: i+1<len (f^mid(g,2,len g)) by A6,A86,XXREAL_0:2;
A88: len f<=j+1 by A86,NAT_D:48;
A89: 1+1<=j by A5,A86,XXREAL_0:2;
then
A90: 1<=j by NAT_D:46;
now
per cases;
case
A91: 1<=i;
i<=len f by A85,NAT_D:46;
then
A92: f/.i=f.i by A91,FINSEQ_4:15;
i<=len (f^mid(g,2,len g)) by A87,NAT_D:46;
then
A93: (
f^mid(g,2,len g))/.i=(f^mid(g,2,len g )).i by A91,FINSEQ_4:15;
i<=len f by A85,NAT_D:46;
then
A94: (f^mid(g,2,len g))/.i=f/.i by A91,A93,A92,FINSEQ_1:64;
A95: j<=len (f^mid(g,2,len g)) by A85,NAT_D:46;
A96: now
assume 1>j-'len f;
then j-'len f+1<=0+1 by NAT_1:13;
then
A97: j-'len f=0 by XREAL_1:6;
then j-len f=0 by A85,XREAL_1:233;
hence (f^mid(g,2,len g)).j = g.(j-'len f+1) by A1,A61,A97,
FINSEQ_1:64;
end;
1<=j+1 by A90,NAT_D:48;
then
A98: (f^mid(g,2,len g))/.(j+1)=(f^mid(g,2,len g )).(j+1) by A85,
FINSEQ_4:15;
A99: LSeg((f^mid(g,2,len g))/.i,(f^mid(g,2,len g))/.(i+1)) =
LSeg(f^mid(g,2,len g),i) by A87,A91,TOPREAL1:def 3;
A100: 1<=i+1 by A91,NAT_D:48;
then
A101: f/.(i+1)=f.(i+1) by A85,FINSEQ_4:15;
A102: now
assume 1>(j+1)-'len f;
then (j+1)-'len f+1<=0+1 by NAT_1:13;
then
A103: (j+1)-'len f=0 by XREAL_1:6;
then (j+1)-len f=0 by A88,XREAL_1:233;
hence
(f^mid(g,2,len g)).(j+1) = g.((j+1)-'len f+1) by A1,A61,A103,
FINSEQ_1:64;
end;
j+1+1<=len f+(len g-1)+1 by A6,A10,A85,XREAL_1:6;
then j+1+1-len f<=len f +len g -len f by XREAL_1:9;
then j-len f+1+1<=len g;
then
A104: j-'len f+1+1<=len g by A86,XREAL_1:233;
then j-'len f+1<=len g by NAT_D:46;
then
A105: g/.(j-'len f+1)=g.(j-'len f+1) by FINSEQ_4:15,NAT_1:11;
j-'len f+1+1-1<=len g-1 by A104,XREAL_1:9;
then
A106: j-'len f+1<=len g-2+1;
then j-'len f+1<=len g-'2+1 by A8,XREAL_1:233;
then
A107: j-'len f<=len g-'2+1 by NAT_D:46;
A108: now
assume
A109: 1<=j-'len f;
then 1<=j-len f by NAT_D:39;
then 1+len f<=j-len f +len f by XREAL_1:6;
then
A110: len f<j by NAT_1:13;
then (f^mid(g,2,len g)).j=mid(g,2,len g).(j-len f) by A95,
FINSEQ_6:108;
then (f^mid(g,2,len g)).j=mid(g,2,len g).(j-'len f) by A110,
XREAL_1:233;
then (f^mid(g,2,len g)).j=g.(j-'len f+2-1) by A8,A107,A109,
FINSEQ_6:122;
hence (f^mid(g,2,len g)).j=g.(j-'len f+1);
end;
A111: j-'len f+1=j-len f+1 by A85,XREAL_1:233
.=j+1-len f
.=j+1-'len f by A88,XREAL_1:233;
A112: now
assume
A113: 1<=(j+1)-'len f;
then 1<=(j+1)-len f by NAT_D:39;
then 1+len f<=(j+1)-len f +len f by XREAL_1:6;
then
A114: len f<(j+1) by NAT_1:13;
then (f^mid(g,2,len g)).(j+1)=mid(g,2,len g).((j+1)-len f)
by A85,FINSEQ_6:108;
then (f^mid(g,2,len g)).(j+1)=mid(g,2,len g).((j+1)-'len f)
by A114,XREAL_1:233;
then (f^mid(g,2,len g)).(j+1)=g.((j+1)-'len f+2-1) by A8,A106
,A111,A113,FINSEQ_6:122;
hence (f^mid(g,2,len g)).(j+1)=g.((j+1)-'len f+1);
end;
1<=1+(j-'len f) by NAT_1:11;
then
A115: LSeg(g,j-'len f+1)=LSeg(g/.(j-'len f+1),g/.(j-'len f+1+1
)) by A104,TOPREAL1:def 3;
1<=j by A89,NAT_D:46;
then
A116: (f^mid(g,2,len g))/.j=g/.(j-'len f+1) by A95,A105,A108,A96,
FINSEQ_4:15;
g/.(j-'len f+1+1)=g.(j-'len f+1+1) by A104,FINSEQ_4:15,NAT_1:11
;
then LSeg(f^mid(g,2,len g),j)=LSeg(g,j-'len f+1 ) by A85,A90
,A111,A115,A116,A98,A112,A102,TOPREAL1:def 3;
then
A117: LSeg(f^mid(g,2,len g),j) c=L~g by TOPREAL3:19;
A118: i+1+1<=len f by A86,NAT_1:13;
(f^mid(g,2,len g))/.(i+1)=(f^mid(g,2,len g)).(i+1) by A87,A100,
FINSEQ_4:15;
then LSeg((f^mid(g,2,len g))/.i,(f^mid(g,2, len g))/.(i+1)) =
LSeg(f/.i,f/.(i+1)) by A85,A100,A94,A101,FINSEQ_1:64;
then
A119: LSeg(f^mid(g,2,len g),i)=LSeg(f,i) by A85,A91,A99,
TOPREAL1:def 3;
then LSeg(f^mid(g,2,len g),i) c= L~f by TOPREAL3:19;
then
A120: LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,2 ,len g),j) c=
{g. 1} by A4,A117,XBOOLE_1:27;
now
per cases;
case
A121: i+1<len f-'1;
A122: 1<=len f by A5,XXREAL_0:2;
A123: len f-'1+1=len f-1+1 by A5,XREAL_1:233,XXREAL_0:2
.=len f;
A124: 1+1-1<=len f -1 by A5,XREAL_1:9;
now
f/.len f in LSeg(f,len f-'1) by A124,A123,TOPREAL1:21;
then
A125: g.1 in LSeg(f,len f-'1) by A1,A122,FINSEQ_4:15;
given x being object such that
A126: x in LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,
2,len g),j);
A127: x in LSeg(f,i) by A119,A126,XBOOLE_0:def 4;
x=g.1 by A120,A126,TARSKI:def 1;
then x in LSeg(f,i)/\ LSeg(f,len f-'1) by A127,A125,
XBOOLE_0:def 4;
then LSeg(f,i) meets LSeg(f,len f-'1) by XBOOLE_0:4;
hence contradiction by A2,A121,TOPREAL1:def 7;
end;
hence thesis by XBOOLE_0:4;
end;
case
i+1>=len f-'1;
then i+1>=len f-1 by A5,XREAL_1:233,XXREAL_0:2;
then
A128: i+1+1>=len f-1+1 by XREAL_1:6;
then
A129: i+1+1=len f by A118,XXREAL_0:1;
then
A130: i+1<=len f by NAT_1:11;
i+1=len f-1 by A129;
then
A131: i+1=len f-'1 by A5,XREAL_1:233,XXREAL_0:2;
A132: len f-'1+1=len f-1+1 by A5,XREAL_1:233,XXREAL_0:2
.=len f;
then 1+1<=len f-'1+1 by A2,TOPREAL1:def 8;
then
A133: 1<=len f-'1 by XREAL_1:6;
A134: i+(1+1)=len f by A118,A128,XXREAL_0:1;
now
1+1-1<=len f-1 by A5,XREAL_1:9;
then
A135: 1<=len f-'1 by NAT_D:39;
len f-'1<=len f by NAT_D:35;
then
A136: len f-'1 in dom f by A135,FINSEQ_3:25;
A137: LSeg(f,i)/\ LSeg(f,len f-'1)={f/.(i+1)} by A2,A91,A131
,A134,TOPREAL1:def 6;
f/.len f in LSeg(f,len f-'1) by A132,A133,TOPREAL1:21;
then
A138: g.1 in LSeg(f,len f-'1) by A1,A61,FINSEQ_4:15;
given x being object such that
A139: x in LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,
2,len g),j);
A140: x=g.1 by A120,A139,TARSKI:def 1;
x in LSeg(f,i) by A119,A139,XBOOLE_0:def 4;
then x in LSeg(f,i)/\ LSeg(f,len f -'1) by A140,A138,
XBOOLE_0:def 4;
then f.len f=f/.(i+1) by A1,A140,A137,TARSKI:def 1;
then
A141: f.len f=f.(len f-'1) by A131,A130,FINSEQ_4:15,NAT_1:11;
len f in dom f by A61,FINSEQ_3:25;
then len f=len f-'1 by A2,A141,A136,FUNCT_1:def 4;
then len f=len f-1 by A5,XREAL_1:233,XXREAL_0:2;
hence contradiction;
end;
hence LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,2,len g),j)
= {} by XBOOLE_0:def 1;
end;
end;
hence
LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,2,len g),j) = {}
by XBOOLE_0:def 7;
end;
case
i<1;
then LSeg(f^mid(g,2,len g),i)={} by TOPREAL1:def 3;
hence
LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,2,len g),j) = {};
end;
end;
hence LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,2,len g),j) = {};
end;
case
A142: i+1<=len f & len f<j;
1+1-1<=len g-1 by A8,XREAL_1:9;
then len f+1<=len f+len mid(g,2,len g) by A10,XREAL_1:7;
then len f<len f+len mid(g,2,len g) by NAT_1:13;
then
A143: i+1<len (f^mid(g,2,len g)) by A6,A142,XXREAL_0:2;
A144: len f<=j+1 by A142,NAT_D:48;
A145: 1+1<=j by A5,A142,XXREAL_0:2;
then
A146: 1<=j by NAT_D:46;
now
per cases;
case
A147: 1<=i;
i<=len f by A85,NAT_D:46;
then
A148: f/.i=f.i by A147,FINSEQ_4:15;
i<=len (f^mid(g,2,len g)) by A143,NAT_D:46;
then
A149: (
f^mid(g,2,len g))/.i=(f^mid(g,2,len g )).i by A147,FINSEQ_4:15;
i<=len f by A85,NAT_D:46;
then
A150: (f^mid(g,2,len g))/.i=f/.i by A147,A149,A148,FINSEQ_1:64;
A151: LSeg((f^mid(g,2,len g))/.i,(f^mid(g,2,len g))/.(i+1)) =
LSeg(f^mid(g,2,len g),i) by A143,A147,TOPREAL1:def 3;
A152: 1<=i+1 by A147,NAT_D:48;
then
A153: f/.(i+1)=f.(i+1) by A85,FINSEQ_4:15;
(f^mid(g,2,len g))/.(i+1)=(f^mid(g,2,len g)).(i+1) by A143,A152
,FINSEQ_4:15;
then LSeg((f^mid(g,2,len g))/.i,(f^mid(g,2, len g))/.(i+1)) =
LSeg(f/.i,f/.(i+1)) by A85,A152,A150,A153,FINSEQ_1:64;
then LSeg(f^mid(g,2,len g),i)=LSeg(f,i) by A85,A147,A151,
TOPREAL1:def 3;
then
A154: LSeg(f^mid(g,2,len g),i) c= L~f by TOPREAL3:19;
A155: j<=len (f^mid(g,2,len g)) by A85,NAT_D:46;
A156: now
assume 1>j-'len f;
then j-'len f+1<=0+1 by NAT_1:13;
then
A157: j-'len f=0 by XREAL_1:6;
then j-len f=0 by A85,XREAL_1:233;
hence (f^mid(g,2,len g)).j = g.(j-'len f+1) by A1,A61,A157,
FINSEQ_1:64;
end;
1<=j+1 by A146,NAT_D:48;
then
A158: (f^mid(g,2,len g))/.(j+1)=(f^mid(g,2,len g )).(j+1) by A85,
FINSEQ_4:15;
A159: now
assume 1>(j+1)-'len f;
then (j+1)-'len f+1<=0+1 by NAT_1:13;
then
A160: (j+1)-'len f=0 by XREAL_1:6;
then (j+1)-len f=0 by A144,XREAL_1:233;
hence
(f^mid(g,2,len g)).(j+1) = g.((j+1)-'len f+1) by A1,A61,A160,
FINSEQ_1:64;
end;
j+1+1<=len f+(len g-1)+1 by A6,A10,A85,XREAL_1:6;
then j+1+1-len f<=len f +len g -len f by XREAL_1:9;
then j-len f+1+1<=len g;
then
A161: j-'len f+1+1<=len g by A142,XREAL_1:233;
then j-'len f+1<=len g by NAT_D:46;
then
A162: g/.(j-'len f+1)=g.(j-'len f+1) by FINSEQ_4:15,NAT_1:11;
j-'len f+1+1-1<=len g-1 by A161,XREAL_1:9;
then
A163: j-'len f+1<=len g-2+1;
then j-'len f+1<=len g-'2+1 by A8,XREAL_1:233;
then
A164: j-'len f<=len g-'2+1 by NAT_D:46;
A165: now
assume
A166: 1<=j-'len f;
then 1<=j-len f by NAT_D:39;
then 1+len f<=j-len f +len f by XREAL_1:6;
then
A167: len f<j by NAT_1:13;
then (f^mid(g,2,len g)).j=mid(g,2,len g).(j-len f) by A155,
FINSEQ_6:108;
then (f^mid(g,2,len g)).j=mid(g,2,len g).(j-'len f) by A167,
XREAL_1:233;
then (f^mid(g,2,len g)).j=g.(j-'len f+2-1) by A8,A164,A166,
FINSEQ_6:122;
hence (f^mid(g,2,len g)).j=g.(j-'len f+1);
end;
A168: j-'len f+1=j-len f+1 by A85,XREAL_1:233
.=j+1-len f
.=j+1-'len f by A144,XREAL_1:233;
A169: now
assume
A170: 1<=(j+1)-'len f;
then 1<=(j+1)-len f by NAT_D:39;
then 1+len f<=(j+1)-len f +len f by XREAL_1:6;
then
A171: len f<(j+1) by NAT_1:13;
then (f^mid(g,2,len g)).(j+1)=mid(g,2,len g).((j+1)-len f)
by A85,FINSEQ_6:108;
then (f^mid(g,2,len g)).(j+1)=mid(g,2,len g).((j+1)-'len f)
by A171,XREAL_1:233;
then (f^mid(g,2,len g)).(j+1)=g.((j+1)-'len f+2-1) by A8,A163
,A168,A170,FINSEQ_6:122;
hence (f^mid(g,2,len g)).(j+1)=g.((j+1)-'len f+1);
end;
1<=1+(j-'len f) by NAT_1:11;
then
A172: LSeg(g,j-'len f+1)=LSeg(g/.(j-'len f+1),g/.(j-'len f+1+1
)) by A161,TOPREAL1:def 3;
1<=j by A145,NAT_D:46;
then
A173: (f^mid(g,2,len g))/.j=g/.(j-'len f+1) by A155,A162,A165,A156,
FINSEQ_4:15;
g/.(j-'len f+1+1)=g.(j-'len f+1+1) by A161,FINSEQ_4:15,NAT_1:11
;
then
A174: LSeg(f^mid(g,2,len g),j)=LSeg(g,j-'len f+1 ) by A85,A146,A168
,A172,A173,A158,A169,A159,TOPREAL1:def 3;
then LSeg(f^mid(g,2,len g),j) c=L~g by TOPREAL3:19;
then
A175: LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,2 ,len g),j) c=
{g. 1} by A4,A154,XBOOLE_1:27;
now
A176: 1+1 in dom g by A8,FINSEQ_3:25;
A177: j-'len f+1=j-len f+1 by A142,XREAL_1:233;
A178: 1+1<=len g by A3,TOPREAL1:def 8;
given x being object such that
A179: x in LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,2, len g),j);
A180: x in LSeg(g,j-'len f+1) by A174,A179,XBOOLE_0:def 4;
A181: x=g.1 by A175,A179,TARSKI:def 1;
then g/.1=x by A9,FINSEQ_4:15;
then x in LSeg(g,1) by A178,TOPREAL1:21;
then
A182: x in LSeg(g,1)/\ LSeg(g,j-'len f+1) by A180,XBOOLE_0:def 4;
then LSeg(g,1) meets LSeg(g,j-'len f+1) by XBOOLE_0:4;
then 1+1 >= j-'len f+1 by A3,TOPREAL1:def 7;
then 1>=j-'len f by XREAL_1:6;
then 1>=j-len f by NAT_D:39;
then
A183: 1+len f>=j-len f+len f by XREAL_1:6;
j>=len f+1 by A142,NAT_1:13;
then
A184: j=len f +1 by A183,XXREAL_0:1;
LSeg(g,j-'len f+1)<>{} by A174,A179;
then 1+2<=len g by A184,A177,TOPREAL1:def 3;
then LSeg(g,1)/\ LSeg(g,j-'len f+1)={g/.(1+1)} by A3,A184
,A177,TOPREAL1:def 6;
then
A185: x=g/.(1+1) by A182,TARSKI:def 1
.=g.(1+1) by A8,FINSEQ_4:15;
1 in dom g by A9,FINSEQ_3:25;
hence contradiction by A3,A181,A185,A176,FUNCT_1:def 4;
end;
hence
LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,2,len g),j) = {}
by XBOOLE_0:def 1;
end;
case
i<1;
then LSeg(f^mid(g,2,len g),i)={} by TOPREAL1:def 3;
hence
LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,2,len g),j) = {};
end;
end;
hence LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,2,len g),j) = {};
end;
end;
hence thesis by XBOOLE_0:def 7;
end;
case
A186: len f<i+1 & j+1<=len (f^mid(g,2,len g));
then
A187: len f<=i by NAT_1:13;
then
A188: i-'len f=i-len f by XREAL_1:233;
A189: 1+1<=i by A5,A187,XXREAL_0:2;
then
A190: 1<=i by NAT_D:46;
then
A191: 1<=i+1 by NAT_D:48;
then
A192: 1<=j by A63,XXREAL_0:2;
A193: 1<=(j-'len f)+1 by NAT_1:11;
A194: len f<j by A63,A186,XXREAL_0:2;
j<=j+1 by NAT_1:11;
then
A195: len f<j+1 by A194,XXREAL_0:2;
A196: 1<=(i-'len f)+1 by NAT_1:11;
A197: j-'len f=j-len f by A63,A186,XREAL_1:233,XXREAL_0:2;
i+1-len f<j-len f by A63,XREAL_1:9;
then
A198: i-'len f +1+1<j-'len f +1 by A188,A197,XREAL_1:6;
now
per cases;
case
A199: j+1<=len (f^mid(g,2,len g));
A200: 1 <=j by A63,A191,XXREAL_0:2;
then 1<=j+1 by NAT_D:48;
then
A201: (f^mid(g,2,len g))/.(j+1)=(f^mid(g,2,len g)).(j+1) by A199,
FINSEQ_4:15;
len f+1<=j by A194,NAT_1:13;
then
A202: len f+1-len f<=j-len f by XREAL_1:9;
A203: 1<=i by A189,NAT_D:46;
then
A204: 1<=i+1 by NAT_D:48;
A205: j<=len (f^mid(g,2,len g)) by A199,NAT_D:46;
then
A206: i+1<len (f^mid(g,2,len g)) by A63,XXREAL_0:2;
then
A207: i<=len (f^mid(g,2,len g)) by NAT_D:46;
i+1<len f+(len g-1) by A10,A206,FINSEQ_1:22;
then
A208: i+1-len f<len f+(len g-1)-len f by XREAL_1:9;
then
A209: i-len f+1+1<len g-1+1 by XREAL_1:6;
then (i-'len f+1)+1<=len g by A187,XREAL_1:233;
then
A210: g/.((i-'len f+1)+1)=g.((i-'len f+1)+1) by FINSEQ_4:15,NAT_1:11;
i+1<=len (f^mid(g,2,len g)) by A63,A205,XXREAL_0:2;
then
A211: (f^mid(g,2,len g))/.(i+1)=(f^mid(g,2,len g)).( i+1) by A204,
FINSEQ_4:15;
A212: LSeg((f^mid(g,2,len g))/.j,(f^mid(g,2,len g))/.(j+1)) = LSeg
(f^mid(g,2,len g),j) by A192,A199,TOPREAL1:def 3;
A213: LSeg((f^mid(g,2,len g))/.i,(f^mid(g,2,len g))/.(i+1)) = LSeg
(f^mid(g,2,len g),i) by A190,A206,TOPREAL1:def 3;
A214: (i-'len f+1)<=len g by A188,A209,NAT_D:46;
then
A215: g/.(i-'len f+1)=g.(i-'len f+1) by FINSEQ_4:15,NAT_1:11;
A216: now
per cases;
case
i<=len f;
then
A217: i=len f by A187,XXREAL_0:1;
then (f^mid(g,2,len g)).i =g.(0+1) by A1,A190,FINSEQ_1:64
.=g.(i-'len f+1) by A217,XREAL_1:232;
hence
(f^mid(g,2,len g))/.i=g/.(i-'len f+1) by A203,A207,A215,
FINSEQ_4:15;
end;
case
A218: i>len f;
then len f+1<=i by NAT_1:13;
then
A219: len f+1-len f<=i-len f by XREAL_1:9;
i-'len f+1-1<=len g-1 by A214,XREAL_1:9;
then
A220: i-'len f<=len g -2+1;
(f^mid(g,2,len g)).i =mid(g,2,len g).(i-'len f) by A188,A207
,A218,FINSEQ_6:108
.=g.(i-'len f+2-1) by A8,A188,A219,A220,FINSEQ_6:122
.=g.(i-'len f +1);
hence
(f^mid(g,2,len g))/.i=g/.(i-'len f+1) by A203,A207,A215,
FINSEQ_4:15;
end;
end;
j+1<=len f+(len g-1) by A10,A199,FINSEQ_1:22;
then
A221: j+1-len f<=len f+(len g-1)-len f by XREAL_1:9;
then
A222: (j-'len f+1)<=len g-2+1 by A197;
A223: j-'len f+1+2-1=j-'len f+1+1;
A224: (f^mid(g,2,len g)).(j+1)=mid(g,2,len g).(j+1-len f) by A195,A199,
FINSEQ_6:108
.=g.(j-'len f +1+1) by A8,A197,A193,A222,A223,FINSEQ_6:122;
A225: i-'len f+1+2-1 =i-'len f+1+1;
A226: (i-'len f+1)<=len g-2+1 by A188,A208;
(f^mid(g,2,len g)).(i+1)=mid(g,2,len g).(i+1-len f) by A186,A206,
FINSEQ_6:108
.=g.(i-'len f +1+1) by A8,A188,A196,A226,A225,FINSEQ_6:122;
then
A227: LSeg(f^mid(g,2,len g),i)=LSeg(g,(i-'len f+1)) by A188,A196,A209
,A216,A211,A210,A213,TOPREAL1:def 3;
A228: j-len f+1+1<=len g-1+1 by A221,XREAL_1:6;
then
A229: (j-'len f+1)<=len g by A197,NAT_D:46;
then
A230: g/.(j-'len f+1)=g.(j-'len f+1) by FINSEQ_4:15,NAT_1:11;
A231: j<=len (f^mid(g,2,len g)) by A199,NAT_D:46;
then
A232: (f^mid(g,2,len g))/.j=(f^mid(g,2,len g)).j by A200,FINSEQ_4:15;
(j-'len f+1)+1<=len g by A63,A186,A228,XREAL_1:233,XXREAL_0:2;
then
A233: g/.((j-'len f+1)+1)=g.((j-'len f+1)+1) by FINSEQ_4:15,NAT_1:11;
j-'len f+1-1<=len g-1 by A229,XREAL_1:9;
then
A234: j-'len f<=len g -2+1;
(f^mid(g,2,len g)).j=mid(g,2,len g).(j-len f) by A194,A231,
FINSEQ_6:108
.=g.(j-'len f+2-1) by A8,A197,A202,A234,FINSEQ_6:122
.=g.(j-'len f +1);
then LSeg(f^mid(g,2,len g),j)=LSeg(g,j-'len f+1) by A197,A193,A228
,A232,A230,A201,A233,A224,A212,TOPREAL1:def 3;
then LSeg(f^mid(g,2,len g),i) misses LSeg(f^mid(g,2,len g),j) by A3
,A198,A227,TOPREAL1:def 7;
hence LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,2,len g),j) = {} by
XBOOLE_0:def 7;
end;
case
j+1>len (f^mid(g,2,len g));
then LSeg(f^mid(g,2,len g),j)={} by TOPREAL1:def 3;
hence LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,2,len g),j) = {};
end;
end;
hence LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,2,len g),j) = {};
end;
case
j+1>len (f^mid(g,2,len g));
then LSeg(f^mid(g,2,len g),j) = {} by TOPREAL1:def 3;
hence LSeg(f^mid(g,2,len g),i) /\ LSeg(f^mid(g,2,len g),j) = {};
end;
end;
hence thesis by XBOOLE_0:def 7;
end;
A235: for i be Nat st 1 <= i & i + 2 <= len (f^mid(g,2,len g)) holds LSeg(f^
mid(g,2,len g),i) /\ LSeg(f^mid(g,2,len g),i+1) = {(f^mid(g,2,len g))/.(i+1)}
proof
let i be Nat;
assume that
A236: 1 <= i and
A237: i + 2 <= len (f^mid(g,2,len g));
A238: 1<=i+1 by A236,NAT_D:48;
A239: i<=len (f^mid(g,2,len g)) by A237,NAT_D:47;
A240: 1<=i+1+1 by A236,NAT_D:48;
A241: i+1<=len (f^mid(g,2,len g)) by A237,NAT_D:47;
i+1+1<=len f + len mid(g,2,len g) by A237,FINSEQ_1:22;
then i+1+1<=len f + (len g -'2+1) by A8,A9,FINSEQ_6:118;
then i+1+1<=len f + (len g -(1+1)+1) by A8,XREAL_1:233;
then
A242: i+1+1-len f<=len f + (len g -(1+1)+1)-len f by XREAL_1:9;
then
A243: i+1-len f+1+1<=len g -1+1 by XREAL_1:6;
then
A244: i-len f+1+1+1<=len g;
now
per cases;
case
A245: i+2<=len f;
A246: (f^mid(g,2,len g))/.(i+1)=(f^mid(g,2,len g)).(i+1) by A238,A241,
FINSEQ_4:15;
i+1+1<=len f by A245;
then
A247: i+1<=len f by NAT_D:46;
then f/.(i+1)=f.(i+1) by A238,FINSEQ_4:15;
then
A248: (f^mid(g,2,len g))/.(i+1)=f/.(i+1) by A238,A247,A246,FINSEQ_1:64;
A249: f/.(i+1+1)=f.(i+1+1) by A240,A245,FINSEQ_4:15;
A250: LSeg((f^mid(g,2,len g))/.(i+1),(f^mid(g,2,len g))/.(i+1+1)) =
LSeg(f^mid(g,2,len g),i+1) by A237,A238,TOPREAL1:def 3;
A251: (f^mid(g,2,len g))/.i=(f^mid(g,2,len g)).i by A236,A239,FINSEQ_4:15;
A252: i<=len f by A247,NAT_D:46;
then f/.i=f.i by A236,FINSEQ_4:15;
then
A253: (f^mid(g,2,len g))/.i=f/.i by A236,A252,A251,FINSEQ_1:64;
(f^mid(g,2,len g))/.(i+1+1)=(f^mid(g,2,len g)).(i+1+1) by A237,A240,
FINSEQ_4:15;
then LSeg((f^mid(g,2,len g))/.(i+1),(f^mid(g,2,len g))/.(i+1+1) ) =
LSeg(f/.(i+1),f/.(i+1+1)) by A240,A245,A248,A249,FINSEQ_1:64;
then
A254: LSeg(f^mid(g,2,len g),i+1)=LSeg(f,i+1) by A238,A245,A250,TOPREAL1:def 3
;
LSeg((f^mid(g,2,len g))/.i,(f^mid(g,2,len g))/.(i+1)) = LSeg(f^
mid(g,2,len g),i) by A236,A241,TOPREAL1:def 3;
then LSeg(f^mid(g,2,len g),i)=LSeg(f,i) by A236,A247,A253,A248,
TOPREAL1:def 3;
hence thesis by A2,A236,A245,A248,A254,TOPREAL1:def 6;
end;
case
i+2>len f;
then
A255: i+2>=len f +1 by NAT_1:13;
now
per cases by A255,XXREAL_0:1;
case
A256: i+2>len f +1;
then i+1+1>len f+1;
then
A257: i+1>=len f +1 by NAT_1:13;
then
A258: i>=len f by XREAL_1:6;
A259: now
assume 1>i-'len f;
then i-'len f+1<=0+1 by NAT_1:13;
then
A260: i-'len f=0 by XREAL_1:6;
then i-len f=0 by A258,XREAL_1:233;
hence (f^mid(g,2,len g)).i = g.(i-'len f+1) by A1,A61,A260,
FINSEQ_1:64;
end;
A261: i+1>=len f by A257,NAT_D:48;
A262: now
assume 1>(i+1)-'len f;
then (i+1)-'len f+1<=0+1 by NAT_1:13;
then
A263: (i+1)-'len f=0 by XREAL_1:6;
then (i+1)-len f=0 by A261,XREAL_1:233;
hence (f^mid(g,2,len g)).(i+1) = g.((i+1)-'len f+1) by A1,A61
,A263,FINSEQ_1:64;
end;
i+1+1>=len f+1+1 by A256,NAT_1:13;
then i+1+1-(len f+1)>=len f+1+1-(len f+1) by XREAL_1:9;
then i-len f+1>=1;
then
A264: i-'len f+1>=1 by A258,XREAL_1:233;
then
A265: i-'len f+1+1>=1 by NAT_D:48;
then
A266: i-len f+1+1>=1 by A258,XREAL_1:233;
then i+1-len f+1>=1;
then
A267: i+1-'len f+1>=1 by A261,XREAL_1:233;
then
A268: i+1-'len f+1+1>=1 by NAT_D:48;
i+1-len f+1>=0+1 by A266;
then
A269: i+1-len f>=0 by XREAL_1:6;
then i+1-'len f+1+1<=len g by A243,XREAL_0:def 2;
then
A270: g/.(i+1-'len f+1+1)=g.(i+1-'len f+1+1) by A268,FINSEQ_4:15;
i+1-'len f+1+1<=len g by A243,A261,XREAL_1:233;
then
A271: LSeg(g,i+1-'len f+1) =LSeg(g/.(i+1-'len f+1),g/.(i+1-'len f+
1+1)) by A267,TOPREAL1:def 3;
i+1+1-len f+1=i+1-len f+1+1;
then
A272: i+1+1-len f+1=i+1-'len f+1+1 by A269,XREAL_0:def 2;
A273: i-'len f+1+1+1<=len g by A244,A258,XREAL_1:233;
then
A274: i-'len f+1+1<=len g by NAT_D:46;
then
A275: LSeg(g,i-'len f+1)=LSeg(g/.(i-'len f+1),g/.(i-'len f+1+1))
by A264,TOPREAL1:def 3;
i-'len f+1+1-1<=len g -1 by A274,XREAL_1:9;
then i-'len f+1<=len g -2+1;
then
A276: i-'len f+1<=len g -'2+1 by A8,XREAL_1:233;
then
A277: i-'len f<=len g -'2+1 by NAT_D:46;
A278: now
assume
A279: 1<=i-'len f;
then 1<=i-len f by NAT_D:39;
then 1+len f<=i-len f +len f by XREAL_1:6;
then
A280: len f<i by NAT_1:13;
then
(f^mid(g,2,len g)).i=mid(g,2,len g).(i-len f)
by A239,FINSEQ_6:108;
then (f^mid(g,2,len g)).i=mid(g,2,len g).(i-'len f) by A280,
XREAL_1:233;
then
(f^mid(g,2,len g)).i=g.(i-'len f+2-1)
by A8,A277,A279,FINSEQ_6:122;
hence (f^mid(g,2,len g)).i=g.(i-'len f+1);
end;
i-'len f+1<=len g by A274,NAT_D:46;
then g/.(i-'len f+1)=g.(i-'len f+1) by A264,FINSEQ_4:15;
then
A281: (f^mid(g,2,len g))/.i=g/.(i-'len f+1) by A236,A239,A278,A259,
FINSEQ_4:15;
A282: i-'len f+1+(1+1)<=len g by A273;
A283: g/.(i-'len f+1+1)=g.(i-'len f+1+1) by A274,A265,FINSEQ_4:15;
i-len f+1<=len g -'2+1 by A258,A276,XREAL_1:233;
then i+1-len f<=len g -'2+1;
then
A284: i+1-'len f<=len g -'2+1 by A261,XREAL_1:233;
A285: now
assume
A286: 1<=(i+1)-'len f;
then 1<=(i+1)-len f by NAT_D:39;
then 1+len f<=(i+1)-len f +len f by XREAL_1:6;
then
A287: len f<(i+1) by NAT_1:13;
then (f^mid(g,2,len g)).(i+1)=mid(g,2,len g).((i+1)-len f) by
A241,FINSEQ_6:108;
then (f^mid(g,2,len g)).(i+1)=mid(g,2,len g).((i+1)-'len f) by
A287,XREAL_1:233;
then (f^mid(g,2,len g)).(i+1)=g.((i+1)-'len f+2-1) by A8,A284
,A286,FINSEQ_6:122;
hence (f^mid(g,2,len g)).(i+1)=g.((i+1)-'len f+1);
end;
A288: now
assume 1>(i+1+1)-'len f;
then
A289: (i+1+1)-'len f+1<=0+1 by NAT_1:13;
then (i+1+1)-'len f<=0 by XREAL_1:6;
then
A290: (i+1+1)-len f=0 by A266,XREAL_0:def 2;
(i+1+1)-'len f=0 by A289,XREAL_1:6;
hence
(f^mid(g,2,len g)).(i+1+1) = g.((i+1+1)-'len f+1) by A1,A61,A290,
FINSEQ_1:64;
end;
i+1-len f+1=i-len f+1+1;
then
A291: i+1-len f+1=i-'len f+1+1 by A258,XREAL_1:233;
then
A292: i+1-'len f+1=i-'len f+1+1 by A261,XREAL_1:233;
A293: i+1+1-'len f<=len g-2+1 by A242,A266,XREAL_0:def 2;
A294: now
assume
A295: 1<=(i+1+1)-'len f;
then 1<=(i+1+1)-len f by NAT_D:39;
then 1+len f<=(i+1+1)-len f +len f by XREAL_1:6;
then
A296: len f<(i+1+1) by NAT_1:13;
then (f^mid(g,2,len g)).(i+1+1)=mid(g,2,len g).((i+1+1)-len f)
by A237,FINSEQ_6:108;
then (f^mid(g,2,len g)).(i+1+1)=mid(g,2,len g).((i+1+1)-'len f)
by A296,XREAL_1:233;
then (f^mid(g,2,len g)).(i+1+1)=g.((i+1+1)-'len f+2-1) by A8,A293
,A295,FINSEQ_6:122;
hence (f^mid(g,2,len g)).(i+1+1)=g.((i+1+1)-'len f+1);
end;
A297: (f^mid(g,2,len g))/.(i+1+1)=(f^mid(g,2,len g)).(i+1+1) by A237,A240
,FINSEQ_4:15;
A298: LSeg(f^mid(g,2,len g),i) =LSeg((f^mid(g,2,len g))/.i,(f^mid(
g,2,len g))/.(i+1)) by A236,A241,TOPREAL1:def 3;
A299: (f^mid(g,2,len g))/.(i+1)=(f^mid(g,2,len g)).(i+1) by A238,A241,
FINSEQ_4:15;
LSeg(f^mid(g,2,len g),i+1) =LSeg((f^mid(g,2,len g))/.(i+1),(
f^mid(g,2,len g))/.(i+1+1)) by A237,A238,TOPREAL1:def 3;
then LSeg(f^mid(g,2,len g),i+1)=LSeg(g,i+1-'len f+1) by A291,A272
,A299,A283,A285,A262,A271,A297,A270,A294,A288,XREAL_0:def 2;
hence thesis by A3,A264,A292,A298,A275,A281,A299,A283,A285,A282,
TOPREAL1:def 6;
end;
case
A300: i+2=len f +1;
then
A301: f/.(i+1)=f.(i+1) by A238,FINSEQ_4:15;
then
A302: f/.(i+1)=g/.1 by A1,A9,A300,FINSEQ_4:15;
(f^mid(g,2,len g))/.(i+1)=(f^mid(g,2,len g)).(i+1) by A238,A241,
FINSEQ_4:15;
then
A303: (f^mid(g,2,len g))/.(i+1)=f/.(i+1) by A238,A300,A301,FINSEQ_1:64;
A304: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A236,A300,TOPREAL1:def 3;
A305: (f^mid(g,2,len g))/.i=(f^mid(g,2,len g)).i by A236,A239,FINSEQ_4:15
;
i+1+1=len f+1 by A300;
then
A306: i<=len f by NAT_D:46;
then f/.i=f.i by A236,FINSEQ_4:15;
then
A307: (f^mid(g,2,len g))/.i=f/.i by A236,A306,A305,FINSEQ_1:64;
A308: LSeg((f^mid(g,2,len g))/.i,(f^mid(g,2,len g))/.(i+1)) = LSeg
(f^mid(g,2,len g),i) by A236,A241,TOPREAL1:def 3;
i=len f -1 by A300;
then
A309: i=len f-'1 by A5,XREAL_1:233,XXREAL_0:2;
A310: g/.1 in LSeg(g/.1,g/.(1+1)) by RLTOPSP1:68;
A311: g/.1=g.1 by A9,FINSEQ_4:15;
then g/.1= f/.len f by A1,A61,FINSEQ_4:15;
then
A312: g/.1 in LSeg(f/.(len f-'1),f/.len f) by RLTOPSP1:68;
len g -2>=0 by A8,XREAL_1:48;
then
A313: 0+1<=len g-2+1 by XREAL_1:6;
len f<(i+1+1) by A300,NAT_1:13;
then (f^mid(g,2,len g)).(i+1+1)=mid(g,2,len g).((i+1+1)-len f) by
A237,FINSEQ_6:108;
then
A314: (f^mid(g,2,len g)).(i+1+1)=g.(2+1-'1) by A8,A300,A313,FINSEQ_6:122
.=g.2 by NAT_D:34;
A315: LSeg(g,1)c=L~g by TOPREAL3:19;
LSeg(f,i)c=L~f by TOPREAL3:19;
then
A316: LSeg(f,i) /\ LSeg(g,1) c= {g/.1} by A4,A311,A315,XBOOLE_1:27;
A317: i+1-'len f+1 =0+1 by A300,XREAL_1:232
.=1;
then
A318: g/.(i+1-'len f+1+1)=g.(i+1-'len f+1+1) by A8,FINSEQ_4:15;
LSeg(g,1)=LSeg(g/.1,g/.(1+1)) by A8,TOPREAL1:def 3;
then g/.1 in LSeg(f,i) /\ LSeg(g,1) by A300,A309,A304,A312,A310,
XBOOLE_0:def 4;
then
A319: {g/.1} c= LSeg(f,i) /\ LSeg(g,1) by ZFMISC_1:31;
A320: (f^mid(g,2,len g))/.(i+1+1)=(f^mid(g,2,len g)).(i+1+1) by A237,A240
,FINSEQ_4:15;
A321: LSeg(f^mid(g,2,len g),i+1) =LSeg((f^mid(g,2,len g))/.(i+1),(
f^mid(g,2,len g))/.(i+1+1)) by A237,A238,TOPREAL1:def 3;
LSeg(g,i+1-'len f+1) =LSeg(g/.(i+1-'len f+1),g/.(i +1-'len f
+1+1)) by A8,A317,TOPREAL1:def 3;
hence thesis by A307,A302,A303,A308,A304,A321,A317,A320,A318,A314
,A319,A316,XBOOLE_0:def 10;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
for i be Nat st 1 <= i & i+1 <= len (f^mid(g,2,len g)) holds ((f^mid(g
,2,len g))/.i)`1 = ((f^mid(g,2,len g))/.(i+1))`1 or ((f^mid(g,2,len g))/.i)`2 =
((f^mid(g,2,len g))/.(i+1))`2
proof
let i be Nat;
assume that
A322: 1 <= i and
A323: i+1 <= len (f^mid(g,2,len g));
now
per cases;
case
A324: i<len f;
i<=len (f^mid(g,2,len g)) by A323,NAT_D:46;
then
A325: (f^mid(g,2,len g))/.i=(f^mid(g,2,len g)).i by A322,FINSEQ_4:15;
f/.i=f.i by A322,A324,FINSEQ_4:15;
then
A326: (f^mid(g,2,len g))/.i=f/.i by A322,A324,A325,FINSEQ_1:64;
A327: 1<=i+1 by A322,NAT_D:48;
then
A328: (f^mid(g,2,len g))/.((i+1))=(f^mid(g,2,len g)).(i+1) by A323,
FINSEQ_4:15;
A329: i+1<=len f by A324,NAT_1:13;
then
A330: (f^mid(g,2,len g)).(i+1)=f.(i+1) by A327,FINSEQ_1:64;
f/.(i+1)=f.(i+1) by A327,A329,FINSEQ_4:15;
hence thesis by A2,A322,A329,A326,A328,A330,TOPREAL1:def 5;
end;
case
A331: i>=len f;
1<=1+(i-'len f) by NAT_1:11;
then 1<=1+(i-len f) by A331,XREAL_1:233;
then 1<=1+i-len f;
then
A332: 1<=i+1-'len f by NAT_D:39;
A333: i<=len (f^mid(g,2,len g)) by A323,NAT_D:46;
A334: i-len f>=0 by A331,XREAL_1:48;
then
A335: i-'len f=i-len f by XREAL_0:def 2;
A336: now
assume 1>i-'len f;
then i-'len f+1<=0+1 by NAT_1:13;
then i-'len f=0 by XREAL_1:6;
hence (f^mid(g,2,len g)).i = g.(i-'len f+1) by A1,A61,A335,
FINSEQ_1:64;
end;
A337: i+1>=len f by A331,NAT_D:48;
then
A338: i+1-'len f+1=i+1-len f+1 by XREAL_1:233
.=i-len f+1+1
.=i-'len f+1+1 by A331,XREAL_1:233;
A339: i+1-len f<=len f+(len g-1)-len f by A6,A10,A323,XREAL_1:9;
then
A340: i-len f+1+1<=len g-1+1 by XREAL_1:6;
then
A341: i-'len f+1+1<=len g by A334,XREAL_0:def 2;
i-'len f<=i-'len f+1 by NAT_1:11;
then
A342: i-'len f<=len g-2+1 by A335,A339,XXREAL_0:2;
A343: now
assume
A344: 1<=i-'len f;
then 1<=i-len f by NAT_D:39;
then 1+len f<=i-len f +len f by XREAL_1:6;
then
A345: len f<i by NAT_1:13;
then (f^mid(g,2,len g)).i=mid(g,2,len g).(i-len f) by A333,
FINSEQ_6:108;
then (f^mid(g,2,len g)).i=mid(g,2,len g).(i-'len f) by A345,
XREAL_1:233;
then (f^mid(g,2,len g)).i=g.(i-'len f+2-1) by A8,A342,A344,
FINSEQ_6:122;
hence (f^mid(g,2,len g)).i=g.(i-'len f+1);
end;
1<=i+1 by A322,NAT_D:48;
then
A346: (f^mid(g,2,len g))/.(i+1)=(f^mid(g,2,len g)).(i+1) by A323,FINSEQ_4:15;
A347: 1<=i-'len f+1 by NAT_1:11;
i+1-len f<=len g-2+1 by A339;
then i+1-len f<=len g-'2+1 by A8,XREAL_1:233;
then
A348: i+1-'len f<=len g -'2+1 by A337,XREAL_1:233;
len f<(i+1) by A331,NAT_1:13;
then (f^mid(g,2,len g)).(i+1)=mid(g,2,len g).((i+1)-len f) by A323,
FINSEQ_6:108;
then (f^mid(g,2,len g)).(i+1)=mid(g,2,len g).((i+1)-'len f) by A337,
XREAL_1:233;
then
A349: (f^mid(g,2,len g)).(i+1)=g.((i+1)-'len f+2-1) by A8,A348,A332,
FINSEQ_6:122;
i-'len f+1+1<=len g by A334,A340,XREAL_0:def 2;
then
A350: g/.(i-'len f+1+1)=g.(i-'len f+1+1) by FINSEQ_4:15,NAT_1:11;
i-'len f+1<=len g by A335,A340,NAT_D:46;
then g/.(i-'len f+1)=g.(i-'len f+1) by FINSEQ_4:15,NAT_1:11;
then (f^mid(g,2,len g))/.i=g/.(i-'len f+1) by A322,A333,A343,A336,
FINSEQ_4:15;
hence thesis by A3,A347,A341,A338,A346,A350,A349,TOPREAL1:def 5;
end;
end;
hence thesis;
end;
then f^mid(g,2,len g) is unfolded s.n.c. special by A235,A62,TOPREAL1:def 5
,def 6,def 7;
hence thesis by A60,A7,TOPREAL1:def 8;
end;
theorem Th39:
for f,g being FinSequence of TOP-REAL 2 st f.len f=g.1 & f is
being_S-Seq & g is being_S-Seq & L~f /\ L~g={g.1} holds f^mid(g,2,len g)
is_S-Seq_joining f/.1,g/.len g
proof
let f,g be FinSequence of TOP-REAL 2;
assume that
A1: f.len f=g.1 and
A2: f is being_S-Seq and
A3: g is being_S-Seq and
A4: L~f /\ L~g={g.1};
A5: f^mid(g,2,len g) is being_S-Seq by A1,A2,A3,A4,Th38;
A6: len g >= 2 by A3,TOPREAL1:def 8;
then
A7: 1+1-1<=len g-1 by XREAL_1:9;
len f >= 2 by A2,TOPREAL1:def 8;
then
A8: 1<=len f by XXREAL_0:2;
then
A9: (f^mid(g,2,len g)).1=f.1 by FINSEQ_1:64
.=f/.1 by A8,FINSEQ_4:15;
A10: len (f^mid(g,2,len g))=len f + len mid(g,2,len g) by FINSEQ_1:22;
A11: 1<=len g by A6,XXREAL_0:2;
then
A12: len mid(g,2,len g)=len g -'2+1 by A6,FINSEQ_6:118;
then
A13: len mid(g,2,len g) =len g -2+1 by A6,XREAL_1:233
.=len g -1;
then
A14: len (mid(g,2,len g))+2-1=len g;
len g-1>=1+1-1 by A6,XREAL_1:9;
then len f+1<=len (f^mid(g,2,len g)) by A10,A13,XREAL_1:6;
then len f<len (f^mid(g,2,len g)) by NAT_1:13;
then (f^mid(g,2,len g)).(len (f^mid(g,2,len g))) =(mid(g,2,len g)).(len (f^
mid(g,2,len g))-len f) by FINSEQ_6:108
.=g.len g by A6,A10,A12,A7,A14,FINSEQ_6:122
.=g/.len g by A11,FINSEQ_4:15;
hence thesis by A5,A9;
end;
theorem
for f being FinSequence of TOP-REAL 2, n being Element of NAT holds L~
(f/^n) c= L~f
proof
let f be FinSequence of TOP-REAL 2, n be Element of NAT;
let x be object;
assume x in L~(f/^n);
then x in union { LSeg(f/^n,i) : 1 <= i & i+1 <= len (f/^n) } by
TOPREAL1:def 4;
then consider Y being set such that
A1: x in Y & Y in { LSeg(f/^n,i) : 1 <= i & i+1 <= len (f/^n) } by TARSKI:def 4
;
consider i such that
A2: Y= LSeg(f/^n,i) and
A3: 1 <= i and
A4: i+1 <= len (f/^n) by A1;
now
per cases;
case
n<=len f;
then LSeg(f/^n,i)=LSeg(f,n+i) by A3,SPPOL_2:4;
then Y c=L~f by A2,TOPREAL3:19;
hence thesis by A1;
end;
case
n>len f;
then f/^n=<*>(the carrier of TOP-REAL 2) by RFINSEQ:def 1;
hence contradiction by A4;
end;
end;
hence thesis;
end;
theorem Th41:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL
2 st p in L~f holds L~R_Cut(f,p) c= L~f
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2 such that
A1: p in L~f;
A2: 1<=Index(p,f) by A1,Th8;
len f <> 0 by A1,TOPREAL1:22;
then
A3: len f >= 0+1 by NAT_1:13;
A4: Index(p,f)<=len f by A1,Th8;
per cases;
suppose
p = f.1;
then R_Cut(f,p)=<*p*> by Def4;
then len R_Cut(f,p)=1 by FINSEQ_1:39;
then L~R_Cut(f,p) = {} by TOPREAL1:22;
hence thesis;
end;
suppose
A5: p<>f.1;
A6: f/.(Index(p,f)) in LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) by RLTOPSP1:68;
A7: len (mid(f,1,Index(p,f))) =Index(p,f)-'1+1 by A3,A2,A4,FINSEQ_6:118
.=Index(p,f) by A1,Th8,XREAL_1:235;
then (mid(f,1,Index(p,f)))<><*>(the carrier of TOP-REAL 2) by A2;
then
A8: L~(mid(f,1,Index(p,f))^<*p*>) = L~mid(f,1,Index(p,f)) \/ LSeg((mid(f,
1,Index(p,f))/.Index(p,f)),p) by A7,SPPOL_2:19;
mid(f,1,Index(p,f)) =(f/^(1-'1))|(Index(p,f)-'1+1) by A2,FINSEQ_6:def 3
.=(f/^(0))|(Index(p,f)-'1+1) by XREAL_1:232
.=f|(Index(p,f)-'1+1)
.=f|Index(p,f) by A1,Th8,XREAL_1:235;
then
A9: L~mid(f,1,Index(p,f)) c= L~f by TOPREAL3:20;
Index(p,f) < len f by A1,Th8;
then
A10: Index(p,f)+1<=len f by NAT_1:13;
then
A11: LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) c= L~f by A1,Th8,SPPOL_2:16;
p in LSeg(f,Index(p,f)) by A1,Th9;
then
A12: p in LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) by A2,A10,TOPREAL1:def 3;
(mid(f,1,Index(p,f)))/.Index(p,f)=mid(f,1,Index(p,f)).Index(p,f) by A2,A7,
FINSEQ_4:15
.=f.(Index(p,f)) by A2,A4,FINSEQ_6:123
.=f/.(Index(p,f)) by A1,A4,Th8,FINSEQ_4:15;
then
LSeg((mid(f,1,Index(p,f))/.Index(p,f)),p) c= LSeg(f/.(Index(p,f)),f/.
(Index(p,f)+1)) by A12,A6,TOPREAL1:6;
then
A13: LSeg((mid(f,1,Index(p,f))/.Index(p,f)),p)c= L~f by A11;
R_Cut(f,p)=mid(f,1,Index(p,f))^<*p*> by A5,Def4;
hence thesis by A8,A13,A9,XBOOLE_1:8;
end;
end;
Lm2: (<*>D)|i=<*>D
proof
len (<*>D)=0;
hence thesis by FINSEQ_1:58;
end;
Lm3: for f1 be FinSequence of D,k be Nat st 1<=k & k<=len f1 holds
mid(f1,k,k)=<*f1/.k*> & len mid(f1,k,k)=1
proof
let f1 be FinSequence of D,k be Nat;
assume that
A1: 1<=k and
A2: k<=len f1;
A3: f1/.k=f1.k by A1,A2,FINSEQ_4:15;
k-'1+1<=len f1 by A1,A2,XREAL_1:235;
then
A4: k-'1+1-(k-'1)<=len f1-(k-'1) by XREAL_1:9;
len (f1/^(k-'1))=len f1-'(k-'1) by RFINSEQ:29;
then
A5: 1<=len (f1/^(k-'1)) by A4,NAT_D:39;
k-'1+1=k by A1,XREAL_1:235;
then
A6: (f1/^(k-'1)).1=f1.k by A2,FINSEQ_6:114;
k-'k+1=k-k+1 by XREAL_1:233
.=1;
then mid(f1,k,k)=(f1/^(k-'1))|1 by FINSEQ_6:def 3
.=<*(f1/^(k-'1)).1*> by A5,CARD_1:27,FINSEQ_5:20;
hence thesis by A6,A3,FINSEQ_1:39;
end;
Lm4: for f1 be FinSequence of D holds mid(f1,0,0)=f1|1
proof
let f1 be FinSequence of D;
0-1<0;
then
A1: 0-'1=0 by XREAL_0:def 2;
0-'0+1=0-0+1 by XREAL_1:233
.=1;
then mid(f1,0,0)=(f1/^(0-'1))|1 by FINSEQ_6:def 3;
hence thesis by A1;
end;
Lm5: for f1 be FinSequence of D,k be Nat st len f1<k holds mid(f1,k
,k)=<*>D
proof
let f1 be FinSequence of D,k be Nat;
assume
A1: len f1<k;
then len f1+1<=k by NAT_1:13;
then
A2: len f1+1-1<=k-1 by XREAL_1:9;
0+1<=k by A1,NAT_1:13;
then len f1<=k-'1 by A2,XREAL_1:233;
then
A3: f1/^(k-'1)=<*>D by FINSEQ_5:32;
k-'k+1=k-k+1 by XREAL_1:233
.=1;
then mid(f1,k,k)=(f1/^(k-'1))|1 by FINSEQ_6:def 3;
hence thesis by A3,Lm2;
end;
Lm6: for f1 be FinSequence of D, i1,i2 holds mid(f1,i1,i2)=Rev mid(f1,i2,i1)
proof
let f1 be FinSequence of D;
let k1,k2 be Nat;
now
per cases;
case
A1: k1<=k2;
then
A2: mid(f1,k1,k2)=(f1/^(k1-'1))|(k2-'k1+1) by FINSEQ_6:def 3;
now
per cases by A1,XXREAL_0:1;
case
k1<k2;
then mid(f1,k2,k1)=Rev mid(f1,k1,k2) by A2,FINSEQ_6:def 3;
hence thesis;
end;
case
A3: k1=k2;
A4: k1=0 or 0+1<=k1 by NAT_1:13;
now
per cases by A4;
case
k1=0;
then
A5: mid(f1,k1,k2)=f1|1 by A3,Lm4;
now
per cases;
case
len f1=0;
then f1=<*>D;
then f1|1=<*>D by Lm2;
hence thesis by A3,A5;
end;
case
len f1<>0;
then f1 <> <*>D;
then f1|1=<*f1.1*> by FINSEQ_5:20;
hence thesis by A3,A5,FINSEQ_5:60;
end;
end;
hence thesis;
end;
case
1<=k1 & k1<= len f1;
then mid(f1,k1,k1)=<*f1/.k1*> by Lm3;
hence thesis by A3,FINSEQ_5:60;
end;
case
len f1<k1;
then mid(f1,k1,k1)=<*>D by Lm5;
hence thesis by A3;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
case
A6: k1>k2;
then mid(f1,k1,k2)=Rev ((f1/^(k2-'1))|(k1-'k2+1)) by FINSEQ_6:def 3;
hence thesis by A6,FINSEQ_6:def 3;
end;
end;
hence thesis;
end;
Lm7: for h being FinSequence of TOP-REAL 2,i1,i2 st 1<=i1 & i1<=len h & 1<=i2
& i2<=len h holds L~mid(h,i1,i2) c= L~h
proof
let h be FinSequence of TOP-REAL 2,i1,i2;
assume that
A1: 1<=i1 and
A2: i1<=len h and
A3: 1<=i2 and
A4: i2<=len h;
thus L~mid(h,i1,i2) c= L~h
proof
let x be object;
assume
A5: x in L~mid(h,i1,i2);
now
per cases;
case
A6: i1<=i2;
x in union { LSeg(mid(h,i1,i2),i) : 1 <= i & i+1 <= len mid(h,i1,
i2) } by A5,TOPREAL1:def 4;
then consider Y being set such that
A7: x in Y & Y in { LSeg(mid(h,i1,i2),i) : 1 <= i & i+1 <= len
mid(h,i1,i2) } by TARSKI:def 4;
consider i such that
A8: Y=LSeg(mid(h,i1,i2),i) and
A9: 1 <= i and
A10: i+1 <= len mid(h,i1,i2) by A7;
A11: LSeg(mid(h,i1,i2),i)=LSeg(mid(h,i1,i2)/.i,mid(h,i1,i2)/.(i+1)) by A9
,A10,TOPREAL1:def 3;
len mid(h,i1,i2)=i2-'i1+1 by A1,A2,A3,A4,A6,FINSEQ_6:118;
then i+1-1<=i2-'i1+1-1 by A10,XREAL_1:9;
then i<=i2-i1 by A6,XREAL_1:233;
then
A12: i+i1<=i2-i1+i1 by XREAL_1:6;
then
A13: i+i1<=len h by A4,XXREAL_0:2;
1+1<=i+i1 by A1,A9,XREAL_1:7;
then
A14: 1+1-1<=i+i1-1 by XREAL_1:9;
then 1<=i+i1-'1 by A1,NAT_1:12,XREAL_1:233;
then
A15: h/.(i+i1-'1)=h.(i+i1-'1) by A13,FINSEQ_4:15,NAT_D:44;
1<=i+1 by NAT_1:11;
then
A16: mid(h,i1,i2).(i+1)=h.(i+1+i1-'1) by A1,A2,A3,A4,A6,A10,FINSEQ_6:118;
A17: i+1+i1-'1=i+1+i1-1 by A1,NAT_1:12,XREAL_1:233
.=i+i1;
then
A18: i+1+i1-'1=i+i1-1+1 .=i+i1-'1+1 by A1,NAT_1:12,XREAL_1:233;
i<=i+1 by NAT_1:11;
then
A19: i<=len mid(h,i1,i2) by A10,XXREAL_0:2;
then
A20: mid(h,i1,i2)/.i=mid(h,i1,i2).i by A9,FINSEQ_4:15;
A21: mid(h,i1,i2)/.(i+1)=mid(h,i1,i2).(i+1) by A10,FINSEQ_4:15,NAT_1:11;
A22: i+i1<=len h by A4,A12,XXREAL_0:2;
mid(h,i1,i2).i=h.(i+i1-'1) by A1,A2,A3,A4,A6,A9,A19,FINSEQ_6:118;
then
LSeg(mid(h,i1,i2),i)=LSeg(h/.(i+i1-'1),h/.(i+1+i1-'1)) by A1,A11,A16
,A20,A21,A15,A17,A22,FINSEQ_4:15,NAT_1:12
.=LSeg(h,i+i1-'1) by A14,A13,A17,A18,TOPREAL1:def 3;
then LSeg(mid(h,i1,i2),i) in { LSeg(h,j) : 1 <= j & j+1 <= len h} by
A14,A17,A18,A22;
then x in union { LSeg(h,j) : 1 <= j & j+1 <= len h} by A7,A8,
TARSKI:def 4;
hence thesis by TOPREAL1:def 4;
end;
case
A23: i1>i2;
mid(h,i1,i2)=Rev mid(h,i2,i1) by Lm6;
then x in L~mid(h,i2,i1) by A5,SPPOL_2:22;
then
x in union { LSeg(mid(h,i2,i1),i) : 1 <= i & i+1 <= len mid(h,i2,
i1) } by TOPREAL1:def 4;
then consider Y being set such that
A24: x in Y & Y in { LSeg(mid(h,i2,i1),i) : 1 <= i & i+1 <= len
mid(h,i2,i1) } by TARSKI:def 4;
consider i such that
A25: Y=LSeg(mid(h,i2,i1),i) and
A26: 1 <= i and
A27: i+1 <= len mid(h,i2,i1) by A24;
A28: LSeg(mid(h,i2,i1),i)=LSeg(mid(h,i2,i1)/.i,mid(h,i2,i1)/.(i+1)) by A26
,A27,TOPREAL1:def 3;
len mid(h,i2,i1)=i1-'i2+1 by A1,A2,A3,A4,A23,FINSEQ_6:118;
then i+1-1<=i1-'i2+1-1 by A27,XREAL_1:9;
then i<=i1-i2 by A23,XREAL_1:233;
then
A29: i+i2<=i1-i2+i2 by XREAL_1:6;
then
A30: i+i2<=len h by A2,XXREAL_0:2;
1+1<=i+i2 by A3,A26,XREAL_1:7;
then
A31: 1+1-1<=i+i2-1 by XREAL_1:9;
then 1<=i+i2-'1 by A3,NAT_1:12,XREAL_1:233;
then
A32: h/.(i+i2-'1)=h.(i+i2-'1) by A30,FINSEQ_4:15,NAT_D:44;
1<=i+1 by NAT_1:11;
then
A33: mid(h,i2,i1).(i+1)=h.(i+1+i2-'1) by A1,A2,A3,A4,A23,A27,FINSEQ_6:118;
A34: i+1+i2-'1=i+1+i2-1 by A3,NAT_1:12,XREAL_1:233
.=i+i2;
then
A35: i+1+i2-'1=i+i2-1+1 .=i+i2-'1+1 by A3,NAT_1:12,XREAL_1:233;
i<=i+1 by NAT_1:11;
then
A36: i<=len mid(h,i2,i1) by A27,XXREAL_0:2;
then
A37: mid(h,i2,i1)/.i=mid(h,i2,i1).i by A26,FINSEQ_4:15;
A38: mid(h,i2,i1)/.(i+1)=mid(h,i2,i1).(i+1) by A27,FINSEQ_4:15,NAT_1:11;
A39: i+i2<=len h by A2,A29,XXREAL_0:2;
mid(h,i2,i1).i=h.(i+i2-'1) by A1,A2,A3,A4,A23,A26,A36,FINSEQ_6:118;
then
LSeg(mid(h,i2,i1),i)=LSeg(h/.(i+i2-'1),h/.(i+1+i2-'1)) by A3,A28,A33
,A37,A38,A32,A34,A39,FINSEQ_4:15,NAT_1:12
.=LSeg(h,i+i2-'1) by A31,A30,A34,A35,TOPREAL1:def 3;
then LSeg(mid(h,i2,i1),i) in { LSeg(h,j) : 1 <= j & j+1 <= len h} by
A31,A34,A35,A39;
then x in union { LSeg(h,j) : 1 <= j & j+1 <= len h} by A24,A25,
TARSKI:def 4;
hence thesis by TOPREAL1:def 4;
end;
end;
hence thesis;
end;
end;
Lm8: i in dom f & j in dom f implies len mid(f,i,j) >= 1
proof
A1: i <= j or j < i;
assume
A2: i in dom f;
then
A3: i <= len f by FINSEQ_3:25;
assume
A4: j in dom f;
then
A5: 1 <= j by FINSEQ_3:25;
A6: j <= len f by A4,FINSEQ_3:25;
1 <= i by A2,FINSEQ_3:25;
then len mid(f,i,j)=i-'j+1 or len mid(f,i,j)=j-'i+1
by A3,A5,A6,A1,FINSEQ_6:118;
hence thesis by NAT_1:11;
end;
Lm9: i in dom f & j in dom f implies mid(f,i,j) is non empty
proof
assume that
A1: i in dom f and
A2: j in dom f;
len mid(f,i,j) >= 1 by A1,A2,Lm8;
hence thesis;
end;
Lm10: i in dom f & j in dom f implies (mid(f,i,j))/.1 = f/.i
proof
assume
A1: i in dom f;
then
A2: 1 <= i by FINSEQ_3:25;
A3: i <= len f by A1,FINSEQ_3:25;
assume
A4: j in dom f;
then
A5: 1 <= j by FINSEQ_3:25;
A6: j <= len f by A4,FINSEQ_3:25;
mid(f,i,j) is non empty by A1,A4,Lm9;
then 1 in dom mid(f,i,j) by FINSEQ_5:6;
hence (mid(f,i,j))/.1 = mid(f,i,j).1 by PARTFUN1:def 6
.= f.i by A2,A3,A5,A6,FINSEQ_6:118
.= f/.i by A1,PARTFUN1:def 6;
end;
theorem Th42:
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
st p in L~f holds L~L_Cut(f,p) c= L~f
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2 such that
A1: p in L~f;
Index(p,f)<len f by A1,Th8;
then
A2: Index(p,f)+1<=len f by NAT_1:13;
A3: 1<=Index(p,f) by A1,Th8;
then
A4: 1<Index(p,f)+1 by NAT_1:13;
then
A5: Index(p,f)+1 in dom f by A2,FINSEQ_3:25;
len f <> 0 by A1,TOPREAL1:22;
then
A6: len f >= 0+1 by NAT_1:13;
then
A7: len f in dom f by FINSEQ_3:25;
per cases;
suppose
p = f.(Index(p,f)+1);
then L_Cut(f,p) = mid(f,Index(p,f)+1,len f) by Def3;
hence thesis by A6,A4,A2,Lm7;
end;
suppose
p <> f.(Index(p,f)+1);
then
A8: L_Cut(f,p) = <*p*>^mid(f,Index(p,f)+1,len f) by Def3;
A9: f/.(Index(p,f)+1) in LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) by RLTOPSP1:68
;
p in LSeg(f,Index(p,f)) by A1,Th9;
then
A10: p in LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) by A3,A2,TOPREAL1:def 3;
A11: LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) c= L~f by A1,A2,Th8,SPPOL_2:16;
mid(f,Index(p,f)+1,len f)/.1 = f/.(Index(p,f)+1) by A7,A5,Lm10;
then LSeg(p,mid(f,Index(p,f)+1,len f)/.1) c= LSeg(f/.(Index(p,f)),f/.(
Index(p,f)+1)) by A10,A9,TOPREAL1:6;
then
A12: LSeg(p,mid(f,Index(p,f)+1,len f)/.1) c= L~f by A11;
mid(f,Index(p,f)+1,len f) <> {} by A7,A5,Lm8,CARD_1:27;
then
A13: L~(<*p*>^mid(f,Index(p,f)+1,len f)) = LSeg(p,mid(f,Index(p,f)+1,len f
)/.1) \/ L~mid(f,Index(p,f)+1,len f) by SPPOL_2:20;
L~mid(f,Index(p,f)+1,len f) c= L~f by A6,A4,A2,Lm7;
hence thesis by A8,A13,A12,XBOOLE_1:8;
end;
end;
theorem Th43:
for f,g being FinSequence of TOP-REAL 2, p being Point of
TOP-REAL 2 st f.len f=g.1 & p in L~f & f is being_S-Seq & g is being_S-Seq & L~
f /\ L~g={g.1} & p<>f.len f holds L_Cut(f,p)^mid(g,2,len g) is_S-Seq_joining p,
g/.len g
proof
let f,g be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume that
A1: f.len f=g.1 and
A2: p in L~f and
A3: f is being_S-Seq and
A4: g is being_S-Seq and
A5: L~f /\ L~g={g.1} and
A6: p<>f.len f;
L_Cut(f,p) is_S-Seq_joining p,f/.len f by A2,A3,A6,Th33;
then
A7: L_Cut(f,p).(len L_Cut(f,p))=f/.len f;
A8: len g >= 2 by A4,TOPREAL1:def 8;
then
A9: 1<=len g by XXREAL_0:2;
g/.1 in LSeg(g/.1,g/.(1+1)) by RLTOPSP1:68;
then g/.1 in LSeg(g,1) by A8,TOPREAL1:def 3;
then g.1 in LSeg(g,1) by A9,FINSEQ_4:15;
then
A10: g.1 in L~g by SPPOL_2:17;
L~(L_Cut(f,p)) c= L~f by A2,Th42;
then
A11: L~(L_Cut(f,p))/\ L~g c= L~f /\ L~g by XBOOLE_1:27;
len f >= 2 by A3,TOPREAL1:def 8;
then
A12: 1<=len f by XXREAL_0:2;
A13: L_Cut(f,p) is being_S-Seq by A2,A3,A6,Th34;
then
A14: 1+1<=len L_Cut(f,p) by TOPREAL1:def 8;
then
A15: 1+1-1<=len L_Cut(f,p)-1 by XREAL_1:9;
A16: 1<=len L_Cut(f,p) by A14,XXREAL_0:2;
then L_Cut(f,p).1=(L_Cut(f,p))/.1 by FINSEQ_4:15;
then
A17: (L_Cut(f,p))/.(1)=p by A2,Th23;
A18: len L_Cut(f,p)-'1+1=len L_Cut(f,p) by A14,XREAL_1:235,XXREAL_0:2;
then
(L_Cut(f,p))/.(len L_Cut(f,p)) in LSeg((L_Cut(f,p))/.(len L_Cut(f,p) -'
1), (L_Cut(f,p))/.(len L_Cut(f,p)-'1+1)) by RLTOPSP1:68;
then L_Cut(f,p).len L_Cut(f,p) in LSeg((L_Cut(f,p))/.(len L_Cut(f,p)-'1), (
L_Cut(f,p))/.(len L_Cut(f,p)-'1+1)) by A16,FINSEQ_4:15;
then
L_Cut(f,p).len L_Cut(f,p) in LSeg(L_Cut(f,p),len L_Cut(f,p)-'1) by A15,A18,
TOPREAL1:def 3;
then f/.len f in L~(L_Cut(f,p)) by A7,SPPOL_2:17;
then f.len f in L~(L_Cut(f,p)) by A12,FINSEQ_4:15;
then g.1 in L~(L_Cut(f,p))/\ L~g by A1,A10,XBOOLE_0:def 4;
then {g.1}c= L~(L_Cut(f,p))/\ L~g by ZFMISC_1:31;
then L~(L_Cut(f,p))/\ L~g={g.1} by A5,A11,XBOOLE_0:def 10;
hence thesis by A1,A4,A12,A13,A7,A17,Th39,FINSEQ_4:15;
end;
theorem
for f,g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2
st f.len f=g.1 & p in L~f & f is being_S-Seq & g is being_S-Seq & L~f /\ L~g={g
.1} & p<>f.len f holds L_Cut(f,p)^mid(g,2,len g) is being_S-Seq
proof
let f,g be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume that
A1: f.len f=g.1 and
A2: p in L~f and
A3: f is being_S-Seq and
A4: g is being_S-Seq and
A5: L~f /\ L~g={g.1} and
A6: p<>f.len f;
L_Cut(f,p)^mid(g,2,len g) is_S-Seq_joining p,g/.len g by A1,A2,A3,A4,A5,A6
,Th43;
hence thesis;
end;
theorem Th45:
for f,g being FinSequence of TOP-REAL 2 st f.len f=g.1 & f is
being_S-Seq & g is being_S-Seq & L~f /\ L~g={g.1} holds mid(f,1,len f-'1)^g is
being_S-Seq
proof
let f,g be FinSequence of TOP-REAL 2;
assume that
A1: f.len f=g.1 and
A2: f is being_S-Seq and
A3: g is being_S-Seq and
A4: L~f /\ L~g={g.1};
A5: Rev f is being_S-Seq by A2;
L~(Rev f)=L~f by SPPOL_2:22;
then
A6: L~(Rev g)/\ L~(Rev f)={g.1} by A4,SPPOL_2:22;
A7: (Rev f).1=f.len f by FINSEQ_5:62;
A8: Rev g is being_S-Seq by A3;
(Rev g).len (Rev g)=(Rev Rev g).1 by FINSEQ_5:62
.=(Rev f).1 by A1,A7;
then
A9: (Rev g)^(mid(Rev f,2,len (Rev f))) is being_S-Seq by A1,A5,A8,A6,A7,Th38;
A10: len f-'1<=len f by NAT_D:50;
A11: len (Rev f)=len f by FINSEQ_5:def 3;
A12: len f >= 2 by A2,TOPREAL1:def 8;
then
A13: len f-1>=1+1-1 by XREAL_1:9;
A14: len f-'1+1=len f-1+1 by A12,XREAL_1:233,XXREAL_0:2
.=len f;
A15: len f-'(len f-'1)+1=len f-(len f-'1)+1 by NAT_D:50,XREAL_1:233
.=len f-(len f-1)+1 by A12,XREAL_1:233,XXREAL_0:2
.=2;
1<=len f by A12,XXREAL_0:2;
then (Rev g)^(Rev mid(f,1,len f-'1)) is being_S-Seq by A13,A10,A15,A11,A14,A9
,FINSEQ_6:113;
then Rev (mid(f,1,len f-'1)^g) is being_S-Seq by FINSEQ_5:64;
then Rev Rev (mid(f,1,len f-'1)^g) is being_S-Seq;
hence thesis;
end;
theorem Th46:
for f,g being FinSequence of TOP-REAL 2 st f.len f=g.1 & f is
being_S-Seq & g is being_S-Seq & L~f /\ L~g={g.1} holds mid(f,1,len f-'1)^g
is_S-Seq_joining f/.1,g/.len g
proof
let f,g be FinSequence of TOP-REAL 2;
assume that
A1: f.len f=g.1 and
A2: f is being_S-Seq and
A3: g is being_S-Seq and
A4: L~f /\ L~g={g.1};
A5: len f-'1<=len f by NAT_D:50;
A6: len f >= 2 by A2,TOPREAL1:def 8;
then 1+1-1<=len f-1 by XREAL_1:9;
then
A7: 1<=len f-'1 by NAT_D:39;
A8: 1<=len f by A6,XXREAL_0:2;
then len mid(f,1,len f-'1)=len f-'1-'1+1 by A5,A7,FINSEQ_6:118
.=len f-'1 -1+1 by A7,XREAL_1:233
.=len f -'1;
then
A9: (mid(f,1,len f-'1)^g).1=mid(f,1,len f-'1).1 by A7,FINSEQ_1:64
.=f.1 by A5,A7,FINSEQ_6:123
.=f/.1 by A8,FINSEQ_4:15;
A10: len (mid(f,1,len f-'1)^g)=len (mid(f,1,len f-'1)) + len g by FINSEQ_1:22;
A11: len g >= 2 by A3,TOPREAL1:def 8;
then
A12: 1<=len g by XXREAL_0:2;
0+len (mid(f,1,len f-'1))<len g+len (mid(f,1,len f-'1)) by A11,XREAL_1:6;
then
A13: (mid(f,1,len f-'1)^g).(len (mid(f,1,len f-'1)^g)) =g.(len (mid(f,1,len
f-'1)^g)-len (mid(f,1,len f-'1))) by A10,FINSEQ_6:108
.=g/.len g by A12,A10,FINSEQ_4:15;
mid(f,1,len f-'1)^g is being_S-Seq by A1,A2,A3,A4,Th45;
hence thesis by A9,A13;
end;
theorem Th47:
for f,g being FinSequence of TOP-REAL 2, p being Point of
TOP-REAL 2 st f.len f=g.1 & p in L~g & f is being_S-Seq & g is being_S-Seq & L~
f /\ L~g={g.1} & p<>g.1 holds mid(f,1,len f -'1)^R_Cut(g,p) is_S-Seq_joining f
/.1,p
proof
let f,g be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume that
A1: f.len f=g.1 and
A2: p in L~g and
A3: f is being_S-Seq and
A4: g is being_S-Seq and
A5: L~f /\ L~g={g.1} and
A6: p<>g.1;
len g >= 2 by A4,TOPREAL1:def 8;
then
A7: 1<=len g by XXREAL_0:2;
R_Cut(g,p) is_S-Seq_joining g/.1,p by A2,A4,A6,Th32;
then
A8: R_Cut(g,p).1=g/.1;
then
A9: R_Cut(g,p).1=f.len f by A1,A7,FINSEQ_4:15;
A10: len f >= 2 by A3,TOPREAL1:def 8;
then
A11: 1<=len f by XXREAL_0:2;
A12: 1+1-1<=len f-1 by A10,XREAL_1:9;
A13: len f-'1+1=len f by A10,XREAL_1:235,XXREAL_0:2;
then f/.len f in LSeg(f/.(len f-'1),f/.(len f-'1+1)) by RLTOPSP1:68;
then f/.len f in LSeg(f,len f-'1) by A12,A13,TOPREAL1:def 3;
then f.len f in LSeg(f,len f-'1) by A11,FINSEQ_4:15;
then
A14: f.len f in L~f by SPPOL_2:17;
A15: R_Cut(g,p) is being_S-Seq by A2,A4,A6,Th35;
then
A16: 1+1<=len R_Cut(g,p) by TOPREAL1:def 8;
then
A17: 1<=len R_Cut(g,p) by XXREAL_0:2;
then R_Cut(g,p).len R_Cut(g,p)=(R_Cut(g,p))/.(len R_Cut(g,p)) by FINSEQ_4:15;
then
A18: (R_Cut(g,p))/.(len R_Cut(g,p))=p by A2,Th24;
(R_Cut(g,p))/.(1) in LSeg((R_Cut(g,p))/.(1), (R_Cut(g,p))/.(1+1)) by
RLTOPSP1:68;
then R_Cut(g,p).1 in LSeg((R_Cut(g,p))/.(1),(R_Cut(g,p))/.(1+1)) by A17,
FINSEQ_4:15;
then R_Cut(g,p).1 in LSeg(R_Cut(g,p),1) by A16,TOPREAL1:def 3;
then g/.1 in L~(R_Cut(g,p)) by A8,SPPOL_2:17;
then g.1 in L~(R_Cut(g,p)) by A7,FINSEQ_4:15;
then f.len f in L~f /\ L~R_Cut(g,p) by A1,A14,XBOOLE_0:def 4;
then
A19: {f.len f}c= L~f /\ L~R_Cut(g,p) by ZFMISC_1:31;
L~(R_Cut(g,p)) c= L~g by A2,Th41;
then L~f /\ L~R_Cut(g,p) c= L~f /\ L~g by XBOOLE_1:27;
then L~f /\ L~R_Cut(g,p)={R_Cut(g,p).1} by A1,A5,A9,A19,XBOOLE_0:def 10;
hence thesis by A3,A15,A9,A18,Th46;
end;
theorem
for f,g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2
st f.len f=g.1 & p in L~g & f is being_S-Seq & g is being_S-Seq & L~f /\ L~g={g
.1} & p<>g.1 holds mid(f,1,len f -'1)^R_Cut(g,p) is being_S-Seq
proof
let f,g be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume that
A1: f.len f=g.1 and
A2: p in L~g and
A3: f is being_S-Seq and
A4: g is being_S-Seq and
A5: L~f /\ L~g={g.1} and
A6: p<>g.1;
mid(f,1,len f -'1)^R_Cut(g,p) is_S-Seq_joining f/.1,p by A1,A2,A3,A4,A5,A6
,Th47;
hence thesis;
end;