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

proof

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

proof

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

end;

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

end;

consider Fy' being Function of X,(bool (Funcs X,(rng F))) such that
A5: for x being set st x in X 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:

now

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;

hence Fy' . y is finite ; :: thesis:

end;

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

proof

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

end;

consider XF being Function of (card X),NAT such that
A8: for x being set st x in card X holds
S₁[x,XF . x] from FUNCT_2:sch 1(A6);
A9: ( dom XF = card X & 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 ;
reconsider rngF = rng F as finite set ;
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 X,(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 X,(n + 1),0 ,1 ; :: thesis:
consider f being Function of X,{0 ,1} such that
A13: ( f = f' & card (f " {0 }) = n + 1 ) by A12, 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 ) ) } ;
A14: 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 set such that
A15: ( z in Intersection Fy,f,0 & 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 ) ) } ) by TARSKI:def 3;
consider x' being set such that
A16: x' in f " {0 } by A13, CARD_1:47, XBOOLE_0:def 1;
f . x' in {0 } by A16, FUNCT_1:def 13;
then ( f . x' = 0 & x' in dom f ) by A16, FUNCT_1:def 13, TARSKI:def 1;
then 0 in rng f by FUNCT_1:def 5;
then consider x being set such that
A17: ( x in dom f & f . x = 0 & z in Fy . x ) by A15, Th24;
z in H₁(x) by A5, A17;
then consider h being Function of X,(rng F) such that
A18: ( z = h & h is one-to-one & h . x = F . x ) ;
A19: for x1 being set st x1 in f0 holds
h . x1 = F . x1

proof

