let X, Y be finite set ; :: thesis:
let F be Function of X,Y; :: thesis:
assume that
A1: dom F = X and
A2: F is one-to-one ; :: thesis:
deffunc H₁( object ) -> set = { h where h is Function of X,(rng F) : ( h is one-to-one & h . $1 = F . $1 ) } ;
A3: for x being object st x in X holds
H₁(x) in bool (Funcs (X,(rng F)))

let x be object ; :: thesis:
assume A4: x in X ; :: thesis:
H₁(x) c= Funcs (X,(rng F))

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in H₁(x) ; :: thesis:
then A5: ex h being Function of X,(rng F) st
( y = h & h is one-to-one & h . x = F . x ) ;
rng F <> {} by A1, A4, RELAT_1:42;
hence y in Funcs (X,(rng F)) by A5, FUNCT_2:8; :: thesis:

end;

hence H₁(x) in bool (Funcs (X,(rng F))) ; :: thesis:

end;

consider Fy9 being Function of X,(bool (Funcs (X,(rng F)))) such that
A6: for x being object st x in X holds
Fy9 . x = H₁(x) from FUNCT_2:sch 2(A3);
defpred S₁[ object , object ] means for n, k being Nat st n = $1 & k = (card X) - (n + 1) holds
$2 = k ! ;
A7: for x being object st x in Segm (card X) holds
ex y being object st
( y in NAT & S₁[x,y] )

proof

let x be object ; :: thesis:
assume A8: x in Segm (card X) ; :: thesis:
reconsider n = x as Element of NAT by A8;
n < card X by A8, NAT_1:44;
then n + 1 <= card X by NAT_1:13;
then reconsider k = (card X) - (n + 1) as Element of NAT by NAT_1:21;
S₁[n,k ! ] ;
hence ex y being object st
( y in NAT & S₁[x,y] ) ; :: thesis:

end;

consider XF being Function of (Segm (card X)),NAT such that
A9: for x being object st x in Segm (card X) holds
S₁[x,XF . x] from FUNCT_2:sch 1(A7);
for y being object st y in dom Fy9 holds
Fy9 . y is finite

proof

let y be object ; :: thesis:
assume y in dom Fy9 ; :: thesis:
then Fy9 . y in rng Fy9 by FUNCT_1:def 3;
hence Fy9 . y is finite ; :: thesis:

end;

then reconsider Fy = Fy9 as finite-yielding Function by FINSET_1:def 4;
reconsider rngF = rng F as finite set ;
A10: dom XF = card X by FUNCT_2:def 1;
then reconsider XF = XF as XFinSequence by AFINSQ_1:5;
reconsider XF = XF as XFinSequence of NAT ;
A11: for n being Nat st n in dom XF holds
ex x, y being set st
( x <> y & ( for f being Function st f in Choose (X,(n + 1),x,y) holds
card (Intersection (Fy,f,x)) = XF . n ) )

proof

