:: Some Properties of Restrictions of Finite Sequences
:: by Czes\law Byli\'nski
::
:: Received January 25, 1995
:: Copyright (c) 1995-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, XXREAL_0, ARYTM_1, ARYTM_3, SUBSET_1, FINSEQ_1,
CARD_1, FUNCT_1, RELAT_1, FINSEQ_4, ZFMISC_1, XBOOLE_0, ORDINAL4, TARSKI,
PARTFUN1, RFINSEQ, FINSEQ_3, FINSEQ_5, NUMBER09;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, ORDINAL1, NUMBERS, NAT_1,
RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_3, FINSEQ_4, ZFMISC_1,
RFINSEQ, NAT_D, XXREAL_0;
constructors XXREAL_0, NAT_1, INT_1, PARTFUN1, FINSEQ_4, ZFMISC_1, RFINSEQ,
NAT_D, REAL_1, RELSET_1, FINSEQ_3;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, INT_1,
FINSEQ_1, CARD_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FUNCT_1, XBOOLE_0;
equalities FINSEQ_1;
expansions FUNCT_1, FINSEQ_1;
theorems TARSKI, NAT_1, PARTFUN2, FUNCT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3,
FINSEQ_4, RFINSEQ, RELAT_1, INT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0,
ORDINAL1, PARTFUN1, XREAL_0, NAT_D;
schemes FINSEQ_1;
begin
reserve i,j,k,n for Nat;
theorem Th1:
for i, n being Nat holds i <= n implies n - i + 1 is Element of NAT
proof
let i, n be Nat;
assume i <= n;
then reconsider ni = n - i as Element of NAT by INT_1:5;
ni + 1 is Element of NAT;
hence thesis;
end;
theorem Th2:
for i,n being Nat holds i in Seg n implies n - i + 1 in Seg n
proof
let i,n be Nat;
assume
A1: i in Seg n;
then i <= n by FINSEQ_1:1;
then reconsider ni = n - i as Element of NAT by INT_1:5;
reconsider j = ni + 1 as Element of NAT;
A2: now
assume j = n + 1;
then -0 = -i;
hence contradiction by A1,FINSEQ_1:1;
end;
j <= n + 1 by XREAL_1:6,XREAL_1:43;
then j < n + 1 by A2,XXREAL_0:1;
then 0+1 <= j & j <= n by NAT_1:13;
hence thesis;
end;
theorem Th3:
for f being Function, x,y being object st f"{y} = {x} holds x in dom
f & y in rng f & f.x = y
proof
let f be Function, x,y be object;
assume f"{y} = {x};
then
A1: x in f"{y} by TARSKI:def 1;
hence
A2: x in dom f by FUNCT_1:def 7;
f.x in {y} by A1,FUNCT_1:def 7;
then f.x = y by TARSKI:def 1;
hence thesis by A2,FUNCT_1:def 3;
end;
theorem
for f being Function holds f is one-to-one iff for x being set st x in
dom f holds f"{f.x} = {x}
proof
let f be Function;
now
hereby
assume
A1: for x being object st x in dom f holds f is_one-to-one_at x;
let x be object;
assume x in dom f;
then f is_one-to-one_at x by A1;
hence f"{f.x} = {x} by FINSEQ_4:2;
end;
assume
A2: for x being object st x in dom f holds f"{f.x} = {x};
let x be object;
assume
A3: x in dom f;
then f"{f.x} = {x} by A2;
hence f is_one-to-one_at x by A3,FINSEQ_4:2;
end;
hence thesis by FINSEQ_4:4;
end;
theorem
for f being Function, y1,y2 being object st f is one-to-one & y1 in rng f
& f"{y1} = f"{y2} holds y1 = y2
proof
let f be Function, y1,y2 be object such that
A1: f is one-to-one & y1 in rng f and
A2: f"{y1} = f"{y2};
consider x1 being object such that
A3: f"{y1} = {x1} by A1,FUNCT_1:74;
f.x1 = y1 by A3,Th3;
hence thesis by A2,A3,Th3;
end;
registration
let x be object;
cluster <*x*> -> trivial;
coherence;
let y be object;
cluster <*x,y*> -> non trivial;
coherence
proof
len <*x,y*> = 2 by FINSEQ_1:44;
hence thesis by NAT_D:60;
end;
end;
registration
cluster one-to-one non empty for FinSequence;
existence
proof
set f = <*{}*>;
f is one-to-one by FINSEQ_3:93;
hence thesis;
end;
end;
theorem Th6:
for f being non empty FinSequence holds 1 in dom f & len f in dom f
proof
let f be non empty FinSequence;
A1: len f >= 1 by NAT_1:14;
hence 1 in dom f by FINSEQ_3:25;
thus thesis by A1,FINSEQ_3:25;
end;
theorem
for f being non empty FinSequence ex i being Nat st i+1 = len f by NAT_1:6;
theorem Th8:
for x being object, f being FinSequence holds len(<*x*>^f) = 1 + len f
proof
let x be object, f be FinSequence;
thus len(<*x*>^f) = len <*x*> + len f by FINSEQ_1:22
.= 1 + len f by FINSEQ_1:39;
end;
theorem
for f being FinSequence, p,q being set st p in rng f & q in rng f &
p..f = q..f holds p = q
proof
let f be FinSequence, p,q be set such that
A1: p in rng f and
A2: q in rng f;
assume p..f = q..f;
hence p = f.(q..f) by A1,FINSEQ_4:19
.= q by A2,FINSEQ_4:19;
end;
theorem Th10:
for f,g being FinSequence st n+1 in dom f & g = f|Seg n holds
f|Seg(n+1) = g^<*f.(n+1)*>
proof
let f,g be FinSequence such that
A1: n+1 in dom f and
A2: g = f|Seg n;
reconsider h = f|Seg(n+1) as FinSequence by FINSEQ_1:15;
n+1 <= len f by A1,FINSEQ_3:25;
then
A3: len h = n+1 by FINSEQ_1:17;
Seg n c= Seg(n+1) by FINSEQ_1:5,NAT_1:11;
then h.(n+1) = f.(n+1) & g = h|Seg n by A2,FINSEQ_1:4,FUNCT_1:49,51;
hence thesis by A3,FINSEQ_3:55;
end;
theorem Th11:
for f being one-to-one FinSequence st i in dom f holds (f.i)..f = i
proof
let f be one-to-one FinSequence;
assume
A1: i in dom f;
then f.i in rng f by FUNCT_1:def 3;
then
A2: f just_once_values f.i by FINSEQ_4:8;
then f <- (f.i) = (f.i)..f by FINSEQ_4:25;
hence thesis by A1,A2,FINSEQ_4:def 3;
end;
reserve D for non empty set,
p for Element of D,
f,g for FinSequence of D;
registration
let D be non empty set;
cluster one-to-one non empty for FinSequence of D;
existence
proof
set x = the Element of D;
set f = <*x*>;
f is one-to-one by FINSEQ_3:93;
hence thesis;
end;
end;
:: FINSEQ_1:17
theorem
dom f = dom g & (for i st i in dom f holds f/.i = g/.i) implies f = g
proof
assume that
A1: dom f = dom g and
A2: for i st i in dom f holds f/.i = g/.i;
now
let k be Nat;
assume
A3: k in dom f;
hence f.k = f/.k by PARTFUN1:def 6
.= g/.k by A2,A3
.= g.k by A1,A3,PARTFUN1:def 6;
end;
hence thesis by A1;
end;
:: FINSEQ_1:18
theorem
len f = len g & (for k st 1 <= k & k <= len f holds f/.k = g/.k)
implies f = g
proof
assume that
A1: len f = len g and
A2: for k st 1 <= k & k <= len f holds f/.k = g/.k;
now
let k be Nat;
assume
A3: 1 <= k & k <= len f;
hence f.k = f/.k by FINSEQ_4:15
.= g/.k by A2,A3
.= g.k by A1,A3,FINSEQ_4:15;
end;
hence thesis by A1;
end;
theorem Th14:
for f being FinSequence st len f = 1 holds f = <*f.1*> by FINSEQ_1:40;
theorem Th15:
(<*p*>^f)/.1 = p
proof
len(<*p*>^f) = 1 + len f by Th8;
then 1 <= len(<*p*>^f) by NAT_1:11;
then 1 in dom(<*p*>^f) by FINSEQ_3:25;
then (<*p*>^f)/.1 = (<*p*>^f).1 by PARTFUN1:def 6;
hence thesis by FINSEQ_1:41;
end;
Lm1: i in dom f implies (f^g).i=f.i by FINSEQ_1:def 7;
theorem Th16:
for f being FinSequence, i being Nat holds len(f|i) <= len f
proof
let f be FinSequence, i be Nat;
i <= len f implies len(f|i) = i by FINSEQ_1:59;
hence thesis by FINSEQ_1:58;
end;
theorem Th17:
for f being FinSequence, i being Nat holds len(f|i) <= i
proof
let f be FinSequence, i be Nat;
i <= len f implies len(f|i) = i by FINSEQ_1:59;
hence thesis by FINSEQ_1:58;
end;
theorem Th18:
for f being FinSequence, i being Nat holds dom(f|i) c= dom f
proof
let f be FinSequence, i be Nat;
f|i c= f by RELAT_1:59;
hence thesis by RELAT_1:11;
end;
theorem Th19:
for f being FinSequence, i being Nat holds rng(f|i) c= rng f
proof
let f be FinSequence, i be Nat;
f|i c= f by RELAT_1:59;
hence thesis by RELAT_1:11;
end;
theorem Th20:
for f being FinSequence st f is non empty holds f|1 = <*f.1*>
proof
let f be FinSequence;
assume f is non empty;
then 1 in dom f by Th6;
then 1 <= len f by FINSEQ_3:25; then
A1: len(f|1) = 1 by FINSEQ_1:59;
(f|Seg 1).1 = f.1 by FINSEQ_1:1,FUNCT_1:49;
hence thesis by A1,FINSEQ_1:40;
end;
theorem
i+1 = len f implies f = (f|i)^<*f/.len f*>
proof
assume
A1: i+1 = len f;
then f is non empty;
then
A2: i+1 in dom f by A1,Th6;
dom f = Seg(i+1) by A1,FINSEQ_1:def 3;
hence f = f|Seg(i+1)
.= (f|i)^<*f.(i+1)*> by A2,Th10
.= (f|i)^<*f/.len f*> by A1,A2,PARTFUN1:def 6;
end;
Lm2: f is one-to-one implies f|i is one-to-one
proof
assume
A1: f is one-to-one;
now
A2: dom(f|i) c= dom f by Th18;
let n,m be Element of NAT such that
A3: n in dom(f|i) and
A4: m in dom(f|i) and
A5: (f|i)/.n = (f|i)/.m;
f/.n = (f|i)/.n by A3,FINSEQ_4:70
.= f/.m by A4,A5,FINSEQ_4:70;
hence n = m by A1,A3,A4,A2,PARTFUN2:10;
end;
hence thesis by PARTFUN2:9;
end;
registration
let i,D;
let f be one-to-one FinSequence of D;
cluster f|i -> one-to-one;
coherence by Lm2;
end;
theorem Th22:
for f, g being FinSequence st i <= len f holds (f^g)|i = f|i
proof
let f, g be FinSequence;
assume
A1: i <= len f;
then
A2: len(f|i) = i by FINSEQ_1:59;
then
A3: dom(f|i) = Seg i by FINSEQ_1:def 3;
A4: now
let j be Nat;
assume
A5: j in dom(f|i);
then j <= i by A3,FINSEQ_1:1;
then
A6: j <= len f by A1,XXREAL_0:2;
j in NAT & 1 <= j by A3,A5,FINSEQ_1:1;
then j in Seg len f by A6;
then
A7: j in dom f by FINSEQ_1:def 3;
thus ((f^g)|i).j = (f^g).j by A3,A5,FUNCT_1:49
.= f.j by A7,FINSEQ_1:def 7
.= (f|i).j by A3,A5,FUNCT_1:49;
end;
i <= len f+len g by A1,NAT_1:12;
then i <= len(f^g) by FINSEQ_1:22;
then len((f^g)|i) = i by FINSEQ_1:59;
hence thesis by A2,A4,FINSEQ_2:9;
end;
theorem
for f, g being FinSequence holds (f^g)|(len f) = f
proof
let f, g be FinSequence;
thus f = f|len f by FINSEQ_2:20
.= (f^g)|(len f) by Th22;
end;
theorem
for f being FinSequence st p in rng f holds (f-|p)^<*p*> = f|(p..f)
proof
let f be FinSequence;
assume
A1: p in rng f;
then consider n being Nat such that
A2: n = p..f - 1 and
A3: f-|p = f | Seg n by FINSEQ_4:def 5;
n+1 in dom f & f.(n+1) = p by A1,A2,FINSEQ_4:19,20;
hence thesis by A2,A3,Th10;
end;
theorem
for f being FinSequence holds len(f/^i) <= len f
proof
let f be FinSequence;
per cases;
suppose
i <= len f;
then len(f/^i) = len f - i by RFINSEQ:def 1;
then len(f/^i)+i = len f;
hence thesis by NAT_1:11;
end;
suppose
len f < i;
then f/^i = {} by RFINSEQ:def 1;
hence thesis;
end;
end;
theorem Th26:
for f being FinSequence st i in dom(f/^n) holds n+i in dom f
proof
let f be FinSequence;
assume
A1: i in dom(f/^n);
per cases;
suppose
A2: n <= len f;
i <= len(f/^n) by A1,FINSEQ_3:25;
then i <= len f - n by A2,RFINSEQ:def 1;
then
A3: n+i <= len f by XREAL_1:19;
1 <= i & i <= i+n by A1,FINSEQ_3:25,NAT_1:11;
then 1 <= i+n by XXREAL_0:2;
hence thesis by A3,FINSEQ_3:25;
end;
suppose
n > len f;
then f/^n = {} by RFINSEQ:def 1;
hence thesis by A1;
end;
end;
theorem Th27:
(for f being FinSequence st i in dom(f/^n) holds (f/^n).i = f.(n+i)) &
(i in dom(f/^n) implies (f/^n)/.i = f/.(n+i))
proof
thus AA: for f being FinSequence st i in dom(f/^n) holds (f/^n).i = f.(n+i)
proof let f be FinSequence;
assume
A1: i in dom(f/^n);
per cases;
suppose
n <= len f;
hence (f/^n).i = f.(n+i) by A1,RFINSEQ:def 1;
end;
suppose
n > len f;
then f/^n = {} by RFINSEQ:def 1;
hence (f/^n).i = f.(n+i) by A1;
end;
end;
assume B1: i in dom (f/^n); then
B2: n+i in dom f by Th26;
(f/^n).i = f.(n+i) by AA,B1; then
(f/^n)/.i = f.(n+i) by B1,PARTFUN1:def 6 .= f/.(n+i) by PARTFUN1:def 6,B2;
hence thesis;
end;
theorem Th28:
for f being FinSequence holds f/^0 = f
proof
let f be FinSequence;
A1: 0 <= len f;
A2: now
let i be Nat;
assume 1 <= i & i <= len(f/^0);
then i in dom(f/^0) by FINSEQ_3:25;
hence (f/^0).i = f.(i+0) by A1,RFINSEQ:def 1
.= f.i;
end;
len(f/^0) = len f - 0 by RFINSEQ:def 1;
hence thesis by A2;
end;
registration
let f be FinSequence;
reduce f /^ 0 to f;
reducibility by Th28;
end;
theorem
f is non empty implies f = <*f/.1*>^(f/^1)
proof
assume A1: f is non empty; then
A2: 1 in dom f by Th6;
f|1 = <*f.1*> by A1,Th20
.= <*f/.1*> by A2,PARTFUN1:def 6;
hence thesis by RFINSEQ:8;
end;
theorem
for f being FinSequence st i+1 = len f holds f/^i = <*f.len f*>
proof
let f be FinSequence;
assume
A1: i+1 = len f;
then i <= len f by NAT_1:11;
then
A2: len(f/^i) = len f - i by RFINSEQ:def 1
.= 1 by A1;
then
A3: 1 in dom(f/^i) by FINSEQ_3:25;
thus f/^i = <*(f/^i).1*> by A2,Th14
.= <*f.len f*> by A1,A3,Th27;
end;
theorem Th31:
j+1 = i & i in dom f implies <*f/.i*>^(f/^i) = f/^j
proof
assume that
A1: j+1 = i and
A2: i in dom f;
set g = <*f/.i*>^(f/^i);
A3: i <= len f by A2,FINSEQ_3:25;
j <= i by A1,NAT_1:11;
then
A4: j <= len f by A3,XXREAL_0:2;
A5: len g = len(f/^i) + 1 by Th8;
then
A6: len g = len f - i + 1 by A3,RFINSEQ:def 1
.= len f - j by A1
.= len(f/^j) by A4,RFINSEQ:def 1;
now
let k be Nat;
assume that
A7: 1 <= k and
A8: k <= len g;
A9: k in dom(f/^j) by A6,A7,A8,FINSEQ_3:25;
per cases;
suppose
A10: k = 1;
hence g.k = f/.i by FINSEQ_1:41
.= f.i by A2,PARTFUN1:def 6
.= (f/^j).k by A1,A4,A9,A10,RFINSEQ:def 1;
end;
suppose
k <> 1;
then
A11: 1 < k by A7,XXREAL_0:1;
reconsider k9 = k-1 as Element of NAT by A7,INT_1:5;
A12: k9 <= len g - 1 by A8,XREAL_1:9;
k9+1 = k;
then 1 <= k9 by A11,NAT_1:13;
then
A13: k9 in dom(f/^i) by A5,A12,FINSEQ_3:25;
len <*f/.i*> = 1 by FINSEQ_1:39;
hence g.k = (f/^i).k9 by A8,A11,FINSEQ_1:24
.= f.(k9+i) by A3,A13,RFINSEQ:def 1
.= f.(k+j) by A1
.= (f/^j).k by A4,A9,RFINSEQ:def 1;
end;
end;
hence thesis by A6;
end;
theorem Th32:
for f being FinSequence st len f <= i holds f/^i is empty
proof
let f be FinSequence;
assume
A1: len f <= i;
per cases;
suppose
len f = i;
then len(f/^i) = len f - len f by RFINSEQ:def 1
.= 0;
hence thesis;
end;
suppose
len f <> i;
then len f < i by A1,XXREAL_0:1;
hence thesis by RFINSEQ:def 1;
end;
end;
theorem Th33:
for f being FinSequence holds rng(f/^n) c= rng f
proof
let f be FinSequence;
let p be object;
assume p in rng(f/^n);
then consider j being object such that
A1: j in dom(f/^n) and
A2: (f/^n).j = p by FUNCT_1:def 3;
reconsider jj = j as Nat by A1;
jj+n in dom f by A1,Th26;
then f.(jj+n) in rng f by FUNCT_1:def 3;
hence thesis by A1,A2,Th27;
end;
Lm3: f is one-to-one implies f/^i is one-to-one
proof
assume
A1: f is one-to-one;
now
let n,m be Element of NAT such that
A2: n in dom(f/^i) and
A3: m in dom(f/^i) and
A4: (f/^i).n = (f/^i).m;
A5: i+n in dom f & i+m in dom f by A2,A3,Th26;
f.(i+n) = (f/^i).n by A2,Th27
.= f.(i+m) by A3,A4,Th27;
then i+n = i+m by A1,A5;
hence n = m;
end;
hence thesis;
end;
registration
let i,D;
let f be one-to-one FinSequence of D;
cluster f/^i -> one-to-one;
coherence by Lm3;
end;
theorem Th34:
for f being FinSequence st
f is one-to-one holds rng(f|n) misses rng(f/^n)
proof
let f be FinSequence;
assume
A1: f is one-to-one;
A2: dom(f|n) c= dom f by Th18;
assume rng(f|n) meets rng(f/^n);
then consider x being object such that
A3: x in rng(f|n) and
A4: x in rng(f/^n) by XBOOLE_0:3;
consider i being object such that
A5: i in dom(f|n) and
A6: (f|n).i = x by A3,FUNCT_1:def 3;
consider j being object such that
A7: j in dom(f/^n) and
A8: (f/^n).j = x by A4,FUNCT_1:def 3;
reconsider ii = i, jj = j as Nat by A7,A5;
A9: jj+n in dom f by A7,Th26;
A10: now
ii <= len(f|n) & len(f|n) <= n by A5,Th17,FINSEQ_3:25;
then
A11: ii <= n by XXREAL_0:2;
assume
A12: ii = jj+n;
then n <= ii by NAT_1:11;
then i = n by A11,XXREAL_0:1;
then j = 0 by A12;
hence contradiction by A7,FINSEQ_3:25;
end;
f.(jj+n) = (f/^n).j by A7,Th27
.= f.i by A5,FUNCT_1:47,A6,A8;
hence contradiction by A1,A5,A2,A9,A10;
end;
theorem
p in rng f implies f |-- p = f/^(p..f)
proof
assume
A1: p in rng f;
then
A2: len (f|--p) = len f - p..f by FINSEQ_4:def 6;
A3: p..f <= len f by A1,FINSEQ_4:21;
then
A4: len (f/^(p..f)) = len f - p..f by RFINSEQ:def 1;
A5: Seg len (f|--p) = dom (f|--p) & Seg len (f/^(p..f)) = dom (f/^(p..f)) by
FINSEQ_1:def 3;
now
let i be Nat;
assume
A6: i in dom (f|--p);
hence (f|--p).i = f.(i + p..f) by A1,FINSEQ_4:def 6
.= (f/^(p..f)).i by A2,A3,A4,A5,A6,RFINSEQ:def 1;
end;
hence thesis by A2,A4,FINSEQ_2:9;
end;
theorem Th36:
for f, g being FinSequence holds (f^g)/^(len f + i) = g/^i
proof
let f, g be FinSequence;
A1: len(f^g) = len f + len g by FINSEQ_1:22;
per cases;
suppose
A2: i <= len g;
then len f + i <= len f + len g by XREAL_1:6;
then
A3: len((f^g)/^(len f + i)) = len g + len f - (len f + i) by A1,RFINSEQ:def 1
.= len g - i
.= len(g/^i) by A2,RFINSEQ:def 1;
now
let k;
assume
A4: 1 <= k & k <= len(g/^i);
then
A5: k in dom(g/^i) by FINSEQ_3:25;
then
A6: i+k in dom g by Th26;
k in dom((f^g)/^(len f + i)) by A3,A4,FINSEQ_3:25;
hence ((f^g)/^(len f + i)).k = (f^g).(len f + i + k) by Th27
.= (f^g).(len f + (i+k))
.= g.(i+k) by A6,FINSEQ_1:def 7
.= (g/^i).k by A5,Th27;
end;
hence thesis by A3;
end;
suppose
A7: i > len g;
then len f + i > len(f^g) by A1,XREAL_1:6;
hence (f^g)/^(len f+i) = {} by RFINSEQ:def 1
.= g/^i by A7,RFINSEQ:def 1;
end;
end;
theorem Th37:
for f, g being FinSequence holds (f^g)/^(len f) = g
proof
let f, g be FinSequence;
thus (f^g)/^(len f) = (f^g)/^(len f + 0) .= g/^0 by Th36
.= g;
end;
registration
let f,g be FinSequence;
reduce (f^g)/^(len f) to g;
reducibility by Th37;
end;
theorem Th38:
p in rng f implies f/.(p..f) = p
proof
assume p in rng f;
then p..f in dom f & f.(p..f) = p by FINSEQ_4:19,20;
hence thesis by PARTFUN1:def 6;
end;
theorem Th39:
i in dom f implies f/.i..f <= i
proof
set p = f/.i;
A1: p..f = Sgm(f"{p}).1 by FINSEQ_4:def 4;
f"{p} c= dom f by RELAT_1:132;
then f"{p} c= Seg len f by FINSEQ_1:def 3;
then
a2: f"{p} is included_in_Seg;
assume
A3: i in dom f;
then f/.i = f.i by PARTFUN1:def 6;
then f.i in {p} by TARSKI:def 1;
then i in f"{p} by A3,FUNCT_1:def 7;
then i in rng Sgm(f"{p}) by a2,FINSEQ_1:def 14;
then consider l being object such that
A4: l in dom Sgm(f"{p}) and
A5: Sgm(f"{p}).l = i by FUNCT_1:def 3;
reconsider l as Element of NAT by A4;
1 <= l & l <= len(Sgm(f"{p})) by A4,FINSEQ_3:25;
hence thesis by a2,A1,A5,FINSEQ_3:41;
end;
theorem
p in rng(f|i) implies p..(f|i) = p..f
proof
A1: dom(f|i) c= dom f by Th18;
assume
A2: p in rng(f|i);
then
A3: p..(f|i) in dom(f|i) by FINSEQ_4:20;
then f/.(p..(f|i)) = (f|i)/.(p..(f|i)) by FINSEQ_4:70
.= p by A2,Th38;
then
A4: p..f <= p..(f|i) by A3,A1,Th39;
p..(f|i) <= len(f|i) by A2,FINSEQ_4:21;
then
A5: p..f <= len(f|i) by A4,XXREAL_0:2;
A6: rng(f|i) c= rng f by Th19;
then 1 <= p..f by A2,FINSEQ_4:21;
then
A7: p..f in dom(f|i) by A5,FINSEQ_3:25;
then (f|i)/.(p..f) = f/.(p..f) by FINSEQ_4:70
.= p by A2,A6,Th38;
then p..(f|i) <= p..f by A7,Th39;
hence thesis by A4,XXREAL_0:1;
end;
theorem
i in dom f & f is one-to-one implies f/.i..f = i
proof
assume
A1: i in dom f;
assume f is one-to-one;
then (f.i)..f = i by A1,Th11;
hence thesis by A1,PARTFUN1:def 6;
end;
definition
let D, f;
let p be set;
func f-:p -> FinSequence of D equals
f|(p..f);
correctness;
end;
theorem Th42:
p in rng f implies len(f-:p) = p..f
proof
assume p in rng f;
then p..f in dom f by FINSEQ_4:20;
then p..f <= len f by FINSEQ_3:25;
hence thesis by FINSEQ_1:59;
end;
theorem Th43:
p in rng f & i in Seg(p..f) implies (f-:p)/.i = f/.i
proof
assume that
A1: p in rng f and
A2: i in Seg(p..f);
p..f in dom f by A1,FINSEQ_4:20;
hence thesis by A2,FINSEQ_4:71;
end;
theorem
p in rng f implies (f-:p)/.1 = f/.1
proof
assume
A1: p in rng f;
then 1 <= p..f by FINSEQ_4:21;
then 1 in Seg(p..f);
hence thesis by A1,Th43;
end;
theorem
p in rng f implies (f-:p)/.(p..f) = p
proof
assume
A1: p in rng f;
then
A2: p..f in dom f by FINSEQ_4:20;
1 <= p..f by A1,FINSEQ_4:21;
then p..f in Seg(p..f);
hence (f-:p)/.(p..f) = f/.(p..f) by A1,Th43
.= f.(p..f) by A2,PARTFUN1:def 6
.= p by A1,FINSEQ_4:19;
end;
theorem
for x being set st x in rng f & p in rng f & x..f<=p..f holds x in rng(f-:p)
proof
let x be set;
assume that
A1: x in rng f and
A2: p in rng f and
A3: x..f<=p..f;
set g = f-:p, i = x..f;
1 <= i by A1,FINSEQ_4:21;
then
A4: i in Seg (p..f) by A3;
Seg len g = dom g by FINSEQ_1:def 3;
then
A5: i in dom g by A2,A4,Th42;
then g.i in rng g by FUNCT_1:def 3;
then g/.i in rng g by A5,PARTFUN1:def 6;
then
A6: f/.i in rng g by A2,A4,Th43;
i in dom f by A1,FINSEQ_4:20;
then f.i in rng g by A6,PARTFUN1:def 6;
hence thesis by A1,FINSEQ_4:19;
end;
theorem
p in rng f implies f-:p is non empty
proof
assume
A1: p in rng f;
then 1 <= p..f by FINSEQ_4:21;
then 1 <= len(f-:p) by A1,Th42;
hence thesis;
end;
theorem
rng(f-:p) c= rng f by Th19;
registration
let D,p;
let f be one-to-one FinSequence of D;
cluster f-:p -> one-to-one;
coherence;
end;
definition
let D, f, p;
func f:-p -> FinSequence of D equals
<*p*>^(f/^p..f);
coherence;
end;
theorem Th49:
p in rng f implies ex i being Element of NAT st i+1 = p..f & f:- p = f/^i
proof
assume
A1: p in rng f;
then reconsider i = p..f - 1 as Element of NAT by FINSEQ_4:21,INT_1:5;
A2: p..f in dom f by A1,FINSEQ_4:20;
take i;
thus
A3: i+1 = p..f;
thus f:-p = <*f/.(p..f)*>^(f/^p..f) by A1,Th38
.= f/^i by A3,A2,Th31;
end;
theorem Th50:
p in rng f implies len (f:-p) = len f - p..f + 1
proof
assume
A1: p in rng f;
then
A2: p..f <= len f by FINSEQ_4:21;
consider i being Element of NAT such that
A3: i+1 = p..f and
A4: f:-p = f/^i by A1,Th49;
i <= p..f by A3,NAT_1:11;
then i <= len f by A2,XXREAL_0:2;
hence len(f:-p) = len f - i by A4,RFINSEQ:def 1
.= len f - p..f + 1 by A3;
end;
theorem Th51:
p in rng f & j+1 in dom(f:-p) implies j+p..f in dom f
proof
assume that
A1: p in rng f and
A2: j+1 in dom(f:-p);
j+1 <= len(f:-p) by A2,FINSEQ_3:25;
then j+1 <= len f - p..f + 1 by A1,Th50;
then j <= len f - p..f by XREAL_1:6;
then
A3: j+p..f <= len f by XREAL_1:19;
A4: p..f <= j+p..f by NAT_1:11;
1 <= p..f by A1,FINSEQ_4:21;
then 1 <= j+p..f by A4,XXREAL_0:2;
hence thesis by A3,FINSEQ_3:25;
end;
registration
let D,p,f;
cluster f:-p -> non empty;
coherence;
end;
theorem Th52:
p in rng f & j+1 in dom(f:-p) implies (f:-p)/.(j+1) = f/.(j+p..f )
proof
assume that
A1: p in rng f and
A2: j+1 in dom(f:-p);
A3: j+p..f in dom f by A1,A2,Th51;
set i = j+1;
A4: p..f <= len f by A1,FINSEQ_4:21;
consider k being Element of NAT such that
A5: k+1 = p..f and
A6: f:-p = f/^k by A1,Th49;
k <= p..f by A5,NAT_1:11;
then
A7: k <= len f by A4,XXREAL_0:2;
thus (f:-p)/.i = (f:-p).i by A2,PARTFUN1:def 6
.= f.(i+k) by A2,A6,A7,RFINSEQ:def 1
.= f/.(j+p..f) by A5,A3,PARTFUN1:def 6;
end;
theorem
(f:-p)/.1 = p by Th15;
theorem
p in rng f implies (f:-p)/.(len(f:-p)) = f/.len f
proof
A1: len(f:-p) in dom(f:-p) by Th6;
assume
A2: p in rng f;
then p..f <= len f by FINSEQ_4:21;
then reconsider j = len f - p..f as Element of NAT by INT_1:5;
len(f:-p) = j + 1 by A2,Th50;
hence (f:-p)/.(len(f:-p)) = f/.(j+p..f) by A2,A1,Th52
.= f/.len f;
end;
theorem
p in rng f implies rng(f:-p) c= rng f
proof
assume p in rng f;
then ex i being Element of NAT st i+1 = p..f & f:-p = f/^i by Th49;
hence thesis by Th33;
end;
theorem
p in rng f & f is one-to-one implies f:-p is one-to-one
proof
assume p in rng f;
then ex i being Element of NAT st i+1 = p..f & f:-p = f/^i by Th49;
hence thesis;
end;
definition
let f be FinSequence;
func Rev f -> FinSequence means :Def3:
len it = len f & for i st i in dom it holds it.i = f.(len f - i + 1);
existence
proof
deffunc F(Nat) = f.(len f - $1 + 1);
ex p being FinSequence st len p = len f & for k being Nat st k in dom
p holds p.k = F(k) from FINSEQ_1:sch 2;
hence thesis;
end;
uniqueness
proof
A1: dom f = Seg len f by FINSEQ_1:def 3;
let f1,f2 be FinSequence such that
A2: len f1 = len f and
A3: for i st i in dom f1 holds f1.i = f.(len f - i + 1) and
A4: len f2 = len f and
A5: for i st i in dom f2 holds f2.i = f.(len f - i + 1);
A6: dom f1 = Seg len f1 by FINSEQ_1:def 3;
A7: dom f2 = Seg len f2 by FINSEQ_1:def 3;
now
let i be Nat;
assume
A8: i in dom f;
then f1.i = f.(len f - i + 1) by A2,A3,A6,A1;
hence f1.i = f2.i by A4,A5,A7,A1,A8;
end;
hence thesis by A2,A4,A6,A1,FINSEQ_2:9;
end;
involutiveness
proof let g,f be FinSequence;
assume that
A9: len g = len f and
A10: for i st i in dom g holds g.i = f.(len f - i + 1);
thus len f = len g by A9;
let i;
assume
A11: i in dom f;
then i in dom g by A9,FINSEQ_3:29;
then i <= len g by FINSEQ_3:25;
then reconsider j = len g - i as Element of NAT by INT_1:5;
i >= 1 by A11,FINSEQ_3:25;
then j+i >= j+1 by XREAL_1:6;
then j < len g by NAT_1:13;
then
1 <= j+1 & j+1 <= len g by NAT_1:11,13;
then
A12: j + 1 in dom g by FINSEQ_3:25;
thus f.i = f.(len f - (j+1) + 1) by A9
.= g.(len g - i + 1) by A10,A12;
end;
end;
theorem Th57:
for f being FinSequence holds dom f = dom Rev f & rng f = rng Rev f
proof
let f be FinSequence;
thus
A1: dom f = Seg len f by FINSEQ_1:def 3
.= Seg len Rev f by Def3
.= dom Rev f by FINSEQ_1:def 3;
A2: len f = len Rev f by Def3;
hereby
let x be object;
assume x in rng f;
then consider i being Nat such that
A3: i in dom f and
A4: f.i = x by FINSEQ_2:10;
i <= len f by A3,FINSEQ_3:25;
then reconsider j = len f - i + 1 as Element of NAT by Th1;
dom f = Seg len f by FINSEQ_1:def 3;
then j in Seg len (Rev f) by A2,A3,Th2;
then
A5: j in dom(Rev f) by FINSEQ_1:def 3;
then (Rev f).j = f.(len f - j + 1) by Def3;
hence x in rng(Rev f) by A4,A5,FUNCT_1:def 3;
end;
let x be object;
assume x in rng(Rev f);
then consider i being Nat such that
A6: i in dom(Rev f) and
A7: (Rev f).i = x by FINSEQ_2:10;
i <= len f by A2,A6,FINSEQ_3:25;
then reconsider j = len f - i + 1 as Element of NAT by Th1;
i in Seg len(Rev f) by A6,FINSEQ_1:def 3;
then j in Seg len (Rev f) by A2,Th2;
then
A8: j in dom (Rev f) by FINSEQ_1:def 3;
(Rev f).i = f.(len f - i + 1) by A6,Def3;
hence thesis by A1,A7,A8,FUNCT_1:def 3;
end;
theorem Th58:
for f being FinSequence st i in dom f holds (Rev f).i = f.(len f - i + 1)
proof
let f be FinSequence;
dom f = dom(Rev f) by Th57;
hence thesis by Def3;
end;
theorem Th59:
for f being FinSequence, i,j being Nat st
i in dom f & i+j = len f + 1 holds j in dom Rev f
proof
let f be FinSequence, i,j be Nat such that
A1: i in dom f and
A2: i+j = len f + 1;
A3: dom f = Seg len f & dom f = dom Rev f by Th57,FINSEQ_1:def 3;
j = len f - i + 1 by A2;
hence thesis by A1,A3,Th2;
end;
registration
let f be empty FinSequence;
cluster Rev f -> empty;
coherence
proof
len {} = 0;
then len (Rev {}) = 0 by Def3;
hence thesis;
end;
end;
theorem
for x being object holds Rev <*x*> = <*x*>
proof
let x be object;
set f = <*x*>;
A1: len f = 1 by FINSEQ_1:39;
now
let i;
assume i in dom f;
then i in Seg len f by FINSEQ_1:def 3;
then i = 1 by A1,FINSEQ_1:2,TARSKI:def 1;
hence f.i = f.(len f - i + 1) by FINSEQ_1:39;
end;
hence thesis by Def3;
end;
theorem
for x1,x2 being object holds Rev <*x1,x2*> = <*x2,x1*>
proof
let x1,x2 be object;
set f = <*x1,x2*>, g = <*x2,x1*>;
A1: len f = 2 by FINSEQ_1:44;
A2: len g = 2 by FINSEQ_1:44;
now
let i;
assume i in dom g;
then
A3: i in Seg len f by A1,A2,FINSEQ_1:def 3;
per cases by A1,A3,FINSEQ_1:2,TARSKI:def 2;
suppose
A4: i = 1;
hence g.i = x2
.= f.(len f - i + 1) by A1,A4;
end;
suppose
A5: i = 2;
hence g.i = x1
.= f.(len f - i + 1) by A1,A5;
end;
end;
hence thesis by A1,A2,Def3;
end;
theorem Th62:
for f being FinSequence holds f.1 = (Rev f).(len f) & f.(len f) = (Rev f).1
proof
let f be FinSequence;
per cases;
suppose
A1: f is empty;
hence f.1 = {}
.= (Rev f).(len f) by A1;
thus f.(len f) = {} by A1
.= (Rev f).1 by A1;
end;
suppose
A3: f is non empty;
then len f in Seg len f by FINSEQ_1:3;
then len f in dom f by FINSEQ_1:def 3;
hence (Rev f).(len f) = f.(len f - len f + 1) by Th58
.= f.1;
len f >= 1 by A3,NAT_1:14;
then 1 in dom f by FINSEQ_3:25;
hence (Rev f).1 = f.(len f - 1 + 1) by Th58
.= f.(len f);
end;
end;
registration
let f be one-to-one FinSequence;
cluster Rev f -> one-to-one;
coherence
proof
set g = Rev f;
let x1,x2 be object such that
A1: x1 in dom g and
A2: x2 in dom g and
A3: g.x1 = g.x2;
reconsider i1 = x1, i2 = x2 as Element of NAT by A1,A2;
A4: len g = len f by Def3;
then i1 <= len f & i2 <= len f by A1,A2,FINSEQ_3:25;
then reconsider
i19 = len f - i1 + 1, i29 = len f - i2 + 1 as Element of NAT by Th1;
A5: f.i19 = g.x1 by A1,Def3
.= f.i29 by A2,A3,Def3;
dom g = Seg len g & dom f = Seg len f by FINSEQ_1:def 3;
then i19 in dom f & i29 in dom f by A1,A2,A4,Th2;
then i19 = i29 by A5,FUNCT_1:def 4;
hence thesis;
end;
end;
theorem Th63:
for f being FinSequence, x being object holds Rev(f^<*x*>) = <*x*>^ (Rev f)
proof
let f be FinSequence, x be object;
set n = len f + 1, g = <*x*>;
A1: len(g^(Rev f)) = len g + len (Rev f) by FINSEQ_1:22
.= 1 + len (Rev f) by FINSEQ_1:39
.= n by Def3;
A2: len (f^g) = n by FINSEQ_2:16;
then
A3: len(Rev(f^g)) = n by Def3;
now
let i be Nat;
A4: len g = 1 by FINSEQ_1:40;
assume
A5: i in dom Rev(f^g);
then
A6: 1 <= i by FINSEQ_3:25;
A7: i <= n by A3,A5,FINSEQ_3:25;
per cases by A6,XXREAL_0:1;
suppose
A8: i = 1;
Seg len g = dom g by FINSEQ_1:def 3;
then
A9: 1 in dom g by A4;
thus (Rev(f^g)).i = (f^g).(n-1+1) by A2,A5,A8,Def3
.= g.1 by FINSEQ_1:42
.= (g^(Rev f)).i by A8,A9,FINSEQ_1:def 7;
end;
suppose
A10: i > 1;
then reconsider j = i-1 as Element of NAT by NAT_1:20;
consider l being Nat such that
A11: i = l + 1 by A10,NAT_1:6;
reconsider k = n - i + 1 as Element of NAT by A7,Th1;
n < len f + i by A10,XREAL_1:8;
then n - i < len f + i - i by XREAL_1:9;
then k < len f + 1 by XREAL_1:6;
then
A12: k <= len f by NAT_1:13;
i - i <= n - i by A7,XREAL_1:9;
then 0 + 1 <= k by XREAL_1:6;
then
A13: k in dom f by A12,FINSEQ_3:25;
l <> 0 by A10,A11;
then
A14: 1 <= j by A11,NAT_1:14;
j <= n - 1 by A7,XREAL_1:9;
then
A15: j in dom f by A14,FINSEQ_3:25;
thus (Rev(f^g)).i = (f^g).(n - i + 1) by A2,A5,Def3
.= f.(len f - j + 1) by A13,FINSEQ_1:def 7
.= (Rev f).j by A15,Th58
.= (g^(Rev f)).i by A1,A7,A4,A10,FINSEQ_1:24;
end;
end;
hence thesis by A1,A3,FINSEQ_2:9;
end;
theorem
for f,g being FinSequence holds Rev(f^g) = (Rev g)^(Rev f)
proof
let f be FinSequence;
defpred P[FinSequence] means Rev(f^$1) = (Rev $1)^(Rev f);
A1: P[{}]
proof
set g = {};
thus Rev(f^g) = Rev f by FINSEQ_1:34
.= (Rev g)^(Rev f) by FINSEQ_1:34;
end;
A2: for g being FinSequence, x being object st P[g] holds P[g^<*x*>]
proof
let g be FinSequence, x be object such that
A3: P[g];
thus Rev(f^(g^<*x*>)) = Rev(f^g^<*x*>) by FINSEQ_1:32
.= <*x*>^((Rev g)^(Rev f)) by A3,Th63
.= <*x*>^(Rev g)^(Rev f) by FINSEQ_1:32
.= (Rev(g^<*x*>))^(Rev f) by Th63;
end;
thus for g being FinSequence holds P[g] from FINSEQ_1:sch 3(A1,A2);
end;
definition
let D be set, f be D-valued FinSequence;
redefine func Rev f -> FinSequence of D; :: redefines Rev (FINSEQ_5, definition)
coherence
proof
set n = len f;
A1: dom f = Seg n by FINSEQ_1:def 3;
now
let i be Nat;
set j = n - i + 1;
assume i in dom (Rev f);
then i in Seg len Rev f by FINSEQ_1:def 3;
then
A2: i in Seg n by Def3;
then j in Seg n by Th2;
then f.j in D by A1,FINSEQ_2:11;
hence Rev f.i in D by A1,A2,Th58;
end;
hence thesis by FINSEQ_2:12;
end;
end;
theorem
f is non empty implies f/.1 = (Rev f)/.len f & f/.len f = (Rev f)/.1
proof
A1: dom f = dom Rev f by Th57;
assume
A2: f is non empty;
then
A3: len f in dom f by Th6;
1 in dom f by A2,Th6;
hence f/.1 = f.1 by PARTFUN1:def 6
.= (Rev f).len f by Th62
.= (Rev f)/.len f by A3,A1,PARTFUN1:def 6;
thus f/.len f = f.(len f) by A3,PARTFUN1:def 6
.= (Rev f).1 by Th62
.= (Rev f)/.1 by A2,A1,Th6,PARTFUN1:def 6;
end;
theorem
i in dom f & i+j = len f + 1 implies f/.i = (Rev f)/.j
proof
assume that
A1: i in dom f and
A2: i+j = len f + 1;
A3: j in dom Rev f by A1,A2,Th59;
A4: i = len f - j + 1 by A2;
thus f/.i = f.i by A1,PARTFUN1:def 6
.= (Rev f).j by A4,A3,Def3
.= (Rev f)/.j by A3,PARTFUN1:def 6;
end;
definition
let D,f,p;
let n be Nat;
func Ins(f,n,p) -> FinSequence of D equals
(f|n)^<*p*>^(f/^n);
coherence;
end;
theorem
Ins(f,0,p) = <*p*>^f by FINSEQ_1:34;
theorem Th68:
len f <= n implies Ins(f,n,p) = f^<*p*>
proof
assume
A1: len f <= n;
then f/^n is empty by Th32;
hence Ins(f,n,p) = (f|n)^<*p*> by FINSEQ_1:34
.= f^<*p*> by A1,FINSEQ_1:58;
end;
theorem
len(Ins(f,n,p)) = len f + 1
proof
per cases;
suppose
A1: n <= len f;
thus len Ins(f,n,p) = len((f|n)^<*p*>) + len(f/^n) by FINSEQ_1:22
.= len((f|n)^<*p*>) + (len f - n) by A1,RFINSEQ:def 1
.= len(f|n)+len<*p*> + (len f - n) by FINSEQ_1:22
.= len(f|n)+1+(len f - n) by FINSEQ_1:39
.= n+1+(len f - n) by A1,FINSEQ_1:59
.= len f + 1;
end;
suppose
len f < n;
then Ins(f,n,p) = f^<*p*> by Th68;
hence thesis by FINSEQ_2:16;
end;
end;
theorem Th70:
rng Ins(f,n,p) = {p} \/ rng f
proof
thus rng Ins(f,n,p) = rng((f|n)^<*p*>) \/ rng(f/^n) by FINSEQ_1:31
.= rng(f|n) \/ rng<*p*> \/ rng(f/^n) by FINSEQ_1:31
.= rng(f|n) \/ rng(f/^n) \/ rng<*p*> by XBOOLE_1:4
.= rng((f|n)^(f/^n)) \/ rng<*p*> by FINSEQ_1:31
.= rng<*p*> \/ rng f by RFINSEQ:8
.= {p} \/ rng f by FINSEQ_1:38;
end;
registration
let D,f,n,p;
cluster Ins(f,n,p) -> non empty;
coherence;
end;
theorem
p in rng Ins(f,n,p)
proof
p in {p} by TARSKI:def 1;
then p in {p} \/ rng f by XBOOLE_0:def 3;
hence thesis by Th70;
end;
theorem Th72:
i in dom(f|n) implies (Ins(f,n,p)).i = f.i
proof
assume
A1: i in dom(f|n);
thus (Ins(f,n,p)).i = ((f|n)^(<*p*>^(f/^n))).i by FINSEQ_1:32
.= (f|n).i by A1,Lm1
.= f.i by A1,FUNCT_1:47;
end;
theorem
n <= len f implies (Ins(f,n,p)).(n+1) = p
proof
A1: 1 <= n+1 by NAT_1:11;
assume n <= len f;
then
A2: len(f|n) = n by FINSEQ_1:59;
then len((f|n)^<*p*>) = n+1 by FINSEQ_2:16;
then n+1 in dom((f|n)^<*p*>) by A1,FINSEQ_3:25;
hence (Ins(f,n,p)).(n+1) = ((f|n)^<*p*>).(n+1) by Lm1
.= p by A2,FINSEQ_1:42;
end;
theorem
n+1 <= i & i <= len f implies (Ins(f,n,p)).(i+1) = f.i
proof
assume that
A1: n+1 <= i and
A2: i <= len f;
reconsider j = i - (n+1) as Element of NAT by A1,INT_1:5;
n+(j+1) <= len f by A2;
then
A3: j+1 <= len f - n by XREAL_1:19;
n <= n+1 by NAT_1:11;
then
A4: n <= i by A1,XXREAL_0:2;
then len(f|n) = n by A2,FINSEQ_1:59,XXREAL_0:2;
then
A5: len((f|n)^<*p*>) = n+1 by FINSEQ_2:16;
n <= len f by A2,A4,XXREAL_0:2;
then 1 <= j+1 & j+1 <= len(f/^n) by A3,NAT_1:11,RFINSEQ:def 1;
then
A6: j+1 in dom(f/^n) by FINSEQ_3:25;
n+1+(j+1) = i+1;
hence (Ins(f,n,p)).(i+1) = (f/^n).(j+1) by A5,A6,FINSEQ_1:def 7
.= f.(n+(j+1)) by A6,Th27
.= f.i;
end;
theorem
1 <= n & f is non empty implies (Ins(f,n,p)).1 = f.1
proof
assume that
A1: 1 <= n and
A2: f is non empty;
A3: n <= len f implies len(f|n) = n by FINSEQ_1:59;
1 <= len f by A2,NAT_1:14;
then 1 <= len(f|n) by A1,A3,FINSEQ_1:58;
then 1 in dom(f|n) by FINSEQ_3:25;
hence thesis by Th72;
end;
theorem
f is one-to-one & not p in rng f implies Ins(f,n,p) is one-to-one
proof
assume that
A1: f is one-to-one and
A2: not p in rng f;
now
let x be object;
assume
A3: x in rng(f/^n);
rng(f/^n) c= rng f by Th33;
then x in rng f by A3;
then not x in {p} by A2,TARSKI:def 1;
then
A4: not x in rng<*p*> by FINSEQ_1:38;
rng(f|n) misses rng(f/^n) by A1,Th34;
then not x in rng(f|n) by A3,XBOOLE_0:3;
then not x in rng(f|n) \/ rng<*p*> by A4,XBOOLE_0:def 3;
hence not x in rng((f|n) ^ <*p*>) by FINSEQ_1:31;
end;
then
A5: rng((f|n) ^ <*p*>) misses rng(f/^n) by XBOOLE_0:3;
now
let x be object;
assume x in rng<*p*>;
then x in {p} by FINSEQ_1:38;
then
A6: not x in rng f by A2,TARSKI:def 1;
rng(f|n) c= rng f by Th19;
hence not x in rng(f|n) by A6;
end;
then <*p*> is one-to-one & rng(f|n) misses rng<*p*> by FINSEQ_3:93,XBOOLE_0:3
;
then (f|n) ^ <*p*> is one-to-one by A1,FINSEQ_3:91;
hence thesis by A1,A5,FINSEQ_3:91;
end;
begin :: Addenda
:: from JORDAN4, 2005.11.16, A.T.
theorem
for f being FinSequence holds
for i1,i2 be Nat st i1<=i2 holds (f|i1)|i2=f|i1 & (f|i2)|i1=f|i1
proof
let f be FinSequence;
let i1,i2 be Nat;
assume
A1: i1<=i2;
len (f|i1)<=i1 by Th17;
hence (f|i1)|i2=f|i1 by A1,FINSEQ_1:58,XXREAL_0:2;
Seg i1 c= Seg i2 by A1,FINSEQ_1:5;
hence thesis by FUNCT_1:51;
end;
theorem
(<*>D)|i = <*>D;
theorem
Rev <*>D = <*>D;
:: from AMISTD_1, 2006.03,15, A.T.
registration
cluster non trivial for FinSequence;
existence
proof
take <*0,0*>;
thus thesis;
end;
end;
:: from JORDAN3, 2007.03.09, A.T
theorem
for f being FinSequence,l1,l2 being Nat holds (f/^l1)|(l2-'l1) = (f|l2)/^l1
proof
let f be FinSequence,l1,l2 be Nat;
per cases;
suppose
A1: l1<=l2;
per cases;
suppose
A2: l2<=len f;
then
A3: l2-l1<=len f-l1 by XREAL_1:9;
A4: l1<=len (f|l2) by A1,A2,FINSEQ_1:59;
then
A5: len ((f|l2)/^l1)=len (f|l2)-l1 by RFINSEQ:def 1
.=l2-l1 by A2,FINSEQ_1:59
.=l2-'l1 by A1,XREAL_1:233;
A6: l1<=len f by A1,A2,XXREAL_0:2;
then len (f/^l1)=len f-l1 by RFINSEQ:def 1;
then
A7: l2-'l1<=len (f/^l1) by A1,A3,XREAL_1:233;
A8: for k being Nat st 1<=k & k<=len ((f|l2)/^l1) holds ((f/^l1)|(l2-'
l1)).k=((f|l2)/^l1).k
proof
let k be Nat such that
A9: 1<=k and
A10: k<=len ((f|l2)/^l1);
A11: k in dom ((f|l2)/^l1) by A9,A10,FINSEQ_3:25;
k<=l2-l1 by A1,A5,A10,XREAL_1:233;
then
A12: k+l1<=l2-l1+l1 by XREAL_1:6;
k<=len (f/^l1) by A7,A5,A10,XXREAL_0:2;
then
A13: k in dom (f/^l1) by A9,FINSEQ_3:25;
k in Seg (l2-'l1) by A5,A9,A10;
then ((f/^l1)|(l2-'l1)).k =(f/^l1).k by FUNCT_1:49
.=f.(k+l1) by A6,A13,RFINSEQ:def 1
.=(f|l2).(k+l1) by A12,FINSEQ_3:112
.=((f|l2)/^l1).k by A4,A11,RFINSEQ:def 1;
hence thesis;
end;
len ((f/^l1)|(l2-'l1)) = l2-'l1 by A7,FINSEQ_1:59;
hence thesis by A5,A8;
end;
suppose
A14: l2>len f;
A15: len (f/^l1)=len f-'l1 by RFINSEQ:29;
f|l2=f by A14,FINSEQ_1:58;
hence thesis by A14,A15,FINSEQ_1:58,NAT_D:42;
end;
end;
suppose
A16: l1>l2;
reconsider l19=l1,l29=l2 as Element of NAT by ORDINAL1:def 12;
l1-l1>l2-l1 by A16,XREAL_1:9;
then l2-'l1=0 by XREAL_0:def 2;
then
A17: (f/^l1)|(l2-'l1)={};
per cases;
suppose
l1<=len f;
then l19>len (f|l29) by A16,FINSEQ_1:59,XXREAL_0:2;
hence thesis by A17,Th32;
end;
suppose
A18: l1>len f;
len (f|l29)<=len f by Th16;
hence thesis by A17,A18,Th32,XXREAL_0:2;
end;
end;
end;
:: from JORDAN8, 2007.03.18, A.T.
reserve D for set,
f for FinSequence of D;
theorem
len f >= 2 implies f|2 = <*f/.1,f/.2*>
proof
set d1 = f/.1, d2 = f/.2;
assume
A1: len f >= 2;
then
A2: len(f|2) = 2 by FINSEQ_1:59;
reconsider D as non empty set by A1;
reconsider f as FinSequence of D;
2 in dom(f|2) by A2,FINSEQ_3:25;
then
A3: d2 = (f|2)/.2 by FINSEQ_4:70
.= (f|2).2 by A2,FINSEQ_4:15;
1 in dom(f|2) by A2,FINSEQ_3:25;
then d1 = (f|2)/.1 by FINSEQ_4:70
.= (f|2).1 by A2,FINSEQ_4:15;
hence thesis by A2,A3,FINSEQ_1:44;
end;
theorem
for D being set, f being FinSequence of D st
k+1 <= len f holds f|(k+1) = f|k^<*f/.(k+1)*>
proof
let D be set, f be FinSequence of D;
A1: 1 <= k+1 by NAT_1:12;
assume k+1 <= len f;
then
A2: k+1 in dom f by A1,FINSEQ_3:25;
then f|Seg(k+1) = (f|k)^<*f.(k+1)*> by Th10 .= (f|k)^<*f/.(k+1)*>
by A2,PARTFUN1:def 6;
hence thesis;
end;
:: from JORDAN3, 2007.03.18, A.T.
theorem Th83:
for p be FinSequence for i be Nat st i < len p
holds p|(i+1) = p|i ^ <*p.(i+1)*>
proof
let p be FinSequence;
let i be Nat;
assume i < len p;
then
A1: i+1 <= len p by NAT_1:13;
1 <= i+1 by NAT_1:11;
then
i+1 in dom p by A1,FINSEQ_3:25;
hence thesis by Th10;
end;
:: from POLYNOM4, 2007.03.18, A.T.
theorem
for p be FinSequence for n be Nat st 1 <= n & n <= len p holds
p = (p|(n-'1))^<*p.n*>^(p/^n)
proof
let p be FinSequence;
let n be Nat;
assume that
A1: 1 <= n and
A2: n <= len p;
len p >= n-'1+1 by A1,A2,XREAL_1:235;
then
A3: len p > n-'1 by NAT_1:13;
p|n = p|(n-'1+1) by A1,XREAL_1:235
.= p|(n-'1)^<*p.(n-'1+1)*> by A3,Th83
.= p|(n-'1)^<*p.n*> by A1,XREAL_1:235;
hence thesis by RFINSEQ:8;
end;
:: from POLYALG1, 2016.10.19, A.K.
theorem Th3:
for f being non empty FinSequence holds f/^1 = Del(f,1)
proof
let f be non empty FinSequence;
consider i be Nat such that
A1: i+1 = len f by NAT_1:6;
reconsider i as Element of NAT by ORDINAL1:def 12;
A2: 1 <= len f by A1,NAT_1:11;
len (f/^1) = len Del(f,1) & for k be Nat st 1 <=k & k <= len (f/^1)
holds (f/^1).k=Del(f,1).k
proof
A3: len (f/^1) = (i+1)-1 by A1,A2,RFINSEQ:def 1
.= i;
1 in dom f by Th6;
hence len (f/^1) = len Del(f,1) by A1,A3,FINSEQ_3:109;
A4: 1 in dom f by Th6;
let k be Nat such that
A5: 1 <=k & k <= len (f/^1);
k in dom (f/^1) by A5,FINSEQ_3:25;
hence (f/^1).k= f.(k+1) by A2,RFINSEQ:def 1
.= Del(f,1).k by A1,A3,A5,A4,FINSEQ_3:111;
end;
hence thesis;
end;
Th29a:
for f being non empty FinSequence holds f = <*f.1*>^(f/^1)
proof
let f be non empty FinSequence;
f|1 = <*f.1*> by Th20;
hence thesis by RFINSEQ:8;
end;
theorem
for f being non empty FinSequence holds f = <*f.1*>^Del(f,1)
proof
let f be non empty FinSequence;
thus f = <*f.1*>^(f/^1) by Th29a
.= <*f.1*>^Del(f,1) by Th3;
end;
theorem
for f being non empty FinSequence holds f = <*f.1*>^(f/^1) by Th29a;