let x1 be set ; :: thesis:
assume A20: x1 in f0 ; :: thesis:
( Fy' . x1 = H₁(x1) & x1 in dom f & f . x1 in {0 } ) by A5, A20, FUNCT_1:def 13;
then ( Fy' . x1 = H₁(x1) & x1 in dom f & f . x1 = 0 ) by TARSKI:def 1;
then h in H₁(x1) by A15, A18, Def2;
then ex h' being Function of X,(rng F) st
( h = h' & h' is one-to-one & h' . 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 set such that
A21: ( y in rng (h | (X \ f0)) & not y in F .: (X \ f0) ) by TARSKI:def 3;
consider x1 being set such that
A22: ( x1 in dom (h | (X \ f0)) & (h | (X \ f0)) . x1 = y ) by A21, FUNCT_1:def 5;
( y in rngF & rngF = F .: X ) by A1, A21, RELAT_1:146;
then ( y in (F .: X) \ (F .: (X \ f0)) & F .: (X \ (X \ f0)) = (F .: X) \ (F .: (X \ f0)) ) by A1, A21, FUNCT_1:123, XBOOLE_0:def 5;
then consider x2 being set such that
A23: ( x2 in dom F & x2 in X \ (X \ f0) & y = F . x2 ) by FUNCT_1:def 12;
X \ (X \ f0) = X /\ (f " {0 }) by XBOOLE_1:48;
then ( x2 in f " {0 } & x1 in (dom h) /\ (X \ f0) & y in rng F ) by A22, A23, FUNCT_1:def 5, RELAT_1:90, XBOOLE_0:def 4;
then ( h . x2 = y & x1 in dom h & h . x1 = y & X = dom h & x1 in X \ f0 & not x2 in X \ f0 ) by A19, A22, A23, FUNCT_1:70, FUNCT_2:def 1, XBOOLE_0:def 4, XBOOLE_0:def 5;
hence contradiction by A18, A23, FUNCT_1:def 8; :: thesis:

end;

hence contradiction by A15, A18, A19; :: thesis:

end;

A24: { 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 set such that
A25: ( 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 ) ) } & not z in Intersection Fy,f,0 ) by TARSKI:def 3;
consider h being Function of X,(rng F) such that
A26: ( h = z & h is one-to-one & rng (h | (X \ f0)) c= F .: (X \ f0) ) and
A27: for x being set st x in f0 holds
h . x = F . x by A25;
consider x being set such that
A28: x in f " {0 } by A13, CARD_1:47, XBOOLE_0:def 1;
x in X by A28;
then ( x in dom Fy' & X \ (X \ f0) = X /\ (f " {0 }) & x in X /\ (f " {0 }) ) by A28, FUNCT_2:def 1, XBOOLE_0:def 4, XBOOLE_1:48;
then ( Fy' . x = H₁(x) & Fy' . x in rng Fy' & h . x = F . x & h is one-to-one ) by A5, A26, A27, A28, FUNCT_1:def 5;
then ( h in Fy' . x & Fy' . x in rng Fy' ) ;
then h in union (rng Fy') by TARSKI:def 4;
then consider y being set such that
A29: ( y in dom f & f . y = 0 & not h in Fy . y ) by A25, A26, Def2;
f . y in {0 } by A29, TARSKI:def 1;
then y in f " {0 } by A29, FUNCT_1:def 13;
then ( h . y = F . y & h is one-to-one ) by A26, A27;
then ( h in H₁(y) & Fy' . y = H₁(y) ) by A5, A29;
hence contradiction by A29; :: thesis:

end;

n < card X by A9, A11, NAT_1:45;
then A30: n + 1 <= card X by NAT_1:13;
then reconsider c = (card X) - (n + 1) as Element of NAT by NAT_1:21;
X,rngF are_equipotent by A1, WELLORD2:def 4;
then ( card rngF = card X & X \ (X \ f0) = X /\ (f " {0 }) ) by CARD_1:21, XBOOLE_1:48;
then ( ( rngF = {} implies X is empty ) & F is Function of X,rngF & { 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 & card rngF = card X & F is one-to-one ) by A1, A14, A24, FUNCT_2:3, XBOOLE_0:def 10;
then ( card (Intersection Fy,f,0 ) = ((card X) -' (n + 1)) ! & (card X) -' (n + 1) = c & XF . n = c ! ) by A8, A9, A11, A13, A30, Th72, XREAL_1:235;
hence card (Intersection Fy,f',0 ) = XF . n by A13; :: thesis:

end;

( dom XF = card X & dom Fy = X ) by FUNCT_2:def 1;
then consider F' being XFinSequence of such that
A31: dom F' = card X and
A32: card (union (rng Fy)) = Sum F' and
A33: for n being Element of NAT st n in dom F' holds
F' . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) by A10, Th69;
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 ) ) } ;
A34: X,rngF are_equipotent by A1, WELLORD2:def 4;
then A35: card rngF = card X by CARD_1:21;
then ((card rngF) -' (card X)) ! = 1 by NEWTON:18, XREAL_1:234;
then A36: ( card { f where f is Function of X,rngF : f is one-to-one } = ((card rngF) ! ) / (((card rngF) -' (card X)) ! ) & ((card rngF) ! ) / (((card rngF) -' (card X)) ! ) = (card rngF) ! ) by A35, Th7;
then reconsider One = { f where f is Function of X,(rng F) : f is one-to-one } as finite set ;
A37: 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 set ; :: according to TARSKI:def 3 :: thesis:
assume A38: x in One \ (union (rng Fy)) ; :: thesis:
x in One by A38;
then consider f being Function of X,(rng F) such that
A39: ( f = x & 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
A40: ( x in X & f . x = F . x ) by A39;
x in dom Fy by A40, FUNCT_2:def 1;
then Fy . x in rng Fy by FUNCT_1:def 5;
then ( H₁(x) in rng Fy & f in H₁(x) ) by A5, A39, A40;
then f in union (rng Fy) by TARSKI:def 4;
hence contradiction by A38, A39, XBOOLE_0:def 5; :: thesis:

end;

A41: { 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 set ; :: according to TARSKI:def 3 :: thesis:
assume A42: 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:
consider f being Function of X,(rng F) such that
A43: ( x = f & f is one-to-one ) and
A44: for x being set st x in X holds
f . x <> F . x by A42;
assume A45: not x in One \ (union (rng Fy)) ; :: thesis:
f in One by A43;
then f in union (rng Fy) by A43, A45, XBOOLE_0:def 5;
then consider Fyy being set such that
A46: ( f in Fyy & Fyy in rng Fy ) by TARSKI:def 4;
consider y being set such that
A47: ( y in dom Fy & Fy . y = Fyy ) by A46, FUNCT_1:def 5;
y in X by A47, FUNCT_2:def 1;
then f in H₁(y) by A5, A46, A47;
then ( y in X & ex g being Function of X,(rng F) st
( f = g & g is one-to-one & g . y = F . y ) ) by A47, FUNCT_2:def 1;
hence contradiction by A44; :: thesis:

end;

A48: union (rng Fy') c= One

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A49: x in union (rng Fy') ; :: thesis:
consider Fyx being set such that
A50: ( x in Fyx & Fyx in rng Fy' ) by A49, TARSKI:def 4;
consider x1 being set such that
A51: ( x1 in dom Fy' & Fy . x1 = Fyx ) by A50, FUNCT_1:def 5;
x in H₁(x1) by A5, A50, A51;
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;

then reconsider u = union (rng Fy) as finite set ;
take F' ; :: thesis:
thus dom F' = card X by A31; :: thesis:
( card (One \ u) = (card One) - (card u) & card One = (card X) ! & One \ u = { 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 ) ) } ) by A34, A36, A37, A41, A48, CARD_1:21, CARD_2:63, XBOOLE_0:def 10;
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 F') by A32; :: thesis:
let n be Element of NAT ; :: thesis:
assume A52: n in dom F' ; :: thesis:
n < card X by A31, A52, NAT_1:45;
then A53: n + 1 <= card X by NAT_1:13;
then reconsider c = (card X) - (n + 1) as Element of NAT by NAT_1:21;
A54: c ! > 0 by NEWTON:23;
( XF . n = c ! & (card X) choose (n + 1) = ((card X) ! ) / ((c ! ) * ((n + 1) ! )) ) by A8, A31, A52, A53, NEWTON:def 3;
then A55: (XF . n) * ((card X) choose (n + 1)) = ((c ! ) * ((card X) ! )) / ((c ! ) * ((n + 1) ! )) by XCMPLX_1:75
.= ((card X) ! ) * ((c ! ) / ((c ! ) * ((n + 1) ! ))) by XCMPLX_1:75
.= ((card X) ! ) * (((c ! ) / (c ! )) / ((n + 1) ! )) by XCMPLX_1:79
.= ((card X) ! ) * (1 / ((n + 1) ! )) by A54, XCMPLX_1:60
.= (((card X) ! ) * 1) / ((n + 1) ! ) by XCMPLX_1:75 ;
F' . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) by A33, A52
.= ((- 1) |^ n) * (((card X) ! ) / ((n + 1) ! )) by A55 ;
hence F' . n = (((- 1) |^ n) * ((card X) ! )) / ((n + 1) ! ) by XCMPLX_1:75; :: thesis: