finseq_3.miz
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 ::
FINSEQ_3:1
Th1: (
Seg 3)
=
{1, 2, 3}
proof
thus (
Seg 3)
= (
{1, 2}
\/
{(2
+ 1)}) by
FINSEQ_1: 2,
FINSEQ_1: 9
.=
{1, 2, 3} by
ENUMSET1: 3;
end;
theorem ::
FINSEQ_3:2
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 ::
FINSEQ_3:3
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 ::
FINSEQ_3:4
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 ::
FINSEQ_3:5
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 ::
FINSEQ_3:6
(
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 ::
FINSEQ_3:7
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 ::
FINSEQ_3:8
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 ::
FINSEQ_3:9
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 ::
FINSEQ_3:10
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 ::
FINSEQ_3:11
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 ::
FINSEQ_3:12
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 be
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 ::
FINSEQ_3:13
(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 ::
FINSEQ_3:14
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 ::
FINSEQ_3:15
((
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 ::
FINSEQ_3:16
(
Seg k)
<> (
Seg (k
+ 1)) by
Th8,
FINSEQ_1: 4;
theorem ::
FINSEQ_3:17
(
Seg k)
= (
Seg (k
+ n)) implies n
=
0 by
Th10,
FINSEQ_1: 3;
theorem ::
FINSEQ_3:18
Th18: (
Seg k)
c= (
Seg (k
+ n)) by
FINSEQ_1: 5,
NAT_1: 12;
theorem ::
FINSEQ_3:19
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 ::
FINSEQ_3:20
Th20: for y be
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 ::
FINSEQ_3:21
(
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 ::
FINSEQ_3:22
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 ::
FINSEQ_3:23
x
in (
dom p) implies x is
Element of
NAT ;
theorem ::
FINSEQ_3:24
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 ::
FINSEQ_3:25
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 ::
FINSEQ_3:26
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;
::$Canceled
theorem ::
FINSEQ_3:29
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 ::
FINSEQ_3:30
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 ::
FINSEQ_3:31
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 ::
FINSEQ_3:32
(
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 ::
FINSEQ_3:33
{}
<>
<*x, y*>;
theorem ::
FINSEQ_3:34
{}
<>
<*x, y, z*>;
theorem ::
FINSEQ_3:35
Th33:
<*x*>
<>
<*y, z*>
proof
(
len
<*x*>)
= 1 by
FINSEQ_1: 40;
hence thesis by
FINSEQ_1: 44;
end;
theorem ::
FINSEQ_3:36
<*u*>
<>
<*x, y, z*>
proof
(
len
<*u*>)
= 1 by
FINSEQ_1: 40;
hence thesis by
FINSEQ_1: 45;
end;
theorem ::
FINSEQ_3:37
<*u, v*>
<>
<*x, y, z*>
proof
(
len
<*u, v*>)
= 2 by
FINSEQ_1: 44;
hence thesis by
FINSEQ_1: 45;
end;
theorem ::
FINSEQ_3:38
Th36: (
len r)
= ((
len p)
+ (
len q)) & (for k be
Nat st k
in (
dom p) holds (r
. k)
= (p
. k)) & (for k be
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 be
Nat st k
in (
dom p) holds (r
. k)
= (p
. k) and
A3: for k be
Nat st k
in (
dom q) holds (r
. ((
len p)
+ k))
= (q
. k);
A4: for k be
Nat st k
in (
dom q) holds (r
. ((
len p)
+ k))
= (q
. k) by
A3;
for k be
Nat st k
in (
dom p) holds (r
. k)
= (p
. k) by
A2;
hence thesis by
A1,
A4,
FINSEQ_1:def 7;
end;
Lm1: A
c= (
Seg k) implies (
Sgm A) is
one-to-one
proof
assume
A1: A
c= (
Seg k);
then
A2: (
rng (
Sgm A))
= A by
FINSEQ_1:def 13;
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
A1,
A9,
A10,
FINSEQ_1:def 13;
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
A1,
A11,
A12,
FINSEQ_1:def 13;
hence contradiction by
A5;
end;
end;
hence thesis;
end;
theorem ::
FINSEQ_3:39
Th37: for A be
finite
set st A
c= (
Seg k) holds (
len (
Sgm A))
= (
card A)
proof
let A be
finite
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;
assume
A3: A
c= (
Seg k);
then
A4: (
rng (
Sgm A))
= A by
FINSEQ_1:def 13;
(
Sgm A) is
one-to-one by
A3,
Lm1;
then ((
Seg (
len (
Sgm A))),A)
are_equipotent by
A1,
A4;
hence thesis by
A2,
CARD_1: 5;
end;
theorem ::
FINSEQ_3:40
Th38: for A be
finite
set st A
c= (
Seg k) holds (
dom (
Sgm A))
= (
Seg (
card A))
proof
let A be
finite
set;
assume A
c= (
Seg k);
then (
len (
Sgm A))
= (
card A) by
Th37;
hence thesis by
FINSEQ_1:def 3;
end;
theorem ::
FINSEQ_3:41
Th39: X
c= (
Seg i) & k
< l & 1
<= n & m
<= (
len (
Sgm X)) & ((
Sgm X)
. m)
= k & ((
Sgm X)
. n)
= l implies m
< n
proof
assume that
A1: X
c= (
Seg i) 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 13;
end;
theorem ::
FINSEQ_3:42
Th40: X
c= (
Seg i) & Y
c= (
Seg j) implies ((for m,n be
Nat st m
in X & n
in Y holds m
< n) iff (
Sgm (X
\/ Y))
= ((
Sgm X)
^ (
Sgm Y)))
proof
assume that
A1: X
c= (
Seg i) and
A2: Y
c= (
Seg j);
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
A3: 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;
thus (for m,n be
Nat st m
in X & n
in Y holds m
< n) implies (
Sgm (X
\/ Y))
= ((
Sgm X)
^ (
Sgm Y))
proof
reconsider X1 = X, Y1 = Y as
finite
set by
A1,
A2;
defpred
P[
Nat] means $1
in (
dom p) implies (r
. $1)
= (p
. $1);
assume
A5: for m,n be
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 13;
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,
A3,
Th37,
XBOOLE_1: 8
.= ((
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 13;
(
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 ;
A18: m
in (X
\/ Y) by
A4,
A17,
FINSEQ_1:def 13;
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 13;
then
consider x be
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
A4,
A12,
A21,
A28,
A27,
FINSEQ_1:def 13;
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
A4,
FINSEQ_1:def 13;
then
consider x be
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
A1,
A2,
A3,
A31,
A34,
A32,
Th39,
XBOOLE_1: 8;
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 13;
A39: k
<= (
len r) by
A16,
A21,
Th25;
1
<= x by
A33,
Th25;
then k
< x by
A1,
A2,
A3,
A34,
A38,
A39,
Th39,
XBOOLE_1: 8;
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 13;
then
consider x be
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
A4,
FINSEQ_1:def 13;
then
consider x be
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
A1,
A2,
A3,
A47,
A50,
A48,
Th39,
XBOOLE_1: 8;
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 be
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 13;
then
consider x be
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
A1,
A2,
A3,
Lm1,
XBOOLE_1: 8;
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 13;
assume
A68: (r
. ((
len p)
+ (k
+ 1)))
<> (q
. (k
+ 1));
A69: m
in (X
\/ Y) by
A4,
A59,
FINSEQ_1:def 13;
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 13;
then
consider x be
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
A4,
A54,
A56,
A70,
A71,
FINSEQ_1:def 13;
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
A4,
FINSEQ_1:def 13;
then
consider x be
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,
A3,
A80,
A83,
A81,
Th39,
XBOOLE_1: 8;
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 13;
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,
A3,
A83,
A87,
A88,
Th39,
XBOOLE_1: 8;
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 13;
then
consider x be
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
A4,
FINSEQ_1:def 13;
then
consider x be
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,
A3,
A91,
A96,
A99,
A97,
Th39,
XBOOLE_1: 8;
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 13;
hence contradiction by
A5,
A67;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
end;
A103:
P[
0 ] by
Th24;
for k be
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 13;
then
consider y be
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 13;
then
consider x be
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
A4,
A109,
A114,
A116,
A110,
FINSEQ_1:def 13;
end;
theorem ::
FINSEQ_3:43
Th41: (
Sgm
{} )
=
{}
proof
{}
c= (
Seg
0 );
hence thesis by
FINSEQ_1: 51;
end;
theorem ::
FINSEQ_3:44
Th42:
0
<> n implies (
Sgm
{n})
=
<*n*>
proof
assume
0
<> n;
then n
in (
Seg n) by
FINSEQ_1: 3;
then
A1:
{n}
c= (
Seg n) by
ZFMISC_1: 31;
then (
len (
Sgm
{n}))
= (
card
{n}) by
Th37;
then
A2: (
len (
Sgm
{n}))
= 1 by
CARD_1: 30;
(
rng (
Sgm
{n}))
=
{n} by
A1,
FINSEQ_1:def 13;
hence thesis by
A2,
FINSEQ_1: 39;
end;
theorem ::
FINSEQ_3:45
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
A5:
{n, m}
c= (
Seg m) by
A3,
A4,
ZFMISC_1: 32;
then
A6: (
Sgm
{n, m}) is
one-to-one by
Lm1;
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,
FINSEQ_1: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 13;
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 13;
end;
end;
hence thesis by
A7,
FINSEQ_1: 44;
end;
theorem ::
FINSEQ_3:46
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 13;
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 be
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 13;
n
<= k by
A13,
FINSEQ_1: 1;
hence contradiction by
A16,
A10,
XXREAL_0: 2;
end;
A17: Y is
one-to-one by
Lm1;
(
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 be
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 be
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, l, m;
assume that
A34: 1
<= i and
A35: i
< j and
A36: j
<= (
len p) and
A37: l
= (p
. i) and
A38: 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,
A37,
A38,
A39,
A40,
FINSEQ_1:def 13;
end;
hence thesis by
A32,
FINSEQ_1:def 13;
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 ::
FINSEQ_3:47
((
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 13;
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 by
Lm1;
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 ::
FINSEQ_3:48
Th46: (
Sgm (
Seg k))
= (
idseq k)
proof
defpred
P[
Nat] means (
Sgm (
Seg $1))
= (
idseq $1);
A1: for k be
Nat st
P[k] holds
P[(k
+ 1)] by
Lm5;
A2:
P[
0 ] by
Th41;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A2,
A1);
hence thesis;
end;
theorem ::
FINSEQ_3:49
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 be
object st x
in (
dom p) holds (p
. x)
= (p
. x);
hence thesis by
A1,
FUNCT_1: 46;
end;
theorem ::
FINSEQ_3:50
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 ::
FINSEQ_3:51
((
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 be
Nat st n
= (m
+ j) by
NAT_1: 10;
hence thesis by
Th48;
end;
theorem ::
FINSEQ_3:52
((
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 ::
FINSEQ_3:53
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 ::
FINSEQ_3:54
(
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 ::
FINSEQ_3:55
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 be
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,
FINSEQ_1: 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,
FINSEQ_1: 40;
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 ::
FINSEQ_3:56
(p
| X) is
FinSequence iff ex k be
Element of
NAT st (X
/\ (
dom p))
= (
Seg k)
proof
thus (p
| X) is
FinSequence implies ex k be
Element of
NAT st (X
/\ (
dom p))
= (
Seg k)
proof
assume (p
| X) is
FinSequence;
then
consider k be
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 be
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 ::
FINSEQ_3:57
Th55: (
card ((p
^ q)
" A))
= ((
card (p
" A))
+ (
card (q
" A)))
proof
set X = ((p
^ q)
" A);
set B = { ((
len p)
+ n) where n be
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 be
Nat st m
in (
dom q) & k
= ((
len p)
+ m);
then
consider m be
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 be
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 be
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 be
object st x
in (q
" A) holds ex y be
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 be
Function such that
A23: (
dom f)
= (q
" A) and
A24: for x be
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 be
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 be
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 ::
FINSEQ_3:58
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;
::
FINSEQ_3:def1
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 ;
((
Seg (
len p))
\ (p
" A))
c= (
Seg (
len p)) by
XBOOLE_1: 36;
then (
rng (
Sgm ((
Seg (
len p))
\ (p
" A))))
c= D by
FINSEQ_1:def 13;
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 ::
FINSEQ_3:59
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 13;
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,
XBOOLE_1: 36;
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 ::
FINSEQ_3:60
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 ::
FINSEQ_3:61
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 ::
FINSEQ_3:62
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 ::
FINSEQ_3:63
(
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 ::
FINSEQ_3:64
(
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 ::
FINSEQ_3:65
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;
A2: (
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
A6: ((
Seg (
len p))
\ (p
" A))
c= (
Seg (
len p)) by
XBOOLE_1: 36;
assume
A7: x
in A;
consider y be
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
A2,
A8,
FUNCT_1: 11;
then
A11: ((p
- A)
. y)
= (p
. z) by
A2,
FUNCT_1: 13;
z
in (
rng q) by
A10,
FUNCT_1:def 3;
then z
in ((
Seg (
len p))
\ (p
" A)) by
A6,
FINSEQ_1:def 13;
then
A12: not z
in (p
" A) by
XBOOLE_0:def 5;
z
in (
dom p) by
A2,
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 be
object such that
A14: y
in (
dom p) and
A15: (p
. y)
= x by
FUNCT_1:def 3;
((
Seg (
len p))
\ (p
" A))
c= (
Seg (
len p)) by
XBOOLE_1: 36;
then
A16: (
rng q)
= ((
Seg (
len p))
\ (p
" A)) by
FINSEQ_1:def 13;
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 be
object such that
A17: z
in (
dom q) and
A18: (q
. z)
= y by
FUNCT_1:def 3;
A19: ((p
- A)
. z)
= x by
A2,
A15,
A17,
A18,
FUNCT_1: 13;
z
in (
dom (p
- A)) by
A2,
A14,
A17,
A18,
FUNCT_1: 11;
hence thesis by
A19,
FUNCT_1:def 3;
end;
theorem ::
FINSEQ_3:66
(
rng (p
- A))
c= (
rng p)
proof
(
rng (p
- A))
= ((
rng p)
\ A) by
Th63;
hence thesis;
end;
theorem ::
FINSEQ_3:67
(
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 ::
FINSEQ_3:68
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 ::
FINSEQ_3:69
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 ::
FINSEQ_3:70
(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 be
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 ::
FINSEQ_3:71
(p
-
{} )
= p
proof
{}
misses (
rng p);
hence thesis by
Th67;
end;
theorem ::
FINSEQ_3:72
(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 be
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;
A2:
now
(t
" A)
c= (
dom t) by
RELAT_1: 132;
then
A3: (t
" A)
c= (
Seg (
len t)) by
FINSEQ_1:def 3;
set S = ((
Seg (
len (p
^
<*x*>)))
\ ((p
^
<*x*>)
" A));
set s = (
Sgm ((
Seg (
len (p
^
<*x*>)))
\ ((p
^
<*x*>)
" A)));
let k be
Nat;
A4: S
c= (
Seg (
len t)) by
XBOOLE_1: 36;
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,
FINSEQ_1: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 be
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
A4,
FINSEQ_1:def 13;
then
consider y be
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,
XBOOLE_1: 36
.= ((
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
A4,
A31,
FINSEQ_1:def 13;
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
A4,
A25,
A35,
FINSEQ_1:def 13;
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,
FINSEQ_1:def 8;
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,
XBOOLE_1: 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,
XBOOLE_1: 36
.= ((
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;
((
Seg (
len t))
\ (t
" A))
c= (
Seg (
len t)) by
XBOOLE_1: 36;
then
A71: (
rng s1)
c= (
Seg (
len t)) by
FINSEQ_1:def 13;
A72: ((
Seg (
len p))
\ (p
" A))
c= (
Seg (
len p)) by
XBOOLE_1: 36;
then
A73: (
rng s2)
c= (
Seg (
len p)) by
FINSEQ_1:def 13;
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,
XBOOLE_1: 36
.= ((
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,
FINSEQ_1: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;
((
len p)
+ 1)
in (
Seg ((
len p)
+ 1)) by
FINSEQ_1: 4;
then
A85:
{((
len p)
+ 1)}
c= (
Seg ((
len p)
+ 1)) by
ZFMISC_1: 31;
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
A72,
A85,
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 be
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 ::
FINSEQ_3:73
((p
^ q)
- A)
= ((p
- A)
^ (q
- A)) by
Lm11;
theorem ::
FINSEQ_3:74
(
{}
- A)
=
{} ;
theorem ::
FINSEQ_3:75
(
<*x*>
- A)
=
<*x*> iff not x
in A by
Lm6;
theorem ::
FINSEQ_3:76
(
<*x*>
- A)
=
{} iff x
in A by
Lm7;
theorem ::
FINSEQ_3:77
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 ::
FINSEQ_3:78
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 ::
FINSEQ_3:79
(
<*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 by
FINSEQ_1: 40;
<*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,
FINSEQ_1:def 9;
hence thesis by
A2,
A8,
Th33,
FINSEQ_1: 40;
end;
theorem ::
FINSEQ_3:80
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 ::
FINSEQ_3:81
(
<*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 by
FINSEQ_1: 40;
<*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,
FINSEQ_1:def 9;
hence thesis by
A2,
A8,
Th33,
FINSEQ_1: 40;
end;
theorem ::
FINSEQ_3:82
(
<*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 ::
FINSEQ_3:83
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 ::
FINSEQ_3:84
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 holds for n st n
in (
dom p) holds for B be
finite
set st B
= { k where k be
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) holds for n st n
in (
dom p) holds for C be
finite
set st C
= { m where m be
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 holds for n st n
in (
dom p) holds for B be
finite
set st B
= { k where k be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 holds for p, A st (
len p)
= l holds for n st n
in (
dom p) holds for B be
finite
set st B
= { k where k be
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 holds for n st n
in (
dom p) holds for B be
finite
set st B
= { k where k be
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 be
Nat st
P[k] holds
P[(k
+ 1)] by
Lm12;
for n be
Nat holds
P[n] from
NAT_1:sch 2(
A1,
A2);
hence thesis;
end;
theorem ::
FINSEQ_3:85
n
in (
dom p) implies for B be
finite
set st B
= { k where k be
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 ::
FINSEQ_3:86
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 ::
FINSEQ_3:87
p is
one-to-one implies (p
- A) is
one-to-one
proof
assume
A1: p is
one-to-one;
A2: (p
- A)
= (p
* (
Sgm ((
Seg (
len p))
\ (p
" A)))) by
FINSEQ_1:def 3;
(
Sgm ((
Seg (
len p))
\ (p
" A))) is
one-to-one by
Lm1,
XBOOLE_1: 36;
hence thesis by
A1,
A2;
end;
theorem ::
FINSEQ_3:88
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 be
Function such that
A3: (
dom f)
= (p
" A) and
A4: for x be
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 be
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 be
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 ::
FINSEQ_3:89
Th87: for A be
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 ::
FINSEQ_3:90
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 ::
FINSEQ_3:91
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 be
Nat st n
in (
dom q) & k2
= ((
len p)
+ n);
then
consider n be
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 be
Nat st n
in (
dom q) & k1
= ((
len p)
+ n);
then
consider n be
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 be
Nat st n
in (
dom q) & k1
= ((
len p)
+ n)) & ex n be
Nat st n
in (
dom q) & k2
= ((
len p)
+ n);
then
consider n2 be
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 be
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 be
object such that
A26: x
in (
rng p) and
A27: x
in (
rng q) by
XBOOLE_0: 3;
consider y1 be
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 be
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 be
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 be
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 ::
FINSEQ_3:92
Th90: A
c= (
Seg k) implies (
Sgm A) is
one-to-one by
Lm1;
theorem ::
FINSEQ_3:93
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,
FINSEQ_1:def 8;
then
A3: y1
= 1 by
TARSKI:def 1;
y2
in
{1} by
A2,
FINSEQ_1: 2,
FINSEQ_1:def 8;
hence thesis by
A3,
TARSKI:def 1;
end;
theorem ::
FINSEQ_3:94
Th92: x
<> y iff
<*x, y*> is
one-to-one
proof
A1: (
<*x, y*>
. 2)
= y by
FINSEQ_1: 44;
2
in
{1, 2} by
TARSKI:def 2;
then
A2: 2
in (
dom
<*x, y*>) by
FINSEQ_1: 2,
FINSEQ_1: 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,
FINSEQ_1: 89;
A8: y1
in
{1, 2} by
A4,
FINSEQ_1: 2,
FINSEQ_1: 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;
then (
<*x, y*>
. y1)
= x by
FINSEQ_1: 44;
hence thesis by
A3,
A6,
A9,
FINSEQ_1: 44;
end;
suppose
A10: y1
= 2 & y2
= 1;
then (
<*x, y*>
. y1)
= y by
FINSEQ_1: 44;
hence thesis by
A3,
A6,
A10,
FINSEQ_1: 44;
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,
FINSEQ_1: 89;
(
<*x, y*>
. 1)
= x by
FINSEQ_1: 44;
hence thesis by
A11,
A12,
A13,
A2,
A1;
end;
theorem ::
FINSEQ_3:95
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 by
FINSEQ_1: 45;
A2: (p
. 3)
= z by
FINSEQ_1: 45;
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 by
FINSEQ_1: 45;
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 ::
FINSEQ_3:96
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 ::
FINSEQ_3:97
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 ::
FINSEQ_3:98
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 ::
FINSEQ_3:99
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,
FINSEQ_1: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 ::
FINSEQ_3:100
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 ::
FINSEQ_3:101
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
theorem ::
FINSEQ_3:102
for D be non
empty
set, df be
FinSequence of D holds df is non
empty implies ex d be
Element of D, df1 be
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 be
FinSequence such that
A2: (
len dta)
= lend1 and
A3: for j be
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 be
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 ::
FINSEQ_3:103
for df be
FinSequence, d be
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;
definition
let i be
natural
Number;
let p be
FinSequence;
::
FINSEQ_3:def2
func
Del (p,i) ->
FinSequence equals (p
* (
Sgm ((
dom p)
\
{i})));
coherence
proof
set q = (
Sgm ((
dom p)
\
{i}));
A1: ((
Seg (
len p))
\
{i})
c= (
Seg (
len p)) by
XBOOLE_1: 36;
(
dom p)
= (
Seg (
len p)) by
FINSEQ_1:def 3;
then (
rng q)
c= (
dom p) by
A1,
FINSEQ_1:def 13;
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 ::
FINSEQ_3:104
Th102: for p be
FinSequence holds (i
in (
dom p) implies ex m be
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;
for x be
object holds x
in ((
Seg (
len p))
\
{i}) implies x
in (
Seg (
len p)) by
XBOOLE_0:def 5;
then
A4: ((
Seg (
len p))
\
{i})
c= (
Seg (
len p));
then (
rng (
Sgm ((
Seg (
len p))
\
{i})))
c= (
Seg (
len p)) by
FINSEQ_1:def 13;
then
reconsider q = (
Sgm ((
dom p)
\
{i})) as
FinSequence of D9 by
A3,
FINSEQ_1:def 4;
p
<>
{} by
A2;
then
consider m be
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 be
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
A4,
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 be
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 ::
FINSEQ_3:105
for D be non
empty
set holds for p be
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 be
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 13;
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;
theorem ::
FINSEQ_3:106
for p be
FinSequence holds (
rng (
Del (p,i)))
c= (
rng p) by
FUNCT_1: 14;
theorem ::
FINSEQ_3:107
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,
XBOOLE_1: 36;
end;
reserve J for
Nat;
theorem ::
FINSEQ_3:108
Th106: for i,k,m,n be
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 be
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
<= $1 implies ((
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 be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
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;
then
A14: (
rng (
Sgm X))
= X by
FINSEQ_1:def 13;
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 be
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 be
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 be
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
A13,
A10,
A39,
A41,
FINSEQ_1:def 13;
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 be
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
A66:
{g}
c= (
Seg g) by
A13;
Y
c= X by
A52,
XBOOLE_1: 7;
then Y
c= (
Seg g) by
A13;
then
A67: (
Sgm X)
= ((
Sgm Y)
^ (
Sgm
{g})) by
A52,
A48,
A66,
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 be
Nat holds
P[k] from
NAT_1:sch 2(
A76,
A4);
hence thesis by
A1,
A2,
A3;
end;
theorem ::
FINSEQ_3:109
Th107: for f be
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 be
Nat st (
len f)
= (k
+ 1) & (
len (
Del (f,n)))
= k by
A2,
Th102;
hence thesis by
A1;
end;
theorem ::
FINSEQ_3:110
for f be
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 be
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;
X
c= (
Seg (
len f)) by
A7,
XBOOLE_1: 36;
then (
rng (
Sgm X))
= X by
FINSEQ_1:def 13;
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 ::
FINSEQ_3:111
for f be
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;
then X
c= (
Seg (
len f)) by
XBOOLE_1: 36;
then (
rng (
Sgm X))
= X by
FINSEQ_1:def 13;
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;
theorem ::
FINSEQ_3:112
Th110: for f be
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 15;
end;
end;
theorem ::
FINSEQ_3:113
for p,q be
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 be
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;
theorem ::
FINSEQ_3:114
Th112: for A be
set, F be
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));
A5: (F
" ((
rng F)
\ A))
c= (
dom F) by
RELAT_1: 132;
then
A6: (F
" ((
rng F)
\ A))
c= (
Seg (
len F)) by
FINSEQ_1:def 3;
then
A7: (
Sgm (F
" ((
rng F)
\ A))) is
one-to-one by
Lm1;
A8: (F
" A)
c= (
dom F) by
RELAT_1: 132;
then
A9: (F
" A)
c= (
Seg (
len F)) by
FINSEQ_1:def 3;
then ((
rng (
Sgm (F
" A)))
/\ (
rng (
Sgm (F
" ((
rng F)
\ A)))))
= ((F
" A)
/\ (
rng (
Sgm (F
" ((
rng F)
\ A))))) by
FINSEQ_1:def 13
.=
{} by
A6,
A3,
FINSEQ_1:def 13;
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 13
.= ((F
" A)
\/ (F
" ((
rng F)
\ A))) by
A6,
FINSEQ_1:def 13
.= (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;
(
Sgm (F
" A)) is
one-to-one by
A9,
Lm1;
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
A1,
A8,
A5,
Th37,
XBOOLE_1: 8
.= (
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 ::
FINSEQ_3:115
for F be
FinSequence, A be
Subset of (
rng F) holds ex p be
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
A6: (F
" (
rng F1))
c= (
Seg (
len F)) by
FINSEQ_1:def 3;
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 (
len (
Sgm (F
" (
rng F2))))
= (
card (F
" (
rng F2))) by
Th37,
RELAT_1: 132
.= (
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
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;
theorem ::
FINSEQ_3:116
for f be
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 14
.= (f
* (
idseq k)) by
Th46
.= f by
A2,
FINSEQ_2: 54;
hence thesis;
end;
theorem ::
FINSEQ_3:117
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;
theorem ::
FINSEQ_3:118
(
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;
theorem ::
FINSEQ_3:119
Th117: for A be
set, i be
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 be
Element of (A
* ) : (
len s)
= i } & p
in B;
then ex s be
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;
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 be
Element of (D
* ) st f
= s & (
len s)
= i by
A1;
ex s be
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 be
Function such that
A2: x
= g and
A3: (
dom g)
= (
dom (
product" S)) and
A4: for z be
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 be
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 be
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 be
Function such that
A11: f
in S and
A12: (g
. a)
= (f
. a) by
CARD_3:def 6;
consider w be
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
A14: (w
. a)
in (
rng w) by
A9,
FUNCT_1:def 3;
thus thesis by
A10,
A12,
A13,
A14;
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
reserve n for
Nat;
theorem ::
FINSEQ_3:120
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 be
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;
::
FINSEQ_3:def3
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 ::
FINSEQ_3:121
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;
::
FINSEQ_3:def4
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 ::
FINSEQ_3:122
for D be non
empty
set, R be
Equivalence_Relation of D, y be
FinSequence of (
Class R) holds 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) holds 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 be
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;
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 ::
FINSEQ_3:123
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 by
FINSEQ_1:def 8;
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 be
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
A2,
A7,
FINSEQ_1:def 8;
end;
(
dom
<*y*>)
= (
Seg 1) by
FINSEQ_1:def 8;
hence thesis by
A1,
A8,
A9,
CARD_3:def 5;
end;
theorem ::
FINSEQ_3:124
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 by
FINSEQ_1: 44;
(
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 be
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
A1,
A7,
FINSEQ_1: 44;
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 ::
FINSEQ_3:125
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 by
FINSEQ_1: 45;
A3: (
<*X, Y, Z*>
. 3)
= Z by
FINSEQ_1: 45;
(
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 be
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
A2,
A3,
A9,
FINSEQ_1: 45;
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 ::
FINSEQ_3:126
(
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 ::
FINSEQ_3:127
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 ::
FINSEQ_3:128
(
product
<*D, D*>)
= (2
-tuples_on D)
proof
thus (
product
<*D, D*>)
= the set of all
<*d1, d2*> where d1 be
Element of D, d2 be
Element of D by
Th125
.= (2
-tuples_on D) by
FINSEQ_2: 99;
end;
theorem ::
FINSEQ_3:129
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 ::
FINSEQ_3:130
(
product
<*D, D, D*>)
= (3
-tuples_on D)
proof
thus (
product
<*D, D, D*>)
= the set of all
<*d1, d2, d3*> where d1 be
Element of D, d2 be
Element of D, d3 be
Element of D by
Th127
.= (3
-tuples_on D) by
FINSEQ_2: 102;
end;
theorem ::
FINSEQ_3:131
Th129: for D be
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,
FINSEQ_1: 38;
then x
= 1 by
TARSKI:def 1;
hence thesis by
FINSEQ_1: 40;
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,
FINSEQ_1: 89;
then x
= 1 or x
= 2 by
TARSKI:def 2;
hence thesis by
FINSEQ_1: 44;
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 by
FINSEQ_1: 45;
end;
end
theorem ::
FINSEQ_3:132
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 by
FINSEQ_1: 40;
A3: (
dom
<*f*>)
= (
Seg 1) &
{f}
=
{f} by
FINSEQ_1: 38;
A4: (
<*(
rng f)*>
. 1)
= (
rng f) by
FINSEQ_1: 40;
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,
A4,
A3,
A6,
FINSEQ_1: 2,
FUNCT_6:def 3;
end;
A7: (
<*(
dom f)*>
. 1)
= (
dom f) by
FINSEQ_1: 40;
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,
A7,
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 ::
FINSEQ_3:133
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 by
FINSEQ_1: 44;
A3: (
dom
<*f, g*>)
= (
Seg 2) &
{f, g}
=
{f, g} by
FINSEQ_1: 89;
A4: (
<*(
rng f), (
rng g)*>
. 1)
= (
rng f) & (
<*(
rng f), (
rng g)*>
. 2)
= (
rng g) by
FINSEQ_1: 44;
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,
A4,
A3,
A6,
FINSEQ_1: 2,
FUNCT_6:def 3;
end;
A7: (
<*(
dom f), (
dom g)*>
. 1)
= (
dom f) & (
<*(
dom f), (
dom g)*>
. 2)
= (
dom g) by
FINSEQ_1: 44;
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,
A7,
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 ::
FINSEQ_3:134
(
doms
<*f, g, h*>)
=
<*(
dom f), (
dom g), (
dom h)*> & (
rngs
<*f, g, h*>)
=
<*(
rng f), (
rng g), (
rng h)*>
proof
A1: (
<*(
rng f), (
rng g), (
rng h)*>
. 3)
= (
rng h) by
FINSEQ_1: 45;
A2: (
<*f, g, h*>
. 1)
= f & (
<*f, g, h*>
. 2)
= g by
FINSEQ_1: 45;
A3: (
<*f, g, h*>
. 3)
= h by
FINSEQ_1: 45;
A4: (
dom
<*f, g, h*>)
= (
Seg 3) &
{f, g, h}
=
{f, g, h} by
FINSEQ_1: 89;
A5: (
<*(
rng f), (
rng g), (
rng h)*>
. 1)
= (
rng f) & (
<*(
rng f), (
rng g), (
rng h)*>
. 2)
= (
rng g) by
FINSEQ_1: 45;
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,
A5,
A1,
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;
A9: (
<*(
dom f), (
dom g), (
dom h)*>
. 3)
= (
dom h) by
FINSEQ_1: 45;
A10: (
<*(
dom f), (
dom g), (
dom h)*>
. 1)
= (
dom f) & (
<*(
dom f), (
dom g), (
dom h)*>
. 2)
= (
dom g) by
FINSEQ_1: 45;
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,
A10,
A9,
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 ::
FINSEQ_3:135
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 ::
FINSEQ_3:136
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 ::
FINSEQ_3:137
(
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,
ZFMISC_1: 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,
SETFAM_1: 11;
hence thesis by
A4,
A3,
FINSEQ_2: 128;
end;
theorem ::
FINSEQ_3:138
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,
FINSEQ_1: 45,
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 by
FINSEQ_1: 44,
FINSEQ_1:def 8;
hence thesis by
A1,
A3,
A2,
A4,
FUNCT_5: 38;
end;
theorem ::
FINSEQ_3:139
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 by
FINSEQ_1: 44,
FINSEQ_1: 45;
hence thesis by
A1,
A2,
FUNCT_5: 38;
end;
theorem ::
FINSEQ_3:140
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,
FINSEQ_1: 45;
hence thesis by
A1,
FUNCT_5: 38;
end;
theorem ::
FINSEQ_3:141
(
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 be
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,
FINSEQ_1: 40;
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 ::
FINSEQ_3:142
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 be
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,
FINSEQ_1: 44,
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,
FINSEQ_1: 44,
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 ::
FINSEQ_3:143
(
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 by
FINSEQ_1:def 8;
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,
FUNCT_6: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,
FINSEQ_1: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;
A8: (
<*x*>
. 1)
= x by
FINSEQ_1:def 8;
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,
A8,
FINSEQ_1:def 8;
end;
theorem ::
FINSEQ_3:144
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,
FUNCT_6: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;
A7: (
<*x, y*>
. 1)
= x & (
<*x, y*>
. 2)
= y by
FINSEQ_1: 44;
A8: 1
in (
Seg 2) & (
<*f1, f2*>
. 1)
= f1 by
FINSEQ_1: 2,
FINSEQ_1: 44,
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,
FINSEQ_1: 44,
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,
A7,
FINSEQ_1: 44;
end;
theorem ::
FINSEQ_3:145
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) by
FINSEQ_1: 44;
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 by
FINSEQ_1: 44;
[(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 ::
FINSEQ_3:146
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) by
FINSEQ_1: 44;
A3: (
<*y1, y2*>
. 1)
= y1 & (
<*y1, y2*>
. 2)
= y2 by
FINSEQ_1: 44;
[(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 ::
FINSEQ_3:147
(
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,
FINSEQ_1:def 8,
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 ::
FINSEQ_3:148
(
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,
FINSEQ_1: 44,
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,
FINSEQ_1: 44,
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 ::
FINSEQ_3:149
(
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,
FINSEQ_1:def 8,
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 ::
FINSEQ_3:150
(
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,
FINSEQ_1: 44,
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,
FINSEQ_1: 44,
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;
theorem ::
FINSEQ_3:151
for f be
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 be
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 be
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;
theorem ::
FINSEQ_3:152
for X be
set, k be
Element of
NAT st X
c= (
Seg k) holds for m,n be
Element of
NAT st m
in (
dom (
Sgm X)) & n
= ((
Sgm X)
. m) holds m
<= n
proof
let X be
set, k be
Element of
NAT ;
defpred
P[
Nat] means ($1
in (
dom (
Sgm X)) & (ex n be
Element of
NAT st n
= ((
Sgm X)
. $1) & $1
<= n)) or ( not $1
in (
dom (
Sgm X)));
assume
A1: X
c= (
Seg k);
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 be
Element of
NAT st n
= ((
Sgm X)
. x) & x
<= n;
A4: (x
+
0 )
< (x
+ 1) by
XREAL_1: 8;
consider n be
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 13;
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 be 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);
(
rng (
Sgm X))
= X by
A1,
FINSEQ_1:def 13;
hence 1
<= n by
A1,
A13,
FINSEQ_1: 1;
end;
then
A14:
P[1];
for x be 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 ::
FINSEQ_3:153
Th151: for p be m
-element
FinSequence holds (
len p)
= m by
CARD_1:def 7;
theorem ::
FINSEQ_3:154
for p be n
-element
FinSequence, q be
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 ::
FINSEQ_3:155
for p be n
-element
FinSequence, q be 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 ::
FINSEQ_3:156
for p be
FinSequence, k be
Nat st k
in (
dom p) holds for i be
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;
theorem ::
FINSEQ_3:157
for q be
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 14;
(
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 ::
FINSEQ_3:158
for p be
FinSubsequence holds (
card p)
= (
len (
Seq p))
proof
let p be
FinSubsequence;
A1: ex k be
Nat st ((
dom p)
c= (
Seg k)) by
FINSEQ_1:def 12;
A2: (
Seq p)
= (p
* (
Sgm (
dom p))) by
FINSEQ_1:def 14;
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;
(
Sgm (
dom p)) is
one-to-one by
A1,
Th90;
then ((
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 ::
FINSEQ_3:159
for q be
FinSubsequence st (
Seq q)
=
<*x*> holds ex i be
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 14;
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 be
Nat such that
A8: (
dom q)
c= (
Seg n) by
FINSEQ_1:def 12;
(
Seg (
card (
dom q)))
=
{1} by
A6,
A8,
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;