:: CARD_FIN semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for x, X' being set st x in X' holds
(X' \ {x}) \/ {x} = X'
by ZFMISC_1:140;

Lm2: for x, X' being set st not x in X' holds
(X' \/ {x}) \ {x} = X'
by ZFMISC_1:141;

theorem Th1: :: CARD_FIN:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being finite set st X c= Y & card X = card Y holds
X = Y
proof end;

theorem Th2: :: CARD_FIN:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) }
proof end;

theorem Th3: :: CARD_FIN:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 }
proof end;

theorem Th4: :: CARD_FIN:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being finite set st ( Y = {} implies X = {} ) holds
card (Funcs X,Y) = (card Y) |^ (card X)
proof end;

theorem Th5: :: CARD_FIN:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) }
proof end;

theorem :: CARD_FIN:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being Nat holds (n ! ) / ((n -' k) ! ) is Nat
proof end;

theorem Th7: :: CARD_FIN:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)) ! )
proof end;

theorem Th8: :: CARD_FIN:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being finite set holds Card { F where F is Function of X,X : F is Permutation of X } = (card X) !
proof end;

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 & 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 & Card (f " {x1}) = k ) )
proof end;
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 & Card (f " {x1}) = k ) ) ) & ( for x being set holds
( x in b2 iff ex f being Function of X,{x1,x2} st
( f = x & Card (f " {x1}) = k ) ) ) holds
b1 = b2
proof end;
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 & Card (f " {x1}) = k ) ) );

theorem :: CARD_FIN:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th10: :: CARD_FIN:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th11: :: CARD_FIN:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for X being finite set st x1 <> x2 holds
card (Choose X,0,x1,x2) = 1
proof end;

theorem Th12: :: CARD_FIN:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for X being finite set holds card (Choose X,(card X),x1,x2) = 1
proof end;

theorem Th13: :: CARD_FIN:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, x being set
for f being Function st f . y = x & y in dom f holds
{y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x}
proof end;

theorem Th14: :: CARD_FIN:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & f . z = x ) }
proof end;

theorem Th15: :: CARD_FIN:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, x being set
for f being Function st f . y <> x holds
(f | ((dom f) \ {y})) " {x} = f " {x}
proof end;

theorem Th16: :: CARD_FIN:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z, x, y being set
for X being finite set
for k being Nat st not z in X & x <> y holds
card (Choose X,k,x,y) = Card { f where f is Function of X \/ {z},{x,y} : ( Card (f " {x}) = k & f . z = y ) }
proof end;

Lm3: for x, y, z being set
for X being finite set
for k being Nat st x <> y & not z in X holds
( { f where f is Function of X \/ {z},{x,y} : ( Card (f " {x}) = k + 1 & f . z = x ) } \/ { f where f is Function of X \/ {z},{x,y} : ( Card (f " {x}) = k + 1 & f . z = y ) } = Choose (X \/ {z}),(k + 1),x,y & { f where f is Function of X \/ {z},{x,y} : ( Card (f " {x}) = k + 1 & f . z = x ) } misses { f where f is Function of X \/ {z},{x,y} : ( Card (f " {x}) = k + 1 & f . z = y ) } )
proof end;

theorem Th17: :: CARD_FIN:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set
for X being finite set
for k being Nat st x <> y & 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))
proof end;

theorem Th18: :: CARD_FIN:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th19: :: CARD_FIN:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th20: :: CARD_FIN:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for X, Y being finite set st x <> y & X misses Y holds
(X --> x) +* (Y --> y) in Choose (X \/ Y),(card X),x,y
proof end;

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) & ( for x being set st x in dom Ch & 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) & ( for x being set st x in dom Ch & Ch . x = y holds
z in F . x ) ) )
proof end;
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) & ( for x being set st x in dom Ch & Ch . x = y holds
z in F . x ) ) ) ) & ( for z being set holds
( z in b2 iff ( z in union (rng F) & ( for x being set st x in dom Ch & Ch . x = y holds
z in F . x ) ) ) ) holds
b1 = b2
proof end;
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) & ( for x being set st x in dom Ch & Ch . x = y holds
z in F . x ) ) ) );

theorem Th21: :: CARD_FIN:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & Ch . z = x holds
y in F . z )
proof end;

theorem Th22: :: CARD_FIN:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y being set
for F, Ch being Function st not Intersection F,Ch,y is empty holds
Ch " {y} c= dom F
proof end;

theorem :: CARD_FIN:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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} & x2 in Ch " {y} holds
F . x1 meets F . x2
proof end;

theorem Th24: :: CARD_FIN:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z, y being set
for F, Ch being Function st z in Intersection F,Ch,y & y in rng Ch holds
ex x being set st
( x in dom Ch & Ch . x = y & z in F . x )
proof end;

theorem :: CARD_FIN:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th26: :: CARD_FIN:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: CARD_FIN:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y being set
for F, Ch being Function st not union (rng F) is empty & Intersection F,Ch,y = union (rng F) holds
F | (Ch " {y}) = (Ch " {y}) --> (union (rng F))
proof end;

theorem Th28: :: CARD_FIN:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y being set
for F being Function holds Intersection F,{} ,y = union (rng F)
proof end;

theorem Th29: :: CARD_FIN:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, X' being set
for F, Ch being Function holds Intersection F,Ch,y c= Intersection F,(Ch | X'),y
proof end;

theorem Th30: :: CARD_FIN:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, X' being set
for Ch, F being Function st Ch " {y} = (Ch | X') " {y} holds
Intersection F,Ch,y = Intersection F,(Ch | X'),y
proof end;

theorem Th31: :: CARD_FIN:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X', y being set
for F, Ch being Function holds Intersection (F | X'),Ch,y c= Intersection F,Ch,y
proof end;

theorem Th32: :: CARD_FIN:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, X' being set
for Ch, F being Function st y in rng Ch & Ch " {y} c= X' holds
Intersection (F | X'),Ch,y = Intersection F,Ch,y
proof end;

theorem Th33: :: CARD_FIN:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for Ch, F being Function st x in Ch " {y} holds
Intersection F,Ch,y c= F . x
proof end;

theorem Th34: :: CARD_FIN:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th35: :: CARD_FIN:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th36: :: CARD_FIN:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y being set
for Ch, F being Function st Ch " {y} = {} holds
Intersection F,Ch,y = union (rng F)
proof end;

theorem Th37: :: CARD_FIN:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for Ch, F being Function st {x} = Ch " {y} holds
Intersection F,Ch,y = F . x
proof end;

theorem Th38: :: CARD_FIN:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: CARD_FIN:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let F be Function;
attr F is finite-yielding means :Def3: :: CARD_FIN:def 3
for x being set holds F . x is finite;
end;

:: deftheorem Def3 defines finite-yielding CARD_FIN:def 3 :
for F being Function holds
( F is finite-yielding iff for x being set holds F . x is finite );

registration
cluster non empty finite-yielding set ;
existence
ex b1 being Function st
( not b1 is empty & b1 is finite-yielding )
proof end;
cluster empty finite-yielding set ;
existence
ex b1 being Function st
( b1 is empty & b1 is finite-yielding )
proof end;
end;

registration
let F be finite-yielding Function;
let x be set ;
cluster F . x -> finite ;
coherence
F . x is finite
by Def3;
end;

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

registration
let F be finite-yielding Function;
let G be Function;
cluster G * F -> finite-yielding ;
coherence
F * G is finite-yielding
proof end;
cluster Intersect F,G -> finite-yielding ;
coherence
Intersect F,G is finite-yielding
proof end;
end;

theorem :: CARD_FIN:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th41: :: CARD_FIN:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Fy being finite-yielding Function st dom Fy is finite holds
union (rng Fy) is finite
proof end;

definition
let F be XFinSequence;
let n be Nat;
:: original: |
redefine func F | n -> XFinSequence;
coherence
F | n is XFinSequence
by AFINSQ_1:12;
end;

definition
let D be set ;
let F be XFinSequence of D;
let n be Nat;
:: original: |
redefine func F | n -> XFinSequence of D;
coherence
F | n is XFinSequence of D
by AFINSQ_1:16;
end;

Lm4: for k being Nat
for F being XFinSequence st k <= len F holds
( len (F | k) = k & dom (F | k) = k )
proof end;

theorem Th42: :: CARD_FIN:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being XFinSequence of D
for b being BinOp of D
for n being Nat st n in dom F & ( b has_a_unity or n <> 0 ) holds
b . (b "**" (F | n)),(F . n) = b "**" (F | (n + 1))
proof end;

theorem :: CARD_FIN:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being XFinSequence of D
for n being Nat st len F = n + 1 holds
F = (F | n) ^ <%(F . n)%>
proof end;

theorem Th44: :: CARD_FIN:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being XFinSequence of NAT
for n being Nat st n in dom F holds
(Sum (F | n)) + (F . n) = Sum (F | (n + 1))
proof end;

theorem Th45: :: CARD_FIN:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being XFinSequence of NAT
for n being Nat st rng F c= {0,n} holds
Sum F = n * (card (F " {n}))
proof end;

theorem :: CARD_FIN:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for n, k being Nat holds
( x in Choose n,k,1,0 iff ex F being XFinSequence of NAT st
( F = x & dom F = n & rng F c= {0,1} & Sum F = k ) )
proof end;

theorem Th47: :: CARD_FIN:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being XFinSequence of D
for b being BinOp of D st ( b has_a_unity or len F >= 1 ) holds
b "**" F = b "**" (XFS2FS F)
proof end;

theorem Th48: :: CARD_FIN:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for b being BinOp of D
for F, G being XFinSequence of D
for P being Permutation of dom F st b is commutative & b is associative & ( b has_a_unity or len F >= 1 ) & G = F * P holds
b "**" F = b "**" G
proof end;

Lm5: for X being finite set ex P being Function of card X,X st P is one-to-one
proof end;

definition
let k be Nat;
let F be finite-yielding Function;
assume A1: dom F is finite ;
func Card_Intersection F,k -> 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 & P is one-to-one & x <> y holds
ex XFS being XFinSequence of NAT st
( dom XFS = dom P & ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = Card (Intersection F,f,x) ) & it = Sum XFS );
existence
ex b1 being 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 & P is one-to-one & x <> y holds
ex XFS being XFinSequence of NAT st
( dom XFS = dom P & ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = Card (Intersection F,f,x) ) & b1 = Sum XFS )
proof end;
uniqueness
for b1, b2 being 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 & P is one-to-one & x <> y holds
ex XFS being XFinSequence of NAT st
( dom XFS = dom P & ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = Card (Intersection F,f,x) ) & b1 = Sum XFS ) ) & ( 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 & P is one-to-one & x <> y holds
ex XFS being XFinSequence of NAT st
( dom XFS = dom P & ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = Card (Intersection F,f,x) ) & b2 = Sum XFS ) ) holds
b1 = b2
proof end;
end;

:: 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 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 & P is one-to-one & x <> y holds
ex XFS being XFinSequence of NAT st
( dom XFS = dom P & ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = Card (Intersection F,f,x) ) & b3 = Sum XFS ) );

theorem :: CARD_FIN:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & P is one-to-one & x <> y holds
for XFS being XFinSequence of NAT st dom XFS = dom P & ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = Card (Intersection Fy,f,x) ) holds
Card_Intersection Fy,k = Sum XFS
proof end;

theorem :: CARD_FIN:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for Fy being finite-yielding Function st dom Fy is finite & k = 0 holds
Card_Intersection Fy,k = Card (union (rng Fy))
proof end;

theorem Th51: :: CARD_FIN:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being finite set
for k being Nat
for Fy being finite-yielding Function st dom Fy = X & k > card X holds
Card_Intersection Fy,k = 0
proof end;

theorem Th52: :: CARD_FIN:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 NAT st
( dom XFS = card X & ( for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z) ) & Card_Intersection Fy,1 = Sum XFS )
proof end;

theorem Th53: :: CARD_FIN:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th54: :: CARD_FIN:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: CARD_FIN:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for X, Y being finite set
for Fy being finite-yielding Function st x <> y & Fy = x,y --> X,Y holds
( Card_Intersection Fy,1 = (card X) + (card Y) & Card_Intersection Fy,2 = card (X /\ Y) )
proof end;

theorem Th56: :: CARD_FIN:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Fy being finite-yielding Function
for x being set st dom Fy is finite & x in dom Fy holds
Card_Intersection Fy,1 = (Card_Intersection (Fy | ((dom Fy) \ {x})),1) + (card (Fy . x))
proof end;

theorem Th57: :: CARD_FIN:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X' being set
for F being Function holds
( dom (Intersect F,((dom F) --> X')) = dom F & ( for x being set st x in dom F holds
(Intersect F,((dom F) --> X')) . x = (F . x) /\ X' ) )
proof end;

theorem Th58: :: CARD_FIN:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X' being set
for F being Function holds (union (rng F)) /\ X' = union (rng (Intersect F,((dom F) --> X')))
proof end;

theorem Th59: :: CARD_FIN:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, X' being set
for F, Ch being Function holds (Intersection F,Ch,y) /\ X' = Intersection (Intersect F,((dom F) --> X')),Ch,y
proof end;

theorem Th60: :: CARD_FIN:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being XFinSequence st F is one-to-one & G is one-to-one & rng F misses rng G holds
F ^ G is one-to-one
proof end;

theorem Th61: :: CARD_FIN:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & x in dom Fy & 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)
proof end;

