:: Stirling Numbers of the Second Kind
:: by Karol P\c{a}k
::
:: Received March 15, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users

theorem Th1: :: STIRL2_1:1

for N being non empty Subset of NAT holds min N = min* N

proof end;

theorem Th2: :: STIRL2_1:2

for K, N being non empty Subset of NAT holds min ((min K),(min N)) = min (K \/ N)

proof end;

theorem :: STIRL2_1:3

for Ke, Ne being Subset of NAT holds min ((min* Ke),(min* Ne)) <= min* (Ke \/ Ne)

proof end;

theorem :: STIRL2_1:4

for Ke, Ne being Subset of NAT st not min* Ne in Ne /\ Ke holds
min* Ne = min* (Ne \ Ke)

proof end;

theorem Th5: :: STIRL2_1:5

for n being Element of NAT holds
( min* {n} = n & min {n} = n )

proof end;

theorem Th6: :: STIRL2_1:6

for n, k being Element of NAT holds
( min* {n,k} = min (n,k) & min {n,k} = min (n,k) )

proof end;

theorem :: STIRL2_1:7

for n, k, l being Element of NAT holds min* {n,k,l} = min (n,(min (k,l)))

proof end;

theorem Th8: :: STIRL2_1:8

for n being Nat holds n is Subset of NAT

proof end;

registration

let n be Nat;

cluster -> natural for Element of Segm n;

coherence
for b₁ being Element of Segm n holds b₁ is natural ;

end;

theorem :: STIRL2_1:9

for n being Nat
for N being non empty Subset of NAT st N c= n holds
n - 1 is Element of NAT

proof end;

theorem Th10: :: STIRL2_1:10

for k, n being Nat st k in Segm n holds
( k <= n - 1 & n - 1 is Element of NAT )

proof end;

theorem :: STIRL2_1:11

for n being Nat holds min* n = 0

proof end;

theorem Th12: :: STIRL2_1:12

for n being Nat
for N being non empty Subset of NAT st N c= Segm n holds
min* N <= n - 1

proof end;

theorem :: STIRL2_1:13

for n being Nat
for N being non empty Subset of NAT st N c= Segm n & N <> {(n - 1)} holds
min* N < n - 1

proof end;

theorem Th14: :: STIRL2_1:14

for n being Nat
for Ne being Subset of NAT st Ne c= Segm n & n > 0 holds
min* Ne <= n - 1

proof end;

definition

let n be Nat;
let X be set ;
let f be Function of (Segm n),X;
let x be set ;
:: original: "
redefine func f " x -> Subset of NAT;
coherence
f " x is Subset of NAT

proof end;

end;

definition

let X be set ;
let k be Nat;
let f be Function of X,(Segm k);
let x be object ;
:: original: .
redefine func f . x -> Element of Segm k;
coherence
f . x is Element of Segm k

proof end;

end;

definition

let n, k be Nat;
let f be Function of (Segm n),(Segm k);

attr f is "increasing means :: STIRL2_1:def 1
( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & ( for l, m being Nat st l in rng f & m in rng f & l < m holds
min* (f " {l}) < min* (f " {m}) ) );

end;

:: deftheorem defines "increasing STIRL2_1:def 1 :
for n, k being Nat
for f being Function of (Segm n),(Segm k) holds
( f is "increasing iff ( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & ( for l, m being Nat st l in rng f & m in rng f & l < m holds
min* (f " {l}) < min* (f " {m}) ) ) );

theorem Th15: :: STIRL2_1:15

for k, n being Nat
for f being Function of (Segm n),(Segm k) st n = 0 & k = 0 holds
( f is onto & f is "increasing )

proof end;

theorem Th16: :: STIRL2_1:16

for k, m, n being Nat
for f being Function of (Segm n),(Segm k) st n > 0 holds
min* (f " {m}) <= n - 1

proof end;

theorem Th17: :: STIRL2_1:17

for k, n being Nat
for f being Function of (Segm n),(Segm k) st f is onto holds
n >= k

proof end;

theorem Th18: :: STIRL2_1:18

for k, n being Nat
for f being Function of (Segm n),(Segm k) st f is onto & f is "increasing holds
for m being Nat st m < k holds
m <= min* (f " {m})

proof end;

theorem Th19: :: STIRL2_1:19

for k, n being Nat
for f being Function of (Segm n),(Segm k) st f is onto & f is "increasing holds
for m being Nat st m < k holds
min* (f " {m}) <= (n - k) + m

proof end;

theorem Th20: :: STIRL2_1:20

for k, n being Nat
for f being Function of (Segm n),(Segm k) st f is onto & f is "increasing & n = k holds
f = id n

proof end;

theorem :: STIRL2_1:21

for k, n being Nat
for f being Function of (Segm n),(Segm k) st f = id n & n > 0 holds
f is "increasing

proof end;

theorem :: STIRL2_1:22

for k, n being Nat holds
not ( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & ( for f being Function of (Segm n),(Segm k) holds not f is "increasing ) )

proof end;

theorem Th23: :: STIRL2_1:23

for k, n being Nat holds
not ( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & n >= k & ( for f being Function of (Segm n),(Segm k) holds
( not f is onto or not f is "increasing ) ) )

proof end;

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

{ f where f is Function of (Segm F₁()),(Segm F₂()) : P₁[f] } is finite

proof end;

theorem Th24: :: STIRL2_1:24

for n, k being Nat holds { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } is finite

proof end;

theorem Th25: :: STIRL2_1:25

for n, k being Nat holds card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } is Element of NAT

proof end;

:: Stirling Numbers of the second kind

definition

let n, k be Nat;

func n block k -> set equals :: STIRL2_1:def 2
card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } ;

coherence
card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } is set ;

end;

:: deftheorem defines block STIRL2_1:def 2 :
for n, k being Nat holds n block k = card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } ;

registration

let n, k be Nat;

cluster n block k -> natural ;

coherence
n block k is natural by Th25;

end;

theorem Th26: :: STIRL2_1:26

for n being Nat holds n block n = 1

proof end;

theorem Th27: :: STIRL2_1:27

for k being Nat st k <> 0 holds
0 block k = 0

proof end;

theorem :: STIRL2_1:28

for k being Nat holds
( 0 block k = 1 iff k = 0 ) by Th26, Th27;

theorem Th29: :: STIRL2_1:29

for k, n being Nat st n < k holds
n block k = 0

proof end;

theorem :: STIRL2_1:30

for n being Nat holds
( n block 0 = 1 iff n = 0 )

proof end;

theorem Th31: :: STIRL2_1:31

for n being Nat st n <> 0 holds
n block 0 = 0

proof end;

theorem Th32: :: STIRL2_1:32

for n being Nat st n <> 0 holds
n block 1 = 1

proof end;

theorem :: STIRL2_1:33

for k, n being Nat holds
( ( ( 1 <= k & k <= n ) or k = n ) iff n block k > 0 )

proof end;

scheme :: STIRL2_1:sch 2
Sch2{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> Function of F₁(),F₂(), F₆( object ) -> object } :

ex h being Function of F₃(),F₄() st
( h | F₁() = F₅() & ( for x being set st x in F₃() \ F₁() holds
h . x = F₆(x) ) )

provided

A1: for x being set st x in F₃() \ F₁() holds
F₆(x) in F₄() and
A2: ( F₁() c= F₃() & F₂() c= F₄() ) and
A3: ( F₂() is empty implies F₁() is empty )

proof end;

scheme :: STIRL2_1:sch 3
Sch3{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅( object ) -> object , P₁[ set , set , set ] } :

card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) }

provided

A1: for x being set st x in F₃() \ F₁() holds
F₅(x) in F₄() and
A2: ( F₁() c= F₃() & F₂() c= F₄() ) and
A3: ( F₂() is empty implies F₁() is empty ) and
A4: for f being Function of F₃(),F₄() st ( for x being set st x in F₃() \ F₁() holds
F₅(x) = f . x ) holds
( P₁[f,F₃(),F₄()] iff P₁[f | F₁(),F₁(),F₂()] )

proof end;

scheme :: STIRL2_1:sch 4
Sch4{ F₁() -> set , F₂() -> set , F₃() -> object , F₄() -> object , P₁[ set , set , set ] } :

card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of (F₁() \/ {F₃()}),(F₂() \/ {F₄()}) : ( P₁[f,F₁() \/ {F₃()},F₂() \/ {F₄()}] & rng (f | F₁()) c= F₂() & f . F₃() = F₄() ) }

provided

A1: ( F₂() is empty implies F₁() is empty ) and
A2: not F₃() in F₁() and
A3: for f being Function of (F₁() \/ {F₃()}),(F₂() \/ {F₄()}) st f . F₃() = F₄() holds
( P₁[f,F₁() \/ {F₃()},F₂() \/ {F₄()}] iff P₁[f | F₁(),F₁(),F₂()] )

proof end;

theorem Th34: :: STIRL2_1:34

for k, n being Nat
for f being Function of (Segm (n + 1)),(Segm (k + 1)) st f is onto & f is "increasing & f " {(f . n)} = {n} holds
f . n = k

proof end;

theorem Th35: :: STIRL2_1:35

for k, n being Nat
for f being Function of (Segm (n + 1)),(Segm k) st k <> 0 & f " {(f . n)} <> {n} holds
ex m being Nat st
( m in f " {(f . n)} & m <> n )

proof end;

theorem Th36: :: STIRL2_1:36

for k, l, m, n being Nat
for f being Function of (Segm n),(Segm k)
for g being Function of (Segm (n + m)),(Segm (k + l)) st g is "increasing & f = g | n holds
for i, j being Nat st i in rng f & j in rng f & i < j holds
min* (f " {i}) < min* (f " {j})

proof end;

theorem Th37: :: STIRL2_1:37

for k, n being Nat
for f being Function of (Segm (n + 1)),(Segm (k + 1)) st f is onto & f is "increasing & f " {(f . n)} = {n} holds
( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds
( g is onto & g is "increasing ) ) )

proof end;

theorem Th38: :: STIRL2_1:38

for k, n being Nat
for f being Function of (Segm (n + 1)),(Segm k)
for g being Function of (Segm n),(Segm k) st f is onto & f is "increasing & f " {(f . n)} <> {n} & f | n = g holds
( g is onto & g is "increasing )

proof end;

theorem Th39: :: STIRL2_1:39

for k, m, n being Nat
for f being Function of (Segm n),(Segm k)
for g being Function of (Segm (n + 1)),(Segm (k + m)) st f is onto & f is "increasing & f = g | n holds
for i, j being Nat st i in rng g & j in rng g & i < j holds
min* (g " {i}) < min* (g " {j})

proof end;

theorem Th40: :: STIRL2_1:40

for k, n being Nat
for f being Function of (Segm n),(Segm k)
for g being Function of (Segm (n + 1)),(Segm (k + 1)) st f is onto & f is "increasing & f = g | (Segm n) & g . n = k holds
( g is onto & g is "increasing & g " {(g . n)} = {n} )

proof end;

theorem Th41: :: STIRL2_1:41

for k, n being Nat
for f being Function of (Segm n),(Segm k)
for g being Function of (Segm (n + 1)),(Segm k) st f is onto & f is "increasing & f = g | (Segm n) & g . n < k holds
( g is onto & g is "increasing & g " {(g . n)} <> {n} )

proof end;

Lm1: for k, n being Nat st k < n holds
n \/ {k} = n

proof end;

theorem Th42: :: STIRL2_1:42

for k, n being Nat holds card { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } = card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) }

proof end;

theorem Th43: :: STIRL2_1:43

for k, n, l being Nat st l < k holds
card { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } = card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) }

proof end;

theorem Th44: :: STIRL2_1:44

for f being Function
for n being Nat holds (union (rng (f | n))) \/ (f . n) = union (rng (f | (n + 1)))

proof end;

scheme :: STIRL2_1:sch 5
Sch6{ F₁() -> non empty set , F₂() -> Nat, P₁[ object , object ] } :

ex p being XFinSequence of F₁() st
( dom p = Segm F₂() & ( for k being Nat st k in Segm F₂() holds
P₁[k,p . k] ) )

provided

A1: for k being Nat st k in Segm F₂() holds
ex x being Element of F₁() st P₁[k,x]

proof end;

Lm2: now :: thesis: for D being non empty set
for F being XFinSequence of D st ( for i being Nat st i in dom F holds
F . i is finite ) & ( for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j ) holds
ex CardF being XFinSequence of NAT st
( dom CardF = dom F & ( for i being Nat st i in dom CardF holds
CardF . i = card (F . i) ) & card (union (rng F)) = Sum CardF )

let D be non empty set ; :: thesis: for F being XFinSequence of D st ( for i being Nat st i in dom F holds
F . i is finite ) & ( for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j ) holds
ex CardF being XFinSequence of NAT st
( dom CardF = dom F & ( for i being Nat st i in dom CardF holds
CardF . i = card (F . i) ) & card (union (rng F)) = Sum CardF )
let F be XFinSequence of D; :: thesis: ( ( for i being Nat st i in dom F holds
F . i is finite ) & ( for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j ) implies ex CardF being XFinSequence of NAT st
( dom CardF = dom F & ( for i being Nat st i in dom CardF holds
CardF . i = card (F . i) ) & card (union (rng F)) = Sum CardF ) )
assume that
A1: for i being Nat st i in dom F holds
F . i is finite and
A2: for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j ; :: thesis: ex CardF being XFinSequence of NAT st
( dom CardF = dom F & ( for i being Nat st i in dom CardF holds
CardF . i = card (F . i) ) & card (union (rng F)) = Sum CardF )
thus ex CardF being XFinSequence of NAT st
( dom CardF = dom F & ( for i being Nat st i in dom CardF holds
CardF . i = card (F . i) ) & card (union (rng F)) = Sum CardF ) :: thesis: verum

proof

defpred S₁[ Nat, set ] means $2 = card (F . $1);
A3: for k being Nat st k in Segm (len F) holds
ex x being Element of NAT st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Segm (len F) implies ex x being Element of NAT st S₁[k,x] )
assume k in Segm (len F) ; :: thesis: ex x being Element of NAT st S₁[k,x]
then F . k is finite by A1;
then reconsider m = card (F . k) as Nat ;
card (F . k) = card m ;
hence ex x being Element of NAT st S₁[k,x] ; :: thesis: verum

end;

consider CardF being XFinSequence of NAT such that
A4: ( dom CardF = Segm (len F) & ( for k being Nat st k in Segm (len F) holds
S₁[k,CardF . k] ) ) from STIRL2_1:sch 5(A3);
take CardF ; :: thesis: ( dom CardF = dom F & ( for i being Nat st i in dom CardF holds
CardF . i = card (F . i) ) & card (union (rng F)) = Sum CardF )
thus dom CardF = dom F by A4; :: thesis: ( ( for i being Nat st i in dom CardF holds
CardF . i = card (F . i) ) & card (union (rng F)) = Sum CardF )
thus A5: for i being Nat st i in dom CardF holds
CardF . i = card (F . i) by A4; :: thesis: card (union (rng F)) = Sum CardF
A6: addnat "**" CardF = Sum CardF by AFINSQ_2:51;

per cases ( len CardF = 0 or len CardF <> 0 ) ;

suppose A7: len CardF = 0 ; :: thesis: card (union (rng F)) = Sum CardF

then union (rng F) is empty by A4, RELAT_1:42, ZFMISC_1:2;
hence card (union (rng F)) = Sum CardF by A7, A6, AFINSQ_2:def 8, BINOP_2:5; :: thesis: verum

end;

suppose A8: len CardF <> 0 ; :: thesis: card (union (rng F)) = Sum CardF

then consider f being sequence of NAT such that
A9: f . 0 = CardF . 0 and
A10: for n being Nat st n + 1 < len CardF holds
f . (n + 1) = addnat . ((f . n),(CardF . (n + 1))) and
A11: addnat "**" CardF = f . ((len CardF) - 1) by AFINSQ_2:def 8;
defpred S₂[ Nat] means ( $1 < len CardF implies ( card (union (rng (F | ($1 + 1)))) = f . $1 & union (rng (F | ($1 + 1))) is finite ) );
A12: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A13: S₂[k] ; :: thesis: S₂[k + 1]
set k1 = k + 1;
set Fk1 = F | (k + 1);
set rFk1 = rng (F | (k + 1));
assume A14: k + 1 < len CardF ; :: thesis: ( card (union (rng (F | ((k + 1) + 1)))) = f . (k + 1) & union (rng (F | ((k + 1) + 1))) is finite )
reconsider urFk1 = union (rng (F | (k + 1))) as finite set by A13, A14, NAT_1:13;
A15: f . (k + 1) = addnat . ((f . k),(CardF . (k + 1))) by A10, A14;
A16: union (rng (F | (k + 1))) misses F . (k + 1)

proof

assume union (rng (F | (k + 1))) meets F . (k + 1) ; :: thesis: contradiction
then consider x being object such that
A17: x in (union (rng (F | (k + 1)))) /\ (F . (k + 1)) by XBOOLE_0:4;
A18: x in F . (k + 1) by A17, XBOOLE_0:def 4;
A19: k + 1 in dom F by A4, A14, NAT_1:44;
x in union (rng (F | (k + 1))) by A17, XBOOLE_0:def 4;
then consider Y being set such that
A20: x in Y and
A21: Y in rng (F | (k + 1)) by TARSKI:def 4;
consider X being object such that
A22: X in dom (F | (k + 1)) and
A23: (F | (k + 1)) . X = Y by A21, FUNCT_1:def 3;
reconsider X = X as Element of NAT by A22;
A24: (F | (k + 1)) . X = F . X by A22, FUNCT_1:47;
A25: X in (dom F) /\ (k + 1) by A22, RELAT_1:61;
then X in k + 1 by XBOOLE_0:def 4;
then A26: X <> k + 1 ;
X in dom F by A25, XBOOLE_0:def 4;
then Y misses F . (k + 1) by A2, A23, A19, A26, A24;
hence contradiction by A20, A18, XBOOLE_0:3; :: thesis: verum

end;

k + 1 in dom F by A4, A14, NAT_1:44;
then reconsider Fk1 = F . (k + 1) as finite set by A1;
k + 1 in len F by A4, A14, NAT_1:44;
then card Fk1 = CardF . (k + 1) by A4;
then A27: f . (k + 1) = (f . k) + (card Fk1) by A15, BINOP_2:def 23;
card (urFk1 \/ Fk1) = (f . k) + (card Fk1) by A13, A14, A16, CARD_2:40, NAT_1:13;
hence ( card (union (rng (F | ((k + 1) + 1)))) = f . (k + 1) & union (rng (F | ((k + 1) + 1))) is finite ) by A27, Th44; :: thesis: verum

end;

reconsider C1 = (len CardF) - 1 as Element of NAT by A8, NAT_1:20;
A28: C1 < C1 + 1 by NAT_1:13;
A29: F | (len CardF) = F by A4;
A30: S₂[ 0 ]

proof

assume 0 < len CardF ; :: thesis: ( card (union (rng (F | (0 + 1)))) = f . 0 & union (rng (F | (0 + 1))) is finite )
A31: union (rng (F | (0 + 1))) = (union (rng (F | 0))) \/ (F . 0) by Th44;
A32: 0 in len CardF by A8, AFINSQ_1:86;
thus card (union (rng (F | (0 + 1)))) = card ({} \/ (F . 0)) by A31, ZFMISC_1:2
.= card (F . 0)
.= CardF . 0 by A32, A5
.= f . 0 by A9 ; :: thesis: union (rng (F | (0 + 1))) is finite
hence union (rng (F | (0 + 1))) is finite ; :: thesis: verum

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A30, A12);
hence card (union (rng F)) = Sum CardF by A11, A28, A29, A6; :: thesis: verum

