:: Pigeon Hole Principle
:: by Wojciech A. Trybulec
::
:: Received April 8, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let f be Function;
let x be set ;
predf is_one-to-one_at x means :Def1: :: FINSEQ_4:def 1
f " (Im (f,x)) = {x};
end;

:: deftheorem Def1 defines is_one-to-one_at FINSEQ_4:def_1_:_
 for f being Function
for x being set holds
( f is_one-to-one_at x iff f " (Im (f,x)) = {x} );

theorem Th1: :: FINSEQ_4:1
for f being Function
for x being set st f is_one-to-one_at x holds
x in dom f
proofend;

theorem Th2: :: FINSEQ_4:2
for f being Function
for x being set holds
( f is_one-to-one_at x iff ( x in dom f & f " {(f . x)} = {x} ) )
proofend;

theorem Th3: :: FINSEQ_4:3
for f being Function
for x being set holds
( f is_one-to-one_at x iff ( x in dom f &amp; ( for z being set st z in dom f &amp; x <> z holds
f . x <> f . z ) ) )
proofend;

theorem :: FINSEQ_4:4
for f being Function holds
( ( for x being set st x in dom f holds
f is_one-to-one_at x ) iff f is one-to-one )
proofend;

definition
let R be Relation;
let y be set ;
predR just_once_values y means :Def2: :: FINSEQ_4:def 2
 card (Coim (R,y)) = 1;
end;

:: deftheorem Def2 defines just_once_values FINSEQ_4:def_2_:_
 for R being Relation
for y being set holds
( R just_once_values y iff card (Coim (R,y)) = 1 );

theorem Th5: :: FINSEQ_4:5
for f being Function
for y being set st f just_once_values y holds
y in rng f
proofend;

theorem Th6: :: FINSEQ_4:6
for f being Function
for y being set holds
( f just_once_values y iff ex x being set st {x} = f " {y} )
proofend;

theorem Th7: :: FINSEQ_4:7
for f being Function
for y being set holds
( f just_once_values y iff ex x being set st
( x in dom f &amp; y = f . x &amp; ( for z being set st z in dom f &amp; z <> x holds
f . z <> y ) ) )
proofend;

theorem Th8: :: FINSEQ_4:8
for f being Function holds
( f is one-to-one iff for y being set st y in rng f holds
f just_once_values y )
proofend;

theorem Th9: :: FINSEQ_4:9
for f being Function
for x being set holds
( f is_one-to-one_at x iff ( x in dom f &amp; f just_once_values f . x ) )
proofend;

definition
let f be Function;
let y be set ;
assume A1: f just_once_values y ;
funcf <- y ->  set  means :Def3: :: FINSEQ_4:def 3
( it in dom f &amp; f . it = y );
existence
 ex b1 being set st
( b1 in dom f &amp; f . b1 = y )
proofend;
uniqueness
 for b1, b2 being set st b1 in dom f &amp; f . b1 = y &amp; b2 in dom f &amp; f . b2 = y holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines <- FINSEQ_4:def_3_:_
 for f being Function
for y being set st f just_once_values y holds
for b3 being set holds
( b3 = f <- y iff ( b3 in dom f &amp; f . b3 = y ) );

theorem :: FINSEQ_4:10
for f being Function
for y being set st f just_once_values y holds
Im (f,(f <- y)) = {y}
proofend;

theorem Th11: :: FINSEQ_4:11
for f being Function
for y being set st f just_once_values y holds
f " {y} = {(f <- y)}
proofend;

theorem :: FINSEQ_4:12
for f being Function
for y being set st f is one-to-one &amp; y in rng f holds
(f ") . y = f <- y
proofend;

theorem :: FINSEQ_4:13
for f being Function
for x being set st f is_one-to-one_at x holds
f <- (f . x) = x
proofend;

theorem :: FINSEQ_4:14
for f being Function
for y being set st f just_once_values y holds
f is_one-to-one_at f <- y
proofend;

definition
let D be non empty set ;
let d1, d2 be Element of D;
:: original:<*
redefine func<*d1,d2*> ->  FinSequence of D;
coherence
 <*d1,d2*> is FinSequence of D by FINSEQ_2:13;
end;

definition
let D be non empty set ;
let d1, d2, d3 be Element of D;
:: original:<*
redefine func<*d1,d2,d3*> ->  FinSequence of D;
coherence
 <*d1,d2,d3*> is FinSequence of D by FINSEQ_2:14;
end;

theorem :: FINSEQ_4:15
for i being Nat
for D being set
for P being FinSequence of D st 1 <= i &amp; i <= len P holds
P /. i = P . i
proofend;

theorem :: FINSEQ_4:16
for D being non empty set
for d being Element of D holds <*d*> /. 1 = d
proofend;

theorem :: FINSEQ_4:17
for D being non empty set
for d1, d2 being Element of D holds
( <*d1,d2*> /. 1 = d1 &amp; <*d1,d2*> /. 2 = d2 )
proofend;

theorem :: FINSEQ_4:18
for D being non empty set
for d1, d2, d3 being Element of D holds
( <*d1,d2,d3*> /. 1 = d1 &amp; <*d1,d2,d3*> /. 2 = d2 &amp; <*d1,d2,d3*> /. 3 = d3 )
proofend;

definition
let p be FinSequence;
let x be set ;
funcx .. p ->  Element of NAT  equals :: FINSEQ_4:def 4
(Sgm (p " {x})) . 1;
coherence
 (Sgm (p " {x})) . 1 is Element of NAT
proofend;
end;

:: deftheorem  defines .. FINSEQ_4:def_4_:_
 for p being FinSequence
for x being set holds x .. p = (Sgm (p " {x})) . 1;

theorem Th19: :: FINSEQ_4:19
for p being FinSequence
for x being set st x in rng p holds
p . (x .. p) = x
proofend;

theorem Th20: :: FINSEQ_4:20
for p being FinSequence
for x being set st x in rng p holds
x .. p in dom p
proofend;

theorem Th21: :: FINSEQ_4:21
for p being FinSequence
for x being set st x in rng p holds
( 1 <= x .. p &amp; x .. p <= len p )
proofend;

theorem Th22: :: FINSEQ_4:22
for p being FinSequence
for x being set st x in rng p holds
( (x .. p) - 1 is Element of NAT &amp; (len p) - (x .. p) is Element of NAT )
proofend;

theorem Th23: :: FINSEQ_4:23
for p being FinSequence
for x being set st x in rng p holds
x .. p in p " {x}
proofend;

theorem Th24: :: FINSEQ_4:24
for p being FinSequence
for x being set
for k being Nat st k in dom p &amp; k < x .. p holds
p . k <> x
proofend;

theorem Th25: :: FINSEQ_4:25
for p being FinSequence
for x being set st p just_once_values x holds
p <- x = x .. p
proofend;

theorem Th26: :: FINSEQ_4:26
for p being FinSequence
for x being set st p just_once_values x holds
for k being Nat st k in dom p &amp; k <> x .. p holds
p . k <> x
proofend;

theorem Th27: :: FINSEQ_4:27
for p being FinSequence
for x being set st x in rng p &amp; ( for k being Nat st k in dom p &amp; k <> x .. p holds
p . k <> x ) holds
p just_once_values x
proofend;

theorem Th28: :: FINSEQ_4:28
for p being FinSequence
for x being set holds
( p just_once_values x iff ( x in rng p &amp; {(x .. p)} = p " {x} ) )
proofend;

theorem :: FINSEQ_4:29
for p being FinSequence
for x being set st p is one-to-one &amp; x in rng p holds
{(x .. p)} = p " {x}
proofend;

theorem Th30: :: FINSEQ_4:30
for p being FinSequence
for x being set holds
( p just_once_values x iff len (p - {x}) = (len p) - 1 )
proofend;

theorem Th31: :: FINSEQ_4:31
for p being FinSequence
for x being set st p just_once_values x holds
for k being Nat st k in dom (p - {x}) holds
( ( k < x .. p implies (p - {x}) . k = p . k ) &amp; ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) )
proofend;

theorem :: FINSEQ_4:32
for p being FinSequence
for x being set st p is one-to-one &amp; x in rng p holds
for k being Nat st k in dom (p - {x}) holds
( ( (p - {x}) . k = p . k implies k < x .. p ) &amp; ( k < x .. p implies (p - {x}) . k = p . k ) &amp; ( (p - {x}) . k = p . (k + 1) implies x .. p <= k ) &amp; ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) )
proofend;

definition
let p be FinSequence;
let x be set ;
assume A1: x in rng p ;
funcp -| x ->  FinSequence means :Def5: :: FINSEQ_4:def 5
 ex n being Nat st
( n = (x .. p) - 1 &amp; it = p | (Seg n) );
existence
 ex b1 being FinSequence ex n being Nat st
( n = (x .. p) - 1 &amp; b1 = p | (Seg n) )
proofend;
uniqueness
 for b1, b2 being FinSequence st ex n being Nat st
( n = (x .. p) - 1 &amp; b1 = p | (Seg n) ) &amp; ex n being Nat st
( n = (x .. p) - 1 &amp; b2 = p | (Seg n) ) holds
b1 = b2 ;
end;

:: deftheorem Def5 defines -| FINSEQ_4:def_5_:_
 for p being FinSequence
for x being set st x in rng p holds
for b3 being FinSequence holds
( b3 = p -| x iff ex n being Nat st
( n = (x .. p) - 1 &amp; b3 = p | (Seg n) ) );

theorem Th33: :: FINSEQ_4:33
for p being FinSequence
for x being set
for n being Nat st x in rng p &amp; n = (x .. p) - 1 holds
p | (Seg n) = p -| x
proofend;

theorem Th34: :: FINSEQ_4:34
for p being FinSequence
for x being set st x in rng p holds
len (p -| x) = (x .. p) - 1
proofend;

theorem Th35: :: FINSEQ_4:35
for p being FinSequence
for x being set
for n being Nat st x in rng p &amp; n = (x .. p) - 1 holds
dom (p -| x) = Seg n
proofend;

theorem Th36: :: FINSEQ_4:36
for p being FinSequence
for x being set
for k being Nat st x in rng p &amp; k in dom (p -| x) holds
p . k = (p -| x) . k
proofend;

theorem Th37: :: FINSEQ_4:37
for p being FinSequence
for x being set st x in rng p holds
not x in rng (p -| x)
proofend;

theorem :: FINSEQ_4:38
for p being FinSequence
for x being set st x in rng p holds
rng (p -| x) misses {x}
proofend;

theorem :: FINSEQ_4:39
for p being FinSequence
for x being set st x in rng p holds
rng (p -| x) c= rng p
proofend;

theorem :: FINSEQ_4:40
for p being FinSequence
for x being set st x in rng p holds
( x .. p = 1 iff p -| x = {} )
proofend;

theorem :: FINSEQ_4:41
for p being FinSequence
for x being set
for D being non empty set st x in rng p &amp; p is FinSequence of D holds
p -| x is FinSequence of D
proofend;

definition
let p be FinSequence;
let x be set ;
assume A1: x in rng p ;
funcp |-- x ->  FinSequence means :Def6: :: FINSEQ_4:def 6
( len it = (len p) - (x .. p) &amp; ( for k being Nat st k in dom it holds
it . k = p . (k + (x .. p)) ) );
existence
 ex b1 being FinSequence st
( len b1 = (len p) - (x .. p) &amp; ( for k being Nat st k in dom b1 holds
b1 . k = p . (k + (x .. p)) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence st len b1 = (len p) - (x .. p) &amp; ( for k being Nat st k in dom b1 holds
b1 . k = p . (k + (x .. p)) ) &amp; len b2 = (len p) - (x .. p) &amp; ( for k being Nat st k in dom b2 holds
b2 . k = p . (k + (x .. p)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines |-- FINSEQ_4:def_6_:_
 for p being FinSequence
for x being set st x in rng p holds
for b3 being FinSequence holds
( b3 = p |-- x iff ( len b3 = (len p) - (x .. p) &amp; ( for k being Nat st k in dom b3 holds
b3 . k = p . (k + (x .. p)) ) ) );

theorem Th42: :: FINSEQ_4:42
for p being FinSequence
for x being set
for n being Nat st x in rng p &amp; n = (len p) - (x .. p) holds
dom (p |-- x) = Seg n
proofend;

theorem Th43: :: FINSEQ_4:43
for p being FinSequence
for x being set
for n being Nat st x in rng p &amp; n in dom (p |-- x) holds
n + (x .. p) in dom p
proofend;

theorem :: FINSEQ_4:44
for p being FinSequence
for x being set st x in rng p holds
rng (p |-- x) c= rng p
proofend;

theorem Th45: :: FINSEQ_4:45
for p being FinSequence
for x being set holds
( p just_once_values x iff ( x in rng p &amp; not x in rng (p |-- x) ) )
proofend;

theorem Th46: :: FINSEQ_4:46
for p being FinSequence
for x being set st x in rng p &amp; p is one-to-one holds
not x in rng (p |-- x)
proofend;

theorem :: FINSEQ_4:47
for p being FinSequence
for x being set holds
( p just_once_values x iff ( x in rng p &amp; rng (p |-- x) misses {x} ) )
proofend;

theorem :: FINSEQ_4:48
for p being FinSequence
for x being set st x in rng p &amp; p is one-to-one holds
rng (p |-- x) misses {x}
proofend;

theorem :: FINSEQ_4:49
for p being FinSequence
for x being set st x in rng p holds
( x .. p = len p iff p |-- x = {} )
proofend;

theorem :: FINSEQ_4:50
for p being FinSequence
for x being set
for D being non empty set st x in rng p &amp; p is FinSequence of D holds
p |-- x is FinSequence of D
proofend;

theorem Th51: :: FINSEQ_4:51
for p being FinSequence
for x being set st x in rng p holds
p = ((p -| x) ^ <*x*>) ^ (p |-- x)
proofend;

theorem :: FINSEQ_4:52
for p being FinSequence
for x being set st x in rng p &amp; p is one-to-one holds
p -| x is one-to-one
proofend;

theorem :: FINSEQ_4:53
for p being FinSequence
for x being set st x in rng p &amp; p is one-to-one holds
p |-- x is one-to-one
proofend;

theorem Th54: :: FINSEQ_4:54
for p being FinSequence
for x being set holds
( p just_once_values x iff ( x in rng p &amp; p - {x} = (p -| x) ^ (p |-- x) ) )
proofend;

theorem :: FINSEQ_4:55
for p being FinSequence
for x being set st x in rng p &amp; p is one-to-one holds
p - {x} = (p -| x) ^ (p |-- x)
proofend;

theorem Th56: :: FINSEQ_4:56
for p being FinSequence
for x being set st x in rng p &amp; p - {x} is one-to-one &amp; p - {x} = (p -| x) ^ (p |-- x) holds
p is one-to-one
proofend;

theorem :: FINSEQ_4:57
for p being FinSequence
for x being set st x in rng p &amp; p is one-to-one holds
rng (p -| x) misses rng (p |-- x)
proofend;

theorem Th58: :: FINSEQ_4:58
for A being set st A is finite holds
ex p being FinSequence st
( rng p = A &amp; p is one-to-one )
proofend;

theorem Th59: :: FINSEQ_4:59
for p being FinSequence st rng p c= dom p &amp; p is one-to-one holds
rng p = dom p
proofend;

theorem Th60: :: FINSEQ_4:60
for p being FinSequence st rng p = dom p holds
p is one-to-one
proofend;

theorem :: FINSEQ_4:61
for p, q being FinSequence st rng p = rng q &amp; len p = len q &amp; q is one-to-one holds
p is one-to-one
proofend;

Lm1:  for A, B being finite set
for f being Function of A,B st card A = card B &amp; rng f = B holds
f is one-to-one
proofend;

theorem Th62: :: FINSEQ_4:62
for p being FinSequence holds
( p is one-to-one iff card (rng p) = len p )
proofend;

theorem :: FINSEQ_4:63
for A, B being finite set
for f being Function of A,B st card A = card B &amp; f is one-to-one holds
rng f = B
proofend;

theorem :: FINSEQ_4:64
for A, B being finite set
for f being Function of A,B st card A = card B &amp; rng f = B holds
f is one-to-one by Lm1;

:: [WP: ] Dirichlet_Principle
:: [WP: ] Pigeon_Hole_Principle
theorem :: FINSEQ_4:65
for B, A being set
for f being Function of A,B st card B in card A &amp; B <> {} holds
ex x, y being set st
( x in A &amp; y in A &amp; x <> y &amp; f . x = f . y )
proofend;

theorem Th66: :: FINSEQ_4:66
for A, B being set
for f being Function of A,B st card A in card B holds
ex x being set st
( x in B &amp; ( for y being set st y in A holds
f . y <> x ) )
proofend;

begin

:: from TOPREAL4
theorem :: FINSEQ_4:67
for D being non empty set
for f being FinSequence of D
for p being Element of D holds (f ^ <*p*>) /. ((len f) + 1) = p
proofend;

:: from GROUP_5
theorem :: FINSEQ_4:68
for k being Nat
for E being non empty set
for p, q being FinSequence of E st k in dom p holds
(p ^ q) /. k = p /. k
proofend;

theorem :: FINSEQ_4:69
for k being Nat
for E being non empty set
for p, q being FinSequence of E st k in dom q holds
(p ^ q) /. ((len p) + k) = q /. k
proofend;

:: from TOPREAL1
theorem :: FINSEQ_4:70
for a, m being Nat
for D being set
for p being FinSequence of D st a in dom (p | m) holds
(p | m) /. a = p /. a
proofend;

:: from GOBOARD1
theorem :: FINSEQ_4:71
for D being set
for f being FinSequence of D
for n, m being Nat st n in dom f &amp; m in Seg n holds
( m in dom f &amp; (f | n) /. m = f /. m )
proofend;

:: from VECTSP_9, 2006.01.06, A.T.
theorem :: FINSEQ_4:72
for n being Nat
for X being finite set st n <= card X holds
ex A being finite Subset of X st card A = n
proofend;

theorem :: FINSEQ_4:73
for x being set
for f being Function st f is one-to-one &amp; x in rng f holds
card (Coim (f,x)) = 1
proofend;

:: form SCMPDS_1, 2006.03.24, A.T.
definition
let x1, x2, x3, x4 be set ;
func<*x1,x2,x3,x4*> ->  set  equals :: FINSEQ_4:def 7
<*x1,x2,x3*> ^ <*x4*>;
correctness
coherence
<*x1,x2,x3*> ^ <*x4*> is set ;
;
let x5 be set ;
func<*x1,x2,x3,x4,x5*> ->  set  equals :: FINSEQ_4:def 8
<*x1,x2,x3*> ^ <*x4,x5*>;
correctness
coherence
<*x1,x2,x3*> ^ <*x4,x5*> is set ;
;
end;

:: deftheorem  defines <* FINSEQ_4:def_7_:_
 for x1, x2, x3, x4 being set holds <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*>;

:: deftheorem  defines <* FINSEQ_4:def_8_:_
 for x1, x2, x3, x4, x5 being set holds <*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*>;

registration
let x1, x2, x3, x4 be set ;
cluster<*x1,x2,x3,x4*> ->  Relation-like Function-like non empty ;
coherence
 ( not <*x1,x2,x3,x4*> is empty &amp; <*x1,x2,x3,x4*> is Function-like &amp; <*x1,x2,x3,x4*> is Relation-like ) ;
let x5 be set ;
cluster<*x1,x2,x3,x4,x5*> ->  Relation-like Function-like non empty ;
coherence
 ( not <*x1,x2,x3,x4,x5*> is empty &amp; <*x1,x2,x3,x4,x5*> is Function-like &amp; <*x1,x2,x3,x4,x5*> is Relation-like ) ;
end;

registration
let x1, x2, x3, x4 be set ;
cluster<*x1,x2,x3,x4*> ->  FinSequence-like ;
coherence
 <*x1,x2,x3,x4*> is FinSequence-like ;
let x5 be set ;
cluster<*x1,x2,x3,x4,x5*> ->  FinSequence-like ;
coherence
 <*x1,x2,x3,x4,x5*> is FinSequence-like ;
end;

definition
let D be non empty set ;
let x1, x2, x3, x4 be Element of D;
:: original:<*
redefine func<*x1,x2,x3,x4*> ->  FinSequence of D;
coherence
 <*x1,x2,x3,x4*> is FinSequence of D
proofend;
end;

definition
let D be non empty set ;
let x1, x2, x3, x4, x5 be Element of D;
:: original:<*
redefine func<*x1,x2,x3,x4,x5*> ->  FinSequence of D;
coherence
 <*x1,x2,x3,x4,x5*> is FinSequence of D
proofend;
end;

theorem Th74: :: FINSEQ_4:74
for x1, x2, x3, x4 being set holds
( <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*> &amp; <*x1,x2,x3,x4*> = <*x1,x2*> ^ <*x3,x4*> &amp; <*x1,x2,x3,x4*> = <*x1*> ^ <*x2,x3,x4*> &amp; <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> )
proofend;

theorem Th75: :: FINSEQ_4:75
for x1, x2, x3, x4, x5 being set holds
( <*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*> &amp; <*x1,x2,x3,x4,x5*> = <*x1,x2,x3,x4*> ^ <*x5*> &amp; <*x1,x2,x3,x4,x5*> = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> &amp; <*x1,x2,x3,x4,x5*> = <*x1,x2*> ^ <*x3,x4,x5*> &amp; <*x1,x2,x3,x4,x5*> = <*x1*> ^ <*x2,x3,x4,x5*> )
proofend;

theorem Th76: :: FINSEQ_4:76
for x1, x2, x3, x4 being set
for p being FinSequence holds
( p = <*x1,x2,x3,x4*> iff ( len p = 4 &amp; p . 1 = x1 &amp; p . 2 = x2 &amp; p . 3 = x3 &amp; p . 4 = x4 ) )
proofend;

theorem :: FINSEQ_4:77
canceled;

theorem Th78: :: FINSEQ_4:78
for x1, x2, x3, x4, x5 being set
for p being FinSequence holds
( p = <*x1,x2,x3,x4,x5*> iff ( len p = 5 &amp; p . 1 = x1 &amp; p . 2 = x2 &amp; p . 3 = x3 &amp; p . 4 = x4 &amp; p . 5 = x5 ) )
proofend;

theorem :: FINSEQ_4:79
canceled;

theorem :: FINSEQ_4:80
for ND being non empty set
for y1, y2, y3, y4 being Element of ND holds
( <*y1,y2,y3,y4*> /. 1 = y1 &amp; <*y1,y2,y3,y4*> /. 2 = y2 &amp; <*y1,y2,y3,y4*> /. 3 = y3 &amp; <*y1,y2,y3,y4*> /. 4 = y4 )
proofend;

theorem :: FINSEQ_4:81
for ND being non empty set
for y1, y2, y3, y4, y5 being Element of ND holds
( <*y1,y2,y3,y4,y5*> /. 1 = y1 &amp; <*y1,y2,y3,y4,y5*> /. 2 = y2 &amp; <*y1,y2,y3,y4,y5*> /. 3 = y3 &amp; <*y1,y2,y3,y4,y5*> /. 4 = y4 &amp; <*y1,y2,y3,y4,y5*> /. 5 = y5 )
proofend;

scheme :: FINSEQ_4:sch 1
Sch1{ F1() ->  non empty set , F2() ->  Nat, P1[ set , set ] } :
 ex f being FinSequence of F1() st
( len f = F2() &amp; ( for n being Nat st n in Seg F2() holds
P1[n,f /. n] ) )
provided
A1: for n being Nat st n in Seg F2() holds
ex d being Element of F1() st P1[n,d]
proofend;

:: form SCMFSA_7, 2007.07.22, A.T.
theorem Th82: :: FINSEQ_4:82
for D being non empty set
for p, q being FinSequence of D st p c= q holds
ex p9 being FinSequence of D st p ^ p9 = q
proofend;

theorem :: FINSEQ_4:83
for D being non empty set
for p, q being FinSequence of D
for i being Element of NAT st p c= q &amp; 1 <= i &amp; i <= len p holds
q . i = p . i
proofend;

scheme :: FINSEQ_4:sch 2
PiLambdaD{ F1() ->  non empty set , F2() ->  Nat, F3( set ) ->  Element of F1() } :
 ex g being FinSequence of F1() st
( len g = F2() &amp; ( for n being Nat st n in dom g holds
g /. n = F3(n) ) )
proofend;

:: from CIRCCMB3, 2009.02.16, A.T.
registration
let x1, x2, x3, x4 be set ;
cluster<*x1,x2,x3,x4*> -> 4 -element ;
coherence
 <*x1,x2,x3,x4*> is 4 -element ;
let x5 be set ;
cluster<*x1,x2,x3,x4,x5*> -> 5 -element ;
coherence
 <*x1,x2,x3,x4,x5*> is 5 -element ;
end;

begin

theorem :: FINSEQ_4:84
for m, n being Nat st m < n holds
ex p being Element of NAT st
( n = m + p &amp; 1 <= p )
proofend;

theorem :: FINSEQ_4:85
for S being set
for D1, D2 being non empty set
for f1 being Function of S,D1
for f2 being Function of D1,D2 st f1 is bijective &amp; f2 is bijective holds
f2 * f1 is bijective
proofend;

:: Partitions &amp; Equivalence Relations
theorem :: FINSEQ_4:86
for Y being set
for E1, E2 being Equivalence_Relation of Y st Class E1 = Class E2 holds
E1 = E2
proofend;

registration
let Z be finite set ;
cluster  ->  finite for a_partition of Z;
coherence
 for b1 being a_partition of Z holds b1 is finite ;
end;

registration
let X be non empty finite set ;
cluster non empty finite V38() with_non-empty_elements for a_partition of X;
existence
 ex b1 being a_partition of X st
( not b1 is empty &amp; b1 is finite )
proofend;
end;

theorem Th87: :: FINSEQ_4:87
for X being non empty set
for PX being a_partition of X
for Pi being set st Pi in PX holds
ex x being Element of X st x in Pi
proofend;

theorem :: FINSEQ_4:88
for X being non empty finite set
for PX being a_partition of X holds card PX <= card X
proofend;

theorem :: FINSEQ_4:89
for A being non empty finite set
for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 holds
card PA2 <= card PA1
proofend;

theorem Th90: :: FINSEQ_4:90
for A being non empty finite set
for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 holds
for p2 being Element of PA2 ex p1 being Element of PA1 st p1 c= p2
proofend;

theorem :: FINSEQ_4:91
for A being non empty finite set
for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 &amp; card PA1 = card PA2 holds
PA1 = PA2
proofend;

registration
let D be set ;
let M be FinSequence of D * ;
let k be Nat;
clusterM /. k ->  Relation-like Function-like ;
coherence
 ( M /. k is Function-like &amp; M /. k is Relation-like ) ;
end;

registration
let D be set ;
let M be FinSequence of D * ;
let k be Nat;
clusterM /. k -> D -valued FinSequence-like for Function;
coherence
 for b1 being Function st b1 = M /. k holds
( b1 is FinSequence-like &amp; b1 is D -valued ) by FINSEQ_1:def_11;
end;