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

proof

let x be object ; :: thesis:
assume A4: x in Segm (card Y) ; :: thesis:
reconsider n = x as Element of NAT by A4;
n < card Y by A4, NAT_1:44;
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 object st
( y in NAT & S₁[x,y] ) ; :: thesis:

end;

consider XF being Function of (Segm (card Y)),NAT such that
A5: for x being object st x in Segm (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₁( object ) -> set = { f where f is Function of X,Y : not $1 in rng f } ;
A6: for x being object st x in Y holds
H₁(x) in bool (Funcs (X,Y))

proof

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

proof

let y be object ; :: 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:8; :: 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 object st x in Y holds
Fy9 . x = H₁(x) from FUNCT_2:sch 2(A6);
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;
union (rng Fy9) c= union (bool (Funcs (X,Y))) by ZFMISC_1:77;
then A9: union (rng Fy) c= Funcs (X,Y) by ZFMISC_1:81;
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: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 (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 object ; :: according to TARSKI:def 3 :: thesis:
assume A16: z in Intersection (Fy,f,0) ; :: thesis:
0 in rng f by A14, CARD_1:27, FUNCT_1:72;
then consider x1 being set such that
A17: x1 in dom f and
f . x1 = 0 and
A18: z in Fy . x1 by A16, Th21;
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 object ; :: 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 7;
then A23: f . gy = 0 by TARSKI:def 1;
gy in dom f by A22, FUNCT_1:def 7;
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;

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

proof

let g9 be object ; :: 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:2, XBOOLE_1:1;
consider y being object such that
A28: y in f " {0} by A14, CARD_1:27, 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 3;
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 7;
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;

now :: thesis:

per cases ;

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

then ( card I = 0 & (((card Y) - n) - 1) |^ (card X) = 0 ) by A1, A15, A24, NAT_1:14, NEWTON:11;
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, Th3; :: 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 INT 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, Th57;
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:44;
A41: { f where f is Function of X,Y : f is onto } c= (Funcs (X,Y)) \ (union (rng Fy))

proof

let x be object ; :: 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:8;
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 object such that
A47: y in dom Fy and
A48: Fy . y = Fyy by A46, FUNCT_1:def 3;
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 object ; :: 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:2;
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 ;
then consider y being object such that
A54: y in Y and
A55: not y in rng f ;
y in dom Fy9 by A54, FUNCT_2:def 1;
then Fy9 . y in rng Fy9 by FUNCT_1:def 3;
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, Th3;
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: