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


begin

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 Ne, Ke 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 Element of n;
coherence
for b1 being Element of n holds b1 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 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= 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= 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= n & n > 0 holds
min* Ne <= n - 1
proof end;

definition
let n be Nat;
let X be set ;
let f be Function of 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,k;
let x be set ;
:: original: .
redefine func f . x -> Element of k;
coherence
f . x is Element of k
proof end;
end;

registration
let X be set ;
let Ne be Subset of NAT;
let f be Function of X,Ne;
let x be set ;
cluster f . x -> natural ;
coherence
f . x is natural
;
end;

definition
let n, k be Nat;
let f be Function of n,k;
attr f is "increasing means :Def1: :: 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 Def1 defines "increasing STIRL2_1:def 1 :
for n, k being Nat
for f being Function of n,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 n, k being Nat
for f being Function of n,k st n = 0 & k = 0 holds
( f is onto & f is "increasing )
proof end;

theorem Th16: :: STIRL2_1:16
for k, n, m being Nat
for f being Function of n,k st n > 0 holds
min* (f " {m}) <= n - 1
proof end;

theorem Th17: :: STIRL2_1:17
for n, k being Nat
for f being Function of n,k st f is onto holds
n >= k
proof end;

theorem Th18: :: STIRL2_1:18
for n, k being Nat
for f being Function of n,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 n,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 n, k being Nat
for f being Function of n,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 n,k st f = id n & n > 0 holds
f is "increasing
proof end;

theorem :: STIRL2_1:22
for n, k being Nat holds
not ( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & ( for f being Function of n,k holds not f is "increasing ) )
proof end;

theorem Th23: :: STIRL2_1:23
for n, k being Nat holds
not ( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & n >= k & ( for f being Function of n,k holds
( not f is onto or not f is "increasing ) ) )
proof end;

scheme :: STIRL2_1:sch 1
Sch1{ F1() -> Nat, F2() -> Nat, P1[ set ] } :
{ f where f is Function of F1(),F2() : P1[f] } is finite
proof end;

theorem Th24: :: STIRL2_1:24
for n, k being Nat holds { f where f is Function of n,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 n,k : ( f is onto & f is "increasing ) } is Element of NAT
proof end;

definition
let n, k be Nat;
func n block k -> Element of NAT equals :: STIRL2_1:def 2
card { f where f is Function of n,k : ( f is onto & f is "increasing ) } ;
coherence
card { f where f is Function of n,k : ( f is onto & f is "increasing ) } is Element of NAT
by Th25;
end;

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

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 n, k 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{ F1() -> set , F2() -> set , F3() -> set , F4() -> set , F5() -> Function of F1(),F2(), F6( set ) -> set } :
ex h being Function of F3(),F4() st
( h | F1() = F5() & ( for x being set st x in F3() \ F1() holds
h . x = F6(x) ) )
provided
A1: for x being set st x in F3() \ F1() holds
F6(x) in F4() and
A2: ( F1() c= F3() & F2() c= F4() ) and
A3: ( F2() is empty implies F1() is empty )
proof end;

scheme :: STIRL2_1:sch 3
Sch3{ F1() -> set , F2() -> set , F3() -> set , F4() -> set , F5( set ) -> set , P1[ set , set , set ] } :
card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
provided
A1: for x being set st x in F3() \ F1() holds
F5(x) in F4() and
A2: ( F1() c= F3() & F2() c= F4() ) and
A3: ( F2() is empty implies F1() is empty ) and
A4: for f being Function of F3(),F4() st ( for x being set st x in F3() \ F1() holds
F5(x) = f . x ) holds
( P1[f,F3(),F4()] iff P1[f | F1(),F1(),F2()] )
proof end;

scheme :: STIRL2_1:sch 4
Sch4{ F1() -> set , F2() -> set , F3() -> set , F4() -> set , P1[ set , set , set ] } :
card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & f . F3() = F4() ) }
provided
A1: ( F2() is empty implies F1() is empty ) and
A2: not F3() in F1() and
A3: for f being Function of (F1() \/ {F3()}),(F2() \/ {F4()}) st f . F3() = F4() holds
( P1[f,F1() \/ {F3()},F2() \/ {F4()}] iff P1[f | F1(),F1(),F2()] )
proof end;

theorem Th34: :: STIRL2_1:34
for n, k being Nat
for f being Function of (n + 1),(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 n, k being Nat
for f being Function of (n + 1),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 n, k, m, l being Nat
for f being Function of n,k
for g being Function of (n + m),(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 n, k being Nat
for f being Function of (n + 1),(k + 1) st f is onto & f is "increasing & f " {(f . n)} = {n} holds
( rng (f | n) c= k & ( for g being Function of n,k st g = f | n holds
( g is onto & g is "increasing ) ) )
proof end;

theorem Th38: :: STIRL2_1:38
for n, k being Nat
for f being Function of (n + 1),k
for g being Function of n,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 n, k, m being Nat
for f being Function of n,k
for g being Function of (n + 1),(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 n, k being Nat
for f being Function of n,k
for g being Function of (n + 1),(k + 1) st f is onto & f is "increasing & f = g | n & g . n = k holds
( g is onto & g is "increasing & g " {(g . n)} = {n} )
proof end;

theorem Th41: :: STIRL2_1:41
for n, k being Nat
for f being Function of n,k
for g being Function of (n + 1),k st f is onto & f is "increasing & f = g | 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 n, k being Nat holds card { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } = card { f where f is Function of n,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 (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } = card { f where f is Function of n,k : ( f is onto & f is "increasing ) }
proof end;

definition
canceled;
end;

:: deftheorem STIRL2_1:def 3 :
canceled;

theorem :: STIRL2_1:44
canceled;

theorem :: STIRL2_1:45
canceled;

theorem :: STIRL2_1:46
canceled;

theorem :: STIRL2_1:47
canceled;

theorem :: STIRL2_1:48
canceled;

theorem :: STIRL2_1:49
canceled;

definition
canceled;
end;

:: deftheorem STIRL2_1:def 4 :
canceled;

theorem :: STIRL2_1:50
canceled;

theorem :: STIRL2_1:51
canceled;

theorem :: STIRL2_1:52
canceled;

theorem :: STIRL2_1:53
canceled;

theorem Th54: :: STIRL2_1:54
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{ F1() -> non empty set , F2() -> Nat, P1[ set , set ] } :
ex p being XFinSequence of F1() st
( dom p = F2() & ( for k being Nat st k in F2() holds
P1[k,p . k] ) )
provided
A1: for k being Nat st k in F2() holds
ex x being Element of F1() st P1[k,x]
proof end;

Lm2: now
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 S1[ Nat, set ] means $2 = card (F . $1);
A3: for k being Nat st k in len F holds
ex x being Element of NAT st S1[k,x]
proof
let k be Nat; :: thesis: ( k in len F implies ex x being Element of NAT st S1[k,x] )
assume k in len F ; :: thesis: ex x being Element of NAT st S1[k,x]
then consider m being Nat such that
A4: F . k,m are_equipotent by A1, CARD_1:74;
card (F . k) = card m by A4, CARD_1:21;
hence ex x being Element of NAT st S1[k,x] ; :: thesis: verum
end;
consider CardF being XFinSequence of NAT such that
A5: ( dom CardF = len F & ( for k being Nat st k in len F holds
S1[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 A5; :: thesis: ( ( for i being Nat st i in dom CardF holds
CardF . i = card (F . i) ) & card (union (rng F)) = Sum CardF )

thus for i being Nat st i in dom CardF holds
CardF . i = card (F . i) by A5; :: thesis: card (union (rng F)) = Sum CardF
A6: addnat "**" CardF = Sum CardF by AFINSQ_2:63;
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 A5, RELAT_1:65, ZFMISC_1:2;
hence card (union (rng F)) = Sum CardF by A7, A6, AFINSQ_2:def 9, BINOP_2:5; :: thesis: verum
end;
suppose A8: len CardF <> 0 ; :: thesis: card (union (rng F)) = Sum CardF
then consider f being Function of NAT,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 9;
defpred S2[ 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 S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A13: S2[k] ; :: thesis: S2[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 set 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 A5, A14, NAT_1:45;
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 set such that
A22: X in dom (F | (k + 1)) and
A23: (F | (k + 1)) . X = Y by A21, FUNCT_1:def 5;
reconsider X = X as Element of NAT by A22;
A24: (F | (k + 1)) . X = F . X by A22, FUNCT_1:70;
A25: X in (dom F) /\ (k + 1) by A22, RELAT_1:90;
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 A5, A14, NAT_1:45;
then reconsider Fk1 = F . (k + 1) as finite set by A1;
k + 1 in len F by A5, A14, NAT_1:45;
then card Fk1 = CardF . (k + 1) by A5;
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:53, NAT_1:13;
hence ( card (union (rng (F | ((k + 1) + 1)))) = f . (k + 1) & union (rng (F | ((k + 1) + 1))) is finite ) by A27, Th54; :: 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 A5, RELAT_1:97;
A30: S2[ 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 Th54;
0 in len CardF by A8, NAT_1:45;
hence ( card (union (rng (F | (0 + 1)))) = f . 0 & union (rng (F | (0 + 1))) is finite ) by A1, A5, A9, A31, ZFMISC_1:2; :: thesis: verum
end;
for k being Nat holds S2[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{ F1() -> finite set , F2() -> finite set , F3() -> set , P1[ set ], F4() -> Function of (card F2()),F2() } :
ex F being XFinSequence of NAT st
( dom F = card F2() & card { g where g is Function of F1(),F2() : P1[g] } = Sum F & ( for i being Nat st i in dom F holds
F . i = card { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . i ) } ) )
provided
A1: ( F4() is onto & F4() is one-to-one ) and
A2: not F2() is empty and
A3: F3() in F1()
proof end;

theorem Th55: :: STIRL2_1:55
for k, n being Nat holds k * (n block k) = card { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }
proof end;

theorem Th56: :: STIRL2_1:56
for n, k being Nat holds (n + 1) block (k + 1) = ((k + 1) * (n block (k + 1))) + (n block k)
proof end;

theorem Th57: :: STIRL2_1:57
for n being Nat st n >= 1 holds
n block 2 = (1 / 2) * ((2 |^ n) - 2)
proof end;

theorem Th58: :: STIRL2_1:58
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:59
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 Th60: :: STIRL2_1:60
( 3 ! = 6 & 4 ! = 24 )
proof end;

theorem Th61: :: STIRL2_1:61
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 Th62: :: STIRL2_1:62
for n being Nat holds (n + 1) block n = (n + 1) choose 2
proof end;

theorem :: STIRL2_1:63
for n being Nat holds (n + 2) block n = (3 * ((n + 2) choose 4)) + ((n + 2) choose 3)
proof end;

theorem Th64: :: STIRL2_1:64
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 Th65: :: STIRL2_1:65
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{ P1[ set ], P2[ set , Function] } :
for F being Function st rng F is finite holds
P1[F]
provided
A1: P1[ {} ] and
A2: for F being Function st ( for x being set st x in rng F & P2[x,F] holds
P1[F | ((dom F) \ (F " {x}))] ) holds
P1[F]
proof end;

theorem Th66: :: STIRL2_1:66
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 Th67: :: STIRL2_1:67
for X, Y, x, y being set 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 Th68: :: STIRL2_1:68
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 Th69: :: STIRL2_1:69
for N being finite Subset of NAT ex Order being Function of N,(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;

Lm4: for X being finite set
for x being set st x in X holds
card (X \ {x}) < card X
proof end;

theorem Th70: :: STIRL2_1:70
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 )
proof end;

Lm5: for n being Element of NAT
for N being finite Subset of NAT
for F being Function of N,(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 Th71: :: STIRL2_1:71
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 :Def5: :: STIRL2_1:def 5
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 Def5 defines "increasing STIRL2_1:def 5 :
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 Th72: :: STIRL2_1:72
for Ne, Ke 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;

theorem :: STIRL2_1:73
for Ne, Ke 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;

theorem Th74: :: STIRL2_1:74
for Ne, Ke, 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:75
for Ne, Ke 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;

theorem :: STIRL2_1:76
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;