let n, k be Nat; :: thesis:
assume A1: k <= n ; :: thesis:

suppose A2: ( n = 0 & k = 0 ) ; :: thesis:

reconsider I = 1 as Element of INT by INT_1:def 2;
set F = <%I%>;
take F = <%I%>; :: thesis:
addint "**" <%I%> = 1 by AFINSQ_2:37;
then Sum F = 1 by AFINSQ_2:50;
hence n block k = (1 / (k !)) * (Sum F) by A2, NEWTON:12, STIRL2_1:26; :: thesis:
thus dom F = k + 1 by A2, AFINSQ_1:33; :: thesis:
let m be Nat; :: thesis:
assume m in dom F ; :: thesis:
then A3: m in {0} by AFINSQ_1:33, CARD_1:49;
then m = 0 by TARSKI:def 1;
then A4: (- 1) |^ m = 1 by NEWTON:4;
A5: (k - m) |^ n = 1 by A2, NEWTON:4;
A6: 0 choose 0 = 1 by NEWTON:19;
m = 0 by A3, TARSKI:def 1;
hence F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n) by A2, A4, A5, A6; :: thesis:

end;

suppose A7: ( n <> 0 & k = 0 ) ; :: thesis:

set F = (k + 1) --> 0;
reconsider Fi = (k + 1) --> 0 as XFinSequence of INT ;
reconsider Fn = (k + 1) --> 0 as XFinSequence of NAT ;
take Fi = Fi; :: thesis:
( rng ((k + 1) --> 0) c= {0} & {0} c= {0,0} ) by ENUMSET1:29, FUNCOP_1:13;
then Sum Fn = 0 * (card (Fn " {0})) by AFINSQ_2:68, XBOOLE_1:1;
hence ( n block k = (1 / (k !)) * (Sum Fi) & dom Fi = k + 1 ) by A7, STIRL2_1:31; :: thesis:
let m be Nat; :: thesis:
assume m in dom Fi ; :: thesis:

now :: thesis:

per cases ;

suppose m = 0 ; :: thesis:

then (k - m) |^ n = 0 by A7, NAT_1:14, NEWTON:11;
hence (k choose m) * ((k - m) |^ n) = 0 ; :: thesis:

end;

suppose m > 0 ; :: thesis:

then k choose m = 0 by A7, NEWTON:def 3;
hence (k choose m) * ((k - m) |^ n) = 0 ; :: thesis:

end;

then A9: ((- 1) |^ m) * ((k choose m) * ((k - m) |^ n)) = 0 ;
thus Fi . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n) by A9; :: thesis:

end;

suppose A10: ( n <> 0 & k <> 0 ) ; :: thesis:

set Perm = { p where p is Function of k,k : p is Permutation of k } ;
card { p where p is Function of k,k : p is Permutation of k } = (card k) ! by Th7;
then reconsider Perm = { p where p is Function of k,k : p is Permutation of k } as finite set ;
reconsider Bloc = { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } as finite set by STIRL2_1:24;
set Onto = { f where f is Function of n,k : f is onto } ;
defpred S₁[ object , object ] means for p being Function of k,k
for f being Function of n,k st $1 = [p,f] holds
$2 = p * f;
reconsider N = n, K = k as non empty Subset of NAT by A10, STIRL2_1:8;
A11: card [:Perm,Bloc:] = (card Perm) * (card Bloc) by CARD_2:46;
A12: for x being object st x in [:Perm,Bloc:] holds
ex y being object st
( y in { f where f is Function of n,k : f is onto } & S₁[x,y] )

proof

let x be object ; :: thesis:
assume x in [:Perm,Bloc:] ; :: thesis:
then consider p9, f9 being object such that
A13: p9 in Perm and
A14: f9 in Bloc and
A15: x = [p9,f9] by ZFMISC_1:def 2;
consider f being Function of (Segm n),(Segm k) such that
A16: f = f9 and
A17: ( f is onto & f is "increasing ) by A14;
A18: rng f = Segm k by A17, FUNCT_2:def 3;
consider p being Function of (Segm k),(Segm k) such that
A19: p = p9 and
A20: p is Permutation of (Segm k) by A13;
reconsider pf = p * f as Function of (Segm n),(Segm k) ;
take pf ; :: thesis:
A21: dom p = Segm k by A10, FUNCT_2:def 1;
rng p = k by A20, FUNCT_2:def 3;
then rng (p * f) = k by A18, A21, RELAT_1:28;
then pf is onto by FUNCT_2:def 3;
hence pf in { f where f is Function of n,k : f is onto } ; :: thesis:
let p1 be Function of k,k; :: thesis:
let f1 be Function of n,k; :: thesis:
assume A22: x = [p1,f1] ; :: thesis:
p1 = p by A15, A19, A22, XTUPLE_0:1;
hence pf = p1 * f1 by A15, A16, A22, XTUPLE_0:1; :: thesis:

end;

consider FP being Function of [:Perm,Bloc:], { f where f is Function of n,k : f is onto } such that
A23: for x being object st x in [:Perm,Bloc:] holds
S₁[x,FP . x] from FUNCT_2:sch 1(A12);
A24: FP is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A25: x1 in dom FP and
A26: x2 in dom FP and
A27: FP . x1 = FP . x2 ; :: thesis:
consider p19, f19 being object such that
A28: p19 in Perm and
A29: f19 in Bloc and
A30: x1 = [p19,f19] by A25, ZFMISC_1:def 2;
consider p1 being Function of k,k such that
A31: p19 = p1 and
A32: p1 is Permutation of k by A28;
consider p29, f29 being object such that
A33: p29 in Perm and
A34: f29 in Bloc and
A35: x2 = [p29,f29] by A26, ZFMISC_1:def 2;
FP . x1 in rng FP by A25, FUNCT_1:def 3;
then FP . x1 in { f where f is Function of n,k : f is onto } ;
then consider fp being Function of N,K such that
A36: FP . x1 = fp and
A37: fp is onto ;
A38: rng fp = K by A37, FUNCT_2:def 3;
consider p2 being Function of k,k such that
A39: p29 = p2 and
A40: p2 is Permutation of k by A33;
consider f2 being Function of (Segm n),(Segm k) such that
A41: f29 = f2 and
A42: ( f2 is onto & f2 is "increasing ) by A34;
rng fp = K by A37, FUNCT_2:def 3;
then reconsider p199 = p1, p299 = p2 as Permutation of (rng fp) by A32, A40;
consider f1 being Function of (Segm n),(Segm k) such that
A43: f19 = f1 and
A44: ( f1 is onto & f1 is "increasing ) by A29;
reconsider f199 = f1, f299 = f2 as Function of N,K ;
A45: rng f2 = K by A42, FUNCT_2:def 3;
for l, m being Nat st l in rng f1 & m in rng f1 & l < m holds
min* (f1 " {l}) < min* (f1 " {m}) by A44, STIRL2_1:def 1;
then A46: f199 is 'increasing by STIRL2_1:def 3;
for l, m being Nat st l in rng f2 & m in rng f2 & l < m holds
min* (f2 " {l}) < min* (f2 " {m}) by A42, STIRL2_1:def 1;
then A47: f299 is 'increasing by STIRL2_1:def 3;
A48: fp = p199 * f199 by A23, A25, A30, A31, A43, A36;
A49: rng f1 = K by A44, FUNCT_2:def 3;
A50: fp = p299 * f299 by A23, A26, A27, A35, A39, A41, A36;
then p199 = p299 by A46, A47, A49, A45, A48, A38, STIRL2_1:65;
hence x1 = x2 by A30, A31, A43, A35, A39, A41, A46, A47, A49, A45, A48, A50, A38, STIRL2_1:65; :: thesis:

end;

consider h being Function of (Segm n),(Segm k) such that
A51: ( h is onto & h is "increasing ) by A1, A10, STIRL2_1:23;
{ f where f is Function of n,k : f is onto } c= rng FP

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { f where f is Function of n,k : f is onto } ; :: thesis:
then consider f being Function of n,k such that
A52: f = x and
A53: f is onto ;
rng f = K by A53, FUNCT_2:def 3;
then consider I being Function of N,K, P being Permutation of K such that
A54: f = P * I and
A55: K = rng I and
A56: I is 'increasing by STIRL2_1:63;
set p = P;
reconsider i = I as Function of (Segm n),(Segm k) ;
for l, m being Nat st l in rng I & m in rng I & l < m holds
min* (I " {l}) < min* (I " {m}) by A56, STIRL2_1:def 3;
then A57: i is "increasing by STIRL2_1:def 1;
i is onto by A55, FUNCT_2:def 3;
then ( P in Perm & i in Bloc ) by A57;
then A58: [P,i] in [:Perm,Bloc:] by ZFMISC_1:def 2;
h in { f where f is Function of n,k : f is onto } by A51;
then A59: [P,i] in dom FP by A58, FUNCT_2:def 1;
FP . [P,i] = f by A23, A54, A58;
hence x in rng FP by A52, A59, FUNCT_1:def 3; :: thesis:

end;

then A60: rng FP = { f where f is Function of n,k : f is onto } ;
h in { f where f is Function of n,k : f is onto } by A51;
then dom FP = [:Perm,Bloc:] by FUNCT_2:def 1;
then { f where f is Function of n,k : f is onto } ,[:Perm,Bloc:] are_equipotent by A24, A60, WELLORD2:def 4;
then A61: card { f where f is Function of n,k : f is onto } = (card Perm) * (card Bloc) by A11, CARD_1:5;
A62: ( ((k !) * (card Bloc)) / (k !) = (card Bloc) * ((k !) / (k !)) & (k !) / (k !) = 1 ) by XCMPLX_1:60, XCMPLX_1:74;
consider F being XFinSequence of INT such that
A63: dom F = (card k) + 1 and
A64: Sum F = card { f where f is Function of n,k : f is onto } and
A65: for m being Nat st m in dom F holds
F . m = (((- 1) |^ m) * ((card k) choose m)) * (((card k) - m) |^ (card n)) by A10, Th58;
take F = F; :: thesis:
card Perm = (card k) ! by Th7;
then Sum F = (k !) * (card Bloc) by A64, A61;
then n block k = ((Sum F) * 1) / (k !) by A62, STIRL2_1:def 2;
hence n block k = (1 / (k !)) * (Sum F) by XCMPLX_1:74; :: thesis:
thus dom F = k + 1 by A63; :: thesis:
let m be Nat; :: thesis:
assume m in dom F ; :: thesis:
hence F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n) by A65; :: thesis:

end;

suppose ( n = 0 & k <> 0 ) ; :: thesis:

hence ex F being XFinSequence of INT st
( n block k = (1 / (k !)) * (Sum F) & dom F = k + 1 & ( for m being Nat st m in dom F holds
F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n) ) ) by A1; :: thesis:

end;

hence ex F being XFinSequence of INT st
( n block k = (1 / (k !)) * (Sum F) & dom F = k + 1 & ( for m being Nat st m in dom F holds
F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n) ) ) ; :: thesis: