let X, Y be finite set ; :: thesis:
assume A1: ( not X is empty & not Y is empty ) ; :: thesis:
deffunc H₁( set ) -> set = { f where f is Function of X,Y : not $1 in rng f } ;
A2: for x being set st x in Y holds
H₁(x) in bool (Funcs X,Y)

proof

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

proof

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

end;

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

end;

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

proof

let y be set ; :: thesis:

per cases ;

suppose y in dom Fy' ; :: thesis:

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

end;

suppose not y in dom Fy' ; :: thesis:

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

end;

then reconsider Fy = Fy' as finite-yielding Function by Def3;
defpred S₁[ set , set ] means for n being Element of NAT st n = $1 holds
$2 = (((card Y) - n) - 1) |^ (card X);
A6: for x being set st x in card Y holds
ex y being set st
( y in NAT & S₁[x,y] )

proof

let x be set ; :: thesis:
assume A7: x in card Y ; :: thesis:
card Y is Subset of NAT by STIRL2_1:8;
then reconsider n = x as Element of NAT by A7;
n < card Y by A7, 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)] & k |^ (card X) is Element of NAT ) ;
hence ex y being set st
( y in NAT & S₁[x,y] ) ; :: thesis:

end;

consider XF being Function of (card Y),NAT such that
A8: for x being set st x in card Y holds
S₁[x,XF . x] from FUNCT_2:sch 1(A6);
A9: ( dom XF = card Y & rng XF c= NAT ) by FUNCT_2:def 1;
then reconsider XF = XF as XFinSequence by AFINSQ_1:7;
reconsider XF = XF as XFinSequence of ;
A10: for n being Element of 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 Element of NAT ; :: thesis:
assume A11: n in dom XF ; :: thesis:
take 0 ; :: thesis:
take 1 ; :: thesis:
thus 0 <> 1 ; :: thesis:
let f' be Function; :: thesis:
assume A12: f' in Choose Y,(n + 1),0 ,1 ; :: thesis:
consider f being Function of Y,{0 ,1} such that
A13: ( f = f' & card (f " {0 }) = n + 1 ) by A12, Def1;
A14: Intersection Fy,f,0 c= Funcs X,(Y \ (f " {0 }))

proof

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

proof

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

end;

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

end;

A20: Funcs X,(Y \ (f " {0 })) c= Intersection Fy,f,0

proof

let g' be set ; :: according to TARSKI:def 3 :: thesis:
assume A21: g' in Funcs X,(Y \ (f " {0 })) ; :: thesis:
consider g being Function such that
A22: ( g' = g & dom g = X & rng g c= Y \ (f " {0 }) ) by A21, FUNCT_2:def 2;
consider y being set such that
A23: y in f " {0 } by A13, CARD_1:47, XBOOLE_0:def 1;
( y in dom f & dom Fy = Y & dom f = Y ) by A23, FUNCT_1:def 13, FUNCT_2:def 1;
then A24: ( H₁(y) = Fy' . y & Fy' . y in rng Fy' ) by A5, FUNCT_1:def 5;
reconsider gg = g as Function of X,Y by A22, FUNCT_2:4, XBOOLE_1:1;
not y in rng g by A22, A23, XBOOLE_0:def 5;
then gg in H₁(y) ;
then A25: g in union (rng Fy) by A24, TARSKI:def 4;
for z being set st z in dom f & f . z = 0 holds
g in Fy . z

proof

let z be set ; :: thesis:
assume A26: ( z in dom f & f . z = 0 ) ; :: thesis:
f . z in {0 } by A26, TARSKI:def 1;
then ( dom f = Y & z in f " {0 } ) by A26, FUNCT_1:def 13, FUNCT_2:def 1;
then ( Fy . z = H₁(z) & not z in rng gg ) by A5, A22, XBOOLE_0:def 5;
hence g in Fy . z ; :: thesis:

end;

hence g' in Intersection Fy,f,0 by A22, A25, Def2; :: thesis:

end;

reconsider I = Intersection Fy,f,0 as finite set by A14;
A27: Funcs X,(Y \ (f " {0 })) = Intersection Fy,f,0 by A14, A20, XBOOLE_0:def 10;
card X <> 0 by A1;
then A28: ( card X >= 1 & card (Y \ (f " {0 })) = (card Y) - (n + 1) ) by A13, CARD_2:63, NAT_1:14;

now

per cases ;

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

then ( card I = 0 & (((card Y) - n) - 1) |^ (card X) = 0 ) by A1, A27, A28, CARD_1:47, NEWTON:16;
hence card (Intersection Fy,f',0 ) = XF . n by A8, A9, A11, A13; :: thesis:

end;

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

then ( XF . n = (((card Y) - n) - 1) |^ (card X) & (card (Y \ (f " {0 }))) |^ (card X) = card I ) by A8, A9, A11, A27, Th4;
hence card (Intersection Fy,f',0 ) = XF . n by A13, A28; :: thesis:

end;

hence card (Intersection Fy,f',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
A29: dom F = card Y and
A30: card (union (rng Fy)) = Sum F and
A31: for n being Element of NAT st n in dom F holds
F . n = (((- 1) |^ n) * (XF . n)) * ((card Y) choose (n + 1)) by A10, Th69;
set Onto = { f where f is Function of X,Y : f is onto } ;
A32: (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 A33: x in (Funcs X,Y) \ (union (rng Fy)) ; :: thesis:
consider f being Function such that
A34: ( x = f & dom f = X & rng f c= Y ) by A33, FUNCT_2:def 2;
reconsider f = f as Function of X,Y by A34, 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 A34;
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
A35: ( y in Y & not y in rng f ) by TARSKI:def 3;
y in dom Fy' by A35, FUNCT_2:def 1;
then Fy' . y in rng Fy' by FUNCT_1:def 5;
then ( H₁(y) in rng Fy' & f in H₁(y) ) by A5, A35;
then f in union (rng Fy) by TARSKI:def 4;
hence contradiction by A33, A34, XBOOLE_0:def 5; :: thesis:

end;

A36: { 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 A37: x in { f where f is Function of X,Y : f is onto } ; :: thesis:
consider f being Function of X,Y such that
A38: ( x = f & f is onto ) by A37;
assume A39: not x in (Funcs X,Y) \ (union (rng Fy)) ; :: thesis:
f in Funcs X,Y by A1, FUNCT_2:11;
then f in union (rng Fy) by A38, A39, XBOOLE_0:def 5;
then consider Fyy being set such that
A40: ( f in Fyy & Fyy in rng Fy ) by TARSKI:def 4;
consider y being set such that
A41: ( y in dom Fy & Fy . y = Fyy ) by A40, FUNCT_1:def 5;
y in Y by A41, FUNCT_2:def 1;
then f in H₁(y) by A5, A40, A41;
then ( y in Y & ex g being Function of X,Y st
( f = g & not y in rng g ) ) by A41, FUNCT_2:def 1;
hence contradiction by A38, FUNCT_2:def 3; :: thesis:

end;

union (rng Fy') c= union (bool (Funcs X,Y)) by ZFMISC_1:95;
then A42: union (rng Fy) c= Funcs X,Y by ZFMISC_1:99;
then reconsider u = union (rng Fy) as finite set ;
take F ; :: thesis:
thus dom F = card Y by A29; :: thesis:
( card ((Funcs X,Y) \ u) = (card (Funcs X,Y)) - (card u) & card (Funcs X,Y) = (card Y) |^ (card X) & (Funcs X,Y) \ u = { f where f is Function of X,Y : f is onto } ) by A1, A32, A36, A42, Th4, CARD_2:63, XBOOLE_0:def 10;
hence card { f where f is Function of X,Y : f is onto } = ((card Y) |^ (card X)) - (Sum F) by A30; :: thesis:
let n be Element of NAT ; :: thesis:
assume A43: n in dom F ; :: thesis:
( F . n = (((- 1) |^ n) * (XF . n)) * ((card Y) choose (n + 1)) & XF . n = (((card Y) - n) - 1) |^ (card X) ) by A8, A29, A31, A43;
hence F . n = (((- 1) |^ n) * ((card Y) choose (n + 1))) * ((((card Y) - n) - 1) |^ (card X)) ; :: thesis: