:: Non-contiguous Substrings and One-to-one Finite Sequences
:: by Wojciech A. Trybulec
::
:: Received April 8, 1990
:: Copyright (c) 1990-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, FINSEQ_1, XBOOLE_0, ARYTM_3, CARD_1, XXREAL_0, ARYTM_1,
NAT_1, SUBSET_1, TARSKI, RELAT_1, ORDINAL4, FUNCT_1, FINSET_1, FINSEQ_2,
FUNCT_2, CARD_3, FUNCOP_1, FINSEQ_3, EQREL_1, ALG_1, FUNCT_6, SETFAM_1,
FINSEQ_4, ZFMISC_1, FUNCT_5, PARTFUN1, XCMPLX_0, ORDINAL1, NUMBER09;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, CARD_1, ORDINAL1,
ZFMISC_1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, FINSEQ_1, RELSET_1,
PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, FINSEQ_2, FINSET_1, NAT_1,
FINSEQOP, XXREAL_0, CARD_3, FUNCT_3, FUNCT_5, FUNCT_6, EQREL_1;
constructors ENUMSET1, PARTFUN1, WELLORD2, XXREAL_0, REAL_1, NAT_1, INT_1,
FINSEQOP, RELSET_1, CARD_3, DOMAIN_1, CARD_2, EQREL_1, FUNCT_6, BINOP_1,
FUNCT_3, FUNCT_5, FINSEQ_2, VALUED_0;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0,
XREAL_0, NAT_1, INT_1, FINSEQ_1, CARD_1, FINSEQ_2, FUNCOP_1, CARD_3,
CARD_2, VALUED_0;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions FUNCT_1, TARSKI, WELLORD2, XBOOLE_0, CARD_3, FUNCOP_1;
equalities FINSEQ_2, CARD_3, FUNCOP_1, FUNCT_6;
expansions FUNCT_1, TARSKI, WELLORD2, XBOOLE_0;
theorems CARD_1, CARD_2, ENUMSET1, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_1,
INT_1, NAT_1, TARSKI, WELLORD2, ZFMISC_1, RELAT_1, XREAL_1, XBOOLE_0,
XBOOLE_1, FUNCT_2, GRFUNC_1, SUBSET_1, XXREAL_0, ORDINAL1, NUMBERS,
CARD_3, FUNCOP_1, EQREL_1, FUNCT_6, SETFAM_1, FUNCT_5, FUNCT_3, XTUPLE_0;
schemes FINSEQ_1, FUNCT_1, NAT_1, CLASSES1, RELSET_1;
begin
reserve p,q,r for FinSequence;
reserve u,v,x,y,y1,y2,z for object, A,D,X,Y for set;
reserve i,j,k,l,m,n for Nat;
theorem Th1:
Seg 3 = {1,2,3}
proof
thus Seg 3 = {1,2} \/ {2 + 1} by FINSEQ_1:2,9
.= {1,2,3} by ENUMSET1:3;
end;
theorem Th2:
Seg 4 = {1,2,3,4}
proof
thus Seg 4 = {1,2,3} \/ {3 + 1} by Th1,FINSEQ_1:9
.= {1,2,3,4} by ENUMSET1:6;
end;
theorem Th3:
Seg 5 = {1,2,3,4,5}
proof
thus Seg 5 = {1,2,3,4} \/ {4 + 1} by Th2,FINSEQ_1:9
.= {1,2,3,4,5} by ENUMSET1:10;
end;
theorem Th4:
Seg 6 = {1,2,3,4,5,6}
proof
thus Seg 6 = {1,2,3,4,5} \/ {5 + 1} by Th3,FINSEQ_1:9
.= {1,2,3,4,5,6} by ENUMSET1:15;
end;
theorem Th5:
Seg 7 = {1,2,3,4,5,6,7}
proof
thus Seg 7 = {1,2,3,4,5,6} \/ {6 + 1} by Th4,FINSEQ_1:9
.= {1,2,3,4,5,6,7} by ENUMSET1:21;
end;
theorem
Seg 8 = {1,2,3,4,5,6,7,8}
proof
thus Seg 8 = {1,2,3,4,5,6,7} \/ {7 + 1} by Th5,FINSEQ_1:9
.= {1,2,3,4,5,6,7,8} by ENUMSET1:28;
end;
theorem Th7:
Seg k = {} iff not k in Seg k
proof
thus Seg k = {} implies not k in Seg k;
assume not k in Seg k;
then k = 0 by FINSEQ_1:3;
hence Seg k = {};
end;
theorem Th8:
not k + 1 in Seg k
proof
assume k + 1 in Seg k;
then
A1: k + 1 <= k by FINSEQ_1:1;
k <= k + 1 by NAT_1:12;
then k + 0 = k + 1 by A1,XXREAL_0:1;
hence thesis;
end;
theorem
k <> 0 implies k in Seg(k + n)
proof
assume k <> 0;
then
A1: 0 + 1 <= k by NAT_1:13;
k <= k + n by NAT_1:12;
hence thesis by A1,FINSEQ_1:1;
end;
theorem Th10:
k + n in Seg k implies n = 0
proof
assume k + n in Seg k;
then k + n <= k + 0 by FINSEQ_1:1;
hence thesis by XREAL_1:6;
end;
theorem
k < n implies k + 1 in Seg n
proof
assume k < n;
then
A1: k + 1 <= n by NAT_1:13;
1 <= k + 1 by NAT_1:12;
hence thesis by A1,FINSEQ_1:1;
end;
theorem Th12:
k in Seg n & m < k implies k - m in Seg n
proof
assume that
A1: k in Seg n and
A2: m < k;
consider i being Nat such that
A3: k = m + i by A2,NAT_1:10;
reconsider x = k - m as Element of NAT by A3,ORDINAL1:def 12;
A4: now
assume not 1 <= x;
then x = 0 by NAT_1:14;
hence contradiction by A2;
end;
A5: k <= n by A1,FINSEQ_1:1;
i <= k by A3,NAT_1:12;
then x <= n by A3,A5,XXREAL_0:2;
hence thesis by A4,FINSEQ_1:1;
end;
theorem
k - n in Seg k iff n < k
proof
thus k - n in Seg k implies n < k
proof
assume
A1: k - n in Seg k;
then reconsider x = k - n as Element of NAT;
assume not n < k;
then k - n <= n - n by XREAL_1:9;
then x = 0;
hence contradiction by A1,FINSEQ_1:1;
end;
thus thesis by Th12,FINSEQ_1:3;
end;
theorem Th14:
Seg k misses {k + 1}
proof
set x = the Element of Seg k /\ {k + 1};
assume not thesis;
then
A1: Seg k /\ {k + 1} <> {};
then
A2: x in Seg k by XBOOLE_0:def 4;
then reconsider x as Element of NAT;
x in {k + 1} by A1,XBOOLE_0:def 4;
then
A3: x = k + 1 by TARSKI:def 1;
x <= k by A2,FINSEQ_1:1;
hence thesis by A3,XREAL_1:29;
end;
theorem
Seg(k + 1) \ Seg k = {k + 1}
proof
A1: Seg(k + 1) = Seg k \/ {k + 1} by FINSEQ_1:9;
Seg k misses {k + 1} by Th14;
hence thesis by A1,XBOOLE_1:88;
end;
:: Theorem Seg(k + 1) \ {k + 1} = Seg k is
:: proved in RLVECT_1 and has a number 104.
theorem
Seg k <> Seg(k + 1) by Th8,FINSEQ_1:4;
theorem
Seg k = Seg(k + n) implies n = 0 by Th10,FINSEQ_1:3;
theorem Th18:
Seg k c= Seg(k + n) by FINSEQ_1:5,NAT_1:12;
theorem Th19:
Seg k, Seg n are_c=-comparable
proof
n <= k or k <= n;
then Seg n c= Seg k or Seg k c= Seg n by FINSEQ_1:5;
hence thesis;
end;
theorem Th20:
for y being object st Seg k = {y} holds k = 1 & y = 1
proof let y be object;
assume
A1: Seg k = {y};
now
per cases;
suppose
k = 0;
hence thesis by A1;
end;
suppose
k <> 0; then
A2: k in Seg k by FINSEQ_1:3;
then 1 <= k by FINSEQ_1:1;
then Seg 1 c= Seg k by FINSEQ_1:5;
then Seg 1 = {y} by A1,ZFMISC_1:33;
hence thesis by A1,A2,FINSEQ_1:2,TARSKI:def 1,ZFMISC_1:3;
end;
end;
hence thesis;
end;
theorem
Seg k = {x,y} & x <> y implies k = 2 & {x,y} = {1,2}
proof
assume that
A1: Seg k = {x,y} and
A2: x <> y;
now
per cases;
suppose
k = 0;
hence thesis by A1;
end;
suppose
A3: k <> 0;
now
per cases;
suppose
k = 1;
hence thesis by A1,A2,FINSEQ_1:2,ZFMISC_1:5;
end;
suppose
A4: k <> 1;
1 <= k by A3,NAT_1:14;
then 1 < k by A4,XXREAL_0:1;
then
A5: 1 + 1 <= k by NAT_1:13;
then Seg 2 c= Seg k by FINSEQ_1:5;
then
A6: 1 = x & 2 = x or 1 = x & 2 = y or 2 = x & 1 = y or 1 = y & 2 =
y by A1,FINSEQ_1:2,ZFMISC_1:22;
now
k in Seg k by A1,Th7;
then
A7: k = 1 or k = 2 by A1,A6,TARSKI:def 2;
assume not k <= 2;
hence contradiction by A7;
end;
hence thesis by A1,A5,FINSEQ_1:2,XXREAL_0:1;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th22:
x in dom p implies x in dom(p ^ q)
proof
dom p c= dom(p ^ q) by FINSEQ_1:26;
hence thesis;
end;
theorem
x in dom p implies x is Element of NAT;
theorem Th24:
x in dom p implies x <> 0
proof
assume x in dom p;
then x in Seg(len p) by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:1;
end;
theorem Th25:
n in dom p iff 1 <= n & n <= len p
proof
thus n in dom p implies 1 <= n & n <= len p
proof
assume n in dom p;
then n in Seg(len p) by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:1;
end;
assume that
A1: 1 <= n and
A2: n <= len p;
n in Seg(len p) by A1,A2,FINSEQ_1:1;
hence thesis by FINSEQ_1:def 3;
end;
theorem
n in dom p iff n - 1 is Element of NAT & len p - n is Element of NAT
proof
thus n in dom p implies n - 1 is Element of NAT & len p - n is Element of NAT
proof
assume
A1: n in dom p; then
A2: n <= len p by Th25;
1 <= n by A1,Th25;
hence thesis by A2,INT_1:5;
end;
assume that
A3: n - 1 is Element of NAT and
A4: len p - n is Element of NAT;
A5: 0 + n <= len p by A4,XREAL_1:19;
0 + 1 <= n by A3,XREAL_1:19;
hence thesis by A5,Th25;
end;
::$CT 2
theorem Th27:
len p = len q iff dom p = dom q
proof
dom p = Seg(len p) by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th28:
len p <= len q iff dom p c= dom q
proof
A1: dom q = Seg(len q) by FINSEQ_1:def 3;
dom p = Seg(len p) by FINSEQ_1:def 3;
hence thesis by A1,FINSEQ_1:5;
end;
theorem Th29:
x in rng p implies 1 in dom p
proof
assume x in rng p;
then p <> {};
then
A1: 1 <= len p by NAT_1:14;
dom p = Seg(len p) by FINSEQ_1:def 3;
hence thesis by A1,FINSEQ_1:1;
end;
theorem
rng p <> {} implies 1 in dom p
proof
set y = the Element of rng p;
assume rng p <> {};
then y in rng p;
hence thesis by Th29;
end;
theorem
{} <> <* x,y *>;
theorem
{} <> <* x,y,z *>;
theorem Th33:
<* x *> <> <* y,z *>
proof
len<* x *> = 1 by FINSEQ_1:40;
hence thesis by FINSEQ_1:44;
end;
theorem
<* u *> <> <* x,y,z *>
proof
len<* u *> = 1 by FINSEQ_1:40;
hence thesis by FINSEQ_1:45;
end;
theorem
<* u,v *> <> <* x,y,z *>
proof
len<* u,v *> = 2 by FINSEQ_1:44;
hence thesis by FINSEQ_1:45;
end;
theorem Th36:
len r = len p + len q & (for k being Nat st k in dom p holds r.k = p.k) &
(for k being Nat st k in dom q holds r.(len p + k) = q.k)
implies r = p ^ q
proof
assume len r = len p + len q;
then
A1: dom r = Seg(len p + len q) by FINSEQ_1:def 3;
assume that
A2: for k being Nat st k in dom p holds r.k = p.k and
A3: for k being Nat st k in dom q holds r.(len p + k) = q.k;
A4: for k being Nat st k in dom q holds r.(len p + k) = q.k by A3;
for k being Nat st k in dom p holds r.k = p.k by A2;
hence thesis by A1,A4,FINSEQ_1:def 7;
end;
registration
let A be included_in_Seg set;
cluster Sgm A -> one-to-one;
coherence
proof
consider k being Nat such that
A1: A c= Seg k by FINSEQ_1:def 13;
A2: rng Sgm A = A by FINSEQ_1:def 14;
let x,y be object;
assume that
A3: x in dom Sgm A and
A4: y in dom Sgm A and
A5: Sgm(A).x = Sgm(A).y and
A6: x <> y;
Sgm(A).y in rng Sgm A by A4,FUNCT_1:def 3; then
A7: Sgm(A).y in Seg k by A1,A2;
Sgm(A).x in rng Sgm A by A3,FUNCT_1:def 3;
then Sgm(A).x in Seg k by A1,A2; then
reconsider m = Sgm(A).x, n = Sgm(A).y as Element of NAT by A7;
reconsider i = x, j = y as Element of NAT by A3,A4;
A8: dom Sgm A = Seg len Sgm A by FINSEQ_1:def 3;
now
per cases by A6,XXREAL_0:1;
suppose
A9: i < j;
A10: j <= len Sgm A by A4,A8,FINSEQ_1:1;
1 <= i by A3,A8,FINSEQ_1:1;
then m < n by A9,A10,FINSEQ_1:def 14;
hence contradiction by A5;
end;
suppose
A11: j < i;
A12: i <= len Sgm A by A3,A8,FINSEQ_1:1;
1 <= j by A4,A8,FINSEQ_1:1;
then n < m by A11,A12,FINSEQ_1:def 14;
hence contradiction by A5;
end;
end;
hence thesis;
end;
end;
theorem Th37:
for A being included_in_Seg set holds len Sgm A = card A
proof
let A be included_in_Seg set;
A1: dom Sgm A = Seg len Sgm A by FINSEQ_1:def 3;
A2: card Seg len Sgm A = len Sgm A by FINSEQ_1:57;
A4: rng Sgm A = A by FINSEQ_1:def 14;
Seg len Sgm A,A are_equipotent by A1,A4;
hence thesis by A2,CARD_1:5;
end;
theorem Th38:
for A being included_in_Seg set holds dom Sgm A = Seg card A
proof
let A be included_in_Seg set;
len Sgm A = card A by Th37;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th39:
X is included_in_Seg & k < l & 1 <= n & m <= len Sgm X & Sgm(X).m = k &
Sgm(X).n = l implies m < n
proof
assume that
A1: X is included_in_Seg and
A2: k < l and
A3: 1 <= n and
A4: m <= len(Sgm X) and
A5: Sgm(X).m = k and
A6: Sgm(X).n = l and
A7: not m < n;
n < m by A2,A5,A6,A7,XXREAL_0:1;
hence thesis by A1,A2,A3,A4,A5,A6,FINSEQ_1:def 14;
end;
theorem Th40:
X is included_in_Seg & Y is included_in_Seg implies
( (for m,n being Nat st m in X & n in Y holds m < n) iff
Sgm(X \/ Y) = Sgm(X) ^ Sgm(Y) )
proof
assume that
a1: X is included_in_Seg and
a2: Y is included_in_Seg;
consider i such that
A1: X c= Seg i by a1,FINSEQ_1:def 13;
consider j such that
A2: Y c= Seg j by a2,FINSEQ_1:def 13;
set r = Sgm(X \/ Y);
set q = Sgm Y;
set p = Sgm X;
Seg i, Seg j are_c=-comparable by Th19;
then Seg i c= Seg j or Seg j c= Seg i;
then
X c= Seg j or Y c= Seg i by A1,A2;
then
A4: X \/ Y c= Seg i or X \/ Y c= Seg j by A1,A2,XBOOLE_1:8;
reconsider X1 = X, Y1 = Y as finite set by A1,A2;
bbb: X1 \/ Y1 is included_in_Seg by A4,FINSEQ_1:def 13;
thus (for m,n being Nat st m in X & n in Y holds m < n) implies
Sgm(X \/ Y) = Sgm(X) ^ Sgm(Y)
proof
defpred P[Nat] means $1 in dom p implies r.$1 = p.$1;
assume
A5: for m,n being Nat st m in X & n in Y holds m < n;
X /\ Y = {}
proof
set x = the Element of X /\ Y;
X = rng p by a1,FINSEQ_1:def 14;
then
A6: X c= NAT;
assume
A7: not thesis;
then x in X by XBOOLE_0:def 4;
then reconsider m = x as Element of NAT by A6;
A8: m in Y by A7,XBOOLE_0:def 4;
m in X by A7,XBOOLE_0:def 4;
hence thesis by A5,A8;
end;
then
A9: X misses Y;
A10: len r = card(X1 \/ Y1) by a1,a2,Th37
.= card X1 + card Y1 by A9,CARD_2:40
.= len p + card Y1 by a1,Th37
.= len p + len q by a2,Th37;
A11: now
let k be Nat;
assume
A12: P[k];
thus P[k+1]
proof
assume
A13: k + 1 in dom p;
then
A14: p.(k + 1) in rng p by FUNCT_1:def 3;
then reconsider n = p.(k + 1) as Element of NAT;
A15: n in X by a1,A14,FINSEQ_1:def 14;
len p <= len r by A10,NAT_1:12;
then Seg(len p) c= Seg(len r) by FINSEQ_1:5;
then dom p c= Seg(len r) by FINSEQ_1:def 3;
then
A16: dom p c= dom r by FINSEQ_1:def 3;
then
A17: r.(k + 1) in rng r by A13,FUNCT_1:def 3;
then reconsider m = r.(k + 1) as Element of NAT;
rng r = X \/ Y by bbb,FINSEQ_1:def 14;
then
A18: m in X \/ Y by A17;
assume
A19: r.(k + 1) <> p.(k + 1);
A20: k + 1 in dom r by A13,A16;
now
per cases;
suppose
A21: k in dom p;
then p.k in rng p by FUNCT_1:def 3;
then reconsider n1 = p.k as Element of NAT;
r.k in rng r by A16,A21,FUNCT_1:def 3;
then reconsider m1 = r.k as Element of NAT;
now
per cases by A19,XXREAL_0:1;
suppose
A22: m < n;
A23: 1 <= k + 1 by A13,Th25;
not m in Y by A5,A15,A22;
then m in X by A18,XBOOLE_0:def 3;
then m in rng p by a1,FINSEQ_1:def 14;
then consider x being object such that
A24: x in dom p and
A25: p.x = m by FUNCT_1:def 3;
reconsider x as Element of NAT by A24;
x <= len p by A24,Th25;
then
A26: x < k + 1 by a1,A22,A25,A23,Th39;
k + 1 in Seg(len r) by A20,FINSEQ_1:def 3;
then
A27: k + 1 <= len r by FINSEQ_1:1;
k in Seg(len p) by A21,FINSEQ_1:def 3;
then
A28: 1 <= k by FINSEQ_1:1;
k < k + 1 by XREAL_1:29;
then
A29: n1 < m by bbb,A12,A21,A28,A27,FINSEQ_1:def 14;
A30: k <= len p by A21,Th25;
1 <= x by A24,Th25;
then k < x by a1,A25,A29,A30,Th39;
hence contradiction by A26,NAT_1:13;
end;
suppose
A31: n < m;
A32: 1 <= k + 1 by A13,Th25;
n in X \/ Y by A15,XBOOLE_0:def 3;
then n in rng r by bbb,FINSEQ_1:def 14;
then consider x being object such that
A33: x in dom r and
A34: r.x = n by FUNCT_1:def 3;
reconsider x as Element of NAT by A33;
x <= len r by A33,Th25;
then
A35: x < k + 1 by bbb,A31,A34,A32,Th39;
A36: k + 1 <= len p by A13,Th25;
A37: k < k + 1 by XREAL_1:29;
1 <= k by A21,Th25;
then
A38: m1 < n by a1,A12,A21,A37,A36,FINSEQ_1:def 14;
A39: k <= len r by A16,A21,Th25;
1 <= x by A33,Th25;
then k < x by bbb,A34,A38,A39,Th39;
hence contradiction by A35,NAT_1:13;
end;
end;
hence contradiction;
end;
suppose
A40: not k in dom p;
A41: k < k + 1 by XREAL_1:29;
k < 1 or len p < k by A40,Th25;
then
A42: k = 0 or len p < k + 1 & k + 1 <= len p by A13,A41,Th25,NAT_1:14
,XXREAL_0:2;
now
per cases by A19,XXREAL_0:1;
suppose
A43: m < n;
then not m in Y by A5,A15;
then m in X by A18,XBOOLE_0:def 3;
then m in rng p by a1,FINSEQ_1:def 14;
then consider x being object such that
A44: x in dom p and
A45: p.x = m by FUNCT_1:def 3;
A46: 1 <= k + 1 by A13,Th25;
reconsider x as Element of NAT by A44;
x <= len p by A44,Th25;
then x < k + 1 by a1,A43,A45,A46,Th39;
hence contradiction by A42,A44,Th24,NAT_1:14;
end;
suppose
A47: n < m;
A48: 1 <= k + 1 by A13,Th25;
n in X \/ Y by A15,XBOOLE_0:def 3;
then n in rng r by bbb,FINSEQ_1:def 14;
then consider x being object such that
A49: x in dom r and
A50: r.x = n by FUNCT_1:def 3;
reconsider x as Element of NAT by A49;
x <= len r by A49,Th25;
then x < k + 1 by bbb,A47,A50,A48,Th39;
hence contradiction by A42,A49,Th24,NAT_1:14;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
end;
A51: P[0] by Th24;
A52: for k being Nat holds P[k] from NAT_1:sch 2(A51,A11);
defpred P[Nat] means $1 in dom q implies r.(len p + $1) = q.$1;
A53: now
let k be Nat;
assume
A54: P[k];
thus P[k+1]
proof
set a = len p + (k + 1);
assume
A55: k + 1 in dom q;
then k + 1 <= len q by Th25;
then
A56: a <= len r by A10,XREAL_1:7;
A57: 1 <= k + 1 by NAT_1:12;
then 1 <= a by NAT_1:12;
then
A58: a in dom r by A56,Th25;
then
A59: r.a in rng r by FUNCT_1:def 3;
reconsider m = r.a as Element of NAT by A59;
A60: now
assume m in X;
then m in rng p by a1,FINSEQ_1:def 14;
then consider x being object such that
A61: x in dom p and
A62: p.x = m by FUNCT_1:def 3;
reconsider x as Element of NAT by A61;
x <= len p by A61,Th25;
then
A63: x <= len r by A10,NAT_1:12;
A64: r is one-to-one by bbb;
1 <= x by A61,Th25;
then
A65: x in dom r by A63,Th25;
r.x = r.a by A52,A61,A62;
then x = a by A58,A64,A65;
then len p + (k + 1) <= len p + 0 by A61,Th25;
hence contradiction by XREAL_1:29;
end;
A66: q.(k + 1) in rng q by A55,FUNCT_1:def 3;
then reconsider n = q.(k + 1) as Element of NAT;
A67: n in Y by a2,A66,FINSEQ_1:def 14;
assume
A68: r.(len p + (k + 1)) <> q.(k + 1);
A69: m in X \/ Y by bbb,A59,FINSEQ_1:def 14;
now
per cases;
suppose
A70: k in dom q;
then q.k in rng q by FUNCT_1:def 3;
then reconsider n1 = q.k as Element of NAT;
1 <= k by A70,Th25;
then
A71: 1 <= len p + k by NAT_1:12;
A72: k <= len q by A70,Th25;
then len p + k <= len r by A10,XREAL_1:7;
then len p + k in dom r by A71,Th25;
then r.(len p + k) in rng r by FUNCT_1:def 3;
then reconsider m1 = r.(len p + k) as Element of NAT;
now
per cases by A68,XXREAL_0:1;
suppose
A73: m < n;
A74: 1 <= k + 1 by A55,Th25;
m in Y by A69,A60,XBOOLE_0:def 3;
then m in rng q by a2,FINSEQ_1:def 14;
then consider x being object such that
A75: x in dom q and
A76: q.x = m by FUNCT_1:def 3;
reconsider x as Element of NAT by A75;
x <= len q by A75,Th25;
then
A77: x < k + 1 by a2,A73,A76,A74,Th39;
len p + k < len p + k + 1 by XREAL_1:29;
then
A78: n1 < m by bbb,A54,A56,A70,A71,FINSEQ_1:def 14;
A79: k <= len q by A70,Th25;
1 <= x by A75,Th25;
then k < x by a2,A76,A78,A79,Th39;
hence contradiction by A77,NAT_1:13;
end;
suppose
A80: n < m;
A81: 1 <= a by A57,NAT_1:12;
n in X \/ Y by A67,XBOOLE_0:def 3;
then n in rng r by bbb,FINSEQ_1:def 14;
then consider x being object such that
A82: x in dom r and
A83: r.x = n by FUNCT_1:def 3;
reconsider x as Element of NAT by A82;
x <= len r by A82,Th25;
then
A84: x < len p + k + 1
by a1,a2,A80,A83,A81,Th39;
A85: k + 1 <= len q by A55,Th25;
A86: k < k + 1 by XREAL_1:29;
1 <= k by A70,Th25;
then
A87: m1 < n by a2,A54,A70,A86,A85,FINSEQ_1:def 14;
A88: len p + k <= len r by A10,A72,XREAL_1:7;
1 <= x by A82,Th25;
then len p + k < x
by a1,a2,A83,A87,A88,Th39;
hence contradiction by A84,NAT_1:13;
end;
end;
hence contradiction;
end;
suppose
A89: not k in dom q;
A90: k < k + 1 by XREAL_1:29;
k < 1 or len q < k by A89,Th25;
then
A91: k = 0 or len q < k + 1 & k + 1 <= len q by A55,A90,Th25,NAT_1:14
,XXREAL_0:2;
now
per cases by A68,XXREAL_0:1;
suppose
A92: m < n;
A93: 1 <= k + 1 by A55,Th25;
m in Y by A69,A60,XBOOLE_0:def 3;
then m in rng q by a2,FINSEQ_1:def 14;
then consider x being object such that
A94: x in dom q and
A95: q.x = m by FUNCT_1:def 3;
reconsider x as Element of NAT by A94;
x <= len q by A94,Th25;
then x < k + 1 by a2,A92,A95,A93,Th39;
hence contradiction by A91,A94,Th24,NAT_1:14;
end;
suppose
A96: n < m;
A97: 1 <= len p + 1 by NAT_1:12;
n in X \/ Y by A67,XBOOLE_0:def 3;
then n in rng r by bbb,FINSEQ_1:def 14;
then consider x being object such that
A98: x in dom r and
A99: r.x = n by FUNCT_1:def 3;
reconsider x as Element of NAT by A98;
x <= len r by A98,Th25;
then x < len p + 1
by a1,a2,A91,A96,A99,A97,Th39;
then
A100: x <= len p by NAT_1:13;
1 <= x by A98,Th25;
then
A101: x in dom p by A100,Th25;
then
A102: p.x in rng p by FUNCT_1:def 3;
n = p.x by A52,A99,A101;
then n in X by a1,A102,FINSEQ_1:def 14;
hence contradiction by A5,A67;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
end;
A103: P[0] by Th24;
for k being Nat holds P[k] from NAT_1:sch 2(A103,A53);
hence thesis by A10,A52,Th36;
end;
assume
A104: Sgm(X \/ Y) = Sgm(X) ^ Sgm(Y);
let m,n be Nat;
assume that
A105: m in X and
A106: n in Y;
n in rng q by a2,A106,FINSEQ_1:def 14;
then consider y being object such that
A107: y in dom q and
A108: q.y = n by FUNCT_1:def 3;
reconsider y as Element of NAT by A107;
A109: n = r.(len p + y) by A104,A107,A108,FINSEQ_1:def 7;
y <= len q by A107,Th25;
then len p + y <= len p + len q by XREAL_1:7;
then
A110: len p + y <= len r by A104,FINSEQ_1:22;
m in rng(Sgm X) by a1,A105,FINSEQ_1:def 14;
then consider x being object such that
A111: x in dom p and
A112: p.x = m by FUNCT_1:def 3;
reconsider x as Element of NAT by A111;
A113: x in Seg(len p) by A111,FINSEQ_1:def 3;
then
A114: 1 <= x by FINSEQ_1:1;
A115: x <= len p by A113,FINSEQ_1:1;
y <> 0 by A107,Th24;
then
A116: x < len p + y by A115,NAT_1:16,XXREAL_0:2;
m = r.x by A104,A111,A112,FINSEQ_1:def 7;
hence thesis by bbb,A109,A114,A116,A110,FINSEQ_1:def 14;
end;
theorem Th41:
Sgm {} = {} by FINSEQ_1:51;
:: The other way of the one above - FINSEQ_1:72.
theorem Th42:
0 <> n implies Sgm{n} = <* n *>
proof
assume 0 <> n;
then n in Seg n by FINSEQ_1:3;
then {n} c= Seg n by ZFMISC_1:31;
then
A3: {n} is included_in_Seg by FINSEQ_1:def 13;
then len(Sgm{n}) = card{n} by Th37;
then
A2: len(Sgm{n}) = 1 by CARD_1:30;
rng(Sgm{n}) = {n} by A3,FINSEQ_1:def 14;
hence thesis by A2,FINSEQ_1:39;
end;
theorem
0 < n & n < m implies Sgm{n,m} = <* n,m *>
proof
assume that
A1: 0 < n and
A2: n < m;
A3: m in Seg m by A2,FINSEQ_1:3;
A4: n in Seg n by A1,FINSEQ_1:3;
Seg n c= Seg m by A2,FINSEQ_1:5;
then {n,m} c= Seg m by A3,A4,ZFMISC_1:32;
then
a5: {n,m} is included_in_Seg by FINSEQ_1:def 13;
then
A6: Sgm{n,m} is one-to-one;
A7: len(Sgm{n,m}) = card{n,m} by a5,Th37
.= 2 by A2,CARD_2:57;
then
A8: dom(Sgm{n,m}) = {1,2} by FINSEQ_1:2,def 3;
then
A9: 1 in dom(Sgm{n,m}) by TARSKI:def 2;
A10: 2 in dom(Sgm{n,m}) by A8,TARSKI:def 2;
A11: rng(Sgm{n,m}) = {n,m} by a5,FINSEQ_1:def 14;
then
A12: Sgm{n,m}.2 in {n,m} by A10,FUNCT_1:def 3;
A13: Sgm{n,m}.1 in {n,m} by A9,A11,FUNCT_1:def 3;
now
per cases by A13,A12,TARSKI:def 2;
suppose
Sgm{n,m}.1 = n & Sgm{n,m}.2 = n;
hence Sgm{n,m}.1 = n & Sgm{n,m}.2 = m by A9,A10,A6;
end;
suppose
Sgm{n,m}.1 = m & Sgm{n,m}.2 = m;
hence Sgm{n,m}.1 = n & Sgm{n,m}.2 = m by A9,A10,A6;
end;
suppose
Sgm{n,m}.1 = n & Sgm{n,m}.2 = m;
hence Sgm{n,m}.1 = n & Sgm{n,m}.2 = m;
end;
suppose
Sgm{n,m}.1 = m & Sgm{n,m}.2 = n;
hence Sgm{n,m}.1 = n & Sgm{n,m}.2 = m by A2,a5,A7,FINSEQ_1:def 14;
end;
end;
hence thesis by A7,FINSEQ_1:44;
end;
theorem Th44:
len Sgm Seg k = k
proof
card Seg k = k by FINSEQ_1:57;
hence thesis by Th37;
end;
Lm2: Sgm Seg(k + 0) | Seg k = Sgm Seg k
proof
card(Seg k) = k by FINSEQ_1:57;
then len Sgm Seg k = k by Th37;
then dom Sgm Seg k = Seg k by FINSEQ_1:def 3;
hence thesis;
end;
Lm3: now
let n;
assume
A1: for k holds Sgm Seg(k + n) | Seg k = Sgm Seg k;
let k;
set X = Sgm Seg(k + (n + 1));
set Y = Sgm Seg(k + 1);
A2: Y | Seg k = Sgm Seg k
proof
reconsider p = Y | Seg k as FinSequence of NAT by FINSEQ_1:18;
A3: len Y = k + 1 by Th44;
then
A4: dom Y = Seg(k + 1) by FINSEQ_1:def 3;
A5: k <= k + 1 by NAT_1:12;
then
A6: dom p = Seg k by A3,FINSEQ_1:17;
A7: rng Y = Seg(k + 1) by FINSEQ_1:def 14;
A8: Y.(k + 1) = k + 1
proof
k + 1 in dom Y by A4,FINSEQ_1:4;
then
A9: Y.(k + 1) in Seg(k + 1) by A7,FUNCT_1:def 3;
then reconsider n = Y.(k + 1) as Element of NAT;
A10: k < k + 1 by XREAL_1:29;
k + 1 in rng Y by A7,FINSEQ_1:4;
then consider x being object such that
A11: x in dom Y and
A12: Y.x = k + 1 by FUNCT_1:def 3;
reconsider x as Element of NAT by A11;
assume not thesis;
then not Y.(k + 1) in {k + 1} by TARSKI:def 1;
then Y.(k + 1) in Seg(k + 1) \ {k + 1} by A9,XBOOLE_0:def 5;
then
A13: Y.(k + 1) in Seg k by FINSEQ_1:10;
A14: x <> k + 1 by A12,A13,FINSEQ_1:1,XREAL_1:29;
x <= k + 1 by A3,A11,Th25;
then
A15: x < k + 1 by A14,XXREAL_0:1;
1 <= x by A11,Th25;
then
A16: k + 1 < n by A3,A12,A15,FINSEQ_1:def 14;
n <= k by A13,FINSEQ_1:1;
hence contradiction by A16,A10,XXREAL_0:2;
end;
A17: Y is one-to-one;
rng p = rng Y \ {Y.(k + 1)}
proof
thus rng p c= rng Y \ {Y.(k + 1)}
proof
let x be object;
assume
A18: x in rng p;
A19: now
assume x in {k + 1};
then
A20: x = k + 1 by TARSKI:def 1;
A21: k < k + 1 by XREAL_1:29;
A22: k + 1 in dom Y by A4,FINSEQ_1:4;
A23: Seg k c= Seg(k + 1) by Th18;
consider y being object such that
A24: y in dom p and
A25: p.y = x by A18,FUNCT_1:def 3;
reconsider y as Element of NAT by A24;
A26: Y.y = p.y by A24,FUNCT_1:47;
y <= k by A6,A24,FINSEQ_1:1;
hence contradiction by A17,A4,A6,A8,A24,A25,A23,A26,A20,A22,A21;
end;
rng p c= rng Y by RELAT_1:70;
hence thesis by A8,A18,A19,XBOOLE_0:def 5;
end;
let x be object;
assume
A27: x in rng Y \ {Y.(k + 1)};
then x in rng Y by XBOOLE_0:def 5;
then consider y being object such that
A28: y in dom Y and
A29: Y.y = x by FUNCT_1:def 3;
now
assume y in {k + 1};
then
A30: x = k + 1 by A8,A29,TARSKI:def 1;
not x in {k + 1} by A8,A27,XBOOLE_0:def 5;
hence contradiction by A30,TARSKI:def 1;
end;
then y in Seg(k + 1) \ {k + 1} by A4,A28,XBOOLE_0:def 5;
then
A31: y in dom p by A6,FINSEQ_1:10;
then p.y = Y.y by FUNCT_1:47;
hence thesis by A29,A31,FUNCT_1:def 3;
end;
then
A32: rng p = Seg k by A7,A8,FINSEQ_1:10;
now
A33: len p = k by A3,A5,FINSEQ_1:17;
let i,j;
assume that
A34: 1 <= i and
A35: i < j and
A36: j <= len p;
set l = p.i;
set m = p.j;
i <= len p by A35,A36,XXREAL_0:2;
then i in dom p by A6,A34,A33,FINSEQ_1:1;
then
A39: p.i = Y.i by FUNCT_1:47;
1 <= j by A34,A35,XXREAL_0:2;
then j in dom p by A6,A36,A33,FINSEQ_1:1;
then
A40: p.j = Y.j by FUNCT_1:47;
len Y = k + 1 by Th44;
then j <= len Y by A36,A33,NAT_1:12;
hence l < m by A34,A35,A39,A40,FINSEQ_1:def 14;
end;
hence thesis by A32,FINSEQ_1:def 14;
end;
X = Sgm Seg(k + 1 + n);
then X | Seg(k + 1) = Y by A1;
then Sgm(Seg k) = X | (Seg(k + 1) /\ Seg k) by A2,RELAT_1:71;
hence Sgm(Seg(k + (n + 1))) | Seg k = Sgm(Seg k) by FINSEQ_1:7,NAT_1:12;
end;
Lm4: for k holds Sgm Seg(k + n) | Seg k = Sgm(Seg k)
proof
defpred P[Nat] means for k holds Sgm(Seg(k + $1)) | Seg k = Sgm(
Seg k);
A1: for k st P[k] holds P[k+1] by Lm3;
A2: P[0] by Lm2;
for n holds P[n] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem
Sgm Seg(k + n) | Seg k = Sgm Seg k by Lm4;
Lm5: now
let k be Nat;
assume
A1: Sgm Seg k = idseq k;
A2: len idseq(k + 1) = k + 1 by CARD_1:def 7;
then
A3: len Sgm(Seg(k + 1)) = len idseq(k + 1) by Th44;
then
A4: dom Sgm Seg(k + 1) = Seg(k+1) by A2,FINSEQ_1:def 3;
now
let j be Nat;
assume
A5: j in dom Sgm Seg(k + 1);
then
A6: j in Seg k \/ {k + 1} by A4,FINSEQ_1:9;
now
per cases by A6,XBOOLE_0:def 3;
suppose
A7: j in Seg k;
A8: idseq(k + 1).j = j by A4,A5,FUNCT_1:18;
A9: Sgm(Seg(k + 1)) | Seg k = Sgm(Seg k) by Lm4;
Sgm(Seg k).j = j by A1,A7,FUNCT_1:18;
hence Sgm(Seg(k + 1)).j = idseq(k + 1).j by A7,A8,A9,FUNCT_1:49;
end;
suppose
A10: j in {k + 1};
set Y = Sgm Seg k;
set X = Sgm Seg(k + 1);
A11: j = k + 1 by A10,TARSKI:def 1;
then
A12: j in Seg(k + 1) by FINSEQ_1:4;
now
rng X = Seg(k + 1) by FINSEQ_1:def 14;
then
A13: X.j in Seg(k + 1) by A5,FUNCT_1:def 3;
then reconsider n = X.j as Element of NAT;
assume X.j <> j;
then not X.j in {j} by TARSKI:def 1;
then X.j in Seg(k + 1) \ {k + 1} by A11,A13,XBOOLE_0:def 5;
then
A14: X.j in Seg k by FINSEQ_1:10;
A15: X is one-to-one;
A16: dom X = Seg(k + 1) by A2,A3,FINSEQ_1:def 3;
A17: k < k + 1 by XREAL_1:29;
X | Seg k = Y by Lm4;
then
A18: X.n = Y.n by A14,FUNCT_1:49
.= n by A1,A14,FUNCT_1:18;
n <= k by A14,FINSEQ_1:1;
hence contradiction by A11,A12,A16,A13,A15,A18,A17;
end;
hence Sgm(Seg(k + 1)).j = idseq(k + 1).j by A11,FINSEQ_1:4,FUNCT_1:18;
end;
end;
hence Sgm(Seg(k + 1)).j = idseq(k + 1).j;
end;
hence Sgm Seg(k + 1) = idseq(k + 1) by A3,FINSEQ_2:9;
end;
theorem Th46:
Sgm Seg k = idseq k
proof
defpred P[Nat] means Sgm Seg $1 = idseq $1;
A1: for k being Nat st P[k] holds P[k+1] by Lm5;
A2: P[0] by Th41;
for k being Nat holds P[k] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem Th47:
p | Seg n = p iff len p <= n
proof
thus p | Seg n = p implies len p <= n by FINSEQ_1:86;
assume len p <= n;
then Seg len p c= Seg n by FINSEQ_1:5;
then dom p c= Seg n by FINSEQ_1:def 3;
then
A1: dom p = dom p /\ Seg n by XBOOLE_1:28;
for x being object st x in dom p holds p.x = p.x;
hence thesis by A1,FUNCT_1:46;
end;
theorem Th48:
idseq(n + k) | Seg n = idseq n
proof
A1: Sgm(Seg n) = idseq n by Th46;
Sgm(Seg(n + k)) = idseq(n + k) by Th46;
hence thesis by A1,Lm4;
end;
theorem
idseq n | Seg m = idseq m iff m <= n
proof
thus idseq n | Seg m = idseq m implies m <= n
proof
assume idseq n | Seg m = idseq m;
then len idseq m <= len idseq n by FINSEQ_1:79;
then m <= len idseq n by CARD_1:def 7;
hence thesis by CARD_1:def 7;
end;
assume m <= n;
then ex j being Nat st n = m + j by NAT_1:10;
hence thesis by Th48;
end;
theorem
idseq n | Seg m = idseq n iff n <= m
proof
len idseq n = n by CARD_1:def 7;
hence thesis by Th47;
end;
theorem Th51:
len p = k + l & q = p | Seg k implies len q = k
proof
assume that
A1: len p = k + l and
A2: q = p | Seg k;
k <= len p by A1,NAT_1:12;
hence thesis by A2,FINSEQ_1:17;
end;
theorem
len p = k + l & q = p | Seg k implies dom q = Seg k
proof
assume that
A1: len p = k + l and
A2: q = p | Seg k;
len q = k by A1,A2,Th51;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th53:
len p = k + 1 & q = p | Seg k implies p = q ^ <* p.(k + 1) *>
proof
assume that
A1: len p = k + 1 and
A2: q = p | Seg k;
A3: for l being Nat holds l in dom q implies p.l = q.l
by A2,FUNCT_1:47;
set r = <* p.(k + 1) *>;
A4: now
let l be Nat;
assume l in dom r;
then l in {1} by FINSEQ_1:2,38;
then
A5: l = 1 by TARSKI:def 1;
hence p.(len q + l) = p.(k + 1) by A1,A2,Th51
.= r.l by A5;
end;
len p = len q + 1 by A1,A2,Th51
.= len q + len<* p.(k + 1) *> by FINSEQ_1:39;
hence thesis by A3,A4,Th36;
end;
theorem
p | X is FinSequence iff ex k being Element of NAT st X /\ dom p = Seg k
proof
thus p | X is FinSequence implies
ex k being Element of NAT st X /\ dom p = Seg k
proof
assume p | X is FinSequence;
then consider k being Nat such that
A1: dom(p | X) = Seg k by FINSEQ_1:def 2;
reconsider k as Element of NAT by ORDINAL1:def 12;
take k;
thus thesis by A1,RELAT_1:61;
end;
given k being Element of NAT such that
A2: X /\ dom p = Seg k;
dom(p | X) = Seg k by A2,RELAT_1:61;
hence thesis by FINSEQ_1:def 2;
end;
theorem Th55:
card((p ^ q) " A) = card(p " A) + card(q " A)
proof
set X = (p ^ q) " A;
set B = {len p + n where n is Element of NAT : n in q " A};
defpred P[object,object] means ex i st $1 = i & $2 = len p + i;
A1: X = p " A \/ B
proof
thus X c= p " A \/ B
proof
let x be object;
assume
A2: x in X;
then
A3: x in dom(p ^ q) by FUNCT_1:def 7;
then reconsider k = x as Element of NAT;
now
per cases by A3,FINSEQ_1:25;
suppose
A4: k in dom p;
then (p ^ q).k = p.k by FINSEQ_1:def 7;
then p.k in A by A2,FUNCT_1:def 7;
then k in p " A by A4,FUNCT_1:def 7;
hence thesis by XBOOLE_0:def 3;
end;
suppose
ex m being Nat st m in dom q & k = len p + m;
then consider m being Nat such that
A5: m in dom q and
A6: k = len p + m;
q.m = (p ^ q).k by A5,A6,FINSEQ_1:def 7;
then q.m in A by A2,FUNCT_1:def 7;
then
A7: m in q " A by A5,FUNCT_1:def 7;
m in NAT by ORDINAL1:def 12;
then k in B by A6,A7;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
let x be object;
assume
A8: x in p " A \/ B;
now
per cases by A8,XBOOLE_0:def 3;
suppose
A9: x in p " A;
then
A10: x in dom p by FUNCT_1:def 7;
then reconsider k = x as Element of NAT;
(p ^ q).k = p.k by A10,FINSEQ_1:def 7;
then
A11: (p ^ q).x in A by A9,FUNCT_1:def 7;
x in dom(p ^ q) by A10,Th22;
hence thesis by A11,FUNCT_1:def 7;
end;
suppose
x in B;
then consider n being Element of NAT such that
A12: x = len p + n and
A13: n in q " A;
A14: n in dom q by A13,FUNCT_1:def 7;
then (p ^ q).(len p + n) = q.n by FINSEQ_1:def 7;
then
A15: (p ^ q).x in A by A12,A13,FUNCT_1:def 7;
x in dom(p ^ q) by A12,A14,FINSEQ_1:28;
hence thesis by A15,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
p " A /\ B = {}
proof
set x = the Element of p " A /\ B;
assume
A16: not thesis;
then x in B by XBOOLE_0:def 4;
then consider n being Element of NAT such that
A17: x = len p + n and
A18: n in q " A;
len p + n in p " A by A16,A17,XBOOLE_0:def 4;
then len p + n in dom p by FUNCT_1:def 7;
then len p + n <= len p + 0 by Th25;
then
A19: n = 0 by XREAL_1:6;
n in dom q by A18,FUNCT_1:def 7;
hence thesis by A19,Th24;
end;
then
A20: p " A misses B;
reconsider B as finite set by A1,FINSET_1:1,XBOOLE_1:7;
A21: card X = card(p " A) + card B by A1,A20,CARD_2:40;
A22: for x being object st x in q " A ex y being object st P[x,y]
proof
let x be object;
assume x in q " A;
then x in dom q by FUNCT_1:def 7;
then reconsider i = x as Element of NAT;
reconsider y = len p + i as set;
take y;
take i;
thus thesis;
end;
consider f being Function such that
A23: dom f = q " A and
A24: for x being object st x in q " A holds P[x,f.x] from CLASSES1:sch 1(A22);
A25: rng f = B
proof
thus rng f c= B
proof
let x be object;
assume x in rng f;
then consider y being object such that
A26: y in dom f and
A27: f.y = x by FUNCT_1:def 3;
consider i such that
A28: y = i and
A29: f.y = len p + i by A23,A24,A26;
i is Element of NAT by ORDINAL1:def 12;
hence thesis by A23,A26,A27,A28,A29;
end;
let x be object;
assume x in B;
then consider n being Element of NAT such that
A30: x = len p + n and
A31: n in q " A;
ex i st n = i & f.n = len p + i by A24,A31;
hence thesis by A23,A30,A31,FUNCT_1:def 3;
end;
f is one-to-one
proof
let x,y be object;
assume that
A32: x in dom f and
A33: y in dom f and
A34: f.x = f.y;
A35: ex j st y = j & f.y = len p + j by A23,A24,A33;
ex i st x = i & f.x = len p + i by A23,A24,A32;
hence thesis by A34,A35;
end;
then q " A,B are_equipotent by A23,A25;
hence thesis by A21,CARD_1:5;
end;
theorem Th56:
p " A c= (p ^ q) " A
proof
let x be object;
A1: dom p c= dom(p ^ q) by FINSEQ_1:26;
assume
A2: x in p " A; then
A3: x in dom p by FUNCT_1:def 7;
then reconsider k = x as Element of NAT;
A4: p.k in A by A2,FUNCT_1:def 7;
p.k = (p ^ q).k by A3,FINSEQ_1:def 7;
hence thesis by A3,A1,A4,FUNCT_1:def 7;
end;
definition
let p,A;
func p - A -> FinSequence equals
p * Sgm ((dom p) \ p " A);
coherence
proof
now
assume p <> {};
then reconsider D = Seg len p as non empty Subset of NAT;
rng Sgm(Seg(len p) \ p " A) = Seg(len p) \ p " A by FINSEQ_1:def 14;
then rng Sgm(Seg(len p) \ p " A) c= D by XBOOLE_1:36;
then reconsider q = Sgm(Seg(len p) \ p " A) as FinSequence of D
by FINSEQ_1:def 4;
reconsider r = p * q as FinSequence by FINSEQ_2:30;
take rr = r;
thus rr = p * Sgm((dom p) \ p " A) by FINSEQ_1:def 3;
end;
hence thesis;
end;
end;
theorem Th57:
len(p - A) = len p - card(p " A)
proof
set q = Sgm(Seg(len p) \ p " A);
A1: Seg len p = dom p by FINSEQ_1:def 3;
Seg(len p) \ p " A c= Seg(len p) by XBOOLE_1:36;
then rng q c= dom p by A1,FINSEQ_1:def 14;
then
A2: dom q = dom(p - A) by A1,RELAT_1:27;
A3: dom q = Seg len q by FINSEQ_1:def 3;
A4: p " A c= Seg len p
proof
let x be object;
A5: p " A c= dom p by RELAT_1:132;
A6: dom p = Seg len p by FINSEQ_1:def 3;
assume x in p " A;
hence thesis by A5,A6;
end;
len q = card(Seg(len p) \ p " A) by Th37;
then len(p - A) = card(Seg(len p) \ p " A) by A2,A3,FINSEQ_1:def 3;
hence len(p - A) = card(Seg(len p)) - card(p " A) by A4,CARD_2:44
.= len p - card(p " A) by FINSEQ_1:57;
end;
theorem Th58:
len(p - A) <= len p
proof
len(p - A) = len p - card(p " A) by Th57;
hence thesis by XREAL_1:43;
end;
theorem Th59:
len(p - A) = len p implies A misses rng p
proof
assume
A1: len(p - A) = len p;
A2: len(p - A) = len p - card(p " A) by Th57;
assume A meets rng p;
then p " A <> {} by RELAT_1:138;
hence thesis by A1,A2;
end;
theorem
n = len p - card(p " A) implies dom(p - A) = Seg n
proof
assume n = len p - card(p " A);
then len(p - A) = n by Th57;
hence thesis by FINSEQ_1:def 3;
end;
theorem
dom(p - A) c= dom p
proof
A1: dom(p - A) = Seg len(p - A) by FINSEQ_1:def 3;
A2: dom p = Seg len p by FINSEQ_1:def 3;
len(p - A) <= len p by Th58;
hence thesis by A1,A2,FINSEQ_1:5;
end;
theorem
dom(p - A) = dom p implies A misses rng p
proof
A1: dom(p - A) = Seg len(p - A) by FINSEQ_1:def 3;
A2: dom p = Seg len p by FINSEQ_1:def 3;
assume dom(p - A) = dom p;
hence thesis by A1,A2,Th59,FINSEQ_1:6;
end;
theorem Th63:
rng(p - A) = rng p \ A
proof
set q = Sgm(Seg(len p) \ p " A);
A1: dom p = Seg len p by FINSEQ_1:def 3;
thus rng(p - A) c= rng p \ A
proof
let x be object;
A3: rng(p * q) c= rng p by RELAT_1:26;
assume
A4: x in rng(p - A);
A5: now
assume
A7: x in A;
consider y being object such that
A8: y in dom(p - A) and
A9: (p - A).y = x by A4,FUNCT_1:def 3;
set z = q.y;
A10: y in dom q by A1,A8,FUNCT_1:11;
then
A11: (p - A).y = p.z by A1,FUNCT_1:13;
z in rng q by A10,FUNCT_1:def 3;
then z in Seg(len p) \ p " A by FINSEQ_1:def 14;
then
A12: not z in p " A by XBOOLE_0:def 5;
z in dom p by A1,A8,FUNCT_1:11;
hence contradiction by A7,A9,A11,A12,FUNCT_1:def 7;
end;
x in rng(p * q) by A4,FINSEQ_1:def 3;
hence thesis by A3,A5,XBOOLE_0:def 5;
end;
let x be object;
assume
A13: x in rng p \ A;
then consider y being object such that
A14: y in dom p and
A15: p.y = x by FUNCT_1:def 3;
A16: rng q = Seg(len p) \ p " A by FINSEQ_1:def 14;
not p.y in A by A13,A15,XBOOLE_0:def 5;
then not y in p " A by FUNCT_1:def 7;
then y in rng q by A14,A1,A16,XBOOLE_0:def 5;
then consider z being object such that
A17: z in dom q and
A18: q.z = y by FUNCT_1:def 3;
A19: (p - A).z = x by A1,A15,A17,A18,FUNCT_1:13;
z in dom(p - A) by A1,A14,A17,A18,FUNCT_1:11;
hence thesis by A19,FUNCT_1:def 3;
end;
theorem
rng(p - A) c= rng p
proof
rng(p - A) = rng p \ A by Th63;
hence thesis;
end;
theorem
rng(p - A) = rng p implies A misses rng p
proof
assume rng(p - A) = rng p;
then rng p \ A = rng p by Th63;
hence thesis by XBOOLE_1:83;
end;
theorem Th66:
p - A = {} iff rng p c= A
proof
thus p - A = {} implies rng p c= A
proof
assume that
A1: p - A = {} and
A2: not rng p c= A;
rng p \ A <> {} by A2,XBOOLE_1:37;
then rng(p - A) <> {} by Th63;
hence thesis by A1;
end;
assume
A3: rng p c= A;
rng(p - A) = rng p \ A by Th63;
hence thesis by A3,XBOOLE_1:37;
end;
theorem Th67:
p - A = p iff A misses rng p
proof
thus p - A = p implies A misses rng p
proof
assume that
A1: p - A = p and
A2: not A misses rng p;
len(p - A) <> len p by A2,Th59;
hence contradiction by A1;
end;
assume A misses rng p;
then p " A = {} by RELAT_1:138;
then Sgm(Seg(len p) \ p " A) = idseq(len p) by Th46;
then p * Sgm(Seg(len p) \ p " A) = p by FINSEQ_2:54;
hence thesis by FINSEQ_1:def 3;
end;
theorem
p - {x} = p iff not x in rng p
proof
thus p - {x} = p implies not x in rng p
proof
assume p - {x} = p; then
A1: {x} misses rng p by Th67;
x in {x} by TARSKI:def 1;
hence thesis by A1,XBOOLE_0:3;
end;
assume
A2: not x in rng p;
{x} misses rng p
proof
assume {x} meets rng p;
then ex y being object st y in {x} & y in rng p by XBOOLE_0:3;
hence thesis by A2,TARSKI:def 1;
end;
hence thesis by Th67;
end;
theorem
p - {} = p
proof
{} misses rng p;
hence thesis by Th67;
end;
theorem
p - rng p = {} by Th66;
Lm6: <* x *> - A = <* x *> iff not x in A
proof
thus <* x *> - A = <* x *> implies not x in A
proof
assume <* x *> - A = <* x *>;
then
A1: rng<* x *> misses A by Th67;
A2: rng<* x *> = {x} by FINSEQ_1:39;
x in {x} by TARSKI:def 1;
hence thesis by A2,A1,XBOOLE_0:3;
end;
assume
A3: not x in A;
rng<* x *> misses A
proof
assume rng<* x *> meets A;
then consider y being object such that
A4: y in rng<* x *> and
A5: y in A by XBOOLE_0:3;
y in {x} by A4,FINSEQ_1:39;
hence thesis by A3,A5,TARSKI:def 1;
end;
hence thesis by Th67;
end;
Lm7: <* x *> - A = {} iff x in A
proof
A1: rng<* x *> = {x} by FINSEQ_1:39;
thus <* x *> - A = {} implies x in A
proof
assume <* x *> - A = {};
then rng<* x *> c= A by Th66;
then {x} c= A by FINSEQ_1:39;
hence thesis by ZFMISC_1:31;
end;
assume x in A;
then rng<* x *> c= A by A1,ZFMISC_1:31;
hence thesis by Th66;
end;
Lm8: (p ^ {}) - A = (p - A) ^ ({} - A)
proof
thus (p ^ {}) - A = p - A by FINSEQ_1:34
.= (p - A) ^ ({} - A) by FINSEQ_1:34;
end;
Lm9:
(p ^ <* x *>) - A = (p - A) ^ (<* x *> - A)
proof
set r = (p ^ <* x *>) - A;
set q = <* x *> - A;
set t = p ^ <* x *>;
A1: len t = len p + len<* x *> by FINSEQ_1:22
.= len p + 1 by FINSEQ_1:40;
set S = Seg(len(p ^ <* x *>)) \ (p ^ <* x *>) " A;
set s = Sgm(Seg(len(p ^ <* x *>)) \ (p ^ <* x *>) " A);
A2: now
t " A c= dom t by RELAT_1:132;
then
A3: t " A c= Seg len t by FINSEQ_1:def 3;
let k be Nat;
assume
A5: k in dom q;
then
A6: not x in A by Lm7,RELAT_1:38;
then
A7: q = <* x *> by Lm6;
then
A8: dom q = {1} by FINSEQ_1:2,def 8;
then
A9: k = 1 by A5,TARSKI:def 1;
A10: p " A = (p ^ <* x *>) " A
proof
thus p " A c= (p ^ <* x *>) " A
proof
let y be object;
assume
A11: y in p " A;
then
A12: y in dom p by FUNCT_1:def 7;
then reconsider z = y as Element of NAT;
p.y in A by A11,FUNCT_1:def 7;
then
A13: t.z in A by A12,FINSEQ_1:def 7;
y in dom t by A12,Th22;
hence thesis by A13,FUNCT_1:def 7;
end;
let y be object;
assume
A14: y in (p ^ <* x *>) " A;
then
A15: y in dom t by FUNCT_1:def 7;
then reconsider z = y as Element of NAT;
A16: t.y in A by A14,FUNCT_1:def 7;
A17: now
given n such that
A18: n in dom q and
A19: z = len p + n;
n = 1 by A8,A18,TARSKI:def 1;
hence contradiction by A6,A16,A19,FINSEQ_1:42;
end;
A20: z in dom p or ex n being Nat st n in dom q & z = len p + n
by A7,A15,FINSEQ_1:25;
then t.z = p.z by A17,FINSEQ_1:def 7;
hence thesis by A16,A20,A17,FUNCT_1:def 7;
end;
A21: now
assume
A22: len t in t " A;
t.(len t) = x by A1,FINSEQ_1:42;
hence contradiction by A6,A22,FUNCT_1:def 7;
end;
A23: dom s = Seg len s by FINSEQ_1:def 3;
len t in Seg len t by A1,FINSEQ_1:4;
then len t in S by A21,XBOOLE_0:def 5;
then len t in rng s by FINSEQ_1:def 14;
then consider y being object such that
A24: y in dom s and
A25: s.y = len t by FUNCT_1:def 3;
reconsider y as Element of NAT by A24;
A26: len(p - A) + k = len p - card(p " A) + k by Th57
.= len p + 1 - card((p ^ <* x *>) " A) by A9,A10
.= len p + len<* x *> - card((p ^ <* x *>) " A) by FINSEQ_1:39
.= len(p ^ <* x *>) - card((p ^ <* x *>) " A) by FINSEQ_1:22
.= len r by Th57;
A27: len s = card S by Th37
.= card(Seg(len t)) - card(t " A) by A3,CARD_2:44
.= len t - card(p " A) by A10,FINSEQ_1:57
.= len p - card(p " A) + k by A1,A9
.= len r by A26,Th57;
then
A28: len s = len(p - A) + 1 by A5,A8,A26,TARSKI:def 1;
then
A29: len r in dom s by A27,A23,FINSEQ_1:4;
A30: now
A31: s.(len s) in rng s by A27,A29,FUNCT_1:def 3;
reconsider w = s.(len s) as Element of NAT by A31;
w in S by A31,FINSEQ_1:def 14;
then
A32: w in Seg(len t) by XBOOLE_0:def 5;
assume
A33: y <> len s;
A34: y in Seg(len s) by A24,FINSEQ_1:def 3;
then y <= len s by FINSEQ_1:1;
then
A35: y < len s by A33,XXREAL_0:1;
1 <= y by A34,FINSEQ_1:1;
then len t < w by A25,A35,FINSEQ_1:def 14;
hence contradiction by A32,FINSEQ_1:1;
end;
dom t = Seg len t by FINSEQ_1:def 3;
hence r.(len(p - A) + k) = t.(len t) by A26,A27,A28,A23,A25,A30,FINSEQ_1:4
,FUNCT_1:13
.= x by A1,FINSEQ_1:42
.= q.k by A7,A9;
end;
A36: now
A37: x in A implies t " A = p " A \/ {len p + 1}
proof
assume
A38: x in A;
thus t " A c= p " A \/ {len p + 1}
proof
let y be object;
assume
A39: y in t " A;
then y in dom t by FUNCT_1:def 7;
then y in Seg(len p + 1) by A1,FINSEQ_1:def 3;
then
A40: y in Seg(len p) \/ {len p + 1} by FINSEQ_1:9;
now
per cases by A40,XBOOLE_0:def 3;
suppose
A41: y in Seg(len p);
then reconsider j = y as Element of NAT;
A42: t.y in A by A39,FUNCT_1:def 7;
A43: y in dom p by A41,FINSEQ_1:def 3;
then p.j = t.j by FINSEQ_1:def 7;
then y in p " A by A43,A42,FUNCT_1:def 7;
hence thesis by XBOOLE_0:def 3;
end;
suppose
y in {len p + 1};
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
let y be object;
assume
A44: y in p " A \/ {len p + 1};
now
per cases by A44,XBOOLE_0:def 3;
suppose
A45: y in p " A;
p " A c= t " A by Th56;
hence thesis by A45;
end;
suppose
y in {len p + 1};
then
A46: y = len p + 1 by TARSKI:def 1;
then y in Seg(len t) by A1,FINSEQ_1:4;
then
A47: y in dom t by FINSEQ_1:def 3;
t.y in A by A38,A46,FINSEQ_1:42;
hence thesis by A47,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
t " A c= dom t by RELAT_1:132;
then
A48: t " A c= Seg(len t) by FINSEQ_1:def 3;
A49: not x in A implies t " A = p " A
proof
assume
A50: not x in A;
thus t " A c= p " A
proof
let y be object;
assume
A51: y in t " A;
then
A52: y in dom t by FUNCT_1:def 7;
then reconsider l = y as Element of NAT;
A53: now
assume l = len p + 1;
then t.l = x by FINSEQ_1:42;
hence contradiction by A50,A51,FUNCT_1:def 7;
end;
A54: y in Seg(len t) by A52,FINSEQ_1:def 3;
then l <= len p + 1 by A1,FINSEQ_1:1;
then l < len p + 1 by A53,XXREAL_0:1;
then
A55: l <= len p by NAT_1:13;
1 <= l by A54,FINSEQ_1:1;
then l in Seg(len p) by A55,FINSEQ_1:1;
then
A56: y in dom p by FINSEQ_1:def 3;
t.l in A by A51,FUNCT_1:def 7;
then p.l in A by A56,FINSEQ_1:def 7;
hence thesis by A56,FUNCT_1:def 7;
end;
thus thesis by Th56;
end;
set s2 = Sgm(Seg(len p) \ p " A);
set s1 = Sgm(Seg(len t) \ t " A);
let k be Nat;
A57: dom p = Seg len p by FINSEQ_1:def 3;
A58: now
{len p + 1} /\ p " A = {}
proof
set z = the Element of {len p + 1} /\ p " A;
A59: p " A c= dom p by RELAT_1:132;
assume
A60: not thesis;
then z in {len p + 1} by XBOOLE_0:def 4;
then
A61: z = len p + 1 by TARSKI:def 1;
A62: dom p = Seg(len p) by FINSEQ_1:def 3;
z in p " A by A60,XBOOLE_0:def 4;
then len p + 1 <= len p by A61,A59,A62,FINSEQ_1:1;
hence thesis by XREAL_1:29;
end;
then
A63: {len p + 1} misses p " A;
assume t " A = p " A;
hence Seg(len t) \ t " A = (Seg(len p) \/ {len p + 1}) \ p " A by A1,
FINSEQ_1:9
.= (Seg(len p) \ p " A) \/ ({len p + 1} \ p " A) by XBOOLE_1:42
.= (Seg(len p) \ p " A) \/ {len p + 1} by A63,XBOOLE_1:83;
end;
Seg(len p) /\ {len p + 1} = {}
proof
set z = the Element of Seg(len p) /\ {len p + 1};
assume
A64: not thesis;
then
A65: z in Seg(len p) by XBOOLE_0:def 4;
then reconsider f = z as Element of NAT;
f in {len p + 1} by A64,XBOOLE_0:def 4;
then
A66: f = len p + 1 by TARSKI:def 1;
f <= len p by A65,FINSEQ_1:1;
hence thesis by A66,XREAL_1:29;
end;
then
A67: Seg(len p) misses {len p + 1};
A68: now
assume t " A = p " A \/ {len p + 1};
hence
Seg(len t) \ t " A = (Seg(len p) \/ {len p + 1}) \ (p " A \/ {len p
+ 1}) by A1,FINSEQ_1:9
.= (Seg(len p) \ (p " A \/ {len p + 1}) \/ ({len p + 1} \ (p " A \/
{len p + 1}))) by XBOOLE_1:42
.= (Seg(len p) \ (p " A \/ {len p + 1})) \/ {} by XBOOLE_1:46
.= (Seg(len p) \ p " A) /\ (Seg(len p) \ {len p + 1}) by XBOOLE_1:53
.= (Seg(len p) \ p " A) /\ Seg(len p) by A67,XBOOLE_1:83
.= (Seg(len p) \ p " A) by XBOOLE_1:28,36;
end;
p " A c= dom p by RELAT_1:132;
then
A69: p " A c= Seg(len p) by FINSEQ_1:def 3;
len s2 = card(Seg(len p) \ p " A) by Th37
.= card(Seg(len p)) - card(p " A) by A69,CARD_2:44;
then
A70: len s2 = len p - card(p " A) by FINSEQ_1:57;
rng s1 = Seg(len t) \ t " A by FINSEQ_1:def 14;
then
A71: rng s1 c= Seg len t by XBOOLE_1:36;
rng s2 = Seg(len p) \ p " A by FINSEQ_1:def 14;
then
A73: rng s2 c= Seg(len p) by XBOOLE_1:36;
assume k in dom(p - A);
then
A74: k in dom s2 by A57,FUNCT_1:11;
then s2.k in rng s2 by FUNCT_1:def 3;
then s2.k in Seg len p by A73;
then
A75: s2.k in dom p by FINSEQ_1:def 3;
len s1 = card(Seg(len t) \ t " A) by Th37
.= card(Seg(len t)) - card(t " A) by A48,CARD_2:44;
then
A76: len s1 = len t - card(t " A) by FINSEQ_1:57;
A77: dom s2 c= dom s1
proof
<* x *> " A c= dom<* x *> by RELAT_1:132;
then <* x *> " A c= {1} by FINSEQ_1:2,def 8;
then
A78: <* x *> " A = {} or <* x *> " A = {1} by ZFMISC_1:33;
let y be object;
A79: card(p " A) <= card(p " A) + 1 by NAT_1:12;
assume
A80: y in dom s2;
then reconsider l = y as Element of NAT;
A81: y in Seg(len s2) by A80,FINSEQ_1:def 3;
then l <= len p - card(p " A) by A70,FINSEQ_1:1;
then l + card(p " A) <= len p by XREAL_1:19;
then
A82: l + card(p " A) + 1 <= len t by A1,XREAL_1:7;
card(t " A) = card(p " A) + card(<* x *> " A) by Th55;
then l + card(t " A) <= l + (card(p " A) + 1) by A78,A79,CARD_1:30
,XREAL_1:7;
then l + card(t " A) <= len t by A82,XXREAL_0:2;
then
A83: l <= len s1 by A76,XREAL_1:19;
1 <= l by A81,FINSEQ_1:1;
then l in Seg(len s1) by A83,FINSEQ_1:1;
hence thesis by FINSEQ_1:def 3;
end;
then s1.k in rng s1 by A74,FUNCT_1:def 3;
then s1.k in Seg len t by A71;
then reconsider l = s1.k as Element of NAT;
dom t = Seg len t by FINSEQ_1:def 3;
then
A84: r.k = t.l by A74,A77,FUNCT_1:13;
A86: now
per cases by A37,A49,A58,A68;
suppose
Seg(len p) \ p " A = Seg(len t) \ t " A;
hence s1.k = s2.k;
end;
suppose
A87: Seg(len t) \ t " A = (Seg(len p) \ p " A) \/ {len p + 1};
now
let m,n be Nat;
assume that
A88: m in Seg(len p) \ p " A and
A89: n in {len p + 1};
m in Seg len p by A88,XBOOLE_0:def 5;
then
A90: m <= len p by FINSEQ_1:1;
A91: len p < len p + 1 by XREAL_1:29;
n = len p + 1 by A89,TARSKI:def 1;
hence m < n by A90,A91,XXREAL_0:2;
end;
then s1 = s2 ^ Sgm{len p + 1} by A87,Th40;
hence s1.k = s2.k by A74,FINSEQ_1:def 7;
end;
end;
(p - A).k = p.(s2.k) by A57,A74,FUNCT_1:13;
hence r.k = (p - A).k by A75,A86,A84,FINSEQ_1:def 7;
end;
len r = len(p ^ <* x *>) - card(t " A) by Th57
.= len p + len<* x *> - card(t " A) by FINSEQ_1:22
.= (len p + len<* x *>) - (card(p " A) + card(<* x *> " A)) by Th55
.= len p - card(p " A) + len<* x *> + (- card(<* x *> " A))
.= len(p - A) + len<* x *> + (- card(<* x *> " A)) by Th57
.= len(p - A) + (len<* x *> - card(<* x *> " A))
.= len(p - A) + len q by Th57;
hence thesis by A36,A2,Th36;
end;
Lm10: now
let q be FinSequence, x be object;
assume
A1: for p,A holds (p ^ q) - A = (p - A) ^ (q - A);
let p,A;
thus (p ^ (q ^ <* x *>)) - A = (p ^ q ^ <* x *>) - A by FINSEQ_1:32
.= ((p ^ q) - A) ^ (<* x *> - A) by Lm9
.= (p - A) ^ (q - A) ^ (<* x *> - A) by A1
.= (p - A) ^ ((q - A) ^ (<* x *> - A)) by FINSEQ_1:32
.= (p - A) ^ ((q ^ <* x *>) - A) by Lm9;
end;
Lm11: for q,p,A holds (p ^ q) - A = (p - A) ^ (q - A)
proof
defpred P[FinSequence] means (p ^ $1) - A = (p - A) ^ ($1 - A);
A1: for q being FinSequence, x be object st P[q] holds P[q^<*x*>] by Lm10;
A2: P[{}] by Lm8;
for q holds P[q] from FINSEQ_1:sch 3(A2,A1);
hence thesis;
end;
theorem
(p ^ q) - A = (p - A) ^ (q - A) by Lm11;
theorem
{} - A = {};
theorem
<* x *> - A = <* x *> iff not x in A by Lm6;
theorem
<* x *> - A = {} iff x in A by Lm7;
theorem Th75:
<* x,y *> - A = {} iff x in A & y in A
proof
A1: <* x,y *> = <* x *> ^ <* y *> by FINSEQ_1:def 9;
thus <* x,y *> - A = {} implies x in A & y in A
proof
assume <* x,y *> - A = {};
then rng<* x,y *> c= A by Th66;
then {x,y} c= A by FINSEQ_2:127;
hence thesis by ZFMISC_1:32;
end;
assume that
A2: x in A and
A3: y in A;
A4: <* y *> - A = {} by A3,Lm7;
<* x *> - A = {} by A2,Lm7;
hence <* x,y *> - A = {} ^ {} by A4,A1,Lm11
.= {};
end;
theorem Th76:
x in A & not y in A implies <* x,y *> - A = <* y *>
proof
assume that
A1: x in A and
A2: not y in A;
A3: <* y *> - A = <* y *> by A2,Lm6;
A4: <* x,y *> = <* x *> ^ <* y *> by FINSEQ_1:def 9;
<* x *> - A = {} by A1,Lm7;
hence <* x,y *> - A = {} ^ <* y *> by A3,A4,Lm11
.= <* y *> by FINSEQ_1:34;
end;
theorem
<* x,y *> - A = <* y *> & x <> y implies x in A & not y in A
proof
assume that
A1: <* x,y *> - A = <* y *> and
A2: x <> y;
assume
A3: not thesis;
A4: y in A implies <* y *> - A = {} by Lm7;
A5: not x in A implies <* x *> - A = <* x *> by Lm6;
A6: not y in A implies <* y *> - A = <* y *> by Lm6;
A7: x in A implies <* x *> - A = {} by Lm7;
A8: <* x *>.1 = x;
<* y *> = (<* x *> ^ <* y *>) - A by A1,FINSEQ_1:def 9
.= (<* x *> - A) ^ (<* y *> - A) by Lm11;
then <* y *> = {} or <* x *> = <* y *> or <* y *> = <* x,y *>
by A7,A5,A4,A6,A3,FINSEQ_1:34,def 9;
hence thesis by A2,A8,Th33,FINSEQ_1:40;
end;
theorem Th78:
not x in A & y in A implies <* x,y *> - A = <* x *>
proof
assume that
A1: not x in A and
A2: y in A;
A3: <* y *> - A = {} by A2,Lm7;
A4: <* x,y *> = <* x *> ^ <* y *> by FINSEQ_1:def 9;
<* x *> - A = <* x *> by A1,Lm6;
hence <* x,y *> - A = <* x *> ^ {} by A3,A4,Lm11
.= <* x *> by FINSEQ_1:34;
end;
theorem
<* x,y *> - A = <* x *> & x <> y implies not x in A & y in A
proof
assume that
A1: <* x,y *> - A = <* x *> and
A2: x <> y;
assume
A3: not thesis;
A4: y in A implies <* y *> - A = {} by Lm7;
A5: not x in A implies <* x *> - A = <* x *> by Lm6;
A6: not y in A implies <* y *> - A = <* y *> by Lm6;
A7: x in A implies <* x *> - A = {} by Lm7;
A8: <* x *>.1 = x;
<* x *> = (<* x *> ^ <* y *>) - A by A1,FINSEQ_1:def 9
.= (<* x *> - A) ^ (<* y *> - A) by Lm11;
then <* x *> = {} or <* x *> = <* y *> or <* x *> = <* x,y *> by A7,A5,A4,A6
,A3,FINSEQ_1:34,def 9;
hence thesis by A2,A8,Th33,FINSEQ_1:40;
end;
theorem
<* x,y *> - A = <* x,y *> iff not x in A & not y in A
proof
A1: <* x,y *> = <* x *> ^ <* y *> by FINSEQ_1:def 9;
thus <* x,y *> - A = <* x,y *> implies not x in A & not y in A
proof
assume
A2: <* x,y *> - A = <* x,y *>;
assume not thesis;
then x in A & y in A or not x in A & y in A or x in A & not y in A;
then
<* x,y *> - A = {} or <* x,y *> - A = <* x *> or <* x,y *> - A = <* y
*> by Th75,Th76,Th78;
hence thesis by A2,Th33;
end;
assume that
A3: not x in A and
A4: not y in A;
A5: <* y *> - A = <* y *> by A4,Lm6;
<* x *> - A = <* x *> by A3,Lm6;
hence thesis by A5,A1,Lm11;
end;
theorem Th81:
len p = k + 1 & q = p | Seg k implies (p.(k + 1) in A iff p - A = q - A)
proof
assume that
A1: len p = k + 1 and
A2: q = p | Seg k;
thus p.(k + 1) in A implies p - A = q - A
proof
assume
A3: p.(k + 1) in A;
thus p - A = (q ^ <* p.(k + 1) *>) - A by A1,A2,Th53
.= (q - A) ^ (<* p.(k + 1) *> - A) by Lm11
.= (q - A) ^ {} by A3,Lm7
.= q - A by FINSEQ_1:34;
end;
assume that
A4: p - A = q - A and
A5: not p.(k + 1) in A;
q - A = (q ^ <* p.(k + 1) *>) - A by A1,A2,A4,Th53
.= (q - A) ^ (<* p.(k + 1) *> - A) by Lm11
.= (q - A) ^ <* p.(k + 1) *> by A5,Lm6;
hence thesis by FINSEQ_1:87;
end;
theorem Th82:
len p = k + 1 & q = p | Seg k implies (not p.(k + 1) in A iff p
- A = (q - A) ^ <* p.(k + 1) *>)
proof
assume that
A1: len p = k + 1 and
A2: q = p | Seg k;
thus not p.(k + 1) in A implies p - A = (q - A) ^ <* p.(k + 1) *>
proof
assume
A3: not p.(k + 1) in A;
thus p - A = (q ^ <* p.(k + 1) *>) - A by A1,A2,Th53
.= (q - A) ^ (<* p.(k + 1) *> - A) by Lm11
.= (q - A) ^ <* p.(k + 1) *> by A3,Lm6;
end;
assume
A4: p - A = (q - A) ^ <* p.(k + 1) *>;
assume p.(k + 1) in A;
then q - A = (q - A) ^ <* p.(k + 1) *> by A1,A2,A4,Th81;
hence contradiction by FINSEQ_1:87;
end;
Lm12: for l st (for p,A st len p = l for n st n in dom p for B being finite
set st B = {k where k is Element of NAT : k in dom p & k <= n & p.k in A} holds
p.n in A or (p - A).(n - card B) = p.n) holds for p,A st len p = l + 1 for n st
n in dom p for C being finite set st C = {m where m is Element of NAT : m in
dom p & m <= n & p.m in A} holds p.n in A or (p - A).(n - card C) = p.n
proof
let l;
assume
A1: for p,A st len p = l for n st n in dom p for B being finite set st B
= {k where k is Element of NAT : k in dom p & k <= n & p.k in A} holds p.n in A
or (p - A).(n - card B) = p.n;
let p,A;
reconsider q = p | Seg l as FinSequence by FINSEQ_1:15;
assume
A2: len p = l + 1;
then
A3: len q = l by Th51;
let n;
set B = {k where k is Element of NAT: k in dom q & k <= n & q.k in A};
B c= dom q
proof
let x be object;
assume x in B;
then
ex k being Element of NAT st x = k & k in dom q & k <= n & q.k in A;
hence thesis;
end;
then reconsider B as finite set;
assume
A4: n in dom p;
let C be finite set such that
A5: C = {m where m is Element of NAT: m in dom p & m <= n & p.m in A};
assume
A6: not p.n in A;
now
per cases;
suppose
A7: p.(l + 1) in A;
A8: n in Seg(l + 1) by A2,A4,FINSEQ_1:def 3;
not n in {l + 1} by A6,A7,TARSKI:def 1;
then n in Seg(l + 1) \ {l + 1} by A8,XBOOLE_0:def 5;
then
A9: n in Seg l by FINSEQ_1:10;
A10: B = C
proof
thus B c= C
proof
let x be object;
A11: dom q c= dom p by RELAT_1:60;
assume x in B;
then consider k being Element of NAT such that
A12: x = k and
A13: k in dom q and
A14: k <= n and
A15: q.k in A;
p.k in A by A13,A15,FUNCT_1:47;
hence thesis by A5,A12,A13,A14,A11;
end;
let x be object;
assume x in C;
then consider m being Element of NAT such that
A16: x = m and
A17: m in dom p and
A18: m <= n and
A19: p.m in A by A5;
m in Seg(len p) by A17,FINSEQ_1:def 3;
then
A20: 1 <= m by FINSEQ_1:1;
n <= l by A9,FINSEQ_1:1;
then m <= l by A18,XXREAL_0:2;
then m in Seg l by A20,FINSEQ_1:1;
then
A21: m in dom q by A3,FINSEQ_1:def 3;
then q.m in A by A19,FUNCT_1:47;
hence thesis by A16,A18,A21;
end;
A22: q - A = p - A by A2,A7,Th81;
A23: n in dom q by A3,A9,FINSEQ_1:def 3;
then p.n = q.n by FUNCT_1:47;
hence thesis by A1,A6,A3,A23,A22,A10;
end;
suppose
not p.(l + 1) in A;
then
A24: p - A = (q - A) ^ <* p.(l + 1) *> by A2,Th82;
now
per cases;
suppose
A25: n = l + 1;
p " A = C
proof
thus p " A c= C
proof
let x be object;
assume
A26: x in p " A;
then
A27: x in dom p by FUNCT_1:def 7;
then reconsider z = x as Element of NAT;
A28: p.x in A by A26,FUNCT_1:def 7;
z in Seg n by A2,A25,A27,FINSEQ_1:def 3;
then z <= n by FINSEQ_1:1;
hence thesis by A5,A27,A28;
end;
let x be object;
assume x in C;
then
ex m being Element of NAT st x = m & m in dom p & m <= n & p.
m in A by A5;
hence thesis by FUNCT_1:def 7;
end;
then
A29: len(p - A) = n - card C by A2,A25,Th57;
len<* p.(l + 1) *> = 1 by FINSEQ_1:39;
then (p - A).(n - card C) = (p - A).(len(q - A) + 1) by A24,A29,
FINSEQ_1:22
.= p.(l + 1) by A24,FINSEQ_1:42;
hence thesis by A25;
end;
suppose
n <> l + 1;
then
A30: not n in {l + 1} by TARSKI:def 1;
n in Seg(l + 1) by A2,A4,FINSEQ_1:def 3;
then n in Seg(l + 1) \ {l + 1} by A30,XBOOLE_0:def 5;
then
A31: n in Seg l by FINSEQ_1:10;
then 1 <= n by FINSEQ_1:1;
then n in Seg n by FINSEQ_1:1;
then
A32: {n} c= Seg n by ZFMISC_1:31;
A33: Seg n \ B c= Seg l \ q " A
proof
let x be object;
assume
A34: x in Seg n \ B;
then reconsider z = x as Element of NAT;
A35: x in Seg n by A34,XBOOLE_0:def 5;
then
A36: 1 <= z by FINSEQ_1:1;
A37: z <= n by A35,FINSEQ_1:1;
A38: now
assume
A39: z in q " A;
then
A40: z in dom q by FUNCT_1:def 7;
q.z in A by A39,FUNCT_1:def 7;
then z in B by A37,A40;
hence contradiction by A34,XBOOLE_0:def 5;
end;
n <= l by A31,FINSEQ_1:1;
then z <= l by A37,XXREAL_0:2;
then z in Seg l by A36,FINSEQ_1:1;
hence thesis by A38,XBOOLE_0:def 5;
end;
A41: B = C
proof
thus B c= C
proof
let x be object;
A42: dom q c= dom p by RELAT_1:60;
assume x in B;
then consider k being Element of NAT such that
A43: x = k and
A44: k in dom q and
A45: k <= n and
A46: q.k in A;
p.k in A by A44,A46,FUNCT_1:47;
hence thesis by A5,A43,A44,A45,A42;
end;
let x be object;
assume x in C;
then consider m being Element of NAT such that
A47: x = m and
A48: m in dom p and
A49: m <= n and
A50: p.m in A by A5;
m in Seg(len p) by A48,FINSEQ_1:def 3;
then
A51: 1 <= m by FINSEQ_1:1;
n <= l by A31,FINSEQ_1:1;
then m <= l by A49,XXREAL_0:2;
then m in Seg l by A51,FINSEQ_1:1;
then
A52: m in dom q by A3,FINSEQ_1:def 3;
then q.m in A by A50,FUNCT_1:47;
hence thesis by A47,A49,A52;
end;
q " A c= dom q by RELAT_1:132;
then
A53: q " A c= Seg l by A3,FINSEQ_1:def 3;
q " A \/ (Seg l \ q " A) = q " A \/ Seg l by XBOOLE_1:39
.= Seg l by A53,XBOOLE_1:12;
then card(Seg l) = card(q " A) + card(Seg l \ q " A) by CARD_2:40
,XBOOLE_1:79;
then
A54: len q = card(q " A) + card(Seg(len q) \ q " A) by A3,FINSEQ_1:57;
set b = card B;
set a = n - card B;
A55: card(Seg n) = n by FINSEQ_1:57;
A56: n in dom q by A3,A31,FINSEQ_1:def 3;
then
A57: not q.n in A by A6,FUNCT_1:47;
A58: B c= (Seg n) \ {n}
proof
let x be object;
assume x in B;
then consider k being Element of NAT such that
A59: x = k and
A60: k in dom q and
A61: k <= n and
A62: q.k in A;
k in Seg(len q) by A60,FINSEQ_1:def 3;
then 1 <= k by FINSEQ_1:1;
then
A63: k in Seg n by A61,FINSEQ_1:1;
not k in {n} by A57,A62,TARSKI:def 1;
hence thesis by A59,A63,XBOOLE_0:def 5;
end;
then card B <= card((Seg n) \ {n}) by NAT_1:43;
then card B <= card(Seg n) - card{n} by A32,CARD_2:44;
then b <= card(Seg n) - 1 by CARD_1:30;
then b <= n - 1 by FINSEQ_1:57;
then b + 1 <= n by XREAL_1:19;
then
A64: 0 + b < a + b by NAT_1:13;
then 0 <= a by XREAL_1:6;
then reconsider a as Element of NAT by INT_1:3;
Seg n \ {n} c= Seg n by XBOOLE_1:36;
then a = card(Seg n \ B) by A58,A55,CARD_2:44,XBOOLE_1:1;
then a <= len q - card(q " A) by A3,A54,A33,NAT_1:43;
then
A65: a <= len(q - A) by Th57;
1 <= a by A64,NAT_1:14;
then a in Seg(len(q - A)) by A65,FINSEQ_1:1;
then
A66: a in dom(q - A) by FINSEQ_1:def 3;
p.n = q.n by A56,FUNCT_1:47;
then (q - A).(n - card B) = p.n by A1,A6,A3,A56;
hence thesis by A24,A41,A66,FINSEQ_1:def 7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
Lm13: for l for p,A st len p = l for n st n in dom p holds for B being finite
set st B = {k where k is Element of NAT: k in dom p & k <= n & p.k in A} holds
p.n in A or (p - A).(n - card B) = p.n
proof
defpred P[Nat] means for p,A st len p = $1 for n st n in dom p
holds for B being finite set st B = {k where k is Element of NAT : k in dom p &
k <= n & p.k in A} holds p.n in A or (p - A).(n - card B) = p.n;
A1: P[0]
proof
let p,A;
assume len p = 0;
then p = {};
hence thesis;
end;
A2: for k being Nat st P[k] holds P[k+1] by Lm12;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
n in dom p implies
for B being finite set st
B = {k where k is Element of NAT : k in dom p & k <= n & p.k in A}
holds p.n in A or (p - A).(n - card B) = p.n
proof
len p = len p;
hence thesis by Lm13;
end;
theorem
p is FinSequence of D implies p - A is FinSequence of D
proof
assume p is FinSequence of D;
then
A1: rng p c= D by FINSEQ_1:def 4;
rng(p - A) = rng p \ A by Th63;
then rng(p - A) c= D by A1;
hence thesis by FINSEQ_1:def 4;
end;
theorem
p is one-to-one implies p - A is one-to-one;
theorem Th86:
p is one-to-one implies len(p - A) = len p - card(A /\ rng p)
proof
A1: p " A c= dom p by RELAT_1:132;
assume
A2: p is one-to-one;
p " A,A /\ rng p are_equipotent
proof
deffunc F(object) = p.$1;
consider f being Function such that
A3: dom f = p " A and
A4: for x being object st x in p " A holds f.x = F(x) from FUNCT_1:sch 3;
take f;
thus f is one-to-one
proof
let x,y be object;
assume that
A5: x in dom f and
A6: y in dom f and
A7: f.x = f.y;
A8: f.y = p.y by A3,A4,A6;
p.x = f.x by A3,A4,A5;
hence thesis by A2,A1,A3,A5,A6,A7,A8;
end;
thus dom f = p " A by A3;
thus rng f c= A /\ rng p
proof
let x be object;
assume x in rng f;
then consider y being object such that
A9: y in dom f and
A10: f.y = x by FUNCT_1:def 3;
A11: p.y in A by A3,A9,FUNCT_1:def 7;
y in dom p by A3,A9,FUNCT_1:def 7;
then
A12: p.y in rng p by FUNCT_1:def 3;
p.y = f.y by A3,A4,A9;
hence thesis by A10,A11,A12,XBOOLE_0:def 4;
end;
let x be object;
assume
A13: x in A /\ rng p;
then x in rng p by XBOOLE_0:def 4;
then consider y being object such that
A14: y in dom p and
A15: p.y = x by FUNCT_1:def 3;
p.y in A by A13,A15,XBOOLE_0:def 4;
then
A16: y in p " A by A14,FUNCT_1:def 7;
then f.y = x by A4,A15;
hence thesis by A3,A16,FUNCT_1:def 3;
end;
then card(p " A) = card(A /\ rng p) by CARD_1:5;
hence thesis by Th57;
end;
theorem Th87:
for A being finite set st p is one-to-one & A c= rng p holds
len (p - A) = len p - card A
proof
let A be finite set;
assume that
A1: p is one-to-one and
A2: A c= rng p;
A /\ rng p = A by A2,XBOOLE_1:28;
hence thesis by A1,Th86;
end;
theorem
p is one-to-one & x in rng p implies len(p - {x}) = len p - 1
proof
assume that
A1: p is one-to-one and
A2: x in rng p;
{x} c= rng p by A2,ZFMISC_1:31;
then len(p - {x}) = len p - card{x} by A1,Th87;
hence thesis by CARD_1:30;
end;
theorem Th89:
rng p misses rng q & p is one-to-one & q is one-to-one iff
p ^ q is one-to-one
proof
thus rng p misses rng q & p is one-to-one & q is one-to-one implies
p ^ q is one-to-one
proof
assume that
A1: rng p misses rng q and
A2: p is one-to-one and
A3: q is one-to-one;
let x,y be object;
assume that
A4: x in dom(p ^ q) and
A5: y in dom(p ^ q) and
A6: (p ^ q).x = (p ^ q).y;
reconsider k1 = x, k2 = y as Element of NAT by A4,A5;
now
per cases by A4,A5,FINSEQ_1:25;
suppose
A7: k1 in dom p & k2 in dom p;
then
A8: (p ^ q).k2 = p.k2 by FINSEQ_1:def 7;
(p ^ q).k1 = p.k1 by A7,FINSEQ_1:def 7;
hence thesis by A2,A6,A7,A8;
end;
suppose
A9: k1 in dom p & ex n being Nat st n in dom q & k2 = len p + n;
then consider n being Nat such that
A10: n in dom q and
A11: k2 = len p + n;
A12: q.n in rng q by A10,FUNCT_1:def 3;
A13: (p ^ q).k1 = p.k1 by A9,FINSEQ_1:def 7;
(p ^ q).k2 = q.n by A9,A11,FINSEQ_1:def 7;
then q.n in rng p by A6,A9,A13,FUNCT_1:def 3;
hence thesis by A1,A12,XBOOLE_0:3;
end;
suppose
A14: k2 in dom p & ex n being Nat st n in dom q & k1 = len p + n;
then consider n being Nat such that
A15: n in dom q and
A16: k1 = len p + n;
A17: q.n in rng q by A15,FUNCT_1:def 3;
A18: (p ^ q).k2 = p.k2 by A14,FINSEQ_1:def 7;
(p ^ q).k1 = q.n by A14,A16,FINSEQ_1:def 7;
then q.n in rng p by A6,A14,A18,FUNCT_1:def 3;
hence thesis by A1,A17,XBOOLE_0:3;
end;
suppose
A19: (ex n being Nat st n in dom q & k1 = len p + n) & ex n being
Nat st n in dom q & k2 = len p + n;
then consider n2 being Nat such that
A20: n2 in dom q and
A21: k2 = len p + n2;
A22: (p ^ q).k2 = q.n2 by A20,A21,FINSEQ_1:def 7;
consider n1 being Nat such that
A23: n1 in dom q and
A24: k1 = len p + n1 by A19;
(p ^ q).k1 = q.n1 by A23,A24,FINSEQ_1:def 7;
hence thesis by A3,A6,A23,A24,A20,A21,A22;
end;
end;
hence thesis;
end;
assume
A25: p ^ q is one-to-one;
thus rng p misses rng q
proof
assume not rng p misses rng q;
then consider x being object such that
A26: x in rng p and
A27: x in rng q by XBOOLE_0:3;
consider y1 being object such that
A28: y1 in dom p and
A29: p.y1 = x by A26,FUNCT_1:def 3;
A30: y1 in Seg(len p) by A28,FINSEQ_1:def 3;
consider y2 being object such that
A31: y2 in dom q and
A32: q.y2 = x by A27,FUNCT_1:def 3;
A33: y2 in Seg len q by A31,FINSEQ_1:def 3;
reconsider y1,y2 as Element of NAT by A28,A31;
A34: len p + y2 in dom(p ^ q) by A31,FINSEQ_1:28;
A35: (p ^ q).y1 = p.y1 by A28,FINSEQ_1:def 7;
A36: (p ^ q).(len p + y2) = q.y2 by A31,FINSEQ_1:def 7;
y1 in dom(p ^ q) by A28,Th22;
then
A37: y1 = len p + y2 by A25,A29,A32,A34,A35,A36;
A38: y1 = y1 + 0;
A39: len p <= len p + y2 by NAT_1:12;
y1 <= len p by A30,FINSEQ_1:1;
then y1 = len p by A37,A39,XXREAL_0:1;
hence thesis by A33,A37,A38,FINSEQ_1:1;
end;
thus p is one-to-one
proof
let x,y be object;
assume that
A40: x in dom p and
A41: y in dom p and
A42: p.x = p.y;
reconsider k = x, l = y as Element of NAT by A40,A41;
A43: (p ^ q).k = p.k by A40,FINSEQ_1:def 7;
A44: (p ^ q).l = p.l by A41,FINSEQ_1:def 7;
A45: l in dom(p ^q) by A41,Th22;
k in dom(p ^ q) by A40,Th22;
hence thesis by A25,A42,A43,A44,A45;
end;
let x,y be object;
assume that
A46: x in dom q and
A47: y in dom q and
A48: q.x = q.y;
consider l being Nat such that
A49: y = l and
A50: len p + l in dom(p ^ q) by A47,FINSEQ_1:27;
A51: (p ^ q).(len p + l) = q.l by A47,A49,FINSEQ_1:def 7;
consider k being Nat such that
A52: x = k and
A53: len p + k in dom(p ^ q) by A46,FINSEQ_1:27;
(p ^ q).(len p + k) = q.k by A46,A52,FINSEQ_1:def 7;
then len p + k = len p + l by A25,A48,A52,A53,A49,A50,A51;
hence thesis by A52,A49;
end;
theorem
A is included_in_Seg implies Sgm A is one-to-one;
theorem Th91:
<* x *> is one-to-one
proof
let y1,y2 be object;
assume that
A1: y1 in dom<* x *> and
A2: y2 in dom<* x *> and
<* x *>.y1 = <* x *>.y2;
y1 in {1} by A1,FINSEQ_1:2,def 8;
then
A3: y1 = 1 by TARSKI:def 1;
y2 in {1} by A2,FINSEQ_1:2,def 8;
hence thesis by A3,TARSKI:def 1;
end;
theorem Th92:
x <> y iff <* x,y *> is one-to-one
proof
A1: <* x,y *>.2 = y;
2 in {1,2} by TARSKI:def 2;
then
A2: 2 in dom<* x,y *> by FINSEQ_1:2,89;
thus x <> y implies <* x,y *> is one-to-one
proof
assume
A3: x <> y;
let y1,y2 be object;
assume that
A4: y1 in dom<* x,y *> and
A5: y2 in dom<* x,y *> and
A6: <* x,y *>.y1 = <* x,y *>.y2;
A7: y2 in {1,2} by A5,FINSEQ_1:2,89;
A8: y1 in {1,2} by A4,FINSEQ_1:2,89;
now
per cases by A8,A7,TARSKI:def 2;
suppose
y1 = 1 & y2 = 1 or y1 = 2 & y2 = 2;
hence thesis;
end;
suppose
A9: y1 = 1 & y2 = 2;
thus thesis by A3,A6,A9;
end;
suppose
A10: y1 = 2 & y2 = 1;
thus thesis by A3,A6,A10;
end;
end;
hence thesis;
end;
assume that
A11: <* x,y *> is one-to-one and
A12: x = y;
1 in {1,2} by TARSKI:def 2;
then
A13: 1 in dom<* x,y *> by FINSEQ_1:2,89;
<* x,y *>.1 = x;
hence thesis by A11,A12,A13,A2,A1;
end;
theorem Th93:
x <> y & y <> z & z <> x iff <* x,y,z *> is one-to-one
proof
set p = <* x,y,z *>;
A1: p.1 = x;
A2: p.3 = z;
thus x <> y & y <> z & z <> x implies <* x,y,z *> is one-to-one
proof
assume that
A3: x <> y and
A4: y <> z and
A5: z <> x;
{x,y} /\ {z} = {}
proof
set y1 = the Element of {x,y} /\ {z};
assume
A6: not thesis;
then y1 in {x,y} by XBOOLE_0:def 4;
then
A7: y1 = x or y1 = y by TARSKI:def 2;
y1 in {z} by A6,XBOOLE_0:def 4;
hence thesis by A4,A5,A7,TARSKI:def 1;
end;
then {} = rng<* x,y *> /\ {z} by FINSEQ_2:127
.= rng<* x,y *> /\ rng<* z *> by FINSEQ_1:38;
then
A8: rng<* x,y *> misses rng<* z *>;
A9: <* z *> is one-to-one by Th91;
<* x,y *> is one-to-one by A3,Th92;
then <* x,y *> ^ <* z *> is one-to-one by A8,A9,Th89;
hence thesis by FINSEQ_1:43;
end;
A10: p.2 = y;
1 in {1,2,3} by ENUMSET1:def 1;
then
A11: 1 in dom p by Th1,FINSEQ_1:89;
3 in {1,2,3} by ENUMSET1:def 1;
then
A12: 3 in dom p by Th1,FINSEQ_1:89;
2 in {1,2,3} by ENUMSET1:def 1;
then
A13: 2 in dom p by Th1,FINSEQ_1:89;
assume <* x,y,z *> is one-to-one;
hence thesis by A11,A13,A12,A1,A10,A2;
end;
theorem Th94:
p is one-to-one & rng p = {x} implies len p = 1
proof
assume that
A1: p is one-to-one and
A2: rng p = {x};
A3: now
given y1,y2 such that
A4: y1 in dom p and
A5: y2 in dom p and
A6: y1 <> y2;
p.y2 in rng p by A5,FUNCT_1:def 3;
then
A7: p.y2 = x by A2,TARSKI:def 1;
p.y1 in rng p by A4,FUNCT_1:def 3;
then p.y1 = x by A2,TARSKI:def 1;
hence contradiction by A1,A4,A5,A6,A7;
end;
set y = the Element of dom p;
A8: dom p <> {} by A2,RELAT_1:42;
A9: dom p = {y}
proof
thus dom p c= {y}
proof
let x be object;
assume x in dom p;
then x = y by A3;
hence thesis by TARSKI:def 1;
end;
let x be object;
y in dom p by A8;
hence thesis by TARSKI:def 1;
end;
dom p = Seg(len p) by FINSEQ_1:def 3;
hence thesis by A9,Th20;
end;
theorem
p is one-to-one & rng p = {x} implies p = <* x *>
proof
assume that
A1: p is one-to-one and
A2: rng p = {x};
len p = 1 by A1,A2,Th94;
hence thesis by A2,FINSEQ_1:39;
end;
theorem Th96:
p is one-to-one & rng p = {x,y} & x <> y implies len p = 2
proof
assume that
A1: p is one-to-one and
A2: rng p = {x,y} and
A3: x <> y;
set q = <* x,y *>;
A4: rng q = {x,y} by FINSEQ_2:127;
A5: len q = 2 by FINSEQ_1:44;
q is one-to-one by A3,Th92;
hence thesis by A1,A2,A4,A5,FINSEQ_1:48;
end;
theorem
p is one-to-one & rng p = {x,y} & x <> y implies
p = <* x,y *> or p = <* y,x *>
proof
assume that
A1: p is one-to-one and
A2: rng p = {x,y} and
A3: x <> y;
A4: len p = 2 by A1,A2,A3,Th96;
then
A5: dom p = {1,2} by FINSEQ_1:2,def 3;
then
A6: 2 in dom p by TARSKI:def 2;
then
A7: p.2 in rng p by FUNCT_1:def 3;
A8: 1 in dom p by A5,TARSKI:def 2;
then p.1 in rng p by FUNCT_1:def 3;
then p.1 = x & p.2 = x or p.1 = x & p.2 = y or p.1 = y & p.2 = x or p.1 = y
& p.2 = y by A2,A7,TARSKI:def 2;
hence thesis by A1,A4,A8,A6,FINSEQ_1:44;
end;
theorem Th98:
p is one-to-one & rng p = {x,y,z} & <* x,y,z *> is one-to-one
implies len p = 3
proof
A1: len <* x,y,z *> = 3 by FINSEQ_1:45;
rng <* x,y,z *> = {x,y,z} by FINSEQ_2:128;
hence thesis by A1,FINSEQ_1:48;
end;
theorem
p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & x <> z implies
len p = 3
proof
assume that
A1: p is one-to-one and
A2: rng p = {x,y,z} and
A3: x <> y and
A4: y <> z and
A5: x <> z;
<* x,y,z *> is one-to-one by A3,A4,A5,Th93;
hence thesis by A1,A2,Th98;
end;
begin :: Addenda
:: from FSM_1
theorem
for D being non empty set, df being FinSequence of D holds
df is non empty implies
ex d being Element of D, df1 being FinSequence of D st
d = df.1 & df = <*d*>^df1
proof
let D be non empty set, df be FinSequence of D;
deffunc F(Nat) = df.($1+1);
assume
A1: df is non empty;
then reconsider lend1 = len df - 1 as Element of NAT by INT_1:5,NAT_1:14;
1 <= len df by A1,NAT_1:14;
then 1 in dom df by Th25;
then reconsider d = df.1 as Element of D by FINSEQ_2:11;
take d;
consider dta being FinSequence such that
A2: len dta = lend1 and
A3: for j being Nat st j in dom dta holds dta.j=F(j) from FINSEQ_1:sch 2;
now
let j be Nat;
assume
A4: j in dom dta;
then j in Seg len dta by FINSEQ_1:def 3;
then j + 1 in Seg (len dta + 1) by FINSEQ_1:60;
then j+1 in dom df by A2,FINSEQ_1:def 3;
then df.(j+1) in D by FINSEQ_2:11;
hence dta.j in D by A3,A4;
end;
then reconsider dta as FinSequence of D by FINSEQ_2:12;
take dta;
thus d = df.1;
now
thus
A5: len (<*d*>^dta) = len <*d*> + len dta by FINSEQ_1:22
.= 1 + (len df - 1) by A2,FINSEQ_1:40
.= len df;
let i be Nat;
A6: dom df = Seg len df by FINSEQ_1:def 3;
assume
A7: i in dom df;
then
A8: 1 <= i by A6,FINSEQ_1:1;
A9: i <= len df by A6,A7,FINSEQ_1:1;
per cases by A8,XXREAL_0:1;
suppose
i = 1;
hence df.i = (<*d*>^dta).i by FINSEQ_1:41;
end;
suppose
A10: i > 1;
then consider j being Element of NAT such that
A11: j = i-1 and
A12: 1 <= j by INT_1:51;
i - 1 <= lend1 by A9,XREAL_1:9;
then
A13: j in dom dta by A2,A11,A12,Th25;
len <*d*> = 1 by FINSEQ_1:40;
then (<*d*>^dta).i = dta.j by A5,A9,A10,A11,FINSEQ_1:24
.= df.(j+1) by A3,A13
.= df.i by A11;
hence df.i = (<*d*>^dta).i;
end;
end;
hence thesis by FINSEQ_2:9;
end;
theorem
for df being FinSequence, d being object holds
i in dom df implies (<*d*>^df).(i+1) = df.i
proof
let df be FinSequence, d be object;
A1: len (<*d*>^df) = len <*d*> + len df by FINSEQ_1:22
.= 1 + len df by FINSEQ_1:40;
assume
A2: i in dom df;
then i in Seg len df by FINSEQ_1:def 3;
then i+1 in Seg len (<*d*>^df) by A1,FINSEQ_1:60;
then i+1 in dom (<*d*>^df) by FINSEQ_1:def 3;
then
A3: i+1 <= len (<*d*>^df) by Th25;
A4: len <*d*> = 1 by FINSEQ_1:40;
1 <= i by A2,Th25;
then 1 < i+1 by NAT_1:13;
hence (<*d*>^df).(i+1) = df.(i + 1 - len <*d*>) by A4,A3,FINSEQ_1:24
.= df.i by A4;
end;
:: from MATRIX_2, 2005.11.16, A.T.
definition
let i be natural Number;
let p be FinSequence;
func Del(p,i) -> FinSequence equals
p * Sgm ((dom p) \ {i});
coherence
proof
set q = Sgm((dom p) \ {i});
rng q = (dom p) \ {i} by FINSEQ_1:def 14;
then rng q c= dom p by XBOOLE_1:36;
then
A2: dom (p*q) = dom q by RELAT_1:27;
dom q = Seg len q by FINSEQ_1:def 3;
hence thesis by A2,FINSEQ_1:def 2;
end;
end;
theorem Th102:
for p being FinSequence holds
(i in dom p implies ex m being Nat st len p = m + 1 & len Del(p,i) = m) &
(not i in dom p implies Del(p,i) = p)
proof
let p be FinSequence;
hereby
not i in (Seg(len p) \ {i})
proof
assume i in (Seg(len p) \ {i});
then not i in {i} by XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
then
A1: card ((Seg(len p) \ {i}) \/ {i})=card (Seg(len p) \ {i}) +1 by CARD_2:41;
assume
A2: i in dom p;
then reconsider D9 = dom p as non empty set;
reconsider D = rng p as non empty set by A2,FUNCT_1:3;
reconsider r = p as Function of D9,D by FUNCT_2:1;
A3: dom p = Seg len p by FINSEQ_1:def 3;
rng Sgm(Seg(len p) \ {i}) = Seg(len p) \ {i} by FINSEQ_1:def 14;
then rng Sgm(Seg(len p) \ {i}) c= Seg len p by XBOOLE_1:36;
then reconsider q = Sgm((dom p) \ {i}) as FinSequence of D9
by A3,FINSEQ_1:def 4;
p <> {} by A2;
then consider m being Nat such that
A5: len p = m+1 by NAT_1:6;
take m;
A6: len(r*q) = len q by FINSEQ_2:33;
i in Seg len p by A2,FINSEQ_1:def 3;
then for x being object
holds x in {i} implies x in Seg(len p) by TARSKI:def 1;
then {i} c= Seg len p;
then card Seg(len p)=card (Seg(len p) \ {i}) +1 by A1,XBOOLE_1:45;
then card (Seg(len p) \ {i}) +1 = m+1 by A5,FINSEQ_1:57;
then len (Sgm(Seg(len p) \ {i}))=m by Th37;
hence len p=m + 1 & len Del(p,i) = m by A5,A6,FINSEQ_1:def 3;
end;
assume not i in dom p;
then for x being object st x in {i} holds not x in dom p by TARSKI:def 1;
then {i} misses dom p by XBOOLE_0:3;
hence Del(p,i) = p * Sgm(dom p) by XBOOLE_1:83
.= p * Sgm(Seg len p) by FINSEQ_1:def 3
.= p * (idseq len p) by Th46
.= p|(Seg len p) by RELAT_1:65
.= p|(dom p) by FINSEQ_1:def 3
.= p;
end;
theorem
for D being non empty set for p being FinSequence of D holds
Del(p,i) is FinSequence of D
proof
let D be non empty set, p be FinSequence of D;
per cases;
suppose
i in dom p;
then reconsider D9=Seg(len p) as non empty set by FINSEQ_1:def 3;
for x being object holds x in (Seg(len p) \ {i}) implies x in Seg(len p)
by XBOOLE_0:def 5;
then Seg(len p) \ {i} c= Seg(len p);
then rng Sgm(Seg(len p) \ {i}) c= Seg(len p) by FINSEQ_1:def 14;
then reconsider q=Sgm(Seg(len p) \ {i}) as FinSequence of D9
by FINSEQ_1:def 4;
p * q = Del(p,i) by FINSEQ_1:def 3;
hence thesis by FINSEQ_2:31;
end;
suppose
not i in dom p;
hence thesis by Th102;
end;
end;
:: from MATRLIN, 2005.11.16, A.T.
theorem
for p be FinSequence holds rng Del(p,i) c= rng p by FUNCT_1:14;
:: from GOBOARD1, 2005.11.16, A.T.
theorem Th105:
n = m + 1 & i in Seg n implies len Sgm(Seg n \ {i}) = m
proof
assume that
A1: n = m + 1 and
A2: i in Seg n;
set X = Seg n \ {i};
i in {i} by TARSKI:def 1;
then not i in X by XBOOLE_0:def 5;
then card X + 1 = card (X \/ {i}) by CARD_2:41
.= card ((Seg n) \/ {i}) by XBOOLE_1:39
.= card (Seg n) by A2,ZFMISC_1:40
.= m + 1 by A1,FINSEQ_1:57;
hence thesis by Th37;
end;
reserve J for Nat;
theorem Th106:
for i,k,m,n being Nat st n=m+1 & k in Seg n & i in Seg m holds
(1<=i & i<k implies Sgm(Seg n \ {k}).i = i) &
(k<=i & i<=m implies Sgm(Seg n \ {k}).i = i+1)
proof
defpred P[Nat] means for n,k,i being Nat st n = $1 + 1
& k in Seg n & i in Seg $1 holds (1<=i & i<k implies Sgm(Seg n \ {k}).i = i) &
(k<=i & i<=$1implies Sgm(Seg n \ {k}).i = i+1);
let i,k,m,n be Nat;
assume that
A1: n = m + 1 and
A2: k in Seg n and
A3: i in Seg m;
A4: for k being Nat st P[k] holds P[k+1]
proof
let k being Nat such that
A5: P[k];
let g,i,n be Nat;
assume that
A6: g = k+1 + 1 and
A7: i in Seg g and
A8: n in Seg(k+1);
A9: 1<=i by A7,FINSEQ_1:1;
set X = Seg g \ {i};
A10: len Sgm(X)=k+1 by A6,A7,Th105;
A11: 1<=n by A8,FINSEQ_1:1;
A12: i<=g by A7,FINSEQ_1:1;
A13: X c= Seg g by XBOOLE_1:36;
A14: rng Sgm(X) = X by FINSEQ_1:def 14;
A15: n<=k+1 by A8,FINSEQ_1:1;
now
per cases;
suppose
A16: i=g; then
A17: k+1<i by A6,NAT_1:13;
X = Seg(k+1)
proof
thus X c= Seg(k+1)
proof
let x be object;
A18: Seg g = {J: 1<=J & J<= g} by FINSEQ_1:def 1;
assume
A19: x in X;
then x in Seg g by XBOOLE_0:def 5;
then consider J such that
A20: x=J and
A21: 1<=J and
A22: J<=g by A18;
not x in {i} by A19,XBOOLE_0:def 5;
then x<>i by TARSKI:def 1;
then J<g by A16,A20,A22,XXREAL_0:1;
then J<=k+1 by A6,NAT_1:13;
hence thesis by A20,A21,FINSEQ_1:1;
end;
let x be object;
assume x in Seg(k+1);
then x in {J: 1<=J & J<=k+1} by FINSEQ_1:def 1;
then consider J such that
A23: x=J and
A24: 1<=J and
A25: J<=k+1;
k+1<=g by A6,NAT_1:11;
then J<=g by A25,XXREAL_0:2;
then
A26: J in Seg g by A24,FINSEQ_1:1;
not J in {i} by A17,A25,TARSKI:def 1;
hence thesis by A23,A26,XBOOLE_0:def 5;
end;
then Sgm X = idseq (k+1) by Th46;
hence 1<=n & n<i implies Sgm(X).n = n by A8,FUNCT_1:17;
thus i<=n & n<=k+1 implies Sgm(Seg g \ {i}).n = n+1 by A6,A16,NAT_1:13;
end;
suppose
A27: i<>g;
set A = {l where l is Nat : 1<=l & l<=g & l<>i};
A28: X = A
proof
thus X c= A
proof
let x be object;
A29: Seg g= {J: 1<=J & J<=g } by FINSEQ_1:def 1;
assume
A30: x in X;
then x in Seg g by XBOOLE_0:def 5;
then consider m being Nat such that
A31: x=m and
A32: 1<=m and
A33: m<=g by A29;
not x in {i} by A30,XBOOLE_0:def 5;
then m<>i by A31,TARSKI:def 1;
hence thesis by A31,A32,A33;
end;
let x be object;
assume x in A;
then consider m being Nat such that
A34: x=m and
A35: 1<=m and
A36: m<=g and
A37: m<>i;
A38: not m in {i} by A37,TARSKI:def 1;
m in Seg g by A35,A36,FINSEQ_1:1;
hence thesis by A34,A38,XBOOLE_0:def 5;
end;
1<=k+1 by A11,A15,XXREAL_0:2;
then k+1 in dom Sgm(X) by A10,Th25;
then Sgm(X).(k+1) in X by A14,FUNCT_1:def 3;
then
A39: ex J st Sgm(X).(k+1) = J & 1<=J & J<=g & J<>i by A28;
1<=g by A9,A12,XXREAL_0:2;
then g in rng Sgm(X) by A14,A27,A28;
then consider x be Nat such that
A40: x in dom Sgm(X) and
A41: Sgm(X).x=g by FINSEQ_2:10;
1<=x by A40,Th25;
then
A42: k+1<=x by A10,A39,A41,FINSEQ_1:def 14;
A43: i<g by A12,A27,XXREAL_0:1;
then
A44: i<=k+1 by A6,NAT_1:13;
A45: x<=k+1 by A10,A40,Th25;
now
per cases by A15,XXREAL_0:1;
suppose
A46: n=k+1;
hence 1<=n & n<i implies Sgm(X).n = n by A6,A43,NAT_1:13;
thus i<=n & n<=k+1 implies Sgm(Seg g \ {i}).n=n+1 by A6,A41,A45,A42
,A46,XXREAL_0:1;
end;
suppose
A47: n<k+1;
set Y = Seg(k+1) \ {i};
A48: now
let j1,j be Nat;
assume that
A49: j1 in Y and
A50: j in {g};
j1 in Seg(k+1) by A49,XBOOLE_0:def 5;
then
A51: j1<=k+1 by FINSEQ_1:1;
j=g by A50,TARSKI:def 1;
hence j1<j by A6,A51,NAT_1:13;
end;
A52: X = Y \/ {g}
proof
thus X c= Y \/ {g}
proof
let x be object;
assume x in X;
then consider J such that
A53: x=J and
A54: 1<=J and
A55: J<=g and
A56: J<>i by A28;
now
per cases by A55,XXREAL_0:1;
suppose
J=g;
then x in {g} by A53,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
J<g;
then J<=k+1 by A6,NAT_1:13;
then
A57: J in Seg(k+1) by A54,FINSEQ_1:1;
not J in {i} by A56,TARSKI:def 1;
then x in Y by A53,A57,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
let x be object such that
A58: x in Y \/ {g};
now
per cases by A58,XBOOLE_0:def 3;
suppose
A59: x in Y;
A60: Seg(k+1)={ s where s is Nat :1<=s & s<=k+1}
by FINSEQ_1:def 1;
x in Seg(k+1) by A59,XBOOLE_0:def 5;
then consider s be Nat such that
A61: x=s and
A62: 1<=s and
A63: s<=k+1 by A60;
not x in {i} by A59,XBOOLE_0:def 5;
then
A64: s<>i by A61,TARSKI:def 1;
k+1<=g by A6,NAT_1:11;
then s<=g by A63,XXREAL_0:2;
hence thesis by A28,A61,A62,A64;
end;
suppose
x in {g};
then
A65: x=g by TARSKI:def 1;
1<=g by A9,A12,XXREAL_0:2;
hence thesis by A27,A28,A65;
end;
end;
hence thesis;
end;
then {g} c= X by XBOOLE_1:7;
then {g} c= Seg g by A13;
then
{g} is included_in_Seg by FINSEQ_1:def 13;
then
A67: Sgm(X) = Sgm(Y)^Sgm({g}) by A52,A48,Th40;
n<=k by A47,NAT_1:13;
then
A68: n in Seg k by A11,FINSEQ_1:1;
A69: i in Seg(k+1) by A9,A44,FINSEQ_1:1;
then len Sgm(Y) = k by Th105;
then
A70: n in dom Sgm(Y) by A68,FINSEQ_1:def 3;
n<=k by A47,NAT_1:13;
then
A71: n in Seg k by A11,FINSEQ_1:1;
then
A72: 1<=n & n<i implies Sgm(Seg(k+1) \ {i}).n = n by A5,A69;
now
assume that
A73: 1<=n and
A74: n<i;
n in Seg len Sgm(Y) by A71,A69,Th105;
then n in dom Sgm(Y) by FINSEQ_1:def 3;
hence Sgm(X).n = n by A72,A67,A73,A74,FINSEQ_1:def 7;
end;
hence 1<=n & n<i implies Sgm(X).n = n;
assume that
A75: i<=n and
n<=k+1;
i<=n & n<=k implies Sgm(Seg(k+1) \ {i}).n = n+1 by A5,A71,A69;
hence Sgm(X).n = n+1 by A47,A67,A75,A70,FINSEQ_1:def 7,NAT_1:13;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A76: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A76,A4);
hence thesis by A1,A2,A3;
end;
theorem Th107:
for f being FinSequence st len f = m+1 & n in dom f holds len Del(f,n) = m
proof
let f be FinSequence such that
A1: len f = m+1 and
A2: n in dom f;
ex k being Nat st len f = k+1 & len Del(f,n) = k by A2,Th102;
hence thesis by A1;
end;
theorem
for f being FinSequence st k < n holds Del(f,n).k = f.k
proof
let f be FinSequence;
assume
A1: k<n;
per cases;
suppose that
A2: n in dom f and
A3: f <> {};
consider m being Nat such that
A4: len f = m+1 by A3,NAT_1:6;
now
per cases;
suppose
A5: 1 <= k;
set X = dom f \ {n};
A6: dom Sgm(X)=Seg len Sgm(X) by FINSEQ_1:def 3;
A7: dom f=Seg len f by FINSEQ_1:def 3;
then
A8: len Sgm X = m by A4,A2,Th105;
rng Sgm(X) = X by FINSEQ_1:def 14;
then
A9: dom (f*Sgm X) = dom Sgm X by RELAT_1:27,XBOOLE_1:36;
n<=m+1 by A4,A2,Th25;
then k<m+1 by A1,XXREAL_0:2;
then k<=m by NAT_1:13;
then
A10: k in Seg m by A5,FINSEQ_1:1;
then 1<=k & k<n implies Sgm(X).k = k by A4,A2,A7,Th106;
hence thesis by A1,A5,A10,A6,A9,A8,FUNCT_1:12;
end;
suppose
A11: not 1 <= k;
Seg len Del (f,n) = Seg m by A4,A2,Th107;
then dom Del (f,n) = Seg m by FINSEQ_1:def 3;
then
A12: not k in dom Del (f,n) by A11,FINSEQ_1:1;
not k in dom f by A11,Th25;
then f.k = {} by FUNCT_1:def 2;
hence thesis by A12,FUNCT_1:def 2;
end;
end;
hence thesis;
end;
suppose
not n in dom f or f = {};
hence thesis by Th102;
end;
end;
theorem
for f being FinSequence st len f = m+1 & n in dom f & n<=k & k<=m
holds Del(f,n).k = f.(k+1)
proof
let f be FinSequence;
assume that
A1: len f = m+1 and
A2: n in dom f and
A3: n<=k and
A4: k<=m;
set X = dom f \ {n};
A5: dom f=Seg len f by FINSEQ_1:def 3;
rng Sgm(X) = X by FINSEQ_1:def 14;
then
A6: dom (f*Sgm(X)) = dom Sgm(X) by RELAT_1:27,XBOOLE_1:36;
A7: len Sgm(X) = m by A1,A2,A5,Th105;
A8: dom Sgm(X)=Seg len Sgm(X) by FINSEQ_1:def 3;
1<=n by A2,Th25;
then 1<=k by A3,XXREAL_0:2;
then
A9: k in Seg m by A4,FINSEQ_1:1;
then n<=k & k<=m implies Sgm(X).k = k+1 by A1,A2,A5,Th106;
hence thesis by A3,A4,A9,A8,A6,A7,FUNCT_1:12;
end;
:: from JORDAN3, 2005.11.16, A.T.
theorem Th110:
for f being FinSequence st k <= n holds (f|n).k = f.k
proof
let f be FinSequence;
assume
A1: k<=n;
per cases by NAT_1:14;
suppose
A2: k = 0;
then
A3: not k in dom f by Th25;
not k in dom(f|n) by A2,Th25;
hence (f|n).k = {} by FUNCT_1:def 2
.= f.k by A3,FUNCT_1:def 2;
end;
suppose
1 <= k;
then k in Seg n by A1,FINSEQ_1:1;
then (f|Seg n).k=f.k by FUNCT_1:49;
hence thesis by FINSEQ_1:def 16;
end;
end;
:: missing, 27.11.2005, A.T.
theorem
for p,q being FinSequence st p c= q holds q|len p = p
proof
let p,q be FinSequence such that
A1: p c= q;
A2: for k being Nat st k in dom p holds p.k = (q|len p).k
proof
let k be Nat;
assume
A3: k in dom p;
then
A4: k <= len p by Th25;
thus p.k = q.k by A1,A3,GRFUNC_1:2
.= (q|len p).k by A4,Th110;
end;
len p <= len q by A1,FINSEQ_1:63;
then len(q|len p) = len p by FINSEQ_1:59;
then dom(q|len p) = dom p by Th27;
hence thesis by A2;
end;
:: from MATRLIN, 2006.01.06, A.T.
theorem Th112:
for A being set, F being FinSequence holds
Sgm(F"A) ^ Sgm(F"(rng F \ A)) is Permutation of dom F
proof
let A be set;
let F be FinSequence;
A1: dom F = Seg len F by FINSEQ_1:def 3;
set p = Sgm(F"A)^Sgm(F"(rng F \ A));
A misses (rng F \ A) by XBOOLE_1:79;
then
A2: A /\ (rng F \ A) = {};
A3: F"A /\ F"(rng F \ A) = F"(A /\ (rng F \ A)) by FUNCT_1:68
.= {} by A2;
then
A4: F"A misses F"(rng F \ A);
F"(rng F \ A) c= dom F by RELAT_1:132;
then F"(rng F \ A) c= Seg len F by FINSEQ_1:def 3;
then
a6: F"(rng F \ A) is included_in_Seg by FINSEQ_1:def 13;
then
A7: Sgm(F"(rng F \ A)) is one-to-one;
F"A c= dom F by RELAT_1:132;
then F"A c= Seg len F by FINSEQ_1:def 3;
then
a9: F"A is included_in_Seg by FINSEQ_1:def 13;
then rng Sgm(F"A) /\ rng Sgm(F"(rng F \ A)) = F"A /\ rng Sgm(F"(rng F \ A))
by FINSEQ_1:def 14
.= {} by a6,A3,FINSEQ_1:def 14;
then
A10: rng Sgm(F"A) misses rng Sgm(F"(rng F \ A));
A11: rng p = rng Sgm(F"A) \/ rng Sgm(F"(rng F \ A)) by FINSEQ_1:31
.= F"A \/ rng Sgm(F"(rng F \ A)) by a9,FINSEQ_1:def 14
.= F"A \/ F"(rng F \ A) by a6,FINSEQ_1:def 14
.= F"(A \/ (rng F \ A)) by RELAT_1:140
.= F"((rng F) \/ A) by XBOOLE_1:39
.= F"(rng F) \/ F"A by RELAT_1:140
.= (dom F) \/ F"A by RELAT_1:134
.= dom F by RELAT_1:132,XBOOLE_1:12;
ww: F"A \/ F"(rng F \ A) is included_in_Seg by a6,a9;
Sgm(F"A) is one-to-one by a9;
then
A12: p is one-to-one by A7,A10,Th89;
len p = len Sgm(F"A) + len Sgm(F"(rng F \ A)) by FINSEQ_1:22
.= card (F"A) + len Sgm(F"(rng F \ A)) by a9,Th37
.= card (F"A) + card (F"(rng F \ A)) by a6,Th37
.= card (F"A \/ F"(rng F \ A)) by A4,CARD_2:40
.= len Sgm (F"A \/ F"(rng F \ A)) by ww,Th37
.= len Sgm (F"(A \/ (rng F \ A))) by RELAT_1:140
.= len Sgm (F"((rng F) \/ A)) by XBOOLE_1:39
.= len Sgm (F"(rng F) \/ F"A) by RELAT_1:140
.= len Sgm (dom F \/ F"A) by RELAT_1:134
.= len Sgm dom F by RELAT_1:132,XBOOLE_1:12
.= card Seg len F by A1,Th37
.= len F by FINSEQ_1:57;
then dom p = dom F by Th27;
then p is Function of dom F, dom F by A11,FUNCT_2:1;
hence thesis by A12,A11,FUNCT_2:57;
end;
theorem
for F being FinSequence, A be Subset of rng F
ex p being Permutation of dom F st (F-A`)^(F-A) = F*p
proof
let F be FinSequence;
let A be Subset of rng F;
set F1 = F-A`, F2 = F-A;
A` = (rng F) \ A by SUBSET_1:def 4;
then F"A` misses F"A by FUNCT_1:71,XBOOLE_1:79;
then card (F"A`) + card (F"A) = card ((F"A`) \/ (F"A)) by CARD_2:40
.=card (F"(A`\/A)) by RELAT_1:140
.= card (F"[#]rng F) by SUBSET_1:10
.= card (F"rng F) by SUBSET_1:def 3
.=card dom F by RELAT_1:134
.=len F by CARD_1:62;
then A1:len F = len F -card (F"A`) + (len F -card (F"A))
.= len F1 + (len F -card (F"A)) by Th57
.= len F1 + len F2 by Th57;
(rng F) \ (rng F1) = (rng F) \ (rng F \ A`) by Th63
.= rng F \ (rng F \ (rng F \ A)) by SUBSET_1:def 4
.= rng F \ (rng F /\ A) by XBOOLE_1:48
.= rng F \ A by XBOOLE_1:47
.= rng F2 by Th63;
then reconsider
p = Sgm(F"(rng F1))^Sgm(F"(rng F2)) as Permutation of dom F by Th112;
reconsider F3 = F * p as FinSequence by FINSEQ_2:40;
take p;
A2: now
A3: F"A` = F"(rng F \ A) by SUBSET_1:def 4
.= F"(rng F) \ F"A by FUNCT_1:69
.= dom F \ F"A by RELAT_1:134;
A4: F"(rng F) = dom F by RELAT_1:134;
then
A5: card(F"(rng F) \ F"A`) = card (F"(rng F)) - card (F"A`) by A3,CARD_2:44
,XBOOLE_1:36
.= card Seg len F - card (F"A`) by A4,FINSEQ_1:def 3
.= len F - card (F"A`) by FINSEQ_1:57
.= len (F - A`) by Th57;
F"(rng F1) c= dom F by RELAT_1:132;
then
F"(rng F1) c= Seg len F by FINSEQ_1:def 3;
then
a6: F"(rng F1) is included_in_Seg by FINSEQ_1:def 13;
let k be Nat such that
A7: k in dom F1;
A8: dom Sgm(F"(rng F1)) = Seg len Sgm(F"(rng F1)) by FINSEQ_1:def 3
.= Seg card(F"(rng F1)) by a6,Th37
.= Seg card(F"(rng F \ A`)) by Th63
.= Seg len (F - A`) by A5,FUNCT_1:69
.= dom F1 by FINSEQ_1:def 3;
dom Sgm(F"(rng F1)) c= dom p by FINSEQ_1:26;
hence (F*p).k = F.(p.k) by A7,A8,FUNCT_1:13
.= F.(Sgm(F"(rng F1)).k) by A7,A8,FINSEQ_1:def 7
.= (F*Sgm(F"(rng F1))).k by A7,A8,FUNCT_1:13
.= (F*Sgm(F"(rng F \ A`))).k by Th63
.= (F*Sgm(F"(rng F \ (rng F \ A)))).k by SUBSET_1:def 4
.= (F*Sgm(F"(rng F /\ A))).k by XBOOLE_1:48
.= (F*Sgm(F"(rng F) /\ F"A)).k by FUNCT_1:68
.= (F*Sgm(dom F /\ F"A)).k by RELAT_1:134
.= F1.k by A3,XBOOLE_1:48;
end;
A9: now
A10: F"(rng F) = dom F by RELAT_1:134;
F"A c= dom F by RELAT_1:132;
then F"A c= F"(rng F) by RELAT_1:134;
then
A11: card(F"(rng F) \ F"A) = card (F"(rng F)) - card (F"A) by CARD_2:44
.= card Seg len F - card (F"A) by A10,FINSEQ_1:def 3
.= len F - card (F"A) by FINSEQ_1:57
.= len (F - A) by Th57;
dom F = Seg len F by FINSEQ_1:def 3;
then F"(rng F2) is included_in_Seg by FINSEQ_1:def 13,RELAT_1:132;
then len Sgm(F"(rng F2)) = card(F"(rng F2)) by Th37
.= card(F"(rng F \ A)) by Th63
.= len (F - A) by A11,FUNCT_1:69;
then
A12: dom Sgm(F"(rng F2)) = dom F2 by Th27;
A13: F"(rng F) = dom F by RELAT_1:134;
F"A` = F"(rng F \ A) by SUBSET_1:def 4
.= F"(rng F) \ F"A by FUNCT_1:69
.= dom F \ F"A by RELAT_1:134; then
A14: card(F"(rng F) \ F"A`) = card (F"(rng F)) - card (F"A`)
by A13,CARD_2:44,XBOOLE_1:36
.= card Seg len F - card (F"A`) by A13,FINSEQ_1:def 3
.= len F - card (F"A`) by FINSEQ_1:57
.= len (F - A`) by Th57;
let k be Nat such that
A15: k in dom F2;
F"(rng F1) c= dom F by RELAT_1:132;
then F"(rng F1) c= Seg len F by FINSEQ_1:def 3;
then F"(rng F1) is included_in_Seg by FINSEQ_1:def 13;
then
A16: len Sgm(F"(rng F1)) = card(F"(rng F1)) by Th37
.= card(F"(rng F \ A`)) by Th63
.= len (F - A`) by A14,FUNCT_1:69;
then len F1 + k in dom p by A15,A12,FINSEQ_1:28;
hence (F*p).(len F1 + k) = F.(p.(len F1 + k)) by FUNCT_1:13
.= F.(Sgm(F"(rng F2)).k) by A15,A12,A16,FINSEQ_1:def 7
.= (F*Sgm(F"(rng F2))).k by A15,A12,FUNCT_1:13
.= (F*Sgm(F"(rng F \ A))).k by Th63
.= (F*Sgm(F"(rng F) \ F"A)).k by FUNCT_1:69
.= F2.k by RELAT_1:134;
end;
len F3 = len F1 + len F2 by A1,FINSEQ_2:44;
hence thesis by A2,A9,Th36;
end;
:: Moved from GRAPH_2 by AK on 27.12.2006
theorem
for f being FinSubsequence holds f is FinSequence implies Seq f = f
proof
let f be FinSubsequence;
assume f is FinSequence;
then reconsider ss9=f as FinSequence;
consider k be Nat such that
A1: dom ss9 = Seg k by FINSEQ_1:def 2;
k in NAT by ORDINAL1:def 12;
then
A2: len ss9 <= k by A1,FINSEQ_1:def 3;
Seq f = f* Sgm Seg k by A1,FINSEQ_1:def 15
.= f* idseq k by Th46
.= f by A2,FINSEQ_2:54;
hence thesis;
end;
:: Moved from SCMBSORT by AK on 10.10.2007
theorem
for t be FinSequence of INT holds t is FinSequence of REAL
proof
let t be FinSequence of INT;
now
let i be Nat;
assume i in dom t;
then
A1: t.i in rng t by FUNCT_1:def 3;
t.i in INT by A1;
hence t.i in REAL by NUMBERS:15;
end;
hence thesis by FINSEQ_2:12;
end;
:: missing, 2008.02.16, A.T,
theorem
len p < len q iff dom p c< dom q
proof
A1: len p = len q iff dom p = dom q by Th27;
len p <= len q iff dom p c= dom q by Th28;
hence thesis by A1,XXREAL_0:1;
end;
:: from CATALG_1, 2009.09.08, A.T.
theorem Th117:
for A being set, i being Nat holds i <> 0 & A = {} iff i-tuples_on A = {}
proof
let A be set, i be Nat;
hereby
assume i <> 0;
then
A1: 0+1 <= i by NAT_1:13;
assume that
A2: A = {} and
A3: i-tuples_on A <> {};
reconsider B = i-tuples_on A as non empty FinSequenceSet of A by A3;
set p = the Element of B;
B = {s where s is Element of A*: len s = i} & p in B;
then ex s being Element of A* st p = s & len s = i;
then 1 in dom p by A1,Th25;
then
A4: rng p <> {} by RELAT_1:42;
thus contradiction by A2,A4;
end;
assume that
A5: i-tuples_on A = {} and
A6: i = 0 or A <> {};
len (<*>A) = 0;
then reconsider A as non empty set by A5,A6,FINSEQ_2:133;
i-tuples_on A is non empty;
hence contradiction by A5;
end;
:: from AMISTD_2, 2009.09.08, A.T.
registration
let i be Nat, D be set;
cluster i-tuples_on D -> with_common_domain;
coherence
proof
set S = i-tuples_on D;
let f, g be Function such that
A1: f in S and
A2: g in S;
A3: ex s being Element of D* st f = s & len s = i by A1;
ex s being Element of D* st g = s & len s = i by A2;
hence thesis by A3,Th27;
end;
end;
registration
let i be Nat, D be set;
cluster i-tuples_on D -> product-like;
coherence
proof
set S = i-tuples_on D;
per cases;
suppose D = {} & i = 0;
then S = { <*>D } by FINSEQ_2:94
.= {{}};
hence thesis by CARD_3:10;
end;
suppose D = {} & i <> 0;
then
A1: S = {} by Th117;
take f = 0 .--> {};
rng f = {{}} by FUNCOP_1:8;
then {} in rng f by TARSKI:def 1;
hence thesis by A1,CARD_3:26;
end;
suppose D <> {};
then reconsider D as non empty set;
set S = i-tuples_on D;
take product" S;
S = product product" S
proof
thus S c= product product" S by CARD_3:77;
let x be object;
assume x in product product" S;
then consider g being Function such that
A2: x = g and
A3: dom g = dom product" S and
A4: for z being object st z in dom product" S holds g.z in (product" S).z
by CARD_3:def 5;
set s = the Element of S;
s in S;
then consider t being Element of D* such that
A5: s = t and
A6: len t = i;
A7: dom g = DOM S by A3,CARD_3:def 12
.= dom s by CARD_3:108;
dom s = Seg len t by A5,FINSEQ_1:def 3;
then
A8: g is FinSequence by A7,FINSEQ_1:def 2;
rng g c= D
proof
let y be object;
assume y in rng g;
then consider a being object such that
A9: a in dom g and
A10: g.a = y by FUNCT_1:def 3;
reconsider a as set by TARSKI:1;
g.a in (product" S).a by A3,A4,A9;
then g.a in pi(S,a) by A3,A9,CARD_3:def 12;
then consider f being Function such that
A11: f in S and
A12: g.a = f.a by CARD_3:def 6;
consider w being Element of D* such that
A13: f = w and len w = i by A11;
dom g = dom w by A7,A11,A13,CARD_3:def 10;
then w.a in rng w by A9,FUNCT_1:def 3;
hence thesis by A10,A12,A13;
end;
then reconsider g as FinSequence of D by A8,FINSEQ_1:def 4;
A15: g in D* by FINSEQ_1:def 11;
len g = i by A5,A6,A7,Th27;
hence thesis by A2,A15;
end;
hence thesis;
end;
end;
end;
begin :: Moved from ALG_1, 2010.03.17
reserve n for Nat;
theorem
for D1,D2 be non empty set, p be FinSequence of D1,
f be Function of D1,D2 holds dom(f*p) = dom p &
len (f*p) = len p &
for n being Nat st n in dom (f*p) holds (f*p).n = f.(p.n)
proof
let D1,D2 be non empty set, p be FinSequence of D1, f be Function of D1,D2;
A1: rng p c= D1 & dom f = D1 by FUNCT_2:def 1;
hence dom(f*p) = dom p by RELAT_1:27;
dom(f*p) = dom p by A1,RELAT_1:27;
hence len(f*p) = len p by Th27;
let n be Nat;
assume n in dom (f*p);
hence thesis by FUNCT_1:12;
end;
definition
let D be non empty set, R be Relation of D;
func ExtendRel(R) -> Relation of D* means :Def3:
for x,y be FinSequence of D holds [x,y] in it iff
len x = len y & for n st n in dom x holds [x.n,y.n] in R;
existence
proof
defpred P[object,object] means
for a,b be FinSequence of D st a = $1 & b = $2
holds len a = len b & for n st n in dom a holds [a.n,b.n] in R;
consider P be Relation of D*,D* such that
A1: for x,y be object holds [x,y] in P iff x in D* & y in D* & P[x,y]
from RELSET_1:sch 1;
take P;
let a,b be FinSequence of D;
thus [a,b] in P implies len a = len b & for n st n in dom a holds [a.n,b.n
] in R by A1;
assume len a = len b & for n st n in dom a holds [a.n,b.n] in R;
then
A2: P[a,b];
a in D* & b in D* by FINSEQ_1:def 11;
hence thesis by A1,A2;
end;
uniqueness
proof
let P,Q be Relation of D*;
assume that
A3: for x,y be FinSequence of D holds [x,y] in P iff len x = len y &
for n st n in dom x holds [x.n,y.n] in R and
A4: for x,y be FinSequence of D holds [x,y] in Q iff len x = len y &
for n st n in dom x holds [x.n,y.n] in R;
for a,b be object holds [a,b] in P iff [a,b] in Q
proof
let a,b be object;
thus [a,b] in P implies [a,b] in Q
proof
assume
A5: [a,b] in P;
then reconsider a1 = a, b1 = b as Element of D* by ZFMISC_1:87;
len a1 = len b1 & for n st n in dom a1 holds [a1.n,b1.n] in R by A3,A5;
hence thesis by A4;
end;
assume
A6: [a,b] in Q;
then reconsider a1 = a, b1 = b as Element of D* by ZFMISC_1:87;
len a1 = len b1 & for n st n in dom a1 holds [a1.n,b1.n] in R by A4,A6;
hence thesis by A3;
end;
hence thesis by RELAT_1:def 2;
end;
end;
theorem
for D be non empty set holds ExtendRel(id D) = id (D*)
proof
let D be non empty set;
set P = ExtendRel(id D), Q = id(D*);
for a,b be object holds [a,b] in P iff [a,b] in Q
proof
let a,b be object;
thus [a,b] in P implies [a,b] in Q
proof
assume
A1: [a,b] in P;
then reconsider a1 = a, b1 = b as Element of D* by ZFMISC_1:87;
A2: now
let n be Nat;
assume n in dom a1;
then [a1.n,b1.n] in id D by A1,Def3;
hence a1.n = b1.n by RELAT_1:def 10;
end;
len a1 = len b1 by A1,Def3;
then a1 = b1 by A2,FINSEQ_2:9;
hence thesis by RELAT_1:def 10;
end;
assume
A3: [a,b] in Q;
then reconsider a1 = a, b1 = b as Element of D* by ZFMISC_1:87;
A4: a1 = b1 by A3,RELAT_1:def 10;
A5: for n st n in dom a1 holds [a1.n,b1.n] in id D
proof
let n;
assume n in dom a1;
then a1.n in D by FINSEQ_2:11;
hence thesis by A4,RELAT_1:def 10;
end;
len a1 = len b1 by A3,RELAT_1:def 10;
hence thesis by A5,Def3;
end;
hence thesis by RELAT_1:def 2;
end;
definition
let D be non empty set, R be Equivalence_Relation of D;
let y be FinSequence of Class(R), x be FinSequence of D;
pred x is_representatives_FS y means
len x = len y & for n st n in dom x holds Class(R,x.n) = y.n;
end;
theorem
for D be non empty set, R be Equivalence_Relation of D,
y be FinSequence of Class(R)
ex x be FinSequence of D st x is_representatives_FS y
proof
let D be non empty set, R be Equivalence_Relation of D,
y be FinSequence of Class R;
defpred P[object,object] means
for u be Element of D st $2 = u holds Class(R,u) = y.$1;
A1: for e be object st e in dom y ex u be object st u in D & P[e,u]
proof
let e be object;
assume e in dom y;
then y.e in rng y by FUNCT_1:def 3;
then consider a be Element of D such that
A2: y.e = Class(R,a) by EQREL_1:36;
take a;
thus a in D;
let u be Element of D;
assume a = u;
hence thesis by A2;
end;
consider f being Function such that
A3: dom f = dom y & rng f c= D &
for e be object st e in dom y holds P[e,f.e] from FUNCT_1:sch 6(A1);
dom f = Seg len y by A3,FINSEQ_1:def 3;
then reconsider f as FinSequence by FINSEQ_1:def 2;
reconsider f as FinSequence of D by A3,FINSEQ_1:def 4;
take f;
thus len f = len y by A3,Th27;
let n;
assume
A4: n in dom f;
then f.n in rng f by FUNCT_1:def 3;
then reconsider u = f.n as Element of D;
Class(R,u) = y.n by A3,A4;
hence thesis;
end;
:: from FUNCT_6, 2011.04.18, A.T.
reserve x,y,y1,y2,z,a,b for object, X,Y,Z,V1,V2 for set,
f,g,h,h9,f1,f2 for Function,
i for Nat,
P for Permutation of X,
D,D1,D2,D3 for non empty set,
d1 for Element of D1,
d2 for Element of D2,
d3 for Element of D3;
theorem Th121:
x in product <*X*> iff ex y st y in X & x = <*y*>
proof
A1: dom <*X*> = Seg 1 by FINSEQ_1:def 8;
A2: <*X*>.1 = X;
A3: 1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
thus x in product <*X*> implies ex y st y in X & x = <*y*>
proof
assume x in product <*X*>;
then consider f such that
A4: x = f and
A5: dom f = dom <*X*> and
A6: for x being object st x in dom <*X*> holds f.x in <*X*>.x by CARD_3:def 5;
reconsider f as FinSequence by A1,A5,FINSEQ_1:def 2;
take f.1;
thus thesis by A1,A3,A2,A4,A5,A6,FINSEQ_1:def 8;
end;
given y such that
A7: y in X and
A8: x = <*y*>;
A9: now
let a be object;
assume a in Seg 1;
then a = 1 by FINSEQ_1:2,TARSKI:def 1;
hence <*y*>.a in <*X*>.a by A7;
end;
dom <*y*> = Seg 1 by FINSEQ_1:def 8;
hence thesis by A1,A8,A9,CARD_3:def 5;
end;
theorem Th122:
z in product <*X,Y*> iff ex x,y st x in X & y in Y & z = <*x,y*>
proof
A1: <*X,Y*>.1 = X & <*X,Y*>.2 = Y;
len <*X,Y*> = 2 by FINSEQ_1:44;
then
A2: dom <*X,Y*> = Seg 2 by FINSEQ_1:def 3;
A3: 1 in Seg 2 & 2 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
thus z in product <*X,Y*> implies ex x,y st x in X & y in Y & z = <*x,y*>
proof
assume z in product <*X,Y*>;
then consider f such that
A4: z = f and
A5: dom f = dom <*X,Y*> and
A6: for x being object st x in dom <*X,Y*> holds f.x in <*X,Y*>.x
by CARD_3:def 5;
reconsider f as FinSequence by A2,A5,FINSEQ_1:def 2;
take f.1, f.2;
len f = 2 by A2,A5,FINSEQ_1:def 3;
hence thesis by A2,A3,A1,A4,A6,FINSEQ_1:44;
end;
given x,y such that
A7: x in X & y in Y and
A8: z = <*x,y*>;
A9: now
let a be object;
assume a in Seg 2;
then a = 1 or a = 2 by FINSEQ_1:2,TARSKI:def 2;
hence <*x,y*>.a in <*X,Y*>.a by A7;
end;
len <*x,y*> = 2 by FINSEQ_1:44;
then dom <*x,y*> = Seg 2 by FINSEQ_1:def 3;
hence thesis by A2,A8,A9,CARD_3:def 5;
end;
theorem Th123:
a in product <*X,Y,Z*> iff
ex x,y,z st x in X & y in Y & z in Z & a = <*x,y,z*>
proof
A1: 3 in Seg 3 by Th1,ENUMSET1:def 1;
A2: <*X,Y,Z*>.1 = X & <*X,Y,Z*>.2 = Y;
A3: <*X,Y,Z*>.3 = Z;
len <*X,Y,Z*> = 3 by FINSEQ_1:45;
then
A4: dom <*X,Y,Z*> = Seg 3 by FINSEQ_1:def 3;
A5: 1 in Seg 3 & 2 in Seg 3 by Th1,ENUMSET1:def 1;
thus a in product <*X,Y,Z*> implies ex x,y,z st x in X & y in Y & z in Z & a
= <*x,y,z*>
proof
assume a in product <*X,Y,Z*>;
then consider f such that
A6: a = f and
A7: dom f = dom <*X,Y,Z*> and
A8: for x being object st x in dom <*X,Y,Z*> holds f.x in <*X,Y,Z*>.x
by CARD_3:def 5;
reconsider f as FinSequence by A4,A7,FINSEQ_1:def 2;
take f.1, f.2, f.3;
len f = 3 by A4,A7,FINSEQ_1:def 3;
hence thesis by A4,A5,A1,A2,A3,A6,A8,FINSEQ_1:45;
end;
given x,y,z such that
A9: x in X & y in Y & z in Z and
A10: a = <*x,y,z*>;
A11: now
let a be object;
assume a in Seg 3;
then a = 1 or a = 2 or a = 3 by Th1,ENUMSET1:def 1;
hence <*x,y,z*>.a in <*X,Y,Z*>.a by A9;
end;
len <*x,y,z*> = 3 by FINSEQ_1:45;
then dom <*x,y,z*> = Seg 3 by FINSEQ_1:def 3;
hence thesis by A4,A10,A11,CARD_3:def 5;
end;
theorem
product <*D*> = 1-tuples_on D
proof
<*D*> = 1 |-> D by FINSEQ_2:59
.= Seg 1 --> D;
then product <*D*> = Funcs(Seg 1,D) by CARD_3:11;
hence thesis by FINSEQ_2:93;
end;
theorem Th125:
product <*D1,D2*> = the set of all <*d1,d2*>
proof
thus product <*D1,D2*> c= the set of all <*d1,d2*>
proof
let a be object;
assume a in product <*D1,D2*>;
then ex x,y st x in D1 & y in D2 & a = <*x,y*> by Th122;
hence thesis;
end;
let a be object;
assume a in the set of all <*d1,d2*>;
then ex d1,d2 st a = <*d1,d2*>;
hence thesis by Th122;
end;
theorem
product <*D,D*> = 2-tuples_on D
proof
thus product <*D,D*> = the set of all
<*d1,d2*> where d1 is Element of D, d2 is Element of
D by Th125
.= 2-tuples_on D by FINSEQ_2:99;
end;
theorem Th127:
product <*D1,D2,D3*> = the set of all <*d1,d2,d3*>
proof
thus product <*D1,D2,D3*> c= the set of all <*d1,d2,d3*>
proof
let a be object;
assume a in product <*D1,D2,D3*>;
then ex x,y,z st x in D1 & y in D2 & z in D3 & a = <*x,y,z*> by Th123;
hence thesis;
end;
let a be object;
assume a in the set of all <*d1,d2,d3*>;
then ex d1,d2,d3 st a = <*d1,d2,d3*>;
hence thesis by Th123;
end;
theorem
product <*D,D,D*> = 3-tuples_on D
proof
thus product <*D,D,D*> = the set of all <*d1,d2,d3*>
where d1 is Element of D, d2 is Element of D,
d3 is Element of D by Th127
.= 3-tuples_on D by FINSEQ_2:102;
end;
theorem Th129:
for D being set holds product (i |-> D) = i-tuples_on D
proof let D be set;
thus product (i |-> D) = product (Seg i --> D)
.= Funcs(Seg i,D) by CARD_3:11
.= i-tuples_on D by FINSEQ_2:93;
end;
registration
let f be Function;
cluster <*f*> -> Function-yielding;
coherence
proof
let x be object;
assume x in dom <*f*>;
then x in {1} by FINSEQ_1:2,38;
then x = 1 by TARSKI:def 1;
hence thesis;
end;
let g be Function;
cluster <*f,g*> -> Function-yielding;
coherence
proof
let x be object;
assume x in dom <*f,g*>;
then x in {1,2} by FINSEQ_1:2,89;
then x = 1 or x = 2 by TARSKI:def 2;
hence thesis;
end;
let h be Function;
cluster <*f,g,h*> -> Function-yielding;
coherence
proof
let x be object;
assume x in dom <*f,g,h*>;
then x in {1,2,3} by FINSEQ_1:89,Th1;
then x = 1 or x = 2 or x = 3 by ENUMSET1:def 1;
hence thesis;
end;
end;
theorem Th130:
doms <*f*> = <*dom f*> & rngs <*f*> = <*rng f*>
proof
A1: dom doms <*f*> = dom <*f*> & dom <*dom f*> = Seg 1
by FINSEQ_1:38,FUNCT_6:def 2;
A2: <*f*>.1 = f;
A3: dom <*f*> = Seg 1 & {f} = {f} by FINSEQ_1:38;
A5: now
let x be object;
assume
A6: x in {1};
then x = 1 by TARSKI:def 1;
hence (rngs <*f*>).x = <*rng f*>.x
by A2,A3,A6,FINSEQ_1:2,FUNCT_6:def 3;
end;
now
let x be object;
assume
A8: x in {1};
then x = 1 by TARSKI:def 1;
hence (doms <*f*>).x = <*dom f*>.x
by A2,A3,A8,FINSEQ_1:2,FUNCT_6:def 2;
end;
hence doms <*f*> = <*dom f*> by A1,A3,FINSEQ_1:2;
dom rngs <*f*> = dom <*f*> & dom <*rng f*> = Seg 1
by FINSEQ_1:38,FUNCT_6:def 3;
hence thesis by A3,A5,FINSEQ_1:2;
end;
theorem Th131:
doms <*f,g*> = <*dom f, dom g*> & rngs <*f,g*> = <*rng f, rng g *>
proof
A1: dom doms <*f,g*> = dom <*f,g*> & dom <*dom f, dom g*> =
Seg 2 by FINSEQ_1:89,FUNCT_6:def 2;
A2: <*f,g*>.1 = f & <*f,g*>.2 = g;
A3: dom <*f,g*> = Seg 2 & {f,g} = {f,g} by FINSEQ_1:89;
A5: now
let x be object;
assume
A6: x in {1,2};
then x = 1 or x = 2 by TARSKI:def 2;
hence (rngs <*f,g*>).x = <*rng f, rng g*>.x
by A2,A3,A6,FINSEQ_1:2,FUNCT_6:def 3;
end;
now
let x be object;
assume
A8: x in {1,2};
then x = 1 or x = 2 by TARSKI:def 2;
hence (doms <*f,g*>).x = <*dom f, dom g*>.x
by A2,A3,A8,FINSEQ_1:2,FUNCT_6:def 2;
end;
hence doms <*f,g*> = <*dom f, dom g*> by A1,A3,FINSEQ_1:2;
dom rngs <*f,g*> = dom <*f,g*> & dom <*rng f, rng g*>
= Seg 2 by FINSEQ_1:89,FUNCT_6:def 3;
hence thesis by A3,A5,FINSEQ_1:2;
end;
theorem
doms <*f,g,h*> = <*dom f, dom g, dom h*> & rngs <*f,g,h*> = <*rng f,
rng g, rng h*>
proof
A2: <*f,g,h*>.1 = f & <*f,g,h*>.2 = g;
A3: <*f,g,h*>.3 = h;
A4: dom <*f,g,h*> = Seg 3 & {f,g,h} = {f,g,h} by FINSEQ_1:89;
A6: now
let x be object;
assume
A7: x in {1,2,3};
then x = 1 or x = 2 or x = 3 by ENUMSET1:def 1;
hence (rngs <*f,g,h*>).x = <*rng f, rng g, rng h*>.x
by A2,A3,A4,A7,Th1,FUNCT_6:def 3;
end;
A8: dom doms <*f,g,h*> = dom <*f,g,h*> & dom <*dom f, dom
g, dom h*> = Seg 3 by FINSEQ_1:89,FUNCT_6:def 2;
now
let x be object;
assume
A11: x in {1,2,3};
then x = 1 or x = 2 or x = 3 by ENUMSET1:def 1;
hence (doms <*f,g,h*>).x = <*dom f, dom g, dom h*>.x by A2,A3,A4
,A11,Th1,FUNCT_6:def 2;
end;
hence doms <*f,g,h*> = <*dom f, dom g, dom h*> by A8,A4,Th1;
dom rngs <*f,g,h*> = dom <*f,g,h*> & dom <*rng f,
rng g, rng h*> = Seg 3 by FINSEQ_1:89,FUNCT_6:def 3;
hence thesis by A4,A6,Th1;
end;
theorem Th133:
Union <*X*> = X & meet <*X*> = X
proof
thus Union <*X*> = union rng <*X*>
.= union {X} by FINSEQ_1:38
.= X by ZFMISC_1:25;
thus meet <*X*> = meet {X} by FINSEQ_1:38
.= X by SETFAM_1:10;
end;
theorem Th134:
Union <*X,Y*> = X \/ Y & meet <*X,Y*> = X /\ Y
proof
thus Union <*X,Y*> = union rng <*X,Y*>
.= union {X,Y} by FINSEQ_2:127
.= X \/ Y by ZFMISC_1:75;
thus meet <*X,Y*> = meet {X,Y} by FINSEQ_2:127
.= X /\ Y by SETFAM_1:11;
end;
theorem
Union <*X,Y,Z*> = X \/ Y \/ Z & meet <*X,Y,Z*> = X /\ Y /\ Z
proof
A1: union ({X,Y} \/ {Z}) = union {X,Y} \/ union {Z} & union {X,Y} = X \/ Y
by ZFMISC_1:75,78;
A2: union {Z} = Z by ZFMISC_1:25;
A3: {X,Y} \/ {Z} = {X,Y,Z} by ENUMSET1:3;
thus Union <*X,Y,Z*> = union rng <*X,Y,Z*>
.= X \/ Y \/ Z by A1,A2,A3,FINSEQ_2:128;
A4: meet {Z} = Z by SETFAM_1:10;
meet ({X,Y} \/ {Z}) = meet {X,Y} /\ meet {Z} & meet {X,Y} = X /\ Y by
SETFAM_1:9,11;
hence thesis by A4,A3,FINSEQ_2:128;
end;
theorem
x in dom f implies <*f*>..(1,x) = f.x & <*f,g*>..(1,x) = f.x &
<*f,g,h*>..(1,x) = f.x
proof
A1: <*f,g,h*>.1 = f & 1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
A2: dom <*f*> = Seg 1 & dom <*f,g*> = Seg 2 by FINSEQ_1:89;
A3: 1 in Seg 2 & 1 in Seg 3 by Th1,ENUMSET1:def 1,FINSEQ_1:2,TARSKI:def 2;
A4: dom <*f,g,h*> = Seg 3 by FINSEQ_1:89;
<*f*>.1 = f & <*f,g*>.1 = f;
hence thesis by A1,A3,A2,A4,FUNCT_5:38;
end;
theorem
x in dom g implies <*f,g*>..(2,x) = g.x & <*f,g,h*>..(2,x) = g.x
proof
A1: 2 in Seg 2 & 2 in Seg 3 by Th1,ENUMSET1:def 1,FINSEQ_1:2,TARSKI:def 2;
A2: dom <*f,g*> = Seg 2 & dom <*f,g,h*> = Seg 3 by FINSEQ_1:89;
<*f,g*>.2 = g & <*f,g,h*>.2 = g;
hence thesis by A1,A2,FUNCT_5:38;
end;
theorem
x in dom h implies <*f,g,h*>..(3,x) = h.x
proof
A1: dom <*f,g,h*> = Seg 3 by FINSEQ_1:89;
<*f,g,h*>.3 = h & 3 in Seg 3 by Th1,ENUMSET1:def 1;
hence thesis by A1,FUNCT_5:38;
end;
theorem
dom <:<*h*>:> = dom h & for x st x in dom h holds <:<*h*>:>.x = <*h.x *>
proof
A1: 1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
A2: rng <:<*h*>:> c= product rngs <*h*> & rngs <*h*> = <*rng h*>
by Th130,FUNCT_6:29;
thus
A3: dom <:<*h*>:> = meet doms <*h*> by FUNCT_6:29
.= meet <*dom h*> by Th130
.= dom h by Th133;
let x;
assume
A4: x in dom h;
then <:<*h*>:>.x in rng <:<*h*>:> by A3,FUNCT_1:def 3;
then consider g such that
A5: <:<*h*>:>.x = g and
A6: dom g = dom <*rng h*> and
for y being object st y in dom <*rng h*> holds g.y in <*rng h*>.y
by A2,CARD_3:def 5;
A7: dom g = Seg 1 by A6,FINSEQ_1:38;
dom <*h*> = Seg 1 & <*h*>.1 = h by FINSEQ_1:38;
then
A8: (uncurry <*h*>).(1,x) = h.x by A4,A1,FUNCT_5:38;
reconsider g as FinSequence by A7,FINSEQ_1:def 2;
A9: len g = 1 by A7,FINSEQ_1:def 3;
g.1 = (uncurry <*h*>).(1,x) by A3,A4,A5,A7,A1,FUNCT_6:31;
hence thesis by A5,A8,A9,FINSEQ_1:40;
end;
theorem Th140:
dom <:<*f1,f2*>:> = dom f1 /\ dom f2 &
for x st x in dom f1 /\ dom f2 holds
<:<*f1,f2*>:>.x = <*f1.x,f2.x*>
proof
A1: dom <*f1,f2*> = Seg 2 by FINSEQ_1:89;
A2: rng <:<*f1,f2*>:> c= product rngs <*f1,f2*> & rngs <*f1,f2*> = <*rng f1,
rng f2*> by Th131,FUNCT_6:29;
thus
A3: dom <:<*f1,f2*>:> = meet doms <*f1,f2*> by FUNCT_6:29
.= meet <*dom f1, dom f2*> by Th131
.= dom f1 /\ dom f2 by Th134;
let x;
assume
A4: x in dom f1 /\ dom f2;
then <:<*f1,f2*>:>.x in rng <:<*f1,f2*>:> by A3,FUNCT_1:def 3;
then consider g such that
A5: <:<*f1,f2*>:>.x = g and
A6: dom g = dom <*rng f1, rng f2*> and
for y being object st y in dom <*rng f1, rng f2*>
holds g.y in <*rng f1, rng f2*> .y
by A2,CARD_3:def 5;
A7: dom g = Seg 2 by A6,FINSEQ_1:89;
A8: 1 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
reconsider g as FinSequence by A7,FINSEQ_1:def 2;
A9: 2 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then
A10: g.2 = (uncurry <*f1,f2*>).(2,x) by A3,A4,A5,A7,FUNCT_6:31;
<*f1,f2*>.2 = f2 & x in dom f2 by A4,XBOOLE_0:def 4;
then
A11: (uncurry <*f1,f2*>).(2,x) = f2.x by A1,A9,FUNCT_5:38;
A12: len g = 2 by A7,FINSEQ_1:def 3;
<*f1,f2*>.1 = f1 & x in dom f1 by A4,XBOOLE_0:def 4;
then
A13: (uncurry <*f1,f2*>).(1,x) = f1.x by A1,A8,FUNCT_5:38;
g.1 = (uncurry <*f1,f2*>).(1,x) by A3,A4,A5,A7,A8,FUNCT_6:31;
hence thesis by A5,A13,A10,A11,A12,FINSEQ_1:44;
end;
theorem
dom Frege<*h*> = product <*dom h*> &
rng Frege<*h*> = product <*rng h*> &
for x st x in dom h holds (Frege<*h*>).<*x*> = <*h.x*>
proof
A1: <*h*>.1 = h;
A2: rngs <*h*> = <*rng h*> by Th130;
A3: doms <*h*> = <*dom h*> by Th130;
hence
dom Frege<*h*> = product <*dom h*> & rng Frege<*h*> = product <*rng h*>
by A2,FUNCT_6:38,def 7;
let x;
assume x in dom h;
then
A4: <*x*> in product doms <*h*> by A3,Th121;
then consider f such that
A5: (Frege<*h*>).<*x*> = f and
dom f = dom <*h*> and
for y st y in dom f holds f.y = (uncurry <*h*>).(y,<*x*>.y) by FUNCT_6:def 7;
A6: dom <*h*> = Seg 1 & 1 in Seg 1 by FINSEQ_1:2,def 8,TARSKI:def 1;
then dom <*rng h*> = Seg 1 & f in product rngs <*h*> by A1,A4,A5,
FINSEQ_1:def 8,FUNCT_6:37;
then
A7: dom f = Seg 1 by A2,CARD_3:9;
reconsider f as FinSequence by A7,FINSEQ_1:def 2;
f.1 = h.(<*x*>.1) by A6,A1,A4,A5,FUNCT_6:37;
hence thesis by A5,A7,FINSEQ_1:def 8;
end;
theorem Th142:
dom Frege<*f1,f2*> = product <*dom f1, dom f2*> &
rng Frege<*f1,f2*> = product <*rng f1, rng f2*> &
for x,y st x in dom f1 & y in dom f2 holds
(Frege<*f1,f2*>).<*x,y*> = <*f1.x, f2.y*>
proof
A1: rngs <*f1,f2*> = <*rng f1, rng f2*> by Th131;
len <*rng f1, rng f2*> = 2 by FINSEQ_1:44;
then
A2: dom <*rng f1, rng f2*> = Seg 2 by FINSEQ_1:def 3;
len <*f1,f2*> = 2 by FINSEQ_1:44;
then
A3: dom <*f1,f2*> = Seg 2 by FINSEQ_1:def 3;
A4: doms <*f1,f2*> = <*dom f1, dom f2*> by Th131;
hence dom Frege<*f1,f2*> = product <*dom f1, dom f2*> & rng Frege<*f1,f2*> =
product <*rng f1, rng f2*> by A1,FUNCT_6:38,def 7;
let x,y;
assume x in dom f1 & y in dom f2;
then
A5: <*x,y*> in product doms <*f1,f2*> by A4,Th122;
then consider f such that
A6: (Frege<*f1,f2*>).<*x,y*> = f and
dom f = dom <*f1,f2*> and
for z st z in dom f holds f.z = (uncurry <*f1,f2*>).(z,<*x,y*>.z)
by FUNCT_6:def 7;
A8: 1 in Seg 2 & <*f1,f2*>.1 = f1 by FINSEQ_1:2,TARSKI:def 2;
then f in product rngs <*f1,f2*> by A3,A5,A6,FUNCT_6:37;
then
A9: dom f = Seg 2 by A1,A2,CARD_3:9;
then reconsider f as FinSequence by FINSEQ_1:def 2;
2 in Seg 2 & <*f1,f2*>.2 = f2 by FINSEQ_1:2,TARSKI:def 2;
then
A10: f.2 = f2.(<*x,y*>.2) by A3,A5,A6,FUNCT_6:37;
A11: len f = 2 by A9,FINSEQ_1:def 3;
f.1 = f1.(<*x,y*>.1) by A3,A8,A5,A6,FUNCT_6:37;
hence thesis by A6,A10,A11,FINSEQ_1:44;
end;
theorem
x in dom f1 & x in dom f2 implies
for y1,y2 holds <:f1,f2:>.x = [y1,y2] iff <:<*f1,f2*>:>.x = <*y1,y2*>
proof
A1: <*f1.x,f2.x*>.1 = f1.x & <*f1.x,f2.x*>.2 = f2.x;
assume x in dom f1 & x in dom f2;
then
A2: x in dom f1 /\ dom f2 by XBOOLE_0:def 4;
let y1,y2;
A3: <*y1,y2*>.1 = y1 & <*y1,y2*>.2 = y2;
[f1.x,f2.x] = [y1,y2] iff f1.x = y1 & f2.x = y2 by XTUPLE_0:1;
hence thesis by A2,A1,A3,Th140,FUNCT_3:48;
end;
theorem
x in dom f1 & y in dom f2 implies for y1,y2 holds
[:f1,f2:].(x,y) = [y1,y2] iff (Frege<*f1,f2*>).<*x,y*> = <*y1,y2*>
proof
assume
A1: x in dom f1 & y in dom f2;
let y1,y2;
A2: <*f1.x,f2.y*>.1 = f1.x & <*f1.x,f2.y*>.2 = f2.y;
A3: <*y1,y2*>.1 = y1 & <*y1,y2*>.2 = y2;
[f1.x,f2.y] = [y1,y2] iff f1.x = y1 & f2.y = y2 by XTUPLE_0:1;
hence thesis by A1,A2,A3,Th142,FUNCT_3:def 8;
end;
theorem
Funcs(<*X*>,Y) = <*Funcs(X,Y)*>
proof
A1: dom <*X*> = Seg 1 by FINSEQ_1:def 8;
A2: dom Funcs(<*X*>,Y) = dom <*X*> by FUNCT_6:def 8;
then reconsider p = Funcs(<*X*>,Y) as FinSequence by A1,FINSEQ_1:def 2;
<*X*>.1 = X & 1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then p.1 = Funcs(X,Y) by A1,FUNCT_6:def 8;
hence thesis by A2,A1,FINSEQ_1:def 8;
end;
theorem
Funcs(<*X,Y*>,Z) = <*Funcs(X,Z), Funcs(Y,Z)*>
proof
A1: Seg len <*X,Y*> = dom <*X,Y*> by FINSEQ_1:def 3;
A2: dom Funcs(<*X,Y*>,Z) = dom <*X,Y*> by FUNCT_6:def 8;
then reconsider p = Funcs(<*X,Y*>,Z) as FinSequence by A1,FINSEQ_1:def 2;
A3: len <*X,Y*> = 2 by FINSEQ_1:44;
then
A4: len p = 2 by A2,A1,FINSEQ_1:def 3;
<*X,Y*>.2 = Y & 2 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then
A5: p.2 = Funcs(Y,Z) by A3,A1,FUNCT_6:def 8;
<*X,Y*>.1 = X & 1 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then p.1 = Funcs(X,Z) by A3,A1,FUNCT_6:def 8;
hence thesis by A4,A5,FINSEQ_1:44;
end;
theorem
Funcs(X,<*Y*>) = <*Funcs(X,Y)*>
proof
A1: dom <*Y*> = Seg 1 by FINSEQ_1:def 8;
A2: dom Funcs(X,<*Y*>) = dom <*Y*> by FUNCT_6:def 9;
then reconsider p = Funcs(X,<*Y*>) as FinSequence by A1,FINSEQ_1:def 2;
<*Y*>.1 = Y & 1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then p.1 = Funcs(X,Y) by A1,FUNCT_6:def 9;
hence thesis by A2,A1,FINSEQ_1:def 8;
end;
theorem
Funcs(X,<*Y,Z*>) = <*Funcs(X,Y), Funcs(X,Z)*>
proof
A1: Seg len <*Y,Z*> = dom <*Y,Z*> by FINSEQ_1:def 3;
A2: dom Funcs(X,<*Y,Z*>) = dom <*Y,Z*> by FUNCT_6:def 9;
then reconsider p = Funcs(X,<*Y,Z*>) as FinSequence by A1,FINSEQ_1:def 2;
A3: len <*Y,Z*> = 2 by FINSEQ_1:44;
then
A4: len p = 2 by A2,A1,FINSEQ_1:def 3;
<*Y,Z*>.2 = Z & 2 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then
A5: p.2 = Funcs(X,Z) by A3,A1,FUNCT_6:def 9;
<*Y,Z*>.1 = Y & 1 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then p.1 = Funcs(X,Y) by A3,A1,FUNCT_6:def 9;
hence thesis by A4,A5,FINSEQ_1:44;
end;
::from JORDAN2C, 2011.07.03, A.T.
theorem
for f being FinSequence st rng f={x,y} & len f=2 holds
f.1=x & f.2=y or f.1=y & f.2=x
proof
let f be FinSequence;
assume that
A1: rng f={x,y} and
A2: len f=2;
2 in dom f by A2,Th25;
then
A3: f.2 in rng f by FUNCT_1:def 3;
A4: now
x in rng f by A1,TARSKI:def 2;
then consider z being object such that
A5: z in dom f and
A6: x=f.z by FUNCT_1:def 3;
reconsider nz=z as Element of NAT by A5;
A7: 1<=nz & nz<=len f by A5,Th25;
assume that
A8: f.1=y and
A9: f.2=y;
per cases by A2,A7,NAT_1:9;
suppose
nz=1;
hence f.1=x & f.2=y by A9,A6;
end;
suppose
nz=1+1;
hence f.1=x & f.2=y by A8,A9,A6;
end;
end;
A10: now
y in rng f by A1,TARSKI:def 2;
then consider z being object such that
A11: z in dom f and
A12: y=f.z by FUNCT_1:def 3;
reconsider nz=z as Element of NAT by A11;
A13: 1<=nz & nz<=len f by A11,Th25;
assume that
A14: f.1=x and
A15: f.2=x;
per cases by A2,A13,NAT_1:9;
suppose
nz=1;
hence f.1=x & f.2=y by A14,A15,A12;
end;
suppose
nz=1+1;
hence f.1=x & f.2=y by A14,A12;
end;
end;
1 in dom f by A2,Th25;
then f.1 in rng f by FUNCT_1:def 3;
hence thesis by A1,A3,A10,A4,TARSKI:def 2;
end;
:: from GLIB_001, 2011.07.30, A.T.
theorem
for X being set st X is included_in_Seg holds
for m,n being Element of NAT st m in dom Sgm X & n = (Sgm X).m holds m <= n
proof
let X be set;
defpred P[Nat] means ($1 in dom Sgm X & (ex n being Element of NAT st n=(
Sgm X).$1 & $1 <= n)) or (not $1 in dom Sgm X);
assume
A1: X is included_in_Seg;
now
let x be non zero Nat;
assume
A2: P[x];
now
per cases by A2;
suppose
A3: x in dom (Sgm X) & ex n being Element of NAT st n = (Sgm X).x & x <= n;
A4: x+0 < x+1 by XREAL_1:8;
consider n being Element of NAT such that
A5: n = Sgm(X).x and
A6: x <= n by A3;
A7: 1 <= x by A3,Th25;
now
set n1 = (Sgm X).(x+1);
assume
A8: x+1 in dom Sgm X;
then (Sgm X).(x+1) in rng Sgm X by FUNCT_1:3;
then reconsider n1 as Element of NAT;
take n1;
thus n1 = (Sgm X).(x+1);
x+1 <= len Sgm X by A8,Th25;
then n < n1 by A1,A7,A4,A5,FINSEQ_1:def 14;
then x < n1 by A6,XXREAL_0:2;
hence x+1 <= n1 by NAT_1:13;
end;
hence P[x+1];
end;
suppose
not x in dom (Sgm X);
then x < 0+1 or x > len Sgm X by Th25;
then x+1 > len Sgm X + 0 by NAT_1:13;
hence P[x+1] by Th25;
end;
end;
hence P[x+1];
end;
then
A9: for x being non zero Nat st P[x] holds P[x+1];
let m, n be Element of NAT;
assume that
A10: m in dom (Sgm X) and
A11: n = (Sgm X).m;
reconsider m9=m as non zero Element of NAT by A10,Th25;
now
set n = (Sgm X).1;
A12: m <= len (Sgm X) by A10,Th25;
1 <= m by A10,Th25;
then 1 <= len (Sgm X) by A12,XXREAL_0:2;
hence 1 in dom (Sgm X) by Th25;
then
A13: (Sgm X).1 in rng (Sgm X) by FUNCT_1:3;
then reconsider n as Element of NAT;
take n;
thus n = (Sgm X).1;
A15: ex k being Nat st X c= Seg k by A1,FINSEQ_1:def 13;
rng (Sgm X) = X by A1,FINSEQ_1:def 14;
hence 1 <= n by A13,A15,FINSEQ_1:1;
end;
then
A14: P[1];
for x being non zero Nat holds P[x] from NAT_1:sch 10(A14,A9);
then P[m9];
hence thesis by A10,A11;
end;
registration
let i be Nat; let D be finite set;
cluster i-tuples_on D -> finite;
coherence
proof
for x be object st x in dom (i |-> D) holds (i |-> D).x is finite
by FUNCOP_1:7; then
A1: i |-> D is finite-yielding by FINSET_1:def 4;
product (i |-> D) = i-tuples_on D by Th129;
hence thesis by A1;
end;
end;
theorem Th151:
for p being m-element FinSequence holds len p = m by CARD_1:def 7;
theorem
for p being n-element FinSequence, q being FinSequence
holds (p^q).1 = p.1 & ... & (p^q).n = p.n
proof let p be n-element FinSequence, q be FinSequence;
let k be Nat;
A1: len p = n by Th151;
assume 1 <= k & k <= n;
then k in dom p by A1,Th25;
hence (p^q).k = p.k by FINSEQ_1:def 7;
end;
reserve n for Nat;
theorem
for p being n-element FinSequence,
q being m-element FinSequence
holds (p^q).(n+(1 qua Nat)) = q.1 & ... & (p^q).(n+m) = q.m
proof let p be n-element FinSequence, q be m-element FinSequence;
A1: len p = n by Th151;
A2: len q = m by Th151;
let k be Nat;
assume 1 <= k & k <= m;
then
A3: n+(1 qua Nat) <= n+k & n+k <= n+m by XREAL_1:6;
thus (p^q).(n+k)= (p^q).(n+k)
.= q.(n+k-n) by A3,A1,A2,FINSEQ_1:23
.= q.k;
end;
theorem
for p being FinSequence, k being Nat st k in dom p
for i being Nat st 1 <= i & i <= k holds i in dom p
proof
let p be FinSequence, k be Nat;
assume
A1: k in dom p;
let i be Nat;
assume that
A2: 1 <= i and
A3: i <= k;
k <= len p by A1,Th25;
then i <= len p by A3,XXREAL_0:2;
hence thesis by A2,Th25;
end;
:: from PNPROC_1, 2012.02.20, A.T.
theorem
for q being FinSubsequence st q = {[i,x]} holds Seq q = <*x*>
proof
let q be FinSubsequence;
assume
A1: q = {[i,x]};
then [i,x] in q by TARSKI:def 1;
then
A2: i in dom q by XTUPLE_0:def 12;
ex k be Nat st dom q c= Seg k by FINSEQ_1:def 12;
then i >= 0 qua Nat+1 by A2,FINSEQ_1:1;
then
A3: i > 0;
then reconsider p = {[i,x]} as FinSubsequence by FINSEQ_1:96;
A4: Seq q = q* Sgm dom q by FINSEQ_1:def 15;
dom p = {i} by RELAT_1:9;
then Seq p = {[i,x]}*<*i*> by A1,A3,A4,Th42
.= <*{[i,x]}.i*> by A1,A2,FINSEQ_2:34
.= <*x*> by GRFUNC_1:6;
hence thesis by A1;
end;
theorem
for p being FinSubsequence holds card p = len Seq p
proof
let p be FinSubsequence;
A2: Seq p = p*(Sgm dom p) by FINSEQ_1:def 15;
A3: rng Sgm dom p = dom p by FINSEQ_1:50;
then
A4: dom Seq p = dom Sgm dom p by A2,RELAT_1:27;
rng Sgm dom p, dom Sgm dom p are_equipotent by WELLORD2:def 4;
then
A5: card dom p = card dom Sgm dom p by A3,CARD_1:5;
card dom p = card p by CARD_1:62;
hence thesis by A4,A5,CARD_1:62;
end;
theorem
for q being FinSubsequence st Seq q = <*x*>
ex i being Element of NAT st q = {[i,x]}
proof
let q be FinSubsequence;
assume Seq q = <*x*>;
then
A1: Seq q = {[1,x]} by FINSEQ_1:def 5;
then
A2: dom Seq q = {1} by RELAT_1:9;
A3: rng Seq q = {x} by A1,RELAT_1:9;
A4: Seq q = q* Sgm(dom q) by FINSEQ_1:def 15;
A5: rng Sgm(dom q) = dom q by FINSEQ_1:50;
then
A6: {1} = dom Sgm(dom q) by A2,A4,RELAT_1:27;
A7: rng Seq q = rng q by A4,A5,RELAT_1:28;
consider n being Nat such that
A8: dom q c= Seg n by FINSEQ_1:def 12;
Seg card dom q = {1} by A6,Th38;
then card dom q = card {1} by FINSEQ_1:57;
then consider y be object such that
A9: dom q = {y} by CARD_1:29;
y in dom q by A9,TARSKI:def 1;
then y in Seg n by A8;
then reconsider y as Element of NAT;
q = {[y,x]} by A3,A7,A9,RELAT_1:189;
hence thesis;
end;
:: suggested by SK, 15.11.2024
theorem Th1:
for p being FinSequence holds len disjoin p = len p
proof
let p be FinSequence;
dom disjoin p = dom p by CARD_3:def 3;
hence thesis by Th27;
end;
:: the case <*X*> is implicitly given by CARD_3:4
theorem
for X,Y being set holds disjoin <*X,Y*> = <*[:X,{1}:],[:Y,{2}:]*>
proof
let X,Y be set;
A1: len disjoin <*X,Y*> = len <*X,Y*> by Th1
.= 2 by FINSEQ_1:44;
then A2: len disjoin <*X,Y*> = len <*[:X,{1}:],[:Y,{2}:]*> by FINSEQ_1:44;
now
let k be Nat;
assume A3: 1 <= k & k <= len disjoin <*X,Y*>;
then 1 <= k & k <= len <*X,Y*> by Th1;
then A4: k in dom <*X,Y*> by Th25;
k = 1+0 or ... or k = 1+1 by A1, A3, NAT_1:62;
then per cases;
suppose A5: k = 1;
thus (disjoin <*X,Y*>).k = [:<*X,Y*>.k,{k}:] by A4, CARD_3:def 3
.= [:X,{1}:] by A5
.= <*[:X,{1}:],[:Y,{2}:]*>.k by A5;
end;
suppose A6: k = 2;
thus (disjoin <*X,Y*>).k = [:<*X,Y*>.k,{k}:] by A4, CARD_3:def 3
.= [:Y,{2}:] by A6
.= <*[:X,{1}:],[:Y,{2}:]*>.k by A6;
end;
end;
hence thesis by A2, FINSEQ_1:def 18;
end;
theorem
for X,Y,Z being set holds
disjoin <*X,Y,Z*> = <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*>
proof
let X,Y,Z be set;
A1: len disjoin <*X,Y,Z*> = len <*X,Y,Z*> by Th1
.= 3 by FINSEQ_1:45; then
A2: len disjoin <*X,Y,Z*> = len <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*>
by FINSEQ_1:45;
now
let k be Nat;
assume A3: 1 <= k & k <= len disjoin <*X,Y,Z*>;
then 1 <= k & k <= len <*X,Y,Z*> by Th1;
then A4: k in dom <*X,Y,Z*> by Th25;
k = 1+0 or ... or k = 1+2 by A1, A3, NAT_1:62;
then per cases;
suppose A5: k = 1;
thus (disjoin <*X,Y,Z*>).k = [:<*X,Y,Z*>.k,{k}:] by A4, CARD_3:def 3
.= [:X,{1}:] by A5
.= <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*>.k by A5;
end;
suppose A6: k = 2;
thus (disjoin <*X,Y,Z*>).k = [:<*X,Y,Z*>.k,{k}:] by A4, CARD_3:def 3
.= [:Y,{2}:] by A6
.= <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*>.k by A6;
end;
suppose A7: k = 3;
thus (disjoin <*X,Y,Z*>).k = [:<*X,Y,Z*>.k,{k}:] by A4, CARD_3:def 3
.= [:Z,{3}:] by A7
.= <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*>.k by A7;
end;
end;
hence thesis by A2, FINSEQ_1:def 18;
end;