:: Stirling Numbers of the Second Kind :: by Karol P\c{a}k :: :: Received March 15, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users begin theorem Th1: :: STIRL2_1:1 for N being non empty Subset of NAT holds min N = min* N proofend; theorem Th2: :: STIRL2_1:2 for K, N being non empty Subset of NAT holds min ((min K),(min N)) = min (K \/ N) proofend; theorem :: STIRL2_1:3 for Ke, Ne being Subset of NAT holds min ((min* Ke),(min* Ne)) <= min* (Ke \/ Ne) proofend; theorem :: STIRL2_1:4 for Ne, Ke being Subset of NAT st not min* Ne in Ne /\ Ke holds min* Ne = min* (Ne \ Ke) proofend; theorem Th5: :: STIRL2_1:5 for n being Element of NAT holds ( min* {n} = n & min {n} = n ) proofend; 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) ) proofend; theorem :: STIRL2_1:7 for n, k, l being Element of NAT holds min* {n,k,l} = min (n,(min (k,l))) proofend; theorem Th8: :: STIRL2_1:8 for n being Nat holds n is Subset of NAT proofend; registration let n be Nat; cluster -> natural for 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 proofend; theorem Th10: :: STIRL2_1:10 for k, n being Nat st k in n holds ( k <= n - 1 & n - 1 is Element of NAT ) proofend; theorem :: STIRL2_1:11 for n being Nat holds min* n = 0 proofend; 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 proofend; 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 proofend; 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 proofend; definition let n be Nat; let X be set ; let f be Function of n,X; let x be set ; :: original:" redefine funcf " x -> Subset of NAT; coherence f " x is Subset of NAT proofend; end; definition let X be set ; let k be Nat; let f be Function of X,k; let x be set ; :: original:. redefine funcf . x -> Element of k; coherence f . x is Element of k proofend; end; definition let n, k be Nat; let f be Function of n,k; attrf 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 ) proofend; 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 proofend; theorem Th17: :: STIRL2_1:17 for n, k being Nat for f being Function of n,k st f is onto holds n >= k proofend; 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}) proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) ) proofend; 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 ) ) ) proofend; scheme :: STIRL2_1:sch 1 Sch1{ F1() -> Nat, F2() -> Nat, P1[ set ] } : { f where f is Function of F1(),F2() : P1[f] } is finite proofend; 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 proofend; 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 proofend; :: Stirling Numbers of the second kind definition let n, k be Nat; funcn 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 proofend; theorem Th27: :: STIRL2_1:27 for k being Nat st k <> 0 holds 0 block k = 0 proofend; 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 proofend; theorem :: STIRL2_1:30 for n being Nat holds ( n block 0 = 1 iff n = 0 ) proofend; theorem Th31: :: STIRL2_1:31 for n being Nat st n <> 0 holds n block 0 = 0 proofend; theorem Th32: :: STIRL2_1:32 for n being Nat st n <> 0 holds n block 1 = 1 proofend; theorem :: STIRL2_1:33 for k, n being Nat holds ( ( ( 1 <= k & k <= n ) or k = n ) iff n block k > 0 ) proofend; 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 ) proofend; 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()] ) proofend; 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()] ) proofend; 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 proofend; 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 ) proofend; 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}) proofend; 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 ) ) ) proofend; 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 ) proofend; 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}) proofend; 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} ) proofend; 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} ) proofend; Lm1: for k, n being Nat st k < n holds n \/ {k} = n proofend; 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 ) } proofend; 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 ) } proofend; 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))) proofend; 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] proofend; 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 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:43; card (F . k) = card m by A4, CARD_1:5; 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:51; percases ( len CardF = 0 or len CardF <> 0 ) ; supposeA7: len CardF = 0 ; ::_thesis: card (union (rng F)) = Sum CardF then union (rng F) is empty by A5, 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; supposeA8: 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_8; 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: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 set 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 A5, A14, NAT_1:44; then reconsider Fk1 = F . (k + 1) as finite set by A1; k + 1 in len F by A5, A14, NAT_1:44; 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: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 A5, RELAT_1:68; 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 Th44; 0 in len CardF by A8, NAT_1:44; 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() proofend; theorem Th45: :: STIRL2_1:45 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} ) } proofend; :: Recursive dependence theorem Th46: :: STIRL2_1:46 for n, k being Nat holds (n + 1) block (k + 1) = ((k + 1) * (n block (k + 1))) + (n block k) proofend; theorem Th47: :: STIRL2_1:47 for n being Nat st n >= 1 holds n block 2 = (1 / 2) * ((2 |^ n) - 2) proofend; theorem Th48: :: STIRL2_1:48 for n being Nat st n >= 2 holds n block 3 = (1 / 6) * (((3 |^ n) - (3 * (2 |^ n))) + 3) proofend; Lm3: for n being Nat holds n |^ 3 = (n * n) * n proofend; 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) proofend; theorem Th50: :: STIRL2_1:50 ( 3 ! = 6 & 4 ! = 24 ) proofend; 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 ) proofend; theorem Th52: :: STIRL2_1:52 for n being Nat holds (n + 1) block n = (n + 1) choose 2 proofend; theorem :: STIRL2_1:53 for n being Nat holds (n + 2) block n = (3 * ((n + 2) choose 4)) + ((n + 2) choose 3) proofend; 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} ) ) proofend; 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 proofend; 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] proofend; 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 proofend; theorem Th57: :: STIRL2_1:57 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 ) proofend; 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 ) ) proofend; theorem Th59: :: STIRL2_1:59 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 ) ) proofend; Lm4: for X being finite set for x being set st x in X holds card (X \ {x}) < card X proofend; 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 ) proofend; 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 ) ) proofend; 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} ) proofend; definition let Ne, Ke be Subset of NAT; let f be Function of Ne,Ke; attrf is "increasing means :Def3: :: 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 Def3 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 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)) proofend; :: existence of an expansion theorem :: STIRL2_1:63 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 ) proofend; :: uniqueness of expansion theorem Th64: :: STIRL2_1:64 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 ) proofend; theorem :: STIRL2_1:65 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 ) proofend; :: [WP: ] 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;