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

begin

definition

let f be Function;
let x be set ;
pred f 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 :: FINSEQ_4:1

canceled;

theorem Th2: :: FINSEQ_4:2

for f being Function
for x being set st f is_one-to-one_at x holds
x in dom f

proof end;

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 & f " {(f . x)} = {x} ) )

proof end;

theorem Th4: :: FINSEQ_4:4

for f being Function
for x being set holds
( f is_one-to-one_at x iff ( x in dom f & ( for z being set st z in dom f & x <> z holds
f . x <> f . z ) ) )

proof end;

theorem :: FINSEQ_4:5

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 )

proof end;

definition

let f be Function;
let y be set ;
pred f just_once_values y means :Def2: :: FINSEQ_4:def 2
ex B being finite set st
( B = f " {y} & card B = 1 );

end;

:: deftheorem Def2 defines just_once_values FINSEQ_4:def 2 :
for f being Function
for y being set holds
( f just_once_values y iff ex B being finite set st
( B = f " {y} & card B = 1 ) );

theorem :: FINSEQ_4:6

canceled;

theorem Th7: :: FINSEQ_4:7

for f being Function
for y being set st f just_once_values y holds
y in rng f

proof end;

theorem Th8: :: FINSEQ_4:8

for f being Function
for y being set holds
( f just_once_values y iff ex x being set st {x} = f " {y} )

proof end;

theorem Th9: :: FINSEQ_4:9

for f being Function
for y being set holds
( f just_once_values y iff ex x being set st
( x in dom f & y = f . x & ( for z being set st z in dom f & z <> x holds
f . z <> y ) ) )

proof end;

theorem Th10: :: FINSEQ_4:10

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 )

proof end;

theorem Th11: :: FINSEQ_4:11

for f being Function
for x being set holds
( f is_one-to-one_at x iff ( x in dom f & f just_once_values f . x ) )

proof end;

definition

let f be Function;
let y be set ;
assume A1: f just_once_values y ;
func f <- y -> set means :Def3: :: FINSEQ_4:def 3
( it in dom f & f . it = y );
existence
ex b₁ being set st
( b₁ in dom f & f . b₁ = y )

proof end;

uniqueness
for b₁, b₂ being set st b₁ in dom f & f . b₁ = y & b₂ in dom f & f . b₂ = y holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines <- FINSEQ_4:def 3 :
for f being Function
for y being set st f just_once_values y holds
for b₃ being set holds
( b₃ = f <- y iff ( b₃ in dom f & f . b₃ = y ) );

theorem :: FINSEQ_4:12

canceled;

theorem :: FINSEQ_4:13

canceled;

theorem :: FINSEQ_4:14

canceled;

theorem :: FINSEQ_4:15

canceled;

theorem :: FINSEQ_4:16

for f being Function
for y being set st f just_once_values y holds
Im (f,(f <- y)) = {y}

proof end;

theorem Th17: :: FINSEQ_4:17

for f being Function
for y being set st f just_once_values y holds
f " {y} = {(f <- y)}

proof end;

theorem :: FINSEQ_4:18

for f being Function
for y being set st f is one-to-one & y in rng f holds
(f ") . y = f <- y

proof end;

theorem :: FINSEQ_4:19

canceled;

theorem :: FINSEQ_4:20

for f being Function
for x being set st f is_one-to-one_at x holds
f <- (f . x) = x

proof end;

theorem :: FINSEQ_4:21

for f being Function
for y being set st f just_once_values y holds
f is_one-to-one_at f <- y

proof end;

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:15;

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:16;

end;

theorem :: FINSEQ_4:22

canceled;

theorem :: FINSEQ_4:23

canceled;

theorem :: FINSEQ_4:24

for i being Nat
for D being set
for P being FinSequence of D st 1 <= i & i <= len P holds
P /. i = P . i

proof end;

theorem :: FINSEQ_4:25

for D being non empty set
for d being Element of D holds <*d*> /. 1 = d

proof end;

theorem :: FINSEQ_4:26

for D being non empty set
for d1, d2 being Element of D holds
( <*d1,d2*> /. 1 = d1 & <*d1,d2*> /. 2 = d2 )

proof end;

theorem :: FINSEQ_4:27

for D being non empty set
for d1, d2, d3 being Element of D holds
( <*d1,d2,d3*> /. 1 = d1 & <*d1,d2,d3*> /. 2 = d2 & <*d1,d2,d3*> /. 3 = d3 )

proof end;

definition

let p be FinSequence;
let x be set ;
canceled;
func x .. p -> Element of NAT equals :: FINSEQ_4:def 5
(Sgm (p " {x})) . 1;
coherence
(Sgm (p " {x})) . 1 is Element of NAT

proof end;

end;

:: deftheorem FINSEQ_4:def 4 :
canceled;

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

theorem :: FINSEQ_4:28

canceled;

theorem Th29: :: FINSEQ_4:29

for p being FinSequence
for x being set st x in rng p holds
p . (x .. p) = x

proof end;

theorem Th30: :: FINSEQ_4:30

for p being FinSequence
for x being set st x in rng p holds
x .. p in dom p

proof end;

theorem Th31: :: FINSEQ_4:31

for p being FinSequence
for x being set st x in rng p holds
( 1 <= x .. p & x .. p <= len p )

proof end;

theorem Th32: :: FINSEQ_4:32

for p being FinSequence
for x being set st x in rng p holds
( (x .. p) - 1 is Element of NAT & (len p) - (x .. p) is Element of NAT )

proof end;

theorem Th33: :: FINSEQ_4:33

for p being FinSequence
for x being set st x in rng p holds
x .. p in p " {x}

proof end;

theorem Th34: :: FINSEQ_4:34

for p being FinSequence
for x being set
for k being Nat st k in dom p & k < x .. p holds
p . k <> x

proof end;

theorem Th35: :: FINSEQ_4:35

for p being FinSequence
for x being set st p just_once_values x holds
p <- x = x .. p

proof end;

theorem Th36: :: FINSEQ_4:36

for p being FinSequence
for x being set st p just_once_values x holds
for k being Nat st k in dom p & k <> x .. p holds
p . k <> x

proof end;

theorem Th37: :: FINSEQ_4:37

for p being FinSequence
for x being set st x in rng p & ( for k being Nat st k in dom p & k <> x .. p holds
p . k <> x ) holds
p just_once_values x

proof end;

theorem Th38: :: FINSEQ_4:38

for p being FinSequence
for x being set holds
( p just_once_values x iff ( x in rng p & {(x .. p)} = p " {x} ) )

proof end;

theorem :: FINSEQ_4:39

for p being FinSequence
for x being set st p is one-to-one & x in rng p holds
{(x .. p)} = p " {x}

proof end;

theorem Th40: :: FINSEQ_4:40

for p being FinSequence
for x being set holds
( p just_once_values x iff len (p - {x}) = (len p) - 1 )

proof end;

theorem Th41: :: FINSEQ_4:41

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 ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) )

proof end;

theorem :: FINSEQ_4:42

for p being FinSequence
for x being set st p is one-to-one & 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 ) & ( k < x .. p implies (p - {x}) . k = p . k ) & ( (p - {x}) . k = p . (k + 1) implies x .. p <= k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) )

proof end;

definition

let p be FinSequence;
let x be set ;
assume A1: x in rng p ;
func p -| x -> FinSequence means :Def6: :: FINSEQ_4:def 6
ex n being Nat st
( n = (x .. p) - 1 & it = p | (Seg n) );
existence
ex b₁ being FinSequence ex n being Nat st
( n = (x .. p) - 1 & b₁ = p | (Seg n) )

proof end;

uniqueness
for b₁, b₂ being FinSequence st ex n being Nat st
( n = (x .. p) - 1 & b₁ = p | (Seg n) ) & ex n being Nat st
( n = (x .. p) - 1 & b₂ = p | (Seg n) ) holds
b₁ = b₂ ;

end;

:: deftheorem Def6 defines -| FINSEQ_4:def 6 :
for p being FinSequence
for x being set st x in rng p holds
for b₃ being FinSequence holds
( b₃ = p -| x iff ex n being Nat st
( n = (x .. p) - 1 & b₃ = p | (Seg n) ) );

theorem :: FINSEQ_4:43

canceled;

theorem :: FINSEQ_4:44

canceled;

theorem Th45: :: FINSEQ_4:45

for p being FinSequence
for x being set
for n being Nat st x in rng p & n = (x .. p) - 1 holds
p | (Seg n) = p -| x

proof end;

theorem Th46: :: FINSEQ_4:46

for p being FinSequence
for x being set st x in rng p holds
len (p -| x) = (x .. p) - 1

proof end;

theorem Th47: :: FINSEQ_4:47

for p being FinSequence
for x being set
for n being Nat st x in rng p & n = (x .. p) - 1 holds
dom (p -| x) = Seg n

proof end;

theorem Th48: :: FINSEQ_4:48

for p being FinSequence
for x being set
for k being Nat st x in rng p & k in dom (p -| x) holds
p . k = (p -| x) . k

proof end;

theorem Th49: :: FINSEQ_4:49

for p being FinSequence
for x being set st x in rng p holds
not x in rng (p -| x)

proof end;

theorem :: FINSEQ_4:50

for p being FinSequence
for x being set st x in rng p holds
rng (p -| x) misses {x}

proof end;

theorem :: FINSEQ_4:51

for p being FinSequence
for x being set st x in rng p holds
rng (p -| x) c= rng p

proof end;

theorem :: FINSEQ_4:52

for p being FinSequence
for x being set st x in rng p holds
( x .. p = 1 iff p -| x = {} )

proof end;

theorem :: FINSEQ_4:53

for p being FinSequence
for x being set
for D being non empty set st x in rng p & p is FinSequence of D holds
p -| x is FinSequence of D

proof end;

definition

let p be FinSequence;
let x be set ;
assume A1: x in rng p ;
func p |-- x -> FinSequence means :Def7: :: FINSEQ_4:def 7
( len it = (len p) - (x .. p) & ( for k being Nat st k in dom it holds
it . k = p . (k + (x .. p)) ) );
existence
ex b₁ being FinSequence st
( len b₁ = (len p) - (x .. p) & ( for k being Nat st k in dom b₁ holds
b₁ . k = p . (k + (x .. p)) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence st len b₁ = (len p) - (x .. p) & ( for k being Nat st k in dom b₁ holds
b₁ . k = p . (k + (x .. p)) ) & len b₂ = (len p) - (x .. p) & ( for k being Nat st k in dom b₂ holds
b₂ . k = p . (k + (x .. p)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines |-- FINSEQ_4:def 7 :
for p being FinSequence
for x being set st x in rng p holds
for b₃ being FinSequence holds
( b₃ = p |-- x iff ( len b₃ = (len p) - (x .. p) & ( for k being Nat st k in dom b₃ holds
b₃ . k = p . (k + (x .. p)) ) ) );

theorem :: FINSEQ_4:54

canceled;

theorem :: FINSEQ_4:55

canceled;

theorem :: FINSEQ_4:56

canceled;

theorem Th57: :: FINSEQ_4:57

for p being FinSequence
for x being set
for n being Nat st x in rng p & n = (len p) - (x .. p) holds
dom (p |-- x) = Seg n

proof end;

theorem Th58: :: FINSEQ_4:58

for p being FinSequence
for x being set
for n being Nat st x in rng p & n in dom (p |-- x) holds
n + (x .. p) in dom p

proof end;

theorem :: FINSEQ_4:59

for p being FinSequence
for x being set st x in rng p holds
rng (p |-- x) c= rng p

proof end;

theorem Th60: :: FINSEQ_4:60

for p being FinSequence
for x being set holds
( p just_once_values x iff ( x in rng p & not x in rng (p |-- x) ) )

proof end;

theorem Th61: :: FINSEQ_4:61

for p being FinSequence
for x being set st x in rng p & p is one-to-one holds
not x in rng (p |-- x)

proof end;

theorem :: FINSEQ_4:62

for p being FinSequence
for x being set holds
( p just_once_values x iff ( x in rng p & rng (p |-- x) misses {x} ) )

proof end;

theorem :: FINSEQ_4:63

for p being FinSequence
for x being set st x in rng p & p is one-to-one holds
rng (p |-- x) misses {x}

proof end;

theorem :: FINSEQ_4:64

for p being FinSequence
for x being set st x in rng p holds
( x .. p = len p iff p |-- x = {} )

proof end;

theorem :: FINSEQ_4:65

for p being FinSequence
for x being set
for D being non empty set st x in rng p & p is FinSequence of D holds
p |-- x is FinSequence of D

proof end;

theorem Th66: :: FINSEQ_4:66

for p being FinSequence
for x being set st x in rng p holds
p = ((p -| x) ^ <*x*>) ^ (p |-- x)

proof end;

theorem :: FINSEQ_4:67

for p being FinSequence
for x being set st x in rng p & p is one-to-one holds
p -| x is one-to-one

proof end;

theorem :: FINSEQ_4:68

for p being FinSequence
for x being set st x in rng p & p is one-to-one holds
p |-- x is one-to-one

proof end;

theorem Th69: :: FINSEQ_4:69

for p being FinSequence
for x being set holds
( p just_once_values x iff ( x in rng p & p - {x} = (p -| x) ^ (p |-- x) ) )

proof end;

theorem :: FINSEQ_4:70

for p being FinSequence
for x being set st x in rng p & p is one-to-one holds
p - {x} = (p -| x) ^ (p |-- x)

proof end;

theorem Th71: :: FINSEQ_4:71

for p being FinSequence
for x being set st x in rng p & p - {x} is one-to-one & p - {x} = (p -| x) ^ (p |-- x) holds
p is one-to-one

proof end;

theorem :: FINSEQ_4:72

for p being FinSequence
for x being set st x in rng p & p is one-to-one holds
rng (p -| x) misses rng (p |-- x)

proof end;

theorem Th73: :: FINSEQ_4:73

for A being set st A is finite holds
ex p being FinSequence st
( rng p = A & p is one-to-one )

proof end;

theorem Th74: :: FINSEQ_4:74

for p being FinSequence st rng p c= dom p & p is one-to-one holds
rng p = dom p

proof end;

theorem Th75: :: FINSEQ_4:75

for p being FinSequence st rng p = dom p holds
p is one-to-one

proof end;

theorem :: FINSEQ_4:76

for p, q being FinSequence st rng p = rng q & len p = len q & q is one-to-one holds
p is one-to-one

proof end;

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

proof end;

theorem Th77: :: FINSEQ_4:77

for p being FinSequence holds
( p is one-to-one iff card (rng p) = len p )

proof end;

theorem :: FINSEQ_4:78

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

proof end;

theorem Th79: :: FINSEQ_4:79

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

theorem :: FINSEQ_4:80

for B, A being set
for f being Function of A,B st card B in card A & B <> {} holds
ex x, y being set st
( x in A & y in A & x <> y & f . x = f . y )

proof end;

theorem Th81: :: FINSEQ_4:81

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 & ( for y being set st y in A holds
f . y <> x ) )

proof end;

begin

theorem :: FINSEQ_4:82

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

proof end;

theorem :: FINSEQ_4:83

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

proof end;

theorem :: FINSEQ_4:84

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

proof end;

theorem :: FINSEQ_4:85

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

proof end;

theorem :: FINSEQ_4:86

for D being set
for f being FinSequence of D
for n, m being Nat st n in dom f & m in Seg n holds
( m in dom f & (f | n) /. m = f /. m )

proof end;

theorem :: FINSEQ_4:87

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

proof end;

theorem :: FINSEQ_4:88

for x being set
for f being Function st f is one-to-one & x in rng f holds
card (f " {x}) = 1

proof end;

definition

let x1, x2, x3, x4 be set ;
func <*x1,x2,x3,x4*> -> set equals :: FINSEQ_4:def 8
<*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 9
<*x1,x2,x3*> ^ <*x4,x5*>;
correctness
coherence
<*x1,x2,x3*> ^ <*x4,x5*> is set ;
;

end;

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

:: deftheorem defines <* FINSEQ_4:def 9 :
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 ;
coherence
( <*x1,x2,x3,x4*> is Function-like & <*x1,x2,x3,x4*> is Relation-like ) ;
let x5 be set ;
cluster <*x1,x2,x3,x4,x5*> -> Relation-like Function-like ;
coherence
( <*x1,x2,x3,x4,x5*> is Function-like & <*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

proof end;

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

proof end;

end;

theorem Th89: :: FINSEQ_4:89

for x1, x2, x3, x4 being set holds
( <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*> & <*x1,x2,x3,x4*> = <*x1,x2*> ^ <*x3,x4*> & <*x1,x2,x3,x4*> = <*x1*> ^ <*x2,x3,x4*> & <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> )

proof end;

theorem Th90: :: FINSEQ_4:90

for x1, x2, x3, x4, x5 being set holds
( <*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*> & <*x1,x2,x3,x4,x5*> = <*x1,x2,x3,x4*> ^ <*x5*> & <*x1,x2,x3,x4,x5*> = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> & <*x1,x2,x3,x4,x5*> = <*x1,x2*> ^ <*x3,x4,x5*> & <*x1,x2,x3,x4,x5*> = <*x1*> ^ <*x2,x3,x4,x5*> )

proof end;

theorem Th91: :: FINSEQ_4:91

for x1, x2, x3, x4 being set
for p being FinSequence holds
( p = <*x1,x2,x3,x4*> iff ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) )

proof end;

theorem Th92: :: FINSEQ_4:92

for x1, x2, x3, x4 being set holds dom <*x1,x2,x3,x4*> = Seg 4

proof end;

theorem Th93: :: FINSEQ_4:93

for x1, x2, x3, x4, x5 being set
for p being FinSequence holds
( p = <*x1,x2,x3,x4,x5*> iff ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) )

proof end;

theorem Th94: :: FINSEQ_4:94

for x1, x2, x3, x4, x5 being set holds dom <*x1,x2,x3,x4,x5*> = Seg 5

proof end;

theorem :: FINSEQ_4:95

for ND being non empty set
for y1, y2, y3, y4 being Element of ND holds
( <*y1,y2,y3,y4*> /. 1 = y1 & <*y1,y2,y3,y4*> /. 2 = y2 & <*y1,y2,y3,y4*> /. 3 = y3 & <*y1,y2,y3,y4*> /. 4 = y4 )

proof end;

theorem :: FINSEQ_4:96

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

proof end;

scheme :: FINSEQ_4:sch 1
Sch1{ F₁() -> non empty set , F₂() -> Nat, P₁[ set , set ] } :

ex f being FinSequence of F₁() st
( len f = F₂() & ( for n being Nat st n in Seg F₂() holds
P₁[n,f /. n] ) )

provided

A1: for n being Nat st n in Seg F₂() holds
ex d being Element of F₁() st P₁[n,d]

proof end;

theorem Th97: :: FINSEQ_4:97

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

proof end;

theorem :: FINSEQ_4:98

for D being non empty set
for p, q being FinSequence of D
for i being Element of NAT st p c= q & 1 <= i & i <= len p holds
q . i = p . i

proof end;

scheme :: FINSEQ_4:sch 2
PiLambdaD{ F₁() -> non empty set , F₂() -> Nat, F₃( set ) -> Element of F₁() } :

ex g being FinSequence of F₁() st
( len g = F₂() & ( for n being Nat st n in dom g holds
g /. n = F₃(n) ) )

proof end;

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:99

for m, n being Nat st m < n holds
ex p being Element of NAT st
( n = m + p & 1 <= p )

proof end;

theorem :: FINSEQ_4:100

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 & f2 is bijective holds
f2 * f1 is bijective

proof end;

theorem :: FINSEQ_4:101

for Y being set
for E1, E2 being Equivalence_Relation of Y st Class E1 = Class E2 holds
E1 = E2

proof end;

registration

let Z be finite set ;
cluster -> finite a_partition of Z;
coherence
for b₁ being a_partition of Z holds b₁ is finite ;

end;

registration

let X be non empty finite set ;
cluster non empty finite with_non-empty_elements a_partition of X;
existence
ex b₁ being a_partition of X st
( not b₁ is empty & b₁ is finite )

proof end;

end;

theorem Th102: :: FINSEQ_4:102

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

proof end;

theorem :: FINSEQ_4:103

for X being non empty finite set
for PX being a_partition of X holds card PX <= card X

proof end;

theorem :: FINSEQ_4:104

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

proof end;

theorem Th105: :: FINSEQ_4:105

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

proof end;

theorem :: FINSEQ_4:106

for A being non empty finite set
for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 & card PA1 = card PA2 holds
PA1 = PA2

proof end;