:: CARD_FIN semantic presentation

Lemma1: for b₁, b₂ being set st b₁ in b₂ holds
(b₂ \ {b₁}) \/ {b₁} = b₂
by ZFMISC_1:140;

Lemma2: for b₁, b₂ being set st not b₁ in b₂ holds
(b₂ \/ {b₁}) \ {b₁} = b₂
by ZFMISC_1:141;

theorem Th1: :: CARD_FIN:1

for b₁, b₂ being finite set st b₁ c= b₂ & card b₁ = card b₂ holds
b₁ = b₂

proof end;

theorem Th2: :: CARD_FIN:2

for b₁, b₂ being finite set
for b₃, b₄ being set st ( b₂ = {} implies b₁ = {} ) & not b₃ in b₁ holds
card (Funcs b₁,b₂) = Card { b₅ where B is Function of b₁ \/ {b₃},b₂ \/ {b₄} : ( rng (b₅ | b₁) c= b₂ & b₅ . b₃ = b₄ ) }

proof end;

theorem Th3: :: CARD_FIN:3

for b₁, b₂ being finite set
for b₃, b₄ being set st not b₃ in b₁ & b₄ in b₂ holds
card (Funcs b₁,b₂) = Card { b₅ where B is Function of b₁ \/ {b₃},b₂ : b₅ . b₃ = b₄ }

proof end;

theorem Th4: :: CARD_FIN:4

for b₁, b₂ being finite set st ( b₁ = {} implies b₂ = {} ) holds
card (Funcs b₂,b₁) = (card b₁) |^ (card b₂)

proof end;

theorem Th5: :: CARD_FIN:5

for b₁, b₂ being finite set
for b₃, b₄ being set st ( b₂ is empty implies b₁ is empty ) & not b₃ in b₁ & not b₄ in b₂ holds
Card { b₅ where B is Function of b₁,b₂ : b₅ is one-to-one } = Card { b₅ where B is Function of b₁ \/ {b₃},b₂ \/ {b₄} : ( b₅ is one-to-one & b₅ . b₃ = b₄ ) }

proof end;

theorem Th6: :: CARD_FIN:6