end;

end;

end;

end;

scheme :: STIRL2_1:sch 6
Sch8{ F₁() -> finite set , F₂() -> finite set , F₃() -> set , P₁[ set ], F₄() -> Function of (card F₂()),F₂() } :

ex F being XFinSequence of NAT st
( dom F = card F₂() & card { g where g is Function of F₁(),F₂() : P₁[g] } = Sum F & ( for i being Nat st i in dom F holds
F . i = card { g where g is Function of F₁(),F₂() : ( P₁[g] & g . F₃() = F₄() . i ) } ) )

provided

A1: ( F₄() is onto & F₄() is one-to-one ) and
A2: not F₂() is empty and
A3: F₃() in F₁()

proof end;

theorem Th45: :: STIRL2_1:45

for k, n being Nat holds k * (n block k) = card { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }

proof end;

:: Recursive dependence

theorem Th46: :: STIRL2_1:46

for k, n being Nat holds (n + 1) block (k + 1) = ((k + 1) * (n block (k + 1))) + (n block k)

proof end;

theorem Th47: :: STIRL2_1:47

for n being Nat st n >= 1 holds
n block 2 = (1 / 2) * ((2 |^ n) - 2)

proof end;

theorem Th48: :: STIRL2_1:48

for n being Nat st n >= 2 holds
n block 3 = (1 / 6) * (((3 |^ n) - (3 * (2 |^ n))) + 3)