let n be Nat; :: thesis:
assume A12: n in dom XF ; :: thesis:
n < len XF by A12, AFINSQ_1:86;
then n < card X by A10;
then A13: n + 1 <= card X by NAT_1:13;
then reconsider c = (card X) - (n + 1) as Element of NAT by NAT_1:21;
A14: (card X) -' (n + 1) = c by A13, XREAL_1:233;
take 0 ; :: thesis:
take 1 ; :: thesis:
thus 0 <> 1 ; :: thesis:
let f9 be Function; :: thesis:
assume f9 in Choose (X,(n + 1),0,1) ; :: thesis:
then consider f being Function of X,{0,1} such that
A15: f = f9 and
A16: card (f " {0}) = n + 1 by Def1;
reconsider f0 = f " {0} as finite set ;
set Xf0 = X \ f0;
set S = { h where h is Function of X,rngF : ( h is one-to-one & rng (h | (X \ f0)) c= F .: (X \ f0) & ( for x being set st x in f0 holds
h . x = F . x ) ) } ;
A17: Intersection (Fy,f,0) c= { h where h is Function of X,rngF : ( h is one-to-one & rng (h | (X \ f0)) c= F .: (X \ f0) & ( for x being set st x in f0 holds
h . x = F . x ) ) }

proof

assume not Intersection (Fy,f,0) c= { h where h is Function of X,rngF : ( h is one-to-one & rng (h | (X \ f0)) c= F .: (X \ f0) & ( for x being set st x in f0 holds
h . x = F . x ) ) } ; :: thesis:
then consider z being object such that
A18: z in Intersection (Fy,f,0) and
A19: not z in { h where h is Function of X,rngF : ( h is one-to-one & rng (h | (X \ f0)) c= F .: (X \ f0) & ( for x being set st x in f0 holds
h . x = F . x ) ) } ;
consider x9 being object such that
A20: x9 in f " {0} by A16, CARD_1:27, XBOOLE_0:def 1;
f . x9 in {0} by A20, FUNCT_1:def 7;
then A21: f . x9 = 0 by TARSKI:def 1;
x9 in dom f by A20, FUNCT_1:def 7;
then 0 in rng f by A21, FUNCT_1:def 3;
then consider x being set such that
A22: x in dom f and
f . x = 0 and
A23: z in Fy . x by A18, Th21;
z in H₁(x) by A6, A22, A23;
then consider h being Function of X,(rng F) such that
A24: z = h and
A25: h is one-to-one and
h . x = F . x ;
A26: for x1 being set st x1 in f0 holds
h . x1 = F . x1

proof

let x1 be set ; :: thesis:
assume A27: x1 in f0 ; :: thesis:
f . x1 in {0} by A27, FUNCT_1:def 7;
then A28: f . x1 = 0 by TARSKI:def 1;
( Fy9 . x1 = H₁(x1) & x1 in dom f ) by A6, A27, FUNCT_1:def 7;
then h in H₁(x1) by A18, A24, A28, Def2;
then ex h9 being Function of X,(rng F) st
( h = h9 & h9 is one-to-one & h9 . x1 = F . x1 ) ;
hence h . x1 = F . x1 ; :: thesis:

end;

rng (h | (X \ f0)) c= F .: (X \ f0)

proof

assume not rng (h | (X \ f0)) c= F .: (X \ f0) ; :: thesis:
then consider y being object such that
A29: y in rng (h | (X \ f0)) and
A30: not y in F .: (X \ f0) ;
consider x1 being object such that
A31: x1 in dom (h | (X \ f0)) and
A32: (h | (X \ f0)) . x1 = y by A29, FUNCT_1:def 3;
A33: h . x1 = y by A31, A32, FUNCT_1:47;
x1 in (dom h) /\ (X \ f0) by A31, RELAT_1:61;
then A34: x1 in X \ f0 by XBOOLE_0:def 4;
A35: F .: (X \ (X \ f0)) = (F .: X) \ (F .: (X \ f0)) by A2, FUNCT_1:64;
rngF = F .: X by A1, RELAT_1:113;
then y in (F .: X) \ (F .: (X \ f0)) by A29, A30, XBOOLE_0:def 5;
then consider x2 being object such that
A36: x2 in dom F and
A37: x2 in X \ (X \ f0) and
A38: y = F . x2 by A35, FUNCT_1:def 6;
y in rng F by A36, A38, FUNCT_1:def 3;
then A39: X = dom h by FUNCT_2:def 1;
X \ (X \ f0) = X /\ (f " {0}) by XBOOLE_1:48;
then x2 in f " {0} by A37, XBOOLE_0:def 4;
then A40: h . x2 = y by A26, A38;
not x2 in X \ f0 by A37, XBOOLE_0:def 5;
hence contradiction by A25, A36, A40, A33, A39, A34; :: thesis:

end;

hence contradiction by A19, A24, A25, A26; :: thesis:

end;

A41: X,rngF are_equipotent by A1, A2, WELLORD2:def 4;
then A42: card rngF = card X by CARD_1:5;
card rngF = card X by A41, CARD_1:5;
then A43: ( rngF = {} implies X is empty ) ;
A44: F is Function of X,rngF by A1, FUNCT_2:1;
{ h where h is Function of X,rngF : ( h is one-to-one & rng (h | (X \ f0)) c= F .: (X \ f0) & ( for x being set st x in f0 holds
h . x = F . x ) ) } c= Intersection (Fy,f,0)

proof

assume not { h where h is Function of X,rngF : ( h is one-to-one & rng (h | (X \ f0)) c= F .: (X \ f0) & ( for x being set st x in f0 holds
h . x = F . x ) ) } c= Intersection (Fy,f,0) ; :: thesis:
then consider z being object such that
A45: z in { h where h is Function of X,rngF : ( h is one-to-one & rng (h | (X \ f0)) c= F .: (X \ f0) & ( for x being set st x in f0 holds
h . x = F . x ) ) } and
A46: not z in Intersection (Fy,f,0) ;
consider h being Function of X,(rng F) such that
A47: h = z and
A48: h is one-to-one and
rng (h | (X \ f0)) c= F .: (X \ f0) and
A49: for x being set st x in f0 holds
h . x = F . x by A45;
consider x being object such that
A50: x in f " {0} by A16, CARD_1:27, XBOOLE_0:def 1;
x in X by A50;
then x in dom Fy9 by FUNCT_2:def 1;
then A51: Fy9 . x in rng Fy9 by FUNCT_1:def 3;
A52: Fy9 . x = H₁(x) by A6, A50;
h . x = F . x by A49, A50;
then h in Fy9 . x by A48, A52;
then h in union (rng Fy9) by A51, TARSKI:def 4;
then consider y being set such that
A53: y in dom f and
A54: f . y = 0 and
A55: not h in Fy . y by A46, A47, Def2;
f . y in {0} by A54, TARSKI:def 1;
then y in f " {0} by A53, FUNCT_1:def 7;
then h . y = F . y by A49;
then h in H₁(y) by A48;
hence contradiction by A6, A53, A55; :: thesis:

end;

then { h where h is Function of X,rngF : ( h is one-to-one & rng (h | (X \ f0)) c= F .: (X \ f0) & ( for x being set st x in f0 holds
h . x = F . x ) ) } = Intersection (Fy,f,0) by A17;
then card (Intersection (Fy,f,0)) = ((card X) -' (n + 1)) ! by A2, A16, A43, A44, A42, Th60;
hence card (Intersection (Fy,f9,0)) = XF . n by A9, A10, A12, A15, A14; :: thesis:

end;

A56: X,rngF are_equipotent by A1, A2, WELLORD2:def 4;
then card rngF = card X by CARD_1:5;
then A57: ( ((card rngF) -' (card X)) ! = 1 & card { f where f is Function of X,rngF : f is one-to-one } = ((card rngF) !) / (((card rngF) -' (card X)) !) ) by Th6, NEWTON:12, XREAL_1:232;
then reconsider One = { f where f is Function of X,(rng F) : f is one-to-one } as finite set ;
set S = { h where h is Function of X,(rng F) : ( h is one-to-one & ( for x being set st x in X holds
h . x <> F . x ) ) } ;
( dom XF = card X & dom Fy = X ) by FUNCT_2:def 1;
then consider F9 being XFinSequence of INT such that
A58: dom F9 = card X and
A59: card (union (rng Fy)) = Sum F9 and
A60: for n being Nat st n in dom F9 holds
F9 . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) by A11, Th57;
A61: union (rng Fy9) c= One

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union (rng Fy9) ; :: thesis:
then consider Fyx being set such that
A62: x in Fyx and
A63: Fyx in rng Fy9 by TARSKI:def 4;
consider x1 being object such that
A64: ( x1 in dom Fy9 & Fy . x1 = Fyx ) by A63, FUNCT_1:def 3;
x in H₁(x1) by A6, A62, A64;
then ex h being Function of X,(rng F) st
( h = x & h is one-to-one & h . x1 = F . x1 ) ;
hence x in One ; :: thesis:

end;

reconsider u = union (rng Fy) as finite set ;
A65: card (One \ u) = (card One) - (card u) by A61, CARD_2:44;
take F9 ; :: thesis:
thus dom F9 = card X by A58; :: thesis:
A66: One \ (union (rng Fy)) c= { h where h is Function of X,(rng F) : ( h is one-to-one & ( for x being set st x in X holds
h . x <> F . x ) ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A67: x in One \ (union (rng Fy)) ; :: thesis:
x in One by A67;
then consider f being Function of X,(rng F) such that
A68: f = x and
A69: f is one-to-one ;
assume not x in { h where h is Function of X,(rng F) : ( h is one-to-one & ( for x being set st x in X holds
h . x <> F . x ) ) } ; :: thesis:
then consider x being set such that
A70: x in X and
A71: f . x = F . x by A68, A69;
x in dom Fy by A70, FUNCT_2:def 1;
then Fy . x in rng Fy by FUNCT_1:def 3;
then A72: H₁(x) in rng Fy by A6, A70;
f in H₁(x) by A69, A71;
then f in union (rng Fy) by A72, TARSKI:def 4;
hence contradiction by A67, A68, XBOOLE_0:def 5; :: thesis:

end;

A73: { h where h is Function of X,(rng F) : ( h is one-to-one & ( for x being set st x in X holds
h . x <> F . x ) ) } c= One \ (union (rng Fy))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { h where h is Function of X,(rng F) : ( h is one-to-one & ( for x being set st x in X holds
h . x <> F . x ) ) } ; :: thesis:
then consider f being Function of X,(rng F) such that
A74: x = f and
A75: f is one-to-one and
A76: for x being set st x in X holds
f . x <> F . x ;
assume A77: not x in One \ (union (rng Fy)) ; :: thesis:
f in One by A75;
then f in union (rng Fy) by A74, A77, XBOOLE_0:def 5;
then consider Fyy being set such that
A78: f in Fyy and
A79: Fyy in rng Fy by TARSKI:def 4;
consider y being object such that
A80: y in dom Fy and
A81: Fy . y = Fyy by A79, FUNCT_1:def 3;
y in X by A80, FUNCT_2:def 1;
then f in H₁(y) by A6, A78, A81;
then A82: ex g being Function of X,(rng F) st
( f = g & g is one-to-one & g . y = F . y ) ;
y in X by A80, FUNCT_2:def 1;
hence contradiction by A76, A82; :: thesis:

end;

card One = (card X) ! by A56, A57, CARD_1:5;
hence card { h where h is Function of X,(rng F) : ( h is one-to-one & ( for x being set st x in X holds
h . x <> F . x ) ) } = ((card X) !) - (Sum F9) by A59, A66, A73, A65, XBOOLE_0:def 10; :: thesis:
let n be Nat; :: thesis:
assume A83: n in dom F9 ; :: thesis:
n < len F9 by A83, AFINSQ_1:86;
then n < card X by A58;
then A84: n + 1 <= card X by NAT_1:13;
then reconsider c = (card X) - (n + 1) as Element of NAT by NAT_1:21;
A85: (card X) choose (n + 1) = ((card X) !) / ((c !) * ((n + 1) !)) by A84, NEWTON:def 3;
XF . n = c ! by A9, A58, A83;
then A87: (XF . n) * ((card X) choose (n + 1)) = ((c !) * ((card X) !)) / ((c !) * ((n + 1) !)) by A85, XCMPLX_1:74
.= ((card X) !) * ((c !) / ((c !) * ((n + 1) !))) by XCMPLX_1:74
.= ((card X) !) * (((c !) / (c !)) / ((n + 1) !)) by XCMPLX_1:78
.= ((card X) !) * (1 / ((n + 1) !)) by XCMPLX_1:60
.= (((card X) !) * 1) / ((n + 1) !) by XCMPLX_1:74 ;
F9 . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) by A60, A83
.= ((- 1) |^ n) * (((card X) !) / ((n + 1) !)) by A87 ;
hence F9 . n = (((- 1) |^ n) * ((card X) !)) / ((n + 1) !) by XCMPLX_1:74; :: thesis: