finseq_1.miz
begin
reserve a for
natural
Number,
k,l,m,n,k1,b,c,i for
Nat,
x,y,z,y1,y2 for
object,
X,Y for
set,
f,g for
Function;
definition
let n be
natural
Number;
::
FINSEQ_1:def1
func
Seg n ->
set equals { k where k be
Nat : 1
<= k & k
<= n };
correctness ;
end
definition
let n be
Nat;
:: original:
Seg
redefine
func
Seg n ->
Subset of
NAT ;
coherence
proof
set X = (
Seg n);
X
c=
NAT
proof
let x be
object;
assume x
in X;
then ex k be
Nat st x
= k & 1
<= k & k
<= n;
hence thesis by
ORDINAL1:def 12;
end;
hence thesis;
end;
end
theorem ::
FINSEQ_1:1
Th1: for a,b be
natural
Number holds a
in (
Seg b) iff 1
<= a & a
<= b
proof
let a,b be
natural
Number;
A1: a is
Nat & b is
Nat by
TARSKI: 1;
a
in { m where m be
Nat : 1
<= m & m
<= b } iff ex m be
Nat st a
= m & 1
<= m & m
<= b;
hence thesis by
A1;
end;
registration
let n be
zero
natural
Number;
cluster (
Seg n) ->
empty;
coherence
proof
assume not (
Seg n) is
empty;
then
consider x be
object such that
A1: x
in (
Seg n);
ex k be
Nat st k
= x & 1
<= k & k
<=
0 by
A1;
hence contradiction;
end;
end
theorem ::
FINSEQ_1:2
Th2: (
Seg 1)
=
{1} & (
Seg 2)
=
{1, 2}
proof
now
let x be
object;
thus x
in (
Seg 1) implies x
in
{1}
proof
assume x
in (
Seg 1);
then
consider k be
Nat such that
A1: x
= k and
A2: 1
<= k & k
<= 1;
k
= 1 by
A2,
XXREAL_0: 1;
hence thesis by
A1,
TARSKI:def 1;
end;
assume x
in
{1};
then x
= 1 by
TARSKI:def 1;
hence x
in (
Seg 1);
end;
hence (
Seg 1)
=
{1} by
TARSKI: 2;
now
let x be
object;
thus x
in (
Seg 2) implies x
in
{1, 2}
proof
assume x
in (
Seg 2);
then
consider k be
Nat such that
A3: x
= k and
A4: 1
<= k and
A5: k
<= 2;
k
<= (1
+ 1) by
A5;
then k
= 1 or k
= 2 by
A4,
NAT_1: 9;
hence thesis by
A3,
TARSKI:def 2;
end;
assume x
in
{1, 2};
then x
= 1 or x
= 2 by
TARSKI:def 2;
hence x
in (
Seg 2);
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
FINSEQ_1:3
Th3: for a be
natural
Number holds a
=
0 or a
in (
Seg a)
proof
let a be
natural
Number;
assume a
<>
0 ;
then ex b be
Nat st a
= (b
+ 1) by
NAT_1: 6;
then a
in
NAT & 1
<= a by
NAT_1: 11;
hence thesis;
end;
registration
let n be non
zero
natural
Number;
cluster (
Seg n) -> non
empty;
coherence by
Th3;
end
theorem ::
FINSEQ_1:4
for a be
natural
Number holds (a
+ 1)
in (
Seg (a
+ 1)) by
Th3;
theorem ::
FINSEQ_1:5
Th5: for a,b be
natural
Number holds a
<= b iff (
Seg a)
c= (
Seg b)
proof
let a,b be
natural
Number;
thus a
<= b implies (
Seg a)
c= (
Seg b)
proof
assume
A1: a
<= b;
let x be
object;
assume x
in (
Seg a);
then
consider c be
Nat such that
A3: x
= c & 1
<= c & c
<= a;
c
<= b by
A1,
A3,
XXREAL_0: 2;
hence thesis by
A3;
end;
assume
A4: (
Seg a)
c= (
Seg b);
now
assume a
<>
0 ;
then a
in (
Seg a) by
Th3;
hence thesis by
A4,
Th1;
end;
hence thesis;
end;
theorem ::
FINSEQ_1:6
Th6: for a,b be
natural
Number holds (
Seg a)
= (
Seg b) implies a
= b
proof
let a,b be
natural
Number;
assume (
Seg a)
= (
Seg b);
then a
<= b & b
<= a by
Th5;
hence thesis by
XXREAL_0: 1;
end;
theorem ::
FINSEQ_1:7
Th7: for a,c be
natural
Number holds c
<= a implies (
Seg c)
= ((
Seg a)
/\ (
Seg c)) by
Th5,
XBOOLE_1: 28;
theorem ::
FINSEQ_1:8
for a,c be
natural
Number holds (
Seg c)
= ((
Seg c)
/\ (
Seg a)) implies c
<= a by
Th6,
Th7;
theorem ::
FINSEQ_1:9
Th9: for a be
natural
Number holds ((
Seg a)
\/
{(a
+ 1)})
= (
Seg (a
+ 1))
proof
let a be
natural
Number;
thus ((
Seg a)
\/
{(a
+ 1)})
c= (
Seg (a
+ 1))
proof
(a
+
0 )
<= (a
+ 1) by
XREAL_1: 7;
then
A1: (
Seg a)
c= (
Seg (a
+ 1)) by
Th5;
let x be
object;
assume x
in ((
Seg a)
\/
{(a
+ 1)});
then x
in (
Seg a) or x
in
{(a
+ 1)} by
XBOOLE_0:def 3;
then x
in (
Seg (a
+ 1)) or x
= (a
+ 1) by
A1,
TARSKI:def 1;
hence thesis by
Th3;
end;
let x be
object;
assume
A2: x
in (
Seg (a
+ 1));
then
reconsider x as
Element of
NAT ;
A3: x
<= (a
+ 1) by
A2,
Th1;
A4: 1
<= x by
A2,
Th1;
x
<= a or x
= (a
+ 1) by
A3,
NAT_1: 8;
then x
in (
Seg a) or x
in
{(a
+ 1)} by
A4,
TARSKI:def 1;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
FINSEQ_1:10
for k be
natural
Number holds (
Seg k)
= ((
Seg (k
+ 1))
\
{(k
+ 1)})
proof
let k be
natural
Number;
A1: (
Seg (k
+ 1))
= ((
Seg k)
\/
{(k
+ 1)}) by
Th9;
(
Seg k)
misses
{(k
+ 1)}
proof
assume not thesis;
then
A2: ((
Seg k)
/\
{(k
+ 1)})
<>
{} ;
set x = the
Element of ((
Seg k)
/\
{(k
+ 1)});
A3: x
in (
Seg k) by
A2,
XBOOLE_0:def 4;
x
in
{(k
+ 1)} by
A2,
XBOOLE_0:def 4;
then x
= (k
+ 1) by
TARSKI:def 1;
hence thesis by
A3,
Th1,
XREAL_1: 29;
end;
hence thesis by
A1,
XBOOLE_1: 88;
end;
definition
let IT be
Relation;
::
FINSEQ_1:def2
attr IT is
FinSequence-like means
:
Def2: ex n st (
dom IT)
= (
Seg n);
end
registration
cluster
empty ->
FinSequence-like for
Relation;
coherence
proof
let R be
Relation;
assume
A1: R is
empty;
take
0 ;
thus thesis by
A1;
end;
end
definition
mode
FinSequence is
FinSequence-like
Function;
end
reserve p,q,r,s,t for
FinSequence;
defpred
P[
object,
object] means ex k st $1
= k & $2
= (k
+ 1);
registration
let n be
natural
Number;
cluster (
Seg n) ->
finite;
coherence
proof
reconsider n as
Nat by
TARSKI: 1;
(
Seg n) is
finite
proof
A1: n
= { k where k be
Nat : k
< n } by
AXIOMS: 4;
A2: for x be
object st x
in n holds ex y be
object st
P[x, y]
proof
let x be
object;
assume x
in n;
then ex k be
Nat st x
= k & k
< n by
A1;
then
reconsider k = x as
Nat;
take (k
+ 1);
thus thesis;
end;
consider f such that
A3: (
dom f)
= n and
A4: for x be
object st x
in n holds
P[x, (f
. x)] from
CLASSES1:sch 1(
A2);
take f;
thus (
rng f)
= (
Seg n)
proof
thus (
rng f)
c= (
Seg n)
proof
let x be
object;
assume x
in (
rng f);
then
consider y be
object such that
A5: y
in (
dom f) and
A6: x
= (f
. y) by
FUNCT_1:def 3;
consider k such that
A7: y
= k and
A8: x
= (k
+ 1) by
A3,
A4,
A5,
A6;
ex m be
Nat st m
= y & m
< n by
A1,
A3,
A5;
then 1
<= (k
+ 1) & (k
+ 1)
<= n by
A7,
NAT_1: 11,
NAT_1: 13;
hence thesis by
A8;
end;
let x be
object;
assume x
in (
Seg n);
then
consider k be
Nat such that
A9: x
= k and
A10: 1
<= k and
A11: k
<= n;
consider i be
Nat such that
A12: (1
+ i)
= k by
A10,
NAT_1: 10;
i
in
NAT & i
< n by
A11,
A12,
NAT_1: 13,
ORDINAL1:def 12;
then
A13: i
in n by
A1;
then
P[i, (f
. i)] by
A4;
hence thesis by
A3,
A9,
A12,
A13,
FUNCT_1:def 3;
end;
thus thesis by
A3,
ORDINAL1:def 12;
end;
hence thesis;
end;
end
registration
cluster
FinSequence-like ->
finite for
Function;
coherence
proof
let f be
Function;
given n such that
A1: (
dom f)
= (
Seg n);
(
rng f) is
finite by
A1,
FINSET_1: 8;
then
[:(
dom f), (
rng f):] is
finite by
A1;
hence thesis by
FINSET_1: 1,
RELAT_1: 7;
end;
end
Lm1: ((
Seg n),n)
are_equipotent
proof
defpred
P[
Nat] means ((
Seg $1),$1)
are_equipotent ;
A1:
P[
0 ];
A2: for n st
P[n] holds
P[(n
+ 1)]
proof
let n such that
A3: ((
Seg n),n)
are_equipotent ;
A4: (
Segm (n
+ 1))
= (
succ (
Segm n)) by
NAT_1: 38
.= (n
\/
{n});
A5: (
Seg (n
+ 1))
= ((
Seg n)
\/
{(n
+ 1)}) & (
{(n
+ 1)},
{n})
are_equipotent by
Th9,
CARD_1: 28;
A6:
now
assume n
meets
{n};
then
consider x be
object such that
A7: x
in n and
A8: x
in
{n} by
XBOOLE_0: 3;
A: x
= n by
A8,
TARSKI:def 1;
reconsider xx = x as
set by
TARSKI: 1;
not xx
in xx;
hence contradiction by
A7,
A;
end;
now
assume (
Seg n)
meets
{(n
+ 1)};
then
consider x be
object such that
A9: x
in (
Seg n) and
A10: x
in
{(n
+ 1)} by
XBOOLE_0: 3;
A11: x
= (n
+ 1) by
A10,
TARSKI:def 1;
not (n
+ 1)
<= n by
NAT_1: 13;
hence contradiction by
A9,
A11,
Th1;
end;
hence thesis by
A3,
A4,
A5,
A6,
CARD_1: 31;
end;
for n holds
P[n] from
NAT_1:sch 2(
A1,
A2);
hence thesis;
end;
registration
let n be
natural
Number;
cluster (
Seg n) -> n
-element;
coherence
proof
n is
Nat by
TARSKI: 1;
hence thesis by
Lm1,
CARD_1:def 2;
end;
end
notation
let p;
synonym
len p for
card p;
end
definition
let p;
:: original:
len
redefine
::
FINSEQ_1:def3
func
len p ->
Element of
NAT means
:
Def3: (
Seg it )
= (
dom p);
coherence
proof
(
card p)
= (
card p);
hence thesis;
end;
compatibility
proof
let k be
Element of
NAT ;
consider n such that
A1: (
dom p)
= (
Seg n) by
Def2;
((
dom p),p)
are_equipotent
proof
deffunc
F(
object) =
[$1, (p
. $1)];
consider g be
Function such that
A2: (
dom g)
= (
dom p) and
A3: for x be
object st x
in (
dom p) holds (g
. x)
=
F(x) from
FUNCT_1:sch 3;
take g;
thus g is
one-to-one
proof
let x,y be
object;
assume that
A4: x
in (
dom g) and
A5: y
in (
dom g);
assume (g
. x)
= (g
. y);
then
[x, (p
. x)]
= (g
. y) by
A2,
A3,
A4
.=
[y, (p
. y)] by
A2,
A3,
A5;
hence thesis by
XTUPLE_0: 1;
end;
thus (
dom g)
= (
dom p) by
A2;
thus (
rng g)
c= p
proof
let i be
object;
assume i
in (
rng g);
then
consider x be
object such that
A6: x
in (
dom g) and
A7: (g
. x)
= i by
FUNCT_1:def 3;
(g
. x)
=
[x, (p
. x)] by
A2,
A3,
A6;
hence thesis by
A2,
A6,
A7,
FUNCT_1: 1;
end;
let x,y be
object;
assume
A8:
[x, y]
in p;
then
A9: x
in (
dom p) by
FUNCT_1: 1;
y
= (p
. x) by
A8,
FUNCT_1: 1;
then (g
. x)
=
[x, y] by
A3,
A8,
FUNCT_1: 1;
hence thesis by
A2,
A9,
FUNCT_1:def 3;
end;
then
A10: (
card p)
= (
card (
dom p)) by
CARD_1: 5;
thus k
= (
card p) implies (
Seg k)
= (
dom p) by
A1,
A10,
Lm1,
CARD_1:def 2;
assume (
Seg k)
= (
dom p);
hence k
= (
card p) by
A10,
Lm1,
CARD_1:def 2;
end;
end
definition
let p;
:: original:
dom
redefine
func
dom p ->
Subset of
NAT ;
coherence
proof
(
dom p)
= (
Seg (
len p)) by
Def3;
hence thesis;
end;
end
theorem ::
FINSEQ_1:11
(ex k st (
dom f)
c= (
Seg k)) implies ex p st f
c= p
proof
given k such that
A1: (
dom f)
c= (
Seg k);
deffunc
F(
object) = (f
. $1);
consider g such that
A2: (
dom g)
= (
Seg k) & for x be
object st x
in (
Seg k) holds (g
. x)
=
F(x) from
FUNCT_1:sch 3;
reconsider g as
FinSequence by
A2,
Def2;
take g;
let y,z be
object;
assume
A3:
[y, z]
in f;
then
A4: y
in (
dom f) by
XTUPLE_0:def 12;
reconsider z as
set by
TARSKI: 1;
A5: (f
. y)
= z by
A3,
FUNCT_1:def 2,
A4;
[y, (g
. y)]
in g by
A1,
A2,
A4,
FUNCT_1: 1;
hence thesis by
A1,
A2,
A4,
A5;
end;
scheme ::
FINSEQ_1:sch1
SeqEx { A() ->
Nat , P[
object,
object] } :
ex p st (
dom p)
= (
Seg A()) & for k st k
in (
Seg A()) holds P[k, (p
. k)]
provided
A1: for k st k
in (
Seg A()) holds ex x st P[k, x];
A2: for x be
object st x
in (
Seg A()) holds ex y be
object st P[x, y] by
A1;
consider f be
Function such that
A3: (
dom f)
= (
Seg A()) & for x be
object st x
in (
Seg A()) holds P[x, (f
. x)] from
CLASSES1:sch 1(
A2);
reconsider p = f as
FinSequence by
A3,
Def2;
take p;
thus thesis by
A3;
end;
scheme ::
FINSEQ_1:sch2
SeqLambda { A() ->
Nat , F(
object) ->
object } :
ex p be
FinSequence st (
len p)
= A() & for k st k
in (
dom p) holds (p
. k)
= F(k);
consider f be
Function such that
A1: (
dom f)
= (
Seg A()) & for x be
object st x
in (
Seg A()) holds (f
. x)
= F(x) from
FUNCT_1:sch 3;
A2: A()
in
NAT by
ORDINAL1:def 12;
reconsider p = f as
FinSequence by
A1,
Def2;
take p;
thus thesis by
A1,
A2,
Def3;
end;
theorem ::
FINSEQ_1:12
z
in p implies ex k st k
in (
dom p) & z
=
[k, (p
. k)]
proof
assume
A1: z
in p;
then
consider x,y be
object such that
A2: z
=
[x, y] by
RELAT_1:def 1;
x
in (
dom p) by
A1,
A2,
FUNCT_1: 1;
then
reconsider k = x as
Nat;
take k;
thus thesis by
A1,
A2,
FUNCT_1: 1;
end;
theorem ::
FINSEQ_1:13
(
dom p)
= (
dom q) & (for k st k
in (
dom p) holds (p
. k)
= (q
. k)) implies p
= q;
theorem ::
FINSEQ_1:14
Th14: (
len p)
= (
len q) & (for k st 1
<= k & k
<= (
len p) holds (p
. k)
= (q
. k)) implies p
= q
proof
assume that
A1: (
len p)
= (
len q) and
A2: for k st 1
<= k & k
<= (
len p) holds (p
. k)
= (q
. k);
A3: (
dom p)
= (
Seg (
len p)) by
Def3;
A4: (
dom q)
= (
Seg (
len q)) by
Def3;
now
let x be
object;
assume
A5: x
in (
dom p);
then
reconsider k = x as
Nat;
1
<= k & k
<= (
len p) by
A3,
A5,
Th1;
hence (p
. x)
= (q
. x) by
A2;
end;
hence thesis by
A1,
A3,
A4;
end;
theorem ::
FINSEQ_1:15
Th15: (p
| (
Seg a)) is
FinSequence
proof
A0: a is
Nat by
TARSKI: 1;
A1: (
dom (p
| (
Seg a)))
= ((
dom p)
/\ (
Seg a)) by
RELAT_1: 61
.= ((
Seg (
len p))
/\ (
Seg a)) by
Def3;
(
len p)
<= a or a
<= (
len p);
then (
dom (p
| (
Seg a)))
= (
Seg (
len p)) or (
dom (p
| (
Seg a)))
= (
Seg a) by
A1,
Th5,
XBOOLE_1: 28;
hence thesis by
A0,
Def2;
end;
theorem ::
FINSEQ_1:16
(
rng p)
c= (
dom f) implies (f
* p) is
FinSequence
proof
assume (
rng p)
c= (
dom f);
then (
dom (f
* p))
= (
dom p) by
RELAT_1: 27
.= (
Seg (
len p)) by
Def3;
hence thesis by
Def2;
end;
theorem ::
FINSEQ_1:17
Th17: a
<= (
len p) & q
= (p
| (
Seg a)) implies (
len q)
= a & (
dom q)
= (
Seg a)
proof
assume that
A1: a
<= (
len p) and
A2: q
= (p
| (
Seg a));
(
Seg a)
c= (
Seg (
len p)) by
A1,
Th5;
then (
Seg a)
c= (
dom p) by
Def3;
then a
in
NAT & (
dom q)
= (
Seg a) by
A2,
ORDINAL1:def 12,
RELAT_1: 62;
hence thesis by
Def3;
end;
definition
let D be
set;
::
FINSEQ_1:def4
mode
FinSequence of D ->
FinSequence means
:
Def4: (
rng it )
c= D;
existence
proof
(
rng
{} )
c= D;
hence thesis;
end;
end
registration
let D be
set;
cluster -> D
-valued for
FinSequence of D;
coherence
proof
let f be
FinSequence of D;
thus (
rng f)
c= D by
Def4;
end;
end
Lm2: for D be
set, f be
FinSequence of D holds f is
PartFunc of
NAT , D
proof
let D be
set, f be
FinSequence of D;
(
dom f)
c=
NAT & (
rng f)
c= D by
Def4;
hence thesis by
RELSET_1: 4;
end;
registration
cluster
empty ->
FinSequence-like for
Relation;
coherence ;
end
registration
let D be
set;
cluster
FinSequence-like for
PartFunc of
NAT , D;
existence
proof
{} is
PartFunc of
NAT , D by
RELSET_1: 12;
hence thesis;
end;
end
definition
let D be
set;
:: original:
FinSequence
redefine
mode
FinSequence of D ->
FinSequence-like
PartFunc of
NAT , D ;
coherence by
Lm2;
end
reserve D for
set;
theorem ::
FINSEQ_1:18
Th18: for p be
FinSequence of D holds (p
| (
Seg a)) is
FinSequence of D
proof
let p be
FinSequence of D;
A1: (p
| (
Seg a)) is
FinSequence by
Th15;
(
rng (p
| (
Seg a)))
c= (
rng p) & (
rng p)
c= D by
Def4,
RELAT_1: 70;
hence thesis by
A1,
Def4,
XBOOLE_1: 1;
end;
theorem ::
FINSEQ_1:19
for D be non
empty
set holds ex p be
FinSequence of D st (
len p)
= a
proof
let D be non
empty
set;
reconsider a as
Element of
NAT by
ORDINAL1:def 12;
set y = the
Element of D;
set p = ((
Seg a)
--> y);
A1: (
dom p)
= (
Seg a) by
FUNCOP_1: 13;
then
reconsider p as
FinSequence by
Def2;
(
rng p)
c=
{y} &
{y}
c= D by
FUNCOP_1: 13,
ZFMISC_1: 31;
then
reconsider q = p as
FinSequence of D by
Def4,
XBOOLE_1: 1;
take q;
thus thesis by
A1,
Def3;
end;
Lm3: q
=
{} iff (
len q)
=
0 ;
theorem ::
FINSEQ_1:20
p
<>
{} iff (
len p)
>= 1
proof
hereby
assume p
<>
{} ;
then ((
len p)
+ 1)
> (
0
+ 1) by
XREAL_1: 8;
hence (
len p)
>= 1 by
NAT_1: 13;
end;
assume (
len p)
>= 1;
hence thesis;
end;
definition
let x be
object;
::
FINSEQ_1:def5
func
<*x*> ->
set equals
{
[1, x]};
coherence ;
end
definition
let D be
set;
::
FINSEQ_1:def6
func
<*> D ->
FinSequence of D equals
{} ;
coherence
proof
(
rng
{} )
c= D;
hence thesis by
Def4;
end;
end
registration
let D be
set;
cluster (
<*> D) ->
empty;
coherence ;
end
registration
let D be
set;
cluster
empty for
FinSequence of D;
existence
proof
take (
<*> D);
thus thesis;
end;
end
definition
let p, q;
::
FINSEQ_1:def7
func p
^ q ->
FinSequence means
:
Def7: (
dom it )
= (
Seg ((
len p)
+ (
len q))) & (for k st k
in (
dom p) holds (it
. k)
= (p
. k)) & for k st k
in (
dom q) holds (it
. ((
len p)
+ k))
= (q
. k);
existence
proof
defpred
P[
object,
object] means (for k st k
= $1 & 1
<= k & k
<= (
len p) holds $2
= (p
. k)) & (for k st k
= $1 & ((
len p)
+ 1)
<= k & k
<= ((
len p)
+ (
len q)) holds $2
= (q
. (k
- (
len p))));
A1: for x be
object st x
in (
Seg ((
len p)
+ (
len q))) holds ex y be
object st
P[x, y]
proof
let x be
object;
assume x
in (
Seg ((
len p)
+ (
len q)));
then
reconsider m = x as
Element of
NAT ;
A2:
now
assume
A3: ((
len p)
+ 1)
<= m;
set y = (q
. (m
- (
len p)));
A4: for k st k
= x & 1
<= k & k
<= (
len p) holds y
= (p
. k)
proof
let k;
assume that
A5: k
= x and 1
<= k and
A6: k
<= (
len p);
(m
+ ((
len p)
+ 1))
<= (m
+ (
len p)) by
A3,
A5,
A6,
XREAL_1: 7;
then ((m
+ (
len p))
+ 1)
<= ((m
+ (
len p))
+
0 );
hence thesis by
XREAL_1: 6;
end;
for k st k
= x & ((
len p)
+ 1)
<= k & k
<= ((
len p)
+ (
len q)) holds y
= (q
. (k
- (
len p)));
hence thesis by
A4;
end;
now
assume
A7: not ((
len p)
+ 1)
<= m;
set y = (p
. m);
(for k st k
= x & 1
<= k & k
<= (
len p) holds y
= (p
. k)) & for k st k
= x & ((
len p)
+ 1)
<= k & k
<= ((
len p)
+ (
len q)) holds y
= (q
. (k
- (
len p))) by
A7;
hence thesis;
end;
hence thesis by
A2;
end;
consider f such that
A8: (
dom f)
= (
Seg ((
len p)
+ (
len q))) & for x be
object st x
in (
Seg ((
len p)
+ (
len q))) holds
P[x, (f
. x)] from
CLASSES1:sch 1(
A1);
A9: for k st k
in (
dom p) holds (f
. k)
= (p
. k)
proof
let k;
assume k
in (
dom p);
then
A10: k
in (
Seg (
len p)) by
Def3;
then
A11: 1
<= k & k
<= (
len p) by
Th1;
(
Seg (
len p))
c= (
Seg ((
len p)
+ (
len q))) by
Th5,
NAT_1: 11;
hence thesis by
A8,
A10,
A11;
end;
A12: for n st n
in (
dom q) holds (f
. ((
len p)
+ n))
= (q
. n)
proof
let n;
assume n
in (
dom q);
then
A13: n
in (
Seg (
len q)) by
Def3;
then
A14: 1
<= n by
Th1;
A15: n
<= (
len q) by
A13,
Th1;
A16: ((
len p)
+ 1)
<= ((
len p)
+ n) by
A14,
XREAL_1: 7;
A17: ((
len p)
+ n)
<= ((
len p)
+ (
len q)) by
A15,
XREAL_1: 7;
((
len p)
+ n)
<= (((
len p)
+ n)
+ (
len p)) by
NAT_1: 11;
then ((
len p)
+ 1)
<= (((
len p)
+ n)
+ (
len p)) by
A16,
XXREAL_0: 2;
then 1
<= ((
len p)
+ n) by
XREAL_1: 6;
then ((
len p)
+ n)
in (
Seg ((
len p)
+ (
len q))) by
A17;
then (f
. ((
len p)
+ n))
= (q
. ((n
+ (
len p))
- (
len p))) by
A8,
A16,
A17;
hence thesis;
end;
reconsider r = f as
FinSequence by
A8,
Def2;
take r;
thus thesis by
A8,
A9,
A12;
end;
uniqueness
proof
let f,g be
FinSequence such that
A18: (
dom f)
= (
Seg ((
len p)
+ (
len q))) and
A19: for k st k
in (
dom p) holds (f
. k)
= (p
. k) and
A20: for k st k
in (
dom q) holds (f
. ((
len p)
+ k))
= (q
. k) and
A21: (
dom g)
= (
Seg ((
len p)
+ (
len q))) and
A22: for k st k
in (
dom p) holds (g
. k)
= (p
. k) and
A23: for k st k
in (
dom q) holds (g
. ((
len p)
+ k))
= (q
. k);
for x be
object st x
in (
Seg ((
len p)
+ (
len q))) holds (f
. x)
= (g
. x)
proof
let x be
object;
assume
A24: x
in (
Seg ((
len p)
+ (
len q)));
then
reconsider k = x as
Element of
NAT ;
A25: 1
<= k by
A24,
Th1;
A26:
now
assume ((
len p)
+ 1)
<= k;
then
consider m be
Nat such that
A27: (((
len p)
+ 1)
+ m)
= k by
NAT_1: 10;
((
len p)
+ (1
+ m))
<= ((
len p)
+ (
len q)) by
A24,
A27,
Th1;
then (1
+
0 )
<= (1
+ m) & (1
+ m)
<= (
len q) by
XREAL_1: 6;
then (1
+ m)
in (
Seg (
len q));
then
A28: (1
+ m)
in (
dom q) by
Def3;
then (g
. ((
len p)
+ (1
+ m)))
= (q
. (1
+ m)) by
A23;
hence thesis by
A20,
A27,
A28;
end;
now
assume not ((
len p)
+ 1)
<= k;
then k
<= (
len p) by
NAT_1: 8;
then k
in (
Seg (
len p)) by
A25;
then
A29: k
in (
dom p) by
Def3;
then (f
. k)
= (p
. k) by
A19;
hence thesis by
A22,
A29;
end;
hence thesis by
A26;
end;
hence thesis by
A18,
A21;
end;
end
theorem ::
FINSEQ_1:21
Th21: p
= ((p
^ q)
| (
dom p))
proof
A1: (
dom (p
^ q))
= (
Seg ((
len p)
+ (
len q))) by
Def7;
A2: (
dom p)
= (
Seg (
len p)) by
Def3;
then
A3: (
dom p)
= ((
dom (p
^ q))
/\ (
Seg (
len p))) by
A1,
Th7,
NAT_1: 12;
for x be
object st x
in (
dom p) holds (p
. x)
= ((p
^ q)
. x) by
Def7;
hence thesis by
A2,
A3,
FUNCT_1: 46;
end;
theorem ::
FINSEQ_1:22
Th22: (
len (p
^ q))
= ((
len p)
+ (
len q))
proof
(
dom (p
^ q))
= (
Seg ((
len p)
+ (
len q))) by
Def7;
hence thesis by
Def3;
end;
theorem ::
FINSEQ_1:23
Th23: for k be
Nat st ((
len p)
+ 1)
<= k & k
<= ((
len p)
+ (
len q)) holds ((p
^ q)
. k)
= (q
. (k
- (
len p)))
proof
let k be
Nat;
assume that
A1: ((
len p)
+ 1)
<= k and
A2: k
<= ((
len p)
+ (
len q));
consider m be
Nat such that
A3: (((
len p)
+ 1)
+ m)
= k by
A1,
NAT_1: 10;
A4: ((
len p)
+ (1
+ m))
= k by
A3;
(1
+ m)
= (k
- (
len p)) by
A3;
then
A5: 1
<= (1
+ m) by
A1,
XREAL_1: 19;
(k
- (
len p))
<= (
len q) by
A2,
XREAL_1: 20;
then (1
+ m)
in (
Seg (
len q)) by
A3,
A5;
then (1
+ m)
in (
dom q) by
Def3;
hence thesis by
A4,
Def7;
end;
theorem ::
FINSEQ_1:24
Th24: for k be
Nat st (
len p)
< k & k
<= (
len (p
^ q)) holds ((p
^ q)
. k)
= (q
. (k
- (
len p)))
proof
let k be
Nat;
assume (
len p)
< k & k
<= (
len (p
^ q));
then ((
len p)
+ 1)
<= k & k
<= ((
len p)
+ (
len q)) by
Th22,
NAT_1: 13;
hence thesis by
Th23;
end;
theorem ::
FINSEQ_1:25
Th25: for k be
Nat st k
in (
dom (p
^ q)) holds (k
in (
dom p) or ex n st n
in (
dom q) & k
= ((
len p)
+ n))
proof
let k be
Nat;
assume k
in (
dom (p
^ q));
then
A1: k
in (
Seg (
len (p
^ q))) by
Def3;
then
A2: k
in (
Seg ((
len p)
+ (
len q))) by
Th22;
A3: k
in
NAT & 1
<= k by
A1,
Th1;
A4:
now
assume not ((
len p)
+ 1)
<= k;
then k
<= (
len p) by
NAT_1: 8;
then k
in (
Seg (
len p)) by
A3;
hence thesis by
Def3;
end;
now
assume ((
len p)
+ 1)
<= k;
then
consider n be
Nat such that
A5: k
= (((
len p)
+ 1)
+ n) by
NAT_1: 10;
((
len p)
+ (1
+ n))
<= ((
len p)
+ (
len q)) by
A2,
A5,
Th1;
then
A6: (1
+ n)
<= (
len q) by
XREAL_1: 6;
1
<= (1
+ n) by
NAT_1: 11;
then (1
+ n)
in (
Seg (
len q)) by
A6;
then
A7: (1
+ n)
in (
dom q) by
Def3;
k
= ((
len p)
+ (1
+ n)) by
A5;
hence thesis by
A7;
end;
hence thesis by
A4;
end;
theorem ::
FINSEQ_1:26
Th26: (
dom p)
c= (
dom (p
^ q))
proof
(
Seg (
len p))
c= (
Seg ((
len p)
+ (
len q))) by
Th5,
NAT_1: 11;
then (
Seg (
len p))
c= (
dom (p
^ q)) by
Def7;
hence thesis by
Def3;
end;
theorem ::
FINSEQ_1:27
Th27: x
in (
dom q) implies ex k st k
= x & ((
len p)
+ k)
in (
dom (p
^ q))
proof
assume
A1: x
in (
dom q);
then
A2: x
in (
Seg (
len q)) by
Def3;
reconsider k = x as
Element of
NAT by
A1;
take k;
A3: 1
<= k by
A2,
Th1;
A4: k
<= (
len q) by
A2,
Th1;
k
<= ((
len p)
+ k) by
NAT_1: 11;
then
A5: 1
<= ((
len p)
+ k) by
A3,
XXREAL_0: 2;
((
len p)
+ k)
<= ((
len p)
+ (
len q)) by
A4,
XREAL_1: 7;
then ((
len p)
+ k)
in (
Seg ((
len p)
+ (
len q))) by
A5;
hence thesis by
Def7;
end;
theorem ::
FINSEQ_1:28
Th28: k
in (
dom q) implies ((
len p)
+ k)
in (
dom (p
^ q))
proof
assume k
in (
dom q);
then ex n st n
= k & ((
len p)
+ n)
in (
dom (p
^ q)) by
Th27;
hence thesis;
end;
theorem ::
FINSEQ_1:29
Th29: (
rng p)
c= (
rng (p
^ q))
proof
let x be
object;
assume x
in (
rng p);
then
consider y be
object such that
A1: y
in (
dom p) and
A2: x
= (p
. y) by
FUNCT_1:def 3;
reconsider k = y as
Element of
NAT by
A1;
A3: (
dom p)
c= (
dom (p
^ q)) by
Th26;
((p
^ q)
. k)
= (p
. k) by
A1,
Def7;
hence x
in (
rng (p
^ q)) by
A1,
A2,
A3,
FUNCT_1:def 3;
end;
theorem ::
FINSEQ_1:30
Th30: (
rng q)
c= (
rng (p
^ q))
proof
let x be
object;
assume x
in (
rng q);
then
consider y be
object such that
A1: y
in (
dom q) and
A2: x
= (q
. y) by
FUNCT_1:def 3;
reconsider k = y as
Element of
NAT by
A1;
((
len p)
+ k)
in (
dom (p
^ q)) & ((p
^ q)
. ((
len p)
+ k))
= (q
. k) by
A1,
Def7,
Th28;
hence x
in (
rng (p
^ q)) by
A2,
FUNCT_1:def 3;
end;
theorem ::
FINSEQ_1:31
Th31: (
rng (p
^ q))
= ((
rng p)
\/ (
rng q))
proof
now
let x be
object;
assume x
in (
rng (p
^ q));
then
consider y be
object such that
A1: y
in (
dom (p
^ q)) and
A2: x
= ((p
^ q)
. y) by
FUNCT_1:def 3;
A3: y
in (
Seg ((
len p)
+ (
len q))) by
A1,
Def7;
reconsider k = y as
Element of
NAT by
A1;
A4: 1
<= k by
A3,
Th1;
A5: k
<= ((
len p)
+ (
len q)) by
A3,
Th1;
A6:
now
assume
A7: ((
len p)
+ 1)
<= k;
then
A8: (q
. (k
- (
len p)))
= x by
A2,
A5,
Th23;
consider m be
Nat such that
A9: (((
len p)
+ 1)
+ m)
= k by
A7,
NAT_1: 10;
((
len p)
+ (1
+ m))
= k by
A9;
then (1
+
0 )
<= (1
+ m) & (1
+ m)
<= (
len q) by
A3,
Th1,
XREAL_1: 6;
then (1
+ m)
in (
Seg (
len q));
then (k
- (
len p))
in (
dom q) by
A9,
Def3;
hence x
in (
rng q) by
A8,
FUNCT_1:def 3;
end;
now
assume not ((
len p)
+ 1)
<= k;
then k
<= (
len p) by
NAT_1: 8;
then k
in (
Seg (
len p)) by
A4;
then
A10: k
in (
dom p) by
Def3;
then (p
. k)
= x by
A2,
Def7;
hence x
in (
rng p) by
A10,
FUNCT_1:def 3;
end;
hence x
in ((
rng p)
\/ (
rng q)) by
A6,
XBOOLE_0:def 3;
end;
then
A11: (
rng (p
^ q))
c= ((
rng p)
\/ (
rng q));
(
rng p)
c= (
rng (p
^ q)) & (
rng q)
c= (
rng (p
^ q)) by
Th29,
Th30;
then ((
rng p)
\/ (
rng q))
c= (
rng (p
^ q)) by
XBOOLE_1: 8;
hence thesis by
A11;
end;
theorem ::
FINSEQ_1:32
Th32: ((p
^ q)
^ r)
= (p
^ (q
^ r))
proof
A1: (
dom ((p
^ q)
^ r))
= (
Seg ((
len (p
^ q))
+ (
len r))) by
Def7
.= (
Seg (((
len p)
+ (
len q))
+ (
len r))) by
Th22
.= (
Seg ((
len p)
+ ((
len q)
+ (
len r))))
.= (
Seg ((
len p)
+ (
len (q
^ r)))) by
Th22;
A2: for k st k
in (
dom p) holds (((p
^ q)
^ r)
. k)
= (p
. k)
proof
let k;
assume
A3: k
in (
dom p);
(
dom p)
c= (
dom (p
^ q)) by
Th26;
hence (((p
^ q)
^ r)
. k)
= ((p
^ q)
. k) by
A3,
Def7
.= (p
. k) by
A3,
Def7;
end;
for k st k
in (
dom (q
^ r)) holds (((p
^ q)
^ r)
. ((
len p)
+ k))
= ((q
^ r)
. k)
proof
let k;
assume
A4: k
in (
dom (q
^ r));
A5:
now
assume
A6: k
in (
dom q);
then ((
len p)
+ k)
in (
dom (p
^ q)) by
Th28;
hence (((p
^ q)
^ r)
. ((
len p)
+ k))
= ((p
^ q)
. ((
len p)
+ k)) by
Def7
.= (q
. k) by
A6,
Def7
.= ((q
^ r)
. k) by
A6,
Def7;
end;
now
assume not k
in (
dom q);
then
consider n such that
A7: n
in (
dom r) and
A8: k
= ((
len q)
+ n) by
A4,
Th25;
thus (((p
^ q)
^ r)
. ((
len p)
+ k))
= (((p
^ q)
^ r)
. (((
len p)
+ (
len q))
+ n)) by
A8
.= (((p
^ q)
^ r)
. ((
len (p
^ q))
+ n)) by
Th22
.= (r
. n) by
A7,
Def7
.= ((q
^ r)
. k) by
A7,
A8,
Def7;
end;
hence thesis by
A5;
end;
hence thesis by
A1,
A2,
Def7;
end;
theorem ::
FINSEQ_1:33
(p
^ r)
= (q
^ r) or (r
^ p)
= (r
^ q) implies p
= q
proof
assume
A1: (p
^ r)
= (q
^ r) or (r
^ p)
= (r
^ q);
A2:
now
assume
A3: (p
^ r)
= (q
^ r);
then ((
len p)
+ (
len r))
= (
len (q
^ r)) by
Th22;
then ((
len p)
+ (
len r))
= ((
len q)
+ (
len r)) by
Th22;
then
A4: (
dom p)
= (
Seg (
len q)) by
Def3
.= (
dom q) by
Def3;
for k st k
in (
dom p) holds (p
. k)
= (q
. k)
proof
let k;
assume
A5: k
in (
dom p);
hence (p
. k)
= ((q
^ r)
. k) by
A3,
Def7
.= (q
. k) by
A4,
A5,
Def7;
end;
hence thesis by
A4;
end;
now
assume
A6: (r
^ p)
= (r
^ q);
then ((
len r)
+ (
len p))
= (
len (r
^ q)) by
Th22
.= ((
len r)
+ (
len q)) by
Th22;
then
A7: (
dom p)
= (
Seg (
len q)) by
Def3
.= (
dom q) by
Def3;
for k st k
in (
dom p) holds (p
. k)
= (q
. k)
proof
let k;
assume
A8: k
in (
dom p);
hence (p
. k)
= ((r
^ q)
. ((
len r)
+ k)) by
A6,
Def7
.= (q
. k) by
A7,
A8,
Def7;
end;
hence thesis by
A7;
end;
hence thesis by
A1,
A2;
end;
theorem ::
FINSEQ_1:34
Th34: (p
^
{} )
= p & (
{}
^ p)
= p
proof
A1: (
dom (p
^
{} ))
= (
Seg (
len (p
^
{} ))) by
Def3
.= (
Seg ((
len p)
+ (
len
{} ))) by
Th22
.= (
dom p) by
Def3;
for k st k
in (
dom p) holds (p
. k)
= ((p
^
{} )
. k) by
Def7;
hence (p
^
{} )
= p by
A1;
A2: (
dom (
{}
^ p))
= (
Seg (
len (
{}
^ p))) by
Def3
.= (
Seg ((
len
{} )
+ (
len p))) by
Th22
.= (
dom p) by
Def3;
for k st k
in (
dom p) holds (p
. k)
= ((
{}
^ p)
. k)
proof
let k;
assume
A3: k
in (
dom p);
thus ((
{}
^ p)
. k)
= ((
{}
^ p)
. ((
len
{} )
+ k))
.= (p
. k) by
A3,
Def7;
end;
hence (
{}
^ p)
= p by
A2;
end;
theorem ::
FINSEQ_1:35
Th35: (p
^ q)
=
{} implies p
=
{} & q
=
{}
proof
assume (p
^ q)
=
{} ;
then
0
= (
len (p
^ q))
.= ((
len p)
+ (
len q)) by
Th22;
hence thesis;
end;
definition
let D be
set;
let p,q be
FinSequence of D;
:: original:
^
redefine
func p
^ q ->
FinSequence of D ;
coherence
proof
A1: (
rng (p
^ q))
= ((
rng p)
\/ (
rng q)) & (
rng p)
c= D by
Def4,
Th31;
(
rng q)
c= D by
Def4;
hence (
rng (p
^ q))
c= D by
A1,
XBOOLE_1: 8;
end;
end
Lm4: for x1,y1 be
object holds
[x, y]
in
{
[x1, y1]} implies x
= x1 & y
= y1
proof
let x1,y1 be
object;
assume
[x, y]
in
{
[x1, y1]};
then
[x, y]
=
[x1, y1] by
TARSKI:def 1;
hence thesis by
XTUPLE_0: 1;
end;
definition
let x be
object;
:: original:
<*
redefine
::
FINSEQ_1:def8
func
<*x*> ->
Function means
:
Def8: (
dom it )
= (
Seg 1) & (it
. 1)
= x;
coherence ;
compatibility
proof
let f be
Function;
hereby
assume
A1: f
=
<*x*>;
hence (
dom f)
= (
Seg 1) by
Th2,
RELAT_1: 9;
[1, x]
in f by
A1,
TARSKI:def 1;
hence (f
. 1)
= x by
FUNCT_1: 1;
end;
assume that
A2: (
dom f)
= (
Seg 1) and
A3: (f
. 1)
= x;
reconsider g =
{
[1, (f
. 1)]} as
Function;
for y,z be
object holds
[y, z]
in f iff
[y, z]
in g
proof
let y,z be
object;
hereby
assume
A4:
[y, z]
in f;
then
A5: y
in
{1} by
A2,
Th2,
XTUPLE_0:def 12;
A6: z
in (
rng f) by
A4,
XTUPLE_0:def 13;
A7: (
rng f)
=
{(f
. 1)} by
A2,
Th2,
FUNCT_1: 4;
A8: y
= 1 by
A5,
TARSKI:def 1;
z
= (f
. 1) by
A6,
A7,
TARSKI:def 1;
hence
[y, z]
in g by
A8,
TARSKI:def 1;
end;
assume
[y, z]
in g;
then
A9: y
= 1 & z
= (f
. 1) by
Lm4;
1
in (
dom f) by
A2;
hence thesis by
A9,
FUNCT_1:def 2;
end;
hence thesis by
A3,
RELAT_1:def 2;
end;
end
registration
let x be
object;
cluster
<*x*> ->
Function-like
Relation-like;
coherence ;
end
registration
let x be
object;
cluster
<*x*> ->
FinSequence-like;
coherence by
Def8;
end
theorem ::
FINSEQ_1:36
Th36: (p
^ q) is
FinSequence of D implies p is
FinSequence of D & q is
FinSequence of D
proof
assume (p
^ q) is
FinSequence of D;
then (
rng (p
^ q))
c= D by
Def4;
then
A1: ((
rng p)
\/ (
rng q))
c= D by
Th31;
(
rng p)
c= ((
rng p)
\/ (
rng q)) by
XBOOLE_1: 7;
hence p is
FinSequence of D by
Def4,
A1,
XBOOLE_1: 1;
(
rng q)
c= ((
rng p)
\/ (
rng q)) by
XBOOLE_1: 7;
hence thesis by
Def4,
A1,
XBOOLE_1: 1;
end;
definition
let x,y be
object;
::
FINSEQ_1:def9
func
<*x,y*> ->
set equals (
<*x*>
^
<*y*>);
correctness ;
let z be
object;
::
FINSEQ_1:def10
func
<*x,y,z*> ->
set equals ((
<*x*>
^
<*y*>)
^
<*z*>);
correctness ;
end
registration
let x,y be
object;
cluster
<*x, y*> ->
Function-like
Relation-like;
coherence ;
let z be
object;
cluster
<*x, y, z*> ->
Function-like
Relation-like;
coherence ;
end
registration
let x,y be
object;
cluster
<*x, y*> ->
FinSequence-like;
coherence ;
let z be
object;
cluster
<*x, y, z*> ->
FinSequence-like;
coherence ;
end
theorem ::
FINSEQ_1:37
for x be
object holds
<*x*>
=
{
[1, x]};
theorem ::
FINSEQ_1:38
Th38: for x be
object holds p
=
<*x*> iff (
dom p)
= (
Seg 1) & (
rng p)
=
{x}
proof
let x be
object;
thus p
=
<*x*> implies (
dom p)
= (
Seg 1) & (
rng p)
=
{x}
proof
assume
A1: p
=
<*x*>;
hence (
dom p)
= (
Seg 1) by
Def8;
(
dom p)
=
{1} by
A1,
Def8,
Th2;
then (
rng p)
=
{(p
. 1)} by
FUNCT_1: 4;
hence thesis by
A1,
Def8;
end;
assume that
A2: (
dom p)
= (
Seg 1) and
A3: (
rng p)
=
{x};
1
in (
dom p) by
A2;
then (p
. 1)
in
{x} by
A3,
FUNCT_1:def 3;
then (p
. 1)
= x by
TARSKI:def 1;
hence thesis by
A2,
Def8;
end;
theorem ::
FINSEQ_1:39
Th39: for x be
object holds p
=
<*x*> iff (
len p)
= 1 & (
rng p)
=
{x}
proof
let x be
object;
(
len p)
= 1 iff (
dom p)
= (
Seg 1) by
Def3;
hence thesis by
Th38;
end;
theorem ::
FINSEQ_1:40
Th40: for x be
object holds p
=
<*x*> iff (
len p)
= 1 & (p
. 1)
= x
proof
let x be
object;
(
len p)
= 1 iff (
dom p)
= (
Seg 1) by
Def3;
hence thesis by
Def8;
end;
theorem ::
FINSEQ_1:41
for x be
object holds ((
<*x*>
^ p)
. 1)
= x
proof
let x be
object;
1
in (
Seg 1);
then 1
in (
dom
<*x*>) by
Def8;
then ((
<*x*>
^ p)
. 1)
= (
<*x*>
. 1) by
Def7;
hence thesis by
Def8;
end;
theorem ::
FINSEQ_1:42
Th42: for x be
object holds ((p
^
<*x*>)
. ((
len p)
+ 1))
= x
proof
let x be
object;
(
dom
<*x*>)
= (
Seg 1) by
Def8;
then 1
in (
dom
<*x*>);
hence ((p
^
<*x*>)
. ((
len p)
+ 1))
= (
<*x*>
. 1) by
Def7
.= x by
Def8;
end;
theorem ::
FINSEQ_1:43
for x,y,z be
object holds
<*x, y, z*>
= (
<*x*>
^
<*y, z*>) &
<*x, y, z*>
= (
<*x, y*>
^
<*z*>) by
Th32;
theorem ::
FINSEQ_1:44
Th44: for x,y be
object holds p
=
<*x, y*> iff (
len p)
= 2 & (p
. 1)
= x & (p
. 2)
= y
proof
let x,y be
object;
thus p
=
<*x, y*> implies (
len p)
= 2 & (p
. 1)
= x & (p
. 2)
= y
proof
assume
A1: p
=
<*x, y*>;
hence (
len p)
= ((
len
<*x*>)
+ (
len
<*y*>)) by
Th22
.= (1
+ (
len
<*y*>)) by
Th39
.= (1
+ 1) by
Th39
.= 2;
A2: 1
in
{1} by
TARSKI:def 1;
then 1
in (
dom
<*x*>) by
Def8,
Th2;
hence (p
. 1)
= (
<*x*>
. 1) by
A1,
Def7
.= x by
Def8;
A3: 1
in (
dom
<*y*>) by
A2,
Def8,
Th2;
thus (p
. 2)
= ((
<*x*>
^
<*y*>)
. (1
+ 1)) by
A1
.= ((
<*x*>
^
<*y*>)
. ((
len
<*x*>)
+ 1)) by
Th39
.= (
<*y*>
. 1) by
A3,
Def7
.= y by
Def8;
end;
assume that
A4: (
len p)
= 2 and
A5: (p
. 1)
= x and
A6: (p
. 2)
= y;
A7: (
dom p)
= (
Seg (1
+ 1)) by
A4,
Def3
.= (
Seg ((
len
<*x*>)
+ 1)) by
Th39
.= (
Seg ((
len
<*x*>)
+ (
len
<*y*>))) by
Th39;
A8: for k st k
in (
dom
<*x*>) holds (p
. k)
= (
<*x*>
. k)
proof
let k;
assume k
in (
dom
<*x*>);
then k
in
{1} by
Def8,
Th2;
then k
= 1 by
TARSKI:def 1;
hence thesis by
A5,
Def8;
end;
for k st k
in (
dom
<*y*>) holds (p
. ((
len
<*x*>)
+ k))
= (
<*y*>
. k)
proof
let k;
assume k
in (
dom
<*y*>);
then
A9: k
in
{1} by
Def8,
Th2;
thus (p
. ((
len
<*x*>)
+ k))
= (p
. (1
+ k)) by
Th39
.= (p
. (1
+ 1)) by
A9,
TARSKI:def 1
.= (
<*y*>
. 1) by
A6,
Def8
.= (
<*y*>
. k) by
A9,
TARSKI:def 1;
end;
hence thesis by
A7,
A8,
Def7;
end;
theorem ::
FINSEQ_1:45
Th45: for x,y,z be
object holds p
=
<*x, y, z*> iff (
len p)
= 3 & (p
. 1)
= x & (p
. 2)
= y & (p
. 3)
= z
proof
let x,y,z be
object;
thus p
=
<*x, y, z*> implies (
len p)
= 3 & (p
. 1)
= x & (p
. 2)
= y & (p
. 3)
= z
proof
assume
A1: p
=
<*x, y, z*>;
hence (
len p)
= ((
len
<*x, y*>)
+ (
len
<*z*>)) by
Th22
.= (2
+ (
len
<*z*>)) by
Th44
.= (2
+ 1) by
Th39
.= 3;
A2: 1
in
{1} by
TARSKI:def 1;
then
A3: 1
in (
dom
<*x*>) by
Def8,
Th2;
thus (p
. 1)
= ((
<*x*>
^
<*y, z*>)
. 1) by
A1,
Th32
.= (
<*x*>
. 1) by
A3,
Def7
.= x by
Def8;
2
in (
Seg 2) & (
len
<*x, y*>)
= 2 by
Th44;
then 2
in (
dom
<*x, y*>) by
Def3;
hence (p
. 2)
= (
<*x, y*>
. 2) by
A1,
Def7
.= y by
Th44;
A4: 1
in (
dom
<*z*>) by
A2,
Def8,
Th2;
thus (p
. 3)
= ((
<*x, y*>
^
<*z*>)
. (2
+ 1)) by
A1
.= ((
<*x, y*>
^
<*z*>)
. ((
len
<*x, y*>)
+ 1)) by
Th44
.= (
<*z*>
. 1) by
A4,
Def7
.= z by
Def8;
end;
assume that
A5: (
len p)
= 3 and
A6: (p
. 1)
= x and
A7: (p
. 2)
= y and
A8: (p
. 3)
= z;
A9: (
dom p)
= (
Seg (2
+ 1)) by
A5,
Def3
.= (
Seg ((
len
<*x, y*>)
+ 1)) by
Th44
.= (
Seg ((
len
<*x, y*>)
+ (
len
<*z*>))) by
Th39;
A10: for k st k
in (
dom
<*x, y*>) holds (p
. k)
= (
<*x, y*>
. k)
proof
let k such that
A11: k
in (
dom
<*x, y*>);
(
len
<*x, y*>)
= 2 by
Th44;
then
A12: k
in (
Seg 2) by
A11,
Def3;
A13: k
= 1 implies (p
. k)
= (
<*x, y*>
. k) by
A6,
Th44;
k
= 2 implies (p
. k)
= (
<*x, y*>
. k) by
A7,
Th44;
hence thesis by
A12,
A13,
Th2,
TARSKI:def 2;
end;
for k st k
in (
dom
<*z*>) holds (p
. ((
len
<*x, y*>)
+ k))
= (
<*z*>
. k)
proof
let k;
assume k
in (
dom
<*z*>);
then k
in
{1} by
Def8,
Th2;
then
A14: k
= 1 by
TARSKI:def 1;
hence (p
. ((
len
<*x, y*>)
+ k))
= (p
. (2
+ 1)) by
Th44
.= (
<*z*>
. k) by
A8,
A14,
Def8;
end;
hence thesis by
A9,
A10,
Def7;
end;
theorem ::
FINSEQ_1:46
Th46: for x be
object holds p
<>
{} implies ex q, x st p
= (q
^
<*x*>)
proof
let x be
object;
assume p
<>
{} ;
then
consider n be
Nat such that
A1: (
len p)
= (n
+ 1) by
NAT_1: 6;
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
reconsider q = (p
| (
Seg n)) as
FinSequence by
Th15;
take q;
take (p
. (
len p));
A2: (
dom q)
= ((
dom p)
/\ (
Seg n)) by
RELAT_1: 61
.= ((
Seg (
len p))
/\ (
Seg n)) by
Def3;
(
Seg n)
c= (
Seg (
len p)) by
Th5,
A1,
NAT_1: 11;
then
A3: (
dom q)
= (
Seg n) by
A2,
XBOOLE_1: 28;
A4: (
dom (q
^
<*(p
. (
len p))*>))
= (
Seg (
len (q
^
<*(p
. (
len p))*>))) by
Def3
.= (
Seg ((
len q)
+ (
len
<*(p
. (
len p))*>))) by
Th22
.= (
Seg ((
len q)
+ 1)) by
Th39
.= (
Seg (
len p)) by
A1,
A3,
Def3
.= (
dom p) by
Def3;
for x be
object st x
in (
dom p) holds (p
. x)
= ((q
^
<*(p
. (
len p))*>)
. x)
proof
let x be
object;
assume
A5: x
in (
dom p);
then
reconsider k = x as
Element of
NAT ;
k
in (
Seg (n
+ 1)) by
A1,
A5,
Def3;
then
A6: k
in ((
Seg n)
\/
{(n
+ 1)}) by
Th9;
A7:
now
assume
A8: k
in (
Seg n);
hence (p
. k)
= (q
. k) by
A3,
FUNCT_1: 47
.= ((q
^
<*(p
. (
len p))*>)
. k) by
A3,
A8,
Def7;
end;
now
assume
A9: k
in
{(n
+ 1)};
1
in (
Seg 1);
then
A10: 1
in (
dom
<*(p
. (
len p))*>) by
Def8;
thus ((q
^
<*(p
. (
len p))*>)
. k)
= ((q
^
<*(p
. (
len p))*>)
. (n
+ 1)) by
A9,
TARSKI:def 1
.= ((q
^
<*(p
. (
len p))*>)
. ((
len q)
+ 1)) by
A3,
Def3
.= (
<*(p
. (
len p))*>
. 1) by
A10,
Def7
.= (p
. (n
+ 1)) by
A1,
Def8
.= (p
. k) by
A9,
TARSKI:def 1;
end;
hence thesis by
A6,
A7,
XBOOLE_0:def 3;
end;
hence (q
^
<*(p
. (
len p))*>)
= p by
A4;
end;
definition
let D be non
empty
set;
let x be
Element of D;
:: original:
<*
redefine
func
<*x*> ->
FinSequence of D ;
coherence
proof
let y be
object;
assume y
in (
rng
<*x*>);
then y
in
{x} by
Th39;
then y
= x by
TARSKI:def 1;
hence thesis;
end;
end
scheme ::
FINSEQ_1:sch3
IndSeq { P[
FinSequence] } :
for p holds P[p]
provided
A1: P[
{} ]
and
A2: for p, x st P[p] holds P[(p
^
<*x*>)];
let p;
defpred
R[
set] means for p st (
len p)
= $1 holds P[p];
consider X be
Subset of
REAL such that
A3: for x be
Element of
REAL holds x
in X iff
R[x] from
SUBSET_1:sch 3;
for k holds k
in X
proof
A4:
0
in
REAL by
XREAL_0:def 1;
defpred
S[
Nat] means $1
in X;
for q st (
len q)
=
0 holds P[q] by
A1,
Lm3;
then
A5:
S[
0 ] by
A3,
A4;
now
let n such that
A6: n
in X;
A7: (n
+ 1)
in
REAL by
NUMBERS: 19;
now
let q;
assume
A8: (
len q)
= (n
+ 1);
then q
<>
{} ;
then
consider r, x such that
A9: q
= (r
^
<*x*>) by
Th46;
(
len q)
= ((
len r)
+ (
len
<*x*>)) by
A9,
Th22
.= ((
len r)
+ 1) by
Th39;
hence P[q] by
A2,
A9,
A3,
A6,
A8;
end;
hence (n
+ 1)
in X by
A3,
A7;
end;
then
A10: for n st
S[n] holds
S[(n
+ 1)];
thus for n holds
S[n] from
NAT_1:sch 2(
A5,
A10);
end;
then (
len p)
in X;
hence thesis by
A3;
end;
theorem ::
FINSEQ_1:47
for p,q,r,s be
FinSequence st (p
^ q)
= (r
^ s) & (
len p)
<= (
len r) holds ex t be
FinSequence st (p
^ t)
= r
proof
defpred
S[
FinSequence] means for p, q, s st (p
^ q)
= ($1
^ s) & (
len p)
<= (
len $1) holds ex t st (p
^ t)
= $1;
A1:
S[
{} ]
proof
let p, q, s;
assume that (p
^ q)
= (
{}
^ s) and
A2: (
len p)
<= (
len
{} );
take
{} ;
thus (p
^
{} )
= p by
Th34
.=
{} by
A2;
end;
A3: for r, x st
S[r] holds
S[(r
^
<*x*>)]
proof
let r, x;
assume
A4: for p, q, s st (p
^ q)
= (r
^ s) & (
len p)
<= (
len r) holds ex t st (p
^ t)
= r;
let p, q, s;
assume that
A5: (p
^ q)
= ((r
^
<*x*>)
^ s) and
A6: (
len p)
<= (
len (r
^
<*x*>));
A7:
now
assume (
len p)
= (
len (r
^
<*x*>));
then
A8: (
dom p)
= (
Seg (
len (r
^
<*x*>))) by
Def3
.= (
dom (r
^
<*x*>)) by
Def3;
A9: for k st k
in (
dom p) holds (p
. k)
= ((r
^
<*x*>)
. k)
proof
let k;
assume
A10: k
in (
dom p);
hence (p
. k)
= (((r
^
<*x*>)
^ s)
. k) by
A5,
Def7
.= ((r
^
<*x*>)
. k) by
A8,
A10,
Def7;
end;
(p
^
{} )
= p by
Th34
.= (r
^
<*x*>) by
A8,
A9;
hence thesis;
end;
now
assume (
len p)
<> (
len (r
^
<*x*>));
then (
len p)
<> ((
len r)
+ (
len
<*x*>)) by
Th22;
then
A11: (
len p)
<> ((
len r)
+ 1) by
Th39;
(
len p)
<= ((
len r)
+ (
len
<*x*>)) by
A6,
Th22;
then
A12: (
len p)
<= ((
len r)
+ 1) by
Th39;
(p
^ q)
= (r
^ (
<*x*>
^ s)) by
A5,
Th32;
then
consider t be
FinSequence such that
A13: (p
^ t)
= r by
A4,
A11,
A12,
NAT_1: 8;
(p
^ (t
^
<*x*>))
= (r
^
<*x*>) by
A13,
Th32;
hence thesis;
end;
hence thesis by
A7;
end;
for r holds
S[r] from
IndSeq(
A1,
A3);
hence thesis;
end;
registration
cluster ->
NAT
-defined for
FinSequence;
coherence
proof
let f be
FinSequence;
thus (
dom f)
c=
NAT ;
end;
end
definition
let D be
set;
::
FINSEQ_1:def11
func D
* ->
set means
:
Def11: x
in it iff x is
FinSequence of D;
existence
proof
defpred
P[
object] means $1 is
FinSequence of D;
consider X such that
A1: for x be
object holds x
in X iff x
in (
bool
[:
NAT , D:]) &
P[x] from
XBOOLE_0:sch 1;
take X;
let x;
thus x
in X implies x is
FinSequence of D by
A1;
assume x is
FinSequence of D;
then
reconsider p = x as
FinSequence of D;
p
c=
[:
NAT , D:];
hence thesis by
A1;
end;
uniqueness
proof
let D1,D2 be
set such that
A2: x
in D1 iff x is
FinSequence of D and
A3: x
in D2 iff x is
FinSequence of D;
now
let x be
object;
thus x
in D1 implies x
in D2
proof
assume x
in D1;
then x is
FinSequence of D by
A2;
hence thesis by
A3;
end;
assume x
in D2;
then x is
FinSequence of D by
A3;
hence x
in D1 by
A2;
end;
hence thesis by
TARSKI: 2;
end;
end
registration
let D be
set;
cluster (D
* ) -> non
empty;
coherence
proof
set f = the
FinSequence of D;
f
in (D
* ) by
Def11;
hence thesis;
end;
end
theorem ::
FINSEQ_1:48
(
rng p)
= (
rng q) & p is
one-to-one & q is
one-to-one implies (
len p)
= (
len q)
proof
defpred
P[
FinSequence] means $1 is
one-to-one implies for q st (
rng $1)
= (
rng q) & q is
one-to-one holds (
len $1)
= (
len q);
A1:
P[
{} ] by
RELAT_1: 41;
now
let p, x;
assume
A2: p is
one-to-one implies for q st (
rng p)
= (
rng q) & q is
one-to-one holds (
len p)
= (
len q);
assume
A3: (p
^
<*x*>) is
one-to-one;
let q;
assume that
A4: (
rng (p
^
<*x*>))
= (
rng q) and
A5: q is
one-to-one;
A6: (
rng (p
^
<*x*>))
= ((
rng p)
\/ (
rng
<*x*>)) by
Th31
.= ((
rng p)
\/
{x}) by
Th38;
x
in
{x} by
TARSKI:def 1;
then x
in (
rng q) by
A4,
A6,
XBOOLE_0:def 3;
then
consider y be
object such that
A7: y
in (
dom q) and
A8: x
= (q
. y) by
FUNCT_1:def 3;
A9: y
in (
Seg (
len q)) by
A7,
Def3;
reconsider y as
Element of
NAT by
A7;
A10: 1
<= y by
A9,
Th1;
then
consider k be
Nat such that
A11: (1
+ k)
= y by
NAT_1: 10;
A12: y
<= (
len q) by
A9,
Th1;
then
consider n be
Nat such that
A13: (y
+ n)
= (
len q) by
NAT_1: 10;
reconsider k, n as
Element of
NAT by
ORDINAL1:def 12;
reconsider q1 = (q
| (
Seg k)) as
FinSequence by
Th15;
defpred
P[
Nat,
object] means $2
= (q
. (y
+ $1));
A14: for j be
Nat st j
in (
Seg n) holds ex x st
P[j, x];
consider q2 be
FinSequence such that
A15: (
dom q2)
= (
Seg n) and
A16: for j be
Nat st j
in (
Seg n) holds
P[j, (q2
. j)] from
SeqEx(
A14);
A17: k
<= y by
A11,
NAT_1: 12;
then
A18: k
<= (
len q) by
A12,
XXREAL_0: 2;
then
A19: (
len q1)
= k by
Th17;
((
len (q1
^
<*x*>))
+ (
len q2))
= (((
len q1)
+ (
len
<*x*>))
+ (
len q2)) by
Th22
.= ((k
+ 1)
+ (
len q2)) by
A19,
Th39
.= (
len q) by
A11,
A13,
A15,
Def3;
then
A20: (
dom q)
= (
Seg ((
len (q1
^
<*x*>))
+ (
len q2))) by
Def3;
A21: (
rng (q1
^ q2))
= ((
rng q)
\
{x})
proof
thus (
rng (q1
^ q2))
c= ((
rng q)
\
{x})
proof
let z be
object;
assume z
in (
rng (q1
^ q2));
then
A22: z
in ((
rng q1)
\/ (
rng q2)) by
Th31;
A23:
now
assume
A24: z
in (
rng q1);
A25: (
rng q1)
= (q
.: (
Seg k)) & (q
.: (
Seg k))
c= (
rng q) by
RELAT_1: 111,
RELAT_1: 115;
consider y1 be
object such that
A26: y1
in (
dom q1) and
A27: (q1
. y1)
= z by
A24,
FUNCT_1:def 3;
A28: (q1
. y1)
= (q
. y1) by
A26,
FUNCT_1: 47;
A29: y1
in (
Seg (
len q1)) by
A26,
Def3;
reconsider y1 as
Element of
NAT by
A26;
A30: y1
<= k by
A19,
A29,
Th1;
A31: k
< y by
A11,
XREAL_1: 29;
(
Seg k)
c= (
Seg (
len q)) by
A17,
Th5,
A12,
XXREAL_0: 2;
then (
dom q1)
c= (
Seg (
len q)) by
A18,
Th17;
then (
dom q1)
c= (
dom q) by
Def3;
then x
<> z by
A5,
A7,
A8,
A26,
A27,
A28,
A30,
A31;
then not z
in
{x} by
TARSKI:def 1;
hence thesis by
A24,
A25,
XBOOLE_0:def 5;
end;
now
assume z
in (
rng q2);
then
consider y1 be
object such that
A32: y1
in (
dom q2) and
A33: (q2
. y1)
= z by
FUNCT_1:def 3;
reconsider y1 as
Element of
NAT by
A32;
A34: (q2
. y1)
= (q
. (y
+ y1)) by
A15,
A16,
A32;
A35: 1
<= (y
+ y1) by
A10,
NAT_1: 12;
y1
<= n by
A15,
A32,
Th1;
then (y
+ y1)
<= (
len q) by
A13,
XREAL_1: 7;
then (y
+ y1)
in (
Seg (
len q)) by
A35;
then
A36: (y
+ y1)
in (
dom q) by
Def3;
then
A37: z
in (
rng q) by
A33,
A34,
FUNCT_1:def 3;
y1
<>
0 by
A15,
A32,
Th1;
then y
<> (y
+ y1);
then x
<> z by
A5,
A7,
A8,
A33,
A34,
A36;
then not z
in
{x} by
TARSKI:def 1;
hence thesis by
A37,
XBOOLE_0:def 5;
end;
hence thesis by
A22,
A23,
XBOOLE_0:def 3;
end;
let z be
object;
assume
A38: z
in ((
rng q)
\
{x});
then
consider y1 be
object such that
A39: y1
in (
dom q) and
A40: z
= (q
. y1) by
FUNCT_1:def 3;
A41: y1
in (
Seg (
len q)) by
A39,
Def3;
reconsider y1 as
Element of
NAT by
A39;
not z
in
{x} by
A38,
XBOOLE_0:def 5;
then
A42: y
<> y1 by
A8,
A40,
TARSKI:def 1;
A43:
now
assume
A44: y
< y1;
then
consider j be
Nat such that
A45: y1
= (y
+ j) by
NAT_1: 10;
A46: 1
<= j by
A44,
A45,
NAT_1: 19;
j
<= n by
A13,
A41,
A45,
Th1,
XREAL_1: 6;
then
A47: j
in (
Seg n) by
A46;
then z
= (q2
. j) by
A16,
A40,
A45;
hence z
in (
rng q2) by
A15,
A47,
FUNCT_1:def 3;
end;
now
assume
A48: y1
< y;
A49: 1
<= y1 by
A41,
Th1;
y1
<= k by
A11,
A48,
NAT_1: 13;
then y1
in (
Seg k) by
A49;
then
A50: y1
in (
dom q1) by
A18,
Th17;
then (q1
. y1)
= z by
A40,
FUNCT_1: 47;
hence z
in (
rng q1) by
A50,
FUNCT_1:def 3;
end;
then z
in ((
rng q1)
\/ (
rng q2)) by
A42,
A43,
XBOOLE_0:def 3,
XXREAL_0: 1;
hence thesis by
Th31;
end;
A51: p
= ((p
^
<*x*>)
| (
dom p)) by
Th21;
A52: (
rng p)
= ((
rng (p
^
<*x*>))
\
{x})
proof
thus (
rng p)
c= ((
rng (p
^
<*x*>))
\
{x})
proof
let z be
object;
assume
A53: z
in (
rng p);
A54: (
rng p)
c= (
rng (p
^
<*x*>)) by
A51,
RELAT_1: 70;
consider y1 be
object such that
A55: y1
in (
dom p) and
A56: (p
. y1)
= z by
A53,
FUNCT_1:def 3;
A57: y1
in (
Seg (
len p)) by
A55,
Def3;
reconsider y1 as
Element of
NAT by
A55;
A58: ((p
^
<*x*>)
. ((
len p)
+ 1))
= x by
Th42;
A59: ((p
^
<*x*>)
. y1)
= (p
. y1) by
A51,
A55,
FUNCT_1: 47;
A60: y1
<= (
len p) by
A57,
Th1;
A61: (
len p)
< ((
len p)
+ 1) by
XREAL_1: 29;
A62: 1
<= y1 by
A57,
Th1;
y1
<= ((
len p)
+ 1) by
A60,
A61,
XXREAL_0: 2;
then
A63: y1
in (
Seg ((
len p)
+ 1)) by
A62;
A64: ((
len p)
+ 1)
in (
Seg ((
len p)
+ 1)) by
Th3;
A65: y1
in (
Seg ((
len p)
+ (
len
<*x*>))) by
A63,
Th40;
A66: ((
len p)
+ 1)
in (
Seg ((
len p)
+ (
len
<*x*>))) by
A64,
Th40;
A67: y1
in (
dom (p
^
<*x*>)) by
A65,
Def7;
((
len p)
+ 1)
in (
dom (p
^
<*x*>)) by
A66,
Def7;
then x
<> z by
A3,
A56,
A58,
A59,
A60,
A61,
A67;
then not z
in
{x} by
TARSKI:def 1;
hence thesis by
A53,
A54,
XBOOLE_0:def 5;
end;
let z be
object;
assume
A68: z
in ((
rng (p
^
<*x*>))
\
{x});
then
A69: z
in (
rng (p
^
<*x*>));
A70: not z
in
{x} by
A68,
XBOOLE_0:def 5;
z
in ((
rng p)
\/ (
rng
<*x*>)) by
A69,
Th31;
then z
in (
rng p) or z
in (
rng
<*x*>) by
XBOOLE_0:def 3;
hence thesis by
A70,
Th38;
end;
A71: (q1
^ q2) is
one-to-one
proof
let y1,y2 be
object;
assume that
A72: y1
in (
dom (q1
^ q2)) & y2
in (
dom (q1
^ q2)) and
A73: ((q1
^ q2)
. y1)
= ((q1
^ q2)
. y2);
reconsider m1 = y1, m2 = y2 as
Element of
NAT by
A72;
A74: q1 is
one-to-one by
A5,
FUNCT_1: 52;
A75:
now
assume
A76: m1
in (
dom q1) & m2
in (
dom q1);
then ((q1
^ q2)
. m1)
= (q1
. m1) & ((q1
^ q2)
. m2)
= (q1
. m2) by
Def7;
hence thesis by
A73,
A74,
A76;
end;
A77:
now
assume
A78: m1
in (
dom q1);
given j be
Nat such that
A79: j
in (
dom q2) and
A80: m2
= ((
len q1)
+ j);
A81: ((q1
^ q2)
. m2)
= (q2
. j) by
A79,
A80,
Def7;
((q1
^ q2)
. m1)
= (q1
. m1) & (q1
. m1)
= (q
. m1) by
A78,
Def7,
FUNCT_1: 47;
then
A82: (q
. m1)
= (q
. (y
+ j)) by
A15,
A16,
A73,
A79,
A81;
1
<= j by
A15,
A79,
Th1;
then
A83: 1
<= (y
+ j) by
NAT_1: 12;
j
<= n by
A15,
A79,
Th1;
then (y
+ j)
<= (
len q) by
A13,
XREAL_1: 7;
then (y
+ j)
in (
Seg (
len q)) by
A83;
then
A84: (y
+ j)
in (
dom q) by
Def3;
m1
in (
Seg k) by
A18,
A78,
Th17;
then
A85: m1
<= k by
Th1;
k
< y by
A11,
XREAL_1: 29;
then
A86: m1
< y by
A85,
XXREAL_0: 2;
(
dom q1)
c= (
dom q) & y
<= (y
+ j) by
NAT_1: 12,
RELAT_1: 60;
hence thesis by
A5,
A78,
A82,
A84,
A86;
end;
A87:
now
assume
A88: m2
in (
dom q1);
given j be
Nat such that
A89: j
in (
dom q2) and
A90: m1
= ((
len q1)
+ j);
A91: ((q1
^ q2)
. m1)
= (q2
. j) by
A89,
A90,
Def7;
((q1
^ q2)
. m2)
= (q1
. m2) & (q1
. m2)
= (q
. m2) by
A88,
Def7,
FUNCT_1: 47;
then
A92: (q
. m2)
= (q
. (y
+ j)) by
A15,
A16,
A73,
A89,
A91;
1
<= j by
A15,
A89,
Th1;
then
A93: 1
<= (y
+ j) by
NAT_1: 12;
j
<= n by
A15,
A89,
Th1;
then (y
+ j)
<= (
len q) by
A13,
XREAL_1: 7;
then (y
+ j)
in (
Seg (
len q)) by
A93;
then
A94: (y
+ j)
in (
dom q) by
Def3;
m2
in (
Seg k) by
A18,
A88,
Th17;
then
A95: m2
<= k by
Th1;
k
< y by
A11,
XREAL_1: 29;
then
A96: m2
< y by
A95,
XXREAL_0: 2;
(
dom q1)
c= (
dom q) & y
<= (y
+ j) by
NAT_1: 12,
RELAT_1: 60;
hence thesis by
A5,
A88,
A92,
A94,
A96;
end;
now
given j1 be
Nat such that
A97: j1
in (
dom q2) and
A98: m1
= ((
len q1)
+ j1);
given j2 be
Nat such that
A99: j2
in (
dom q2) and
A100: m2
= ((
len q1)
+ j2);
A101: ((q1
^ q2)
. m1)
= (q2
. j1) by
A97,
A98,
Def7;
A102: ((q1
^ q2)
. m2)
= (q2
. j2) by
A99,
A100,
Def7;
A103: ((q1
^ q2)
. m1)
= (q
. (y
+ j1)) by
A15,
A16,
A97,
A101;
A104: ((q1
^ q2)
. m2)
= (q
. (y
+ j2)) by
A15,
A16,
A99,
A102;
A105: 1
<= j1 by
A15,
A97,
Th1;
A106: 1
<= j2 by
A15,
A99,
Th1;
A107: 1
<= (y
+ j1) by
A105,
NAT_1: 12;
A108: 1
<= (y
+ j2) by
A106,
NAT_1: 12;
A109: j1
<= n by
A15,
A97,
Th1;
A110: j2
<= n by
A15,
A99,
Th1;
A111: (y
+ j1)
<= (
len q) by
A13,
A109,
XREAL_1: 7;
A112: (y
+ j2)
<= (
len q) by
A13,
A110,
XREAL_1: 7;
A113: (y
+ j1)
in (
Seg (
len q)) by
A107,
A111;
A114: (y
+ j2)
in (
Seg (
len q)) by
A108,
A112;
A115: (y
+ j1)
in (
dom q) by
A113,
Def3;
(y
+ j2)
in (
dom q) by
A114,
Def3;
then (y
+ j1)
= (y
+ j2) by
A5,
A73,
A103,
A104,
A115;
hence thesis by
A98,
A100;
end;
hence thesis by
A72,
A75,
A77,
A87,
Th25;
end;
A116:
now
let j be
Nat;
assume
A117: j
in (
dom (q1
^
<*x*>));
A118:
now
assume
A119: j
in (
dom q1);
then ((q1
^
<*x*>)
. j)
= (q1
. j) by
Def7;
hence (q
. j)
= ((q1
^
<*x*>)
. j) by
A119,
FUNCT_1: 47;
end;
now
given i be
Nat such that
A120: i
in (
dom
<*x*>) and
A121: j
= ((
len q1)
+ i);
i
in
{1} by
A120,
Th2,
Th38;
then i
= 1 by
TARSKI:def 1;
hence (q
. j)
= ((q1
^
<*x*>)
. j) by
A8,
A11,
A19,
A121,
Th42;
end;
hence (q
. j)
= ((q1
^
<*x*>)
. j) by
A117,
A118,
Th25;
end;
now
let j be
Nat;
assume j
in (
dom q2);
hence (q2
. j)
= (q
. (((
len q1)
+ 1)
+ j)) by
A11,
A15,
A16,
A19
.= (q
. (((
len q1)
+ (
len
<*x*>))
+ j)) by
Th39
.= (q
. ((
len (q1
^
<*x*>))
+ j)) by
Th22;
end;
then ((q1
^
<*x*>)
^ q2)
= q by
A20,
A116,
Def7;
then
A122: (
len q)
= ((
len (q1
^
<*x*>))
+ (
len q2)) by
Th22
.= (((
len
<*x*>)
+ (
len q1))
+ (
len q2)) by
Th22
.= ((1
+ (
len q1))
+ (
len q2)) by
Th40
.= (1
+ ((
len q1)
+ (
len q2)))
.= ((
len (q1
^ q2))
+ 1) by
Th22;
(
len (p
^
<*x*>))
= ((
len p)
+ (
len
<*x*>)) by
Th22
.= ((
len p)
+ 1) by
Th40;
hence (
len (p
^
<*x*>))
= (
len q) by
A2,
A3,
A4,
A21,
A51,
A52,
A71,
A122,
FUNCT_1: 52;
end;
then
A123: for p, x st
P[p] holds
P[(p
^
<*x*>)];
for p holds
P[p] from
IndSeq(
A1,
A123);
hence thesis;
end;
theorem ::
FINSEQ_1:49
{}
in (D
* )
proof
{}
= (
<*> D);
hence thesis by
Def11;
end;
scheme ::
FINSEQ_1:sch4
SepSeq { D() -> non
empty
set , P[
FinSequence] } :
ex X st for x holds x
in X iff ex p st p
in (D()
* ) & P[p] & x
= p;
defpred
R[
object] means ex p st P[p] & $1
= p;
consider Y such that
A1: for x be
object holds x
in Y iff x
in (D()
* ) &
R[x] from
XBOOLE_0:sch 1;
take Y;
x
in Y iff ex p st p
in (D()
* ) & P[p] & x
= p
proof
now
assume x
in Y;
then x
in (D()
* ) & ex p st P[p] & x
= p by
A1;
hence ex p st p
in (D()
* ) & P[p] & x
= p;
end;
hence thesis by
A1;
end;
hence thesis;
end;
definition
let IT be
Function;
::
FINSEQ_1:def12
attr IT is
FinSubsequence-like means
:
Def12: ex k st (
dom IT)
c= (
Seg k);
end
registration
cluster
FinSubsequence-like for
Function;
existence
proof
take
{} , (
len
{} );
thus thesis;
end;
end
definition
mode
FinSubsequence is
FinSubsequence-like
Function;
end
registration
cluster
FinSequence-like ->
FinSubsequence-like for
Function;
coherence ;
let p be
FinSubsequence, X be
set;
cluster (p
| X) ->
FinSubsequence-like;
coherence
proof
consider k such that
A1: (
dom p)
c= (
Seg k) by
Def12;
(
dom (p
| X))
c= (
dom p) by
RELAT_1: 60;
hence thesis by
A1,
XBOOLE_1: 1;
end;
cluster (X
|` p) ->
FinSubsequence-like;
coherence
proof
consider k such that
A2: (
dom p)
c= (
Seg k) by
Def12;
(
dom (X
|` p))
c= (
dom p) by
FUNCT_1: 56;
hence thesis by
A2,
XBOOLE_1: 1;
end;
end
registration
cluster ->
NAT
-defined for
FinSubsequence;
coherence
proof
let f be
FinSubsequence;
ex n st (
dom f)
c= (
Seg n) by
Def12;
hence (
dom f)
c=
NAT by
XBOOLE_1: 1;
end;
end
reserve p9 for
FinSubsequence;
definition
let X;
given k be
Nat such that
A1: X
c= (
Seg k);
::
FINSEQ_1:def13
func
Sgm X ->
FinSequence of
NAT means
:
Def13: (
rng it )
= X & for l,m,k1,k2 be
Nat st 1
<= l & l
< m & m
<= (
len it ) & k1
= (it
. l) & k2
= (it
. m) holds k1
< k2;
existence
proof
defpred
P[
Nat] means for X st X
c= (
Seg $1) holds ex p be
FinSequence of
NAT st (
rng p)
= X & for l,m,k1,k2 be
Nat st (1
<= l & l
< m & m
<= (
len p) & k1
= (p
. l) & k2
= (p
. m)) holds k1
< k2;
A2:
P[
0 ]
proof
let X;
assume
A3: X
c= (
Seg
0 );
take (
<*>
NAT );
thus (
rng (
<*>
NAT ))
= X by
A3;
thus thesis;
end;
A4: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat such that
A5: for X st X
c= (
Seg k) holds ex p be
FinSequence of
NAT st (
rng p)
= X & for l,m,k1,k2 be
Nat st 1
<= l & l
< m & m
<= (
len p) & k1
= (p
. l) & k2
= (p
. m) holds k1
< k2;
let X;
assume
A6: X
c= (
Seg (k
+ 1));
now
assume not X
c= (
Seg k);
then
consider x be
object such that
A7: x
in X and
A8: not x
in (
Seg k);
x
in (
Seg (k
+ 1)) by
A6,
A7;
then
reconsider n = x as
Element of
NAT ;
A9: n
= (k
+ 1)
proof
assume
A10: n
<> (k
+ 1);
A11: n
<= (k
+ 1) by
A6,
A7,
Th1;
A12: 1
<= n by
A6,
A7,
Th1;
n
<= k by
A10,
A11,
NAT_1: 8;
hence contradiction by
A8,
A12;
end;
set Y = (X
\
{(k
+ 1)});
A13: Y
c= (
Seg k)
proof
let x be
object;
assume
A14: x
in Y;
then
A15: x
in X;
A16: not x
in
{(k
+ 1)} by
A14,
XBOOLE_0:def 5;
A17: x
in (
Seg (k
+ 1)) by
A6,
A15;
A18: x
<> (k
+ 1) by
A16,
TARSKI:def 1;
reconsider m = x as
Element of
NAT by
A17;
A19: m
<= (k
+ 1) by
A6,
A15,
Th1;
A20: 1
<= m by
A6,
A15,
Th1;
m
<= k by
A18,
A19,
NAT_1: 8;
hence thesis by
A20;
end;
then
consider p be
FinSequence of
NAT such that
A21: (
rng p)
= Y and
A22: for l,m,k1,k2 be
Nat st 1
<= l & l
< m & m
<= (
len p) & k1
= (p
. l) & k2
= (p
. m) holds k1
< k2 by
A5;
consider q such that
A23: q
= (p
^
<*(k
+ 1)*>);
reconsider q as
FinSequence of
NAT by
A23;
A24: (
rng q)
= ((
rng p)
\/ (
rng
<*(k
+ 1)*>)) by
A23,
Th31
.= (Y
\/
{(k
+ 1)}) by
A21,
Th38
.= (X
\/
{(k
+ 1)}) by
XBOOLE_1: 39
.= X by
A7,
A9,
XBOOLE_1: 12,
ZFMISC_1: 31;
for l,m,k1,k2 be
Nat st 1
<= l & l
< m & m
<= (
len q) & k1
= (q
. l) & k2
= (q
. m) holds k1
< k2
proof
let l,m,k1,k2 be
Nat;
assume that
A25: 1
<= l and
A26: l
< m and
A27: m
<= (
len q) and
A28: k1
= (q
. l) and
A29: k2
= (q
. m);
l
< (
len (p
^
<*(k
+ 1)*>)) by
A23,
A26,
A27,
XXREAL_0: 2;
then l
< ((
len p)
+ (
len
<*(k
+ 1)*>)) by
Th22;
then l
< ((
len p)
+ 1) by
Th39;
then l
<= (
len p) by
NAT_1: 13;
then l
in (
Seg (
len p)) by
A25;
then
A30: l
in (
dom p) by
Def3;
A31: 1
<= m by
A25,
A26,
XXREAL_0: 2;
A32:
now
assume
A33: m
= (
len q);
k1
= (p
. l) by
A23,
A28,
A30,
Def7;
then k1
in Y by
A21,
A30,
FUNCT_1:def 3;
then
A34: k1
<= k by
A13,
Th1;
(q
. m)
= ((p
^
<*(k
+ 1)*>)
. ((
len p)
+ (
len
<*(k
+ 1)*>))) by
A23,
A33,
Th22
.= ((p
^
<*(k
+ 1)*>)
. ((
len p)
+ 1)) by
Th39
.= (k
+ 1) by
Th42;
hence thesis by
A29,
A34,
NAT_1: 13;
end;
now
assume m
<> (
len q);
then m
< (
len (p
^
<*(k
+ 1)*>)) by
A23,
A27,
XXREAL_0: 1;
then m
< ((
len p)
+ (
len
<*(k
+ 1)*>)) by
Th22;
then m
< ((
len p)
+ 1) by
Th39;
then
A35: m
<= (
len p) by
NAT_1: 13;
then m
in (
Seg (
len p)) by
A31;
then m
in (
dom p) by
Def3;
then
A36: k2
= (p
. m) by
A23,
A29,
Def7;
k1
= (p
. l) by
A23,
A28,
A30,
Def7;
hence thesis by
A22,
A25,
A26,
A35,
A36;
end;
hence thesis by
A32;
end;
hence thesis by
A24;
end;
hence thesis by
A5;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A2,
A4);
hence thesis by
A1;
end;
uniqueness
proof
let p,q be
FinSequence of
NAT such that
A37: ((
rng p)
= X & for l,m,k1,k2 be
Nat st 1
<= l & l
< m & m
<= (
len p) & k1
= (p
. l) & k2
= (p
. m) holds k1
< k2) & ((
rng q)
= X & for l,m,k1,k2 be
Nat st 1
<= l & l
< m & m
<= (
len q) & k1
= (q
. l) & k2
= (q
. m) holds k1
< k2);
defpred
S[
FinSequence] means for X st ex k be
Nat st X
c= (
Seg k) holds ($1 is
FinSequence of
NAT & (
rng $1)
= X & for l,m,k1,k2 be
Nat st (1
<= l & l
< m & m
<= (
len $1) & k1
= ($1
. l) & k2
= ($1
. m)) holds k1
< k2) implies for q be
FinSequence of
NAT st (
rng q)
= X & for l,m,k1,k2 be
Nat st (1
<= l & l
< m & m
<= (
len q) & k1
= (q
. l) & k2
= (q
. m)) holds k1
< k2 holds q
= $1;
A38:
S[
{} ];
A39: for p, x st
S[p] holds
S[(p
^
<*x*>)]
proof
let p, x;
assume
A40:
S[p];
let X;
given k be
Nat such that
A41: X
c= (
Seg k);
assume that
A42: (p
^
<*x*>) is
FinSequence of
NAT and
A43: (
rng (p
^
<*x*>))
= X and
A44: for l,m,k1,k2 be
Nat st 1
<= l & l
< m & m
<= (
len (p
^
<*x*>)) & k1
= ((p
^
<*x*>)
. l) & k2
= ((p
^
<*x*>)
. m) holds k1
< k2;
let q be
FinSequence of
NAT ;
assume that
A45: (
rng q)
= X and
A46: for l,m,k1,k2 be
Nat st 1
<= l & l
< m & m
<= (
len q) & k1
= (q
. l) & k2
= (q
. m) holds k1
< k2;
1
in (
Seg 1);
then
A47: 1
in (
dom
<*x*>) by
Def8;
A48: ex m st m
= x & for l st l
in X & l
<> x holds l
< m
proof
<*x*> is
FinSequence of
NAT by
A42,
Th36;
then (
rng
<*x*>)
c=
NAT by
Def4;
then
{x}
c=
NAT by
Th38;
then
reconsider m = x as
Element of
NAT by
ZFMISC_1: 31;
take m;
thus m
= x;
thus for l st l
in X & l
<> x holds l
< m
proof
let l;
assume that
A49: l
in X and
A50: l
<> x;
consider y be
object such that
A51: y
in (
dom (p
^
<*x*>)) and
A52: l
= ((p
^
<*x*>)
. y) by
A43,
A49,
FUNCT_1:def 3;
A53: y
in (
Seg (
len (p
^
<*x*>))) by
A51,
Def3;
reconsider k = y as
Element of
NAT by
A51;
k
<= (
len (p
^
<*x*>)) by
A53,
Th1;
then k
<= ((
len p)
+ (
len
<*x*>)) by
Th22;
then
A54: k
<= ((
len p)
+ 1) by
Th39;
A55: k
<> ((
len p)
+ 1)
proof
assume k
= ((
len p)
+ 1);
then ((p
^
<*x*>)
. k)
= (
<*x*>
. 1) by
A47,
Def7
.= x by
Def8;
hence contradiction by
A50,
A52;
end;
A56: 1
<= k by
A53,
Th1;
k
< ((
len p)
+ 1) by
A54,
A55,
XXREAL_0: 1;
then k
< ((
len p)
+ (
len
<*x*>)) by
Th39;
then
A57: k
< (
len (p
^
<*x*>)) by
Th22;
m
= ((p
^
<*x*>)
. ((
len p)
+ 1)) by
Th42
.= ((p
^
<*x*>)
. ((
len p)
+ (
len
<*x*>))) by
Th39
.= ((p
^
<*x*>)
. (
len (p
^
<*x*>))) by
Th22;
hence thesis by
A44,
A52,
A56,
A57;
end;
end;
then
reconsider m = x as
Nat;
(
len q)
<>
0
proof
assume (
len q)
=
0 ;
then (p
^
<*x*>)
=
{} by
A43,
A45,
Lm3,
RELAT_1: 38;
then
0
= (
len (p
^
<*x*>))
.= ((
len p)
+ (
len
<*x*>)) by
Th22
.= (1
+ (
len p)) by
Th39;
hence contradiction;
end;
then
consider n be
Nat such that
A58: (
len q)
= (n
+ 1) by
NAT_1: 6;
deffunc
F(
Nat) = (q
. $1);
ex q9 be
FinSequence st (
len q9)
= n & for m st m
in (
dom q9) holds (q9
. m)
=
F(m) from
SeqLambda;
then
consider q9 be
FinSequence such that
A59: (
len q9)
= n and
A60: for m st m
in (
dom q9) holds (q9
. m)
= (q
. m);
now
let x be
object;
assume x
in (
rng q9);
then
consider y be
object such that
A61: y
in (
dom q9) and
A62: x
= (q9
. y) by
FUNCT_1:def 3;
A63: y
in (
Seg (
len q9)) by
A61,
Def3;
reconsider y as
Element of
NAT by
A61;
A64: y
<= n by
A59,
A63,
Th1;
A65: n
<= (n
+ 1) by
NAT_1: 11;
A66: 1
<= y by
A63,
Th1;
y
<= (n
+ 1) by
A64,
A65,
XXREAL_0: 2;
then y
in (
Seg (n
+ 1)) by
A66;
then y
in (
dom q) by
A58,
Def3;
then
A67: (q
. y)
in (
rng q) by
FUNCT_1:def 3;
(
rng q)
c=
NAT by
Def4;
then (q
. y)
in
NAT by
A67;
hence x
in
NAT by
A60,
A61,
A62;
end;
then
reconsider f = q9 as
FinSequence of
NAT by
Def4,
TARSKI:def 3;
A68: (
dom q)
= (
Seg (n
+ 1)) by
A58,
Def3
.= (
Seg ((
len q9)
+ (
len
<*x*>))) by
A59,
Th39;
A69: for m st m
in (
dom
<*x*>) holds (q
. ((
len q9)
+ m))
= (
<*x*>
. m)
proof
let m;
assume m
in (
dom
<*x*>);
then
A70: m
in
{1} by
Def8,
Th2;
then
A71: m
= 1 by
TARSKI:def 1;
(q
. ((
len q9)
+ m))
= x
proof
assume (q
. ((
len q9)
+ m))
<> x;
then
A72: (q
. (
len q))
<> x by
A58,
A59,
A70,
TARSKI:def 1;
consider d be
Nat such that
A73: d
= x and
A74: for l st l
in X & l
<> x holds l
< d by
A48;
x
in
{x} by
TARSKI:def 1;
then x
in (
rng
<*x*>) by
Th38;
then x
in ((
rng p)
\/ (
rng
<*x*>)) by
XBOOLE_0:def 3;
then x
in (
rng q) by
A43,
A45,
Th31;
then
consider y be
object such that
A75: y
in (
dom q) and
A76: x
= (q
. y) by
FUNCT_1:def 3;
A77: y
in (
Seg (
len q)) by
A75,
Def3;
reconsider y as
Element of
NAT by
A75;
A78: 1
<= y by
A77,
Th1;
A79: y
<= (
len q) by
A77,
Th1;
then
A80: y
< (
len q) by
A72,
A76,
XXREAL_0: 1;
1
<= (
len q) by
A78,
A79,
XXREAL_0: 2;
then (
len q)
in (
Seg (
len q));
then
A81: (
len q)
in (
dom q) by
Def3;
A82: (q
. (
len q))
in X by
A45,
A81,
FUNCT_1:def 3;
reconsider k = (q
. (
len q)) as
Nat;
k
< d by
A72,
A74,
A82;
hence contradiction by
A46,
A73,
A76,
A78,
A80;
end;
hence thesis by
A71,
Th40;
end;
then
A83: (q9
^
<*x*>)
= q by
A60,
A68,
Def7;
A84: not x
in (
rng p)
proof
assume x
in (
rng p);
then
consider y be
object such that
A85: y
in (
dom p) and
A86: x
= (p
. y) by
FUNCT_1:def 3;
A87: y
in (
Seg (
len p)) by
A85,
Def3;
reconsider y as
Element of
NAT by
A85;
A88: y
<= (
len p) by
A87,
Th1;
A89: ((
len p)
+ 1)
= ((
len p)
+ (
len
<*x*>)) by
Th39
.= (
len (p
^
<*x*>)) by
Th22;
A90: 1
<= y by
A87,
Th1;
A91: y
< ((
len p)
+ 1) by
A88,
NAT_1: 13;
A92: m
= ((p
^
<*x*>)
. y) by
A85,
A86,
Def7;
m
= ((p
^
<*x*>)
. ((
len p)
+ 1)) by
Th42;
hence contradiction by
A44,
A89,
A90,
A91,
A92;
end;
A93: X
= ((
rng p)
\/ (
rng
<*x*>)) by
A43,
Th31
.= ((
rng p)
\/
{x}) by
Th39;
A94: for z be
object holds z
in (((
rng p)
\/
{x})
\
{x}) iff z
in (
rng p)
proof
let z be
object;
thus z
in (((
rng p)
\/
{x})
\
{x}) implies z
in (
rng p)
proof
assume
A95: z
in (((
rng p)
\/
{x})
\
{x});
then not z
in
{x} by
XBOOLE_0:def 5;
hence thesis by
A95,
XBOOLE_0:def 3;
end;
assume z
in (
rng p);
then ( not z
in
{x}) & z
in ((
rng p)
\/
{x}) by
A84,
TARSKI:def 1,
XBOOLE_0:def 3;
hence thesis by
XBOOLE_0:def 5;
end;
A96: for l,m,k1,k2 be
Nat st 1
<= l & l
< m & m
<= (
len p) & k1
= (p
. l) & k2
= (p
. m) holds k1
< k2
proof
let l,m,k1,k2 be
Nat;
assume that
A97: 1
<= l and
A98: l
< m and
A99: m
<= (
len p) and
A100: k1
= (p
. l) and
A101: k2
= (p
. m);
l
<= (
len p) by
A98,
A99,
XXREAL_0: 2;
then l
in (
Seg (
len p)) by
A97;
then l
in (
dom p) by
Def3;
then
A102: k1
= ((p
^
<*x*>)
. l) by
A100,
Def7;
1
<= m by
A97,
A98,
XXREAL_0: 2;
then m
in (
Seg (
len p)) by
A99;
then m
in (
dom p) by
Def3;
then
A103: k2
= ((p
^
<*x*>)
. m) by
A101,
Def7;
(
len p)
<= ((
len p)
+ 1) by
NAT_1: 11;
then m
<= ((
len p)
+ 1) by
A99,
XXREAL_0: 2;
then m
<= ((
len p)
+ (
len
<*x*>)) by
Th39;
then m
<= (
len (p
^
<*x*>)) by
Th22;
hence thesis by
A44,
A97,
A98,
A102,
A103;
end;
A104: p is
FinSequence of
NAT by
A42,
Th36;
A105: (
rng p)
= (X
\
{x}) by
A93,
A94,
TARSKI: 2;
A106: not x
in (
rng f)
proof
assume x
in (
rng f);
then
consider y be
object such that
A107: y
in (
dom f) and
A108: x
= (f
. y) by
FUNCT_1:def 3;
A109: y
in (
Seg (
len f)) by
A107,
Def3;
reconsider y as
Element of
NAT by
A107;
A110: y
<= (
len f) by
A109,
Th1;
A111: ((
len f)
+ 1)
= ((
len f)
+ (
len
<*x*>)) by
Th39
.= (
len (f
^
<*x*>)) by
Th22;
A112: 1
<= y by
A109,
Th1;
A113: y
< ((
len f)
+ 1) by
A110,
NAT_1: 13;
A114: m
= (q
. y) by
A60,
A107,
A108;
m
= (q
. ((
len f)
+ 1)) by
A83,
Th42;
hence contradiction by
A46,
A83,
A111,
A112,
A113,
A114;
end;
A115: X
= ((
rng f)
\/ (
rng
<*x*>)) by
A45,
A83,
Th31
.= ((
rng f)
\/
{x}) by
Th39;
A116: for z be
object holds z
in (((
rng f)
\/
{x})
\
{x}) iff z
in (
rng f)
proof
let z be
object;
thus z
in (((
rng f)
\/
{x})
\
{x}) implies z
in (
rng f)
proof
assume
A117: z
in (((
rng f)
\/
{x})
\
{x});
then not z
in
{x} by
XBOOLE_0:def 5;
hence thesis by
A117,
XBOOLE_0:def 3;
end;
assume z
in (
rng f);
then ( not z
in
{x}) & z
in ((
rng f)
\/
{x}) by
A106,
TARSKI:def 1,
XBOOLE_0:def 3;
hence thesis by
XBOOLE_0:def 5;
end;
A118: for l,m,k1,k2 be
Nat st 1
<= l & l
< m & m
<= (
len f) & k1
= (f
. l) & k2
= (f
. m) holds k1
< k2
proof
let l,m,k1,k2 be
Nat;
assume that
A119: 1
<= l and
A120: l
< m and
A121: m
<= (
len f) and
A122: k1
= (f
. l) and
A123: k2
= (f
. m);
A124: m
<= (
len q) by
A58,
A59,
A121,
NAT_1: 13;
l
<= n by
A59,
A120,
A121,
XXREAL_0: 2;
then
A125: l
in (
Seg n) by
A119;
1
<= m by
A119,
A120,
XXREAL_0: 2;
then
A126: m
in (
Seg n) by
A59,
A121;
A127: l
in (
dom q9) by
A59,
A125,
Def3;
A128: m
in (
dom q9) by
A59,
A126,
Def3;
A129: k1
= (q
. l) by
A60,
A122,
A127;
k2
= (q
. m) by
A60,
A123,
A128;
hence thesis by
A46,
A119,
A120,
A124,
A129;
end;
(
rng f)
= (X
\
{x}) by
A115,
A116,
TARSKI: 2;
then q9
= p by
A40,
A41,
A96,
A104,
A105,
A118,
XBOOLE_1: 1;
hence thesis by
A60,
A68,
A69,
Def7;
end;
for p holds
S[p] from
IndSeq(
A38,
A39);
hence thesis by
A1,
A37;
end;
end
theorem ::
FINSEQ_1:50
Th50: (
rng (
Sgm (
dom p9)))
= (
dom p9)
proof
ex k st (
dom p9)
c= (
Seg k) by
Def12;
hence thesis by
Def13;
end;
definition
let p9;
::
FINSEQ_1:def14
func
Seq p9 ->
Function equals (p9
* (
Sgm (
dom p9)));
coherence ;
end
registration
let p9;
cluster (
Seq p9) ->
FinSequence-like;
coherence
proof
(
rng (
Sgm (
dom p9)))
= (
dom p9) by
Th50;
then (
dom (p9
* (
Sgm (
dom p9))))
= (
dom (
Sgm (
dom p9))) by
RELAT_1: 27
.= (
Seg (
len (
Sgm (
dom p9)))) by
Def3;
hence thesis;
end;
end
theorem ::
FINSEQ_1:51
for X st ex k st X
c= (
Seg k) holds (
Sgm X)
=
{} iff X
=
{}
proof
let X;
given k such that
A1: X
c= (
Seg k);
thus (
Sgm X)
=
{} implies X
=
{}
proof
assume (
Sgm X)
=
{} ;
hence X
= (
rng
{} ) by
A1,
Def13
.=
{} ;
end;
assume X
=
{} ;
then (
rng (
Sgm X))
=
{} by
A1,
Def13;
hence thesis;
end;
begin
theorem ::
FINSEQ_1:52
D is
finite iff ex p st D
= (
rng p)
proof
thus D is
finite implies ex p st D
= (
rng p)
proof
given g be
Function such that
A1: (
rng g)
= D and
A2: (
dom g)
in
omega ;
reconsider n = (
dom g) as
Element of
NAT by
A2;
defpred
R[
object,
object] means
P[$2, $1];
A3: for x be
object st x
in (
Seg n) holds ex y be
object st
R[x, y]
proof
let x be
object;
assume
A4: x
in (
Seg n);
then
reconsider x as
Element of
NAT ;
x
>= 1 by
A4,
Th1;
then ex k be
Nat st x
= (1
+ k) by
NAT_1: 10;
hence thesis;
end;
consider f such that
A5: (
dom f)
= (
Seg n) and
A6: for x be
object st x
in (
Seg n) holds
R[x, (f
. x)] from
CLASSES1:sch 1(
A3);
A7: (
rng f)
= (
dom g)
proof
A8: n
= { k where k be
Nat : k
< n } by
AXIOMS: 4;
thus (
rng f)
c= (
dom g)
proof
let x be
object;
assume x
in (
rng f);
then
consider y be
object such that
A9: y
in (
dom f) and
A10: x
= (f
. y) by
FUNCT_1:def 3;
consider k such that
A11: x
= k and
A12: y
= (k
+ 1) by
A5,
A6,
A9,
A10;
(k
+ 1)
<= n by
A5,
A9,
A12,
Th1;
then k
< n by
NAT_1: 13;
hence thesis by
A8,
A11;
end;
let x be
object;
assume x
in (
dom g);
then
consider k be
Nat such that
A13: x
= k and
A14: k
< n by
A8;
1
<= (k
+ 1) & (k
+ 1)
<= n by
A14,
NAT_1: 11,
NAT_1: 13;
then
A15: (k
+ 1)
in (
Seg n);
then ex k1 st (f
. (k
+ 1))
= k1 & (k
+ 1)
= (k1
+ 1) by
A6;
hence thesis by
A5,
A13,
A15,
FUNCT_1:def 3;
end;
then (
dom (g
* f))
= (
Seg n) by
A5,
RELAT_1: 27;
then
reconsider p = (g
* f) as
FinSequence by
Def2;
take p;
thus thesis by
A1,
A7,
RELAT_1: 28;
end;
given p such that
A16: D
= (
rng p);
consider n such that
A17: (
dom p)
= (
Seg n) by
Def2;
A18: n
= { k where k be
Nat : k
< n } by
AXIOMS: 4;
A19: for x be
object st x
in n holds ex y be
object st
P[x, y]
proof
let x be
object;
assume x
in n;
then ex k be
Nat st x
= k & k
< n by
A18;
then
reconsider k = x as
Nat;
take (k
+ 1);
thus thesis;
end;
consider f such that
A20: (
dom f)
= n and
A21: for x be
object st x
in n holds
P[x, (f
. x)] from
CLASSES1:sch 1(
A19);
take (p
* f);
A22: (
rng f)
= (
dom p)
proof
thus (
rng f)
c= (
dom p)
proof
let x be
object;
assume x
in (
rng f);
then
consider y be
object such that
A23: y
in (
dom f) and
A24: x
= (f
. y) by
FUNCT_1:def 3;
consider k such that
A25: y
= k and
A26: x
= (k
+ 1) by
A20,
A21,
A23,
A24;
ex m be
Nat st k
= m & m
< n by
A18,
A20,
A23,
A25;
then 1
<= (k
+ 1) & (k
+ 1)
<= n by
NAT_1: 11,
NAT_1: 13;
hence thesis by
A17,
A26;
end;
let x be
object;
assume
A27: x
in (
dom p);
then
reconsider x as
Element of
NAT ;
1
<= x by
A17,
A27,
Th1;
then
consider m be
Nat such that
A28: x
= (1
+ m) by
NAT_1: 10;
x
<= n by
A17,
A27,
Th1;
then m
< n by
A28,
NAT_1: 13;
then
A29: m
in n by
A18;
then ex k st m
= k & (f
. m)
= (k
+ 1) by
A21;
hence thesis by
A20,
A28,
A29,
FUNCT_1:def 3;
end;
hence (
rng (p
* f))
= D by
A16,
RELAT_1: 28;
(
dom (p
* f))
= (
dom f) by
A22,
RELAT_1: 27;
hence thesis by
A20,
ORDINAL1:def 12;
end;
begin
theorem ::
FINSEQ_1:53
((
Seg n),(
Seg m))
are_equipotent implies n
= m
proof
defpred
P[
Nat] means ex n st ((
Seg n),(
Seg $1))
are_equipotent & n
<> $1;
assume ((
Seg n),(
Seg m))
are_equipotent & n
<> m;
then
A1: ex m be
Nat st
P[m];
consider m be
Nat such that
A2:
P[m] and
A3: for k be
Nat st
P[k] holds m
<= k from
NAT_1:sch 5(
A1);
consider n such that
A4: ((
Seg n),(
Seg m))
are_equipotent and
A5: n
<> m by
A2;
A6: ex f st f is
one-to-one & (
dom f)
= (
Seg n) & (
rng f)
= (
Seg m) by
A4;
A7:
now
assume m
=
0 ;
then (
Seg m)
=
{} ;
then (
Seg m)
= (
Seg n) by
A6,
RELAT_1: 42;
hence contradiction by
A5,
Th6;
end;
then
consider m1 be
Nat such that
A8: m
= (m1
+ 1) by
NAT_1: 6;
A9:
now
assume n
=
0 ;
then (
Seg n)
=
{} ;
then (
Seg m)
= (
Seg n) by
A6,
RELAT_1: 42;
hence contradiction by
A5,
Th6;
end;
then
consider n1 be
Nat such that
A10: n
= (n1
+ 1) by
NAT_1: 6;
A11: n
in (
Seg n) by
A9,
Th3;
A12: m
in (
Seg m) by
A7,
Th3;
A13: not (n1
+ 1)
<= n1 by
NAT_1: 13;
A14: not (m1
+ 1)
<= m1 by
NAT_1: 13;
A15: not n
in (
Seg n1) by
A10,
A13,
Th1;
A16: not m
in (
Seg m1) by
A8,
A14,
Th1;
A17: ((
Seg n1)
/\
{n})
c=
{}
proof
let x be
object;
assume x
in ((
Seg n1)
/\
{n});
then x
in (
Seg n1) & x
in
{n} by
XBOOLE_0:def 4;
hence thesis by
A15,
TARSKI:def 1;
end;
A18: ((
Seg m1)
/\
{m})
c=
{}
proof
let x be
object;
assume x
in ((
Seg m1)
/\
{m});
then x
in (
Seg m1) & x
in
{m} by
XBOOLE_0:def 4;
hence thesis by
A16,
TARSKI:def 1;
end;
A19: (
Seg n)
= ((
Seg n1)
\/
{n}) by
A10,
Th9;
A20: (
Seg m)
= ((
Seg m1)
\/
{m}) by
A8,
Th9;
A21: ((
Seg n1)
/\
{n})
=
{} by
A17;
A22: ((
Seg m1)
/\
{m})
=
{} by
A18;
A23: ((
Seg n1)
\
{n})
= (((
Seg n1)
\/
{n})
\
{n}) & (
Seg n1)
misses
{n} by
A21,
XBOOLE_1: 40;
A24: ((
Seg m1)
\
{m})
= (((
Seg m1)
\/
{m})
\
{m}) & (
Seg m1)
misses
{m} by
A22,
XBOOLE_1: 40;
A25: ((
Seg n)
\
{n})
= (
Seg n1) by
A19,
A23,
XBOOLE_1: 83;
((
Seg m)
\
{m})
= (
Seg m1) by
A20,
A24,
XBOOLE_1: 83;
hence contradiction by
A3,
A4,
A5,
A8,
A10,
A11,
A12,
A14,
A25,
CARD_1: 34;
end;
theorem ::
FINSEQ_1:54
((
Seg n),n)
are_equipotent by
Lm1;
theorem ::
FINSEQ_1:55
(
card (
Seg n))
= (
card n) by
Lm1,
CARD_1: 5;
theorem ::
FINSEQ_1:56
Th56: X is
finite implies ex n st (X,(
Seg n))
are_equipotent
proof
assume X is
finite;
then
reconsider n = (
card X) as
Nat;
A1: (X,n)
are_equipotent by
CARD_1:def 2;
take n;
(n,(
Seg n))
are_equipotent by
Lm1;
hence thesis by
A1,
WELLORD2: 15;
end;
theorem ::
FINSEQ_1:57
for n be
Nat holds (
card (
Seg n))
= n by
Lm1,
CARD_1:def 2;
begin
registration
let x be
object;
cluster
<*x*> -> non
empty;
coherence ;
end
registration
cluster non
empty for
FinSequence;
existence
proof
take
<*
0 *>;
thus thesis;
end;
end
registration
let f1 be
FinSequence, f2 be non
empty
FinSequence;
cluster (f1
^ f2) -> non
empty;
coherence by
Th35;
cluster (f2
^ f1) -> non
empty;
coherence by
Th35;
end
registration
let x,y be
object;
cluster
<*x, y*> -> non
empty;
coherence ;
let z be
object;
cluster
<*x, y, z*> -> non
empty;
coherence ;
end
scheme ::
FINSEQ_1:sch5
SeqDEx { D() -> non
empty
set , A() ->
Nat , P[
object,
object] } :
ex p be
FinSequence of D() st (
dom p)
= (
Seg A()) & for k st k
in (
Seg A()) holds P[k, (p
. k)]
provided
A1: for k st k
in (
Seg A()) holds ex x be
Element of D() st P[k, x];
A2: for y be
object st y
in (
Seg A()) holds ex x be
object st x
in D() & P[y, x]
proof
let y be
object;
assume
A3: y
in (
Seg A());
then
reconsider k = y as
Element of
NAT ;
consider x be
Element of D() such that
A4: P[k, x] by
A1,
A3;
take x;
thus thesis by
A4;
end;
consider f be
Function such that
A5: (
dom f)
= (
Seg A()) and
A6: (
rng f)
c= D() and
A7: for y be
object st y
in (
Seg A()) holds P[y, (f
. y)] from
FUNCT_1:sch 6(
A2);
reconsider f as
FinSequence by
A5,
Def2;
reconsider p = f as
FinSequence of D() by
A6,
Def4;
take p;
thus thesis by
A5,
A7;
end;
reserve D for
set,
p for
FinSequence of D,
m for
Nat;
definition
let m;
let p be
FinSequence;
::
FINSEQ_1:def15
func p
| m ->
FinSequence equals (p
| (
Seg m));
coherence by
Th15;
end
definition
let D, m, p;
:: original:
|
redefine
func p
| m ->
FinSequence of D ;
coherence by
Th18;
end
registration
let f be
FinSequence;
cluster (f
|
0 ) ->
empty;
coherence ;
end
theorem ::
FINSEQ_1:58
Th58: (
len q)
<= i implies (q
| i)
= q
proof
assume (
len q)
<= i;
then (
Seg (
len q))
c= (
Seg i) by
Th5;
then (
dom q)
c= (
Seg i) by
Def3;
hence thesis by
RELAT_1: 68;
end;
theorem ::
FINSEQ_1:59
Th59: i
<= (
len q) implies (
len (q
| i))
= i
proof
assume i
<= (
len q);
then (
Seg i)
c= (
Seg (
len q)) by
Th5;
then (
Seg i)
c= (
dom q) by
Def3;
then i
in
NAT & (
Seg i)
= (
dom (q
| i)) by
ORDINAL1:def 12,
RELAT_1: 62;
hence thesis by
Def3;
end;
registration
let f be non
empty
FinSequence;
reduce (
len (f
| 1)) to 1;
reducibility
proof
1
<= (
len f) by
NAT_1: 14;
hence thesis by
Th59;
end;
cluster (f
| 1) -> 1
-element;
coherence ;
end
registration
let p be non
empty
FinSequence, n be non
zero
Nat;
cluster (p
| n) -> non
empty;
coherence
proof
per cases ;
suppose n
<= (
len p);
then ((n
+ 1)
- 1)
<= ((
len p)
-
0 );
then (
len (p
| n))
= n by
Th59;
hence thesis;
end;
suppose (
len p)
<= n;
hence thesis by
Th58;
end;
end;
end
theorem ::
FINSEQ_1:60
i
in (
Seg n) implies (i
+ m)
in (
Seg (n
+ m))
proof
assume
A1: i
in (
Seg n);
then
A2: 1
<= i by
Th1;
A3: i
<= n by
A1,
Th1;
i
<= (i
+ m) by
NAT_1: 11;
then 1
<= (i
+ m) by
A2,
XXREAL_0: 2;
hence thesis by
A3,
Th1,
XREAL_1: 7;
end;
theorem ::
FINSEQ_1:61
i
>
0 & (i
+ m)
in (
Seg (n
+ m)) implies i
in (
Seg n) & i
in (
Seg (n
+ m))
proof
assume that
A1: i
>
0 and
A2: (i
+ m)
in (
Seg (n
+ m));
1
= (
0
+ 1);
then
A3: 1
<= i by
A1,
NAT_1: 13;
A4: (i
+ m)
<= (n
+ m) by
A2,
Th1;
i
<= n by
A2,
Th1,
XREAL_1: 6;
hence i
in (
Seg n) by
A3;
i
<= (i
+ m) by
NAT_1: 11;
then i
<= (n
+ m) by
A4,
XXREAL_0: 2;
hence thesis by
A3;
end;
definition
let R be
Relation;
::
FINSEQ_1:def16
func R
[*] ->
Relation means for x,y be
object holds
[x, y]
in it iff x
in (
field R) & y
in (
field R) & ex p be
FinSequence st (
len p)
>= 1 & (p
. 1)
= x & (p
. (
len p))
= y & for i be
Nat st i
>= 1 & i
< (
len p) holds
[(p
. i), (p
. (i
+ 1))]
in R;
existence
proof
defpred
X[
object,
object] means ex p be
FinSequence st (
len p)
>= 1 & (p
. 1)
= $1 & (p
. (
len p))
= $2 & for i be
Nat st i
>= 1 & i
< (
len p) holds
[(p
. i), (p
. (i
+ 1))]
in R;
thus ex S be
Relation st for x,y be
object holds
[x, y]
in S iff x
in (
field R) & y
in (
field R) &
X[x, y] from
RELAT_1:sch 1;
end;
uniqueness
proof
let R1,R2 be
Relation such that
A1: for x,y be
object holds
[x, y]
in R1 iff x
in (
field R) & y
in (
field R) & ex p be
FinSequence st (
len p)
>= 1 & (p
. 1)
= x & (p
. (
len p))
= y & for i be
Nat st i
>= 1 & i
< (
len p) holds
[(p
. i), (p
. (i
+ 1))]
in R and
A2: for x,y be
object holds
[x, y]
in R2 iff x
in (
field R) & y
in (
field R) & ex p be
FinSequence st (
len p)
>= 1 & (p
. 1)
= x & (p
. (
len p))
= y & for i be
Nat st i
>= 1 & i
< (
len p) holds
[(p
. i), (p
. (i
+ 1))]
in R;
let x,y be
object;
thus
[x, y]
in R1 implies
[x, y]
in R2
proof
assume
A3:
[x, y]
in R1;
then
A4: x
in (
field R) & y
in (
field R) by
A1;
ex p be
FinSequence st (
len p)
>= 1 & (p
. 1)
= x & (p
. (
len p))
= y & for i be
Nat st i
>= 1 & i
< (
len p) holds
[(p
. i), (p
. (i
+ 1))]
in R by
A1,
A3;
hence thesis by
A2,
A4;
end;
assume
A5:
[x, y]
in R2;
then
A6: x
in (
field R) & y
in (
field R) by
A2;
ex p be
FinSequence st (
len p)
>= 1 & (p
. 1)
= x & (p
. (
len p))
= y & for i be
Nat st i
>= 1 & i
< (
len p) holds
[(p
. i), (p
. (i
+ 1))]
in R by
A2,
A5;
hence thesis by
A1,
A6;
end;
end
theorem ::
FINSEQ_1:62
for D1,D2 be
set st D1
c= D2 holds (D1
* )
c= (D2
* )
proof
let D1,D2 be
set such that
A1: D1
c= D2;
let x be
object;
assume x
in (D1
* );
then
reconsider p = x as
FinSequence of D1 by
Def11;
(
rng p)
c= D1 by
Def4;
then x is
FinSequence of D2 by
Def4,
A1,
XBOOLE_1: 1;
hence thesis by
Def11;
end;
registration
let D be
set;
cluster (D
* ) ->
functional;
coherence by
Def11;
end
theorem ::
FINSEQ_1:63
for p,q be
FinSequence st p
c= q holds (
len p)
<= (
len q)
proof
let p,q be
FinSequence;
assume p
c= q;
then (
Segm (
card p))
c= (
Segm (
card q)) by
CARD_1: 11;
hence thesis by
NAT_1: 39;
end;
theorem ::
FINSEQ_1:64
for p,q be
FinSequence, i be
Nat st 1
<= i & i
<= (
len p) holds ((p
^ q)
. i)
= (p
. i)
proof
let p,q be
FinSequence, i be
Nat;
assume
A1: 1
<= i & i
<= (
len p);
i
in
NAT & (
Seg (
len p))
= (
dom p) by
Def3,
ORDINAL1:def 12;
then i
in (
dom p) by
A1;
hence thesis by
Def7;
end;
theorem ::
FINSEQ_1:65
for p,q be
FinSequence, i be
Nat st 1
<= i & i
<= (
len q) holds ((p
^ q)
. ((
len p)
+ i))
= (q
. i)
proof
let p,q be
FinSequence, i be
Nat;
assume 1
<= i & i
<= (
len q);
then ((
len p)
+ 1)
<= ((
len p)
+ i) & ((
len p)
+ i)
<= ((
len p)
+ (
len q)) by
XREAL_1: 6;
hence ((p
^ q)
. ((
len p)
+ i))
= (q
. (((
len p)
+ i)
- (
len p))) by
Th23
.= (q
. i);
end;
scheme ::
FINSEQ_1:sch6
FinSegRng { n() ->
Nat , F(
set) ->
set , P[
set] } :
{ F(i) where i be
Nat : i
<= n() & P[i] } is
finite;
set F = { F(i) where i be
Nat : i
<= n() & P[i] };
deffunc
G(
Nat) = F(-);
consider f be
FinSequence such that
A1: (
len f)
= (n()
+ 1) and
A2: for k st k
in (
dom f) holds (f
. k)
=
G(k) from
SeqLambda;
F
c= (
rng f)
proof
let x be
object;
assume x
in F;
then
consider j be
Nat such that
A3: x
= F(j) and
A4: j
<= n() and P[j];
1
<= (j
+ 1) & (j
+ 1)
<= (n()
+ 1) by
A4,
NAT_1: 11,
XREAL_1: 6;
then (j
+ 1)
in (
Seg (n()
+ 1));
then
A5: (j
+ 1)
in (
dom f) by
A1,
Def3;
then (f
. (j
+ 1))
= F(-) by
A2
.= F(j);
hence thesis by
A3,
A5,
FUNCT_1:def 3;
end;
hence thesis;
end;
Lm5: x
in (
Seg n) implies x
= 1 or ... or x
= n
proof
assume
A1: x
in (
Seg n);
then
reconsider k = x as
Nat;
1
<= k & k
<= n by
A1,
Th1;
hence thesis;
end;
theorem ::
FINSEQ_1:66
Th66: for x1,x2,x3,x4 be
set, p be
FinSequence st p
= (((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>) holds (
len p)
= 4 & (p
. 1)
= x1 & (p
. 2)
= x2 & (p
. 3)
= x3 & (p
. 4)
= x4
proof
let x1,x2,x3,x4 be
set, p be
FinSequence;
assume
A1: p
= (((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>);
set p13 = ((
<*x1*>
^
<*x2*>)
^
<*x3*>);
A2: p13
=
<*x1, x2, x3*>;
then
A3: (
len p13)
= 3 by
Th45;
A4: (p13
. 1)
= x1 & (p13
. 2)
= x2 by
A2,
Th45;
A5: (p13
. 3)
= x3 by
A2,
Th45;
thus (
len p)
= ((
len p13)
+ (
len
<*x4*>)) by
A1,
Th22
.= (3
+ 1) by
A3,
Th40
.= 4;
A6: (
dom p13)
= (
Seg 3) by
A3,
Def3;
1
in (
Seg 3) & ... & 3
in (
Seg 3);
hence (p
. 1)
= x1 & (p
. 2)
= x2 & (p
. 3)
= x3 by
A1,
A4,
A5,
Def7,
A6;
thus (p
. 4)
= (p
. ((
len p13)
+ 1)) by
A3
.= x4 by
A1,
Th42;
end;
theorem ::
FINSEQ_1:67
Th67: for x1,x2,x3,x4,x5 be
set, p be
FinSequence st p
= ((((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>)
^
<*x5*>) holds (
len p)
= 5 & (p
. 1)
= x1 & (p
. 2)
= x2 & (p
. 3)
= x3 & (p
. 4)
= x4 & (p
. 5)
= x5
proof
let x1,x2,x3,x4,x5 be
set, p be
FinSequence;
assume
A1: p
= ((((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>)
^
<*x5*>);
set p14 = (((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>);
A2: (
len p14)
= 4 by
Th66;
A3: (p14
. 1)
= x1 & (p14
. 2)
= x2 by
Th66;
A4: (p14
. 3)
= x3 & (p14
. 4)
= x4 by
Th66;
thus (
len p)
= ((
len p14)
+ (
len
<*x5*>)) by
A1,
Th22
.= (4
+ 1) by
A2,
Th40
.= 5;
A5: (
dom p14)
= (
Seg 4) by
A2,
Def3;
1
in (
Seg 4) & ... & 4
in (
Seg 4);
hence (p
. 1)
= x1 & (p
. 2)
= x2 & (p
. 3)
= x3 & (p
. 4)
= x4 by
A1,
A3,
A4,
Def7,
A5;
thus (p
. 5)
= (p
. ((
len p14)
+ 1)) by
A2
.= x5 by
A1,
Th42;
end;
theorem ::
FINSEQ_1:68
Th68: for x1,x2,x3,x4,x5,x6 be
set, p be
FinSequence st p
= (((((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>)
^
<*x5*>)
^
<*x6*>) holds (
len p)
= 6 & (p
. 1)
= x1 & (p
. 2)
= x2 & (p
. 3)
= x3 & (p
. 4)
= x4 & (p
. 5)
= x5 & (p
. 6)
= x6
proof
let x1,x2,x3,x4,x5,x6 be
set, p be
FinSequence;
assume
A1: p
= (((((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>)
^
<*x5*>)
^
<*x6*>);
set p15 = ((((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>)
^
<*x5*>);
A2: (
len p15)
= 5 by
Th67;
A3: (p15
. 1)
= x1 & (p15
. 2)
= x2 by
Th67;
A4: (p15
. 3)
= x3 & (p15
. 4)
= x4 by
Th67;
A5: (p15
. 5)
= x5 by
Th67;
thus (
len p)
= ((
len p15)
+ (
len
<*x6*>)) by
A1,
Th22
.= (5
+ 1) by
A2,
Th40
.= 6;
A6: (
dom p15)
= (
Seg 5) by
A2,
Def3;
1
in (
Seg 5) & ... & 5
in (
Seg 5);
hence (p
. 1)
= x1 & (p
. 2)
= x2 & (p
. 3)
= x3 & (p
. 4)
= x4 & (p
. 5)
= x5 by
A1,
A3,
A4,
A5,
Def7,
A6;
thus (p
. 6)
= (p
. ((
len p15)
+ 1)) by
A2
.= x6 by
A1,
Th42;
end;
theorem ::
FINSEQ_1:69
Th69: for x1,x2,x3,x4,x5,x6,x7 be
set, p be
FinSequence st p
= ((((((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>)
^
<*x5*>)
^
<*x6*>)
^
<*x7*>) holds (
len p)
= 7 & (p
. 1)
= x1 & (p
. 2)
= x2 & (p
. 3)
= x3 & (p
. 4)
= x4 & (p
. 5)
= x5 & (p
. 6)
= x6 & (p
. 7)
= x7
proof
let x1,x2,x3,x4,x5,x6,x7 be
set, p be
FinSequence;
assume
A1: p
= ((((((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>)
^
<*x5*>)
^
<*x6*>)
^
<*x7*>);
set p16 = (((((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>)
^
<*x5*>)
^
<*x6*>);
A2: (
len p16)
= 6 by
Th68;
A3: (p16
. 1)
= x1 & (p16
. 2)
= x2 by
Th68;
A4: (p16
. 3)
= x3 & (p16
. 4)
= x4 by
Th68;
A5: (p16
. 5)
= x5 & (p16
. 6)
= x6 by
Th68;
thus (
len p)
= ((
len p16)
+ (
len
<*x7*>)) by
A1,
Th22
.= (6
+ 1) by
A2,
Th40
.= 7;
A6: (
dom p16)
= (
Seg 6) by
A2,
Def3;
1
in (
Seg 6) & ... & 6
in (
Seg 6);
hence (p
. 1)
= x1 & (p
. 2)
= x2 & (p
. 3)
= x3 & (p
. 4)
= x4 & (p
. 5)
= x5 & (p
. 6)
= x6 by
A1,
A3,
A4,
A5,
Def7,
A6;
thus (p
. 7)
= (p
. ((
len p16)
+ 1)) by
A2
.= x7 by
A1,
Th42;
end;
theorem ::
FINSEQ_1:70
Th70: for x1,x2,x3,x4,x5,x6,x7,x8 be
set, p be
FinSequence st p
= (((((((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>)
^
<*x5*>)
^
<*x6*>)
^
<*x7*>)
^
<*x8*>) holds (
len p)
= 8 & (p
. 1)
= x1 & (p
. 2)
= x2 & (p
. 3)
= x3 & (p
. 4)
= x4 & (p
. 5)
= x5 & (p
. 6)
= x6 & (p
. 7)
= x7 & (p
. 8)
= x8
proof
let x1,x2,x3,x4,x5,x6,x7,x8 be
set, p be
FinSequence;
thus p
= (((((((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>)
^
<*x5*>)
^
<*x6*>)
^
<*x7*>)
^
<*x8*>) implies (
len p)
= 8 & (p
. 1)
= x1 & (p
. 2)
= x2 & (p
. 3)
= x3 & (p
. 4)
= x4 & (p
. 5)
= x5 & (p
. 6)
= x6 & (p
. 7)
= x7 & (p
. 8)
= x8
proof
assume
A1: p
= (((((((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>)
^
<*x5*>)
^
<*x6*>)
^
<*x7*>)
^
<*x8*>);
set p17 = ((((((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>)
^
<*x5*>)
^
<*x6*>)
^
<*x7*>);
A2: (
len p17)
= 7 by
Th69;
A3: (p17
. 1)
= x1 & (p17
. 2)
= x2 by
Th69;
A4: (p17
. 3)
= x3 & (p17
. 4)
= x4 by
Th69;
A5: (p17
. 5)
= x5 & (p17
. 6)
= x6 by
Th69;
A6: (p17
. 7)
= x7 by
Th69;
thus (
len p)
= ((
len p17)
+ (
len
<*x8*>)) by
A1,
Th22
.= (7
+ 1) by
A2,
Th40
.= 8;
A7: (
dom p17)
= (
Seg 7) by
A2,
Def3;
1
in (
Seg 7) & ... & 7
in (
Seg 7);
hence (p
. 1)
= x1 & (p
. 2)
= x2 & (p
. 3)
= x3 & (p
. 4)
= x4 & (p
. 5)
= x5 & (p
. 6)
= x6 & (p
. 7)
= x7 by
A1,
A3,
A4,
A5,
A6,
Def7,
A7;
thus (p
. 8)
= (p
. ((
len p17)
+ 1)) by
A2
.= x8 by
A1,
Th42;
end;
end;
theorem ::
FINSEQ_1:71
for x1,x2,x3,x4,x5,x6,x7,x8,x9 be
set, p be
FinSequence st p
= ((((((((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>)
^
<*x5*>)
^
<*x6*>)
^
<*x7*>)
^
<*x8*>)
^
<*x9*>) holds (
len p)
= 9 & (p
. 1)
= x1 & (p
. 2)
= x2 & (p
. 3)
= x3 & (p
. 4)
= x4 & (p
. 5)
= x5 & (p
. 6)
= x6 & (p
. 7)
= x7 & (p
. 8)
= x8 & (p
. 9)
= x9
proof
let x1,x2,x3,x4,x5,x6,x7,x8,x9 be
set, p be
FinSequence;
thus p
= ((((((((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>)
^
<*x5*>)
^
<*x6*>)
^
<*x7*>)
^
<*x8*>)
^
<*x9*>) implies (
len p)
= 9 & (p
. 1)
= x1 & (p
. 2)
= x2 & (p
. 3)
= x3 & (p
. 4)
= x4 & (p
. 5)
= x5 & (p
. 6)
= x6 & (p
. 7)
= x7 & (p
. 8)
= x8 & (p
. 9)
= x9
proof
assume
A1: p
= ((((((((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>)
^
<*x5*>)
^
<*x6*>)
^
<*x7*>)
^
<*x8*>)
^
<*x9*>);
set p17 = (((((((
<*x1*>
^
<*x2*>)
^
<*x3*>)
^
<*x4*>)
^
<*x5*>)
^
<*x6*>)
^
<*x7*>)
^
<*x8*>);
A2: (
len p17)
= 8 by
Th70;
A3: (p17
. 1)
= x1 & (p17
. 2)
= x2 by
Th70;
A4: (p17
. 3)
= x3 & (p17
. 4)
= x4 by
Th70;
A5: (p17
. 5)
= x5 & (p17
. 6)
= x6 by
Th70;
A6: (p17
. 7)
= x7 & (p17
. 8)
= x8 by
Th70;
thus (
len p)
= ((
len p17)
+ (
len
<*x9*>)) by
A1,
Th22
.= (8
+ 1) by
A2,
Th40
.= 9;
A7: (
dom p17)
= (
Seg 8) by
A2,
Def3;
1
in (
Seg 8) & ... & 8
in (
Seg 8);
hence (p
. 1)
= x1 & (p
. 2)
= x2 & (p
. 3)
= x3 & (p
. 4)
= x4 & (p
. 5)
= x5 & (p
. 6)
= x6 & (p
. 7)
= x7 & (p
. 8)
= x8 by
A1,
A3,
A4,
A5,
A6,
Def7,
A7;
thus (p
. 9)
= (p
. ((
len p17)
+ 1)) by
A2
.= x9 by
A1,
Th42;
end;
end;
theorem ::
FINSEQ_1:72
for p be
FinSequence holds (p
| (
Seg
0 ))
=
{} ;
theorem ::
FINSEQ_1:73
for f,g be
FinSequence holds (f
| (
Seg
0 ))
= (g
| (
Seg
0 ));
theorem ::
FINSEQ_1:74
for D be non
empty
set, x be
Element of D holds
<*x*> is
FinSequence of D;
theorem ::
FINSEQ_1:75
for D be
set, p,q be
FinSequence of D holds (p
^ q) is
FinSequence of D;
reserve a,b,c,d,e,f for
object;
theorem ::
FINSEQ_1:76
<*a*>
=
<*b*> implies a
= b
proof
assume
A1:
<*a*>
=
<*b*>;
thus a
= (
<*a*>
. 1) by
Def8
.= b by
A1,
Def8;
end;
theorem ::
FINSEQ_1:77
<*a, b*>
=
<*c, d*> implies a
= c & b
= d
proof
assume
A1:
<*a, b*>
=
<*c, d*>;
thus a
= (
<*a, b*>
. 1) by
Th44
.= c by
A1,
Th44;
thus b
= (
<*a, b*>
. 2) by
Th44
.= d by
A1,
Th44;
end;
theorem ::
FINSEQ_1:78
<*a, b, c*>
=
<*d, e, f*> implies a
= d & b
= e & c
= f
proof
assume
A1:
<*a, b, c*>
=
<*d, e, f*>;
thus a
= (
<*a, b, c*>
. 1) by
Th45
.= d by
A1,
Th45;
thus b
= (
<*a, b, c*>
. 2) by
Th45
.= e by
A1,
Th45;
thus c
= (
<*a, b, c*>
. 3) by
Th45
.= f by
A1,
Th45;
end;
registration
cluster non
empty
non-empty for
FinSequence;
existence
proof
take
<*
{
{} }*>;
thus
<*
{
{} }*> is non
empty;
assume
{}
in (
rng
<*
{
{} }*>);
then
{}
in
{
{
{} }} by
Th38;
hence contradiction by
TARSKI:def 1;
end;
end
theorem ::
FINSEQ_1:79
Th79: for p,q be
FinSequence st q
= (p
| (
Seg n)) holds (
len q)
<= (
len p)
proof
let p,q be
FinSequence;
assume q
= (p
| (
Seg n));
then
A1: (
dom q)
= ((
dom p)
/\ (
Seg n)) by
RELAT_1: 61;
(
Seg (
len q))
= (
dom q) & (
Seg (
len p))
= (
dom p) by
Def3;
hence thesis by
Th5,
A1,
XBOOLE_1: 17;
end;
theorem ::
FINSEQ_1:80
for p,r be
FinSequence st r
= (p
| (
Seg n)) holds ex q be
FinSequence st p
= (r
^ q)
proof
let p,r be
FinSequence;
assume
A1: r
= (p
| (
Seg n));
then
consider m be
Nat such that
A2: (
len p)
= ((
len r)
+ m) by
Th79,
NAT_1: 10;
deffunc
U(
Nat) = (p
. ((
len r)
+ $1));
consider q be
FinSequence such that
A3: (
len q)
= m & for k st k
in (
dom q) holds (q
. k)
=
U(k) from
SeqLambda;
take q;
A4: (
len p)
= (
len (r
^ q)) by
A2,
A3,
Th22;
now
let k such that
A5: 1
<= k and
A6: k
<= (
len p);
A7:
now
assume k
<= (
len r);
then
A8: k
in (
Seg (
len r)) by
A5;
A9: (
dom r)
= (
Seg (
len r)) by
Def3;
then ((r
^ q)
. k)
= (r
. k) by
A8,
Def7;
hence (p
. k)
= ((r
^ q)
. k) by
A1,
A8,
A9,
FUNCT_1: 47;
end;
now
assume
A10: not k
<= (
len r);
then
consider j be
Nat such that
A11: k
= ((
len r)
+ j) by
NAT_1: 10;
(k
- (
len r))
= j by
A11;
then
A12: ((r
^ q)
. k)
= (q
. j) by
A4,
A6,
A10,
Th24;
j
<>
0 by
A10,
A11;
then
A13: (
0
+ 1)
<= j by
NAT_1: 13;
j
<= (
len q) by
A2,
A3,
A6,
A11,
XREAL_1: 6;
then j
in (
Seg m) by
A3,
A13;
then j
in (
dom q) by
A3,
Def3;
hence (p
. k)
= ((r
^ q)
. k) by
A3,
A11,
A12;
end;
hence (p
. k)
= ((r
^ q)
. k) by
A7;
end;
hence thesis by
A4,
Th14;
end;
registration
let D be non
empty
set;
cluster non
empty for
FinSequence of D;
existence
proof
set x = the
Element of D;
take
<*x*>;
thus thesis;
end;
end
registration
let D be non
empty
set;
cluster non
emptyD
-valued for
FinSequence;
existence
proof
set x = the
Element of D;
take
<*x*>;
thus thesis;
end;
end
definition
let p,q be
FinSequence;
:: original:
=
redefine
::
FINSEQ_1:def17
pred p
= q means (
len p)
= (
len q) & for k st 1
<= k & k
<= (
len p) holds (p
. k)
= (q
. k);
compatibility by
Th14;
end
theorem ::
FINSEQ_1:81
for x,y,z be
object holds 1
in (
dom
<*x, y, z*>) & 2
in (
dom
<*x, y, z*>) & 3
in (
dom
<*x, y, z*>)
proof
let x,y,z be
object;
(
len
<*x, y, z*>)
= 3 by
Th45;
then (
dom
<*x, y, z*>)
= (
Seg 3) by
Def3;
hence thesis;
end;
theorem ::
FINSEQ_1:82
for p be
FinSequence, n,m be
Nat st m
<= n holds ((p
| n)
| m)
= (p
| m) by
Th5,
RELAT_1: 74;
reserve m for
Nat;
theorem ::
FINSEQ_1:83
(
Seg n)
= ((n
+ 1)
\
{
0 })
proof
A1: (n
+ 1)
= { m : m
< (n
+ 1) } by
AXIOMS: 4;
thus (
Seg n)
c= ((n
+ 1)
\
{
0 })
proof
let x be
object;
assume x
in (
Seg n);
then
consider k be
Nat such that
A2: x
= k and
A3: 1
<= k and
A4: k
<= n;
k
< (n
+ 1) by
A4,
NAT_1: 13;
then
A5: x
in (n
+ 1) by
A1,
A2;
not x
in
{
0 } by
A2,
A3,
TARSKI:def 1;
hence thesis by
A5,
XBOOLE_0:def 5;
end;
let x be
object;
assume
A6: x
in ((n
+ 1)
\
{
0 });
then
A7: x
in (n
+ 1);
A8: not x
in
{
0 } by
A6,
XBOOLE_0:def 5;
consider m such that
A9: x
= m and
A10: m
< (n
+ 1) by
A1,
A7;
A11: x
<>
0 by
A8,
TARSKI:def 1;
(
0
+ 1)
= 1;
then
A12: 1
<= m by
A9,
A11,
NAT_1: 13;
m
<= n by
A10,
NAT_1: 13;
hence thesis by
A9,
A12;
end;
registration
let n be
natural
Number;
cluster n
-element for
FinSequence;
existence
proof
A1: n is
Nat by
TARSKI: 1;
set p = ((
Seg n)
-->
{} );
(
dom p)
= (
Seg n) by
FUNCOP_1: 13;
then
reconsider p as
FinSequence by
A1,
Def2;
take p;
(
Seg (
len p))
= (
dom p) by
Def3;
hence (
len p)
= n by
Th6,
FUNCOP_1: 13;
end;
end
registration
let x be
object;
cluster
<*x*> -> 1
-element;
coherence ;
let y be
object;
cluster
<*x, y*> -> 2
-element;
coherence by
Th44;
let z be
object;
cluster
<*x, y, z*> -> 3
-element;
coherence by
Th45;
end
definition
let X be
set;
::
FINSEQ_1:def18
attr X is
FinSequence-membered means
:
Def18: x
in X implies x is
FinSequence;
end
registration
cluster
empty ->
FinSequence-membered for
set;
coherence ;
end
registration
cluster non
empty
FinSequence-membered for
set;
existence
proof
take X =
{ the
FinSequence};
thus X is non
empty;
let x;
thus thesis by
TARSKI:def 1;
end;
end
registration
let X be
set;
cluster (X
* ) ->
FinSequence-membered;
coherence by
Def11;
end
theorem ::
FINSEQ_1:84
for f be
Function st f
in (D
* ) & x
in (
dom f) holds (f
. x)
in D
proof
let f be
Function such that
A1: f
in (D
* ) and
A2: x
in (
dom f);
f is
FinSequence of D by
A1,
Def11;
then
A3: (
rng f)
c= D by
Def4;
(f
. x)
in (
rng f) by
A2,
FUNCT_1: 3;
hence (f
. x)
in D by
A3;
end;
registration
cluster
FinSequence-membered ->
functional for
set;
coherence ;
end
theorem ::
FINSEQ_1:85
for X be
FinSequence-membered
set holds ex Y be non
empty
set st X
c= (Y
* )
proof
let X be
FinSequence-membered
set;
set Z = { (
rng f) where f be
Element of X : f
in X };
take Y = (
succ (
union Z));
let x be
object;
assume
A1: x
in X;
then
reconsider x as
FinSequence by
Def18;
(
rng x)
in { (
rng f) where f be
Element of X : f
in X } by
A1;
then (
rng x)
c= Y by
ORDINAL3: 1,
SETFAM_1: 41;
then x is
FinSequence of Y by
Def4;
hence thesis by
Def11;
end;
registration
let X be
FinSequence-membered
set;
cluster ->
FinSequence-like for
Element of X;
coherence
proof
let e be
Element of X;
X is
empty or X is non
empty;
hence thesis by
Def18,
SUBSET_1:def 1;
end;
end
registration
let X be
FinSequence-membered
set;
cluster ->
FinSequence-membered for
Subset of X;
coherence ;
end
theorem ::
FINSEQ_1:86
for p,q be
FinSequence st q
= (p
| (
Seg n)) holds (
len q)
<= n
proof
let p,q be
FinSequence;
assume q
= (p
| (
Seg n));
then
A1: (
dom q)
= ((
dom p)
/\ (
Seg n)) by
RELAT_1: 61;
(
Seg (
len q))
= (
dom q) by
Def3;
hence thesis by
Th5,
A1,
XBOOLE_1: 17;
end;
theorem ::
FINSEQ_1:87
for p,q be
FinSequence st p
= (p
^ q) or p
= (q
^ p) holds q
=
{}
proof
let p,q be
FinSequence such that
A1: p
= (p
^ q) or p
= (q
^ p);
(
len (p
^ q))
= ((
len p)
+ (
len q)) & (
len (q
^ p))
= ((
len q)
+ (
len p)) by
Th22;
hence thesis by
A1;
end;
theorem ::
FINSEQ_1:88
for p,q be
FinSequence st (p
^ q)
=
<*x*> holds p
=
<*x*> & q
=
{} or p
=
{} & q
=
<*x*>
proof
let p,q be
FinSequence;
assume
A1: (p
^ q)
=
<*x*>;
then
A2: 1
= (
len (p
^ q)) by
Th40
.= ((
len p)
+ (
len q)) by
Th22;
A3:
now
assume (
len p)
=
0 ;
hence p
=
{} ;
hence q
=
<*x*> by
A1,
Th34;
end;
now
assume (
len p)
<>
0 ;
then
A4: (
0
+ 1)
<= (
len p) by
NAT_1: 13;
(
len p)
<= 1 by
A2,
NAT_1: 11;
then (
len p)
= 1 by
A4,
XXREAL_0: 1;
hence q
=
{} by
A2;
hence p
=
<*x*> by
A1,
Th34;
end;
hence thesis by
A3;
end;
theorem ::
FINSEQ_1:89
Th88: for f be n
-element
FinSequence holds (
dom f)
= (
Seg n)
proof
let f be n
-element
FinSequence;
(
len f)
= n by
CARD_1:def 7;
hence (
dom f)
= (
Seg n) by
Def3;
end;
registration
let n,m be
natural
Number;
let f be n
-element
FinSequence, g be m
-element
FinSequence;
cluster (f
^ g) -> (n
+ m)
-element;
coherence
proof
(
len f)
= n & (
len g)
= m by
CARD_1:def 7;
hence (
len (f
^ g))
= (n
+ m) by
Th22;
end;
end
registration
cluster
increasing ->
one-to-one for
real-valued
FinSequence;
coherence
proof
let f be
real-valued
FinSequence;
assume
A1: f is
increasing;
let x,y be
object;
assume that
A2: x
in (
dom f) & y
in (
dom f) and
A3: (f
. x)
= (f
. y);
reconsider nx = x, ny = y as
Element of
NAT by
A2;
nx
<= ny & nx
>= ny by
A1,
A2,
A3,
VALUED_0:def 13;
hence thesis by
XXREAL_0: 1;
end;
end
theorem ::
FINSEQ_1:90
for x,y be
object st x
in (
dom
<*y*>) holds x
= 1
proof
let x,y be
object;
assume x
in (
dom
<*y*>);
then x
in (
Seg 1) by
Th38;
hence thesis by
Th2,
TARSKI:def 1;
end;
registration
let X;
cluster X
-valued for
FinSequence;
existence
proof
take (
<*> X);
thus thesis;
end;
end
registration
let D be
FinSequence-membered
set;
let f be D
-valued
Function;
let x be
object;
cluster (f
. x) ->
FinSequence-like;
coherence
proof
per cases ;
suppose x
in (
dom f);
then
A1: (f
. x)
in (
rng f) by
FUNCT_1:def 3;
(
rng f)
c= D by
RELAT_1:def 19;
hence thesis by
A1;
end;
suppose not x
in (
dom f);
hence thesis by
FUNCT_1:def 2;
end;
end;
end
theorem ::
FINSEQ_1:91
x
in (
Seg n) implies x
= 1 or ... or x
= n by
Lm5;
theorem ::
FINSEQ_1:92
(
dom
<*x, y*>)
=
{1, 2}
proof
thus (
dom
<*x, y*>)
= (
Seg (
len
<*x, y*>)) by
Def3
.=
{1, 2} by
Th2,
Th44;
end;
begin
registration
let A be
finite
set;
cluster
onto
one-to-one for
FinSequence of A;
existence
proof
consider n such that
A1: (A,(
Seg n))
are_equipotent by
Th56;
consider f be
Function such that
A2: f is
one-to-one and
A3: (
dom f)
= (
Seg n) and
A4: (
rng f)
= A by
A1,
WELLORD2:def 4;
f is
FinSequence by
A3,
Def2;
then
reconsider f as
FinSequence of A by
A4,
Def4;
take f;
thus thesis by
A2,
A4,
FUNCT_2:def 3;
end;
end
definition
let A be
finite
set;
::
FINSEQ_1:def19
func
canFS A ->
FinSequence equals the
one-to-one
onto
FinSequence of A;
coherence ;
end
definition
let A be
finite
set;
:: original:
canFS
redefine
func
canFS A ->
FinSequence of A ;
coherence ;
end
registration
let A be
finite
set;
cluster (
canFS A) ->
one-to-one
onto;
coherence ;
end
theorem ::
FINSEQ_1:93
Th92: for A be
finite
set holds (
len (
canFS A))
= (
card A)
proof
let A be
finite
set;
thus (
card (
canFS A))
= (
card (
dom (
canFS A))) by
CARD_1: 62
.= (
card (
rng (
canFS A))) by
CARD_1: 70
.= (
card A) by
FUNCT_2:def 3;
end;
registration
let A be
finite non
empty
set;
cluster (
canFS A) -> non
empty;
coherence
proof
(
len (
canFS A))
= (
card A) by
Th92;
hence thesis;
end;
end
theorem ::
FINSEQ_1:94
for a be
object holds (
canFS
{a})
=
<*a*>
proof
let a be
object;
A1: (
rng (
canFS
{a}))
=
{a} by
FUNCT_2:def 3;
(
len (
canFS
{a}))
= (
card
{a}) by
Th92
.= 1 by
CARD_1: 30;
hence thesis by
A1,
Th39;
end;
theorem ::
FINSEQ_1:95
for A be
finite
set holds ((
canFS A)
" ) is
Function of A, (
Seg (
card A))
proof
let A be
finite
set;
(
len (
canFS A))
= (
card A) by
Th92;
then (
dom (
canFS A))
= (
Seg (
card A)) by
Def3;
then
A1: (
rng ((
canFS A)
" ))
= (
Seg (
card A)) by
FUNCT_1: 33;
(
rng (
canFS A))
= A by
FUNCT_2:def 3;
then (
dom ((
canFS A)
" ))
= A by
FUNCT_1: 33;
hence thesis by
A1,
FUNCT_2: 1;
end;
theorem ::
FINSEQ_1:96
i
>
0 implies
{
[i, x]} is
FinSubsequence
proof
assume
A1: i
>
0 ;
A2: (
dom
{
[i, x]})
=
{i} by
RELAT_1: 9;
{i}
c= (
Seg i)
proof
let x be
object;
assume x
in
{i};
then x
= i by
TARSKI:def 1;
hence thesis by
A1,
Th3;
end;
hence thesis by
A2,
Def12;
end;
Lm6: for p be
FinSubsequence st (
Seq p)
=
{} holds p
=
{}
proof
let p be
FinSubsequence such that
A1: (
Seq p)
=
{} ;
(
rng (
Sgm (
dom p)))
= (
dom p) by
Th50;
then (
dom
{} )
= (
dom (
Sgm (
dom p))) by
A1,
RELAT_1: 27;
then (
Sgm (
dom p))
=
{} ;
then (
dom p)
= (
rng
{} ) by
Th50;
hence thesis;
end;
theorem ::
FINSEQ_1:97
for q be
FinSubsequence holds q
=
{} iff (
Seq q)
=
{} by
Lm6;
registration
cluster ->
finite for
FinSubsequence;
coherence
proof
let q be
FinSubsequence;
ex n be
Nat st (
dom q)
c= (
Seg n) by
Def12;
hence thesis by
FINSET_1: 10;
end;
end
reserve x1,x2,y1,y2 for
set;
theorem ::
FINSEQ_1:98
{
[x1, y1],
[x2, y2]} is
FinSequence implies x1
= 1 & x2
= 1 & y1
= y2 or x1
= 1 & x2
= 2 or x1
= 2 & x2
= 1
proof
assume
{
[x1, y1],
[x2, y2]} is
FinSequence;
then
reconsider p =
{
[x1, y1],
[x2, y2]} as
FinSequence;
A1: (
dom p)
=
{x1, x2} by
RELAT_1: 10;
then
A2: x1
in (
dom p) by
TARSKI:def 2;
A3: x2
in (
dom p) by
A1,
TARSKI:def 2;
A4:
[x1, y1]
in p by
TARSKI:def 2;
A5:
[x2, y2]
in p by
TARSKI:def 2;
A6: (p
. x1)
= y1 by
A4,
FUNCT_1: 1;
A7: (p
. x2)
= y2 by
A5,
FUNCT_1: 1;
A8: (
dom p)
= (
Seg (
len p)) by
Def3;
A9: (
len p)
<= (1
+ 1) by
CARD_2: 50;
A10: (
len p)
>= (
0 qua
Nat
+ 1) by
NAT_1: 13;
A11:
now
assume (
len p)
= 1;
hence x1
= 1 & x2
= 1 by
A2,
A3,
A8,
Th2,
TARSKI:def 1;
hence y1
= y2 by
A5,
A6,
FUNCT_1: 1;
end;
now
assume
A12: (
len p)
= 2;
A13: x1
= x2 implies p
=
{
[x1, y1]} by
A6,
A7,
ENUMSET1: 29;
x1
= 1 & x2
= 2 or x1
= 2 & x2
= 1 or x1
= 1 & x2
= 1 or x1
= 2 & x2
= 2 by
A2,
A3,
A8,
A12,
Th2,
TARSKI:def 2;
hence x1
= 1 & x2
= 2 or x1
= 2 & x2
= 1 by
A12,
A13,
CARD_1: 30;
end;
hence thesis by
A9,
A10,
A11,
NAT_1: 9;
end;
theorem ::
FINSEQ_1:99
<*x1, x2*>
=
{
[1, x1],
[2, x2]}
proof
reconsider f =
{
[1, x1],
[2, x2]} as
Function by
GRFUNC_1: 8;
A1: (
dom f)
=
{1, 2} by
RELAT_1: 10;
then
A2: (
dom
<*x1, x2*>)
= (
dom f) by
Th2,
Th88;
now
let x be
object;
assume
A3: x
in
{1, 2};
per cases by
A3,
TARSKI:def 2;
suppose
A4: x
= 1;
then
A5: (
<*x1, x2*>
. x)
= x1 by
Th44;
[x, x1]
in f by
A4,
TARSKI:def 2;
hence (f
. x)
= (
<*x1, x2*>
. x) by
A5,
FUNCT_1: 1;
end;
suppose
A6: x
= 2;
then
A7: (
<*x1, x2*>
. x)
= x2 by
Th44;
[x, x2]
in f by
A6,
TARSKI:def 2;
hence (f
. x)
= (
<*x1, x2*>
. x) by
A7,
FUNCT_1: 1;
end;
end;
hence thesis by
A1,
A2,
FUNCT_1: 2;
end;
reserve j for
Nat;
theorem ::
FINSEQ_1:100
for q be
FinSubsequence holds (
dom (
Seq q))
= (
dom (
Sgm (
dom q)))
proof
let q be
FinSubsequence;
(
rng (
Sgm (
dom q)))
= (
dom q) by
Th50;
hence thesis by
RELAT_1: 27;
end;
theorem ::
FINSEQ_1:101
for q be
FinSubsequence holds (
rng q)
= (
rng (
Seq q))
proof
let q be
FinSubsequence;
(
dom q)
= (
rng (
Sgm (
dom q))) by
Th50;
hence thesis by
RELAT_1: 28;
end;
registration
cluster
one-to-one for
FinSequence;
existence
proof
take
{} ;
thus thesis;
end;
end
registration
let D;
cluster
one-to-one for
FinSequence of D;
existence
proof
take (
<*> D);
thus thesis;
end;
end
registration
cluster non
empty
natural-valued for
FinSequence;
existence
proof
<*
0 *> is
natural-valued &
<*
0 *> is non
empty;
hence thesis;
end;
end