proof end;

Lm3: for n being Nat holds n |^ 3 = (n * n) * n

proof end;

theorem :: STIRL2_1:49

for n being Nat st n >= 3 holds
n block 4 = (1 / 24) * ((((4 |^ n) - (4 * (3 |^ n))) + (6 * (2 |^ n))) - 4)

proof end;

theorem Th50: :: STIRL2_1:50

( 3 ! = 6 & 4 ! = 24 )

proof end;

theorem Th51: :: STIRL2_1:51

for n being Nat holds
( n choose 1 = n & n choose 2 = (n * (n - 1)) / 2 & n choose 3 = ((n * (n - 1)) * (n - 2)) / 6 & n choose 4 = (((n * (n - 1)) * (n - 2)) * (n - 3)) / 24 )

proof end;

theorem Th52: :: STIRL2_1:52

for n being Nat holds (n + 1) block n = (n + 1) choose 2

proof end;

theorem :: STIRL2_1:53

for n being Nat holds (n + 2) block n = (3 * ((n + 2) choose 4)) + ((n + 2) choose 3)

proof end;

theorem Th54: :: STIRL2_1:54

for F being Function
for y being set holds
( rng (F | ((dom F) \ (F " {y}))) = (rng F) \ {y} & ( for x being set st x <> y holds
(F | ((dom F) \ (F " {y}))) " {x} = F " {x} ) )

proof end;

theorem Th55: :: STIRL2_1:55

for k being Nat
for X, x being set st card X = k + 1 & x in X holds
card (X \ {x}) = k

proof end;

scheme :: STIRL2_1:sch 7
Sch9{ P₁[ set ], P₂[ set , Function] } :

for F being Function st rng F is finite holds
P₁[F]

provided

A1: P₁[ {} ] and
A2: for F being Function st ( for x being set st x in rng F & P₂[x,F] holds
P₁[F | ((dom F) \ (F " {x}))] ) holds
P₁[F]

proof end;

theorem Th56: :: STIRL2_1:56

for N being Subset of NAT st N is finite holds
ex k being Nat st
for n being Nat st n in N holds
n <= k

proof end;

theorem Th57: :: STIRL2_1:57

for X, Y being set
for x, y being object st ( Y is empty implies X is empty ) & not x in X holds
for F being Function of X,Y ex G being Function of (X \/ {x}),(Y \/ {y}) st
( G | X = F & G . x = y )

proof end;

theorem Th58: :: STIRL2_1:58

for X, Y, x, y being set st ( Y is empty implies X is empty ) holds
for F being Function of X,Y
for G being Function of (X \/ {x}),(Y \/ {y}) st G | X = F & G . x = y holds
( ( F is onto implies G is onto ) & ( not y in Y & F is one-to-one implies G is one-to-one ) )

proof end;

theorem Th59: :: STIRL2_1:59

for N being finite Subset of NAT ex Order being Function of N,(Segm (card N)) st
( Order is bijective & ( for n, k being Nat st n in dom Order & k in dom Order & n < k holds
Order . n < Order . k ) )

proof end;

theorem :: STIRL2_1:60

canceled;

Th60: for X, Y being finite set
for F being Function of X,Y st card X = card Y holds
( F is onto iff F is one-to-one )
by FINSEQ_4:63;

Lm5: for n being Element of NAT
for N being finite Subset of NAT
for F being Function of N,(Segm (card N)) st n in N & F is bijective & ( for n, k being Nat st n in dom F & k in dom F & n < k holds
F . n < F . k ) holds
ex P being Permutation of N st
for k being Nat st k in N holds
( ( k < n implies P . k = (F ") . ((F . k) + 1) ) & ( k = n implies P . k = (F ") . 0 ) & ( k > n implies P . k = k ) )

proof end;

theorem Th61: :: STIRL2_1:61

for F, G being Function
for y being set st y in rng (G * F) & G is one-to-one holds
ex x being set st
( x in dom G & x in rng F & G " {y} = {x} & F " {x} = (G * F) " {y} )

proof end;

definition

let Ne, Ke be Subset of NAT;
let f be Function of Ne,Ke;

attr f is 'increasing means :: STIRL2_1:def 3
for l, m being Nat st l in rng f & m in rng f & l < m holds
min* (f " {l}) < min* (f " {m});

end;

:: deftheorem defines 'increasing STIRL2_1:def 3 :
for Ne, Ke being Subset of NAT
for f being Function of Ne,Ke holds
( f is 'increasing iff for l, m being Nat st l in rng f & m in rng f & l < m holds
min* (f " {l}) < min* (f " {m}) );

theorem Th62: :: STIRL2_1:62

for Ke, Ne being Subset of NAT
for F being Function of Ne,Ke st F is 'increasing holds
min* (rng F) = F . (min* (dom F))

proof end;

:: existence of an expansion

theorem :: STIRL2_1:63

for Ke, Ne being Subset of NAT
for F being Function of Ne,Ke st rng F is finite holds
ex I being Function of Ne,Ke ex P being Permutation of (rng F) st
( F = P * I & rng F = rng I & I is 'increasing )

proof end;

:: uniqueness of expansion

theorem Th64: :: STIRL2_1:64

for Ke, Ne, Me being Subset of NAT
for F being Function of Ne,Ke st rng F is finite holds
for I1, I2 being Function of Ne,Me
for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds
( P1 = P2 & I1 = I2 )

proof end;

theorem :: STIRL2_1:65

for Ke, Ne being Subset of NAT
for F being Function of Ne,Ke st rng F is finite holds
for I1, I2 being Function of Ne,Ke
for P1, P2 being Permutation of (rng F) st F = P1 * I1 & F = P2 * I2 & rng F = rng I1 & rng F = rng I2 & I1 is 'increasing & I2 is 'increasing holds
( P1 = P2 & I1 = I2 )

proof end;

:: Stirling numbers of the second kind

theorem :: STIRL2_1:66

for D being non empty set
for F being XFinSequence of D st ( for i being Nat st i in dom F holds
F . i is finite ) & ( for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j ) holds
ex CardF being XFinSequence of NAT st
( dom CardF = dom F & ( for i being Nat st i in dom CardF holds
CardF . i = card (F . i) ) & card (union (rng F)) = Sum CardF ) by Lm2;