Copyright (c) 1995 Association of Mizar Users
environ
vocabulary ARYTM_1, FINSEQ_1, FUNCT_1, RELAT_1, FINSEQ_4, REALSET1, RFINSEQ,
BOOLE, RLSUB_2, FINSEQ_5;
notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, RELAT_1,
FUNCT_1, FINSEQ_1, FINSEQ_4, REALSET1, RFINSEQ, TOPREAL1;
constructors REAL_1, NAT_1, REALSET1, RFINSEQ, TOPREAL1, FINSEQ_4, INT_1,
MEMBERED, XBOOLE_0;
clusters SUBSET_1, FUNCT_1, FINSEQ_1, RELSET_1, INT_1, TOPREAL1, NAT_1,
MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FUNCT_1, XBOOLE_0;
theorems TARSKI, AXIOMS, ZFMISC_1, REAL_1, NAT_1, RLVECT_1, RLVECT_2,
PARTFUN2, FUNCT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, RFINSEQ,
SPPOL_1, REALSET1, TOPREAL1, TOPREAL4, GOBOARD1, PROB_1, RELAT_1,
GROUP_5, INT_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
schemes FINSEQ_1;
begin
reserve i,j,k,m,n for Nat;
theorem Th1:
i <= n implies n - i + 1 is Nat
proof assume i <= n;
then reconsider n_i = n - i as Nat by INT_1:18;
n_i + 1 is Nat;
hence thesis;
end;
theorem Th2:
i in Seg n implies n - i + 1 in Seg n
proof
assume A1: i in Seg n;
then 1 <= i & i <= n by FINSEQ_1:3;
then reconsider n_i = n - i as Nat by INT_1:18;
reconsider j = n_i + 1 as Nat;
0 <= n_i by NAT_1:18;
then A2: 0+1 <= j by AXIOMS:24;
0 <= i by NAT_1:18;
then n_i <= n by PROB_1:2;
then A3: j <= n + 1 by AXIOMS:24;
now assume j = n + 1;
then n_i = n + 1 - 1 by XCMPLX_1:26 .= n by XCMPLX_1:26;
then 0 = n_i-n by XCMPLX_1:14
.= (-i+n)-n by XCMPLX_0:def 8
.= -i by XCMPLX_1:26;
hence contradiction by A1,FINSEQ_1:3,REAL_1:26;
end;
then j < n + 1 by A3,REAL_1:def 5;
then j <= n by NAT_1:38;
hence thesis by A2,FINSEQ_1:3;
end;
theorem Th3:
for f being Function, x,y being set st f"{y} = {x}
holds x in dom f & y in rng f & f.x = y
proof let f be Function, x,y be set;
assume f"{y} = {x};
then A1: x in f"{y} by TARSKI:def 1;
hence
A2: x in dom f by FUNCT_1:def 13;
f.x in {y} by A1,FUNCT_1:def 13;
then f.x = y by TARSKI:def 1;
hence thesis by A2,FUNCT_1:def 5;
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 set st x in dom f holds f is_one-to-one_at x;
let x be set;
assume x in dom f;
then f is_one-to-one_at x by A1;
hence f"{f.x} = {x} by FINSEQ_4:3;
end;
assume
A2: for x being set st x in dom f holds f"{f.x} = {x};
let x be set;
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:3;
end;
hence thesis by FINSEQ_4:5;
end;
theorem
for f being Function, y1,y2 being set
st f is one-to-one & y1 in rng f & y2 in rng f & f"{y1} = f"{y2}
holds y1 = y2
proof let f be Function, y1,y2 be set such that
A1: f is one-to-one and
A2: y1 in rng f and
A3: y2 in rng f and
A4: f"{y1} = f"{y2};
consider x1 being set such that
A5: f"{y1} = {x1} by A1,A2,FUNCT_1:144;
consider x2 being set such that
A6: f"{y2} = {x2} by A1,A3,FUNCT_1:144;
f.x1 = y1 & f.x2 = y2 by A5,A6,Th3;
hence thesis by A4,A5,A6,ZFMISC_1:6;
end;
definition let x be set;
cluster <*x*> -> non empty;
coherence
proof <*x*> = { [1,x] } by FINSEQ_1:52; hence thesis; end;
end;
definition
cluster empty -> trivial set;
coherence by REALSET1:def 12;
end;
definition let x be set;
cluster <*x*> -> trivial;
coherence
proof len <*x*> = 1 by FINSEQ_1:56;
hence thesis by SPPOL_1:2;
end;
let y be set;
cluster <*x,y*> -> non trivial;
coherence
proof len <*x,y*> = 2 by FINSEQ_1:61;
hence thesis by SPPOL_1:2;
end;
end;
definition
cluster one-to-one non empty FinSequence;
existence
proof consider x being set;
set f = <*x*>;
f is non empty & f is one-to-one by FINSEQ_3:102;
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;
len f <> 0 by FINSEQ_1:25;
then A1: len f >= 1 by RLVECT_1:99;
hence 1 in dom f by FINSEQ_3:27;
thus len f in dom f by A1,FINSEQ_3:27;
end;
theorem
for f being non empty FinSequence ex i st i+1 = len f
proof let f be non empty FinSequence;
len f <> 0 by FINSEQ_1:25;
hence thesis by NAT_1:22;
end;
theorem Th8:
for x being set, f being FinSequence holds len(<*x*>^f) = 1 + len f
proof let x be set, f be FinSequence;
thus len(<*x*>^f) = len <*x*> + len f by FINSEQ_1:35
.= 1 + len f by FINSEQ_1:56;
end;
scheme domSeqLambda{A()->Nat,F(set) -> set}:
ex p being FinSequence st len p = A() & for k st k in dom p holds p.k=F(k)
proof
deffunc G(Nat) = F($1);
consider p being FinSequence such that
A1: len p = A() and
A2: for k st k in Seg A() holds p.k=G(k) from SeqLambda;
take p;
thus len p = A() by A1;
let k;
assume k in dom p;
then k in Seg A() by A1,FINSEQ_1:def 3;
hence thesis by A2;
end;
canceled;
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:29 .= q by A2,FINSEQ_4:29;
end;
theorem Th11:
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:19;
n+1 in Seg(n+1) by FINSEQ_1:6;
then A3: h.(n+1) = f.(n+1) by FUNCT_1:72;
n <= n+1 by NAT_1:29;
then Seg n c= Seg(n+1) by FINSEQ_1:7;
then A4: g = h|Seg n by A2,FUNCT_1:82;
n+1 <= len f by A1,FINSEQ_3:27;
then len h = n+1 by FINSEQ_1:21;
hence f|Seg(n+1) = g^<*f.(n+1)*> by A3,A4,FINSEQ_3:61;
end;
theorem Th12:
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 5;
then A2: f just_once_values f.i by FINSEQ_4:10;
then f <- (f.i) = (f.i)..f by FINSEQ_4:35;
hence (f.i)..f = i 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;
definition let D be non empty set;
cluster one-to-one non empty FinSequence of D;
existence
proof consider x being Element of D;
set f = <*x*>;
f is non empty & f is one-to-one by FINSEQ_3:102;
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; assume
A3: k in dom f;
hence f.k = f/.k by FINSEQ_4:def 4
.= g/.k by A2,A3
.= g.k by A1,A3,FINSEQ_4:def 4;
end;
hence thesis by A1,FINSEQ_1:17;
end;
:: FINSEQ_1:18
theorem Th14:
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; assume
A3: 1 <= k & k <= len f;
hence f.k = f/.k by FINSEQ_4:24
.= g/.k by A2,A3
.= g.k by A1,A3,FINSEQ_4:24;
end;
hence thesis by A1,FINSEQ_1:18;
end;
theorem Th15:
len f = 1 implies f = <*f/.1*>
proof
assume
A1: len f = 1;
then f is non empty by FINSEQ_1:25;
then 1 in dom f by Th6;
then f.1 = f/.1 by FINSEQ_4:def 4;
hence thesis by A1,FINSEQ_1:57;
end;
theorem Th16:
for D being non empty set, p being Element of D,
f being FinSequence of D holds
(<*p*>^f)/.1 = p
proof let D be non empty set, p be Element of D, f be FinSequence of D;
len(<*p*>^f) = 1 + len f by Th8;
then 1 <= 1 & 1 <= len(<*p*>^f) by NAT_1:29;
then 1 in dom(<*p*>^f) by FINSEQ_3:27;
then (<*p*>^f)/.1 = (<*p*>^f).1 by FINSEQ_4:def 4;
hence thesis by FINSEQ_1:58;
end;
:: FINSEQ_1:def 7
Lm1:
i in dom f implies (f^g)/.i=f/.i
proof assume
A1: i in dom f;
dom f c= dom(f^g) by FINSEQ_1:39;
hence (f^g)/.i = (f^g).i by A1,FINSEQ_4:def 4
.= f.i by A1,FINSEQ_1:def 7
.= f/.i by A1,FINSEQ_4:def 4;
end;
canceled;
theorem Th18:
for D being set, f being FinSequence of D holds
len(f|i) <= len f
proof let D be set, f be FinSequence of D;
i <= len f implies len(f|i) = i by TOPREAL1:3;
hence thesis by TOPREAL1:2;
end;
theorem Th19:
for D being set, f being FinSequence of D holds
len(f|i) <= i
proof let D be set, f be FinSequence of D;
i <= len f implies len(f|i) = i by TOPREAL1:3;
hence thesis by TOPREAL1:2;
end;
theorem Th20:
for D being set, f being FinSequence of D holds
dom(f|i) c= dom f
proof let D be set, f be FinSequence of D;
let j be set;
assume
A1: j in dom(f|i);
then reconsider j as Nat;
A2: len(f|i) <= len f by Th18;
j <= len (f|i) by A1,FINSEQ_3:27;
then A3: j <= len f by A2,AXIOMS:22;
1 <= j by A1,FINSEQ_3:27;
hence thesis by A3,FINSEQ_3:27;
end;
theorem Th21:
rng(f|i) c= rng f
proof
let p be set;
assume p in rng(f|i);
then consider j being Nat such that
A1: j in dom(f|i) and
A2: (f|i)/.j = p by PARTFUN2:4;
dom(f|i) c= dom f by Th20;
then f/.j in rng f by A1,PARTFUN2:4;
hence p in rng f by A1,A2,TOPREAL1:1;
end;
canceled;
theorem Th23:
for D being set, f being FinSequence of D holds
f is non empty implies f|1 = <*f/.1*>
proof
let D be set, f be FinSequence of D;
assume f is non empty;
then 1 in dom f by Th6;
then 1 <= len f by FINSEQ_3:27;
then A1: len(f|1) = 1 by TOPREAL1:3;
then A2: 1 in dom(f|1) by FINSEQ_3:27;
then A3: (f|1)/.1 = (f|1).1 by FINSEQ_4:def 4;
f/.1 = (f|1)/.1 by A2,TOPREAL1:1;
hence thesis by A1,A3,FINSEQ_1:57;
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 by FINSEQ_1:25;
then A2: i+1 in dom f by A1,Th6;
A3: f|i = f|Seg i by TOPREAL1:def 1;
dom f = Seg(i+1) by A1,FINSEQ_1:def 3;
hence f = f|Seg(i+1) by RELAT_1:97
.= (f|i)^<*f.(i+1)*> by A2,A3,Th11
.= (f|i)^<*f/.len f*> by A1,A2,FINSEQ_4:def 4;
end;
Lm2:
f is one-to-one implies f|i is one-to-one
proof assume
A1: f is one-to-one;
now let n,m such that
A2: n in dom(f|i) and
A3: m in dom(f|i) and
A4: (f|i)/.n = (f|i)/.m;
A5: dom(f|i) c= dom f by Th20;
f/.n = (f|i)/.n by A2,TOPREAL1:1 .= f/.m by A3,A4,TOPREAL1:1;
hence n = m by A1,A2,A3,A5,PARTFUN2:17;
end;
hence thesis by PARTFUN2:16;
end;
definition let i,D; let f be one-to-one FinSequence of D;
cluster f|i -> one-to-one;
coherence by Lm2;
end;
theorem Th25:
for D being set, f, g being FinSequence of D holds
i <= len f implies (f^g)|i = f|i
proof
let D be set, f, g be FinSequence of D;
assume
A1: i <= len f;
then A2: len(f|i) = i by TOPREAL1:3;
i <= len f+len g by A1,NAT_1:37;
then i <= len(f^g) by FINSEQ_1:35;
then A3: len((f^g)|i) = i by TOPREAL1:3;
now let j;
assume
A4: j in Seg i;
then j <= i by FINSEQ_1:3;
then 1 <= j & j <= len f by A1,A4,AXIOMS:22,FINSEQ_1:3;
then j in Seg len f by FINSEQ_1:3;
then A5: j in dom f by FINSEQ_1:def 3;
thus ((f^g)|i).j = ((f^g)|(Seg i)).j by TOPREAL1:def 1
.= (f^g).j by A4,FUNCT_1:72
.= f.j by A5,FINSEQ_1:def 7
.= (f|(Seg i)).j by A4,FUNCT_1:72
.= (f|i).j by TOPREAL1:def 1;
end;
hence (f^g)|i = f|i by A2,A3,FINSEQ_2:10;
end;
theorem
for D being set, f, g being FinSequence of D holds
(f^g)|(len f) = f
proof
let D be set, f, g be FinSequence of D;
f|len f = f|(Seg len f) by TOPREAL1:def 1;
hence f = f|len f by FINSEQ_2:23 .= (f^g)|(len f) by Th25;
end;
theorem
for D being set, f being FinSequence of D holds
p in rng f implies (f-|p)^<*p*> = f|(p..f)
proof let D be set, f be FinSequence of D;
assume
A1: p in rng f;
then consider n such that
A2: n = p..f - 1 and
A3: f-|p = f | Seg n by FINSEQ_4:def 6;
A4: n+1 = p..f by A2,XCMPLX_1:27;
then n+1 in dom f & f.(n+1) = p by A1,FINSEQ_4:29,30;
hence (f-|p)^<*p*> = f|Seg(n+1) by A3,Th11
.= f|(p..f) by A4,TOPREAL1:def 1;
end;
theorem
len(f/^i) <= len f
proof
per cases;
suppose
i <= len f;
then len(f/^i) = len f - i by RFINSEQ:def 2;
then len(f/^i)+i = len f by XCMPLX_1:27;
hence thesis by NAT_1:29;
suppose len f < i;
then f/^i = <*>D by RFINSEQ:def 2;
then len(f/^i) = 0 by FINSEQ_1:32;
hence thesis by NAT_1:18;
end;
theorem Th29:
i in dom(f/^n) implies n+i in dom f
proof assume
A1: i in dom(f/^n);
per cases;
suppose
A2: n <= len f;
A3: 1 <= i by A1,FINSEQ_3:27;
i <= i+n by NAT_1:29;
then A4: 1 <= i+n by A3,AXIOMS:22;
i <= len(f/^n) by A1,FINSEQ_3:27;
then i <= len f - n by A2,RFINSEQ:def 2;
then n+i <= len f by REAL_1:84;
hence n+i in dom f by A4,FINSEQ_3:27;
suppose n > len f;
then f/^n = <*>D by RFINSEQ:def 2;
hence thesis by A1,FINSEQ_1:26;
end;
theorem Th30:
i in dom(f/^n) implies (f/^n)/.i = f/.(n+i)
proof assume
A1: i in dom(f/^n);
per cases;
suppose
A2: n <= len f;
A3: n+i in dom f by A1,Th29;
thus (f/^n)/.i = (f/^n).i by A1,FINSEQ_4:def 4
.= f.(n+i) by A1,A2,RFINSEQ:def 2
.= f/.(n+i) by A3,FINSEQ_4:def 4;
suppose n > len f;
then f/^n = <*>D by RFINSEQ:def 2;
hence thesis by A1,FINSEQ_1:26;
end;
theorem Th31:
f/^0 = f
proof
A1: 0 <= len f by NAT_1:18;
then A2: len(f/^0) = len f - 0 by RFINSEQ:def 2
.= len f;
now
let i;
assume 1 <= i & i <= len(f/^0);
then i in dom(f/^0) by FINSEQ_3:27;
hence (f/^0).i = f.(i+0) by A1,RFINSEQ:def 2
.= f.i;
end;
hence thesis by A2,FINSEQ_1:18;
end;
theorem
f is non empty implies f = <*f/.1*>^(f/^1)
proof assume f is non empty;
then f|1 = <*f/.1*> by Th23;
hence thesis by RFINSEQ:21;
end;
theorem
i+1 = len f implies f/^i = <*f/.len f*>
proof assume
A1: i+1 = len f;
then i <= len f by NAT_1:29;
then A2: len(f/^i) = len f - i by RFINSEQ:def 2
.= 1 by A1,XCMPLX_1:26;
then A3: 1 in dom(f/^i) by FINSEQ_3:27;
thus f/^i = <*(f/^i)/.1*> by A2,Th15
.= <*f/.len f*> by A1,A3,Th30;
end;
theorem Th34:
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:27;
j <= i by A1,NAT_1:29;
then A4: j <= len f by A3,AXIOMS:22;
A5: len g = len(f/^i) + 1 by Th8;
then A6: len g = len f - i + 1 by A3,RFINSEQ:def 2
.= len f - j - 1 + 1 by A1,XCMPLX_1:36
.= len f - j by XCMPLX_1:27
.= len(f/^j) by A4,RFINSEQ:def 2;
now let k;
assume that
A7: 1 <= k and
A8: k <= len g;
A9: k in dom(f/^j) by A6,A7,A8,FINSEQ_3:27;
per cases;
suppose
A10: k = 1;
hence g.k = f/.i by FINSEQ_1:58
.= f.i by A2,FINSEQ_4:def 4
.= (f/^j).k by A1,A4,A9,A10,RFINSEQ:def 2;
suppose
k <> 1;
then A11: 1 < k by A7,REAL_1:def 5;
reconsider k' = k-1 as Nat by A7,INT_1:18;
k'+1 = k by XCMPLX_1:27;
then A12: 1 <= k' by A11,NAT_1:38;
k' <= len g - 1 by A8,REAL_1:49;
then k' <= len(f/^i) by A5,XCMPLX_1:26;
then A13: k' in dom(f/^i) by A12,FINSEQ_3:27;
len <*f/.i*> = 1 by FINSEQ_1:56;
hence g.k = (f/^i).k' by A8,A11,FINSEQ_1:37
.= f.(k'+i) by A3,A13,RFINSEQ:def 2
.= f.(k'+1+j) by A1,XCMPLX_1:1
.= f.(k+j) by XCMPLX_1:27
.= (f/^j).k by A4,A9,RFINSEQ:def 2;
end;
hence <*f/.i*>^(f/^i) = f/^j by A6,FINSEQ_1:18;
end;
theorem Th35:
for D being set, f being FinSequence of D holds
len f <= i implies f/^i is empty
proof
let D be set, f be FinSequence of D;
assume
A1: len f <= i;
per cases;
suppose len f = i;
then len(f/^i) = len f - len f by RFINSEQ:def 2
.= 0 by XCMPLX_1:14;
hence thesis by FINSEQ_1:25;
suppose len f <> i;
then len f < i by A1,REAL_1:def 5;
then f/^i = <*>D by RFINSEQ:def 2;
hence thesis;
end;
theorem Th36:
rng(f/^n) c= rng f
proof
let p be set;
assume p in rng(f/^n);
then consider j being Nat such that
A1: j in dom(f/^n) and
A2: (f/^n)/.j = p by PARTFUN2:4;
j+n in dom f by A1,Th29;
then f/.(j+n) in rng f by PARTFUN2:4;
hence p in rng f by A1,A2,Th30;
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 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,Th29;
f/.(i+n) = (f/^i)/.n by A2,Th30 .= f/.(i+m) by A3,A4,Th30;
then i+n = i+m by A1,A5,PARTFUN2:17;
hence n = m by XCMPLX_1:2;
end;
hence thesis by PARTFUN2:16;
end;
definition let i,D; let f be one-to-one FinSequence of D;
cluster f/^i -> one-to-one;
coherence by Lm3;
end;
theorem Th37:
f is one-to-one implies rng(f|n) misses rng(f/^n)
proof assume
A1: f is one-to-one;
assume rng(f|n) meets rng(f/^n);
then consider x being set such that
A2: x in rng(f|n) and
A3: x in rng(f/^n) by XBOOLE_0:3;
consider i such that
A4: i in dom(f|n) and
A5: (f|n)/.i = x by A2,PARTFUN2:4;
consider j such that
A6: j in dom(f/^n) and
A7: (f/^n)/.j = x by A3,PARTFUN2:4;
A8: dom(f|n) c= dom f by Th20;
A9: j+n in dom f by A6,Th29;
A10: f/.(j+n) = (f/^n)/.j by A6,Th30
.= f/.i by A4,A5,A7,TOPREAL1:1;
now assume
A11: i = j+n;
A12: i <= len(f|n) by A4,FINSEQ_3:27;
len(f|n) <= n by Th19;
then A13: i <= n by A12,AXIOMS:22;
n <= i by A11,NAT_1:29;
then i = n by A13,AXIOMS:21;
then j = n-n by A11,XCMPLX_1:26
.= 0 by XCMPLX_1:14;
hence contradiction by A6,FINSEQ_3:27;
end;
hence contradiction by A1,A4,A8,A9,A10,PARTFUN2:17;
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 7;
A3: p..f <= len f by A1,FINSEQ_4:31;
then A4: len (f/^(p..f)) = len f - p..f by RFINSEQ:def 2;
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;
assume
A6: i in dom (f|--p);
hence (f|--p).i = f.(i + p..f) by A1,FINSEQ_4:def 7
.= (f/^(p..f)).i by A2,A3,A4,A5,A6,RFINSEQ:def 2;
end;
hence thesis by A2,A4,A5,FINSEQ_2:10;
end;
theorem Th39:
(f^g)/^(len f + i) = g/^i
proof
A1: len(f^g) = len f + len g by FINSEQ_1:35;
per cases;
suppose
A2: i <= len g;
then len f + i <= len f + len g by AXIOMS:24;
then A3: len((f^g)/^(len f + i)) = len g + len f - (len f + i) by A1,RFINSEQ:
def 2
.= len g + len f - len f - i by XCMPLX_1:36
.= len g - i by XCMPLX_1:26
.= len(g/^i) by A2,RFINSEQ:def 2;
now let k;
assume
A4: 1 <= k & k <= len(g/^i);
then A5: k in dom(g/^i) by FINSEQ_3:27;
then A6: i+k in dom g by Th29;
k in dom((f^g)/^(len f + i)) by A3,A4,FINSEQ_3:27;
hence ((f^g)/^(len f + i))/.k = (f^g)/.(len f + i + k) by Th30
.= (f^g)/.(len f + (i+k)) by XCMPLX_1:1
.= g/.(i+k) by A6,GROUP_5:96
.= (g/^i)/.k by A5,Th30;
end;
hence (f^g)/^(len f + i) = g/^i by A3,Th14;
suppose
A7: i > len g;
then len f + i > len(f^g) by A1,REAL_1:53;
hence (f^g)/^(len f+i) = <*>D by RFINSEQ:def 2
.= g/^i by A7,RFINSEQ:def 2;
end;
theorem
(f^g)/^(len f) = g
proof
thus (f^g)/^(len f) = (f^g)/^(len f + 0)
.= g/^0 by Th39
.= g by Th31;
end;
theorem Th41:
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:29,30;
hence thesis by FINSEQ_4:def 4;
end;
theorem Th42:
i in dom f implies f/.i..f <= i
proof assume that
A1: i in dom f;
set p = f/.i;
A2: p..f = Sgm(f"{p}).1 by FINSEQ_4:def 5;
f"{p} c= dom f by RELAT_1:167;
then A3: f"{p} c= Seg len f by FINSEQ_1:def 3;
f/.i = f.i by A1,FINSEQ_4:def 4;
then f.i in {p} by TARSKI:def 1;
then i in f"{p} by A1,FUNCT_1:def 13;
then i in rng Sgm(f"{p}) by A3,FINSEQ_1:def 13;
then consider l being set such that
A4: l in dom Sgm(f"{p}) and
A5: Sgm(f"{p}).l = i by FUNCT_1:def 5;
reconsider l as Nat by A4;
1 <= l & l <= len(Sgm(f"{p})) by A4,FINSEQ_3:27;
hence p..f <= i by A2,A3,A5,FINSEQ_3:46;
end;
theorem
p in rng(f|i) implies p..(f|i) = p..f
proof assume
A1: p in rng(f|i);
then A2: p..(f|i) in dom(f|i) by FINSEQ_4:30;
A3: dom(f|i) c= dom f by Th20;
A4: rng(f|i) c= rng f by Th21;
f/.(p..(f|i)) = (f|i)/.(p..(f|i)) by A2,TOPREAL1:1
.= p by A1,Th41;
then A5: p..f <= p..(f|i) by A2,A3,Th42;
A6: 1 <= p..f by A1,A4,FINSEQ_4:31;
p..(f|i) <= len(f|i) by A1,FINSEQ_4:31;
then p..f <= len(f|i) by A5,AXIOMS:22;
then A7: p..f in dom(f|i) by A6,FINSEQ_3:27;
then (f|i)/.(p..f) = f/.(p..f) by TOPREAL1:1
.= p by A1,A4,Th41;
then p..(f|i) <= p..f by A7,Th42;
hence thesis by A5,AXIOMS:21;
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,Th12;
hence thesis by A1,FINSEQ_4:def 4;
end;
definition let D, f; let p be set;
func f-:p -> FinSequence of D equals
:Def1: f|(p..f);
correctness;
end;
theorem Th45:
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:30;
then A1: p..f <= len f by FINSEQ_3:27;
f-:p = f|(p..f) by Def1;
hence thesis by A1,TOPREAL1:3;
end;
theorem Th46:
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);
A3: p..f in dom f by A1,FINSEQ_4:30;
thus (f-:p)/.i = (f|(p..f))/.i by Def1 .= f/.i by A2,A3,GOBOARD1:10;
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:31;
then 1 in Seg(p..f) by FINSEQ_1:3;
hence (f-:p)/.1 = f/.1 by A1,Th46;
end;
theorem
p in rng f implies (f-:p)/.(p..f) = p
proof
assume
A1: p in rng f;
then 1 <= p..f & p..f <= p..f by FINSEQ_4:31;
then A2: p..f in Seg(p..f) by FINSEQ_1:3;
A3: p..f in dom f by A1,FINSEQ_4:30;
thus (f-:p)/.(p..f) = f/.(p..f) by A1,A2,Th46
.= f.(p..f) by A3,FINSEQ_4:def 4
.= p by A1,FINSEQ_4:29;
end;
theorem
for x being set holds
x in rng f & p in rng f & x..f<=p..f implies 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;
A4: i in dom f by A1,FINSEQ_4:30;
1 <= i by A1,FINSEQ_4:31;
then A5: i in Seg (p..f) by A3,FINSEQ_1:3;
Seg len g = dom g by FINSEQ_1:def 3;
then A6: i in dom g by A2,A5,Th45;
then g.i in rng g by FUNCT_1:def 5;
then g/.i in rng g by A6,FINSEQ_4:def 4;
then f/.i in rng g by A2,A5,Th46;
then f.i in rng g by A4,FINSEQ_4:def 4;
hence thesis by A1,FINSEQ_4:29;
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:31;
then 1 <= len(f-:p) by A1,Th45;
hence thesis by FINSEQ_3:27,RELAT_1:60;
end;
theorem
rng(f-:p) c= rng f
proof f-:p = f|(p..f) by Def1;
hence thesis by Th21;
end;
definition let D,p; let f be one-to-one FinSequence of D;
cluster f-:p -> one-to-one;
coherence
proof f-:p = f|(p..f) by Def1;
hence thesis;
end;
end;
definition let D, f, p;
func f:-p -> FinSequence of D equals
:Def2: <*p*>^(f/^p..f);
correctness;
end;
theorem Th52:
p in rng f implies ex i st i+1 = p..f & f:-p = f/^i
proof assume
A1: p in rng f;
then 1 <= p..f by FINSEQ_4:31;
then reconsider i = p..f - 1 as Nat by INT_1:18;
take i;
thus
A2: i+1 = p..f by XCMPLX_1:27;
A3: p..f in dom f by A1,FINSEQ_4:30;
thus f:-p = <*p*>^(f/^p..f) by Def2
.= <*f/.(p..f)*>^(f/^p..f) by A1,Th41
.= f/^i by A2,A3,Th34;
end;
theorem Th53:
p in rng f implies len (f:-p) = len f - p..f + 1
proof
assume
A1: p in rng f;
then consider i such that
A2: i+1 = p..f and
A3: f:-p = f/^i by Th52;
i <= p..f & p..f <= len f by A1,A2,FINSEQ_4:31,NAT_1:29;
then i <= len f by AXIOMS:22;
hence len(f:-p) = len f - i by A3,RFINSEQ:def 2
.= len f - (p..f - 1) by A2,XCMPLX_1:26
.= len f - p..f + 1 by XCMPLX_1:37;
end;
theorem Th54:
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:27;
then j+1 <= len f - p..f + 1 by A1,Th53;
then j <= len f - p..f by REAL_1:53;
then A3: j+p..f <= len f by REAL_1:84;
1 <= p..f & p..f <= j+p..f by A1,FINSEQ_4:31,NAT_1:29;
then 1 <= j+p..f by AXIOMS:22;
hence j+p..f in dom f by A3,FINSEQ_3:27;
end;
Lm4:
f:-p is non empty
proof f:-p = <*p*>^(f/^p..f) by Def2;
then len(f:-p) = 1 + len(f/^p..f) by Th8;
hence thesis by FINSEQ_1:25;
end;
definition let D,p,f;
cluster f:-p -> non empty;
coherence by Lm4;
end;
theorem Th55:
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);
set i = j+1;
consider k such that
A3: k+1 = p..f and
A4: f:-p = f/^k by A1,Th52;
k <= p..f & p..f <= len f by A1,A3,FINSEQ_4:31,NAT_1:29;
then A5: k <= len f by AXIOMS:22;
A6: j+p..f in dom f by A1,A2,Th54;
thus (f:-p)/.i = (f:-p).i by A2,FINSEQ_4:def 4
.= f.(i+k) by A2,A4,A5,RFINSEQ:def 2
.= f.(j+p..f) by A3,XCMPLX_1:1
.= f/.(j+p..f) by A6,FINSEQ_4:def 4;
end;
theorem
(f:-p)/.1 = p
proof f:-p = <*p*>^(f/^p..f) by Def2;
hence thesis by Th16;
end;
theorem
p in rng f implies (f:-p)/.(len(f:-p)) = f/.len f
proof assume
A1: p in rng f;
then p..f <= len f by FINSEQ_4:31;
then reconsider j = len f - p..f as Nat by INT_1:18;
A2: len(f:-p) = j + 1 by A1,Th53;
len(f:-p) in dom(f:-p) by Th6;
hence (f:-p)/.(len(f:-p)) = f/.(j+p..f) by A1,A2,Th55
.= f/.len f by XCMPLX_1:27;
end;
theorem
p in rng f implies rng(f:-p) c= rng f
proof assume p in rng f;
then ex i st i+1 = p..f & f:-p = f/^i by Th52;
hence thesis by Th36;
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 st i+1 = p..f & f:-p = f/^i by Th52;
hence thesis by Lm3;
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 st k in dom p holds p.k = F(k) from domSeqLambda;
hence thesis;
end;
uniqueness
proof let f1,f2 be FinSequence such that
A1: len f1 = len f and
A2: for i st i in dom f1 holds f1.i = f.(len f - i + 1) and
A3: len f2 = len f and
A4: for i st i in dom f2 holds f2.i = f.(len f - i + 1);
A5: dom f1 = Seg len f1 & dom f2 = Seg len f2 & dom f = Seg len f
by FINSEQ_1:def 3;
now let i; assume i in dom f;
then f1.i = f.(len f - i + 1) & f2.i = f.(len f - i + 1)
by A1,A2,A3,A4,A5;
hence f1.i = f2.i;
end;
hence thesis by A1,A3,A5,FINSEQ_2:10;
end;
end;
theorem Th60:
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 set;
assume x in rng f;
then consider i such that
A3: i in dom f and
A4: f.i = x by FINSEQ_2:11;
i <= len f by A3,FINSEQ_3:27;
then reconsider j = len f - i + 1 as Nat by Th1;
A5: len f - j + 1 = len f - (len f - i) - 1 + 1 by XCMPLX_1:36
.= len f - (len f - i) by XCMPLX_1:27
.= len f - len f + i by XCMPLX_1:37
.= 0 + i by XCMPLX_1:14
.= i;
dom f = Seg len f by FINSEQ_1:def 3;
then j in Seg len (Rev f) by A2,A3,Th2;
then A6: 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,A6,FUNCT_1:def 5;
end;
let x be set;
assume x in rng(Rev f);
then consider i such that
A7: i in dom(Rev f) and
A8: (Rev f).i = x by FINSEQ_2:11;
A9: (Rev f).i = f.(len f - i + 1) by A7,Def3;
i <= len f by A2,A7,FINSEQ_3:27;
then reconsider j = len f - i + 1 as Nat by Th1;
i in Seg len(Rev f) by A7,FINSEQ_1:def 3;
then j in Seg len (Rev f) by A2,Th2;
then j in dom (Rev f) by FINSEQ_1:def 3;
hence x in rng f by A1,A8,A9,FUNCT_1:def 5;
end;
theorem Th61:
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 Th60;
hence thesis by Def3;
end;
theorem Th62:
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 by FINSEQ_1:def 3;
A4: j = len f + 1 - i by A2,XCMPLX_1:26
.= len f - i + 1 by XCMPLX_1:29;
dom f = dom Rev f by Th60;
hence j in dom Rev f by A1,A3,A4,Th2;
end;
definition let f be empty FinSequence;
cluster Rev f -> empty;
coherence
proof len {} = 0 by FINSEQ_1:25;
then len (Rev {}) = 0 by Def3;
hence thesis by FINSEQ_1:25;
end;
end;
theorem
for x being set holds Rev <*x*> = <*x*>
proof let x be set;
set f = <*x*>;
A1: len f = 1 by FINSEQ_1:56;
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:4,TARSKI:def 1;
hence f.i = f.(len f - i + 1) by A1;
end;
hence thesis by Def3;
end;
theorem
for x1,x2 being set holds Rev <*x1,x2*> = <*x2,x1*>
proof let x1,x2 be set;
set f = <*x1,x2*>, g = <*x2,x1*>;
A1: len f = 2 & len g = 2 by FINSEQ_1:61;
now let i; assume i in dom g;
then A2: i in Seg len f by A1,FINSEQ_1:def 3;
per cases by A1,A2,FINSEQ_1:4,TARSKI:def 2;
suppose
A3: i = 1;
hence g.i = x2 by FINSEQ_1:61
.= f.(len f - i + 1) by A1,A3,FINSEQ_1:61;
suppose
A4: i = 2;
hence g.i = x1 by FINSEQ_1:61
.= f.(len f - i + 1) by A1,A4,FINSEQ_1:61;
end;
hence thesis by A1,Def3;
end;
theorem Th65:
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;
then A2: dom Rev f = {} by Th60,RELAT_1:60;
thus f.1 = {} by A1,FUNCT_1:def 4,RELAT_1:60 .= (Rev f).(len f) by A2,
FUNCT_1:def 4;
thus f.(len f) = {} by A1,FUNCT_1:def 4,RELAT_1:60 .= (Rev f).1 by A2,
FUNCT_1:def 4;
suppose f is non empty;
then A3: len f <> 0 by FINSEQ_1:25;
then len f in Seg len f by FINSEQ_1:5;
then len f in dom f by FINSEQ_1:def 3;
hence (Rev f).(len f) = f.(len f - len f + 1) by Th61
.= f.(0 + 1) by XCMPLX_1:14
.= f.1;
1 >= 1 & len f >= 1 by A3,RLVECT_1:99;
then 1 in dom f by FINSEQ_3:27;
hence (Rev f).1 = f.(len f - 1 + 1) by Th61
.= f.(len f) by XCMPLX_1:27;
end;
definition let f be one-to-one FinSequence;
cluster Rev f -> one-to-one;
coherence
proof
set g = Rev f;
let x1,x2 be set such that
A1: x1 in dom g & x2 in dom g and
A2: g.x1 = g.x2;
reconsider i1 = x1, i2 = x2 as Nat by A1;
A3: dom g = Seg len g by FINSEQ_1:def 3;
A4: len g = len f by Def3;
then i1 <= len f & i2 <= len f by A1,FINSEQ_3:27;
then reconsider i1' = len f - i1 + 1, i2' = len f - i2 + 1 as Nat by Th1;
dom f = Seg len f by FINSEQ_1:def 3;
then A5: i1' in dom f & i2' in dom f by A1,A3,A4,Th2;
f.i1' = g.x1 by A1,Def3
.= f.i2' by A1,A2,Def3;
then i1' = i2' by A5,FUNCT_1:def 8;
then len f - i1 = len f - i2 by XCMPLX_1:2;
hence x1 = x2 by XCMPLX_1:20;
end;
end;
theorem Th66:
for f being FinSequence, x being set holds Rev(f^<*x*>) = <*x*>^(Rev f)
proof let f be FinSequence, x be set;
set n = len f + 1, g = <*x*>;
A1: len (f^g) = n by FINSEQ_2:19;
A2: len(g^(Rev f)) = len g + len (Rev f) by FINSEQ_1:35
.= 1 + len (Rev f) by FINSEQ_1:56
.= n by Def3;
A3: len(Rev(f^g)) = n by A1,Def3;
now let i; assume
A4: i in Seg n;
then A5: 1 <= i & i <= n by FINSEQ_1:3;
A6: len g = 1 by FINSEQ_1:57;
A7: i in dom(Rev(f^g)) by A3,A4,FINSEQ_1:def 3;
per cases by A5,REAL_1:def 5;
suppose
A8: i = 1;
Seg len g = dom g by FINSEQ_1:def 3;
then A9: 1 in dom g by A6,FINSEQ_1:4,TARSKI:def 1;
thus (Rev(f^g)).i = (f^g).(n-1+1) by A1,A7,A8,Def3
.= (f^g).n by XCMPLX_1:27
.= x by FINSEQ_1:59
.= g.1 by FINSEQ_1:57
.= (g^(Rev f)).i by A8,A9,FINSEQ_1:def 7;
suppose
A10: i > 1;
then reconsider j = i-1 as Nat by RLVECT_2:103;
reconsider k = n - i + 1 as Nat by A5,Th1;
0 < i by A10,AXIOMS:22;
then consider l being Nat such that
A11: i = l + 1 by NAT_1:22;
l <> 0 by A10,A11;
then 1 <= l by RLVECT_1:99;
then A12: 1 <= j by A11,XCMPLX_1:26;
j <= n - 1 by A5,REAL_1:49;
then j <= len f by XCMPLX_1:26;
then A13: j in dom f by A12,FINSEQ_3:27;
i - i <= n - i by A5,REAL_1:49;
then 0 <= n - i by XCMPLX_1:14;
then A14: 0 + 1 <= k by AXIOMS:24;
n < len f + i by A10,REAL_1:67;
then n - i < len f + i - i by REAL_1:54;
then n - i < len f by XCMPLX_1:26;
then k < len f + 1 by REAL_1:53;
then k <= len f by NAT_1:38;
then A15: k in dom f by A14,FINSEQ_3:27;
thus (Rev(f^g)).i = (f^g).(n - i + 1) by A1,A7,Def3
.= f.k by A15,FINSEQ_1:def 7
.= f.(len f + (1 - i) + 1) by XCMPLX_1:29
.= f.(len f - j + 1) by XCMPLX_1:38
.= (Rev f).j by A13,Th61
.= (g^(Rev f)).i by A2,A5,A6,A10,FINSEQ_1:37;
end;
hence thesis by A2,A3,FINSEQ_2:10;
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:47
.= (Rev g)^(Rev f) by FINSEQ_1:47;
end;
A2: for g being FinSequence, x being set st P[g] holds P[g^<*x*>]
proof let g be FinSequence, x be set such that
A3: P[g];
thus Rev(f^(g^<*x*>)) = Rev(f^g^<*x*>) by FINSEQ_1:45
.= <*x*>^((Rev g)^(Rev f)) by A3,Th66
.= <*x*>^(Rev g)^(Rev f) by FINSEQ_1:45
.= (Rev(g^<*x*>))^(Rev f) by Th66;
end;
thus for g being FinSequence holds P[g] from IndSeq(A1,A2);
end;
definition let D,f;
redefine func Rev f -> FinSequence of D;
coherence
proof set n = len f;
A1: dom f = Seg n by FINSEQ_1:def 3;
now let i;
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 i <= n by A1,FINSEQ_3:27;
then j in Seg n & j is Nat by A2,Th1,Th2;
then f.j in D by A1,FINSEQ_2:13;
hence Rev f.i in D by A1,A2,Th61;
end;
hence thesis by FINSEQ_2:14;
end;
end;
theorem
f is non empty implies f/.1 = (Rev f)/.len f & f/.len f = (Rev f)/.1
proof assume
A1: f is non empty;
then A2: 1 in dom f by Th6;
A3: len f in dom f by A1,Th6;
A4: dom f = dom Rev f by Th60;
thus f/.1 = f.1 by A2,FINSEQ_4:def 4
.= (Rev f).len f by Th65
.= (Rev f)/.len f by A3,A4,FINSEQ_4:def 4;
thus f/.len f = f.(len f) by A3,FINSEQ_4:def 4
.= (Rev f).1 by Th65
.= (Rev f)/.1 by A2,A4,FINSEQ_4:def 4;
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: i = len f + 1 - j by A2,XCMPLX_1:26
.= len f - j + 1 by XCMPLX_1:29;
A4: j in dom Rev f by A1,A2,Th62;
thus f/.i = f.i by A1,FINSEQ_4:def 4
.= (Rev f).j by A3,A4,Def3
.= (Rev f)/.j by A4,FINSEQ_4:def 4;
end;
definition let D,f,p,n;
func Ins(f,n,p) -> FinSequence of D equals
:Def4: (f|n)^<*p*>^(f/^n);
correctness;
end;
theorem
Ins(f,0,p) = <*p*>^f
proof
thus Ins(f,0,p) = (f|0)^<*p*>^(f/^0) by Def4
.= <*p*>^(f/^0) by FINSEQ_1:47
.= <*p*>^f by Th31;
end;
theorem Th71:
len f <= n implies Ins(f,n,p) = f^<*p*>
proof assume
A1: len f <= n;
then A2: f/^n is empty by Th35;
thus Ins(f,n,p) = (f|n)^<*p*>^(f/^n) by Def4
.= (f|n)^<*p*> by A2,FINSEQ_1:47
.= f^<*p*> by A1,TOPREAL1:2;
end;
theorem Th72:
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*>^(f/^n)) by Def4
.= len((f|n)^<*p*>) + len(f/^n) by FINSEQ_1:35
.= len((f|n)^<*p*>) + (len f - n) by A1,RFINSEQ:def 2
.= len(f|n)+len<*p*> + (len f - n) by FINSEQ_1:35
.= len(f|n)+1+(len f - n) by FINSEQ_1:56
.= n+1+(len f - n) by A1,TOPREAL1:3
.= len f - n + n + 1 by XCMPLX_1:1
.= len f + 1 by XCMPLX_1:27;
suppose len f < n;
then Ins(f,n,p) = f^<*p*> by Th71;
hence thesis by FINSEQ_2:19;
end;
theorem Th73:
rng Ins(f,n,p) = {p} \/ rng f
proof
thus rng Ins(f,n,p)
= rng((f|n)^<*p*>^(f/^n)) by Def4
.= rng((f|n)^<*p*>) \/ rng(f/^n) by FINSEQ_1:44
.= rng(f|n) \/ rng<*p*> \/ rng(f/^n) by FINSEQ_1:44
.= rng(f|n) \/ rng(f/^n) \/ rng<*p*> by XBOOLE_1:4
.= rng((f|n)^(f/^n)) \/ rng<*p*> by FINSEQ_1:44
.= rng<*p*> \/ rng f by RFINSEQ:21
.= {p} \/ rng f by FINSEQ_1:55;
end;
definition let D,f,n,p;
cluster Ins(f,n,p) -> non empty;
coherence
proof
len(Ins(f,n,p)) = len f + 1 by Th72;
hence thesis by FINSEQ_1:25;
end;
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 2;
hence thesis by Th73;
end;
theorem Th75:
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 Def4
.= ((f|n)^(<*p*>^(f/^n)))/.i by FINSEQ_1:45
.= (f|n)/.i by A1,Lm1
.= f/.i by A1,TOPREAL1:1;
end;
theorem
n <= len f implies (Ins(f,n,p))/.(n+1) = p
proof assume
n <= len f;
then A1: len(f|n) = n by TOPREAL1:3;
then A2: len((f|n)^<*p*>) = n+1 by FINSEQ_2:19;
1 <= n+1 by NAT_1:29;
then A3: n+1 in dom((f|n)^<*p*>) by A2,FINSEQ_3:27;
thus (Ins(f,n,p))/.(n+1) = ((f|n)^<*p*>^(f/^n))/.(n+1) by Def4
.= ((f|n)^<*p*>)/.(n+1) by A3,Lm1
.= p by A1,TOPREAL4:1;
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;
n <= n+1 by NAT_1:29;
then n <= i by A1,AXIOMS:22;
then A3: n <= len f by A2,AXIOMS:22;
then len(f|n) = n by TOPREAL1:3;
then A4: len((f|n)^<*p*>) = n+1 by FINSEQ_2:19;
reconsider j = i - (n+1) as Nat by A1,INT_1:18;
A5: n+1+j = i by XCMPLX_1:27;
then A6: n+1+(j+1) = i+1 by XCMPLX_1:1;
A7: 1 <= j+1 by NAT_1:29;
n+(j+1) <= len f by A2,A5,XCMPLX_1:1;
then j+1 <= len f - n by REAL_1:84;
then j+1 <= len(f/^n) by A3,RFINSEQ:def 2;
then A8: j+1 in dom(f/^n) by A7,FINSEQ_3:27;
thus (Ins(f,n,p))/.(i+1) = ((f|n)^<*p*>^(f/^n))/.(i+1) by Def4
.= (f/^n)/.(j+1) by A4,A6,A8,GROUP_5:96
.= f/.(n+(j+1)) by A8,Th30
.= f/.i by A5,XCMPLX_1:1;
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;
len f <> 0 by A2,FINSEQ_1:25;
then A3: 1 <= len f by RLVECT_1:99;
n <= len f implies len(f|n) = n by TOPREAL1:3;
then 1 <= len(f|n) by A1,A3,TOPREAL1:2;
then 1 in dom(f|n) by FINSEQ_3:27;
hence thesis by Th75;
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;
A3: f|n is one-to-one by A1,Lm2;
A4: <*p*> is one-to-one by FINSEQ_3:102;
now let x be set;
assume x in rng<*p*>;
then x in {p} by FINSEQ_1:55;
then A5: not x in rng f by A2,TARSKI:def 1;
rng(f|n) c= rng f by Th21;
hence not x in rng(f|n) by A5;
end;
then rng(f|n) misses rng<*p*> by XBOOLE_0:3;
then A6: (f|n) ^ <*p*> is one-to-one by A3,A4,FINSEQ_3:98;
A7: f/^n is one-to-one by A1,Lm3;
now let x be set;
assume
A8: x in rng(f/^n);
rng(f|n) misses rng(f/^n) by A1,Th37;
then A9: not x in rng(f|n) by A8,XBOOLE_0:3;
rng(f/^n) c= rng f by Th36;
then x in rng f by A8;
then not x in {p} by A2,TARSKI:def 1;
then not x in rng<*p*> by FINSEQ_1:55;
then not x in rng(f|n) \/ rng<*p*> by A9,XBOOLE_0:def 2;
hence not x in rng((f|n) ^ <*p*>) by FINSEQ_1:44;
end;
then rng((f|n) ^ <*p*>) misses rng(f/^n) by XBOOLE_0:3;
then (f|n) ^ <*p*> ^ (f/^n) is one-to-one by A6,A7,FINSEQ_3:98;
hence thesis by Def4;
end;