:: Cardinal Numbers and Finite Sets
:: by Karol P\c{a}k
::
:: Received May 24, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

theorem Th1: :: CARD_FIN:1
for X, Y being finite set st X c= Y & card X = card Y holds
X = Y
proofend;

theorem Th2: :: CARD_FIN:2
for X, Y being finite set
for x, y being set st ( Y = {} implies X = {} ) & not x in X holds
card (Funcs (X,Y)) = card  {  F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y )  }
proofend;

theorem Th3: :: CARD_FIN:3
for X, Y being finite set
for x, y being set st not x in X & y in Y holds
card (Funcs (X,Y)) = card  {  F where F is Function of (X \/ {x}),Y : F . x = y  }
proofend;

:: card Funcs(X,Y)
theorem Th4: :: CARD_FIN:4
for Y, X being finite set st ( Y = {} implies X = {} ) holds
card (Funcs (X,Y)) = (card Y) |^ (card X)
proofend;

theorem Th5: :: CARD_FIN:5
for X, Y being finite set
for x, y being set st ( Y is empty implies X is empty ) & not x in X & not y in Y holds
card  {  F where F is Function of X,Y : F is one-to-one  }  = card  {  F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y )  }
proofend;

theorem :: CARD_FIN:6
for n, k being Nat holds (n !) / ((n -' k) !) is Element of NAT
proofend;

:: one-to-one
theorem Th7: :: CARD_FIN:7
for X, Y being finite set st card X <= card Y holds
card  {  F where F is Function of X,Y : F is one-to-one  }  = ((card Y) !) / (((card Y) -' (card X)) !)
proofend;

:: Permutation of X
theorem Th8: :: CARD_FIN:8
for X being finite set holds card  {  F where F is Function of X,X : F is Permutation of X  }  = (card X) !
proofend;

definition
let X be finite set ;
let k be Nat;
let x1, x2 be set ;
func Choose (X,k,x1,x2) ->  Subset of (Funcs (X,{x1,x2})) means :Def1: :: CARD_FIN:def 1
 for x being set holds
( x in it iff ex f being Function of X,{x1,x2} st
( f = x &amp; card (f " {x1}) = k ) );
existence
 ex b1 being Subset of (Funcs (X,{x1,x2})) st
for x being set holds
( x in b1 iff ex f being Function of X,{x1,x2} st
( f = x &amp; card (f " {x1}) = k ) )
proofend;
uniqueness
 for b1, b2 being Subset of (Funcs (X,{x1,x2})) st ( for x being set holds
( x in b1 iff ex f being Function of X,{x1,x2} st
( f = x &amp; card (f " {x1}) = k ) ) ) &amp; ( for x being set holds
( x in b2 iff ex f being Function of X,{x1,x2} st
( f = x &amp; card (f " {x1}) = k ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Choose CARD_FIN:def_1_:_
 for X being finite set
for k being Nat
for x1, x2 being set
for b5 being Subset of (Funcs (X,{x1,x2})) holds
( b5 = Choose (X,k,x1,x2) iff for x being set holds
( x in b5 iff ex f being Function of X,{x1,x2} st
( f = x &amp; card (f " {x1}) = k ) ) );

theorem :: CARD_FIN:9
for x1 being set
for X being finite set
for k being Nat st card X <> k holds
Choose (X,k,x1,x1) is empty
proofend;

theorem Th10: :: CARD_FIN:10
for x1, x2 being set
for X being finite set
for k being Nat st card X < k holds
Choose (X,k,x1,x2) is empty
proofend;

theorem Th11: :: CARD_FIN:11
for x1, x2 being set
for X being finite set st x1 <> x2 holds
card (Choose (X,0,x1,x2)) = 1
proofend;

theorem Th12: :: CARD_FIN:12
for x1, x2 being set
for X being finite set holds card (Choose (X,(card X),x1,x2)) = 1
proofend;

theorem Th13: :: CARD_FIN:13
for z, x, y being set
for X being finite set
for k being Nat st not z in X holds
card (Choose (X,k,x,y)) = card  {  f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 &amp; f . z = x )  }
proofend;

theorem Th14: :: CARD_FIN:14
for z, x, y being set
for X being finite set
for k being Nat st not z in X &amp; x <> y holds
card (Choose (X,k,x,y)) = card  {  f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k &amp; f . z = y )  }
proofend;

Lm1:  for x, y, z being set
for X being finite set
for k being Nat st x <> y holds
(  {  f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 &amp; f . z = x )  }  \/  {  f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 &amp; f . z = y )  }  = Choose ((X \/ {z}),(k + 1),x,y) &amp;  {  f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 &amp; f . z = x )  }  misses  {  f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 &amp; f . z = y )  }  )
proofend;

theorem Th15: :: CARD_FIN:15
for x, y, z being set
for X being finite set
for k being Nat st x <> y &amp; not z in X holds
card (Choose ((X \/ {z}),(k + 1),x,y)) = (card (Choose (X,(k + 1),x,y))) + (card (Choose (X,k,x,y)))
proofend;

:: n choose k
:: [WP: ] Formula_for_the_Number_of_Combinations
theorem Th16: :: CARD_FIN:16
for x, y being set
for X being finite set
for k being Nat st x <> y holds
card (Choose (X,k,x,y)) = (card X) choose k
proofend;

theorem Th17: :: CARD_FIN:17
for x, y being set
for Y, X being finite set st x <> y holds
(Y --> y) +* (X --> x) in Choose ((X \/ Y),(card X),x,y)
proofend;

theorem Th18: :: CARD_FIN:18
for x, y being set
for X, Y being finite set st x <> y &amp; X misses Y holds
(X --> x) +* (Y --> y) in Choose ((X \/ Y),(card X),x,y)
proofend;

definition
let F, Ch be Function;
let y be set ;
func Intersection (F,Ch,y) ->  Subset of (union (rng F)) means :Def2: :: CARD_FIN:def 2
 for z being set holds
( z in it iff ( z in union (rng F) &amp; ( for x being set st x in dom Ch &amp; Ch . x = y holds
z in F . x ) ) );
existence
 ex b1 being Subset of (union (rng F)) st
for z being set holds
( z in b1 iff ( z in union (rng F) &amp; ( for x being set st x in dom Ch &amp; Ch . x = y holds
z in F . x ) ) )
proofend;
uniqueness
 for b1, b2 being Subset of (union (rng F)) st ( for z being set holds
( z in b1 iff ( z in union (rng F) &amp; ( for x being set st x in dom Ch &amp; Ch . x = y holds
z in F . x ) ) ) ) &amp; ( for z being set holds
( z in b2 iff ( z in union (rng F) &amp; ( for x being set st x in dom Ch &amp; Ch . x = y holds
z in F . x ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines Intersection CARD_FIN:def_2_:_
 for F, Ch being Function
for y being set
for b4 being Subset of (union (rng F)) holds
( b4 = Intersection (F,Ch,y) iff for z being set holds
( z in b4 iff ( z in union (rng F) &amp; ( for x being set st x in dom Ch &amp; Ch . x = y holds
z in F . x ) ) ) );

theorem Th19: :: CARD_FIN:19
for x, y being set
for F, Ch being Function st not (dom F) /\ (Ch " {x}) is empty holds
( y in Intersection (F,Ch,x) iff for z being set st z in dom Ch &amp; Ch . z = x holds
y in F . z )
proofend;

theorem Th20: :: CARD_FIN:20
for y being set
for F, Ch being Function st not Intersection (F,Ch,y) is empty holds
Ch " {y} c= dom F
proofend;

theorem :: CARD_FIN:21
for y being set
for F, Ch being Function st not Intersection (F,Ch,y) is empty holds
for x1, x2 being set st x1 in Ch " {y} &amp; x2 in Ch " {y} holds
F . x1 meets F . x2
proofend;

theorem Th22: :: CARD_FIN:22
for z, y being set
for F, Ch being Function st z in Intersection (F,Ch,y) &amp; y in rng Ch holds
ex x being set st
( x in dom Ch &amp; Ch . x = y &amp; z in F . x )
proofend;

theorem :: CARD_FIN:23
for y being set
for F, Ch being Function st ( F is empty or union (rng F) is empty ) holds
Intersection (F,Ch,y) = union (rng F) by RELAT_1:38, ZFMISC_1:2;

theorem Th24: :: CARD_FIN:24
for y being set
for F, Ch being Function st F | (Ch " {y}) = (Ch " {y}) --> (union (rng F)) holds
Intersection (F,Ch,y) = union (rng F)
proofend;

theorem :: CARD_FIN:25
for y being set
for F, Ch being Function st not union (rng F) is empty &amp; Intersection (F,Ch,y) = union (rng F) holds
F | (Ch " {y}) = (Ch " {y}) --> (union (rng F))
proofend;

theorem Th26: :: CARD_FIN:26
for y being set
for F being Function holds Intersection (F,{},y) = union (rng F)
proofend;

theorem Th27: :: CARD_FIN:27
for y, X9 being set
for F, Ch being Function holds Intersection (F,Ch,y) c= Intersection (F,(Ch | X9),y)
proofend;

theorem Th28: :: CARD_FIN:28
for y, X9 being set
for Ch, F being Function st Ch " {y} = (Ch | X9) " {y} holds
Intersection (F,Ch,y) = Intersection (F,(Ch | X9),y)
proofend;

theorem Th29: :: CARD_FIN:29
for X9, y being set
for F, Ch being Function holds Intersection ((F | X9),Ch,y) c= Intersection (F,Ch,y)
proofend;

theorem Th30: :: CARD_FIN:30
for y, X9 being set
for Ch, F being Function st y in rng Ch &amp; Ch " {y} c= X9 holds
Intersection ((F | X9),Ch,y) = Intersection (F,Ch,y)
proofend;

theorem Th31: :: CARD_FIN:31
for x, y being set
for Ch, F being Function st x in Ch " {y} holds
Intersection (F,Ch,y) c= F . x
proofend;

theorem Th32: :: CARD_FIN:32
for x, y being set
for Ch, F being Function st x in Ch " {y} holds
(Intersection (F,(Ch | ((dom Ch) \ {x})),y)) /\ (F . x) = Intersection (F,Ch,y)
proofend;

theorem Th33: :: CARD_FIN:33
for x1, x2 being set
for F, Ch1, Ch2 being Function st Ch1 " {x1} = Ch2 " {x2} holds
Intersection (F,Ch1,x1) = Intersection (F,Ch2,x2)
proofend;

theorem Th34: :: CARD_FIN:34
for y being set
for Ch, F being Function st Ch " {y} = {} holds
Intersection (F,Ch,y) = union (rng F)
proofend;

theorem Th35: :: CARD_FIN:35
for x, y being set
for Ch, F being Function st {x} = Ch " {y} holds
Intersection (F,Ch,y) = F . x
proofend;

theorem Th36: :: CARD_FIN:36
for x1, x2, y being set
for Ch, F being Function st {x1,x2} = Ch " {y} holds
Intersection (F,Ch,y) = (F . x1) /\ (F . x2)
proofend;

theorem :: CARD_FIN:37
for y, x being set
for F being Function st not F is empty holds
( y in Intersection (F,((dom F) --> x),x) iff for z being set st z in dom F holds
y in F . z )
proofend;

registration
let F be finite-yielding Function;
let X be set ;
clusterF | X ->  finite-yielding ;
coherence
 F | X is finite-yielding
proofend;
end;

registration
let F be finite-yielding Function;
let G be Function;
clusterG (#) F ->  finite-yielding ;
coherence
 F * G is finite-yielding
proofend;
cluster Intersect (F,G) ->  finite-yielding ;
coherence
 Intersect (F,G) is finite-yielding
proofend;
end;

theorem :: CARD_FIN:38
for y being set
for Ch being Function
for Fy being finite-yielding Function st y in rng Ch holds
Intersection (Fy,Ch,y) is finite
proofend;

theorem Th39: :: CARD_FIN:39
for Fy being finite-yielding Function st dom Fy is finite holds
union (rng Fy) is finite
proofend;

theorem :: CARD_FIN:40
for x being set
for n, k being Nat holds
( x in Choose (n,k,1,0) iff ex F being XFinSequence of st
( F = x &amp; dom F = n &amp; rng F c= {0,1} &amp; Sum F = k ) )
proofend;

Lm2:  for X being finite set ex P being Function of (card X),X st P is one-to-one
proofend;

definition
canceled;
let k be Nat;
let F be finite-yielding Function;
assume A1: dom F is finite ;
func Card_Intersection (F,k) ->  Element of NAT  means :Def4: :: CARD_FIN:def 4
 for x, y being set
for X being finite set
for P being Function of (card (Choose (X,k,x,y))),(Choose (X,k,x,y)) st dom F = X &amp; P is one-to-one &amp; x <> y holds
ex XFS being XFinSequence of st
( dom XFS = dom P &amp; ( for z being set
for f being Function st z in dom XFS &amp; f = P . z holds
XFS . z = card (Intersection (F,f,x)) ) &amp; it = Sum XFS );
existence
 ex b1 being Element of NAT st
for x, y being set
for X being finite set
for P being Function of (card (Choose (X,k,x,y))),(Choose (X,k,x,y)) st dom F = X &amp; P is one-to-one &amp; x <> y holds
ex XFS being XFinSequence of st
( dom XFS = dom P &amp; ( for z being set
for f being Function st z in dom XFS &amp; f = P . z holds
XFS . z = card (Intersection (F,f,x)) ) &amp; b1 = Sum XFS )
proofend;
uniqueness
 for b1, b2 being Element of NAT st ( for x, y being set
for X being finite set
for P being Function of (card (Choose (X,k,x,y))),(Choose (X,k,x,y)) st dom F = X &amp; P is one-to-one &amp; x <> y holds
ex XFS being XFinSequence of st
( dom XFS = dom P &amp; ( for z being set
for f being Function st z in dom XFS &amp; f = P . z holds
XFS . z = card (Intersection (F,f,x)) ) &amp; b1 = Sum XFS ) ) &amp; ( for x, y being set
for X being finite set
for P being Function of (card (Choose (X,k,x,y))),(Choose (X,k,x,y)) st dom F = X &amp; P is one-to-one &amp; x <> y holds
ex XFS being XFinSequence of st
( dom XFS = dom P &amp; ( for z being set
for f being Function st z in dom XFS &amp; f = P . z holds
XFS . z = card (Intersection (F,f,x)) ) &amp; b2 = Sum XFS ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  CARD_FIN:def_3_:_
canceled;

:: deftheorem Def4 defines Card_Intersection CARD_FIN:def_4_:_
 for k being Nat
for F being finite-yielding Function st dom F is finite holds
for b3 being Element of NAT holds
( b3 = Card_Intersection (F,k) iff for x, y being set
for X being finite set
for P being Function of (card (Choose (X,k,x,y))),(Choose (X,k,x,y)) st dom F = X &amp; P is one-to-one &amp; x <> y holds
ex XFS being XFinSequence of st
( dom XFS = dom P &amp; ( for z being set
for f being Function st z in dom XFS &amp; f = P . z holds
XFS . z = card (Intersection (F,f,x)) ) &amp; b3 = Sum XFS ) );

theorem :: CARD_FIN:41
for k being Nat
for Fy being finite-yielding Function
for x, y being set
for X being finite set
for P being Function of (card (Choose (X,k,x,y))),(Choose (X,k,x,y)) st dom Fy = X &amp; P is one-to-one &amp; x <> y holds
for XFS being XFinSequence of st dom XFS = dom P &amp; ( for z being set
for f being Function st z in dom XFS &amp; f = P . z holds
XFS . z = card (Intersection (Fy,f,x)) ) holds
Card_Intersection (Fy,k) = Sum XFS
proofend;

theorem :: CARD_FIN:42
for k being Nat
for Fy being finite-yielding Function st dom Fy is finite &amp; k = 0 holds
Card_Intersection (Fy,k) = card (union (rng Fy))
proofend;

theorem Th43: :: CARD_FIN:43
for X being finite set
for k being Nat
for Fy being finite-yielding Function st dom Fy = X &amp; k > card X holds
Card_Intersection (Fy,k) = 0
proofend;

theorem Th44: :: CARD_FIN:44
for Fy being finite-yielding Function
for X being finite set st dom Fy = X holds
for P being Function of (card X),X st P is one-to-one holds
ex XFS being XFinSequence of st
( dom XFS = card X &amp; ( for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) ) &amp; Card_Intersection (Fy,1) = Sum XFS )
proofend;

theorem Th45: :: CARD_FIN:45
for x being set
for X being finite set
for Fy being finite-yielding Function st dom Fy = X holds
Card_Intersection (Fy,(card X)) = card (Intersection (Fy,(X --> x),x))
proofend;

theorem Th46: :: CARD_FIN:46
for x being set
for X being finite set
for Fy being finite-yielding Function st Fy = x .--> X holds
Card_Intersection (Fy,1) = card X
proofend;

theorem :: CARD_FIN:47
for x, y being set
for X, Y being finite set
for Fy being finite-yielding Function st x <> y &amp; Fy = (x,y) --> (X,Y) holds
( Card_Intersection (Fy,1) = (card X) + (card Y) &amp; Card_Intersection (Fy,2) = card (X /\ Y) )
proofend;

theorem Th48: :: CARD_FIN:48
for Fy being finite-yielding Function
for x being set st dom Fy is finite &amp; x in dom Fy holds
Card_Intersection (Fy,1) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),1)) + (card (Fy . x))
proofend;

theorem Th49: :: CARD_FIN:49
for X9 being set
for F being Function holds
( dom (Intersect (F,((dom F) --> X9))) = dom F &amp; ( for x being set st x in dom F holds
(Intersect (F,((dom F) --> X9))) . x = (F . x) /\ X9 ) )
proofend;

theorem Th50: :: CARD_FIN:50
for X9 being set
for F being Function holds (union (rng F)) /\ X9 = union (rng (Intersect (F,((dom F) --> X9))))
proofend;

theorem Th51: :: CARD_FIN:51
for y, X9 being set
for F, Ch being Function holds (Intersection (F,Ch,y)) /\ X9 = Intersection ((Intersect (F,((dom F) --> X9))),Ch,y)
proofend;

theorem Th52: :: CARD_FIN:52
for F, G being XFinSequence st F is one-to-one &amp; G is one-to-one &amp; rng F misses rng G holds
F ^ G is one-to-one
proofend;

theorem Th53: :: CARD_FIN:53
for k being Nat
for Fy being finite-yielding Function
for X being finite set
for x being set
for n being Nat st dom Fy = X &amp; x in dom Fy &amp; k > 0 holds
Card_Intersection (Fy,(k + 1)) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),(k + 1))) + (Card_Intersection ((Intersect ((Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x)))),k))
proofend;

theorem Th54: :: CARD_FIN:54
for x being set
for F being Function st x in dom F holds
union (rng F) = (union (rng (F | ((dom F) \ {x})))) \/ (F . x)
proofend;

theorem Th55: :: CARD_FIN:55
for Fy being finite-yielding Function
for X being finite set ex XFS being XFinSequence of st
( dom XFS = card X &amp; ( for n being Nat st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection (Fy,(n + 1))) ) )
proofend;

:: The principle of inclusions and the disconnections
:: [WP: ] Principle_of_Inclusion/Exclusion
theorem Th56: :: CARD_FIN:56
for Fy being finite-yielding Function
for X being finite set st dom Fy = X holds
for XFS being XFinSequence of st dom XFS = card X &amp; ( for n being Nat st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection (Fy,(n + 1))) ) holds
card (union (rng Fy)) = Sum XFS
proofend;

theorem Th57: :: CARD_FIN:57
for Fy being finite-yielding Function
for X being finite set
for n, k being Nat st dom Fy = X &amp; ex x, y being set st
( x <> y &amp; ( for f being Function st f in Choose (X,k,x,y) holds
card (Intersection (Fy,f,x)) = n ) ) holds
Card_Intersection (Fy,k) = n * ((card X) choose k)
proofend;

theorem Th58: :: CARD_FIN:58
for Fy being finite-yielding Function
for X being finite set st dom Fy = X holds
for XF being XFinSequence of st dom XF = card X &amp; ( for n being Nat st n in dom XF holds
ex x, y being set st
( x <> y &amp; ( for f being Function st f in Choose (X,(n + 1),x,y) holds
card (Intersection (Fy,f,x)) = XF . n ) ) ) holds
ex F being XFinSequence of st
( dom F = card X &amp; card (union (rng Fy)) = Sum F &amp; ( for n being Nat st n in dom F holds
F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) )
proofend;

Lm3:  for X, Y being finite set st not X is empty &amp; not Y is empty holds
ex F being XFinSequence of st
( dom F = card Y &amp; ((card Y) |^ (card X)) - (Sum F) = card  {  f where f is Function of X,Y : f is onto  }  &amp; ( for n being Nat st n in dom F holds
F . n = (((- 1) |^ n) * ((card Y) choose (n + 1))) * ((((card Y) - n) - 1) |^ (card X)) ) )
proofend;

:: onto
theorem Th59: :: CARD_FIN:59
for X, Y being finite set st not X is empty &amp; not Y is empty holds
ex F being XFinSequence of st
( dom F = (card Y) + 1 &amp; Sum F = card  {  f where f is Function of X,Y : f is onto  }  &amp; ( for n being Nat st n in dom F holds
F . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X)) ) )
proofend;

:: n block k
theorem :: CARD_FIN:60
for n, k being Nat st k <= n holds
ex F being XFinSequence of st
( n block k = (1 / (k !)) * (Sum F) &amp; dom F = k + 1 &amp; ( for m being Nat st m in dom F holds
F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n) ) )
proofend;

theorem Th61: :: CARD_FIN:61
for X1, Y1, X being finite set st ( Y1 is empty implies X1 is empty ) &amp; X c= X1 holds
for F being Function of X1,Y1 st F is one-to-one &amp; card X1 = card Y1 holds
((card X1) -' (card X)) ! = card  {  f where f is Function of X1,Y1 : ( f is one-to-one &amp; rng (f | (X1 \ X)) c= F .: (X1 \ X) &amp; ( for x being set st x in X holds
f . x = F . x ) )  }
proofend;

Lm4:  for X, Y being finite set
for F being Function of X,Y st dom F = X &amp; F is one-to-one holds
ex XF being XFinSequence of st
( dom XF = card X &amp; ((card X) !) - (Sum XF) = card  {  h where h is Function of X,(rng F) : ( h is one-to-one &amp; ( for x being set st x in X holds
h . x <> F . x ) )  }  &amp; ( for n being Nat st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) !)) / ((n + 1) !) ) )
proofend;

theorem Th62: :: CARD_FIN:62
for X being finite set
for F being Function st dom F = X &amp; F is one-to-one holds
ex XF being XFinSequence of st
( Sum XF = card  {  h where h is Function of X,(rng F) : ( h is one-to-one &amp; ( for x being set st x in X holds
h . x <> F . x ) )  }  &amp; dom XF = (card X) + 1 &amp; ( for n being Nat st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) !)) / (n !) ) )
proofend;

:: disorders
theorem :: CARD_FIN:63
for X being finite set ex XF being XFinSequence of st
( Sum XF = card  {  h where h is Function of X,X : ( h is one-to-one &amp; ( for x being set st x in X holds
h . x <> x ) )  }  &amp; dom XF = (card X) + 1 &amp; ( for n being Nat st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) !)) / (n !) ) )
proofend;