:: More on the Finite Sequences on the Plane
:: by Andrzej Trybulec
::
:: Received October 25, 2001
:: Copyright (c) 2001-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, TARSKI, XBOOLE_0, ZFMISC_1, FUNCT_1, GOBOARD1, SUBSET_1,
FINSEQ_1, ARYTM_3, XXREAL_0, FINSEQ_6, RELAT_1, PARTFUN1, FINSEQ_4,
CARD_1, ORDINAL4, RFINSEQ, NAT_1, GRAPH_2, MATRIX_1, ARYTM_1, FINSEQ_5,
EUCLID, RLTOPSP1, TOPREAL1, GOBOARD5, STRUCT_0, MCART_1, SETFAM_1,
PRE_TOPC;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
NAT_D, SETFAM_1, FUNCT_1, PARTFUN1, FINSEQ_5, FINSEQ_6, RFINSEQ, GRAPH_2,
MATRIX_0, RELSET_1, FINSEQ_1, ZFMISC_1, STRUCT_0, PRE_TOPC, RLTOPSP1,
EUCLID, TOPREAL1, GOBOARD1, GOBOARD5, FINSEQ_4, XXREAL_0;
constructors SETFAM_1, REAL_1, FINSEQ_4, RFINSEQ, NAT_D, FINSEQ_5, REALSET2,
GOBOARD1, GOBOARD5, GRAPH_2, SPRECT_1, RELSET_1;
registrations XBOOLE_0, ORDINAL1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1,
FINSEQ_5, FINSEQ_6, STRUCT_0, SPPOL_2, GOBOARD9, SPRECT_1, REVROT_1,
CARD_1, FUNCT_1, RELAT_1, EUCLID;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions FINSEQ_6, GOBOARD1, GOBOARD5, TOPREAL1, TARSKI;
equalities TOPREAL1;
expansions GOBOARD1, TOPREAL1, TARSKI;
theorems GRAPH_2, FINSEQ_3, NAT_1, FINSEQ_5, TOPREAL1, FINSEQ_1, TARSKI,
FUNCT_1, FINSEQ_4, ZFMISC_1, PARTFUN2, FINSEQ_6, RELAT_1, RFINSEQ, INT_1,
MSSCYC_1, REVROT_1, GOBOARD2, TOPREAL3, GOBOARD3, SPPOL_2, GOBOARD5,
GOBOARD7, ENUMSET1, SETFAM_1, XBOOLE_0, XBOOLE_1, XREAL_1, CARD_1,
XXREAL_0, PARTFUN1, NAT_D, SEQM_3;
begin
theorem Th1:
for A,x,y being set st A c= {x,y} & x in A & not y in A holds A = {x}
proof
let A,x,y be set such that
A1: A c= {x,y} and
A2: x in A and
A3: not y in A;
per cases by A1,ZFMISC_1:36;
suppose
A = {};
hence thesis by A2;
end;
suppose
A = {x};
hence thesis;
end;
suppose
A = {y};
hence thesis by A3,TARSKI:def 1;
end;
suppose
A = {x,y};
hence thesis by A3,TARSKI:def 2;
end;
end;
registration
cluster trivial for Function;
existence
proof
take {};
thus thesis;
end;
end;
begin :: FinSequences
reserve G for Go-board,
i,j,k,m,n for Nat;
registration
cluster non constant for FinSequence;
existence
proof
set f = the non constant FinSequence;
take f;
thus thesis;
end;
end;
theorem Th2:
for f being non trivial FinSequence holds 1 < len f
proof
let f be non trivial FinSequence;
1+1 <= len f by NAT_D:60;
hence thesis by NAT_1:13;
end;
theorem Th3:
for D being non trivial set for f being non constant circular
FinSequence of D holds len f > 2
proof
let D be non trivial set;
let f be non constant circular FinSequence of D;
assume
A1: len f <= 2;
per cases by A1,XXREAL_0:1;
suppose
len f < 1+1;
then len f <= 1 by NAT_1:13;
then reconsider f as trivial Function by Th2;
f is constant;
hence contradiction;
end;
suppose
A2: len f = 2;
then
A3: dom f = {1,2} by FINSEQ_1:2,def 3;
for n,m being Nat st n in dom f & m in dom f holds f.n=f.m
proof
let n,m be Nat such that
A4: n in dom f and
A5: m in dom f;
per cases by A3,A4,A5,TARSKI:def 2;
suppose
n = 1 & m = 1 or n = 2 & m = 2;
hence thesis;
end;
suppose that
A6: n = 1 and
A7: m = 2;
A8: m in dom f by A3,A7,TARSKI:def 2;
n in dom f by A3,A6,TARSKI:def 2;
hence f.n = f/.1 by A6,PARTFUN1:def 6
.= f/.len f by FINSEQ_6:def 1
.= f.m by A2,A7,A8,PARTFUN1:def 6;
end;
suppose that
A9: n = 2 and
A10: m = 1;
A11: n in dom f by A3,A9,TARSKI:def 2;
m in dom f by A3,A10,TARSKI:def 2;
hence f.m = f/.1 by A10,PARTFUN1:def 6
.= f/.len f by FINSEQ_6:def 1
.= f.n by A2,A9,A11,PARTFUN1:def 6;
end;
end;
hence contradiction by SEQM_3:def 10;
end;
end;
theorem Th4:
for f being FinSequence, x being set holds x in rng f or x..f = 0
proof
let f be FinSequence, x be set;
assume
A1: not x in rng f;
A2: now
assume f " {x} <> {};
then consider y being object such that
A3: y in f " {x} by XBOOLE_0:def 1;
f.y in {x} by A3,FUNCT_1:def 7;
then
A4: f.y = x by TARSKI:def 1;
y in dom f by A3,FUNCT_1:def 7;
hence contradiction by A1,A4,FUNCT_1:3;
end;
thus x..f = Sgm(f " {x}).1 by FINSEQ_4:def 4
.= 0 by A2,FINSEQ_3:43;
end;
theorem Th5:
for p being set, D being non empty set for f being non empty
FinSequence of D for g being FinSequence of D st p..f = len f holds (f^g)|--p =
g
proof
let p be set, D be non empty set;
let f being non empty FinSequence of D;
let g being FinSequence of D such that
A1: p..f = len f;
A2: p in rng f by A1,Th4;
then
A3: p..(f^g) = len f by A1,FINSEQ_6:6;
rng f c= rng(f^g) by FINSEQ_1:29;
hence (f^g) |-- p = (f^g)/^(p..(f^g)) by A2,FINSEQ_5:35
.= g by A3;
end;
theorem Th6:
for D being non empty set for f being non empty one-to-one
FinSequence of D holds f/.len f..f = len f
proof
let D be non empty set;
let f be non empty one-to-one FinSequence of D;
A1: len f in dom f by FINSEQ_5:6;
A2: for i being Nat st 1 <= i & i < len f holds f.i <> f.len f
proof
let i be Nat such that
A3: 1 <= i and
A4: i < len f;
i in dom f by A3,A4,FINSEQ_3:25;
hence thesis by A1,A4,FUNCT_1:def 4;
end;
f/.len f = f.len f by A1,PARTFUN1:def 6;
hence thesis by A1,A2,FINSEQ_6:2;
end;
theorem Th7:
for f,g being FinSequence holds len f <= len(f^'g)
proof
let f,g be FinSequence;
f ^' g = f^(2, len g)-cut g by FINSEQ_6:def 5;
then len(f^'g) = len f + len(2, len g)-cut g by FINSEQ_1:22;
hence thesis by NAT_1:11;
end;
theorem Th8:
for f,g being FinSequence for x being set st x in rng f holds x..
f = x..(f^'g)
proof
let f,g be FinSequence, x be set;
assume
A1: x in rng f;
then
A2: f.(x..f) = x by FINSEQ_4:19;
A3: x..f in dom f by A1,FINSEQ_4:20;
then
A4: x..f <= len f by FINSEQ_3:25;
A5: for i being Nat st 1 <= i & i < x..f holds (f^'g).i <> x
proof
let i be Nat such that
A6: 1 <= i and
A7: i < x..f;
A8: i < len f by A4,A7,XXREAL_0:2;
then
A9: i in dom f by A6,FINSEQ_3:25;
(f^'g).i = f.i by A6,A8,FINSEQ_6:140;
hence thesis by A7,A9,FINSEQ_4:24;
end;
len f <= len(f^'g) by Th7;
then
A10: dom f c= dom(f^'g) by FINSEQ_3:30;
1 <= x..f by A3,FINSEQ_3:25;
then (f^'g).(x..f) = x by A2,A4,FINSEQ_6:140;
hence thesis by A3,A10,A5,FINSEQ_6:2;
end;
theorem
for f being non empty FinSequence for g being FinSequence holds len g
<= len(f^'g)
proof
let f be non empty FinSequence, g be FinSequence;
per cases;
suppose
g = {};
hence thesis;
end;
suppose
A1: g <> {};
A2: len f >= 1 by NAT_1:14;
len (f^'g) +1 = len f + len g by A1,FINSEQ_6:139;
then len (f^'g) +1 >= 1 + len g by A2,XREAL_1:6;
hence thesis by XREAL_1:6;
end;
end;
theorem Th10:
for f,g being FinSequence holds rng f c= rng(f^'g)
proof
let f,g be FinSequence;
f^'g = f^(2, len g)-cut g by FINSEQ_6:def 5;
hence thesis by FINSEQ_1:29;
end;
theorem Th11:
for D being non empty set for f being non empty FinSequence of D
for g being non trivial FinSequence of D st g/.len g = f/.1 holds f^'g is
circular
proof
let D be non empty set;
let f be non empty FinSequence of D, g be non trivial FinSequence of D;
assume g/.len g = f/.1;
hence (f^'g)/.1 = g/.len g by FINSEQ_6:155
.= (f^'g)/.len(f^'g) by FINSEQ_6:156;
end;
theorem Th12:
for D being non empty set for M being Matrix of D for f being
FinSequence of D for g being non empty FinSequence of D st f/.len f = g/.1 & f
is_sequence_on M & g is_sequence_on M holds f^'g is_sequence_on M
proof
let D be non empty set;
let M be Matrix of D;
let f be FinSequence of D;
let g be non empty FinSequence of D such that
A1: f/.len f = g/.1 and
A2: f is_sequence_on M and
A3: g is_sequence_on M;
A4: len (f^'g) +1 = len f + len g by FINSEQ_6:139;
thus for n st n in dom(f^'g) ex i,j st [i,j] in Indices M & (f^'g)/.n = M*(i
,j)
proof
let n such that
A5: n in dom(f^'g);
per cases;
suppose
A6: n <= len f;
A7: 1 <= n by A5,FINSEQ_3:25;
then n in dom f by A6,FINSEQ_3:25;
then consider i,j such that
A8: [i,j] in Indices M and
A9: f/.n = M*(i,j) by A2;
take i,j;
thus [i,j] in Indices M by A8;
thus thesis by A6,A7,A9,FINSEQ_6:159;
end;
suppose
A10: n > len f;
then consider k be Nat such that
A11: n = len f + k by NAT_1:10;
reconsider k as Nat;
A12: 1 <= k+1 by NAT_1:11;
n <= len(f^'g) by A5,FINSEQ_3:25;
then n < len f + len g by A4,NAT_1:13;
then
A13: k < len g by A11,XREAL_1:6;
then k+1 <= len g by NAT_1:13;
then k+1 in dom g by A12,FINSEQ_3:25;
then consider i,j such that
A14: [i,j] in Indices M and
A15: g/.(k+1) = M*(i,j) by A3;
take i,j;
thus [i,j] in Indices M by A14;
len f + 1 <= n by A10,NAT_1:13;
then 1 <= k by A11,XREAL_1:6;
hence thesis by A11,A13,A15,FINSEQ_6:160;
end;
end;
let n such that
A16: n in dom(f^'g) and
A17: n+1 in dom(f^'g);
let m,k,i,j such that
A18: [m,k] in Indices M and
A19: [i,j] in Indices M and
A20: (f^'g)/.n = M*(m,k) and
A21: (f^'g)/.(n+1) = M*(i,j);
per cases by XXREAL_0:1;
suppose
A22: n < len f;
then
A23: n+1 <= len f by NAT_1:13;
then
A24: f/.(n+1) = M*(i,j) by A21,FINSEQ_6:159,NAT_1:11;
A25: 1 <= n by A16,FINSEQ_3:25;
then
A26: n in dom f by A22,FINSEQ_3:25;
1 <= n+1 by NAT_1:11;
then
A27: n+1 in dom f by A23,FINSEQ_3:25;
f/.n = M*(m,k) by A20,A22,A25,FINSEQ_6:159;
hence thesis by A2,A18,A19,A26,A27,A24;
end;
suppose
A28: n > len f;
then consider k0 being Nat such that
A29: n = len f + k0 by NAT_1:10;
reconsider k0 as Nat;
A30: 1 <= k0+1 by NAT_1:11;
n <= len(f^'g) by A16,FINSEQ_3:25;
then n < len f + len g by A4,NAT_1:13;
then
A31: k0 < len g by A29,XREAL_1:6;
then k0+1 <= len g by NAT_1:13;
then
A32: k0+1 in dom g by A30,FINSEQ_3:25;
A33: 1 <= k0+1+1 by NAT_1:11;
n+1 <= len(f^'g) by A17,FINSEQ_3:25;
then len f + (k0+1) < len f + len g by A4,A29,NAT_1:13;
then
A34: k0+1 < len g by XREAL_1:6;
then k0+1+1 <= len g by NAT_1:13;
then
A35: k0+1+1 in dom g by A33,FINSEQ_3:25;
len f + 1 <= n by A28,NAT_1:13;
then 1 <= k0 by A29,XREAL_1:6;
then
A36: g/.(k0+1) = M*(m,k) by A20,A29,A31,FINSEQ_6:160;
g/.(k0+1+1) = (f^'g)/.(len f +(k0+1)) by A34,FINSEQ_6:160,NAT_1:11
.= M*(i,j) by A21,A29;
hence thesis by A3,A18,A19,A32,A35,A36;
end;
suppose
A37: n = len f;
n+1 <= len(f^'g) by A17,FINSEQ_3:25;
then len f + 1 < len f + len g by A4,A37,NAT_1:13;
then
A38: 1 < len g by XREAL_1:6;
then 1+1 <= len g by NAT_1:13;
then
A39: 1+1 in dom g by FINSEQ_3:25;
1 <= n by A16,FINSEQ_3:25;
then
A40: g/.1 = M*(m,k) by A1,A20,A37,FINSEQ_6:159;
A41: 1 in dom g by FINSEQ_5:6;
g/.(1+1) = M*(i,j) by A21,A37,A38,FINSEQ_6:160;
hence thesis by A3,A18,A19,A40,A39,A41;
end;
end;
Lm1: for p be FinSequence, m, n be Nat st 1<=m & m<=n+1 & n<=len p
holds len (m, n)-cut p +m = n+1 & for i being Nat st i<len (m, n)
-cut p holds ((m, n)-cut p).(i+1)=p.(m+i)
proof
let p be FinSequence, m, n be Nat such that
A1: 1<=m and
A2: m<=n+1 and
A3: n<=len p;
A4: m = n+1 or m < n+1 by A2,XXREAL_0:1;
per cases by A4,NAT_1:13;
suppose
A5: m = n+1;
then n < m by XREAL_1:29;
then (m, n)-cut p = {} by FINSEQ_6:def 4;
hence len (m, n)-cut p +m = n+1 by A5;
not(1<=m & m<=n & n<=len p) by A5,XREAL_1:29;
hence thesis by CARD_1:27,FINSEQ_6:def 4;
end;
suppose
m<=n;
hence thesis by A1,A3,FINSEQ_6:def 4;
end;
end;
theorem Th13:
for D being set, f being FinSequence of D st 1 <= k holds
(k+1,len f)-cut f = f/^k
proof
let D be set, f being FinSequence of D such that
A1: 1 <= k;
per cases;
suppose
A2: len f < k;
k <= k+1 by NAT_1:11;
then len f < k+1 by A2,XXREAL_0:2;
hence (k+1, len f)-cut f = {} by FINSEQ_6:def 4
.= f/^k by A2,FINSEQ_5:32;
end;
suppose
A3: f = {};
then
A4: len f = 0;
thus (k+1, len f)-cut f = <*>D by A3,FINSEQ_6:def 4
.= f/^k by A1,A4,RFINSEQ:def 1;
end;
suppose that
A5: k <= len f;
set IT = (k+1, len f)-cut f;
A6: 1 <= k+1 by NAT_1:11;
A7: k+1 <= len f + 1 by A5,XREAL_1:6;
A8: for m be Nat st m in dom IT holds IT.m = f.(m+k)
proof
let m be Nat such that
A9: m in dom IT;
1 <= m by A9,FINSEQ_3:25;
then consider i be Nat such that
A10: m = 1+i by NAT_1:10;
reconsider i as Nat;
m <= len IT by A9,FINSEQ_3:25;
then i < len IT by A10,NAT_1:13;
hence IT.m = f.(k+1+i) by A6,A7,A10,Lm1
.= f.(m+k) by A10;
end;
len f + 1 = len IT + (k+1) by A6,A7,Lm1
.= len IT + k+1;
then len IT = len f - k;
hence thesis by A5,A8,RFINSEQ:def 1;
end;
end;
theorem Th14:
for D being set, f being FinSequence of D st k <= len f holds (1
, k)-cut f = f|k
proof
let D be set, f being FinSequence of D such that
A1: k <= len f;
per cases;
suppose
A2: 0+1 > k;
A3: f|0 = {};
k = 0 by A2,NAT_1:13;
hence thesis by A3,FINSEQ_6:def 4;
end;
suppose
A4: 1 <= k;
A5: len(f|k)+1 = k+1 by A1,FINSEQ_1:59;
for i being Nat st i<len(f|k) holds (f|k).(i+1)= f.(1+i)
proof
let i be Nat;
assume i<len(f|k);
then i+1 <= k by A5,NAT_1:13;
hence thesis by FINSEQ_3:112;
end;
hence thesis by A1,A4,A5,FINSEQ_6:def 4;
end;
end;
theorem Th15:
for p being set, D being non empty set for f being non empty
FinSequence of D for g being FinSequence of D st p..f = len f holds (f^g)-|p =
(1,len f -' 1)-cut f
proof
let p be set, D be non empty set, f be non empty FinSequence of D, g be
FinSequence of D such that
A1: p..f = len f;
p in rng f by A1,Th4;
then
A2: p..(f^g) = p..f by FINSEQ_6:6;
reconsider i = len f - 1 as Element of NAT by INT_1:5,NAT_1:14;
A3: len f -' 1 = i by NAT_1:14,XREAL_1:233;
len(f^g) = len f + len g by FINSEQ_1:22;
then
A4: len f <= len(f^g) by NAT_1:11;
rng f c= rng(f^g) by FINSEQ_1:29;
hence (f^g)-|p = (f^g)|Seg i by A1,A2,Th4,FINSEQ_4:33
.= (f^g)|i by FINSEQ_1:def 16
.= (1,len f -' 1)-cut(f^g) by A4,A3,Th14,NAT_D:44
.= (1,len f -' 1)-cut f by MSSCYC_1:2,NAT_D:44;
end;
theorem Th16:
for D being non empty set for f,g being non empty FinSequence of
D st g/.1..f = len f holds (f^'g:-g/.1) = g
proof
let D be non empty set;
let f,g be non empty FinSequence of D such that
A1: g/.1..f = len f;
A2: g/.1 in rng f by A1,Th4;
A3: 1 <= len g by NAT_1:14;
A4: f^'g = f^(2, len g)-cut g by FINSEQ_6:def 5;
then rng f c= rng(f^'g) by FINSEQ_1:29;
hence (f^'g:-g/.1) = <*g/.1*>^(f^'g |-- g/.1) by A2,FINSEQ_6:41
.= <*g/.1*>^(2, len g)-cut g by A1,A4,Th5
.= <*g.1*>^(2, len g)-cut g by A3,FINSEQ_4:15
.= ((1,1)-cut g)^(1+1, len g)-cut g by A3,FINSEQ_6:132
.= g by FINSEQ_6:135,NAT_1:14;
end;
theorem Th17:
for D being non empty set for f,g being non empty FinSequence of
D st g/.1..f = len f holds (f^'g-:g/.1) = f
proof
let D be non empty set;
let f,g be non empty FinSequence of D such that
A1: g/.1..f = len f;
A2: g/.1 in rng f by A1,Th4;
g/.1 in rng f by A1,Th4;
then
A3: g/.1 = f.len f by A1,FINSEQ_4:19;
A4: 1 <= len f by NAT_1:14;
A5: len f -' 1 + 1 = len f by NAT_1:14,XREAL_1:235;
A6: f^'g = f^(2, len g)-cut g by FINSEQ_6:def 5;
then rng f c= rng(f^'g) by FINSEQ_1:29;
hence (f^'g-:g/.1) = (f^'g -| g/.1)^<*g/.1*> by A2,FINSEQ_6:40
.= ((1, len f -' 1)-cut f)^<*g/.1*> by A1,A6,Th15
.= ((1, len f -' 1)-cut f)^((len f,len f)-cut f) by A4,A3,FINSEQ_6:132
.= f by A5,FINSEQ_6:135,NAT_D:44;
end;
theorem Th18:
for D being non trivial set for f being non empty FinSequence of
D for g being non trivial FinSequence of D st g/.1 = f/.len f & for i st 1 <= i
& i < len f holds f/.i <> g/.1 holds Rotate(f^'g,g/.1) = g^'f
proof
let D be non trivial set;
let f being non empty FinSequence of D;
let g being non trivial FinSequence of D such that
A1: g/.1 = f/.len f and
A2: for i st 1 <= i & i < len f holds f/.i <> g/.1;
A3: g/.1 in rng f by A1,FINSEQ_6:168;
A4: len f in dom f by FINSEQ_5:6;
then
A5: f.len f = f/.len f by PARTFUN1:def 6;
for i being Nat st 1 <= i & i < len f holds f.i <> f.len f
proof
let i be Nat such that
A6: 1 <= i and
A7: i < len f;
f.i = f/.i by A6,A7,FINSEQ_4:15;
hence thesis by A1,A2,A5,A6,A7;
end;
then
A8: g/.1..f = len f by A1,A4,A5,FINSEQ_6:2;
then
A9: (f^'g:-g/.1) = g by Th16;
(f^'g-:g/.1) = f by A8,Th17;
then
A10: (f^'g-:g/.1)/^1 = (1+1, len f)-cut f by Th13;
rng f c= rng(f^'g) by Th10;
hence Rotate(f^'g,g/.1) = (f^'g:-g/.1)^((f^'g-:g/.1)/^1) by A3,FINSEQ_6:def 2
.= g^'f by A9,A10,FINSEQ_6:def 5;
end;
begin :: TOP-REAL
theorem Th19:
for f being non trivial FinSequence of TOP-REAL 2 holds LSeg(f,1 ) = L~(f|2)
proof
let f be non trivial FinSequence of TOP-REAL 2;
A1: 1+1 <= len f by NAT_D:60;
then
A2: f|2 = <*f/.1,f/.2*> by FINSEQ_5:81;
thus LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A1,TOPREAL1:def 3
.= L~(f|2) by A2,SPPOL_2:21;
end;
theorem Th20:
for f being s.c.c. FinSequence of TOP-REAL 2, n st n < len f
holds f|n is s.n.c.
proof
let f be s.c.c. FinSequence of TOP-REAL 2, n such that
A1: n < len f;
let i,j be Nat such that
A2: i+1 < j;
A3: len(f|n) <= n by FINSEQ_5:17;
per cases;
suppose
n < j+1;
then len(f|n) < j+1 by A3,XXREAL_0:2;
then LSeg(f|n,j) = {} by TOPREAL1:def 3;
then LSeg(f|n,i) /\ LSeg(f|n,j) = {};
hence thesis by XBOOLE_0:def 7;
end;
suppose
len(f|n) < j+1;
then LSeg(f|n,j) = {} by TOPREAL1:def 3;
then LSeg(f|n,i) /\ LSeg(f|n,j) = {};
hence thesis by XBOOLE_0:def 7;
end;
suppose that
A4: j+1 <= n and
A5: j+1 <= len(f|n);
j+1 < len f by A1,A4,XXREAL_0:2;
then
A6: LSeg(f,i) misses LSeg(f,j) by A2,GOBOARD5:def 4;
j <= j+1 by NAT_1:11;
then
A7: i+1 <= j+1 by A2,XXREAL_0:2;
LSeg(f,j) = LSeg(f|n,j) by A5,SPPOL_2:3;
hence thesis by A5,A6,A7,SPPOL_2:3,XXREAL_0:2;
end;
end;
theorem Th21:
for f being s.c.c. FinSequence of TOP-REAL 2, n st 1 <= n holds
f/^n is s.n.c.
proof
let f be s.c.c. FinSequence of TOP-REAL 2, n such that
A1: 1 <= n;
let i,j be Nat such that
A2: i+1 < j;
per cases;
suppose
i < 1;
then LSeg(f/^n,i) = {} by TOPREAL1:def 3;
then LSeg(f/^n,i) /\ LSeg(f/^n,j) = {};
hence thesis by XBOOLE_0:def 7;
end;
suppose
n > len f;
then f/^n = <*>the carrier of TOP-REAL2 by RFINSEQ:def 1;
then not(1 <= i & i+1 <= len(f/^n));
then LSeg(f/^n,i) = {} by TOPREAL1:def 3;
then LSeg(f/^n,i) /\ LSeg(f/^n,j) = {};
hence thesis by XBOOLE_0:def 7;
end;
suppose
len(f/^n) <= j;
then len(f/^n) < j+1 by NAT_1:13;
then LSeg(f/^n,j) = {} by TOPREAL1:def 3;
then LSeg(f/^n,i) /\ LSeg(f/^n,j) = {};
hence thesis by XBOOLE_0:def 7;
end;
suppose that
A3: n <= len f and
A4: 1 <= i and
A5: j < len(f/^n);
A6: j < len f - n by A3,A5,RFINSEQ:def 1;
then
A7: j+1 <= len f - n by INT_1:7;
1+1 <= i+1 by A4,XREAL_1:6;
then 1+1 <= j by A2,XXREAL_0:2;
then 1 < j by NAT_1:13;
then
A8: LSeg(f,j+n) = LSeg(f/^n,j) by A7,SPPOL_2:5;
i+1+n < j+n by A2,XREAL_1:6;
then
A9: i+n+1 < j+n;
j <= j+1 by NAT_1:11;
then i+1 <= j+1 by A2,XXREAL_0:2;
then
A10: i+1 <= len f - n by A7,XXREAL_0:2;
1+1 <= i+n by A1,A4,XREAL_1:7;
then
A11: 1 < i+n by NAT_1:13;
j+n < len f by A6,XREAL_1:20;
then LSeg(f,i+n) misses LSeg(f,j+n) by A11,A9,GOBOARD5:def 4;
hence thesis by A4,A8,A10,SPPOL_2:5;
end;
end;
theorem Th22:
for f being circular s.c.c. FinSequence of TOP-REAL 2, n st n <
len f & len f > 4 holds f|n is one-to-one
proof
let f be circular s.c.c. FinSequence of TOP-REAL 2,n such that
A1: n < len f and
A2: len f > 4;
for c1,c2 being Element of NAT st c1 in dom(f|n) & c2 in dom(f|n) & (f|n
)/.c1 = (f|n)/.c2 holds c1 = c2
proof
A3: len(f|n) <= n by FINSEQ_5:17;
A4: len(f|n) <= n by FINSEQ_5:17;
let c1,c2 being Element of NAT such that
A5: c1 in dom(f|n) and
A6: c2 in dom(f|n) and
A7: (f|n)/.c1 = (f|n)/.c2;
A8: 1 <= c1 by A5,FINSEQ_3:25;
c1 <= len(f|n) by A5,FINSEQ_3:25;
then c1 <= n by A3,XXREAL_0:2;
then
A9: c1 < len f by A1,XXREAL_0:2;
A10: 1 <= c2 by A6,FINSEQ_3:25;
A11: (f|n)/.c1 = f/.c1 by A5,FINSEQ_4:70;
c2 <= len(f|n) by A6,FINSEQ_3:25;
then c2 <= n by A4,XXREAL_0:2;
then
A12: c2 < len f by A1,XXREAL_0:2;
A13: (f|n)/.c2 = f/.c2 by A6,FINSEQ_4:70;
assume
A14: c1 <> c2;
per cases by A14,XXREAL_0:1;
suppose
c1 < c2;
hence thesis by A2,A7,A8,A12,A11,A13,GOBOARD7:35;
end;
suppose
c2 < c1;
hence thesis by A2,A7,A10,A9,A11,A13,GOBOARD7:35;
end;
end;
hence thesis by PARTFUN2:9;
end;
theorem Th23:
for f being circular s.c.c. FinSequence of TOP-REAL 2 st len f >
4 for i,j being Nat st 1 < i & i < j & j <= len f holds f/.i <> f/.j
proof
let f be circular s.c.c. FinSequence of TOP-REAL 2 such that
A1: len f > 4;
let i,j be Nat such that
A2: 1 < i and
A3: i < j and
A4: j <= len f;
per cases by A4,XXREAL_0:1;
suppose
j < len f;
hence thesis by A1,A2,A3,GOBOARD7:35;
end;
suppose
j = len f;
then
A5: f/.j = f/.1 by FINSEQ_6:def 1;
i < len f by A3,A4,XXREAL_0:2;
hence thesis by A1,A2,A5,GOBOARD7:35;
end;
end;
theorem Th24:
for f being circular s.c.c. FinSequence of TOP-REAL 2, n st 1 <=
n & len f > 4 holds f/^n is one-to-one
proof
let f be circular s.c.c. FinSequence of TOP-REAL 2,n such that
A1: 1 <= n and
A2: len f > 4;
for c1,c2 being Element of NAT st c1 in dom(f/^n) & c2 in dom(f/^n) & (f
/^n)/.c1 = (f/^n)/.c2 holds c1 = c2
proof
let c1,c2 being Element of NAT such that
A3: c1 in dom(f/^n) and
A4: c2 in dom(f/^n) and
A5: (f/^n)/.c1 = (f/^n)/.c2;
A6: (f/^n)/.c1 = f/.(c1+n) by A3,FINSEQ_5:27;
A7: n <= len f by A3,RELAT_1:38,RFINSEQ:def 1;
then len(f/^n) = len f - n by RFINSEQ:def 1;
then
A8: len(f/^n) + n = len f;
len(f/^n) = len f - n by A7,RFINSEQ:def 1;
then
A9: len(f/^n) + n = len f;
c1 <= len(f/^n) by A3,FINSEQ_3:25;
then
A10: c1+n <= len f by A9,XREAL_1:6;
0+1 <= c1 by A3,FINSEQ_3:25;
then
A11: 1+0 < c1+n by A1,XREAL_1:8;
A12: (f/^n)/.c2 = f/.(c2+n) by A4,FINSEQ_5:27;
c2 <= len(f/^n) by A4,FINSEQ_3:25;
then
A13: c2+n <= len f by A8,XREAL_1:6;
0+1 <= c2 by A4,FINSEQ_3:25;
then
A14: 1+0 < c2+n by A1,XREAL_1:8;
assume
A15: c1 <> c2;
per cases by A15,XXREAL_0:1;
suppose
c1 < c2;
then c1+n < c2+n by XREAL_1:6;
hence thesis by A2,A5,A11,A13,A6,A12,Th23;
end;
suppose
c2 < c1;
then c2+n < c1+n by XREAL_1:6;
hence thesis by A2,A5,A14,A10,A6,A12,Th23;
end;
end;
hence thesis by PARTFUN2:9;
end;
theorem Th25:
for f being special non empty FinSequence of TOP-REAL 2 holds (m
,n)-cut f is special
proof
let f being special non empty FinSequence of TOP-REAL 2;
set h = (m,n)-cut f;
let i be Nat such that
A1: 1 <= i and
A2: i+1 <= len h;
per cases;
suppose
not(1<=m & m<=n & n<=len f);
then h = {} by FINSEQ_6:def 4;
hence thesis by A2;
end;
suppose
A3: 1<=m & m<=n & n<=len f;
then
A4: 1+1 <= i+m by A1,XREAL_1:7;
then
A5: 1 <= i+m by XXREAL_0:2;
A6: i-'1+m = i+m-'1 by A1,NAT_D:38;
then
A7: 1 <= i-'1+m by A4,NAT_D:55;
A8: i-'1+m+1 = i+m-'1+1 by A1,NAT_D:38
.= i+m by A4,XREAL_1:235,XXREAL_0:2;
A9: i < len h by A2,NAT_1:13;
len h +m = n+1 by A3,FINSEQ_6:def 4;
then i+m < n+1 by A9,XREAL_1:6;
then i+m <= n by NAT_1:13;
then
A10: i+m <= len f by A3,XXREAL_0:2;
then
A11: i-'1+m <= len f by A6,NAT_D:44;
i -' 1 <= i by NAT_D:44;
then
A12: i -' 1 < len h by A9,XXREAL_0:2;
A13: h/.(i+1) =h.(i+1) by A2,FINSEQ_4:15,NAT_1:11
.= f.(i+m) by A3,A9,FINSEQ_6:def 4
.= f/.(i+m) by A5,A10,FINSEQ_4:15;
i-'1+1 = i by A1,XREAL_1:235;
then h/.i =h.(i -' 1+1) by A1,A9,FINSEQ_4:15
.= f.(i-'1+m) by A3,A12,FINSEQ_6:def 4
.= f/.(i-'1+m) by A6,A4,A11,FINSEQ_4:15,NAT_D:55;
hence thesis by A7,A10,A13,A8,TOPREAL1:def 5;
end;
end;
theorem Th26:
for f being special non empty FinSequence of TOP-REAL 2 for g
being special non trivial FinSequence of TOP-REAL 2 st f/.len f = g/.1 holds f
^'g is special
proof
let f be special non empty FinSequence of TOP-REAL 2;
let g be special non trivial FinSequence of TOP-REAL 2 such that
A1: f/.len f = g/.1;
set h = (2, len g)-cut g;
A2: f^'g = f^(2, len g)-cut g by FINSEQ_6:def 5;
A3: 1+1 <= len g by NAT_D:60;
then
A4: (g/.1)`1 = (g/.(1+1))`1 or (g/.1)`2 = (g/.(1+1))`2 by TOPREAL1:def 5;
len g <= len g +1 by NAT_1:11;
then
A5: 2<=len g+1 by A3,XXREAL_0:2;
len h +1+1 = len h +(1+1) .= len g+1 by A5,Lm1;
then 1 <= len h by A3,XREAL_1:6;
then
A6: h/.1 = h.1 by FINSEQ_4:15
.= g.(1+1) by A3,FINSEQ_6:138
.= g/.(1+1) by A3,FINSEQ_4:15;
h is special by Th25;
hence thesis by A1,A2,A6,A4,GOBOARD2:8;
end;
theorem Th27:
for f being circular unfolded s.c.c. FinSequence of TOP-REAL 2
st len f > 4 holds LSeg(f,1) /\ L~(f/^1) = {f/.1,f/.2}
proof
let f be circular unfolded s.c.c. FinSequence of TOP-REAL 2 such that
A1: len f > 4;
A2: 1+2 <= len f by A1,XXREAL_0:2;
set h2 = f/^1;
A3: 1 <= len f by A1,XXREAL_0:2;
then
A4: len h2 = len f - 1 by RFINSEQ:def 1;
then
A5: len h2 + 1 = len f;
len f > 3+1 by A1;
then
A6: len h2 > 2+1 by A5,XREAL_1:6;
then
A7: 1+1 <= len(f/^1) by XXREAL_0:2;
set SFY = { LSeg(f/^1,i) : 1 < i & i+1 < len(f/^1) }, Reszta = union SFY;
A8: len(f/^1)-'1+1 <= len(f/^1) by A6,XREAL_1:235,XXREAL_0:2;
A9: 1 < len f by A1,XXREAL_0:2;
for Z being set holds Z in {{}} iff ex X,Y being set st X in {LSeg(f,1)
} & Y in SFY & Z = X /\ Y
proof
let Z be set;
thus Z in {{}} implies ex X,Y being set st X in {LSeg(f,1)} & Y in SFY & Z
= X /\ Y
proof
assume
A10: Z in {{}};
take X = LSeg(f,1), Y = LSeg(f,2+1);
thus X in {LSeg(f,1)} by TARSKI:def 1;
Y = LSeg(f/^1,2) by A3,SPPOL_2:4;
hence Y in SFY by A6;
A11: 1+1 < 3;
3+1 < len f by A1;
then X misses Y by A11,GOBOARD5:def 4;
then X /\ Y = {} by XBOOLE_0:def 7;
hence Z = X /\ Y by A10,TARSKI:def 1;
end;
given X,Y being set such that
A12: X in {LSeg(f,1)} and
A13: Y in SFY and
A14: Z = X /\ Y;
A15: X = LSeg(f,1) by A12,TARSKI:def 1;
consider i such that
A16: Y = LSeg(f/^1,i) and
A17: 1 < i and
A18: i+1 < len(f/^1) by A13;
A19: 1+1 < i+1 by A17,XREAL_1:6;
A20: i+1+1 < len f by A5,A18,XREAL_1:6;
LSeg(f/^1,i) = LSeg(f,i+1) by A9,A17,SPPOL_2:4;
then X misses Y by A15,A16,A20,A19,GOBOARD5:def 4;
then Z = {} by A14,XBOOLE_0:def 7;
hence thesis by TARSKI:def 1;
end;
then INTERSECTION({LSeg(f,1)},SFY) = {{}} by SETFAM_1:def 5;
then
A21: LSeg(f,1) /\Reszta = union {{}} by SETFAM_1:25
.= {} by ZFMISC_1:25;
A22: L~(f/^1) c= LSeg(f/^1,1) \/ LSeg(f/^1,len(f/^1)-'1) \/ Reszta
proof
let u be object;
assume u in L~(f/^1);
then consider e being set such that
A23: u in e and
A24: e in { LSeg(f/^1,i) : 1 <= i & i+1 <= len(f/^1) } by TARSKI:def 4;
consider i such that
A25: e = LSeg(f/^1,i) and
A26: 1 <= i and
A27: i+1 <= len(f/^1) by A24;
per cases by A26,A27,XXREAL_0:1;
suppose
i = 1;
then u in LSeg(f/^1,1) \/ LSeg(f/^1,len(f/^1)-'1) by A23,A25,
XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
i+1 = len(f/^1);
then i = len(f/^1)-'1 by NAT_D:34;
then u in LSeg(f/^1,1) \/ LSeg(f/^1,len(f/^1)-'1) by A23,A25,
XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
1 < i & i+1 < len(f/^1);
then e in SFY by A25;
then u in Reszta by A23,TARSKI:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
A28: Reszta c= L~(f/^1)
proof
let u be object;
assume u in Reszta;
then consider e being set such that
A29: u in e and
A30: e in SFY by TARSKI:def 4;
ex i st e = LSeg(f/^1,i) & 1 < i & i+1 < len(f/^1) by A30;
then e in { LSeg(f/^1,i) : 1 <= i & i+1 <= len(f/^1) };
hence thesis by A29,TARSKI:def 4;
end;
1+(len(f/^1)-'1) = len(f/^1) by A6,XREAL_1:235,XXREAL_0:2
.= len f -' 1 by A1,A4,XREAL_1:233,XXREAL_0:2;
then
A31: LSeg(f,1) /\ LSeg(f/^1,len(f/^1)-'1) = LSeg(f,1) /\ LSeg(f,len f-'1) by A3
,A7,NAT_D:55,SPPOL_2:4
.= {f/.1} by A1,REVROT_1:30;
1+1 <= len h2 by A6,NAT_1:13;
then LSeg(f/^1,1) in { LSeg(f/^1,i) : 1 <= i & i+1 <= len(f/^1) };
then
A32: LSeg(f/^1,1) c= L~(f/^1) by ZFMISC_1:74;
A33: LSeg(f,1) /\ LSeg(f/^1,1) = LSeg(f,1) /\ LSeg(f,1+1) by A3,SPPOL_2:4
.= {f/.(1+1)} by A2,TOPREAL1:def 6;
1 <= len(f/^1)-'1 by A7,NAT_D:55;
then
LSeg(f/^1,len(f/^1)-'1) in { LSeg(f/^1,i) : 1 <= i & i+1 <= len(f/^1) }
by A8;
then LSeg(f/^1,len(f/^1)-'1) c= L~(f/^1) by ZFMISC_1:74;
then LSeg(f/^1,1) \/ LSeg(f/^1,len(f/^1)-'1) c= L~(f/^1) by A32,XBOOLE_1:8;
then LSeg(f/^1,1) \/ LSeg(f/^1,len(f/^1)-'1) \/ Reszta c= L~(f/^1) by A28,
XBOOLE_1:8;
then L~(f/^1) = LSeg(f/^1,1) \/ LSeg(f/^1,len(f/^1)-'1) \/ Reszta by A22,
XBOOLE_0:def 10;
hence
LSeg(f,1) /\ L~(f/^1) = LSeg(f,1) /\ (LSeg(f/^1,1) \/ LSeg(f/^1,len(f/^
1)-'1)) \/ {} by A21,XBOOLE_1:23
.= {f/.1} \/ {f/.2} by A33,A31,XBOOLE_1:23
.= {f/.1,f/.2} by ENUMSET1:1;
end;
theorem Th28:
for f,g being FinSequence of TOP-REAL 2 st j < len f holds LSeg(
f^'g,j) = LSeg(f,j)
proof
let f,g be FinSequence of TOP-REAL 2 such that
A1: j < len f;
per cases;
suppose
A2: j < 1;
hence LSeg(f^'g,j) = {} by TOPREAL1:def 3
.= LSeg(f,j) by A2,TOPREAL1:def 3;
end;
suppose
A3: 1 <= j;
then
A4: (f^'g)/.j = f/.j by A1,FINSEQ_6:159;
A5: j+1 <= len f by A1,NAT_1:13;
then
A6: (f^'g)/.(j+1) = f/.(j+1) by FINSEQ_6:159,NAT_1:11;
len f <= len(f^'g) by Th7;
then j+1 <= len (f^'g) by A5,XXREAL_0:2;
hence LSeg(f^'g,j) = LSeg((f^'g)/.j,(f^'g)/.(j+1)) by A3,TOPREAL1:def 3
.= LSeg(f,j) by A3,A4,A5,A6,TOPREAL1:def 3;
end;
end;
theorem Th29:
for f,g being non empty FinSequence of TOP-REAL 2 st 1 <= j & j+
1 < len g holds LSeg(f^'g,len f+j) = LSeg(g,j+1)
proof
let f,g be non empty FinSequence of TOP-REAL 2 such that
A1: 1 <= j and
A2: j+1 < len g;
A3: (f^'g)/.(len f +j+1) = (f^'g)/.(len f +(j+1))
.= g/.(j+1+1) by A2,FINSEQ_6:160,NAT_1:11;
j+0 <= j+1 by XREAL_1:6;
then j < len g by A2,XXREAL_0:2;
then
A4: (f^'g)/.(len f +j) = g/.(j+1) by A1,FINSEQ_6:160;
A5: 1 <= j+1 by NAT_1:11;
len f + (j+1) < len f + len g by A2,XREAL_1:6;
then len f +j+1 < len (f^'g)+1 by FINSEQ_6:139;
then
A6: len f +j+1 <= len (f^'g) by NAT_1:13;
A7: j+1+1 <= len g by A2,NAT_1:13;
j <= len f + j by NAT_1:11;
then 1 <= len f +j by A1,XXREAL_0:2;
hence LSeg(f^'g,len f+j) = LSeg((f^'g)/.(len f+j),(f^'g)/.(len f+j+1)) by A6,
TOPREAL1:def 3
.= LSeg(g,j+1) by A4,A5,A3,A7,TOPREAL1:def 3;
end;
theorem Th30:
for f being non empty FinSequence of TOP-REAL 2 for g being non
trivial FinSequence of TOP-REAL 2 st f/.len f = g/.1 holds LSeg(f^'g,len f) =
LSeg(g,1)
proof
let f be non empty FinSequence of TOP-REAL 2;
A1: 1 <= len f by NAT_1:14;
let g be non trivial FinSequence of TOP-REAL 2;
assume f/.len f = g/.1;
then
A2: (f^'g)/.(len f +0) = g/.(0+1) by A1,FINSEQ_6:159;
A3: 1 < len g by Th2;
then
A4: (f^'g)/.(len f +0+1) = g/.(0+1+1) by FINSEQ_6:160;
A5: 1+1 <= len g by A3,NAT_1:13;
len f + 0+1 < len f + len g by A3,XREAL_1:6;
then len f +0+1 < len (f^'g)+1 by FINSEQ_6:139;
then len f +0+1 <= len (f^'g) by NAT_1:13;
hence LSeg(f^'g,len f) = LSeg((f^'g)/.(len f+0),(f^'g)/.(len f+0+1)) by A1,
TOPREAL1:def 3
.= LSeg(g,1) by A2,A4,A5,TOPREAL1:def 3;
end;
theorem Th31:
for f being non empty FinSequence of TOP-REAL 2 for g being non
trivial FinSequence of TOP-REAL 2 st j+1 < len g & f/.len f = g/.1 holds LSeg(f
^'g,len f+j) = LSeg(g,j+1)
proof
let f be non empty FinSequence of TOP-REAL 2;
let g be non trivial FinSequence of TOP-REAL 2 such that
A1: j+1 < len g and
A2: f/.len f = g/.1;
per cases by NAT_1:14;
suppose
j = 0;
hence thesis by A2,Th30;
end;
suppose
1 <= j;
hence thesis by A1,Th29;
end;
end;
theorem Th32:
for f being non empty s.n.c. unfolded FinSequence of TOP-REAL 2,
i st 1 <= i & i < len f holds LSeg(f,i) /\ rng f = {f/.i,f/.(i+1)}
proof
let f be non empty s.n.c. unfolded FinSequence of TOP-REAL 2, i such that
A1: 1 <= i and
A2: i < len f;
A3: i in dom f by A1,A2,FINSEQ_3:25;
then f/.i = f.i by PARTFUN1:def 6;
then
A4: f/.i in rng f by A3,FUNCT_1:3;
assume
A5: LSeg(f,i) /\ rng f <> {f/.i,f/.(i+1)};
A6: i+1 <= len f by A2,NAT_1:13;
then f/.i in LSeg(f,i) by A1,TOPREAL1:21;
then
A7: f/.i in LSeg(f,i) /\ rng f by A4,XBOOLE_0:def 4;
A8: 1 < i+1 by A1,XREAL_1:29;
then
A9: i+1 in dom f by A6,FINSEQ_3:25;
then f/.(i+1) = f.(i+1) by PARTFUN1:def 6;
then
A10: f/.(i+1) in rng f by A9,FUNCT_1:3;
f/.(i+1) in LSeg(f,i) by A1,A6,TOPREAL1:21;
then f/.(i+1) in LSeg(f,i) /\ rng f by A10,XBOOLE_0:def 4;
then {f/.i,f/.(i+1)} c= LSeg(f,i) /\ rng f by A7,ZFMISC_1:32;
then not LSeg(f,i) /\ rng f c= {f/.i,f/.(i+1)} by A5,XBOOLE_0:def 10;
then consider x being object such that
A11: x in LSeg(f,i) /\ rng f and
A12: not x in {f/.i,f/.(i+1)};
reconsider x as Point of TOP-REAL 2 by A11;
A13: x in LSeg(f,i) by A11,XBOOLE_0:def 4;
x in rng f by A11,XBOOLE_0:def 4;
then consider j being object such that
A14: j in dom f and
A15: x = f.j by FUNCT_1:def 3;
A16: x = f/.j by A14,A15,PARTFUN1:def 6;
reconsider j as Nat by A14;
A17: 1 <= j by A14,FINSEQ_3:25;
reconsider j as Nat;
A18: x <> f/.i by A12,TARSKI:def 2;
then
A19: j <> i by A14,A15,PARTFUN1:def 6;
A20: x <> f/.(i+1) by A12,TARSKI:def 2;
then
A21: j <> i+1 by A14,A15,PARTFUN1:def 6;
now
per cases by A19,XXREAL_0:1;
suppose
A22: j+1 > len f;
A23: j <= len f by A14,FINSEQ_3:25;
len f <= j by A22,NAT_1:13;
then
A24: j = len f by A23,XXREAL_0:1;
consider k be Nat such that
A25: len f = 1 + k by A6,A8,NAT_1:10,XXREAL_0:2;
reconsider k as Nat;
1 < len f by A6,A8,XXREAL_0:2;
then 1 <= k by A25,NAT_1:13;
then
A26: x in LSeg(f,k) by A16,A24,A25,TOPREAL1:21;
i <= k by A2,A25,NAT_1:13;
then i < k by A20,A16,A24,A25,XXREAL_0:1;
then
A27: i+1 <= k by NAT_1:13;
now
per cases by A27,XXREAL_0:1;
suppose
A28: i+1 = k;
then i+(1+1) <= len f by A25;
then LSeg(f,i) /\ LSeg(f,k) = {f/.(i+1)} by A1,A28,TOPREAL1:def 6;
then x in {f/.(i+1)} by A13,A26,XBOOLE_0:def 4;
hence contradiction by A20,TARSKI:def 1;
end;
suppose
i+1 < k;
then LSeg(f,i) misses LSeg(f,k) by TOPREAL1:def 7;
hence contradiction by A13,A26,XBOOLE_0:3;
end;
end;
hence contradiction;
end;
suppose that
A29: i < j and
A30: j+1 <= len f;
i+1 <= j by A29,NAT_1:13;
then i+1 < j by A21,XXREAL_0:1;
then
A31: LSeg(f,i) misses LSeg(f,j) by TOPREAL1:def 7;
x in LSeg(f,j) by A16,A17,A30,TOPREAL1:21;
hence contradiction by A13,A31,XBOOLE_0:3;
end;
suppose
A32: j < i;
then j+1 <= i+1 by XREAL_1:6;
then j+1 <= len f by A6,XXREAL_0:2;
then x in LSeg(f,j) by A16,A17,TOPREAL1:21;
then
A33: x in LSeg(f,i) /\ LSeg(f,j) by A13,XBOOLE_0:def 4;
A34: j+1 <= i by A32,NAT_1:13;
now
per cases by A34,XXREAL_0:1;
suppose
A35: j+1 = i;
then j+1+1 <= len f by A2,NAT_1:13;
then j+(1+1) <= len f;
then LSeg(f,i) /\ LSeg(f,j) = {f/.i} by A17,A35,TOPREAL1:def 6;
hence contradiction by A18,A33,TARSKI:def 1;
end;
suppose
j+1 < i;
then LSeg(f,j) misses LSeg(f,i) by TOPREAL1:def 7;
hence contradiction by A33,XBOOLE_0:4;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
Lm2: for f being non empty s.n.c. one-to-one unfolded FinSequence of TOP-REAL
2 for g being non trivial s.n.c. one-to-one unfolded FinSequence of TOP-REAL 2
for i,j st i < len f & 1 < i for x being Point of TOP-REAL 2 st x in LSeg(f^'g,
i) /\ LSeg(f^'g,j) holds x <> f/.1
proof
let f being non empty s.n.c. one-to-one unfolded FinSequence of TOP-REAL 2;
let g being non trivial s.n.c. one-to-one unfolded FinSequence of TOP-REAL 2;
let i,j such that
A1: i < len f and
A2: 1 < i;
A3: 1 < i+1 by A2,XREAL_1:29;
A4: LSeg(f,i) /\ rng f = {f/.i,f/.(i+1)} by A1,A2,Th32;
i+1 <= len f by A1,NAT_1:13;
then
A5: i+1 in dom f by A3,FINSEQ_3:25;
A6: LSeg(f^'g,i) = LSeg(f,i) by A1,Th28;
let x being Point of TOP-REAL 2;
assume x in LSeg(f^'g,i) /\ LSeg(f^'g,j);
then
A7: x in LSeg(f,i) by A6,XBOOLE_0:def 4;
A8: 1 in dom f by FINSEQ_5:6;
assume that
A9: x = f/.1;
x = f.1 by A9,A8,PARTFUN1:def 6;
then x in rng f by A8,FUNCT_1:3;
then x in LSeg(f,i) /\ rng f by A7,XBOOLE_0:def 4;
then
A10: x = f/.i or x = f/.(i+1) by A4,TARSKI:def 2;
i in dom f by A1,A2,FINSEQ_3:25;
hence contradiction by A2,A9,A8,A10,A3,A5,PARTFUN2:10;
end;
Lm3: for f being non empty s.n.c. one-to-one unfolded FinSequence of TOP-REAL
2 for g being non trivial s.n.c. one-to-one unfolded FinSequence of TOP-REAL 2
for i,j st j > len f & j+1 < len(f^'g) for x being Point of TOP-REAL 2 st x in
LSeg(f^'g,i) /\ LSeg(f^'g,j) holds x <> g/.len g
proof
let f being non empty s.n.c. one-to-one unfolded FinSequence of TOP-REAL 2;
let g being non trivial s.n.c. one-to-one unfolded FinSequence of TOP-REAL 2;
let i,j such that
A1: j > len f and
A2: j+1 < len(f^'g);
consider k be Nat such that
A3: j = len f + k by A1,NAT_1:10;
len(f^'g)+1 = len f + len g by FINSEQ_6:139;
then
A4: j+1+1 < len f + len g by A2,XREAL_1:6;
reconsider k as Nat;
j+1+1 = len f+(k+1+1) by A3;
then
A5: k+1+1 < len g by A4,XREAL_1:6;
1 <= k+1+1 by NAT_1:11;
then
A6: k+1+1 in dom g by A5,FINSEQ_3:25;
let x being Point of TOP-REAL 2 such that
A7: x in LSeg(f^'g,i) /\ LSeg(f^'g,j);
A8: len g in dom g by FINSEQ_5:6;
A9: k+1 <= k+1+1 by NAT_1:11;
then
A10: k+1 < len g by A5,XXREAL_0:2;
then
A11: LSeg(g,k+1) /\ rng g = {g/.(k+1),g/.(k+1+1)} by Th32,NAT_1:11;
assume that
A12: x = g/.len g;
x = g.len g by A12,A8,PARTFUN1:def 6;
then
A13: x in rng g by A8,FUNCT_1:3;
1 <= k+1 by NAT_1:11;
then
A14: k+1 in dom g by A10,FINSEQ_3:25;
len f + 0 < len f +k by A1,A3;
then 0 < k;
then 0+1 <= k by NAT_1:13;
then LSeg(f^'g,j) = LSeg(g,k+1) by A3,A10,Th29;
then x in LSeg(g,k+1) by A7,XBOOLE_0:def 4;
then x in LSeg(g,k+1) /\ rng g by A13,XBOOLE_0:def 4;
then x = g/.(k+1) or x = g/.(k+1+1) by A11,TARSKI:def 2;
hence contradiction by A12,A5,A9,A8,A14,A6,PARTFUN2:10;
end;
theorem Th33:
for f,g being non trivial s.n.c. one-to-one unfolded FinSequence
of TOP-REAL 2 st L~f /\ L~g = {f/.1,g/.1} & f/.1 = g/.len g & g/.1 = f/.len f
holds f ^' g is s.c.c.
proof
let f,g being non trivial s.n.c. one-to-one unfolded FinSequence of TOP-REAL
2 such that
A1: L~f /\ L~g = {f/.1,g/.1} and
A2: f/.1 = g/.len g and
A3: g/.1 = f/.len f;
A4: for i st 1 <= i & i < len f holds f/.i <> g/.1
proof
A5: len f in dom f by FINSEQ_5:6;
then
A6: f/.len f = f.len f by PARTFUN1:def 6;
let i such that
A7: 1 <= i and
A8: i < len f;
A9: i in dom f by A7,A8,FINSEQ_3:25;
then f/.i = f.i by PARTFUN1:def 6;
hence thesis by A3,A8,A9,A5,A6,FUNCT_1:def 4;
end;
A10: len(f^'g)+1 = len f + len g by FINSEQ_6:139;
A11: len(g^'f)+1 = len f + len g by FINSEQ_6:139;
let i,j such that
A12: i+1 < j and
A13: i > 1 & j < len(f^'g) or j+1 < len(f^'g);
A14: i < j by A12,NAT_1:13;
j <= j+1 by NAT_1:11;
then
A15: j < len(f^'g) by A13,XXREAL_0:2;
per cases by NAT_1:14;
suppose
i = 0;
then LSeg(f^'g,i) = {} by TOPREAL1:def 3;
then LSeg(f^'g,i) /\ LSeg(f^'g,j) = {};
hence thesis by XBOOLE_0:def 7;
end;
suppose
A16: j < len f;
then i < len f by A14,XXREAL_0:2;
then
A17: LSeg(f^'g,i) = LSeg(f,i) by Th28;
LSeg(f^'g,j) = LSeg(f,j) by A16,Th28;
hence thesis by A12,A17,TOPREAL1:def 7;
end;
suppose
A18: i >= len f;
then consider m be Nat such that
A19: i = len f + m by NAT_1:10;
consider n be Nat such that
A20: j = len f + n by A14,A18,NAT_1:10,XXREAL_0:2;
reconsider m,n as Nat;
A21: 1 <= m+1 by NAT_1:11;
j+1 < len f + len g by A15,A10,XREAL_1:6;
then len f + (n+1) < len f + len g by A20;
then
A22: n+1 < len g by XREAL_1:6;
A23: m < n by A14,A19,A20,XREAL_1:6;
then m+1 <= n by NAT_1:13;
then 1 <= n by A21,XXREAL_0:2;
then
A24: LSeg(f^'g,j) = LSeg(g,n+1) by A20,A22,Th29;
i + 1 + 1 < j + 1 by A12,XREAL_1:6;
then len f + (m + (1 + 1)) < len f + (n + 1) by A19,A20;
then
A25: m+1+1 < n+1 by XREAL_1:6;
m+1 < n+1 by A23,XREAL_1:6;
then m+1 < len g by A22,XXREAL_0:2;
then LSeg(f^'g,i) = LSeg(g,m+1) by A3,A19,Th31;
hence thesis by A24,A25,TOPREAL1:def 7;
end;
suppose that
A26: j >= len f and
A27: i < len f and
A28: 1 <= i;
consider k be Nat such that
A29: j = len f + k by A26,NAT_1:10;
reconsider k as Nat;
j+1 < len f+ len g by A15,A10,XREAL_1:6;
then len f + (k +1) < len f+ len g by A29;
then k+1 < len g by XREAL_1:6;
then LSeg(f^'g,j) = LSeg(g,k+1) by A3,A29,Th31;
then
A30: LSeg(f^'g,j) c= L~g by TOPREAL3:19;
assume LSeg(f^'g,i) meets LSeg(f^'g,j);
then consider x being object such that
A31: x in LSeg(f^'g,i) /\ LSeg(f^'g,j) by XBOOLE_0:4;
LSeg(f^'g,i) = LSeg(f,i) by A27,Th28;
then LSeg(f^'g,i) c= L~f by TOPREAL3:19;
then
A32: LSeg(f^'g,i) /\ LSeg(f^'g,j) c= {f/.1,g/.1} by A1,A30,XBOOLE_1:27;
now
per cases by A13,A26,A31,A32,TARSKI:def 2,XXREAL_0:1;
suppose
1 < i & x = f/.1;
hence contradiction by A27,A31,Lm2;
end;
suppose that
A33: j > len f + 0 and
A34: x = g/.1;
j+0 < j+1 by XREAL_1:6;
then
A35: len f < j+1 by A33,XXREAL_0:2;
j+1 < len(g^'f) + 1 by A15,A10,A11,XREAL_1:6;
then j+1 -' len f < len g by A11,A35,NAT_D:54;
then
A36: j -' len f+1 < len g by A33,NAT_D:38;
A37: Rotate(f^'g,g/.1) = g^'f by A3,A4,Th18;
0 < j -' len f by A33,NAT_D:52;
then
A38: 0+1 < j -' len f+1 by XREAL_1:6;
A39: len f in dom f by FINSEQ_5:6;
then f.len f = f/.len f by PARTFUN1:def 6;
then
A40: g/.1 in rng f by A3,A39,FUNCT_1:3;
then
A41: g/.1..(f^'g) = g/.1..f by Th8
.= len f by A3,Th6;
A42: rng f c= rng(f^'g) by Th10;
then
A43: LSeg(f^'g,j) = LSeg(Rotate((f^'g),g/.1),j -' g/.1..(f^'g)+1) by A15,A33
,A40,A41,REVROT_1:25;
f^'g is circular by A2,Th11;
then
LSeg(f^'g,i) = LSeg(Rotate((f^'g),g/.1),i + len (f^'g) -' g/.1..(
f^'g)) by A27,A28,A40,A41,A42,REVROT_1:32;
hence contradiction by A31,A34,A37,A41,A43,A36,A38,Lm2;
end;
suppose that
A44: j = len f and
A45: x = g/.1;
i <= i+1 by NAT_1:11;
then i < j by A12,XXREAL_0:2;
then LSeg(f^'g,i) = LSeg(f,i) by A44,Th28;
then
A46: f/.len f in LSeg(f,i) by A3,A31,A45,XBOOLE_0:def 4;
i <= i+1 by NAT_1:11;
then i < len f by A12,A44,XXREAL_0:2;
then
A47: i in dom f by A28,FINSEQ_3:25;
1 <= i+1 by NAT_1:11;
then i+1 in dom f by A12,A44,FINSEQ_3:25;
hence contradiction by A12,A44,A47,A46,GOBOARD2:2;
end;
suppose that
A48: j > len f and
A49: x = f/.1 and
A50: j+1 < len(f^'g);
thus thesis by A2,A31,A48,A49,A50,Lm3;
end;
suppose that
A51: j = len f and
A52: x = f/.1 and
A53: j+1 < len(f^'g);
0+1 < len g by Th2;
then LSeg(f^'g,len f+0) = LSeg(g,0+1) by A3,Th31;
then
A54: g/.len g in LSeg(g,1) by A2,A31,A51,A52,XBOOLE_0:def 4;
j+1+1 < len f+ len g by A10,A53,XREAL_1:6;
then
A55: j+(1+1) < len f+ len g;
then 1+1 < len g by A51,XREAL_1:6;
then
A56: 1+1 in dom g by FINSEQ_3:25;
1 in dom g by FINSEQ_5:6;
hence contradiction by A51,A55,A54,A56,GOBOARD2:2;
end;
end;
hence contradiction;
end;
end;
reserve f,g,g1,g2 for FinSequence of TOP-REAL 2;
theorem Th34:
f is unfolded & g is unfolded & f/.len f = g/.1 & LSeg(f,len f
-' 1) /\ LSeg(g,1) = { f/.len f } implies f^'g is unfolded
proof
assume that
A1: f is unfolded and
A2: g is unfolded and
A3: f/.len f = g/.1 and
A4: LSeg(f,len f -' 1) /\ LSeg(g,1) = { f/.len f };
set c = (1+1, len g)-cut g, k = len f -' 1;
reconsider g9 = g as unfolded FinSequence of TOP-REAL 2 by A2;
A5: c = g9/^1 by Th13;
A6: f ^' g = f^(1+1, len g)-cut g by FINSEQ_6:def 5;
len g <= 2 implies len g = 0 or ... or len g = 2;
then per cases;
suppose
f is empty;
hence thesis by A6,A5,FINSEQ_1:34;
end;
suppose
len g = 0;
then g = {};
then c = <*>the carrier of TOP-REAL 2 by A5,FINSEQ_6:80;
hence thesis by A1,A6,FINSEQ_1:34;
end;
suppose
len g = 1;
then c = {} by A5,FINSEQ_6:167;
hence thesis by A1,A6,FINSEQ_1:34;
end;
suppose that
A7: f is non empty and
A8: len g = 1+1;
A9: k+1 = len f by A7,NAT_1:14,XREAL_1:235;
g|len g = g by FINSEQ_1:58;
then g = <*g/.1,g/.2*> by A8,FINSEQ_5:81;
then
A10: f^'g = f^<*g/.2*> by A6,A5,FINSEQ_6:46;
1 <= len g - 1 by A8;
then 1 <= len(g/^1) by A8,RFINSEQ:def 1;
then
A11: 1 in dom(g/^1) by FINSEQ_3:25;
then
A12: c/.1 = (g/^1).1 by A5,PARTFUN1:def 6
.= g.(1+1) by A8,A11,RFINSEQ:def 1
.= g/.(1+1) by A8,FINSEQ_4:15;
then LSeg(g,1) = LSeg(f/.len f,c/.1) by A3,A8,TOPREAL1:def 3;
hence thesis by A1,A4,A9,A10,A12,SPPOL_2:30;
end;
suppose that
A13: f is non empty and
A14: 2 < len g;
A15: 1 <= len g by A14,XXREAL_0:2;
then
A16: LSeg(g/^1,1) = LSeg(g,1+1) by SPPOL_2:4;
1+1 <= len g by A14;
then 1 <= len g - 1 by XREAL_1:19;
then 1 <= len(g/^1) by A15,RFINSEQ:def 1;
then
A17: 1 in dom(g/^1) by FINSEQ_3:25;
then
A18: c/.1 = (g/^1).1 by A5,PARTFUN1:def 6
.= g.(1+1) by A15,A17,RFINSEQ:def 1
.= g/.(1+1) by A14,FINSEQ_4:15;
then
A19: LSeg(g,1) = LSeg(f/.len f,c/.1) by A3,A14,TOPREAL1:def 3;
A20: k+1 = len f by A13,NAT_1:14,XREAL_1:235;
1 + 2 <= len g by A14,NAT_1:13;
then LSeg(g,1) /\ LSeg(c,1) = {c/.1} by A5,A18,A16,TOPREAL1:def 6;
hence thesis by A1,A4,A6,A5,A20,A19,SPPOL_2:31;
end;
end;
theorem Th35:
f is non empty & g is non trivial & f/.len f = g/.1 implies
L~(f^'g) = L~f \/ L~g
proof
assume that
A1: f is non empty and
A2: g is non trivial and
A3: f/.len f = g/.1;
set c = (1+1, len g)-cut g;
A4: c = g/^1 by Th13;
A5: len g > 1 by A2,Th2;
then len c = len g - 1 by A4,RFINSEQ:def 1;
then len c > 1-1 by A5,XREAL_1:9;
then len c > 0;
then
A6: c is non empty;
g is not empty by A2;
then g = <*g/.1*>^c by A4,FINSEQ_5:29;
then
A7: LSeg(g/.1,c/.1) \/ L~c = L~g by A6,SPPOL_2:20;
L~(f^c) = L~f \/ LSeg(f/.(len f),c/.1) \/ L~c by A1,A6,SPPOL_2:23
.= L~f \/ (LSeg(g/.1,c/.1) \/ L~c) by A3,XBOOLE_1:4;
hence thesis by A7,FINSEQ_6:def 5;
end;
theorem
(for n be Nat st n in dom f ex i,j be Nat st [i,j] in Indices G & f/.n
=G*(i,j)) & f is non constant circular unfolded s.c.c. special & len f > 4
implies ex g st g is_sequence_on G & g is unfolded s.c.c. special & L~f = L~g &
f/.1 = g/.1 & f/.len f = g/.len g & len f <= len g
proof
assume that
A1: for n be Nat st n in dom f ex i,j be Nat st [i,j] in Indices G & f/.
n=G*(i,j) and
A2: f is non constant circular unfolded and
A3: f is s.c.c. and
A4: f is special and
A5: len f > 4;
reconsider f9 = f as non constant unfolded s.c.c. special circular
FinSequence of TOP-REAL 2 by A2,A3,A4;
reconsider f9 as non constant unfolded s.c.c. special circular non empty
FinSequence of TOP-REAL 2;
set h1 = f9|2, h2 = f9/^1;
A6: len f > 1+1 by A2,Th3;
then
A7: len h1 = 1+1 by FINSEQ_1:59;
then reconsider h1 as non trivial FinSequence of TOP-REAL 2 by NAT_D:60;
A8: h1 is s.n.c. by A6,Th20;
len h1 in dom h1 by A7,FINSEQ_3:25;
then
A9: h1/.len h1 = f/.(1+1) by A7,FINSEQ_4:70;
1 <= len f by A2,Th3,XXREAL_0:2;
then
A10: len h2 = len f - 1 by RFINSEQ:def 1;
then
A11: len h2 + 1 = len f;
A12: dom h1 c= dom f by FINSEQ_5:18;
A13: for n being Nat st n in dom h1 ex i,j be Nat st [
i,j] in Indices G & h1/.n=G*(i,j)
proof
let n be Nat;
assume
A14: n in dom h1;
then consider i,j be Nat such that
A15: [i,j] in Indices G and
A16: f/.n=G*(i,j) by A1,A12;
reconsider i, j as Nat;
take i,j;
thus [i,j] in Indices G by A15;
thus thesis by A14,A16,FINSEQ_4:70;
end;
h1 is one-to-one by A5,Th3,Th22;
then consider g1 such that
A17: g1 is_sequence_on G and
A18: g1 is one-to-one unfolded s.n.c. special and
A19: L~h1 = L~g1 and
A20: h1/.1 = g1/.1 and
A21: h1/.len h1 = g1/.len g1 and
A22: len h1 <= len g1 by A13,A8,GOBOARD3:1;
reconsider g1 as non trivial FinSequence of TOP-REAL 2 by A7,A22,NAT_D:60;
A23: 1 <= len g1 -'1 by A7,A22,NAT_D:55;
len g1 -'1 +1 = len g1 by A7,A22,XREAL_1:235,XXREAL_0:2;
then
A24: g1/.len g1 in LSeg(g1,len g1 -'1) by A23,TOPREAL1:21;
A25: LSeg(g1,len g1 -' 1) c= L~g1 by TOPREAL3:19;
A26: len h2 > 1+1-1 by A6,A10,XREAL_1:9;
then
A27: len h2 >= 2 by NAT_1:13;
then reconsider h2 as non trivial FinSequence of TOP-REAL 2 by NAT_D:60;
A28: h2 is s.n.c. by Th21;
A29: len h2 in dom h2 by FINSEQ_5:6;
A30: 1 in dom h1 by FINSEQ_5:6;
then
A31: h1/.1 = f/.1 by FINSEQ_4:70;
then
A32: h1/.1 = f/.len f by FINSEQ_6:def 1
.= h2/.len h2 by A11,A29,FINSEQ_5:27;
A33: for n being Nat st n in dom h2 ex i,j be Nat st [
i,j] in Indices G & h2/.n=G*(i,j)
proof
let n be Nat;
assume
A34: n in dom h2;
then consider i,j be Nat such that
A35: [i,j] in Indices G and
A36: f/.(n+1)=G*(i,j) by A1,FINSEQ_5:26;
reconsider i, j as Nat;
take i,j;
thus [i,j] in Indices G by A35;
thus thesis by A34,A36,FINSEQ_5:27;
end;
h2 is one-to-one by A5,Th24;
then consider g2 such that
A37: g2 is_sequence_on G and
A38: g2 is one-to-one unfolded s.n.c. special and
A39: L~h2 = L~g2 and
A40: h2/.1 = g2/.1 and
A41: h2/.len h2 = g2/.len g2 and
A42: len h2 <= len g2 by A33,A28,GOBOARD3:1;
A43: len g2 >= 1+1 by A27,A42,XXREAL_0:2;
then reconsider g2 as non trivial FinSequence of TOP-REAL 2 by NAT_D:60;
A44: len g2 -'1 +1 = len g2 by A43,XREAL_1:235,XXREAL_0:2;
A45: LSeg(g2,1) c= L~g2 by TOPREAL3:19;
take g = g1 ^' g2;
1 in dom h2 by A26,FINSEQ_3:25;
then
A46: h1/.len h1= h2/.1 by A9,FINSEQ_5:27;
hence g is_sequence_on G by A17,A21,A37,A40,Th12;
LSeg(f,1) /\ L~h2 = {h1/.1,h2/.1} by A5,A9,A46,A31,Th27;
then
A47: L~g1 /\ L~g2 = {g1/.1,g2/.1} by A19,A20,A39,A40,Th19;
len h2 > 3+1-1 by A5,A10,XREAL_1:9;
then 2+1 < len g2 by A42,XXREAL_0:2;
then
A48: 1+1 < len g2 -' 1 by NAT_D:52;
then 1 <= len g2-'1 by NAT_1:13;
then
A49: g2/.len g2 in LSeg(g2,len g2-'1) by A44,TOPREAL1:21;
LSeg(g2,1) misses LSeg(g2,len g2-'1) by A38,A48;
then not g2/.len g2 in LSeg(g2,1) by A49,XBOOLE_0:3;
then
A50: not g2/.len g2 in LSeg(g1,len g1 -' 1) /\ LSeg(g2,1) by XBOOLE_0:def 4;
g2/.1 in LSeg(g2,1) by A43,TOPREAL1:21;
then g2/.1 in LSeg(g1,len g1 -' 1) /\ LSeg(g2,1) by A21,A40,A46,A24,
XBOOLE_0:def 4;
then LSeg(g1,len g1 -' 1) /\ LSeg(g2,1) = { g2/.1 } by A20,A41,A32,A47,A50
,A25,A45,Th1,XBOOLE_1:27;
hence g is unfolded by A18,A21,A38,A40,A46,Th34;
thus g is s.c.c. by A18,A20,A21,A38,A40,A41,A46,A32,A47,Th33;
thus g is special by A18,A21,A38,A40,A46,Th26;
A51: (1+1, len h2)-cut h2 = h2/^1 by Th13;
A52: f = h1^(f/^(1+1)) by RFINSEQ:8
.= h1^(2, len h2)-cut h2 by A51,FINSEQ_6:81
.= h1^'h2 by FINSEQ_6:def 5;
then
A53: len f + 1 = len h1 + len h2 by FINSEQ_6:139;
thus L~f = L~h1 \/ L~h2 by A52,A46,Th35
.= L~g by A19,A21,A39,A40,A46,Th35;
thus f/.1 = h1/.1 by A30,FINSEQ_4:70
.= g/.1 by A20,FINSEQ_6:155;
thus f/.len f = h2/.len h2 by A11,A29,FINSEQ_5:27
.= g/.len g by A41,FINSEQ_6:156;
len g + 1 = len g1 + len g2 by FINSEQ_6:139;
then len f +1 <= len g +1 by A22,A42,A53,XREAL_1:7;
hence thesis by XREAL_1:6;
end;