theorem Th62: :: CARD_FIN:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for b being BinOp of D
for F, G, bFG being XFinSequence of D st b is commutative & b is associative & ( b has_a_unity or len F >= 1 ) & len F = len G & len F = len bFG & ( for n being Nat st n in dom bFG holds
bFG . n = b . (F . n),(G . n) ) holds
b "**" (F ^ G) = b "**" bFG
proof end;

definition
let Fi be XFinSequence of INT ;
func Sum Fi -> Integer equals :: CARD_FIN:def 5
addint "**" Fi;
coherence
addint "**" Fi is Integer
;
end;

:: deftheorem defines Sum CARD_FIN:def 5 :
for Fi being XFinSequence of INT holds Sum Fi = addint "**" Fi;

definition
let Fi be XFinSequence of INT ;
let x be set ;
:: original: .
redefine func Fi . x -> Integer;
coherence
Fi . x is Integer
proof end;
end;

theorem Th63: :: CARD_FIN:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Fn being XFinSequence of NAT
for Fi being XFinSequence of INT st Fi = Fn holds
Sum Fi = Sum Fn
proof end;

theorem Th64: :: CARD_FIN:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, Fi being XFinSequence of INT
for i being Integer st dom F = dom Fi & ( for n being Nat st n in dom F holds
i * (F . n) = Fi . n ) holds
i * (Sum F) = Sum Fi
proof end;

theorem Th65: :: CARD_FIN:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th66: :: CARD_FIN:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Fy being finite-yielding Function
for X being finite set ex XFS being XFinSequence of INT st
( dom XFS = card X & ( for n being Nat st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ) )
proof end;

theorem Th67: :: CARD_FIN:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Fy being finite-yielding Function
for X being finite set st dom Fy = X holds
for XFS being XFinSequence of INT st dom XFS = card X & ( 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
proof end;

theorem Th68: :: CARD_FIN:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Fy being finite-yielding Function
for X being finite set
for n, k being Nat st dom Fy = X & ex x, y being set st
( x <> y & ( 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)
proof end;

theorem Th69: :: CARD_FIN:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Fy being finite-yielding Function
for X being finite set st dom Fy = X holds
for XF being XFinSequence of NAT st dom XF = card X & ( 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 X,(n + 1),x,y holds
Card (Intersection Fy,f,x) = XF . n ) ) ) holds
ex F being XFinSequence of INT st
( dom F = card X & Card (union (rng Fy)) = Sum F & ( for n being Nat st n in dom F holds
F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) )
proof end;

Lm6: for X, Y being finite set st not X is empty & not Y is empty holds
ex F being XFinSequence of INT st
( dom F = card Y & ((card Y) |^ (card X)) - (Sum F) = Card { f where f is Function of X,Y : f is onto } & ( 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)) ) )
proof end;

theorem Th70: :: CARD_FIN:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being finite set st not X is empty & not Y is empty holds
ex F being XFinSequence of INT st
( dom F = (card Y) + 1 & Sum F = Card { f where f is Function of X,Y : f is onto } & ( for n being Nat st n in dom F holds
F . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X)) ) )
proof end;

theorem :: CARD_FIN:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being Nat st k <= n holds
ex F being XFinSequence of INT st
( n block k = (1 / (k ! )) * (Sum F) & dom F = k + 1 & ( for m being Nat st m in dom F holds
F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n) ) )
proof end;

theorem Th72: :: CARD_FIN:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, Y1, X being finite set st ( Y1 is empty implies X1 is empty ) & X c= X1 holds
for F being Function of X1,Y1 st F is one-to-one & card X1 = card Y1 holds
((card X1) -' (card X)) ! = Card { f where f is Function of X1,Y1 : ( f is one-to-one & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X holds
f . x = F . x ) )
}
proof end;

Lm7: for X, Y being finite set
for F being Function of X,Y st dom F = X & F is one-to-one holds
ex XF being XFinSequence of INT st
( dom XF = card X & ((card X) ! ) - (Sum XF) = 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 ) )
}
& ( for n being Nat st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) ! )) / ((n + 1) ! ) ) )
proof end;

theorem Th73: :: CARD_FIN:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being finite set
for F being Function st dom F = X & F is one-to-one holds
ex XF being XFinSequence of INT st
( Sum XF = 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 ) )
}
& dom XF = (card X) + 1 & ( for n being Nat st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! ) ) )
proof end;

theorem :: CARD_FIN:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being finite set ex XF being XFinSequence of INT st
( Sum XF = Card { h where h is Function of X,X : ( h is one-to-one & ( for x being set st x in X holds
h . x <> x ) )
}
& dom XF = (card X) + 1 & ( for n being Nat st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! ) ) )
proof end;