:: by Karol P\c{a}k

::

:: Received March 15, 2005

:: Copyright (c) 2005-2016 Association of Mizar Users

registration
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

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

min* N < 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

end;
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;

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

end;
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;

:: 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}) ) ) );

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 )

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

for f being Function of (Segm n),(Segm k) st n > 0 holds

min* (f " {m}) <= n - 1

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})

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

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

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

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 ) )

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 ) ) )

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;

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;

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

end;
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 ) } ;

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

:: 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 ) } ;

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
end;

scheme :: STIRL2_1:sch 2

Sch2{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> set , F_{4}() -> set , F_{5}() -> Function of F_{1}(),F_{2}(), F_{6}( object ) -> object } :

Sch2{ F

ex h being Function of F_{3}(),F_{4}() st

( h | F_{1}() = F_{5}() & ( for x being set st x in F_{3}() \ F_{1}() holds

h . x = F_{6}(x) ) )

provided( h | F

h . x = F

A1:
for x being set st x in F_{3}() \ F_{1}() holds

F_{6}(x) in F_{4}()
and

A2: ( F_{1}() c= F_{3}() & F_{2}() c= F_{4}() )
and

A3: ( F_{2}() is empty implies F_{1}() is empty )

F

A2: ( F

A3: ( F

proof end;

scheme :: STIRL2_1:sch 3

Sch3{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> set , F_{4}() -> set , F_{5}( object ) -> object , P_{1}[ set , set , set ] } :

Sch3{ F

card { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }

providedf . x = F

A1:
for x being set st x in F_{3}() \ F_{1}() holds

F_{5}(x) in F_{4}()
and

A2: ( F_{1}() c= F_{3}() & F_{2}() c= F_{4}() )
and

A3: ( F_{2}() is empty implies F_{1}() is empty )
and

A4: for f being Function of F_{3}(),F_{4}() st ( for x being set st x in F_{3}() \ F_{1}() holds

F_{5}(x) = f . x ) holds

( P_{1}[f,F_{3}(),F_{4}()] iff P_{1}[f | F_{1}(),F_{1}(),F_{2}()] )

F

A2: ( F

A3: ( F

A4: for f being Function of F

F

( P

proof end;

scheme :: STIRL2_1:sch 4

Sch4{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> object , F_{4}() -> object , P_{1}[ set , set , set ] } :

Sch4{ F

card { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & f . F_{3}() = F_{4}() ) }

provided
A1:
( F_{2}() is empty implies F_{1}() is empty )
and

A2: not F_{3}() in F_{1}()
and

A3: for f being Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) st f . F_{3}() = F_{4}() holds

( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] iff P_{1}[f | F_{1}(),F_{1}(),F_{2}()] )

A2: not F

A3: for f being Function of (F

( P

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

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 )

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})

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 ) ) )

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 )

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})

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} )

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} )

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 ) }

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)))

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

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 )

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

end;
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_{1}[ 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_{1}[k,x]

A4: ( dom CardF = Segm (len F) & ( for k being Nat st k in Segm (len F) holds

S_{1}[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;

end;
A3: for k being Nat st k in Segm (len F) holds

ex x being Element of NAT st S

proof

consider CardF being XFinSequence of NAT such that
let k be Nat; :: thesis: ( k in Segm (len F) implies ex x being Element of NAT st S_{1}[k,x] )

assume k in Segm (len F) ; :: thesis: ex x being Element of NAT st S_{1}[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_{1}[k,x]
; :: thesis: verum

end;
assume k in Segm (len F) ; :: thesis: ex x being Element of NAT st S

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

A4: ( dom CardF = Segm (len F) & ( for k being Nat st k in Segm (len F) holds

S

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 )
;

end;

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;
hence card (union (rng F)) = Sum CardF by A7, A6, AFINSQ_2:def 8, BINOP_2:5; :: thesis: verum

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_{2}[ 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_{2}[k] holds

S_{2}[k + 1]

A28: C1 < C1 + 1 by NAT_1:13;

A29: F | (len CardF) = F by A4;

A30: S_{2}[ 0 ]
_{2}[k]
from NAT_1:sch 2(A30, A12);

hence card (union (rng F)) = Sum CardF by A11, A28, A29, A6; :: thesis: verum

end;
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

A12: for k being Nat st S

S

proof

reconsider C1 = (len CardF) - 1 as Element of NAT by A8, NAT_1:20;
let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

assume A13: S_{2}[k]
; :: thesis: S_{2}[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)

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;
assume A13: S

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

k + 1 in dom F
by A4, A14, NAT_1:44;
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;
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

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

A28: C1 < C1 + 1 by NAT_1:13;

A29: F | (len CardF) = F by A4;

A30: S

proof

for k being Nat holds S
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;
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

hence card (union (rng F)) = Sum CardF by A11, A28, A29, A6; :: thesis: verum

scheme :: STIRL2_1:sch 6

Sch8{ F_{1}() -> finite set , F_{2}() -> finite set , F_{3}() -> set , P_{1}[ set ], F_{4}() -> Function of (card F_{2}()),F_{2}() } :

Sch8{ F

ex F being XFinSequence of NAT st

( dom F = card F_{2}() & card { g where g is Function of F_{1}(),F_{2}() : P_{1}[g] } = Sum F & ( for i being Nat st i in dom F holds

F . i = card { g where g is Function of F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . i ) } ) )

provided( dom F = card F

F . i = card { g where g is Function of F

A1:
( F_{4}() is onto & F_{4}() is one-to-one )
and

A2: not F_{2}() is empty
and

A3: F_{3}() in F_{1}()

A2: not F

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

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)

n block 4 = (1 / 24) * ((((4 |^ n) - (4 * (3 |^ n))) + (6 * (2 |^ n))) - 4)

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 )

( 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 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} ) )

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

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 )

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 ) )

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 ) )

( 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 Th60: :: STIRL2_1:60

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 )

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,(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} )

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;

:: 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}) );

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))

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 )

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 )

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 )

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

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;