for b₁, b₂ being Nat holds (b₁ ! ) / ((b₁ -' b₂) ! ) is Nat

proof end;

theorem Th7: :: CARD_FIN:7

for b₁, b₂ being finite set st card b₁ <= card b₂ holds
Card { b₃ where B is Function of b₁,b₂ : b₃ is one-to-one } = ((card b₂) ! ) / (((card b₂) -' (card b₁)) ! )

proof end;

theorem Th8: :: CARD_FIN:8

for b₁ being finite set holds Card { b₂ where B is Function of b₁,b₁ : b₂ is Permutation of b₁ } = (card b₁) !

proof end;

definition

let c₁ be finite set ;
let c₂ be Nat;
let c₃, c₄ be set ;
func Choose c₁,c₂,c₃,c₄ -> Subset of (Funcs a₁,{a₃,a₄}) means :Def1: :: CARD_FIN:def 1
for b₁ being set holds
( b₁ in a₅ iff ex b₂ being Function of a₁,{a₃,a₄} st
( b₂ = b₁ & Card (b₂ " {a₃}) = a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Choose CARD_FIN:def 1 :

theorem Th9: :: CARD_FIN:9

for b₁ being set
for b₂ being finite set
for b₃ being Nat st card b₂ <> b₃ holds
Choose b₂,b₃,b₁,b₁ is empty

proof end;

theorem Th10: :: CARD_FIN:10

for b₁, b₂ being set
for b₃ being finite set
for b₄ being Nat st card b₃ < b₄ holds
Choose b₃,b₄,b₁,b₂ is empty

proof end;

theorem Th11: :: CARD_FIN:11

for b₁, b₂ being set
for b₃ being finite set st b₁ <> b₂ holds
card (Choose b₃,0,b₁,b₂) = 1

proof end;

theorem Th12: :: CARD_FIN:12

for b₁, b₂ being set
for b₃ being finite set holds card (Choose b₃,(card b₃),b₁,b₂) = 1

proof end;

theorem Th13: :: CARD_FIN:13

for b₁, b₂ being set
for b₃ being Function st b₃ . b₁ = b₂ & b₁ in dom b₃ holds
{b₁} \/ ((b₃ | ((dom b₃) \ {b₁})) " {b₂}) = b₃ " {b₂}

proof end;

theorem Th14: :: CARD_FIN:14

for b₁, b₂, b₃ being set
for b₄ being finite set
for b₅ being Nat st not b₁ in b₄ holds
card (Choose b₄,b₅,b₂,b₃) = Card { b₆ where B is Function of b₄ \/ {b₁},{b₂,b₃} : ( Card (b₆ " {b₂}) = b₅ + 1 & b₆ . b₁ = b₂ ) }

proof end;

theorem Th15: :: CARD_FIN:15

for b₁, b₂ being set
for b₃ being Function st b₃ . b₁ <> b₂ holds
(b₃ | ((dom b₃) \ {b₁})) " {b₂} = b₃ " {b₂}

proof end;

theorem Th16: :: CARD_FIN:16

for b₁, b₂, b₃ being set
for b₄ being finite set
for b₅ being Nat st not b₁ in b₄ & b₂ <> b₃ holds
card (Choose b₄,b₅,b₂,b₃) = Card { b₆ where B is Function of b₄ \/ {b₁},{b₂,b₃} : ( Card (b₆ " {b₂}) = b₅ & b₆ . b₁ = b₃ ) }

proof end;

Lemma18: for b₁, b₂, b₃ being set
for b₄ being finite set
for b₅ being Nat st b₁ <> b₂ & not b₃ in b₄ holds
( { b₆ where B is Function of b₄ \/ {b₃},{b₁,b₂} : ( Card (b₆ " {b₁}) = b₅ + 1 & b₆ . b₃ = b₁ ) } \/ { b₆ where B is Function of b₄ \/ {b₃},{b₁,b₂} : ( Card (b₆ " {b₁}) = b₅ + 1 & b₆ . b₃ = b₂ ) } = Choose (b₄ \/ {b₃}),(b₅ + 1),b₁,b₂ & { b₆ where B is Function of b₄ \/ {b₃},{b₁,b₂} : ( Card (b₆ " {b₁}) = b₅ + 1 & b₆ . b₃ = b₁ ) } misses { b₆ where B is Function of b₄ \/ {b₃},{b₁,b₂} : ( Card (b₆ " {b₁}) = b₅ + 1 & b₆ . b₃ = b₂ ) } )

proof end;

theorem Th17: :: CARD_FIN:17

for b₁, b₂, b₃ being set
for b₄ being finite set
for b₅ being Nat st b₁ <> b₂ & not b₃ in b₄ holds
card (Choose (b₄ \/ {b₃}),(b₅ + 1),b₁,b₂) = (card (Choose b₄,(b₅ + 1),b₁,b₂)) + (card (Choose b₄,b₅,b₁,b₂))

proof end;

theorem Th18: :: CARD_FIN:18

for b₁, b₂ being set
for b₃ being finite set
for b₄ being Nat st b₁ <> b₂ holds
card (Choose b₃,b₄,b₁,b₂) = (card b₃) choose b₄

proof end;

theorem Th19: :: CARD_FIN:19

for b₁, b₂ being set
for b₃, b₄ being finite set st b₁ <> b₂ holds
(b₃ --> b₂) +* (b₄ --> b₁) in Choose (b₄ \/ b₃),(card b₄),b₁,b₂

proof end;

theorem Th20: :: CARD_FIN:20

for b₁, b₂ being set
for b₃, b₄ being finite set st b₁ <> b₂ & b₃ misses b₄ holds
(b₃ --> b₁) +* (b₄ --> b₂) in Choose (b₃ \/ b₄),(card b₃),b₁,b₂

proof end;

definition

let c₁, c₂ be Function;
let c₃ be set ;
func Intersection c₁,c₂,c₃ -> Subset of (union (rng a₁)) means :Def2: :: CARD_FIN:def 2
for b₁ being set holds
( b₁ in a₄ iff ( b₁ in union (rng a₁) & ( for b₂ being set st b₂ in dom a₂ & a₂ . b₂ = a₃ holds
b₁ in a₁ . b₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Intersection CARD_FIN:def 2 :

theorem Th21: :: CARD_FIN:21

for b₁, b₂ being set
for b₃, b₄ being Function st not (dom b₃) /\ (b₄ " {b₁}) is empty holds
( b₂ in Intersection b₃,b₄,b₁ iff for b₅ being set st b₅ in dom b₄ & b₄ . b₅ = b₁ holds
b₂ in b₃ . b₅ )

proof end;

theorem Th22: :: CARD_FIN:22

for b₁ being set
for b₂, b₃ being Function st not Intersection b₂,b₃,b₁ is empty holds
b₃ " {b₁} c= dom b₂

proof end;

theorem Th23: :: CARD_FIN:23

for b₁ being set
for b₂, b₃ being Function st not Intersection b₂,b₃,b₁ is empty holds
for b₄, b₅ being set st b₄ in b₃ " {b₁} & b₅ in b₃ " {b₁} holds
b₂ . b₄ meets b₂ . b₅

proof end;

theorem Th24: :: CARD_FIN:24

for b₁, b₂ being set
for b₃, b₄ being Function st b₁ in Intersection b₃,b₄,b₂ & b₂ in rng b₄ holds
ex b₅ being set st
( b₅ in dom b₄ & b₄ . b₅ = b₂ & b₁ in b₃ . b₅ )

proof end;

theorem Th25: :: CARD_FIN:25

for b₁ being set
for b₂, b₃ being Function st ( b₂ is empty or union (rng b₂) is empty ) holds
Intersection b₂,b₃,b₁ = union (rng b₂)

proof end;

theorem Th26: :: CARD_FIN:26

for b₁ being set
for b₂, b₃ being Function st b₂ | (b₃ " {b₁}) = (b₃ " {b₁}) --> (union (rng b₂)) holds
Intersection b₂,b₃,b₁ = union (rng b₂)

proof end;

theorem Th27: :: CARD_FIN:27

for b₁ being set
for b₂, b₃ being Function st not union (rng b₂) is empty & Intersection b₂,b₃,b₁ = union (rng b₂) holds
b₂ | (b₃ " {b₁}) = (b₃ " {b₁}) --> (union (rng b₂))

proof end;

theorem Th28: :: CARD_FIN:28

for b₁ being set
for b₂ being Function holds Intersection b₂,{} ,b₁ = union (rng b₂)

proof end;

theorem Th29: :: CARD_FIN:29

for b₁, b₂ being set
for b₃, b₄ being Function holds Intersection b₃,b₄,b₁ c= Intersection b₃,(b₄ | b₂),b₁

proof end;

theorem Th30: :: CARD_FIN:30

for b₁, b₂ being set
for b₃, b₄ being Function st b₃ " {b₁} = (b₃ | b₂) " {b₁} holds
Intersection b₄,b₃,b₁ = Intersection b₄,(b₃ | b₂),b₁

proof end;

theorem Th31: :: CARD_FIN:31

for b₁, b₂ being set
for b₃, b₄ being Function holds Intersection (b₃ | b₁),b₄,b₂ c= Intersection b₃,b₄,b₂

proof end;

theorem Th32: :: CARD_FIN:32

for b₁, b₂ being set
for b₃, b₄ being Function st b₁ in rng b₃ & b₃ " {b₁} c= b₂ holds
Intersection (b₄ | b₂),b₃,b₁ = Intersection b₄,b₃,b₁

proof end;

theorem Th33: :: CARD_FIN:33

for b₁, b₂ being set
for b₃, b₄ being Function st b₁ in b₃ " {b₂} holds
Intersection b₄,b₃,b₂ c= b₄ . b₁

proof end;

theorem Th34: :: CARD_FIN:34

for b₁, b₂ being set
for b₃, b₄ being Function st b₁ in b₃ " {b₂} holds
(Intersection b₄,(b₃ | ((dom b₃) \ {b₁})),b₂) /\ (b₄ . b₁) = Intersection b₄,b₃,b₂

proof end;

theorem Th35: :: CARD_FIN:35

for b₁, b₂ being set
for b₃, b₄, b₅ being Function st b₄ " {b₁} = b₅ " {b₂} holds
Intersection b₃,b₄,b₁ = Intersection b₃,b₅,b₂

proof end;

theorem Th36: :: CARD_FIN:36

for b₁ being set
for b₂, b₃ being Function st b₂ " {b₁} = {} holds
Intersection b₃,b₂,b₁ = union (rng b₃)

proof end;

theorem Th37: :: CARD_FIN:37

for b₁, b₂ being set
for b₃, b₄ being Function st {b₁} = b₃ " {b₂} holds
Intersection b₄,b₃,b₂ = b₄ . b₁

proof end;

theorem Th38: :: CARD_FIN:38

for b₁, b₂, b₃ being set
for b₄, b₅ being Function st {b₁,b₂} = b₄ " {b₃} holds
Intersection b₅,b₄,b₃ = (b₅ . b₁) /\ (b₅ . b₂)

proof end;

theorem Th39: :: CARD_FIN:39

for b₁, b₂ being set
for b₃ being Function st not b₃ is empty holds
( b₁ in Intersection b₃,((dom b₃) --> b₂),b₂ iff for b₄ being set st b₄ in dom b₃ holds
b₁ in b₃ . b₄ )

proof end;

definition

let c₁ be Function;
attr a₁ is finite-yielding means :Def3: :: CARD_FIN:def 3
for b₁ being set holds a₁ . b₁ is finite;

end;

:: deftheorem Def3 defines finite-yielding CARD_FIN:def 3 :

registration

cluster non empty finite-yielding set ;
existence

proof end;

cluster empty finite-yielding set ;
existence

proof end;

end;

registration

let c₁ be finite-yielding Function;
let c₂ be set ;
cluster a₁ . a₂ -> finite ;
coherence by Def3;

end;

registration

let c₁ be finite-yielding Function;
let c₂ be set ;
cluster a₁ | a₂ -> finite-yielding ;
coherence

proof end;

end;

registration

let c₁ be finite-yielding Function;
let c₂ be Function;
cluster a₂ * a₁ -> finite-yielding ;
coherence

proof end;

cluster Intersect a₁,a₂ -> finite-yielding ;
coherence

proof end;

end;

theorem Th40: :: CARD_FIN:40

for b₁ being set
for b₂ being Function
for b₃ being finite-yielding Function st b₁ in rng b₂ holds
Intersection b₃,b₂,b₁ is finite

proof end;

theorem Th41: :: CARD_FIN:41

for b₁ being finite-yielding Function st dom b₁ is finite holds
union (rng b₁) is finite

proof end;

definition

let c₁ be XFinSequence;
let c₂ be Nat;
redefine func | as c₁ | c₂ -> XFinSequence;
coherence by AFINSQ_1:12;

end;

definition

let c₁ be set ;
let c₂ be XFinSequence of c₁;
let c₃ be Nat;
redefine func | as c₂ | c₃ -> XFinSequence of a₁;
coherence by AFINSQ_1:16;

end;

Lemma41: for b₁ being Nat
for b₂ being XFinSequence st b₁ <= len b₂ holds
( len (b₂ | b₁) = b₁ & dom (b₂ | b₁) = b₁ )

proof end;

theorem Th42: :: CARD_FIN:42

for b₁ being non empty set
for b₂ being XFinSequence of b₁
for b₃ being BinOp of b₁
for b₄ being Nat st b₄ in dom b₂ & ( b₃ has_a_unity or b₄ <> 0 ) holds
b₃ . (b₃ "**" (b₂ | b₄)),(b₂ . b₄) = b₃ "**" (b₂ | (b₄ + 1))

proof end;

theorem Th43: :: CARD_FIN:43

for b₁ being non empty set
for b₂ being XFinSequence of b₁
for b₃ being Nat st len b₂ = b₃ + 1 holds
b₂ = (b₂ | b₃) ^ <%(b₂ . b₃)%>

proof end;

theorem Th44: :: CARD_FIN:44

for b₁ being XFinSequence of NAT
for b₂ being Nat st b₂ in dom b₁ holds
(Sum (b₁ | b₂)) + (b₁ . b₂) = Sum (b₁ | (b₂ + 1))

proof end;

theorem Th45: :: CARD_FIN:45

for b₁ being XFinSequence of NAT
for b₂ being Nat st rng b₁ c= {0,b₂} holds
Sum b₁ = b₂ * (card (b₁ " {b₂}))

proof end;

theorem Th46: :: CARD_FIN:46

for b₁ being set
for b₂, b₃ being Nat holds
( b₁ in Choose b₂,b₃,1,0 iff ex b₄ being XFinSequence of NAT st
( b₄ = b₁ & dom b₄ = b₂ & rng b₄ c= {0,1} & Sum b₄ = b₃ ) )

proof end;

theorem Th47: :: CARD_FIN:47

for b₁ being non empty set
for b₂ being XFinSequence of b₁
for b₃ being BinOp of b₁ st ( b₃ has_a_unity or len b₂ >= 1 ) holds
b₃ "**" b₂ = b₃ "**" (XFS2FS b₂)

proof end;

theorem Th48: :: CARD_FIN:48

for b₁ being non empty set
for b₂ being BinOp of b₁
for b₃, b₄ being XFinSequence of b₁
for b₅ being Permutation of dom b₃ st b₂ is commutative & b₂ is associative & ( b₂ has_a_unity or len b₃ >= 1 ) & b₄ = b₃ * b₅ holds
b₂ "**" b₃ = b₂ "**" b₄

proof end;

Lemma47: for b₁ being finite set ex b₂ being Function of card b₁,b₁ st b₂ is one-to-one

proof end;

definition

let c₁ be Nat;
let c₂ be finite-yielding Function;
assume E48: dom c₂ is finite ;
func Card_Intersection c₂,c₁ -> Nat means :Def4: :: CARD_FIN:def 4
for b₁, b₂ being set
for b₃ being finite set
for b₄ being Function of card (Choose b₃,a₁,b₁,b₂), Choose b₃,a₁,b₁,b₂ st dom a₂ = b₃ & b₄ is one-to-one & b₁ <> b₂ holds
ex b₅ being XFinSequence of NAT st
( dom b₅ = dom b₄ & ( for b₆ being set
for b₇ being Function st b₆ in dom b₅ & b₇ = b₄ . b₆ holds
b₅ . b₆ = Card (Intersection a₂,b₇,b₁) ) & a₃ = Sum b₅ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Card_Intersection CARD_FIN:def 4 :

theorem Th49: :: CARD_FIN:49

for b₁ being Nat
for b₂ being finite-yielding Function
for b₃, b₄ being set
for b₅ being finite set
for b₆ being Function of card (Choose b₅,b₁,b₃,b₄), Choose b₅,b₁,b₃,b₄ st dom b₂ = b₅ & b₆ is one-to-one & b₃ <> b₄ holds
for b₇ being XFinSequence of NAT st dom b₇ = dom b₆ & ( for b₈ being set
for b₉ being Function st b₈ in dom b₇ & b₉ = b₆ . b₈ holds
b₇ . b₈ = Card (Intersection b₂,b₉,b₃) ) holds
Card_Intersection b₂,b₁ = Sum b₇

proof end;

theorem Th50: :: CARD_FIN:50

for b₁ being Nat
for b₂ being finite-yielding Function st dom b₂ is finite & b₁ = 0 holds
Card_Intersection b₂,b₁ = Card (union (rng b₂))

proof end;

theorem Th51: :: CARD_FIN:51

for b₁ being finite set
for b₂ being Nat
for b₃ being finite-yielding Function st dom b₃ = b₁ & b₂ > card b₁ holds
Card_Intersection b₃,b₂ = 0

proof end;

theorem Th52: :: CARD_FIN:52

for b₁ being finite-yielding Function
for b₂ being finite set st dom b₁ = b₂ holds
for b₃ being Function of card b₂,b₂ st b₃ is one-to-one holds
ex b₄ being XFinSequence of NAT st
( dom b₄ = card b₂ & ( for b₅ being set st b₅ in dom b₄ holds
b₄ . b₅ = card ((b₁ * b₃) . b₅) ) & Card_Intersection b₁,1 = Sum b₄ )

proof end;

theorem Th53: :: CARD_FIN:53

for b₁ being set
for b₂ being finite set
for b₃ being finite-yielding Function st dom b₃ = b₂ holds
Card_Intersection b₃,(card b₂) = Card (Intersection b₃,(b₂ --> b₁),b₁)

proof end;

theorem Th54: :: CARD_FIN:54

for b₁ being set
for b₂ being finite set
for b₃ being finite-yielding Function st b₃ = b₁ .--> b₂ holds
Card_Intersection b₃,1 = card b₂

proof end;

theorem Th55: :: CARD_FIN:55

for b₁, b₂ being set
for b₃, b₄ being finite set
for b₅ being finite-yielding Function st b₁ <> b₂ & b₅ = b₁,b₂ --> b₃,b₄ holds
( Card_Intersection b₅,1 = (card b₃) + (card b₄) & Card_Intersection b₅,2 = card (b₃ /\ b₄) )

proof end;

theorem Th56: :: CARD_FIN:56

for b₁ being finite-yielding Function
for b₂ being set st dom b₁ is finite & b₂ in dom b₁ holds
Card_Intersection b₁,1 = (Card_Intersection (b₁ | ((dom b₁) \ {b₂})),1) + (card (b₁ . b₂))

proof end;

theorem Th57: :: CARD_FIN:57

for b₁ being set
for b₂ being Function holds
( dom (Intersect b₂,((dom b₂) --> b₁)) = dom b₂ & ( for b₃ being set st b₃ in dom b₂ holds
(Intersect b₂,((dom b₂) --> b₁)) . b₃ = (b₂ . b₃) /\ b₁ ) )

proof end;

theorem Th58: :: CARD_FIN:58

for b₁ being set
for b₂ being Function holds (union (rng b₂)) /\ b₁ = union (rng (Intersect b₂,((dom b₂) --> b₁)))

proof end;

theorem Th59: :: CARD_FIN:59

for b₁, b₂ being set
for b₃, b₄ being Function holds (Intersection b₃,b₄,b₁) /\ b₂ = Intersection (Intersect b₃,((dom b₃) --> b₂)),b₄,b₁

proof end;

theorem Th60: :: CARD_FIN:60

for b₁, b₂ being XFinSequence st b₁ is one-to-one & b₂ is one-to-one & rng b₁ misses rng b₂ holds
b₁ ^ b₂ is one-to-one

proof end;

theorem Th61: :: CARD_FIN:61

for b₁ being Nat
for b₂ being finite-yielding Function
for b₃ being finite set
for b₄ being set
for b₅ being Nat st dom b₂ = b₃ & b₄ in dom b₂ & b₁ > 0 holds
Card_Intersection b₂,(b₁ + 1) = (Card_Intersection (b₂ | ((dom b₂) \ {b₄})),(b₁ + 1)) + (Card_Intersection (Intersect (b₂ | ((dom b₂) \ {b₄})),(((dom b₂) \ {b₄}) --> (b₂ . b₄))),b₁)

proof end;

theorem Th62: :: CARD_FIN:62

for b₁ being non empty set
for b₂ being BinOp of b₁
for b₃, b₄, b₅ being XFinSequence of b₁ st b₂ is commutative & b₂ is associative & ( b₂ has_a_unity or len b₃ >= 1 ) & len b₃ = len b₄ & len b₃ = len b₅ & ( for b₆ being Nat st b₆ in dom b₅ holds
b₅ . b₆ = b₂ . (b₃ . b₆),(b₄ . b₆) ) holds
b₂ "**" (b₃ ^ b₄) = b₂ "**" b₅

proof end;

definition

let c₁ be XFinSequence of INT ;
func Sum c₁ -> Integer equals :: CARD_FIN:def 5
addint "**" a₁;
coherence ;

end;

:: deftheorem Def5 defines Sum CARD_FIN:def 5 :

definition

let c₁ be XFinSequence of INT ;
let c₂ be set ;
redefine func . as c₁ . c₂ -> Integer;
coherence

proof end;

end;

theorem Th63: :: CARD_FIN:63

for b₁ being XFinSequence of NAT
for b₂ being XFinSequence of INT st b₂ = b₁ holds
Sum b₂ = Sum b₁

proof end;

theorem Th64: :: CARD_FIN:64

for b₁, b₂ being XFinSequence of INT
for b₃ being Integer st dom b₁ = dom b₂ & ( for b₄ being Nat st b₄ in dom b₁ holds
b₃ * (b₁ . b₄) = b₂ . b₄ ) holds
b₃ * (Sum b₁) = Sum b₂

proof end;

theorem Th65: :: CARD_FIN:65

for b₁ being set
for b₂ being Function st b₁ in dom b₂ holds
union (rng b₂) = (union (rng (b₂ | ((dom b₂) \ {b₁})))) \/ (b₂ . b₁)

proof end;

theorem Th66: :: CARD_FIN:66

for b₁ being finite-yielding Function
for b₂ being finite set ex b₃ being XFinSequence of INT st
( dom b₃ = card b₂ & ( for b₄ being Nat st b₄ in dom b₃ holds
b₃ . b₄ = ((- 1) |^ b₄) * (Card_Intersection b₁,(b₄ + 1)) ) )

proof end;

theorem Th67: :: CARD_FIN:67

for b₁ being finite-yielding Function
for b₂ being finite set st dom b₁ = b₂ holds
for b₃ being XFinSequence of INT st dom b₃ = card b₂ & ( for b₄ being Nat st b₄ in dom b₃ holds
b₃ . b₄ = ((- 1) |^ b₄) * (Card_Intersection b₁,(b₄ + 1)) ) holds
Card (union (rng b₁)) = Sum b₃

proof end;

theorem Th68: :: CARD_FIN:68

for b₁ being finite-yielding Function
for b₂ being finite set
for b₃, b₄ being Nat st dom b₁ = b₂ & ex b₅, b₆ being set st
( b₅ <> b₆ & ( for b₇ being Function st b₇ in Choose b₂,b₄,b₅,b₆ holds
Card (Intersection b₁,b₇,b₅) = b₃ ) ) holds
Card_Intersection b₁,b₄ = b₃ * ((card b₂) choose b₄)

proof end;

theorem Th69: :: CARD_FIN:69

for b₁ being finite-yielding Function
for b₂ being finite set st dom b₁ = b₂ holds
for b₃ being XFinSequence of NAT st dom b₃ = card b₂ & ( for b₄ being Nat st b₄ in dom b₃ holds
ex b₅, b₆ being set st
( b₅ <> b₆ & ( for b₇ being Function st b₇ in Choose b₂,(b₄ + 1),b₅,b₆ holds
Card (Intersection b₁,b₇,b₅) = b₃ . b₄ ) ) ) holds
ex b₄ being XFinSequence of INT st
( dom b₄ = card b₂ & Card (union (rng b₁)) = Sum b₄ & ( for b₅ being Nat st b₅ in dom b₄ holds
b₄ . b₅ = (((- 1) |^ b₅) * (b₃ . b₅)) * ((card b₂) choose (b₅ + 1)) ) )

proof end;

Lemma67: for b₁, b₂ being finite set st not b₁ is empty & not b₂ is empty holds
ex b₃ being XFinSequence of INT st
( dom b₃ = card b₂ & ((card b₂) |^ (card b₁)) - (Sum b₃) = Card { b₄ where B is Function of b₁,b₂ : b₄ is onto } & ( for b₄ being Nat st b₄ in dom b₃ holds
b₃ . b₄ = (((- 1) |^ b₄) * ((card b₂) choose (b₄ + 1))) * ((((card b₂) - b₄) - 1) |^ (card b₁)) ) )

proof end;

theorem Th70: :: CARD_FIN:70

for b₁, b₂ being finite set st not b₁ is empty & not b₂ is empty holds
ex b₃ being XFinSequence of INT st
( dom b₃ = (card b₂) + 1 & Sum b₃ = Card { b₄ where B is Function of b₁,b₂ : b₄ is onto } & ( for b₄ being Nat st b₄ in dom b₃ holds
b₃ . b₄ = (((- 1) |^ b₄) * ((card b₂) choose b₄)) * (((card b₂) - b₄) |^ (card b₁)) ) )

proof end;

theorem Th71: :: CARD_FIN:71

for b₁, b₂ being Nat st b₂ <= b₁ holds
ex b₃ being XFinSequence of INT st
( b₁ block b₂ = (1 / (b₂ ! )) * (Sum b₃) & dom b₃ = b₂ + 1 & ( for b₄ being Nat st b₄ in dom b₃ holds
b₃ . b₄ = (((- 1) |^ b₄) * (b₂ choose b₄)) * ((b₂ - b₄) |^ b₁) ) )

proof end;

theorem Th72: :: CARD_FIN:72

for b₁, b₂, b₃ being finite set st ( b₂ is empty implies b₁ is empty ) & b₃ c= b₁ holds
for b₄ being Function of b₁,b₂ st b₄ is one-to-one & card b₁ = card b₂ holds
((card b₁) -' (card b₃)) ! = Card { b₅ where B is Function of b₁,b₂ : ( b₅ is one-to-one & rng (b₅ | (b₁ \ b₃)) c= b₄ .: (b₁ \ b₃) & ( for b₁ being set st b₆ in b₃ holds
b₅ . b₆ = b₄ . b₆ ) ) }

proof end;

Lemma70: for b₁, b₂ being finite set
for b₃ being Function of b₁,b₂ st dom b₃ = b₁ & b₃ is one-to-one holds
ex b₄ being XFinSequence of INT st
( dom b₄ = card b₁ & ((card b₁) ! ) - (Sum b₄) = Card { b₅ where B is Function of b₁, rng b₃ : ( b₅ is one-to-one & ( for b₁ being set st b₆ in b₁ holds
b₅ . b₆ <> b₃ . b₆ ) ) } & ( for b₅ being Nat st b₅ in dom b₄ holds
b₄ . b₅ = (((- 1) |^ b₅) * ((card b₁) ! )) / ((b₅ + 1) ! ) ) )

proof end;

theorem Th73: :: CARD_FIN:73

for b₁ being finite set
for b₂ being Function st dom b₂ = b₁ & b₂ is one-to-one holds
ex b₃ being XFinSequence of INT st
( Sum b₃ = Card { b₄ where B is Function of b₁, rng b₂ : ( b₄ is one-to-one & ( for b₁ being set st b₅ in b₁ holds
b₄ . b₅ <> b₂ . b₅ ) ) } & dom b₃ = (card b₁) + 1 & ( for b₄ being Nat st b₄ in dom b₃ holds
b₃ . b₄ = (((- 1) |^ b₄) * ((card b₁) ! )) / (b₄ ! ) ) )

proof end;

theorem Th74: :: CARD_FIN:74

for b₁ being finite set ex b₂ being XFinSequence of INT st
( Sum b₂ = Card { b₃ where B is Function of b₁,b₁ : ( b₃ is one-to-one & ( for b₁ being set st b₄ in b₁ holds
b₃ . b₄ <> b₄ ) ) } & dom b₂ = (card b₁) + 1 & ( for b₃ being Nat st b₃ in dom b₂ holds
b₂ . b₃ = (((- 1) |^ b₃) * ((card b₁) ! )) / (b₃ ! ) ) )

proof end;