let n, k be Nat; ( k <= n implies ex F being XFinSequence of 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) ) ) )
assume A1:
k <= n
; ex F being XFinSequence of 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) ) )
now per cases
( ( n = 0 & k = 0 ) or ( n <> 0 & k = 0 ) or ( n <> 0 & k <> 0 ) or ( n = 0 & k <> 0 ) )
;
suppose A2:
(
n = 0 &
k = 0 )
;
ex F being set 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) ) )reconsider I = 1 as
Element of
INT by INT_1:def 2;
set F =
<%I%>;
take F =
<%I%>;
( 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) ) )
addint "**" <%I%> = 1
by AFINSQ_2:49;
then
Sum F = 1
by AFINSQ_2:62;
hence
n block k = (1 / (k !)) * (Sum F)
by A2, NEWTON:18, STIRL2_1:26;
( dom F = k + 1 & ( for m being Nat st m in dom F holds
F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n) ) )thus
dom F = k + 1
by A2, AFINSQ_1:36;
for m being Nat st m in dom F holds
F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n)let m be
Nat;
( m in dom F implies F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n) )assume
m in dom F
;
F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n)then A3:
m in {0}
by AFINSQ_1:36, CARD_1:87;
then
m = 0
by TARSKI:def 1;
then A4:
(- 1) |^ m = 1
by NEWTON:9;
A5:
(k - m) |^ n = 1
by A2, NEWTON:9;
X:
0 choose 0 = 1
by NEWTON:29;
m = 0
by A3, TARSKI:def 1;
hence
F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n)
by A2, A4, A5, AFINSQ_1:38, X;
verum end; suppose A12:
(
n <> 0 &
k <> 0 )
;
ex F being XFinSequence of 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) ) )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 Th8;
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 n,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 S1[
set ,
set ]
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 A12, STIRL2_1:8;
A13:
card [:Perm,Bloc:] = (card Perm) * (card Bloc)
by CARD_2:65;
A14:
for
x being
set st
x in [:Perm,Bloc:] holds
ex
y being
set st
(
y in { f where f is Function of n,k : f is onto } &
S1[
x,
y] )
proof
let x be
set ;
( x in [:Perm,Bloc:] implies ex y being set st
( y in { f where f is Function of n,k : f is onto } & S1[x,y] ) )
assume
x in [:Perm,Bloc:]
;
ex y being set st
( y in { f where f is Function of n,k : f is onto } & S1[x,y] )
then consider p9,
f9 being
set such that A15:
p9 in Perm
and A16:
f9 in Bloc
and A17:
x = [p9,f9]
by ZFMISC_1:def 2;
consider f being
Function of
n,
k such that A18:
f = f9
and A19:
(
f is
onto &
f is
"increasing )
by A16;
A20:
rng f = k
by A19, FUNCT_2:def 3;
consider p being
Function of
k,
k such that A21:
p = p9
and A22:
p is
Permutation of
k
by A15;
reconsider pf =
p * f as
Function of
n,
k ;
take
pf
;
( pf in { f where f is Function of n,k : f is onto } & S1[x,pf] )
A23:
dom p = k
by A12, FUNCT_2:def 1;
rng p = k
by A22, FUNCT_2:def 3;
then
rng (p * f) = k
by A20, A23, RELAT_1:47;
then
pf is
onto
by FUNCT_2:def 3;
hence
pf in { f where f is Function of n,k : f is onto }
;
S1[x,pf]
let p1 be
Function of
k,
k;
for f being Function of n,k st x = [p1,f] holds
pf = p1 * flet f1 be
Function of
n,
k;
( x = [p1,f1] implies pf = p1 * f1 )
assume A24:
x = [p1,f1]
;
pf = p1 * f1
p1 = p
by A17, A21, A24, ZFMISC_1:33;
hence
pf = p1 * f1
by A17, A18, A24, ZFMISC_1:33;
verum
end; consider FP being
Function of
[:Perm,Bloc:],
{ f where f is Function of n,k : f is onto } such that A25:
for
x being
set st
x in [:Perm,Bloc:] holds
S1[
x,
FP . x]
from FUNCT_2:sch 1(A14);
A26:
FP is
one-to-one
proof
let x1 be
set ;
FUNCT_1:def 8 for b1 being set holds
( not x1 in proj1 FP or not b1 in proj1 FP or not FP . x1 = FP . b1 or x1 = b1 )let x2 be
set ;
( not x1 in proj1 FP or not x2 in proj1 FP or not FP . x1 = FP . x2 or x1 = x2 )
assume that A27:
x1 in dom FP
and A28:
x2 in dom FP
and A29:
FP . x1 = FP . x2
;
x1 = x2
consider p19,
f19 being
set such that A30:
p19 in Perm
and A31:
f19 in Bloc
and A32:
x1 = [p19,f19]
by A27, ZFMISC_1:def 2;
consider p1 being
Function of
k,
k such that A33:
p19 = p1
and A34:
p1 is
Permutation of
k
by A30;
consider p29,
f29 being
set such that A35:
p29 in Perm
and A36:
f29 in Bloc
and A37:
x2 = [p29,f29]
by A28, ZFMISC_1:def 2;
FP . x1 in rng FP
by A27, FUNCT_1:def 5;
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 A38:
FP . x1 = fp
and A39:
fp is
onto
;
A40:
rng fp = K
by A39, FUNCT_2:def 3;
consider p2 being
Function of
k,
k such that A41:
p29 = p2
and A42:
p2 is
Permutation of
k
by A35;
consider f2 being
Function of
n,
k such that A43:
f29 = f2
and A44:
(
f2 is
onto &
f2 is
"increasing )
by A36;
rng fp = K
by A39, FUNCT_2:def 3;
then reconsider p199 =
p1,
p299 =
p2 as
Permutation of
(rng fp) by A34, A42;
consider f1 being
Function of
n,
k such that A45:
f19 = f1
and A46:
(
f1 is
onto &
f1 is
"increasing )
by A31;
reconsider f199 =
f1,
f299 =
f2 as
Function of
N,
K ;
A47:
rng f2 = K
by A44, 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 A46, STIRL2_1:def 1;
then A48:
f199 is
"increasing
by STIRL2_1:def 5;
for
l,
m being
Nat st
l in rng f2 &
m in rng f2 &
l < m holds
min* (f2 " {l}) < min* (f2 " {m})
by A44, STIRL2_1:def 1;
then A49:
f299 is
"increasing
by STIRL2_1:def 5;
A50:
fp = p199 * f199
by A25, A27, A32, A33, A45, A38;
A51:
rng f1 = K
by A46, FUNCT_2:def 3;
A52:
fp = p299 * f299
by A25, A28, A29, A37, A41, A43, A38;
then
p199 = p299
by A48, A49, A51, A47, A50, A40, STIRL2_1:75;
hence
x1 = x2
by A32, A33, A45, A37, A41, A43, A48, A49, A51, A47, A50, A52, A40, STIRL2_1:75;
verum
end; consider h being
Function of
n,
k such that A53:
(
h is
onto &
h is
"increasing )
by A1, A12, STIRL2_1:23;
{ f where f is Function of n,k : f is onto } c= rng FP
proof
let x be
set ;
TARSKI:def 3 ( not x in { f where f is Function of n,k : f is onto } or x in rng FP )
assume
x in { f where f is Function of n,k : f is onto }
;
x in rng FP
then consider f being
Function of
n,
k such that A54:
f = x
and A55:
f is
onto
;
rng f = K
by A55, FUNCT_2:def 3;
then consider I being
Function of
N,
K,
P being
Permutation of
K such that A56:
f = P * I
and A57:
K = rng I
and A58:
I is
"increasing
by STIRL2_1:73;
set p =
P;
reconsider i =
I as
Function of
n,
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 A58, STIRL2_1:def 5;
then A59:
i is
"increasing
by STIRL2_1:def 1;
i is
onto
by A57, FUNCT_2:def 3;
then
(
P in Perm &
i in Bloc )
by A59;
then A60:
[P,i] in [:Perm,Bloc:]
by ZFMISC_1:def 2;
h in { f where f is Function of n,k : f is onto }
by A53;
then A61:
[P,i] in dom FP
by A60, FUNCT_2:def 1;
FP . [P,i] = f
by A25, A56, A60;
hence
x in rng FP
by A54, A61, FUNCT_1:def 5;
verum
end; then A62:
rng FP = { f where f is Function of n,k : f is onto }
by XBOOLE_0:def 10;
h in { f where f is Function of n,k : f is onto }
by A53;
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 A26, A62, WELLORD2:def 4;
then A63:
card { f where f is Function of n,k : f is onto } = (card Perm) * (card Bloc)
by A13, CARD_1:21;
k ! > 0
by NEWTON:23;
then A64:
(
((k !) * (card Bloc)) / (k !) = (card Bloc) * ((k !) / (k !)) &
(k !) / (k !) = 1 )
by XCMPLX_1:60, XCMPLX_1:75;
consider F being
XFinSequence of
such that A65:
dom F = (card k) + 1
and A66:
Sum F = card { f where f is Function of n,k : f is onto }
and A67:
for
m being
Nat st
m in dom F holds
F . m = (((- 1) |^ m) * ((card k) choose m)) * (((card k) - m) |^ (card n))
by A12, Th70;
take F =
F;
( 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) ) )
card Perm = (card k) !
by Th8;
then
Sum F = (k !) * (card Bloc)
by A66, A63, CARD_1:def 5;
then
n block k = ((Sum F) * 1) / (k !)
by A64, STIRL2_1:def 2;
hence
n block k = (1 / (k !)) * (Sum F)
by XCMPLX_1:75;
( dom F = k + 1 & ( for m being Nat st m in dom F holds
F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n) ) )thus
dom F = k + 1
by A65, CARD_1:def 5;
for m being Nat st m in dom F holds
F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n)A68:
(
card k = k &
card n = n )
by CARD_1:def 5;
let m be
Nat;
( m in dom F implies F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n) )assume
m in dom F
;
F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n)hence
F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n)
by A67, A68;
verum end;
hence
ex F being XFinSequence of 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) ) )
; verum