let X, Y be finite set ; :: thesis:
assume that
A1: not X is empty and
A2: not Y is empty ; :: thesis:
defpred S₁[ set , set ] means for n being Nat st n = $1 holds
$2 = (((card Y) - n) - 1) |^ (card X);
A3: for x being set st x in card Y holds
ex y being set st
( y in NAT & S₁[x,y] )

let x be set ; :: thesis:
assume A4: x in card Y ; :: thesis:
card Y is Subset of NAT by STIRL2_1:8;
then reconsider n = x as Element of NAT by A4;
n < card Y by A4, NAT_1:45;
then n + 1 <= card Y by NAT_1:13;
then reconsider k = (card Y) - (n + 1) as Element of NAT by NAT_1:21;
S₁[n,k |^ (card X)] ;
hence ex y being set st
( y in NAT & S₁[x,y] ) ; :: thesis:

end;

consider XF being Function of (card Y),NAT such that
A5: for x being set st x in card Y holds
S₁[x,XF . x] from FUNCT_2:sch 1(A3);
set Onto = { f where f is Function of X,Y : f is onto } ;
deffunc H₁( set ) -> set = { f where f is Function of X,Y : not $1 in rng f } ;
A6: for x being set st x in Y holds
H₁(x) in bool (Funcs X,Y)

proof

let x be set ; :: thesis:
assume A7: x in Y ; :: thesis:
H₁(x) c= Funcs X,Y

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in H₁(x) ; :: thesis:
then ex f being Function of X,Y st
( y = f & not x in rng f ) ;
hence y in Funcs X,Y by A7, FUNCT_2:11; :: thesis:

end;

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

end;

consider Fy9 being Function of Y,(bool (Funcs X,Y)) such that
A8: for x being set st x in Y holds
Fy9 . x = H₁(x) from FUNCT_2:sch 2(A6);
for y being set holds Fy9 . y is finite

proof

let y be set ; :: thesis:

per cases ;

suppose y in dom Fy9 ; :: thesis:

then Fy9 . y in rng Fy9 by FUNCT_1:def 5;
hence Fy9 . y is finite ; :: thesis:

end;

suppose not y in dom Fy9 ; :: thesis:

hence Fy9 . y is finite by FUNCT_1:def 4; :: thesis:

end;

then reconsider Fy = Fy9 as finite-yielding Function by Def3;
union (rng Fy9) c= union (bool (Funcs X,Y)) by ZFMISC_1:95;
then A9: union (rng Fy) c= Funcs X,Y by ZFMISC_1:99;
then reconsider u = union (rng Fy) as finite set ;
A10: dom XF = card Y by FUNCT_2:def 1;
then reconsider XF = XF as XFinSequence by AFINSQ_1:7;
reconsider XF = XF as XFinSequence of ;
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 Y,(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:
take 0 ; :: thesis:
take 1 ; :: thesis:
thus 0 <> 1 ; :: thesis:
let f9 be Function; :: thesis:
assume f9 in Choose Y,(n + 1),0 ,1 ; :: thesis:
then consider f being Function of Y,{0 ,1} such that
A13: f = f9 and
A14: card (f " {0 }) = n + 1 by Def1;
A15: Intersection Fy,f,0 c= Funcs X,(Y \ (f " {0 }))

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A16: z in Intersection Fy,f,0 ; :: thesis:
0 in rng f by A14, CARD_1:47, FUNCT_1:142;
then consider x1 being set such that
A17: x1 in dom f and
f . x1 = 0 and
A18: z in Fy . x1 by A16, Th24;
z in H₁(x1) by A8, A17, A18;
then consider g being Function of X,Y such that
A19: z = g and
not x1 in rng g ;
A20: rng g c= Y \ (f " {0 })

proof

let gy be set ; :: according to TARSKI:def 3 :: thesis:
assume A21: gy in rng g ; :: thesis:
assume not gy in Y \ (f " {0 }) ; :: thesis:
then A22: gy in f " {0 } by A21, XBOOLE_0:def 5;
then f . gy in {0 } by FUNCT_1:def 13;
then A23: f . gy = 0 by TARSKI:def 1;
gy in dom f by A22, FUNCT_1:def 13;
then g in Fy . gy by A16, A19, A23, Def2;
then g in H₁(gy) by A8, A21;
then ex h being Function of X,Y st
( g = h & not gy in rng h ) ;
hence contradiction by A21; :: thesis:

end;

dom g = X by A17, FUNCT_2:def 1;
hence z in Funcs X,(Y \ (f " {0 })) by A19, A20, FUNCT_2:def 2; :: thesis:

end;

then reconsider I = Intersection Fy,f,0 as finite set ;
A24: card (Y \ (f " {0 })) = (card Y) - (n + 1) by A14, CARD_2:63;
Funcs X,(Y \ (f " {0 })) c= Intersection Fy,f,0

proof

let g9 be set ; :: according to TARSKI:def 3 :: thesis:
assume g9 in Funcs X,(Y \ (f " {0 })) ; :: thesis:
then consider g being Function such that
A25: g9 = g and
A26: dom g = X and
A27: rng g c= Y \ (f " {0 }) by FUNCT_2:def 2;
reconsider gg = g as Function of X,Y by A26, A27, FUNCT_2:4, XBOOLE_1:1;
consider y being set such that
A28: y in f " {0 } by A14, CARD_1:47, XBOOLE_0:def 1;
not y in rng g by A27, A28, XBOOLE_0:def 5;
then A29: gg in H₁(y) ;
dom Fy = Y by FUNCT_2:def 1;
then A30: Fy9 . y in rng Fy9 by A28, FUNCT_1:def 5;
A31: for z being set st z in dom f & f . z = 0 holds
g in Fy . z

proof

let z be set ; :: thesis:
assume that
A32: z in dom f and
A33: f . z = 0 ; :: thesis:
f . z in {0 } by A33, TARSKI:def 1;
then z in f " {0 } by A32, FUNCT_1:def 13;
then A34: not z in rng gg by A27, XBOOLE_0:def 5;
Fy . z = H₁(z) by A8, A32;
hence g in Fy . z by A34; :: thesis:

end;

H₁(y) = Fy9 . y by A8, A28;
then g in union (rng Fy) by A30, A29, TARSKI:def 4;
hence g9 in Intersection Fy,f,0 by A25, A31, Def2; :: thesis:

end;

then A35: Funcs X,(Y \ (f " {0 })) = Intersection Fy,f,0 by A15, XBOOLE_0:def 10;

now

per cases ;

suppose Y \ (f " {0 }) = {} ; :: thesis:

then ( card I = 0 & (((card Y) - n) - 1) |^ (card X) = 0 ) by A1, A15, A24, CARD_1:47, NAT_1:14, NEWTON:16;
hence card (Intersection Fy,f9,0 ) = XF . n by A5, A10, A12, A13; :: thesis:

end;

suppose A36: Y \ (f " {0 }) <> {} ; :: thesis:

XF . n = (((card Y) - n) - 1) |^ (card X) by A5, A10, A12;
hence card (Intersection Fy,f9,0 ) = XF . n by A13, A35, A24, A36, Th4; :: thesis:

end;

hence card (Intersection Fy,f9,0 ) = XF . n ; :: thesis:

end;

( dom XF = card Y & dom Fy = Y ) by FUNCT_2:def 1;
then consider F being XFinSequence of such that
A37: dom F = card Y and
A38: card (union (rng Fy)) = Sum F and
A39: for n being Nat st n in dom F holds
F . n = (((- 1) |^ n) * (XF . n)) * ((card Y) choose (n + 1)) by A11, Th69;
take F ; :: thesis:
thus dom F = card Y by A37; :: thesis:
A40: card ((Funcs X,Y) \ u) = (card (Funcs X,Y)) - (card u) by A9, CARD_2:63;
A41: { f where f is Function of X,Y : f is onto } c= (Funcs X,Y) \ (union (rng Fy))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { f where f is Function of X,Y : f is onto } ; :: thesis:
then consider f being Function of X,Y such that
A42: x = f and
A43: f is onto ;
assume A44: not x in (Funcs X,Y) \ (union (rng Fy)) ; :: thesis:
f in Funcs X,Y by A2, FUNCT_2:11;
then f in union (rng Fy) by A42, A44, XBOOLE_0:def 5;
then consider Fyy being set such that
A45: f in Fyy and
A46: Fyy in rng Fy by TARSKI:def 4;
consider y being set such that
A47: y in dom Fy and
A48: Fy . y = Fyy by A46, FUNCT_1:def 5;
y in Y by A47, FUNCT_2:def 1;
then f in H₁(y) by A8, A45, A48;
then A49: ex g being Function of X,Y st
( f = g & not y in rng g ) ;
y in Y by A47, FUNCT_2:def 1;
hence contradiction by A43, A49, FUNCT_2:def 3; :: thesis:

end;

A50: (Funcs X,Y) \ (union (rng Fy)) c= { f where f is Function of X,Y : f is onto }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A51: x in (Funcs X,Y) \ (union (rng Fy)) ; :: thesis:
consider f being Function such that
A52: x = f and
A53: ( dom f = X & rng f c= Y ) by A51, FUNCT_2:def 2;
reconsider f = f as Function of X,Y by A53, FUNCT_2:4;
assume not x in { f where f is Function of X,Y : f is onto } ; :: thesis:
then not f is onto by A52;
then rng f <> Y by FUNCT_2:def 3;
then not Y c= rng f by XBOOLE_0:def 10;
then consider y being set such that
A54: y in Y and
A55: not y in rng f by TARSKI:def 3;
y in dom Fy9 by A54, FUNCT_2:def 1;
then Fy9 . y in rng Fy9 by FUNCT_1:def 5;
then A56: H₁(y) in rng Fy9 by A8, A54;
f in H₁(y) by A55;
then f in union (rng Fy) by A56, TARSKI:def 4;
hence contradiction by A51, A52, XBOOLE_0:def 5; :: thesis:

end;

card (Funcs X,Y) = (card Y) |^ (card X) by A2, Th4;
hence card { f where f is Function of X,Y : f is onto } = ((card Y) |^ (card X)) - (Sum F) by A38, A50, A41, A40, XBOOLE_0:def 10; :: thesis:
let n be Nat; :: thesis:
assume A57: n in dom F ; :: thesis:
A58: F . n = (((- 1) |^ n) * (XF . n)) * ((card Y) choose (n + 1)) by A39, A57;
XF . n = (((card Y) - n) - 1) |^ (card X) by A5, A37, A57;
hence F . n = (((- 1) |^ n) * ((card Y) choose (n + 1))) * ((((card Y) - n) - 1) |^ (card X)) by A58; :: thesis: