:: Cardinal Numbers and Finite Sets
:: by Karol P\c{a}k
::
:: Received May 24, 2005
:: Copyright (c) 2005-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, FUNCT_1, NAT_1, TARSKI, FINSET_1, RELAT_1,
AFINSQ_1, ARYTM_1, ARYTM_3, FINSEQ_1, XXREAL_0, CARD_1, XBOOLE_0,
ORDINAL4, CARD_3, BINOP_1, FINSOP_1, FUNCOP_1, BINOP_2, FUNCT_2, INT_1,
VALUED_1, NEWTON, REALSET1, ZFMISC_1, FUNCT_4, EQREL_1, SETFAM_1,
STIRL2_1, CARD_FIN;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, RELAT_1,
FUNCT_1, XCMPLX_0, NAT_1, FINSET_1, XXREAL_0, NAT_D, AFINSQ_1, VALUED_1,
RELSET_1, PARTFUN1, DOMAIN_1, FUNCT_2, FUNCT_4, FUNCOP_1, INT_1,
ENUMSET1, BINOP_1, BINOP_2, RECDEF_1, AFINSQ_2, ZFMISC_1, NEWTON,
STIRL2_1, YELLOW20;
constructors PARTFUN3, BINOM, WELLORD2, DOMAIN_1, SETWISEO, REAL_1, NAT_D,
YELLOW20, RECDEF_1, BINOP_2, RELSET_1, ORDINAL4, AFINSQ_1, SEQ_4,
AFINSQ_2, STIRL2_1, NUMBERS, NEWTON;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FUNCOP_1, FUNCT_4, FINSET_1, FRAENKEL, NUMBERS, XXREAL_0, XREAL_0, NAT_1,
INT_1, BINOP_2, CARD_1, WSIERP_1, AFINSQ_1, RELSET_1, VALUED_1, VALUED_0,
AFINSQ_2, NEWTON;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, FUNCT_1, FINSET_1;
equalities FUNCOP_1, RELAT_1, ORDINAL1;
expansions TARSKI, XBOOLE_0, FUNCT_1;
theorems AFINSQ_1, TARSKI, FUNCT_1, XBOOLE_0, ZFMISC_1, RELAT_1, XBOOLE_1,
NAT_1, FUNCT_2, FINSET_1, XCMPLX_1, CARD_2, INT_1, WELLORD2, ENUMSET1,
CARD_1, BINOP_2, NEWTON, XREAL_1, FUNCOP_1, STIRL2_1, FUNCT_5, IRRAT_1,
FUNCT_4, YELLOW20, XXREAL_0, NAT_D, XREAL_0, AFINSQ_2, ORDINAL1,
VALUED_1, XTUPLE_0, FINSEQ_4;
schemes FUNCT_2, NAT_1, XBOOLE_0, STIRL2_1;
begin
reserve x, x1, x2, y, z, X9 for set,
X, Y for finite set,
n, k, m for Nat,
f for Function;
::$CT
theorem Th1:
for X,Y,x,y 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
defpred P[set,set,set] means 1=1;
let X,Y,x,y;
assume
A1: Y={} implies X={};
set F2={f where f is Function of (X\/{x}),(Y\/{y}): P[f,X\/{x},Y\/{y}]&rng (
f|X) c=Y & f.x=y};
A2: for f be Function of X\/{x},Y\/{y} st f.x=y holds P[f,X\/{x},Y\/{y}] iff
P[f|X,X,Y];
set F1={f where f is Function of X,Y:P[f,X,Y]};
assume
A3: not x in X;
set F3={F where F is Function of X\/{x},Y\/{y}:rng (F|X) c=Y & F.x=y};
A4: Funcs(X,Y) c= F1
proof
let F be object;
assume F in Funcs(X,Y);
then F is Function of X,Y by FUNCT_2:66;
hence thesis;
end;
A5: F2 c= F3
proof
let F be object;
assume F in F2;
then
ex f be Function of (X\/{x}),(Y\/{y}) st f=F & P[f,X\/{x},Y\/{y}]&rng
(f|X) c=Y & f.x=y;
hence thesis;
end;
A6: Y is empty implies X is empty by A1;
A7: card F1=card F2 from STIRL2_1:sch 4(A6,A3,A2);
A8: F3 c= F2
proof
let F be object;
assume F in F3;
then ex f be Function of (X\/{x}),(Y\/{y}) st f=F & rng (f|X) c=Y & f.x=y;
hence thesis;
end;
F1 c= Funcs(X,Y)
proof
let F be object;
assume F in F1;
then ex f be Function of X,Y st f=F & P[f,X,Y];
hence thesis by A1,FUNCT_2:8;
end;
then Funcs(X,Y) = F1 by A4;
hence thesis by A5,A8,A7,XBOOLE_0:def 10;
end;
theorem Th2:
for X,Y,x,y 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
let X,Y,x,y such that
A1: not x in X and
A2: y in Y;
set F2={F where F is Function of X\/{x},Y:F.x=y};
set F1={F where F is Function of X\/{x},Y\/{y}:rng (F|X) c=Y & F.x=y};
{y} c= Y by A2,ZFMISC_1:31;
then
A3: Y=Y\/{y} by XBOOLE_1:12;
A4: F2 c= F1
proof
let f be object;
assume f in F2;
then consider F be Function of X\/{x},Y such that
A5: f=F & F.x=y;
rng (F|X) c=Y;
hence thesis by A3,A5;
end;
F1 c= F2
proof
let f be object;
assume f in F1;
then ex F be Function of X\/{x},Y\/{y} st f=F & rng (F|X) c=Y & F.x=y;
hence thesis by A3;
end;
then F1=F2 by A4;
hence thesis by A1,A2,Th1;
end;
:: card Funcs(X,Y)
theorem Th3:
(Y={} implies X={}) implies card Funcs(X,Y) = card Y |^ card X
proof
assume
A1: Y={} implies X={};
per cases;
suppose
A2: Y is empty;
then card Funcs(X,Y)=1 by A1,CARD_1:30,FUNCT_2:127;
hence thesis by A1,A2,NEWTON:4;
end;
suppose
A3: Y is non empty;
defpred P[Nat] means for X,Y st Y is non empty & card X= $1
holds card Funcs(X,Y)=card Y |^ card X;
A4: for n st P[n] holds P[n+1]
proof
defpred Q[set] means 1=1;
let n such that
A5: P[n];
let X,Y such that
A6: Y is non empty and
A7: card X=n+1;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
reconsider cY=card Y |^ nn as Element of NAT;
card Y,Y are_equipotent by CARD_1:def 2;
then consider f be Function such that
A8: f is one-to-one and
A9: dom f= card Y and
A10: rng f= Y by WELLORD2:def 4;
reconsider f as Function of card Y,Y by A9,A10,FUNCT_2:1;
consider x being object such that
A11: x in X by A7,CARD_1:27,XBOOLE_0:def 1;
reconsider x as set by TARSKI:1;
A12: x in X by A11;
A13: f is onto one-to-one by A8,A10,FUNCT_2:def 3;
consider F be XFinSequence of NAT such that
A14: dom F = card Y and
A15: card{g where g is Function of X,Y:Q[g]} = Sum(F) and
A16: for k st k in dom F holds F.k = card{g where g is Function of X
,Y:Q[g] & g.x=f.k} from STIRL2_1:sch 6(A13,A6,A12);
A17: for k be Nat st k in dom F holds F.k=cY
proof
set Xx=X\{x};
let k be Nat such that
A18: k in dom F;
A19: f.k in rng f by A9,A14,A18,FUNCT_1:def 3;
set F3={g where g is Function of X,Y:Q[g] & g.x=f.k};
set F2={g where g is Function of Xx\/{x},Y: g.x=f.k};
A20: F3 c= F2
proof
let G be object;
assume G in F3;
then
A21: ex g be Function of X,Y st g=G & Q[g] & g.x=f.k;
Xx\/{x}=X by A12,ZFMISC_1:116;
hence thesis by A21;
end;
F2 c=F3
proof
let G be object;
assume G in F2;
then
A22: ex g be Function of Xx\/{x},Y st g=G & g.x=f.k;
Xx\/{x}=X by A12,ZFMISC_1:116;
hence thesis by A22;
end;
then
A23: F2=F3 by A20;
card Xx=n by A7,A12,STIRL2_1:55;
then
A24: card Funcs(Xx,Y)=cY by A5,A19;
x in {x} by TARSKI:def 1;
then not x in Xx by XBOOLE_0:def 5;
then card Funcs(Xx,Y)=card F2 by A19,Th2;
hence thesis by A16,A18,A23,A24;
end;
then for k be Nat st k in dom F holds F.k >= cY;
then
A25: Sum F >= len F*card Y|^n by AFINSQ_2:60;
set F1={g where g is Function of X,Y:Q[g]};
A26: Funcs(X,Y) c= F1
proof
let G be object;
assume G in Funcs(X,Y);
then G is Function of X,Y by FUNCT_2:66;
hence thesis;
end;
F1 c= Funcs(X,Y)
proof
let G be object;
assume G in F1;
then ex g be Function of X,Y st g=G & Q[g];
hence thesis by A6,FUNCT_2:8;
end;
then
A27: Funcs(X,Y) = F1 by A26;
for k be Nat st k in dom F holds F.k <= cY by A17;
then Sum F<=len F*card Y|^n by AFINSQ_2:59;
then Sum F = card Y * card Y |^ n by A14,A25,XXREAL_0:1;
hence thesis by A7,A15,A27,NEWTON:6;
end;
A28: P[0]
proof
let X,Y such that
Y is non empty and
A29: card X=0;
X is empty by A29;
then Funcs(X,Y) = {{}} by FUNCT_5:57;
then card Funcs(X,Y)=1 by CARD_1:30;
hence thesis by A29,NEWTON:4;
end;
for n holds P[n] from NAT_1:sch 2(A28,A4);
hence thesis by A3;
end;
end;
theorem Th4:
for X,Y,x,y 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
let X,Y,x,y such that
A1: Y is empty implies X is empty and
A2: not x in X and
A3: not y in Y;
defpred P[Function,set,set] means $1 is one-to-one & rng ($1|X) c=Y;
A4: for f be Function of X\/{x},Y\/{y} st f.x=y holds P[f,X\/{x},Y\/{y}] iff
P[f|X,X,Y]
proof
let f be Function of X\/{x},Y\/{y} such that
A5: f.x=y;
thus P[f,X\/{x},Y\/{y}] implies P[f|X,X,Y] by FUNCT_1:52;
thus P[f|X,X,Y] implies P[f,X\/{x},Y\/{y}]
proof
(X\/{x})/\X=X & dom f = X\/{x} by FUNCT_2:def 1,XBOOLE_1:21;
then
A6: dom (f|X)=X by RELAT_1:61;
assume that
A7: f|X is one-to-one and
A8: rng (f|X|X) c=Y;
rng (f|X) c= Y by A8;
then f|X is Function of X,Y by A6,FUNCT_2:2;
hence thesis by A1,A3,A5,A7,A8,STIRL2_1:58;
end;
end;
set F3={F where F is Function of X\/{x},Y\/{y}: F is one-to-one & F.x=y};
A9: F3 c= {f where f is Function of (X\/{x}),(Y\/{y}): P[f,X\/{x},Y\/{y}] &
rng (f|X) c=Y & f.x=y}
proof
let z be object;
assume z in F3;
then consider F be Function of X\/{x},Y\/{y} such that
A10: z=F and
A11: F is one-to-one & F.x=y;
rng (F|X) c=Y
proof
A12: dom F=X\/{x} by FUNCT_2:def 1;
x in {x} by TARSKI:def 1;
then
A13: x in dom F by A12,XBOOLE_0:def 3;
assume not rng (F|X) c=Y;
then consider fz be object such that
A14: fz in rng (F|X) and
A15: not fz in Y;
consider z be object such that
A16: z in dom (F|X) and
A17: fz=(F|X).z by A14,FUNCT_1:def 3;
A18: z in dom F by A16,RELAT_1:57;
A19: fz in Y or fz in {y} by A14,XBOOLE_0:def 3;
A20: z in X by A16;
F.z=(F|X).z by A16,FUNCT_1:47;
then y=F.z by A15,A17,A19,TARSKI:def 1;
hence thesis by A2,A11,A13,A20,A18;
end;
hence thesis by A10,A11;
end;
A21: {f where f is Function of (X\/{x}),(Y\/{y}): P[f,X\/{x},Y\/{y}]&rng (f|
X) c=Y &f.x=y} c= F3
proof
let z be object;
assume z in {f where f is Function of (X\/{x}),(Y\/{y}): P[f,X\/{x},Y\/{
y}] & rng (f|X) c=Y & f.x=y};
then ex f be Function of (X\/{x}),(Y\/{y}) st z=f & P[f,X\/{x},Y\/{y}] &
rng (f|X) c=Y & f.x=y;
hence thesis;
end;
set F2={f where f is Function of X,Y:f is one-to-one & rng (f|X) c= Y};
set F1={F where F is Function of X,Y:F is one-to-one};
A22: F1 c=F2
proof
let z be object;
assume z in F1;
then consider F be Function of X,Y such that
A23: z=F & F is one-to-one;
rng (F|X) c= rng F;
hence thesis by A23;
end;
A24: not x in X by A2;
A25: card{f where f is Function of X,Y:P[f,X,Y]}= card{f where f is Function
of (X\/{x}),(Y\/{y}): P[f,X\/{x},Y\/{y}]&rng (f|X) c=Y & f.x=y} from
STIRL2_1:
sch 4(A1,A24,A4);
F2 c=F1
proof
let z be object;
assume z in F2;
then ex f be Function of X,Y st z=f & f is one-to-one & rng (f|X)c= Y;
hence thesis;
end;
then F2=F1 by A22;
hence thesis by A9,A21,A25,XBOOLE_0:def 10;
end;
theorem
n!/((n-'k)!) is Element of NAT
proof
n!/((n-'k)!) is integer by IRRAT_1:36,NAT_D:35;
hence thesis by INT_1:3;
end;
:: one-to-one
theorem Th6:
card X <= card Y implies card {F where F is Function of X,Y:F is
one-to-one} = card Y!/((card Y-'card X)!)
proof
defpred P[Nat] means for X,Y st card Y=$1 & 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)!);
A1: for n st P[n] holds P[n+1]
proof
let n such that
A2: P[n];
let X,Y such that
A3: card Y=n+1 and
A4: card X <= card Y;
per cases;
suppose
A5: X is empty;
set F1={F where F is Function of X,Y:F is one-to-one};
A6: F1 c= {{}}
proof
let x be object;
assume x in F1;
then ex F be Function of X,Y st x=F & F is one-to-one;
then x={} by A5;
hence thesis by TARSKI:def 1;
end;
A7: rng {} c=Y;
card Y-card X=card Y by A5;
then
A8: (card Y-'card X)!=card Y! by XREAL_0:def 2;
A9: card Y! /((card Y-'card X)!)=1 by A8,XCMPLX_1:60;
dom {}=X by A5;
then {} is Function of X,Y by A7,FUNCT_2:2;
then {} in F1;
then F1 = {{}} by A6,ZFMISC_1:33;
hence thesis by A9,CARD_1:30;
end;
suppose
X is non empty;
then consider x being object such that
A10: x in X;
reconsider x as set by TARSKI:1;
A11: x in X by A10;
defpred F[Function] means $1 is one-to-one;
card Y,Y are_equipotent by CARD_1:def 2;
then consider f be Function such that
A12: f is one-to-one and
A13: dom f= card Y and
A14: rng f= Y by WELLORD2:def 4;
reconsider f as Function of card Y,Y by A13,A14,FUNCT_2:1;
A15: Y is non empty by A3;
A16: f is onto one-to-one by A12,A14,FUNCT_2:def 3;
consider F be XFinSequence of NAT such that
A17: dom F = card Y and
A18: card{g where g is Function of X,Y:F[g]} = Sum(F) and
A19: for k st k in dom F holds F.k = card{g where g is Function of X
,Y:F[g] & g.x=f.k} from STIRL2_1:sch 6(A16,A15,A11);
A20: for k be Nat st k in dom F holds F.k= n!/((card Y-'card X)!)
proof
card X >0 by A11;
then reconsider cX1=card X-1 as Element of NAT by NAT_1:20;
set Xx=X\{x};
x in {x} by TARSKI:def 1;
then
A21: not x in Xx by XBOOLE_0:def 5;
A22: X=Xx\/{x} by A11,ZFMISC_1:116;
A23: (cX1+1)-1<=(n+1)-1 by A3,A4,XREAL_1:9;
then
A24: n-cX1>=cX1-cX1 by XREAL_1:9;
let k be Nat such that
A25: k in dom F;
A26: f.k in Y by A13,A14,A17,A25,FUNCT_1:def 3;
set Yy=Y\{f.k};
A27: Y=Yy\/{f.k} by A26,ZFMISC_1:116;
f.k in {f.k} by TARSKI:def 1;
then
A28: not f.k in Yy by XBOOLE_0:def 5;
cX1+1 <=n+1 by A3,A4;
then
A29: card Xx =cX1 by A11,STIRL2_1:55;
A30: card Yy =n by A3,A26,STIRL2_1:55;
then
A31: Yy is empty implies Xx is empty by A23,A29;
A32: card {g where g is Function of Xx,Yy:g is one-to-one}= n!/((card
Yy-' card Xx)!) by A2,A23,A29,A30;
card Y-card X >= card X -card X by A4,XREAL_1:9;
then
card Y-'card X=((card Yy+1)-1)-((card Xx+1)-1) by A3,A29,A30,XREAL_0:def 2
.=card Yy-'card Xx by A29,A30,A24,XREAL_0:def 2;
then
card{g where g is Function of X,Y:g is one-to-one & g.x=f.k} = n!
/((card Y-'card X)!) by A32,A27,A22,A28,A21,A31,Th4;
hence thesis by A19,A25;
end;
then for k be Nat st k in dom F holds F.k >= n!/((card Y-'card X)!);
then
A33: Sum F>=len F*(n!/((card Y-'card X)!)) by AFINSQ_2:60;
for k be Nat st k in dom F holds F.k <= n!/((card Y-'card X)!) by A20;
then Sum F<=len F*(n!/((card Y-'card X)!)) by AFINSQ_2:59;
then Sum F = (n+1) *((n!/((card Y-'card X)!))) by A3,A17,A33,XXREAL_0:1
.=((n+1)*(n!))/((card Y-'card X)!) by XCMPLX_1:74
.=card Y!/((card Y-'card X)!) by A3,NEWTON:15;
hence thesis by A18;
end;
end;
A34: P[0]
proof
let X,Y such that
A35: card Y=0 and
A36: card X <= card Y;
card Y-card X=0 by A35,A36;
then
A37: (card Y-'card X)!=1 by NEWTON:12,XREAL_0:def 2;
set F1={F where F is Function of X,Y:F is one-to-one};
A38: F1 c= {{}}
proof
let x be object;
assume x in F1;
then
A39: ex F be Function of X,Y st x=F & F is one-to-one;
Y={} by A35;
then x={} by A39;
hence thesis by TARSKI:def 1;
end;
dom {}=X & rng {}=Y by A35,A36;
then {} is Function of X,Y by FUNCT_2:1;
then {} in F1;
then F1 = {{}} by A38,ZFMISC_1:33;
hence thesis by A35,A37,CARD_1:30,NEWTON:12;
end;
for n holds P[n] from NAT_1:sch 2(A34,A1);
hence thesis;
end;
:: Permutation of X
theorem Th7:
card{F where F is Function of X,X:F is Permutation of X}=card X!
proof
set F1={F where F is Function of X,X:F is one-to-one};
set F2={F where F is Function of X,X:F is Permutation of X};
A1: F1 c= F2
proof
let x be object;
assume x in F1;
then consider F be Function of X,X such that
A2: x=F and
A3: F is one-to-one;
card X=card X;
then F is onto by A3,FINSEQ_4:63;
hence thesis by A2,A3;
end;
(card X-'card X)!=1 by NEWTON:12,XREAL_1:232;
then
A4: card X!/((card X-'card X)!)=card X!;
F2 c= F1
proof
let x be object;
assume x in F2;
then ex F be Function of X,X st x=F & F is Permutation of X;
hence thesis;
end;
then F1=F2 by A1;
hence thesis by A4,Th6;
end;
definition
let X,k; let x1,x2 be object;
func Choose(X,k,x1,x2) -> Subset of Funcs(X,{x1,x2}) means
:Def1:
x in it iff ex f be Function of X,{x1,x2} st f = x & card (f"{x1})=k;
existence
proof
defpred P[object] means
ex f be Function of X,{x1,x2} st $1=f & card (f"{x1})=k;
consider F being set such that
A1: for x being object holds x in F iff x in bool [:X,{x1,x2}:] & P[x]
from XBOOLE_0:sch 1;
F c= Funcs(X,{x1,x2})
proof
let x be object;
assume x in F;
then ex f be Function of X,{x1,x2} st x=f & card (f"{x1})=k by A1;
hence thesis by FUNCT_2:8;
end;
then reconsider F as Subset of Funcs(X,{x1,x2});
take F;
let x;
thus x in F implies ex f be Function of X,{x1,x2} st x=f & card (f"{x1}) =
k by A1;
given f be Function of X,{x1,x2} such that
A2: x = f & card (f"{x1})=k;
thus thesis by A1,A2;
end;
uniqueness
proof
let F1,F2 be Subset of Funcs(X,{x1,x2}) such that
A3: x in F1 iff ex f be Function of X,{x1,x2} st x = f & card (f"{x1}) =k and
A4: x in F2 iff ex f be Function of X,{x1,x2} st x = f & card (f"{x1}) =k;
for x being object holds x in F1 iff x in F2
proof let x be object;
x in F1 iff ex f be Function of X,{x1,x2} st x=f& card (f"{x1})=k by A3;
hence thesis by A4;
end;
hence thesis by TARSKI:2;
end;
end;
theorem
card X<>k implies Choose(X,k,x1,x1) is empty
proof
assume
A1: card X<>k;
assume Choose(X,k,x1,x1) is non empty;
then consider y being object such that
A2: y in Choose(X,k,x1,x1);
consider f be Function of X,{x1,x1} such that
f = y and
A3: card (f"{x1}) = k by A2,Def1;
per cases;
suppose
A4: rng f is empty;
A5: dom f=X by FUNCT_2:def 1;
dom f={} by A4,RELAT_1:42;
hence thesis by A1,A3,A5;
end;
suppose
A6: rng f is non empty;
{x1,x1}={x1} by ENUMSET1:29;
then rng f={x1} by A6,ZFMISC_1:33;
then f"{x1}=dom f by RELAT_1:134;
hence thesis by A1,A3,FUNCT_2:def 1;
end;
end;
theorem Th9:
for x1,x2 being object holds
card X < k implies Choose(X,k,x1,x2) is empty
proof let x1,x2 be object;
assume
A1: card X < k;
assume Choose(X,k,x1,x2) is non empty;
then consider z being object such that
A2: z in Choose(X,k,x1,x2);
ex f be Function of X,{x1,x2} st f = z & card (f"{x1}) = k by A2,Def1;
hence thesis by A1,NAT_1:43;
end;
theorem Th10:
for x1,x2 being object holds
x1<>x2 implies card Choose(X,0,x1,x2)=1
proof let x1,x2 be object;
assume
A1: x1<>x2;
per cases;
suppose
A2: X is empty;
dom {}=X by A2;
then reconsider Empty={} as Function of X,{x1,x2} by XBOOLE_1:2;
A3: Choose(X,0,x1,x2) c= {Empty}
proof
let z be object;
assume z in Choose(X,0,x1,x2);
then consider f be Function of X,{x1,x2} such that
A4: z=f and
card (f"{x1})=0 by Def1;
dom f=X by FUNCT_2:def 1;
then f=Empty;
hence thesis by A4,TARSKI:def 1;
end;
Empty"{x1}={} & card {}=0;
then Empty in Choose(X,0,x1,x2) by Def1;
then Choose(X,0,x1,x2)={Empty} by A3,ZFMISC_1:33;
hence thesis by CARD_1:30;
end;
suppose
A5: X is non empty;
then consider f be Function such that
A6: dom f=X and
A7: rng f={x2} by FUNCT_1:5;
rng f c= {x1,x2} by A7,ZFMISC_1:36;
then
A8: f is Function of X,{x1,x2} by A6,FUNCT_2:2;
A9: Choose(X,0,x1,x2) c= {f}
proof
let z be object;
assume z in Choose(X,0,x1,x2);
then consider g be Function of X,{x1,x2} such that
A10: z=g and
A11: card (g"{x1})=0 by Def1;
g"{x1}={} by A11;
then not x1 in rng g by FUNCT_1:72;
then ( not rng g={x1})& not rng g={x1,x2} by TARSKI:def 1,def 2;
then dom g=X & rng g={x2} by A5,FUNCT_2:def 1,ZFMISC_1:36;
then g=f by A6,A7,FUNCT_1:7;
hence thesis by A10,TARSKI:def 1;
end;
not x1 in rng f by A1,A7,TARSKI:def 1;
then
A12: f"{x1}={} by FUNCT_1:72;
card {}=0;
then f in Choose(X,0,x1,x2) by A12,A8,Def1;
then Choose(X,0,x1,x2)={f} by A9,ZFMISC_1:33;
hence thesis by CARD_1:30;
end;
end;
theorem Th11:
for x1,x2 being object holds
card Choose(X,card X,x1,x2)=1
proof let x1,x2 be object;
per cases;
suppose
A1: X is empty;
dom {}=X by A1;
then reconsider Empty={} as Function of X,{x1,x2} by XBOOLE_1:2;
A2: Choose(X,card X,x1,x2) c= {Empty}
proof
let z be object;
assume z in Choose(X,card X,x1,x2);
then consider f be Function of X,{x1,x2} such that
A3: z=f and
card (f"{x1})=card X by Def1;
dom f=X by FUNCT_2:def 1;
then f=Empty;
hence thesis by A3,TARSKI:def 1;
end;
Empty"{x1}={};
then Empty in Choose(X,card X,x1,x2) by A1,Def1;
then Choose(X,card X,x1,x2)={Empty} by A2,ZFMISC_1:33;
hence thesis by CARD_1:30;
end;
suppose
A4: X is non empty;
then consider f be Function such that
A5: dom f=X and
A6: rng f={x1} by FUNCT_1:5;
rng f c= {x1,x2} by A6,ZFMISC_1:36;
then
A7: f is Function of X,{x1,x2} by A5,FUNCT_2:2;
A8: Choose(X,card X,x1,x2) c= {f}
proof
let z be object;
assume z in Choose(X,card X,x1,x2);
then consider g be Function of X,{x1,x2} such that
A9: z=g and
A10: card (g"{x1})=card X by Def1;
A11: now
per cases;
suppose
x1=x2;
then {x1,x2}={x1} by ENUMSET1:29;
hence rng g={x1} by A4,ZFMISC_1:33;
end;
suppose
A12: x1<>x2;
g"{x2}={}
proof
assume g"{x2}<>{};
then consider z being object such that
A13: z in g"{x2} by XBOOLE_0:def 1;
g.z in {x2} by A13,FUNCT_1:def 7;
then
A14: g.z=x2 by TARSKI:def 1;
g"{x1}=X by A10,CARD_2:102;
then g.z in {x1} by A13,FUNCT_1:def 7;
hence thesis by A12,A14,TARSKI:def 1;
end;
then not x2 in rng g by FUNCT_1:72;
then ( not rng g={x2})& not rng g={x1,x2} by TARSKI:def 1,def 2;
hence rng g={x1} by A4,ZFMISC_1:36;
end;
end;
dom g=X by FUNCT_2:def 1;
then g=f by A5,A6,A11,FUNCT_1:7;
hence thesis by A9,TARSKI:def 1;
end;
card (f"{x1})=card X by A5,A6,RELAT_1:134;
then f in Choose(X,card X,x1,x2) by A7,Def1;
then Choose(X,card X,x1,x2)={f} by A8,ZFMISC_1:33;
hence thesis by CARD_1:30;
end;
end;
theorem Th12:
for z,x,y being object holds
not z in X implies 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 let z,x,y be object;
set F1={f where f is Function of X\/{z},{x,y}:card (f"{x})=k+1 & f.z=x};
defpred P[set,set,set] means for f be Function st f=$1 holds card ((f|X)"{x}
)=k;
A1: for f be Function of X\/{z},{x,y}\/{x} st f.z=x holds P[f,X\/{z},{x,y}\/
{x}] iff P[f|X,X,{x,y}]
proof
let f be Function of X\/{z},{x,y}\/{x} such that
f.z=x;
(f|X)=((f|X)|X);
hence thesis;
end;
set F3={f where f is Function of X\/{z},{x,y}\/{x}: P[f,X\/{z},{x,y}\/{x}] &
rng (f|X) c={x,y} & f.z=x};
set F2={f where f is Function of X,{x,y}:P[f,X,{x,y}]};
assume
A2: not z in X;
A3: F3 c= F1
proof
{x}\/{x,y}={x,x,y} by ENUMSET1:2;
then
A4: {x,y}\/{x}={x,y} by ENUMSET1:30;
z in {z} by TARSKI:def 1;
then
A5: z in X\/{z} by XBOOLE_0:def 3;
let x1 be object;
assume x1 in F3;
then consider f be Function of X\/{z},{x,y}\/{x} such that
A6: x1=f and
A7: P[f,X\/{z},{x,y}\/{x}] and
rng (f|X) c={x,y} and
A8: f.z=x;
dom f=X\/{z} & (X\/{z})\{z}=X by A2,FUNCT_2:def 1,ZFMISC_1:117;
then
A9: {z}\/(f|X)"{x}=f"{x} by A8,A5,AFINSQ_2:66;
not z in dom f/\X by A2,XBOOLE_0:def 4;
then not z in dom (f|X) by RELAT_1:61;
then
A10: not z in (f|X)"{x} by FUNCT_1:def 7;
card ((f|X)"{x})=k by A7;
then card (f"{x})=k+1 by A9,A10,CARD_2:41;
hence thesis by A6,A8,A4;
end;
A11: F2 c=Choose(X,k,x,y)
proof
let x1 be object;
assume x1 in F2;
then consider f be Function of X,{x,y} such that
A12: x1=f and
A13: P[f,X,{x,y}];
f|X=f;
then card (f"{x})=k by A13;
hence thesis by A12,Def1;
end;
A14: Choose(X,k,x,y)c= F2
proof
let x1 be object;
assume x1 in Choose(X,k,x,y);
then consider f be Function of X,{x,y} such that
A15: x1=f and
A16: card (f"{x})=k by Def1;
P[f,X,{x,y}] by A16;
hence thesis by A15;
end;
A17: {x,y} is empty implies X is empty;
A18: card F2=card F3 from STIRL2_1:sch 4(A17,A2,A1);
F1 c= F3
proof
z in {z} by TARSKI:def 1;
then
A19: z in X\/{z} by XBOOLE_0:def 3;
let x1 be object;
assume x1 in F1;
then consider f be Function of X\/{z},{x,y} such that
A20: x1=f and
A21: card (f"{x})=k+1 and
A22: f.z=x;
not z in dom f/\X by A2,XBOOLE_0:def 4;
then not z in dom (f|X) by RELAT_1:61;
then
A23: not z in ((f|X)"{x}) by FUNCT_1:def 7;
dom f=X\/{z} & (X\/{z})\{z}=X by A2,FUNCT_2:def 1,ZFMISC_1:117;
then ((f|X)"{x})\/{z}=f"{x} by A22,A19,AFINSQ_2:66;
then card ((f|X)"{x})+1=k+1 by A21,A23,CARD_2:41;
then
A24: P[f,X\/{z},{x,y}\/{x}];
{x}\/{x,y}={x,x,y} by ENUMSET1:2;
then rng (f|X) c={x,y} & f is Function of X\/{z},{x,y}\/{x} by ENUMSET1:30;
hence thesis by A20,A22,A24;
end;
then F1=F3 by A3;
hence thesis by A11,A14,A18,XBOOLE_0:def 10;
end;
theorem Th13:
for z,x,y being object holds
not z in X & x<>y implies 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 let z,x,y be object;
assume that
A1: not z in X and
A2: x<>y;
defpred P[set,set,set] means for f be Function st f=$1 holds card (f"{x})=k;
A3: for f be Function of X\/{z},{x,y}\/{y} st f.z=y holds P[f,X\/{z},{x,y}\/
{y}] iff P[f|X,X,{x,y}]
proof
let f be Function of X\/{z},{x,y}\/{y} such that
A4: f.z=y;
(X\/{z})\{z}=X & dom f=X\/{z} by A1,FUNCT_2:def 1,ZFMISC_1:117;
then (f|X)"{x} = f"{x} by A2,A4,AFINSQ_2:67;
hence thesis;
end;
set F2={f where f is Function of X\/{z},{x,y}\/{y}: P[f,X\/{z},{x,y}\/{y}] &
rng (f|X) c={x,y} & f.z=y};
set F1={f where f is Function of X,{x,y}:P[f,X,{x,y}]};
A5: {x,y} is empty implies X is empty;
A6: card F1=card F2 from STIRL2_1:sch 4(A5,A1,A3);
set F3={f where f is Function of X\/{z},{x,y}:card (f"{x})=k & f.z=y};
A7: F2 c= F3
proof
let x1 be object;
assume x1 in F2;
then consider f be Function of X\/{z},{x,y}\/{y} such that
A8: x1=f and
A9: P[f,X\/{z},{x,y}\/{y}] and
rng (f|X) c={x,y} and
A10: f.z=y;
{x,y}\/{y}={y,y,x} by ENUMSET1:2;
then
A11: f is Function of X\/{z},{x,y} by ENUMSET1:30;
card (f"{x})=k by A9;
hence thesis by A8,A10,A11;
end;
A12: F3 c= F2
proof
let x1 be object;
assume x1 in F3;
then consider f be Function of X\/{z},{x,y}such that
A13: f=x1 and
A14: card (f"{x})=k and
A15: f.z=y;
{x,y}\/{y}={y,y,x} by ENUMSET1:2;
then
A16: rng (f|X) c={x,y} & f is Function of X\/{z},{x,y}\/{y} by ENUMSET1:30;
P[f,X\/{z},{x,y}\/{y}] by A14;
hence thesis by A13,A15,A16;
end;
A17: Choose(X,k,x,y) c= F1
proof
let x1 be object;
assume x1 in Choose(X,k,x,y);
then consider f be Function of X,{x,y} such that
A18: x1=f and
A19: card (f"{x})=k by Def1;
P[f,X,{x,y}] by A19;
hence thesis by A18;
end;
F1 c= Choose(X,k,x,y)
proof
let x1 be object;
assume x1 in F1;
then consider f be Function of X,{x,y} such that
A20: x1=f and
A21: P[f,X,{x,y}];
card (f"{x})=k by A21;
hence thesis by A20,Def1;
end;
then Choose(X,k,x,y) = F1 by A17;
hence thesis by A7,A12,A6,XBOOLE_0:def 10;
end;
Lm1:
for z,x,y being object holds
x<>y implies {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 let z,x,y be object;
set F1={f where f is Function of X\/{z},{x,y}:card (f"{x})=k+1 & f.z=x};
set F2={f where f is Function of X\/{z},{x,y}:card (f"{x})=k+1 & f.z=y};
assume
A1: x<>y;
A2: F1 misses F2
proof
assume F1 meets F2;
then F1/\F2<>{};
then consider x1 being object such that
A3: x1 in F1/\F2 by XBOOLE_0:def 1;
x1 in F2 by A3,XBOOLE_0:def 4;
then
A4: ex f2 be Function of X\/{z},{x,y} st x1=f2 & card (f2"{x })=k+1 & f2.z =y;
x1 in F1 by A3,XBOOLE_0:def 4;
then
ex f1 be Function of X\/{z},{x,y} st x1=f1 & card (f1"{x })=k+1 & f1.z =x;
hence thesis by A1,A4;
end;
A5: F2 c=Choose(X\/{z},k+1,x,y)
proof
let x1 be object;
assume x1 in F2;
then
ex f be Function of X\/{z},{x,y} st x1=f & card (f"{x})=k+1 & f.z=y;
hence thesis by Def1;
end;
A6: Choose(X\/{z},k+1,x,y) c= F1\/F2
proof
let x1 be object;
assume x1 in Choose(X\/{z},k+1,x,y);
then consider f be Function of X\/{z},{x,y} such that
A7: f=x1 & card (f"{x})=k+1 by Def1;
z in {z} by TARSKI:def 1;
then
A8: z in X\/{z} by XBOOLE_0:def 3;
dom f=X\/{z} by FUNCT_2:def 1;
then f.z in rng f by A8,FUNCT_1:def 3;
then f.z=x or f.z=y by TARSKI:def 2;
then x1 in F1 or x1 in F2 by A7;
hence thesis by XBOOLE_0:def 3;
end;
F1 c=Choose(X\/{z},k+1,x,y)
proof
let x1 be object;
assume x1 in F1; then
ex f be Function of X\/{z},{x,y} st x1=f & card (f"{x})=k+1 & f.z=x;
hence thesis by Def1;
end;
then F1\/F2 c= Choose(X\/{z},k+1,x,y) by A5,XBOOLE_1:8;
hence thesis by A6,A2;
end;
theorem Th14:
for z,x,y being object holds
x<>y & not z in X implies card Choose(X\/{z},k+1,x,y)= card
Choose(X,k+1,x,y)+ card Choose(X,k,x,y)
proof let z,x,y be object;
assume that
A1: x<>y and
A2: not z in X;
set F2={f where f is Function of X\/{z},{x,y}:card (f"{x})=k+1 & f.z=y};
set F1={f where f is Function of X\/{z},{x,y}:card (f"{x})=k+1 & f.z=x};
A3: F1 \/F2= Choose(X\/{z},k+1,x,y) by A1,Lm1;
F1 c= F1\/F2 & F2 c= F1\/F2 by XBOOLE_1:7;
then reconsider F1,F2 as finite set by A3;
A4: card F1=card Choose(X,k,x,y) by A2,Th12;
card (F1 \/ F2) = card F1 + card F2 & card F2=card Choose(X,k+1,x,y)
by A1,A2
,Lm1,Th13,CARD_2:40;
hence thesis by A1,A4,Lm1;
end;
:: n choose k
::$N Formula for the Number of Combinations
::$L https://en.wikipedia.org/wiki/Combination Formula for the Number of Combinations
theorem Th15:
for x,y being object holds
x<>y implies card Choose(X,k,x,y)=card X choose k
proof let x,y be object;
defpred P[Nat] means for k,X st k+ card X <= $1 holds card Choose
(X,k,x,y)=(card X) choose k;
assume
A1: x<>y;
A2: for n st P[n] holds P[n+1]
proof
let n such that
A3: P[n];
let k,X such that
A4: k+ card X <= n+1;
per cases by A4,XXREAL_0:1;
suppose
k+ card X < n+1;
then k+card X<=n by NAT_1:13;
hence thesis by A3;
end;
suppose
A5: k+ card X = n+1;
per cases;
suppose
A6: k=0 & card X>=0;
then card Choose(X,k,x,y)=1 by A1,Th10;
hence thesis by A6,NEWTON:19;
end;
suppose
A7: k>0 & card X=0;
then Choose(X,k,x,y) is empty by Th9;
hence thesis by A7,NEWTON:def 3;
end;
suppose
A8: k>0 & card X>0;
then reconsider cXz=(card X)-1 as Element of NAT by NAT_1:20;
reconsider k1=k-1 as Element of NAT by A8,NAT_1:20;
consider z being object such that
A9: z in X by A8,CARD_1:27,XBOOLE_0:def 1;
set Xz=X\{z};
z in {z} by TARSKI:def 1;
then
A10: not z in Xz by XBOOLE_0:def 5;
Xz\/{z}=X by A9,ZFMISC_1:116;
then
A11: card Choose(X,k1+1,x,y)= card Choose(Xz,k1+1,x,y)+ card Choose(Xz
,k1,x, y) by A1,A10,Th14;
card X=cXz+1;
then
A12: card Xz=cXz by A9,STIRL2_1:55;
cXz< cXz+1 by NAT_1:13;
then
A13: card Xz < card X by A9,STIRL2_1:55;
then k+card Xz<n+1 by A5,XREAL_1:8;
then k+card Xz<=n by NAT_1:13;
then
A14: card Choose(Xz,k1+1,x,y)=(card Xz) choose (k1+1) by A3;
k1<k1+1 by NAT_1:13;
then k1+card Xz<n+1 by A5,A13,XREAL_1:8;
then k1+card Xz<=n by NAT_1:13;
then
A15: card Choose(Xz,k1,x,y)=(card Xz) choose k1 by A3;
card X=cXz+1;
hence thesis by A14,A15,A11,A12,NEWTON:22;
end;
end;
end;
A16: P[0]
proof
let k,X;
A17: 0 choose 0 = 1 by NEWTON:19;
assume k+ card X <= 0;
then k+ card X =0 & card X=0;
hence thesis by A1,Th10,A17;
end;
for n holds P[n] from NAT_1:sch 2(A16,A2);
then P[k+card X];
hence thesis;
end;
theorem Th16:
for x,y being object holds
x<>y implies (Y-->y)+*(X-->x) in Choose(X\/Y,card X,x,y)
proof let x,y be object;
set F=(Y-->y)+*(X-->x);
dom (Y-->y)=Y & dom (X-->x)=X;
then
A1: dom F=X\/Y by FUNCT_4:def 1;
{y} c= {x,y} by ZFMISC_1:7;
then
A2: rng (Y-->y) c= {x,y};
{x} c= {x,y} by ZFMISC_1:7;
then rng (X-->x)c= {x,y};
then rng F c= rng(X-->x)\/rng(Y-->y) & rng(X-->x)\/rng(Y-->y)c={x,y} by A2,
FUNCT_4:17,XBOOLE_1:8;
then reconsider F as Function of X\/Y,{x,y} by A1,FUNCT_2:2,XBOOLE_1:1;
assume
A3: x<>y;
A4: F"{x}c=X
proof
let z be object such that
A5: z in F"{x};
A6: z in X or z in Y by A5,XBOOLE_0:def 3;
F.z in {x} by A5,FUNCT_1:def 7;
then
A7: F.z=x by TARSKI:def 1;
z in dom F by A5,FUNCT_1:def 7;
then
A8: z in dom (X-->x)\/dom (Y-->y);
assume
A9: not z in X;
F.z=(Y-->y).z by A9,A8,FUNCT_4:def 1;
hence contradiction by A3,A9,A6,A7,FUNCOP_1:7;
end;
X c= F"{x}
proof
let z be object such that
A10: z in X;
A11: z in dom F by A1,A10,XBOOLE_0:def 3;
z in dom (X-->x) by A10;
then
A12: F.z=(X-->x).z by FUNCT_4:13;
(X-->x).z=x by A10,FUNCOP_1:7;
then F.z in {x} by A12,TARSKI:def 1;
hence thesis by A11,FUNCT_1:def 7;
end;
then X=F"{x} by A4;
hence thesis by Def1;
end;
theorem Th17:
x<>y & X misses Y implies (X-->x)+*(Y-->y) in Choose(X\/Y,card X ,x,y)
proof
assume that
A1: x<>y and
A2: X misses Y;
dom (X-->x)=X & dom (Y-->y)=Y;
then (X-->x)+*(Y-->y)=(Y-->y)+*(X-->x) by A2,FUNCT_4:35;
hence thesis by A1,Th16;
end;
definition
let F,Ch be Function,y be object;
func Intersection(F,Ch,y) -> Subset of union rng F means
:Def2:
z in it iff z in union rng F & for x st x in dom Ch & Ch.x=y holds z in F.x;
existence
proof
defpred P[object] means for x st x in dom Ch & Ch.x=y holds $1 in F.x;
consider I be set such that
A1: for z being object holds z in I iff z in union rng F & P[z]
from XBOOLE_0:sch 1;
I c= union rng F
by A1;
then reconsider I as Subset of union rng F;
take I;
thus thesis by A1;
end;
uniqueness
proof
let I1,I2 be Subset of union rng F such that
A2: z in I1 iff z in union rng F & for x st x in dom Ch & Ch.x=y holds
z in F.x and
A3: z in I2 iff z in union rng F & for x st x in dom Ch & Ch.x=y holds
z in F.x;
for z being object holds z in I1 iff z in I2
proof let z be object;
z in I1 iff z in union rng F & for x st x in dom Ch & Ch.x=y holds z
in F.x by A2;
hence thesis by A3;
end;
hence thesis by TARSKI:2;
end;
end;
reserve F,Ch for Function;
theorem Th18:
for F,Ch st dom F/\Ch"{x} is non empty holds y in Intersection(F
,Ch,x) iff for z st z in dom Ch & Ch.z=x holds y in F.z
proof
let F,Ch such that
A1: dom F/\Ch"{x} is non empty;
thus y in Intersection(F,Ch,x) implies for z st z in dom Ch & Ch.z=x holds y
in F.z by Def2;
thus (for z st z in dom Ch & Ch.z=x holds y in F.z) implies y in
Intersection(F,Ch,x)
proof
consider z being object such that
A2: z in dom F/\Ch"{x} by A1;
A3: z in Ch"{x} by A2,XBOOLE_0:def 4;
then Ch.z in {x} by FUNCT_1:def 7;
then
A4: Ch.z=x by TARSKI:def 1;
z in dom F by A2,XBOOLE_0:def 4;
then
A5: F.z in rng F by FUNCT_1:def 3;
assume
A6: for z st z in dom Ch & Ch.z=x holds y in F.z;
z in dom Ch by A3,FUNCT_1:def 7;
then y in F.z by A6,A4;
then y in union rng F by A5,TARSKI:def 4;
hence thesis by A6,Def2;
end;
end;
theorem Th19:
Intersection(F,Ch,y) is non empty implies Ch"{y} c= dom F
proof
assume Intersection(F,Ch,y) is non empty;
then consider z being object such that
A1: z in Intersection(F,Ch,y);
assume not Ch"{y} c= dom F;
then consider x being object such that
A2: x in Ch"{y} and
A3: not x in dom F;
Ch.x in {y} by A2,FUNCT_1:def 7;
then
A4: Ch.x=y by TARSKI:def 1;
x in dom Ch by A2,FUNCT_1:def 7;
then z in F.x by A1,A4,Def2;
hence thesis by A3,FUNCT_1:def 2;
end;
theorem
Intersection(F,Ch,y) is non empty implies for x1,x2 st x1 in Ch"{y} &
x2 in Ch"{y} holds F.x1 meets F.x2
proof
assume Intersection(F,Ch,y) is non empty;
then consider z being object such that
A1: z in Intersection(F,Ch,y);
let x1,x2 such that
A2: x1 in Ch"{y} and
A3: x2 in Ch"{y};
Ch.x2 in {y} by A3,FUNCT_1:def 7;
then
A4: Ch.x2=y by TARSKI:def 1;
Ch.x1 in {y} by A2,FUNCT_1:def 7;
then
A5: Ch.x1=y by TARSKI:def 1;
x2 in dom Ch by A3,FUNCT_1:def 7;
then
A6: z in F.x2 by A1,A4,Def2;
x1 in dom Ch by A2,FUNCT_1:def 7;
then z in F.x1 by A1,A5,Def2;
hence thesis by A6,XBOOLE_0:3;
end;
theorem Th21:
z in Intersection(F,Ch,y) & y in rng Ch implies ex x st x in dom
Ch & Ch.x=y & z in F.x
proof
assume that
A1: z in Intersection(F,Ch,y) and
A2: y in rng Ch;
Ch"{y} <> {} by A2,FUNCT_1:72;
then consider x being object such that
A3: x in Ch"{y} by XBOOLE_0:def 1;
Ch.x in {y} by A3,FUNCT_1:def 7;
then
A4: Ch.x=y by TARSKI:def 1;
A5: x in dom Ch by A3,FUNCT_1:def 7;
x in dom Ch by A3,FUNCT_1:def 7;
then z in F.x by A1,A4,Def2;
hence thesis by A4,A5;
end;
theorem
F is empty or union rng F is empty implies Intersection(F,Ch,y)=union
rng F by RELAT_1:38,ZFMISC_1:2;
theorem Th23:
for y being object holds
F|Ch"{y}=(Ch"{y}-->union rng F)
implies Intersection(F,Ch,y) = union rng F
proof let y be object;
set ChF=Ch"{y}-->union rng F;
assume
A1: F|Ch"{y}=ChF;
union rng F c= Intersection(F,Ch,y)
proof
let z be object such that
A2: z in union rng F;
now
let x such that
A3: x in dom Ch and
A4: Ch.x=y;
Ch.x in {y} by A4,TARSKI:def 1;
then
A5: x in Ch"{y} by A3,FUNCT_1:def 7;
then dom ChF= Ch"{y} & ChF.x=union rng F by FUNCOP_1:7;
hence z in F.x by A1,A2,A5,FUNCT_1:47;
end;
hence thesis by A2,Def2;
end;
hence thesis;
end;
theorem
union rng F is non empty & Intersection(F,Ch,y)=union rng F implies F|
Ch"{y}=(Ch"{y}-->union rng F)
proof
set ChF=Ch"{y}-->union rng F;
assume that
A1: union rng F is non empty and
A2: Intersection(F,Ch,y) = union rng F;
A3: dom F/\Ch"{y} =dom (F|Ch"{y}) by RELAT_1:61;
dom F/\Ch"{y}=Ch"{y} by A1,A2,Th19,XBOOLE_1:28;
then
A4: dom (F|Ch"{y})=dom ChF by A3;
assume F|Ch"{y}<>ChF;
then consider x being object such that
A5: x in dom (F|Ch"{y}) and
A6: (F|Ch"{y}).x<>ChF.x by A4;
x in dom F /\ Ch"{y} by A5,RELAT_1:61;
then
A7: x in dom F by XBOOLE_0:def 4;
x in dom F /\ Ch"{y} by A5,RELAT_1:61;
then
A8: x in Ch"{y} by XBOOLE_0:def 4;
then
A9: ChF.x=union rng F by FUNCOP_1:7;
Ch.x in {y} by A8,FUNCT_1:def 7;
then
A10: Ch.x =y by TARSKI:def 1;
F.x=(F|Ch"{y}).x by A5,FUNCT_1:47;
then (F|Ch"{y}).x in rng F by A7,FUNCT_1:def 3;
then (F|Ch"{y}).x c= ChF.x by A9,ZFMISC_1:74;
then not union rng F c= (F|Ch"{y}).x by A6,A9;
then consider z being object such that
A11: z in union rng F and
A12: not z in (F|Ch"{y}).x;
x in dom Ch by A8,FUNCT_1:def 7;
then z in F.x by A2,A11,A10,Def2;
hence thesis by A5,A12,FUNCT_1:47;
end;
theorem Th25:
for y being object holds
Intersection(F,{},y)=union rng F
proof let y be object;
F|({}"{y} qua set)=({}"{y}-->union rng F);
hence thesis by Th23;
end;
theorem Th26:
for y being object holds
Intersection(F,Ch,y) c= Intersection(F,Ch|X9,y)
proof let y be object;
let z be object such that
A1: z in Intersection(F,Ch,y);
now
let x such that
A2: x in dom (Ch|X9) and
A3: Ch|X9.x=y;
x in dom Ch/\X9 by A2,RELAT_1:61;
then
A4: x in dom Ch by XBOOLE_0:def 4;
Ch.x=y by A2,A3,FUNCT_1:47;
hence z in F.x by A1,A4,Def2;
end;
hence thesis by A1,Def2;
end;
theorem Th27:
Ch"{y}=(Ch|X9)"{y} implies Intersection(F,Ch,y)=Intersection(F, Ch|X9,y)
proof
assume
A1: Ch"{y}=(Ch|X9)"{y};
A2: Intersection(F,Ch|X9,y) c=Intersection(F,Ch,y)
proof
let z be object such that
A3: z in Intersection(F,Ch|X9,y);
now
let x such that
A4: x in dom Ch and
A5: Ch.x=y;
Ch.x in {y} by A5,TARSKI:def 1;
then
A6: x in (Ch|X9)"{y} by A1,A4,FUNCT_1:def 7;
then (Ch|X9).x in {y} by FUNCT_1:def 7;
then
A7: (Ch|X9).x = y by TARSKI:def 1;
x in dom (Ch|X9) by A6,FUNCT_1:def 7;
hence z in F.x by A3,A7,Def2;
end;
hence thesis by A3,Def2;
end;
Intersection(F,Ch,y) c= Intersection(F,Ch|X9,y) by Th26;
hence thesis by A2;
end;
theorem Th28:
Intersection(F|X9,Ch,y) c= Intersection(F,Ch,y)
proof
let z be object such that
A1: z in Intersection(F|X9,Ch,y);
A2: now
A3: Ch"{y} c= dom (F|X9) by A1,Th19;
let x such that
A4: x in dom Ch and
A5: Ch.x=y;
Ch.x in {y} by A5,TARSKI:def 1;
then
A6: x in Ch"{y} by A4,FUNCT_1:def 7;
z in F|X9.x by A1,A4,A5,Def2;
hence z in F.x by A6,A3,FUNCT_1:47;
end;
union rng (F|X9) c= union rng F & z in union rng (F|X9) by A1,RELAT_1:70
,ZFMISC_1:77;
hence thesis by A2,Def2;
end;
theorem Th29:
y in rng Ch & Ch"{y} c= X9 implies Intersection(F|X9,Ch,y) =
Intersection(F,Ch,y)
proof
assume that
A1: y in rng Ch and
A2: Ch"{y} c= X9;
A3: Intersection(F,Ch,y) c=Intersection(F|X9,Ch,y)
proof
let z be object such that
A4: z in Intersection(F,Ch,y);
A5: now
let x such that
A6: x in dom Ch and
A7: Ch.x=y;
Ch.x in {y} by A7,TARSKI:def 1;
then
A8: x in Ch"{y} by A6,FUNCT_1:def 7;
z in F.x by A4,A6,A7,Def2;
then x in dom F by FUNCT_1:def 2;
then x in dom F/\X9 by A2,A8,XBOOLE_0:def 4;
then
A9: x in dom (F|X9) by RELAT_1:61;
z in F.x by A4,A6,A7,Def2;
hence z in F|X9.x by A9,FUNCT_1:47;
end;
consider x such that
A10: x in dom Ch and
A11: Ch.x=y and
A12: z in F.x by A1,A4,Th21;
Ch.x in {y} by A11,TARSKI:def 1;
then
A13: x in Ch"{y} by A10,FUNCT_1:def 7;
x in dom F by A12,FUNCT_1:def 2;
then x in dom F/\X9 by A2,A13,XBOOLE_0:def 4;
then x in dom (F|X9) by RELAT_1:61;
then
A14: F|X9.x in rng (F|X9) by FUNCT_1:def 3;
z in F|X9.x by A5,A10,A11;
then z in union rng (F|X9) by A14,TARSKI:def 4;
hence thesis by A5,Def2;
end;
Intersection(F|X9,Ch,y) c=Intersection(F,Ch,y) by Th28;
hence thesis by A3;
end;
theorem Th30:
for x,y being object holds
x in Ch"{y} implies Intersection(F,Ch,y) c= F.x
proof let x,y be object;
assume
A1: x in Ch"{y};
then
A2: x in dom Ch by FUNCT_1:def 7;
Ch.x in {y} by A1,FUNCT_1:def 7;
then
A3: Ch.x=y by TARSKI:def 1;
let z be object;
assume z in Intersection(F,Ch,y);
hence thesis by A2,A3,Def2;
end;
theorem Th31:
for x,y being object holds
x in Ch"{y} implies Intersection(F,Ch|(dom Ch\{x}),y)/\F.x=
Intersection(F,Ch,y)
proof let x,y be object;
set d=dom Ch\{x};
set Chd=Ch|d;
set I1=Intersection(F,Ch,y);
set I2=Intersection(F,Chd,y);
assume x in Ch"{y};
then
A1: I1 c= F.x by Th30;
A2: I2/\F.x c= I1
proof
let z be object such that
A3: z in I2/\F.x;
now
let x1 such that
A4: x1 in dom Ch and
A5: Ch.x1=y;
per cases by A4,XBOOLE_0:def 5;
suppose
A6: x1 in d;
A7: z in I2 by A3,XBOOLE_0:def 4;
A8: dom Ch/\d= dom Chd & dom Ch/\d =d by RELAT_1:61,XBOOLE_1:28;
then Chd.x1=y by A5,A6,FUNCT_1:47;
hence z in F.x1 by A6,A8,A7,Def2;
end;
suppose
x1 in {x};
then x1=x by TARSKI:def 1;
hence z in F.x1 by A3,XBOOLE_0:def 4;
end;
end;
hence thesis by A3,Def2;
end;
I1 c= I2 by Th26;
then I1 c= I2/\F.x by A1,XBOOLE_1:19;
hence thesis by A2;
end;
theorem Th32:
for x1,x2 being object
for Ch1,Ch2 be Function st Ch1"{x1}=Ch2"{x2} holds Intersection(
F,Ch1,x1)=Intersection(F,Ch2,x2)
proof let x1,x2 be object;
let Ch1,Ch2 be Function such that
A1: Ch1"{x1}=Ch2"{x2};
thus Intersection(F,Ch1,x1)c=Intersection(F,Ch2,x2)
proof
let z be object such that
A2: z in Intersection(F,Ch1,x1);
now
let x such that
A3: x in dom Ch2 and
A4: Ch2.x=x2;
Ch2.x in {x2} by A4,TARSKI:def 1;
then
A5: x in Ch1"{x1} by A1,A3,FUNCT_1:def 7;
then Ch1.x in {x1} by FUNCT_1:def 7;
then
A6: Ch1.x=x1 by TARSKI:def 1;
x in dom Ch1 by A5,FUNCT_1:def 7;
hence z in F.x by A2,A6,Def2;
end;
hence thesis by A2,Def2;
end;
thus Intersection(F,Ch2,x2)c=Intersection(F,Ch1,x1)
proof
let z be object such that
A7: z in Intersection(F,Ch2,x2);
now
let x such that
A8: x in dom Ch1 and
A9: Ch1.x=x1;
Ch1.x in {x1} by A9,TARSKI:def 1;
then
A10: x in Ch2"{x2} by A1,A8,FUNCT_1:def 7;
then Ch2.x in {x2} by FUNCT_1:def 7;
then
A11: Ch2.x=x2 by TARSKI:def 1;
x in dom Ch2 by A10,FUNCT_1:def 7;
hence z in F.x by A7,A11,Def2;
end;
hence thesis by A7,Def2;
end;
end;
theorem Th33:
for y being object holds
Ch"{y}={} implies Intersection(F,Ch,y)=union rng F
proof let y be object;
reconsider E ={} as set;
A1: Ch|E={} & Intersection(F,{},y)=union rng F by Th25;
assume Ch"{y}={};
then (Ch|E)"{y} = Ch"{y};
hence thesis by A1,Th32;
end;
theorem Th34:
for x,y being object holds
{x}=Ch"{y} implies Intersection(F,Ch,y)=F.x
proof let x,y be object;
A1: (dom Ch\{x}) misses {x} by XBOOLE_1:79;
assume
A2: {x}=Ch"{y};
then (Ch|(dom Ch\{x}))"{y}=(dom Ch\{x}) /\ {x} by FUNCT_1:70;
then (Ch|(dom Ch\{x}))"{y}={} by A1;
then
A3: Intersection(F,Ch|(dom Ch\{x}),y)=union rng F by Th33;
x in Ch"{y} by A2,TARSKI:def 1;
then
A4: union rng F/\F.x=Intersection(F,Ch,y) by A3,Th31;
per cases;
suppose
x in dom F;
then F.x in rng F by FUNCT_1:def 3;
hence thesis by A4,XBOOLE_1:28,ZFMISC_1:74;
end;
suppose
not x in dom F;
then F.x={} by FUNCT_1:def 2;
hence thesis by A4;
end;
end;
theorem Th35:
{x1,x2}=Ch"{y} implies Intersection(F,Ch,y)=F.x1 /\ F.x2
proof
assume
A1: {x1,x2}=Ch"{y};
per cases;
suppose
A2: x1=x2;
then Ch"{y}={x1} by A1,ENUMSET1:29;
hence thesis by A2,Th34;
end;
suppose
A3: x1<>x2;
Ch"{y}/\(dom Ch\{x1})=(Ch"{y}/\dom Ch)\{x1} & Ch"{y}/\dom Ch={x1,x2}
by A1,RELAT_1:132,XBOOLE_1:28,49;
then Ch"{y}/\(dom Ch\{x1})={x2} by A3,ZFMISC_1:17;
then
A4: (Ch|(dom Ch\{x1}))"{y}={x2} by FUNCT_1:70;
x1 in Ch"{y} by A1,TARSKI:def 2;
then Intersection(F,Ch|(dom Ch\{x1}),y)/\F.x1=Intersection(F,Ch,y) by Th31;
hence thesis by A4,Th34;
end;
end;
theorem
for F st F is non empty holds y in Intersection(F,(dom F-->x),x) iff
for z st z in dom F holds y in F.z
proof
let F such that
A1: F is non empty;
set Ch=dom F-->x;
thus y in Intersection(F,Ch,x) implies for z st z in dom F holds y in F.z
proof
assume
A2: y in Intersection(F,Ch,x);
let z;
assume z in dom F;
then z in dom Ch & Ch.z=x by FUNCOP_1:7;
hence thesis by A2,Def2;
end;
Ch"{x}=dom F by FUNCOP_1:15;
then
A3: dom F/\Ch"{x}=dom F;
assume for z st z in dom F holds y in F.z;
then for z st z in dom Ch & Ch.z=x holds y in F.z;
hence thesis by A1,A3,Th18;
end;
registration
let F be finite-yielding Function,X be set;
cluster F|X -> finite-yielding;
coherence
proof
let x be object;
assume
x in dom (F|X);
then (F|X).x=F.x by FUNCT_1:47;
hence thesis;
end;
end;
registration
let F be finite-yielding Function,G be Function;
cluster F*G -> finite-yielding;
coherence
proof
let x be object;
assume
x in dom (F*G);
then (F*G).x =F.(G.x) by FUNCT_1:12;
hence thesis;
end;
cluster Intersect(F,G) -> finite-yielding;
coherence
proof
let x be object;
assume
x in dom Intersect(F,G);
then x in (dom F)/\(dom G) by YELLOW20:def 2;
then Intersect(F,G).x=F.x/\G.x by YELLOW20:def 2;
hence thesis;
end;
end;
reserve Fy for finite-yielding Function;
theorem
y in rng Ch implies Intersection(Fy,Ch,y) is finite
proof
assume y in rng Ch;
then consider x being object such that
A1: x in dom Ch and
A2: Ch.x=y by FUNCT_1:def 3;
Ch.x in {y} by A2,TARSKI:def 1;
then x in Ch"{y} by A1,FUNCT_1:def 7;
then Intersection(Fy,Ch,y) c= Fy.x by Th30;
hence thesis;
end;
theorem Th38:
dom Fy is finite implies union rng Fy is finite
proof
assume dom Fy is finite;
then rng Fy is finite by FINSET_1:8;
hence thesis;
end;
theorem
x in Choose(n,k,1,0) iff ex F be XFinSequence of NAT st F = x & dom F
= n & rng F c= {0,1} & Sum F=k
proof
thus x in Choose(n,k,1,0) implies ex F be XFinSequence of NAT st F = x & dom
F = n & rng F c= {0,1} & Sum F=k
proof
assume x in Choose(n,k,1,0);
then consider F be Function of n,{0,1} such that
A1: x=F & card (F"{1})=k by Def1;
A2: rng F c= {0,1};
dom F=n by FUNCT_2:def 1;
then reconsider F as XFinSequence by AFINSQ_1:5;
rng F is Subset of NAT by A2,XBOOLE_1:1;
then reconsider F as XFinSequence of NAT by RELAT_1:def 19;
take F;
Sum F= 1*card (F"{1}) by A2,AFINSQ_2:68;
hence thesis by A1,A2,FUNCT_2:def 1;
end;
given F be XFinSequence of NAT such that
A3: F = x and
A4: dom F = n & rng F c= {0,1} & Sum F=k;
1*card (F"{1})=k & F is Function of n,{0,1} by A4,AFINSQ_2:68,FUNCT_2:2;
hence thesis by A3,Def1;
end;
Lm2: ex P be Function of card X,X st P is one-to-one
proof
card X,X are_equipotent by CARD_1:def 2;
then consider P be Function such that
A1: P is one-to-one and
A2: dom P=card X & rng P=X by WELLORD2:def 4;
P is Function of card X,X by A2,FUNCT_2:1;
hence thesis by A1;
end;
definition
::$CD
let k;
let F be finite-yielding Function;
assume
A1: dom F is finite;
func Card_Intersection(F,k) -> Element of NAT means
:Def3:
for x,y be object,X
be finite set, P be Function of card Choose(X,k,x,y),Choose(X,k,x,y) st dom F=X
& P is one-to-one & x<>y ex XFS be XFinSequence of NAT st dom XFS=dom P & (for
z,f st z in dom XFS & f=P.z holds XFS.z=card(Intersection(F,f,x))) & it=Sum XFS
;
existence
proof
reconsider D=dom F as finite set by A1;
set Ch1=Choose(D,k,0,1);
card Ch1,Ch1 are_equipotent by CARD_1:def 2;
then consider P1 be Function such that
A2: P1 is one-to-one and
A3: dom P1=card Ch1 and
A4: rng P1=Ch1 by WELLORD2:def 4;
reconsider P1 as Function of card Ch1,Ch1 by A3,A4,FUNCT_2:1;
defpred xfs1[object,object] means
for f st f=P1.$1 holds $2=card Intersection(F,f,0);
A5: for x being object st x in card Ch1 ex y being object st
y in NAT & xfs1[x,y]
proof
let x be object;
assume x in card Ch1;
then x in dom P1 by CARD_1:27,FUNCT_2:def 1;
then P1.x in rng P1 by FUNCT_1:def 3;
then consider f be Function of D,{0,1} such that
A6: f = P1.x and
card (f"{0}) = k by Def1;
union rng F is finite by A1,Th38;
then reconsider I=Intersection(F,f,0) as finite set;
take card I;
thus thesis by A6;
end;
consider XFS1 be Function of card Ch1,NAT such that
A7: for x being object st x in card Ch1 holds xfs1[x,XFS1.x]
from FUNCT_2:sch 1(A5);
A8: dom XFS1 =card Ch1 by FUNCT_2:def 1;
then reconsider XFS1 as XFinSequence by AFINSQ_1:5;
reconsider XFS1 as XFinSequence of NAT;
reconsider S=Sum XFS1 as Element of NAT by ORDINAL1:def 12;
take S;
let x,y be object,X be finite set, P be Function of card Choose(X,k,x,y),
Choose(X,k,x,y) such that
A9: dom F=X and
A10: P is one-to-one and
A11: x<>y;
defpred perm[object,object] means for f1 be Function of D,{0,1},
f be Function of
X,{x,y} st f1=P1.$1 & f=P.$2 holds f1"{0}=f"{x} & for z st z in X holds (f1.z=0
iff f.z=x)&(f1.z=1 iff f.z=y);
set Ch=Choose(X,k,x,y);
A12: for x1 being object st x1 in card Ch1
ex x2 being object st x2 in card Ch1 & perm[x1,x2]
proof
card card Choose(X,k,x,y)=card Choose(X,k,x,y);
then P is onto by A10,FINSEQ_4:63;
then
A13: rng P=Ch by FUNCT_2:def 3;
let x1 be object;
assume x1 in card Ch1;
then P1.x1 in rng P1 by A3,FUNCT_1:def 3;
then consider f1 be Function of D,{0,1} such that
A14: f1=P1.x1 and
A15: card (f1"{0})=k by Def1;
defpred pf[object,object] means (f1.$1=0 iff $2=x)&(f1.$1=1 iff $2=y);
A16: for d be object st d in X ex fd be object st fd in {x,y} & pf[d,fd]
proof
let d be object;
assume d in X;
then d in dom f1 by A9,FUNCT_2:def 1;
then f1.d in rng f1 by FUNCT_1:def 3;
then
A17: f1.d=0 or f1.d=1 by TARSKI:def 2;
x in {x,y} & y in {x,y} by TARSKI:def 2;
hence thesis by A11,A17;
end;
consider f be Function of X,{x,y} such that
A18: for d be object st d in X holds pf[d,f.d] from FUNCT_2:sch 1(A16);
A19: dom f1=D by FUNCT_2:def 1;
A20: f1"{0}c=f"{x}
proof
let z be object;
assume
A21: z in f1"{0};
then f1.z in {0} by FUNCT_1:def 7;
then
A22: f1.z=0 by TARSKI:def 1;
A23: dom f1=dom f by A9,A19,FUNCT_2:def 1;
then z in dom f by A19,A21;
then f.z=x by A18,A22;
then f.z in {x} by TARSKI:def 1;
hence thesis by A19,A21,A23,FUNCT_1:def 7;
end;
A24: f"{x}c=f1"{0}
proof
let z be object;
assume
A25: z in f"{x};
then f.z in {x} by FUNCT_1:def 7;
then f.z=x by TARSKI:def 1;
then f1.z=0 by A18,A25;
then f1.z in {0} by TARSKI:def 1;
hence thesis by A9,A19,A25,FUNCT_1:def 7;
end;
then f"{x}=f1"{0} by A20;
then f in Ch by A15,Def1;
then consider x2 being object such that
A26: x2 in dom P and
A27: P.x2=f by A13,FUNCT_1:def 3;
reconsider x2 as set by TARSKI:1;
take x2;
card Ch=card X choose k & card Ch1 = card D choose k by A11,Th15;
hence x2 in card Ch1 by A9,A26;
let f19 be Function of D,{0,1},f9 be Function of X,{x,y} such that
A28: f19=P1.x1 & f9=P.x2;
thus f9"{x}=f19"{0} by A14,A24,A20,A27,A28;
let z;
assume z in X;
hence thesis by A14,A18,A27,A28;
end;
consider Perm be Function of card Ch1,card Ch1 such that
A29: for x1 being object st x1 in card Ch1 holds perm[x1,Perm.x1]
from FUNCT_2:sch 1(A12);
now
A30: Ch={} implies card Ch={};
let z1,z2 be object such that
A31: z1 in dom Perm and
A32: z2 in dom Perm and
A33: Perm.z1 = Perm.z2;
A34: card X = card D by A9;
card Ch=card X choose k & card Ch1=card D choose k by A11,Th15;
then card Ch1 = card Ch by A34;
then Perm.z1 in card Ch by A31,FUNCT_2:5;
then Perm.z1 in dom P by A30,FUNCT_2:def 1;
then P.(Perm.z1) in rng P by FUNCT_1:def 3;
then consider PPermz1 be Function of X,{x,y} such that
A35: PPermz1=P.(Perm.z1) and
card(PPermz1"{x})=k by Def1;
P1.z2 in rng P1 by A3,A32,FUNCT_1:def 3;
then consider P1z2 be Function of D,{0,1} such that
A36: P1.z2=P1z2 and
card (P1z2"{0})=k by Def1;
P1.z1 in rng P1 by A3,A31,FUNCT_1:def 3;
then consider P1z1 be Function of D,{0,1} such that
A37: P1.z1=P1z1 and
card (P1z1"{0})=k by Def1;
A38: for z being object st z in dom P1z1 holds P1z1.z=P1z2.z
proof
let z be object such that
A39: z in dom P1z1;
A40: P1z1.z in rng P1z1 by A39,FUNCT_1:def 3;
per cases by A40,TARSKI:def 2;
suppose
A41: P1z1.z=0;
then PPermz1.z=x by A9,A29,A31,A37,A35,A39;
hence thesis by A9,A29,A32,A33,A36,A35,A39,A41;
end;
suppose
A42: P1z1.z=1;
then PPermz1.z=y by A9,A29,A31,A37,A35,A39;
hence thesis by A9,A29,A32,A33,A36,A35,A39,A42;
end;
end;
dom P1z1=D & dom P1z2=D by FUNCT_2:def 1;
then P1z1=P1z2 by A38;
hence z1=z2 by A2,A3,A31,A32,A37,A36;
end;
then
A43: Perm is one-to-one;
card card Ch1=card card Ch1;
then
A44: Perm is one-to-one onto by A43,FINSEQ_4:63;
defpred xfs[object,object] means
for f st f=P.$1 holds $2=card Intersection(F,f,x);
A45: for x1 being object st x1 in card Ch
ex x2 being object st x2 in NAT & xfs[x1,x2]
proof
let x1 be object;
assume x1 in card Ch;
then x1 in dom P by CARD_1:27,FUNCT_2:def 1;
then P.x1 in rng P by FUNCT_1:def 3;
then consider f be Function of X,{x,y} such that
A46: f = P.x1 and
card (f"{x}) = k by Def1;
union rng F is finite by A1,Th38;
then reconsider I=Intersection(F,f,x) as finite set;
take card I;
thus thesis by A46;
end;
consider XFS be Function of card Ch,NAT such that
A47: for x1 being object st x1 in card Ch holds xfs[x1,XFS.x1]
from FUNCT_2:sch 1(A45);
A48: dom XFS =card Ch by FUNCT_2:def 1;
then reconsider XFS as XFinSequence by AFINSQ_1:5;
reconsider XFS as XFinSequence of NAT;
take XFS;
Ch={} implies card Ch={};
then dom P=card Ch by FUNCT_2:def 1;
hence
A49: dom XFS=dom P by FUNCT_2:def 1;
hence
for z,f st z in dom XFS & f=P.z holds XFS.z=card(Intersection(F,f,x))
by A47;
A50: card Ch1=card D choose k by Th15;
A51: card Ch=card X choose k by A11,Th15;
then card Ch1=dom XFS by A9,A50,FUNCT_2:def 1;
then reconsider Perm as Permutation of dom XFS by A44;
A52: dom XFS=dom XFS1 by A9,A48,A50,A51,FUNCT_2:def 1;
A53: for z being object st z in dom XFS1 holds XFS1.z =(XFS*Perm).z
proof
let z being object such that
A54: z in dom XFS1;
A55: z in dom Perm by A8,A54,FUNCT_2:52;
A56: Perm.z in dom XFS by A52,A54,FUNCT_2:5;
then P.(Perm.z) in rng P by A49,FUNCT_1:def 3;
then consider p be Function of X,{x,y} such that
A57: p=P.(Perm.z) and
card (p"{x})=k by Def1;
A58: XFS.(Perm.z)=card Intersection(F,p,x) by A47,A48,A57,A56;
P1.z in rng P1 by A3,A8,A54,FUNCT_1:def 3;
then consider p1 be Function of D,{0,1} such that
A59: p1=P1.z and
card (p1"{0})=k by Def1;
p1"{0}=p"{x} by A8,A29,A54,A57,A59;
then
A60: Intersection(F,p1,0)=Intersection(F,p,x) by Th32;
XFS1.z=card Intersection(F,p1,0) by A7,A8,A54,A59;
hence thesis by A60,A58,A55,FUNCT_1:13;
end;
rng Perm c= dom XFS & dom Perm=dom XFS by FUNCT_2:52;
then dom XFS1=dom (XFS*Perm) by A52,RELAT_1:27;
then XFS1=XFS*Perm by A53;
then
A61: addnat "**" XFS=addnat "**" XFS1 by AFINSQ_2:45;
addnat "**" XFS1=Sum XFS1 by AFINSQ_2:51;
hence thesis by A61,AFINSQ_2:51;
end;
uniqueness
proof
reconsider D=dom F as finite set by A1;
let n1,n2 be Element of NAT such that
A62: for x,y be object,X be finite set, P be Function of card Choose(X,k
,x,y),Choose(X,k,x,y) st dom F=X & P is one-to-one & x<>y ex XFS be
XFinSequence of NAT st dom XFS=dom P & (for z,f st z in dom XFS & f=P.z holds
XFS.z=card(Intersection(F,f,x))) & n1=Sum XFS and
A63: for x,y be object,X be finite set, P be Function of card Choose(X,k
,x,y),Choose(X,k,x,y) st dom F=X & P is one-to-one & x<>y ex XFS be
XFinSequence of NAT st dom XFS=dom P & (for z,f st z in dom XFS & f=P.z holds
XFS.z=card(Intersection(F,f,x))) & n2=Sum XFS;
set Ch1=Choose(D,k,0,1);
card Ch1,Ch1 are_equipotent by CARD_1:def 2;
then consider P be Function such that
A64: P is one-to-one and
A65: dom P=card Ch1 & rng P=Ch1 by WELLORD2:def 4;
reconsider P as Function of card Ch1,Ch1 by A65,FUNCT_2:1;
consider XFS1 be XFinSequence of NAT such that
A66: dom XFS1=dom P and
A67: for z,f st z in dom XFS1 & f=P.z holds XFS1.z=card(Intersection(
F,f,0)) and
A68: n1=Sum XFS1 by A62,A64;
consider XFS2 be XFinSequence of NAT such that
A69: dom XFS2=dom P and
A70: for z,f st z in dom XFS2 & f=P.z holds XFS2.z=card(Intersection(
F,f,0)) and
A71: n2=Sum XFS2 by A63,A64;
now
let z be object such that
A72: z in dom XFS1;
P.z in rng P by A66,A72,FUNCT_1:def 3;
then consider Pz be Function of D,{0,1} such that
A73: Pz=P.z and
card (Pz"{0})=k by Def1;
XFS2.z=card(Intersection(F,Pz,0)) by A66,A69,A70,A72,A73;
hence XFS2.z=XFS1.z by A67,A72,A73;
end;
hence thesis by A66,A68,A69,A71,FUNCT_1:2;
end;
end;
theorem
for x,y be set,X be finite set, P be Function of card Choose(X,k,x,y),
Choose(X,k,x,y) st dom Fy=X & P is one-to-one & x<>y for XFS be XFinSequence of
NAT st dom XFS=dom P & (for z,f st z in dom XFS & f=P.z holds XFS.z=card(
Intersection(Fy,f,x))) holds Card_Intersection(Fy,k)=Sum XFS
proof
let x,y be set,X be finite set, P be Function of card Choose(X,k,x,y),Choose
(X,k,x,y);
assume dom Fy=X & P is one-to-one & x<>y;
then consider XFS be XFinSequence of NAT such that
A1: dom XFS=dom P and
A2: for z,f st z in dom XFS & f=P.z holds XFS.z=card(Intersection(Fy,f,x )) and
A3: Card_Intersection(Fy,k)=Sum XFS by Def3;
let XFS1 be XFinSequence of NAT such that
A4: dom XFS1=dom P and
A5: for z,f st z in dom XFS1 & f=P.z holds XFS1.z=card(Intersection(Fy,f ,x));
now
let z be object such that
A6: z in dom XFS;
P.z in rng P by A1,A6,FUNCT_1:def 3;
then consider Pz be Function of X,{x,y} such that
A7: Pz=P.z and
card (Pz"{x})=k by Def1;
XFS1.z=card(Intersection(Fy,Pz,x)) by A4,A5,A1,A6,A7;
hence XFS1.z=XFS.z by A2,A6,A7;
end;
hence thesis by A4,A1,A3,FUNCT_1:2;
end;
theorem
dom Fy is finite & k=0 implies Card_Intersection(Fy,k)=card (union rng Fy)
proof
assume that
A1: dom Fy is finite and
A2: k=0;
reconsider X=dom Fy as finite set by A1;
set Ch=Choose(X,k,0,1);
consider P be Function of card Ch,Ch such that
A3: P is one-to-one by Lm2;
A4: card Ch=1 by A2,Th10;
then
A5: dom P=1 by CARD_1:27,FUNCT_2:def 1;
consider XFS be XFinSequence of NAT such that
A6: dom XFS=dom P and
A7: for z,f st z in dom XFS & f=P.z holds XFS.z=card(Intersection(Fy,f,0 )) and
A8: Card_Intersection(Fy,k)=Sum XFS by A3,Def3;
len XFS=1 by A6,A4,CARD_1:27,FUNCT_2:def 1;
then XFS=<%XFS.0%> by AFINSQ_1:34;
then
A9: addnat "**" XFS=XFS.0 by AFINSQ_2:37;
A10: 0 in 1 by CARD_1:49,TARSKI:def 1;
then P.0 in rng P by A5,FUNCT_1:def 3;
then consider P0 be Function of X,{0,1} such that
A11: P0=P.0 and
A12: card (P0"{0})=0 by A2,Def1;
P0"{0}={} by A12;
then
A13: Intersection(Fy,P0,0)=union rng Fy by Th33;
XFS.0=card(Intersection(Fy,P0,0)) by A6,A7,A5,A10,A11;
hence thesis by A8,A13,A9,AFINSQ_2:51;
end;
theorem Th42:
dom Fy=X & k > card X implies Card_Intersection(Fy,k)=0
proof
assume that
A1: dom Fy=X and
A2: k > card X;
set Ch=Choose(X,k,0,1);
consider P be Function of card Ch,Ch such that
A3: P is one-to-one by Lm2;
consider XFS be XFinSequence of NAT such that
A4: dom XFS=dom P and
for z,f st z in dom XFS & f=P.z holds XFS.z=card(Intersection(Fy,f,0)) and
A5: Card_Intersection(Fy,k)=Sum XFS by A1,A3,Def3;
Ch is empty by A2,Th9;
then XFS=0 by A4;
hence thesis by A5;
end;
theorem Th43:
for Fy,X st dom Fy=X for P be Function of card X,X st P is
one-to-one holds ex XFS be XFinSequence of NAT st dom XFS=card X & (for z st z
in dom XFS holds XFS.z=card ((Fy*P).z))& Card_Intersection(Fy,1)=Sum XFS
proof
let Fy,X such that
A1: dom Fy=X;
let P be Function of card X,X such that
A2: P is one-to-one;
per cases;
suppose
A3: X ={};
reconsider XFS={} as XFinSequence;
reconsider XFS as XFinSequence of NAT;
take XFS;
thus card X=dom XFS & for z st z in dom XFS holds XFS.z=card ((Fy*P).z) by
A3;
Sum XFS=0;
hence thesis by A1,A3,Th42,CARD_1:27;
end;
suppose
X <>{};
then reconsider cX=card X as non empty set;
deffunc xfs(Element of cX)=card ((Fy*P).$1);
consider XFS be Function of cX,NAT such that
A4: for x be Element of cX holds XFS.x = xfs(x) from FUNCT_2:sch 4;
A5: dom XFS=cX by FUNCT_2:def 1;
then reconsider XFS as XFinSequence by AFINSQ_1:5;
reconsider XFS as XFinSequence of NAT;
take XFS;
thus card X=dom XFS by FUNCT_2:def 1;
thus for z st z in dom XFS holds XFS.z=card ((Fy*P).z) by A4,A5;
thus Card_Intersection(Fy,1)=Sum XFS
proof
deffunc p1(object)=(P.$1 .-->0) +* ((X\{P.$1})-->1);
A6: for x being object st x in cX holds p1(x) in Choose(X,1,0,1)
proof
let x be object;
assume x in cX;
then x in dom P by CARD_1:27,FUNCT_2:def 1;
then P.x in rng P by FUNCT_1:def 3;
then
A7: {P.x}\/(X\{P.x})=X by ZFMISC_1:116;
{P.x} misses (X\{P.x}) & card {P.x}=1 by CARD_1:30,XBOOLE_1:79;
hence thesis by A7,Th17;
end;
consider P1 be Function of cX,Choose(X,1,0,1) such that
A8: for z being object st z in cX holds P1.z = p1(z) from FUNCT_2:sch 2(A6);
Choose(X,1,0,1) c= rng P1
proof
card X=card card X;
then
A9: P is onto by A2,FINSEQ_4:63;
let z be object;
assume z in Choose(X,1,0,1);
then consider F be Function of X,{0,1} such that
A10: F=z and
A11: card (F"{0})=1 by Def1;
consider x1 being object such that
A12: F"{0}={x1} by A11,CARD_2:42;
A13: x1 in {x1} by TARSKI:def 1;
then x1 in X by A12;
then x1 in rng P by A9,FUNCT_2:def 3;
then consider x2 being object such that
A14: x2 in dom P and
A15: P.x2=x1 by FUNCT_1:def 3;
A16: P1.x2=F
proof
set F1=(X\{P.x2})-->1;
set F0=P.x2 .-->0;
set P1x=F0+*F1;
A17: {P.x2}\/(X\{P.x2})=X by A12,A13,A15,ZFMISC_1:116;
A18: now
let d be object such that
A19: d in dom F;
now
per cases by A17,A19,XBOOLE_0:def 3;
suppose
A20: d in {P.x2};
A21: {P.x2} misses (X\{P.x2}) by XBOOLE_1:79;
dom F0={P.x2} & dom F1=(X\{P.x2});
then P1x.d=F0.d by A20,A21,FUNCT_4:16;
then
A22: P1x.d=0;
F.d in {0} by A12,A15,A20,FUNCT_1:def 7;
hence P1x.d=F.d by A22,TARSKI:def 1;
end;
suppose
A23: d in X\{P.x2};
then d in dom F1;
then P1x.d=F1.d by FUNCT_4:13;
then
A24: P1x.d=1 by A23,FUNCOP_1:7;
A25: X=dom F by FUNCT_2:def 1;
not d in {x1} by A15,A23,XBOOLE_0:def 5;
then not F.d in {0} by A12,A23,A25,FUNCT_1:def 7;
then
A26: not F.d=0 by TARSKI:def 1;
F.d in rng F by A23,A25,FUNCT_1:def 3;
hence P1x.d=F.d by A24,A26,TARSKI:def 2;
end;
end;
hence P1x.d=F.d;
end;
A27: X=dom F0\/dom F1 by A17;
dom F=X & dom P1x=dom F0\/dom F1 by FUNCT_2:def 1,FUNCT_4:def 1;
then P1x=F by A27,A18;
hence thesis by A8,A14;
end;
card Choose(X,1,0,1)= card X choose 1 by Th15;
then card Choose(X,1,0,1)=cX by NAT_1:14,NEWTON:23;
then dom P1 =cX by CARD_1:27,FUNCT_2:def 1;
hence thesis by A10,A14,A16,FUNCT_1:def 3;
end;
then
A28: Choose(X,1,0,1) = rng P1;
then
A29: P1 is onto by FUNCT_2:def 3;
card Choose(X,1,0,1)= card X choose 1 by Th15;
then
A30: card X=card Choose(X,1,0,1) by A28,NAT_1:14,NEWTON:23;
then reconsider P1 as Function of card Choose(X,1,0,1),Choose(X,1,0,1);
card card X=card X;
then P1 is one-to-one by A29,A30,FINSEQ_4:63;
then consider XFS1 be XFinSequence of NAT such that
A31: dom XFS1=dom P1 and
A32: for z,f st z in dom XFS1 & f=P1.z holds XFS1.z=card(
Intersection(Fy,f,0)) and
A33: Card_Intersection(Fy,1)=Sum XFS1 by A1,Def3;
Choose(X,1,0,1)={} implies card Choose(X,1,0,1)={};
then
A34: dom P1=card Choose(X,1,0,1) by FUNCT_2:def 1;
A35: for z be object st z in dom XFS1 holds XFS1.z=XFS.z
proof
let z be object such that
A36: z in dom XFS1;
p1(z) in Choose(X,1,0,1) by A6,A30,A31,A36;
then consider f be Function of X,{0,1} such that
A37: f=p1(z) and
A38: card (f"{0})=1 by Def1;
consider x1 being object such that
A39: f"{0}={x1} by A38,CARD_2:42;
P1.z=p1(z) by A8,A30,A31,A36;
then
A40: XFS1.z = card(Intersection(Fy,f,0)) by A32,A36,A37;
A41: 0 in {0} by TARSKI:def 1;
A43: P.z in {P.z} by TARSKI:def 1;
A44: P.z in dom (P.z .-->0)\/dom((X\{P.z})-->1 ) by A43,XBOOLE_0:def 3;
( not P.z in X\{P.z})& (P.z .-->0).(P.z)=0 by A43,XBOOLE_0:def 5;
then
A45: p1(z).(P.z)=0 by A44,FUNCT_4:def 1;
P.z in dom p1(z) by A44,FUNCT_4:def 1;
then
A46: P.z in f"{0} by A37,A45,A41,FUNCT_1:def 7;
then P.z=x1 by A39,TARSKI:def 1;
then
A47: card(Intersection(Fy,f,0))=card (Fy.(P.z)) by A39,Th34;
A48: XFS.z=card ((Fy*P).z) by A4,A30,A31,A36;
z in dom P by A30,A31,A34,A36,A46,FUNCT_2:def 1;
hence thesis by A47,A40,A48,FUNCT_1:13;
end;
dom XFS1=dom XFS by A30,A31,A34,FUNCT_2:def 1;
hence thesis by A33,A35,FUNCT_1:def 11;
end;
end;
end;
theorem Th44:
for x being object holds
dom Fy=X implies Card_Intersection(Fy,card X)=card Intersection( Fy,X-->x,x)
proof let x be object;
set Ch=Choose(X,card X,x,{x});
consider P be Function of card Ch,Ch such that
A1: P is one-to-one by Lm2;
S: x in {x} by TARSKI:def 1;
then
reconsider x as set;
not x in x; then
A2: x<>{x} by S;
assume dom Fy=X;
then consider XFS be XFinSequence of NAT such that
A3: dom XFS=dom P and
A4: ( for z,f st z in dom XFS & f=P.z holds XFS.z=card(Intersection(Fy,f
,x)))& Card_Intersection(Fy,card X)=Sum XFS by A1,A2,Def3;
A5: card Ch=1 by Th11;
then consider ch being object such that
A6: Ch={ch} by CARD_2:42;
x in {x} by TARSKI:def 1;
then X\/{}=X & {x}<>x;
then ({}-->{x})+*(X-->x) in Ch by Th16;
then {}+*(X-->x) in Ch;
then X-->x in Ch;
then
A7: X-->x=ch by A6,TARSKI:def 1;
A8: Ch={} implies card Ch={};
then
A9: dom P=card Ch by FUNCT_2:def 1;
then 0 in dom P by A5,CARD_1:49,TARSKI:def 1;
then P.0 in rng P by FUNCT_1:def 3;
then
A10: P.0=ch by A6,TARSKI:def 1;
len XFS=1 by A3,A8,A5,FUNCT_2:def 1;
then XFS=<%XFS.0%> by AFINSQ_1:34;
then addnat "**" XFS=XFS.0 by AFINSQ_2:37;
then
A11: Sum XFS=XFS.0 by AFINSQ_2:51;
0 in dom XFS by A3,A5,A9,CARD_1:49,TARSKI:def 1;
hence thesis by A4,A11,A10,A7;
end;
theorem Th45:
for x being object holds
Fy=x.-->X implies Card_Intersection(Fy,1)=card X
proof let x be object;
assume
A1: Fy=x.-->X;
then
A2: dom Fy={x};
A3: x in {x} by TARSKI:def 1;
then
A4: (x.-->x)"{x}={x} by FUNCOP_1:14;
Fy.x=X by A1,A3,FUNCOP_1:7;
then 1=card {x} & Intersection(Fy,x.-->x,x)=X by A4,Th34,CARD_1:30;
hence thesis by A2,Th44;
end;
theorem
x<>y & Fy=(x,y)-->(X,Y) implies Card_Intersection(Fy,1)=card X + card
Y & Card_Intersection(Fy,2)=card (X/\Y)
proof
assume that
A1: x<>y and
A2: Fy=(x,y)-->(X,Y);
set P=(0,1)-->(x,y);
A3: dom P={0,1} & rng P={x,y} by FUNCT_4:62,64;
card {x,y}=2 by A1,CARD_2:57;
then reconsider P as Function of card {x,y},{x,y} by A3,CARD_1:50,FUNCT_2:1;
A4: card card {x,y}=card {x,y};
A5: P.0=x & Fy.x=X by A1,A2,FUNCT_4:63;
A6: P.1=y & Fy.y=Y by A2,FUNCT_4:63;
A7: dom Fy={x,y} by A2,FUNCT_4:62;
rng P={x,y} by FUNCT_4:64;
then P is onto by FUNCT_2:def 3;
then P is one-to-one by A4,FINSEQ_4:63;
then consider XFS be XFinSequence of NAT such that
A8: dom XFS=card {x,y} and
A9: for z st z in dom XFS holds XFS.z=card ((Fy*P).z) and
A10: Card_Intersection(Fy,1)=Sum XFS by A7,Th43;
len XFS=2 by A1,A8,CARD_2:57;
then
A11: XFS=<%XFS.0,XFS.1%> by AFINSQ_1:38;
A12: dom P={0,1} by FUNCT_4:62;
then 1 in dom P by TARSKI:def 2;
then
A13: (Fy*P).1=Fy.(P.1) by FUNCT_1:13;
0 in {0} by TARSKI:def 1;
then
A14: ({x,y}-->0)"{0}={x,y} by FUNCOP_1:14;
Fy.x=X & Fy.y=Y by A1,A2,FUNCT_4:63;
then
A15: Intersection(Fy,{x,y}-->0,0)=X/\Y by A14,Th35;
0 in dom P by A12,TARSKI:def 2;
then
A16: (Fy*P).0=Fy.(P.0) by FUNCT_1:13;
A17: dom XFS=2 by A1,A8,CARD_2:57;
then 1 in dom XFS by CARD_1:50,TARSKI:def 2;
then
A18: XFS.1=card Y by A9,A6,A13;
0 in dom XFS by A17,CARD_1:50,TARSKI:def 2;
then XFS.0=card X by A9,A5,A16;
then addnat "**" XFS=addnat.(card X,card Y) by A11,A18,AFINSQ_2:38;
then
A19: addnat "**" XFS=card X + card Y by BINOP_2:def 23;
card {x,y}=2 & dom Fy={x,y} by A1,A2,CARD_2:57,FUNCT_4:62;
hence thesis by A10,A19,A15,Th44,AFINSQ_2:51;
end;
theorem Th47:
for Fy,x 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
let Fy,x such that
A1: dom Fy is finite and
A2: x in dom Fy;
reconsider X=dom Fy as finite set by A1;
card X>0 by A2;
then reconsider k=card X-1 as Element of NAT by NAT_1:20;
set Xx=X\{x};
A3: Xx={}implies card Xx={};
consider Px be Function of card Xx,Xx such that
A4: Px is one-to-one by Lm2;
not card Xx in card Xx;
then consider P be Function of card Xx\/{card Xx},Xx\/{x} such that
A5: P|(card Xx) = Px and
A6: P.(card Xx)=x by A3,STIRL2_1:57;
not x in Xx by ZFMISC_1:56;
then
A7: P is one-to-one by A4,A3,A5,A6,STIRL2_1:58;
A8: card X=Segm(k+1);
then
A9: card Xx= Segm k by A2,STIRL2_1:55;
then card X=card Xx\/{card Xx} by A8,AFINSQ_1:2;
then reconsider P as Function of card X,X by A2,ZFMISC_1:116;
consider XFS be XFinSequence of NAT such that
A10: dom XFS=card X and
A11: for z st z in dom XFS holds XFS.z=card ((Fy*P).z) and
A12: Card_Intersection(Fy,1)=Sum XFS by A7,Th43;
A13: P.k=x by A2,A6,A8,STIRL2_1:55;
X/\Xx=Xx by XBOOLE_1:28;
then dom (Fy|Xx)=Xx by RELAT_1:61;
then consider XFSx be XFinSequence of NAT such that
A14: dom XFSx=card Xx and
A15: for z st z in dom XFSx holds XFSx.z=card (((Fy|Xx)*Px).z) and
A16: Card_Intersection(Fy|Xx,1)=Sum XFSx by A4,Th43;
k<k+1 by NAT_1:13;
then
A17: Segm k c= Segm(k+1) by NAT_1:39;
A18: for y being object st y in dom XFSx holds XFS.y = XFSx.y
proof
A19: Xx=X/\Xx & X/\Xx=dom (Fy|Xx) by RELAT_1:61,XBOOLE_1:28;
let y be object such that
A20: y in dom XFSx;
A21: XFS.y=card ((Fy*P).y) by A14,A9,A10,A11,A17,A20;
A22: dom Px=k by A3,A9,FUNCT_2:def 1;
then Px.y in rng Px by A14,A9,A20,FUNCT_1:def 3;
then
A23: (Fy|Xx).(Px.y)=Fy.(Px.y) by A19,FUNCT_1:47;
dom P=k+1 by CARD_1:27,FUNCT_2:def 1;
then
A24: (Fy*P).y=Fy.(P.y) by A14,A9,A17,A20,FUNCT_1:13;
Px.y=P.y by A14,A5,A9,A20,A22,FUNCT_1:47;
then (Fy*P).y=((Fy|Xx)*Px).y by A14,A9,A20,A22,A24,A23,FUNCT_1:13;
hence thesis by A15,A20,A21;
end;
k<k+1 by NAT_1:13;
then
A25: k in Segm(k+1) by NAT_1:44;
then k in dom P by CARD_1:27,FUNCT_2:def 1;
then
A26: (Fy*P).k=Fy.(P.k) by FUNCT_1:13;
dom XFS /\k=dom XFSx by A14,A9,A10,A17,XBOOLE_1:28;
then XFS|k=XFSx by A18,FUNCT_1:46;
then
A27: Sum XFSx +XFS.k=Sum (XFS|(k+1)) by A10,A25,AFINSQ_2:65;
XFS.k=card ((Fy*P).k) by A10,A11,A25;
hence thesis by A16,A10,A12,A27,A26,A13;
end;
theorem Th48:
dom Intersect(F,dom F-->X9)=dom F & for x st x in dom F holds
Intersect(F,dom F-->X9).x = F.x /\ X9
proof
A1: dom F/\dom(dom F-->X9)=dom F;
hence dom F=dom Intersect(F,dom F-->X9) by YELLOW20:def 2;
let x;
assume
A2: x in dom F;
then Intersect(F,dom F-->X9).x=F.x/\(dom F-->X9).x by A1,YELLOW20:def 2;
hence thesis by A2,FUNCOP_1:7;
end;
theorem Th49:
(union rng F)/\X9=union rng Intersect(F,dom F-->X9)
proof
set I= Intersect(F,dom F-->X9);
thus (union rng F)/\X9 c= union rng I
proof
let x be object such that
A1: x in (union rng F)/\X9;
A2: x in X9 by A1,XBOOLE_0:def 4;
x in union rng F by A1,XBOOLE_0:def 4;
then consider Fx be set such that
A3: x in Fx and
A4: Fx in rng F by TARSKI:def 4;
consider x1 being object such that
A5: x1 in dom F and
A6: F.x1=Fx by A4,FUNCT_1:def 3;
x1 in dom I by A5,Th48;
then
A7: I.x1 in rng I by FUNCT_1:def 3;
I.x1=Fx/\X9 by A5,A6,Th48;
then x in I.x1 by A3,A2,XBOOLE_0:def 4;
hence thesis by A7,TARSKI:def 4;
end;
thus union rng I c= (union rng F)/\X9
proof
let x be object;
assume x in union rng I;
then consider Ix be set such that
A8: x in Ix and
A9: Ix in rng I by TARSKI:def 4;
consider x1 being object such that
A10: x1 in dom I and
A11: I.x1=Ix by A9,FUNCT_1:def 3;
A12: x1 in dom F by A10,Th48;
then
A13: F.x1 in rng F by FUNCT_1:def 3;
A14: I.x1=F.x1/\X9 by A12,Th48;
then x in F.x1 by A8,A11,XBOOLE_0:def 4;
then
A15: x in union rng F by A13,TARSKI:def 4;
x in X9 by A8,A11,A14,XBOOLE_0:def 4;
hence thesis by A15,XBOOLE_0:def 4;
end;
end;
theorem Th50:
Intersection(F,Ch,y)/\X9= Intersection(Intersect(F,dom F-->X9), Ch,y)
proof
set I=Intersect(F,dom F-->X9);
set Int1=Intersection(F,Ch,y);
set Int2=Intersection(I,Ch,y);
thus Int1/\X9 c= Int2
proof
let x be object such that
A1: x in Int1/\X9;
A2: for z st z in dom Ch & Ch.z=y holds x in I.z
proof
A3: x in Int1 by A1,XBOOLE_0:def 4;
let z;
assume z in dom Ch & Ch.z=y;
then
A4: x in F.z by A3,Def2;
then
A5: z in dom F by FUNCT_1:def 2;
x in X9 by A1,XBOOLE_0:def 4;
then x in F.z/\X9 by A4,XBOOLE_0:def 4;
hence thesis by A5,Th48;
end;
x in X9 by A1,XBOOLE_0:def 4;
then x in (union rng F)/\X9 by A1,XBOOLE_0:def 4;
then x in union rng I by Th49;
hence thesis by A2,Def2;
end;
thus Int2 c= Int1/\X9
proof
let x be object such that
A6: x in Int2;
x in union rng I by A6;
then
A7: x in (union rng F)/\X9 by Th49;
then
A8: x in X9 by XBOOLE_0:def 4;
A9: for z st z in dom Ch & Ch.z=y holds x in F.z
proof
A10: dom I=dom F by Th48;
let z;
assume z in dom Ch & Ch.z=y;
then
A11: x in I.z by A6,Def2;
then z in dom I by FUNCT_1:def 2;
then x in F.z/\X9 by A11,A10,Th48;
hence thesis by XBOOLE_0:def 4;
end;
x in union rng F by A7,XBOOLE_0:def 4;
then x in Int1 by A9,Def2;
hence thesis by A8,XBOOLE_0:def 4;
end;
end;
theorem Th51:
for F, G be 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
let F, G be XFinSequence such that
A1: F is one-to-one and
A2: G is one-to-one and
A3: rng F misses rng G;
len F,rng F are_equipotent by A1,WELLORD2:def 4;
then
A4: card len F=card rng F by CARD_1:5;
len G,rng G are_equipotent by A2,WELLORD2:def 4;
then
A5: card len G=card rng G by CARD_1:5;
reconsider FG=F^G as Function of dom (F^G),rng (F^G) by FUNCT_2:1;
A6: dom (F^G)=len F+len G by AFINSQ_1:def 3;
A7: FG is onto by FUNCT_2:def 3;
card(rng F\/rng G)=card rng F + card rng G by A3,CARD_2:40;
then card dom (F^G)=card rng (F^G) by A4,A5,A6,AFINSQ_1:26;
hence thesis by A7,FINSEQ_4:63;
end;
theorem Th52:
for Fy,X,x,n 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
let Fy,X,x,n such that
A1: dom Fy = X and
A2: x in dom Fy and
A3: k>0;
set Xx=X\{x};
A4: Xx\/{x}=X by A1,A2,ZFMISC_1:116;
set I=Intersect(Fy|(dom Fy\{x}),(dom Fy\{x})-->Fy.x);
set X1={f where f is Function of Xx\/{x},{1,0}:card (f"{1})=k+1 & f.x=1};
set X0={f where f is Function of Xx\/{x},{1,0}:card (f"{1})=k+1 & f.x=0};
X0\/X1=Choose(Xx\/{x},k+1,1,0) by Lm1;
then reconsider X0,X1 as finite set by FINSET_1:1,XBOOLE_1:7;
consider P1 be Function of card X1,X1 such that
A5: P1 is one-to-one by Lm2;
not x in Xx by ZFMISC_1:56;
then
A6: card Choose(Xx,k,1,0)=card X1 by Th12;
defpred p1[object,object] means ex f st f=P1.$1 & f in X1 & $2=f|Xx;
A7: for x1 being object st x1 in card X1
ex P1x1 be object st P1x1 in Choose(Xx,k,1,0) & p1[x1,P1x1]
proof
not x in Xx by ZFMISC_1:56;
then
A8: (Xx\/{x})\{x}=Xx by ZFMISC_1:117;
let x1 be object;
assume x1 in card X1;
then x1 in dom P1 by CARD_1:27,FUNCT_2:def 1;
then
A9: P1.x1 in rng P1 by FUNCT_1:def 3;
then P1.x1 in X1;
then consider P1x1 be Function of Xx\/{x},{1,0} such that
A10: P1.x1=P1x1 and
A11: card (P1x1"{1})=k+1 and
A12: P1x1.x=1;
A13: dom P1x1=Xx\/{x} by FUNCT_2:def 1;
A14: rng (P1x1|Xx) c= {1,0};
(Xx\/{x})/\Xx=Xx by XBOOLE_1:7,28;
then dom (P1x1|Xx)=Xx by A13,RELAT_1:61;
then reconsider Px=P1x1|Xx as Function of Xx,{1,0} by A14,FUNCT_2:2;
A15: not x in Px"{1} by ZFMISC_1:56;
x in {x} & dom P1x1=Xx\/{x} by FUNCT_2:def 1,TARSKI:def 1;
then x in dom P1x1 by XBOOLE_0:def 3;
then P1x1"{1}=Px"{1}\/{x} by A12,A13,A8,AFINSQ_2:66;
then k+1 =card (Px"{1})+1 by A11,A15,CARD_2:41;
then Px in Choose(Xx,k,1,0) by Def1;
hence thesis by A9,A10;
end;
consider P1x be Function of card X1,Choose(Xx,k,1,0) such that
A16: for x1 being object st x1 in card X1 holds p1[x1,P1x.x1]
from FUNCT_2:sch 1(A7);
for x1,x2 being object st x1 in dom P1x & x2 in dom P1x & P1x.x1 = P1x.x2
holds x1 = x2
proof
let x1,x2 be object such that
A17: x1 in dom P1x and
A18: x2 in dom P1x and
A19: P1x.x1 = P1x.x2;
consider f2 be Function such that
A20: f2=P1.x2 and
A21: f2 in X1 and
A22: P1x.x2=f2|Xx by A16,A18;
consider f1 be Function such that
A23: f1=P1.x1 and
A24: f1 in X1 and
A25: P1x.x1=f1|Xx by A16,A17;
A26: ex F be Function of Xx\/{x},{1,0} st f1=F &card (F"{1})=k+1&F.x=1 by A24;
then
A27: dom f1=Xx\/{x} by FUNCT_2:def 1;
A28: ex F be Function of Xx\/{x},{1,0} st f2=F & card (F"{1})=k+1 & F.x=1
by A21;
then
A29: dom f2=Xx\/{x} by FUNCT_2:def 1;
for z being object st z in dom f1 holds f1.z = f2.z
proof
let z be object such that
A30: z in dom f1;
now
per cases by A27,A30,XBOOLE_0:def 3;
suppose
A31: z in Xx;
then z in dom f1/\Xx by A30,XBOOLE_0:def 4;
then
A32: (f1|Xx).z=f1.z by FUNCT_1:48;
z in dom f2/\Xx by A27,A29,A30,A31,XBOOLE_0:def 4;
hence thesis by A19,A25,A22,A32,FUNCT_1:48;
end;
suppose
z in {x};
then z=x by TARSKI:def 1;
hence thesis by A26,A28;
end;
end;
hence thesis;
end;
then
A33: f1=f2 by A27,A29;
X1={} implies card X1={};
then dom P1=card X1 by FUNCT_2:def 1;
hence thesis by A5,A17,A18,A23,A20,A33;
end;
then
A34: P1x is one-to-one;
Xx/\X=Xx by XBOOLE_1:28;
then
A35: dom (Fy|(dom Fy\{x}))=Xx by A1,RELAT_1:61;
then dom I=Xx by A1,Th48;
then consider XFS1 be XFinSequence of NAT such that
A36: dom XFS1=dom P1x and
A37: for z,f st z in dom XFS1 & f=P1x.z holds XFS1.z=card(Intersection(
I,f,1)) and
A38: Card_Intersection(I,k)=Sum XFS1 by A6,A34,Def3;
A39: addnat "**" XFS1=Card_Intersection(I,k) by A38,AFINSQ_2:51;
not x in Xx by ZFMISC_1:56;
then
A40: card Choose(Xx,k+1,1,0)=card X0 by Th13;
set Ch=Choose(X,k+1,1,0);
consider P0 be Function of card X0,X0 such that
A41: P0 is one-to-one by Lm2;
A42: X1={} implies card X1={};
then
A43: dom P1=card X1 by FUNCT_2:def 1;
A44: X0={} implies card X0={};
then dom P0=card X0 by FUNCT_2:def 1;
then reconsider XP0=P0,XP1=P1 as XFinSequence by A43,AFINSQ_1:5;
A45: card X0=len XP0 by A44,FUNCT_2:def 1;
defpred p0[object,object] means ex f st f=P0.$1 & f in X0 & $2=f|Xx;
A46: for x0 be object st x0 in card X0
ex P0x0 be object st P0x0 in Choose(Xx,k+1,1,0) & p0[x0,P0x0]
proof
let x0 be object;
assume x0 in card X0;
then x0 in dom P0 by CARD_1:27,FUNCT_2:def 1;
then
A47: P0.x0 in rng P0 by FUNCT_1:def 3;
then P0.x0 in X0;
then consider P0x0 be Function of Xx\/{x},{1,0} such that
A48: P0.x0=P0x0 and
A49: card (P0x0"{1})=k+1 and
A50: P0x0.x=0;
A51: dom P0x0=Xx\/{x} by FUNCT_2:def 1;
A52: rng (P0x0|Xx) c= {1,0};
(Xx\/{x})/\Xx=Xx by XBOOLE_1:7,28;
then dom (P0x0|Xx)=Xx by A51,RELAT_1:61;
then reconsider Px=P0x0|Xx as Function of Xx,{1,0} by A52,FUNCT_2:2;
not x in Xx by ZFMISC_1:56;
then (Xx\/{x})\{x}=Xx by ZFMISC_1:117;
then P0x0"{1}=Px"{1} by A50,A51,AFINSQ_2:67;
then Px in Choose(Xx,k+1,1,0) by A49,Def1;
hence thesis by A47,A48;
end;
consider P0x be Function of card X0,Choose(Xx,k+1,1,0) such that
A53: for x1 being object st x1 in card X0 holds p0[x1,P0x.x1]
from FUNCT_2:sch 1(A46);
rng P0 \/ rng P1 c= X0\/X1 by XBOOLE_1:13;
then rng (XP0^XP1) c= X0\/X1 by AFINSQ_1:26;
then
A54: rng (XP0^XP1) c= Ch by A4,Lm1;
A55: card X1=len XP1 by A42,FUNCT_2:def 1;
for x1,x2 being object st x1 in dom P0x & x2 in dom P0x & P0x.x1 = P0x.x2
holds x1 = x2
proof
let x1,x2 be object such that
A56: x1 in dom P0x and
A57: x2 in dom P0x and
A58: P0x.x1 = P0x.x2;
consider f2 be Function such that
A59: f2=P0.x2 and
A60: f2 in X0 and
A61: P0x.x2=f2|Xx by A53,A57;
consider f1 be Function such that
A62: f1=P0.x1 and
A63: f1 in X0 and
A64: P0x.x1=f1|Xx by A53,A56;
A65: ex F be Function of Xx\/{x},{1,0} st f1=F &card (F"{1})=k+1&F.x=0 by A63;
then
A66: dom f1=Xx\/{x} by FUNCT_2:def 1;
A67: ex F be Function of Xx\/{x},{1,0} st f2=F & card (F"{1})=k+1 & F.x=0
by A60;
then
A68: dom f2=Xx\/{x} by FUNCT_2:def 1;
for z being object st z in dom f1 holds f1.z = f2.z
proof
let z be object such that
A69: z in dom f1;
now
per cases by A66,A69,XBOOLE_0:def 3;
suppose
A70: z in Xx;
then z in dom f1/\Xx by A69,XBOOLE_0:def 4;
then
A71: (f1|Xx).z=f1.z by FUNCT_1:48;
z in dom f2/\Xx by A66,A68,A69,A70,XBOOLE_0:def 4;
hence thesis by A58,A64,A61,A71,FUNCT_1:48;
end;
suppose
z in {x};
then z=x by TARSKI:def 1;
hence thesis by A65,A67;
end;
end;
hence thesis;
end;
then
A72: f1=f2 by A66,A68;
X0={} implies card X0={};
then dom P0=card X0 by FUNCT_2:def 1;
hence thesis by A41,A56,A57,A62,A59,A72;
end;
then P0x is one-to-one;
then consider XFS0 be XFinSequence of NAT such that
A73: dom XFS0=dom P0x and
A74: for z,f st z in dom XFS0 & f=P0x.z holds XFS0.z=card(Intersection(
Fy|(dom Fy\{x}),f,1)) and
A75: Card_Intersection(Fy|(dom Fy\{x}),k+1)=Sum XFS0 by A40,A35,Def3;
Choose(Xx,k+1,1,0)={} implies card Choose(Xx,k+1,1,0)={};
then
A76: dom P0x=card X0 by A40,FUNCT_2:def 1;
not x in Xx by ZFMISC_1:56;
then card X0+card X1=card Ch by A40,A6,A4,Th14;
then dom (XP0^XP1)=card Ch by A45,A55,AFINSQ_1:def 3;
then reconsider XP01=XP0^XP1 as Function of card Ch,Ch by A54,FUNCT_2:2;
rng P0 misses rng P1 by Lm1,XBOOLE_1:64;
then XP01 is one-to-one by A41,A5,Th51;
then consider XFS be XFinSequence of NAT such that
A77: dom XFS=dom XP01 and
A78: for z,f st z in dom XFS & f=XP01.z holds XFS.z=card(Intersection(
Fy,f,1)) and
A79: Card_Intersection(Fy,k+1)=Sum XFS by A1,Def3;
A80: addnat "**" XFS=Card_Intersection(Fy,k+1) by A79,AFINSQ_2:51;
Choose(Xx,k,1,0)={} implies card Choose(Xx,k,1,0)={};
then
A81: dom P1x=card X1 by A6,FUNCT_2:def 1;
A82: for n be Nat st n in dom XFS0 holds XFS.n=XFS0.n
proof
let n be Nat such that
A83: n in dom XFS0;
consider fx be Function such that
A84: fx=P0.n and
A85: fx in X0 and
A86: P0x.n=fx|Xx by A53,A73,A83;
A87: XFS0.n=card(Intersection(Fy|Xx,fx|Xx,1)) by A1,A74,A83,A86;
A88: ex fx9 be Function of Xx\/{x},{1,0} st fx=fx9 & card ( fx9"{1})=k+1 &
fx9.x=0 by A85;
then consider x1 being object such that
A89: x1 in fx"{1} by CARD_1:27,XBOOLE_0:def 1;
fx.x1 in {1} by A89,FUNCT_1:def 7;
then
A90: fx.x1=1 by TARSKI:def 1;
x1 in dom fx by A89,FUNCT_1:def 7;
then
A91: 1 in rng fx by A90,FUNCT_1:def 3;
A92: Xx\/{x}=X by A1,A2,ZFMISC_1:116;
A93: dom XFS0+(0 qua Nat) <=dom XFS0+dom XFS1 by XREAL_1:7;
dom fx=Xx\/{x} by A88,FUNCT_2:def 1;
then
A94: fx"{1}=(fx|Xx)"{1} by A88,A92,AFINSQ_2:67;
n< len XFS0 by A83,AFINSQ_1:86;
then n< len XFS0+dom XFS1 by A93,XXREAL_0:2;
then n < len XFS by A73,A36,A45,A55,A77,A76,A81,AFINSQ_1:def 3;
then
A95: n in dom XFS by AFINSQ_1:86;
XP01.n=XP0.n by A73,A45,A83,AFINSQ_1:def 3;
then
A96: XFS.n=card(Intersection(Fy,fx,1)) by A78,A84,A95;
(fx|Xx)"{1} c= dom (fx|Xx) & dom (fx|Xx)c= Xx by RELAT_1:58,132;
then Intersection(Fy|Xx,fx,1)=Intersection(Fy,fx,1) by A94,A91,Th29,
XBOOLE_1:1;
hence thesis by A94,A96,A87,Th27;
end;
X1={} implies card X1={};
then
A97: dom P1=card X1 by FUNCT_2:def 1;
A98: for n be Nat st n in dom XFS1 holds XFS.(len XFS0 + n) = XFS1.n
proof
A99: Xx\/{x}=X by A1,A2,ZFMISC_1:116;
let n be Nat such that
A100: n in dom XFS1;
consider fx be Function such that
A101: fx=P1.n and
A102: fx in X1 and
A103: P1x.n=fx|Xx by A16,A36,A100;
consider fx9 be Function of Xx\/{x},{1,0} such that
A104: fx=fx9 and
A105: card (fx9"{1})=k+1 and
A106: fx9.x=1 by A102;
A107: Intersection(Intersect(Fy|Xx,Xx-->Fy.x),fx|Xx,1)= Intersection(Fy|Xx
, fx|Xx,1)/\Fy.x by A1,A35,Th50;
A108: dom fx9=Xx\/{x} by FUNCT_2:def 1;
then
A109: dom fx=X by A1,A2,A104,ZFMISC_1:116;
A110: 1 in rng (fx|Xx) & (fx|Xx)"{1} c= Xx
proof
A111: (fx|Xx)"{1} c= dom (fx|Xx) & dom (fx|Xx)=dom fx /\Xx by RELAT_1:61,132;
reconsider fx1=(fx|Xx)"{1} as finite set;
not x in Xx by ZFMISC_1:56;
then not x in dom fx/\Xx by XBOOLE_0:def 4;
then not x in dom (fx|Xx) by RELAT_1:61;
then
A112: not x in fx1 by FUNCT_1:def 7;
{x}\/fx1=fx"{1} by A1,A2,A104,A106,A109,AFINSQ_2:66;
then card fx1+1=k+1 by A104,A105,A112,CARD_2:41;
then consider y being object such that
A113: y in fx1 by A3,CARD_1:27,XBOOLE_0:def 1;
y in dom (fx|Xx) by A113,FUNCT_1:def 7;
then
A114: (fx|Xx).y in rng (fx|Xx) by FUNCT_1:def 3;
dom fx /\Xx c= Xx & (fx|Xx).y in {1} by A113,FUNCT_1:def 7,XBOOLE_1:17;
hence thesis by A111,A114,TARSKI:def 1;
end;
n< len XFS1 by A100,AFINSQ_1:86;
then len XFS0+n < dom XFS0+dom XFS1 by XREAL_1:8;
then dom XFS0+n < len XFS by A73,A36,A45,A55,A77,A76,A81,AFINSQ_1:def 3;
then
A115: dom XFS0+n in dom XFS by AFINSQ_1:86;
XP01.(n+len XP0)=fx by A36,A97,A100,A101,AFINSQ_1:def 3;
then
A116: XFS.(dom XFS0+n)=card(Intersection(Fy,fx,1)) by A73,A45,A78,A76,A115;
fx.x in {1} by A104,A106,TARSKI:def 1;
then
A117: x in fx"{1} by A1,A2,A104,A108,A99,FUNCT_1:def 7;
XFS1.n=card(Intersection (Intersect(Fy|Xx,Xx-->Fy.x),fx|Xx,1)) by A1,A37
,A100,A103;
then XFS1.n=card(Intersection(Fy,fx|Xx,1)/\Fy.x) by A110,A107,Th29;
hence thesis by A117,A109,A116,Th31;
end;
dom XFS=len XFS0 + len XFS1 by A73,A36,A45,A55,A77,A76,A81,AFINSQ_1:def 3;
then XFS=XFS0^XFS1 by A82,A98,AFINSQ_1:def 3;
then
A118: addnat "**" XFS=addnat.(addnat "**" XFS0,addnat "**" XFS1) by AFINSQ_2:42
;
addnat "**" XFS0=Card_Intersection(Fy|(dom Fy\{x}),k+1) by A75,AFINSQ_2:51;
hence thesis by A118,A39,A80,BINOP_2:def 23;
end;
theorem Th53:
x in dom F implies union rng F=union rng (F|(dom F\{x}))\/F.x
proof
set d=dom F\{x};
set Fd=F|d;
A1: F|dom F=F;
assume
A2: x in dom F;
then d\/{x}=dom F by ZFMISC_1:116;
then F=Fd\/(F|{x}) by A1,RELAT_1:78;
then
A3: rng F= rng Fd\/rng (F|{x}) by RELAT_1:12;
Im(F,x)={F.x} by A2,FUNCT_1:59;
then rng (F|{x})={F.x} by RELAT_1:115;
then union rng F=union rng Fd \/union {F.x} by A3,ZFMISC_1:78;
hence thesis by ZFMISC_1:25;
end;
theorem Th54:
for Fy be finite-yielding Function,X ex XFS be XFinSequence of
INT st dom XFS = card X & for n st n in dom XFS holds XFS.n=((-1)|^n)*
Card_Intersection(Fy,n+1)
proof
let Fy be finite-yielding Function,X;
defpred P[set,set] means for n st n=$1 holds $2=((-1)|^n)*Card_Intersection(
Fy,n+1);
A1: for k st k in Segm card X ex x be Element of INT st P[k,x]
proof
let k such that
k in Segm card X;
reconsider C=((-1)|^k)*Card_Intersection(Fy,k+1) as Element of INT
by INT_1:def 2;
take C;
thus thesis;
end;
consider XFS be XFinSequence of INT such that
A2: dom XFS = Segm card X & for k st k in Segm card X holds P[k,XFS.k] from
STIRL2_1:sch 5(A1);
take XFS;
thus thesis by A2;
end;
:: The principle of inclusions and the disconnections
::$N Principle of Inclusion/Exclusion
::$L https://en.wikipedia.org/wiki/Inclusionâexclusion_principle Inclusionâexclusion principle
theorem Th55:
for Fy be finite-yielding Function,X st dom Fy=X for XFS be
XFinSequence of INT st dom XFS= card X & for n st n in dom XFS holds XFS.n=((-1
)|^n)*Card_Intersection(Fy,n+1) holds card union rng Fy=Sum XFS
proof
defpred P[Nat] means for Fy be finite-yielding Function,X st dom
Fy=X & card X=$1 for XFS be XFinSequence of INT st dom XFS= card X & for n st n
in dom XFS holds XFS.n=((-1)|^n)*Card_Intersection(Fy,n+1) holds card union rng
Fy=Sum XFS;
A1: for k st P[k] holds P[k+1]
proof
let k such that
A2: P[k];
let Fy be finite-yielding Function,X such that
A3: dom Fy=X and
A4: card X=k+1;
rng Fy is finite & for x st x in rng Fy holds x is finite
by A3,FINSET_1:8;
then reconsider urngFy=union rng Fy as finite set;
let XFS be XFinSequence of INT such that
A5: dom XFS=card X and
A6: for n st n in dom XFS holds XFS.n=((-1)|^n)*Card_Intersection(Fy, n+1);
per cases;
suppose
A7: k=0;
then len XFS=1 by A4,A5;
then
A8: XFS=<%XFS.0%> by AFINSQ_1:34;
XFS.0 is Element of INT by INT_1:def 2;
then
A9: addint "**" XFS=XFS.0 by A8,AFINSQ_2:37;
0 in dom XFS by A4,A5,A7,CARD_1:49,TARSKI:def 1;
then
A10: XFS.0=((-1)|^0)*Card_Intersection(Fy, (0 qua Nat)+1) by A6;
consider x being object such that
A11: dom Fy={x} by A3,A4,A7,CARD_2:42;
A12: rng Fy={Fy.x} by A11,FUNCT_1:4;
then
A13: union rng Fy= Fy.x by ZFMISC_1:25;
(-1)|^0=1 & Fy=x.-->Fy.x by A11,A12,FUNCOP_1:9,NEWTON:4;
then XFS.0= card union rng Fy by Th45,A13,A10;
hence thesis by A9,AFINSQ_2:50;
end;
suppose
A14: k>0;
consider x being object such that
A15: x in dom Fy by A3,A4,CARD_1:27,XBOOLE_0:def 1;
reconsider x as set by TARSKI:1;
set Xx=X\{x};
A16: card Xx=k by A3,A4,A15,STIRL2_1:55;
set FyX=Fy|Xx;
reconsider urngFyX=union rng FyX as finite set;
set Fyx=Fy.x;
set I=Intersect(FyX,dom FyX-->Fy.x);
consider XFyX be XFinSequence of INT such that
A17: dom XFyX = card Xx and
A18: for n st n in dom XFyX holds XFyX.n=((-1)|^n)*Card_Intersection
(FyX,n+1) by Th54;
urngFyX/\Fy.x=union rng I by Th49;
then reconsider urngI=union rng I as finite set;
consider XI be XFinSequence of INT such that
A19: dom XI = card Xx and
A20: for n st n in dom XI holds XI.n=((-1)|^n)*Card_Intersection(I,n
+1) by Th54;
set XI1 = (-1)(#)XI;
reconsider XI1 as XFinSequence of INT;
reconsider XcF=<%card Fyx%>,X0=<%0%> as XFinSequence of INT;
reconsider
F1=<%card Fyx%>^XI1,F2=XFyX^<%0%> as XFinSequence of INT;
A21: card Xx=k by A3,A4,A15,STIRL2_1:55;
reconsider zz=0 as Element of INT by INT_1:def 2;
A22:addint "**" X0 = zz by AFINSQ_2:37;
card Fyx is Element of INT by INT_1:def 2;
then A23:addint "**" XcF = card Fyx by AFINSQ_2:37;
A24: (-1)*Sum XI=Sum XI1 by AFINSQ_2:64;
A25:addint "**" F1 = addint.(card Fyx,addint "**" XI1) by A23,AFINSQ_2:42
.= card Fyx+(addint "**" XI1) by BINOP_2:def 20
.= card Fyx+Sum XI1 by AFINSQ_2:50;
A26:(addint "**" F2)=addint.(addint "**" XFyX,0) by A22,AFINSQ_2:42
.= addint "**" XFyX +zz by BINOP_2:def 20
.=Sum XFyX by AFINSQ_2:50;
A27: Sum (F1^F2) = (Sum F1) + Sum F2 by AFINSQ_2:55
.= (addint "**" F1) + Sum F2 by AFINSQ_2:50
.= card Fyx+(-1)*Sum XI+Sum XFyX by A24,A25,A26,AFINSQ_2:50;
A28: urngFyX\/Fyx = urngFy by A3,A15,Th53;
A29: urngFyX/\Fyx=urngI by Th49;
A30: dom FyX=Xx by A3,RELAT_1:62;
then dom I=Xx by Th48;
then
A31: card urngI=Sum XI by A2,A19,A20,A21;
len <%card Fyx%>=1 & len XI1=card Xx by A19,AFINSQ_1:33,VALUED_1:def 5;
then
A32: len F1=k+1 by A16,AFINSQ_1:17;
A33: for n be Nat st n in dom XFS holds XFS.n=addint.(F1.n,F2.n)
proof
let n be Nat such that
A34: n in dom XFS;
A35: n < len XFS by A34,AFINSQ_1:86;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
per cases;
suppose
A36: n=0;
A37: 0 in Segm k by A14,NAT_1:44;
k=dom XFyX by A3,A4,A15,A17,STIRL2_1:55;
then
A38: F2.0=XFyX.0 & XFyX.0=((-1)|^0)*
Card_Intersection(FyX,(0 qua Nat)+1) by A18,AFINSQ_1:def 3,A37;
F1.0=card Fyx & (-1)|^0=1 by AFINSQ_1:35,NEWTON:4;
then
A39: addint.(F1.0,F2.0)
=card Fyx+Card_Intersection(FyX,(0 qua Nat)+1) by A38,
BINOP_2:def 20;
A40: (-1)|^0=1 by NEWTON:4;
XFS.0=((-1)|^0)*Card_Intersection(Fy,(0 qua Nat)+1) by A6,A34,A36;
hence thesis by A3,A15,A36,A39,A40,Th47;
end;
suppose
A41: n>0;
then reconsider n1=n-1 as Element of NAT by NAT_1:20;
A42: len <%card Fyx%>=1 by AFINSQ_1:33;
A43: card Xx=k by A3,A4,A15,STIRL2_1:55;
A44: n < k+1 by A4,A5,A35;
then
A45: n<=k by NAT_1:13;
A46: n1<n1+1 by NAT_1:13;
then n1 <k by A45,XXREAL_0:2;
then n1 < len XI by A19,A43;
then n1 in dom XI by AFINSQ_1:86;
then
A47: XI1.n1=(-1)*XI.n1 & XI.n1=((-1)|^n1)*Card_Intersection(I,n1+1)
by A20,VALUED_1:6;
(0 qua Nat)+1<=n by A46,NAT_1:13;
then F1.n=((-1)*((-1)|^n1))*Card_Intersection(I,n1+1) by A32,A44,A42
,A47,AFINSQ_1:19;
then
A48: F1.n=((-1)|^(n1+1))*Card_Intersection(I,n1+1) by NEWTON:6;
A49: XFS.n=((-1)|^n)*Card_Intersection(Fy,n+1) by A6,A34;
Card_Intersection(Fy,n+1)= Card_Intersection(FyX,n+1)+
Card_Intersection (I,N) by A3,A15,A30,A41,Th52;
then
A50: XFS.n=((-1)|^n)*Card_Intersection(FyX,n+1)+ ((-1)|^n)*
Card_Intersection(I,N) by A49;
per cases by A45,XXREAL_0:1;
suppose
n<k;
then
A51: n in Segm k by NAT_1:44;
card Xx=k by A3,A4,A15,STIRL2_1:55;
then XFyX.n=((-1)|^n)*Card_Intersection(FyX,n+1) & F2.n=XFyX.n by
A17,A18,A51,AFINSQ_1:def 3;
hence thesis by A50,A48,BINOP_2:def 20;
end;
suppose
A52: n=k;
then n=card Xx by A3,A4,A15,STIRL2_1:55;
then n+1>card Xx by NAT_1:13;
then
A53: Card_Intersection(FyX,n+1)=0 by A30,Th42;
n=len XFyX by A3,A4,A15,A17,A52,STIRL2_1:55;
then F2.n=0 by AFINSQ_1:36;
hence thesis by A50,A48,A53,BINOP_2:def 20;
end;
end;
end;
card urngFyX=Sum XFyX by A2,A30,A17,A18,A21;
then
A54: card urngFy= Sum XFyX+card Fyx-Sum XI by A31,A28,A29,CARD_2:45;
A55: len <%0%>=1 by AFINSQ_1:33;
len XFyX=card Xx by A17;
then
A56: len F2=k+1 by A55,A16,AFINSQ_1:17;
A57: len XFS=k+1 by A4,A5;
Sum XFS = addint "**" XFS by AFINSQ_2:50
.= addint "**" (F1^F2)
by A32,A56,A33,A57,AFINSQ_2:46
.= Sum (F1^F2) by AFINSQ_2:50;
hence thesis by A27,A54;
end;
end;
A58: P[0]
proof
let Fy be finite-yielding Function,X such that
A59: dom Fy=X and
A60: card X=0;
dom Fy={} by A59,A60;
then
A61: rng Fy={} by RELAT_1:42;
let XFS be XFinSequence of INT such that
A62: dom XFS=card X and
for n st n in dom XFS holds XFS.n=((-1)|^n)*Card_Intersection(Fy,n+1);
len XFS=0 by A60,A62;
then addint "**" XFS = the_unity_wrt addint by AFINSQ_2:def 8
.= 0 by BINOP_2:4;
hence thesis by A61,AFINSQ_2:50,ZFMISC_1:2;
end;
for k holds P[k] from NAT_1:sch 2(A58,A1);
hence thesis;
end;
theorem Th56:
for Fy,X,n,k st dom Fy=X holds (ex x,y st x<>y & for f st f in
Choose(X,k,x,y) holds card(Intersection(Fy,f,x))=n) implies Card_Intersection(
Fy,k)=n*(card X choose k)
proof
let Fy,X,n,k such that
A1: X=dom Fy;
assume ex x,y st x<>y & for f st f in Choose(X,k,x,y) holds card(
Intersection(Fy,f,x))=n;
then consider x,y such that
A2: x<>y and
A3: for f st f in Choose(X,k,x,y) holds card(Intersection(Fy,f,x))=n;
set Ch=Choose(X,k,x,y);
consider P be Function of card Ch,Ch such that
A4: P is one-to-one by Lm2;
consider XFS be XFinSequence of NAT such that
A5: dom XFS=dom P and
A6: for z,f st z in dom XFS & f=P.z holds XFS.z=card(Intersection(Fy,f,x )) and
A7: Card_Intersection(Fy,k)=Sum XFS by A1,A2,A4,Def3;
for z being object st z in dom XFS holds XFS.z = n
proof
let z be object such that
A8: z in dom XFS;
A9: P.z in rng P by A5,A8,FUNCT_1:def 3;
then consider f be Function of X,{x,y} such that
A10: f=P.z and
card (f"{x})=k by Def1;
XFS.z=card(Intersection(Fy,f,x)) by A6,A8,A10;
hence thesis by A3,A9,A10;
end;
then
A11: XFS=dom XFS-->n by FUNCOP_1:11;
then
A12: rng XFS c= {n} by FUNCOP_1:13;
Ch={} implies card Ch={};
then
A13: dom P=card Ch by FUNCT_2:def 1;
n in {n} by TARSKI:def 1;
then {n} c= {0,n} & XFS"{n}=dom P by A5,A11,FUNCOP_1:14,ZFMISC_1:7;
then Sum XFS=n*card card Ch by A12,A13,AFINSQ_2:68,XBOOLE_1:1;
hence thesis by A2,A7,Th15;
end;
theorem Th57:
for Fy,X st dom Fy=X for XF be XFinSequence of NAT st dom XF=
card X & for n st n in dom XF holds ex x,y st x<>y & for f st f in Choose(X,n+1
,x,y) holds card(Intersection(Fy,f,x))=XF.n holds ex F be XFinSequence of INT
st dom F=card X & card union rng Fy = Sum F & for n st n in dom F holds F.n=((-
1)|^n)*XF.n*(card X choose (n+1))
proof
let Fy,X such that
A1: dom Fy=X;
let XF be XFinSequence of NAT such that
A2: dom XF=card X & for n st n in dom XF holds ex x,y st x<>y & for f st
f in Choose(X,n+1,x,y) holds card(Intersection(Fy,f,x))=XF.n;
defpred f[object,object] means
for n st n=$1 holds $2=((-1)|^n)*(XF.n)*(card X choose (n+1));
A3: for x being object st x in card X ex y being object st y in INT & f[x,y]
proof
A4: card X is Subset of NAT by STIRL2_1:8;
let x be object;
assume x in card X;
then reconsider x9=x as Element of NAT by A4;
reconsider xx=((-1)|^x9)*(XF.x9) as Integer;
reconsider ch=card X choose (x9+1) as Integer;
take xx*ch;
thus thesis by INT_1:def 2;
end;
consider F be Function of card X,INT such that
A5: for x being object st x in card X holds f[x,F.x] from FUNCT_2:sch 1(A3);
A6: dom F =card X by FUNCT_2:def 1;
then reconsider F as XFinSequence by AFINSQ_1:5;
reconsider F as XFinSequence of INT;
take F;
for n st n in dom F holds F.n=((-1)|^n)*Card_Intersection(Fy,n+1)
proof
let n such that
A7: n in dom F;
ex x,y st x<>y & for f st f in Choose(X,n+1,x,y) holds card(
Intersection(Fy,f,x))=XF.n by A2,A6,A7;
then
A8: Card_Intersection(Fy,n+1)=(XF.n)*(card X choose (n+1)) by A1,Th56;
F.n=((-1)|^n)*(XF.n)*(card X choose (n+1)) by A5,A6,A7;
hence thesis by A8;
end;
hence thesis by A1,A5,A6,Th55;
end;
Lm3: for X,Y be finite set st X is non empty & Y is non empty ex F be
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 st n in dom F holds F.n=((-1)|^n)*(card
Y choose (n+1))*((card Y-n-1) |^ card X)
proof
let X,Y be finite set such that
A1: X is non empty and
A2: Y is non empty;
defpred xf[object,object] means
for n st n=$1 holds $2=(card Y-n-1) |^ card X;
A3: for x being object st x in Segm card Y
ex y being object st y in NAT & xf[x,y]
proof
let x be object such that
A4: x in Segm card Y;
reconsider n=x as Element of NAT by A4;
n< card Y by A4,NAT_1:44;
then n+1<=card Y by NAT_1:13;
then reconsider k=(card Y)-(n+1) as Element of NAT by NAT_1:21;
xf[n, k|^ card X];
hence thesis;
end;
consider XF be Function of Segm card Y,NAT such that
A5: for x being object st x in Segm card Y
holds xf[x,XF.x] from FUNCT_2:sch 1(A3);
set Onto={f where f is Function of X,Y:f is onto};
deffunc fy(object)={f where f is Function of X,Y:not $1 in rng f};
A6: for x be object st x in Y holds fy(x) in bool Funcs(X,Y)
proof
let x be object such that
A7: x in Y;
fy(x) c= Funcs(X,Y)
proof
let y be object;
assume y in fy(x);
then ex f be Function of X,Y st y=f & not x in rng f;
hence thesis by A7,FUNCT_2:8;
end;
hence thesis;
end;
consider Fy9 be Function of Y,bool Funcs(X,Y) such that
A8: for x being object st x in Y holds Fy9.x = fy(x) from FUNCT_2:sch 2(A6);
for y being object st y in dom Fy9 holds Fy9.y is finite
proof
let y be object;
assume
y in dom Fy9;
then Fy9.y in rng Fy9 by FUNCT_1:def 3;
hence thesis;
end;
then reconsider Fy=Fy9 as finite-yielding Function by FINSET_1:def 4;
union rng Fy9 c= union bool Funcs(X,Y) by ZFMISC_1:77;
then
A9: union rng Fy c= Funcs(X,Y) by ZFMISC_1:81;
reconsider u=union rng Fy as finite set;
A10: dom XF=card Y by FUNCT_2:def 1;
then reconsider XF as XFinSequence by AFINSQ_1:5;
reconsider XF as XFinSequence of NAT;
A11: for n st n in dom XF holds ex x,y st x<>y & for f st f in Choose(Y,n+1,
x,y) holds card(Intersection(Fy,f,x))=XF.n
proof
let n such that
A12: n in dom XF;
take 0,1;
thus 0<>1;
let f9 be Function;
assume f9 in Choose(Y,n+1,0,1);
then consider f be Function of Y,{0,1} such that
A13: f = f9 and
A14: card (f"{0})=n+1 by Def1;
A15: Intersection(Fy,f,0) c= Funcs(X,Y\f"{0})
proof
let z be object such that
A16: z in Intersection(Fy,f,0);
0 in rng f by A14,CARD_1:27,FUNCT_1:72;
then consider x1 such that
A17: x1 in dom f and
f.x1=0 and
A18: z in Fy.x1 by A16,Th21;
z in fy(x1) by A8,A17,A18;
then consider g be Function of X,Y such that
A19: z=g and
not x1 in rng g;
A20: rng g c= Y\f"{0}
proof
let gy be object such that
A21: gy in rng g;
assume not gy in Y\f"{0};
then
A22: gy in f"{0} by A21,XBOOLE_0:def 5;
then f.gy in {0} by FUNCT_1:def 7;
then
A23: f.gy =0 by TARSKI:def 1;
gy in dom f by A22,FUNCT_1:def 7;
then g in Fy.gy by A16,A19,A23,Def2;
then g in fy(gy) by A8,A21;
then ex h be Function of X,Y st g=h & not gy in rng h;
hence contradiction by A21;
end;
dom g=X by A17,FUNCT_2:def 1;
hence thesis by A19,A20,FUNCT_2:def 2;
end;
reconsider I=Intersection(Fy,f,0) as finite set;
A24: card (Y\f"{0})=card Y-(n+1) by A14,CARD_2:44;
Funcs(X,Y\f"{0}) c= Intersection(Fy,f,0)
proof
let g9 be object;
assume g9 in Funcs(X,Y\f"{0});
then consider g be Function such that
A25: g9 = g and
A26: dom g = X and
A27: rng g c= Y\f"{0} by FUNCT_2:def 2;
reconsider gg=g as Function of X,Y by A26,A27,FUNCT_2:2,XBOOLE_1:1;
consider y being object such that
A28: y in f"{0} by A14,CARD_1:27,XBOOLE_0:def 1;
not y in rng g by A27,A28,XBOOLE_0:def 5;
then
A29: gg in fy(y);
dom Fy=Y by FUNCT_2:def 1;
then
A30: Fy9.y in rng Fy9 by A28,FUNCT_1:def 3;
A31: for z st z in dom f & f.z=0 holds g in Fy.z
proof
let z such that
A32: z in dom f and
A33: f.z=0;
f.z in {0} by A33,TARSKI:def 1;
then z in f"{0} by A32,FUNCT_1:def 7;
then
A34: not z in rng gg by A27,XBOOLE_0:def 5;
Fy.z=fy(z) by A8,A32;
hence thesis by A34;
end;
fy(y)=Fy9.y by A8,A28;
then g in union rng Fy by A30,A29,TARSKI:def 4;
hence thesis by A25,A31,Def2;
end;
then
A35: Funcs(X,Y\f"{0}) = Intersection(Fy,f,0) by A15;
now
per cases;
suppose
Y\f"{0}={};
then card I = 0 & (card Y - n-1)|^card X =0 by A1,A15,A24,NAT_1:14,
NEWTON:11;
hence thesis by A5,A10,A12,A13;
end;
suppose
A36: Y\f"{0} <>{};
XF.n=(card Y-n-1) |^ card X by A5,A10,A12;
hence thesis by A13,A35,A24,A36,Th3;
end;
end;
hence thesis;
end;
dom XF= card Y & dom Fy = Y by FUNCT_2:def 1;
then consider F be XFinSequence of INT such that
A37: dom F=card Y and
A38: card union rng Fy = Sum F and
A39: for n st n in dom F holds F.n=((-1)|^n)*XF.n*(card Y choose (n+1))
by A11,Th57;
take F;
thus dom F = card Y by A37;
A40: card(Funcs(X,Y)\u) = card Funcs(X,Y) - card u by A9,CARD_2:44;
A41: Onto c= Funcs(X,Y) \ union rng Fy
proof
let x be object;
assume x in Onto;
then consider f be Function of X,Y such that
A42: x=f and
A43: f is onto;
assume
A44: not x in Funcs(X,Y) \ union rng Fy;
f in Funcs(X,Y) by A2,FUNCT_2:8;
then f in union rng Fy by A42,A44,XBOOLE_0:def 5;
then consider Fyy be set such that
A45: f in Fyy and
A46: Fyy in rng Fy by TARSKI:def 4;
consider y being object such that
A47: y in dom Fy and
A48: Fy.y=Fyy by A46,FUNCT_1:def 3;
y in Y by A47,FUNCT_2:def 1;
then f in fy(y) by A8,A45,A48;
then
A49: ex g be Function of X,Y st f=g & not y in rng g;
y in Y by A47,FUNCT_2:def 1;
hence contradiction by A43,A49,FUNCT_2:def 3;
end;
A50: Funcs(X,Y) \ union rng Fy c= Onto
proof
let x be object such that
A51: x in Funcs(X,Y) \ union rng Fy;
consider f such that
A52: x = f and
A53: dom f = X & rng f c= Y by A51,FUNCT_2:def 2;
reconsider f as Function of X,Y by A53,FUNCT_2:2;
assume not x in Onto;
then not f is onto by A52;
then rng f<>Y by FUNCT_2:def 3;
then not Y c= rng f;
then consider y being object such that
A54: y in Y and
A55: not y in rng f;
y in dom Fy9 by A54,FUNCT_2:def 1;
then Fy9.y in rng Fy9 by FUNCT_1:def 3;
then
A56: fy(y) in rng Fy9 by A8,A54;
f in fy(y) by A55;
then f in union rng Fy by A56,TARSKI:def 4;
hence thesis by A51,A52,XBOOLE_0:def 5;
end;
card Funcs(X,Y) =card Y |^ card X by A2,Th3;
hence card Onto=(card Y |^ card X) - Sum F by A38,A50,A41,A40,XBOOLE_0:def 10
;
let n such that
A57: n in dom F;
A58: F.n=((-1)|^n)*XF.n*(card Y choose (n+1)) by A39,A57;
XF.n=(card Y-n-1) |^ card X by A5,A37,A57;
hence thesis by A58;
end;
:: onto
theorem Th58:
for X,Y be finite set st X is non empty & Y is non empty ex F be
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 st n in dom F holds F.n=((-1)|^n)*(card Y choose n)*(
(card Y-n) |^ card X)
proof
let X,Y be finite set such that
A1: X is non empty & Y is non empty;
reconsider c = card Y|^ card X as Element of INT by INT_1:def 2;
A2: len <%c%>=1 by AFINSQ_1:33;
set Onto= {f where f is Function of X,Y:f is onto};
consider F be XFinSequence of INT such that
A3: dom F = card Y and
A4: (card Y|^ card X)-Sum F=card Onto and
A5: for n st n in dom F holds F.n=((-1)|^n)*(card Y choose (n+1))*((card
Y-n-1) |^ card X) by A1,Lm3;
set F1 = (-1)(#)F;
reconsider F1 as XFinSequence of INT;
A6: dom F1 = dom F & dom F = card Y by A3,VALUED_1:def 5;
reconsider GF1=<%c%>^F1 as XFinSequence of INT;
take GF1;
len F1=card Y by A3,VALUED_1:def 5;
hence
A7: dom GF1 = card Y +1 by A2,AFINSQ_1:def 3;
(-1)*Sum F =Sum F1 by AFINSQ_2:64;
then c -Sum F=c +Sum F1 .=addint.(c,Sum F1) by BINOP_2:def 20
.=addint.(addint "**" <%c%>,Sum F1) by AFINSQ_2:37
.=addint.(addint "**" <%c%>,addint "**" F1) by AFINSQ_2:50
.=addint "**" GF1 by AFINSQ_2:42
.=Sum GF1 by AFINSQ_2:50;
hence Sum GF1=card Onto by A4;
let n such that
A8: n in dom GF1;
now
per cases;
suppose
A9: n=0;
then ((-1)|^n)=1 & (card Y choose n) =1 by NEWTON:4,19;
hence thesis by A9,AFINSQ_1:35;
end;
suppose
n>0;
then reconsider n1=n-1 as Element of NAT by NAT_1:20;
n < len GF1 by A8,AFINSQ_1:86;
then n < card Y +1 by A7;
then n1+1 <= card Y by NAT_1:13;
then n1 < card Y by NAT_1:13;
then n1 < len F1 by A6;
then
A10: n1 in dom F1 by AFINSQ_1:86;
then
A11: F.n1=((-1)|^n1)*(card Y choose (n1+1))*((card Y-n1-1)|^ card X) by A5,A6;
len <% c %>=1 by AFINSQ_1:33;
then
A12: GF1.(n1+1)=F1.n1 by A10,AFINSQ_1:def 3;
then
A13: (-1)*((-1)|^n1)=(-1)|^n by NEWTON:6;
GF1.(n1+1)=(-1)*F.n1 by A12,VALUED_1:6;
hence thesis by A11,A13;
end;
end;
hence thesis;
end;
:: n block k
theorem
for n,k st k <= n ex F be XFinSequence of INT st n block k = 1/(k!) *
Sum F & dom F = k+1 & for m st m in dom F holds F.m=((-1)|^m)*(k choose m)*((k-
m) |^ n)
proof
let n,k such that
A1: k <= n;
now
per cases;
suppose
A2: n=0 & k=0;
reconsider I=1 as Element of INT by INT_1:def 2;
set F=<%I%>;
take F;
addint "**" <%I%>=1 by AFINSQ_2:37;
then Sum F = 1 by AFINSQ_2:50;
hence n block k= 1/(k!) * Sum F by A2,NEWTON:12,STIRL2_1:26;
thus dom F=k+1 by A2,AFINSQ_1:33;
let m;
assume m in dom F;
then
A3: m in {0} by AFINSQ_1:33,CARD_1:49;
then m=0 by TARSKI:def 1;
then
A4: (-1) |^m=1 by NEWTON:4;
A5: ((k-m) |^n)=1 by A2,NEWTON:4;
A6: 0 choose 0 = 1 by NEWTON:19;
m=0 by A3,TARSKI:def 1;
hence F.m=((-1) |^m)*(k choose m)*((k-m) |^n) by A2,A4,A5,A6;
end;
suppose
A7: n<>0 & k=0;
set F=k+1 -->0;
reconsider Fi=F as XFinSequence of INT;
reconsider Fn=F as XFinSequence of NAT;
take Fi;
rng F c={0} & {0} c={0,0} by ENUMSET1:29,FUNCOP_1:13;
then
Sum Fn= 0*card (Fn"{0}) by AFINSQ_2:68,XBOOLE_1:1;
hence n block k = 1/(k!) * Sum Fi & dom Fi=k+1 by A7,STIRL2_1:31;
let m such that
m in dom Fi;
now
per cases;
suppose
m=0;
then (k-m) |^ n=0 by A7,NAT_1:14,NEWTON:11;
hence (k choose m)*((k-m) |^ n)=0;
end;
suppose
m>0;
then (k choose m)=0 by A7,NEWTON:def 3;
hence (k choose m)*((k-m) |^ n)=0;
end;
end;
then
A9: ((-1)|^m)*((k choose m)*((k-m) |^ n))=0;
thus Fi.m=((-1)|^m)*(k choose m)*((k-m) |^ n) by A9;
end;
suppose
A10: n<>0 & k<>0;
set Perm={p where p is Function of k,k:p is Permutation of k};
card Perm=(card k)! by Th7;
then reconsider Perm as finite set;
reconsider Bloc={f where f is Function of Segm n,Segm k:
f is onto "increasing} as
finite set by STIRL2_1:24;
set Onto={f where f is Function of n,k:f is onto};
defpred P[object,object] means
for p be Function of k,k, f be Function of n,k
st $1=[p,f] holds $2=p*f;
reconsider N=n,K=k as non empty Subset of NAT by A10,STIRL2_1:8;
A11: card [:Perm,Bloc:]= card Perm * card Bloc by CARD_2:46;
A12: for x being object st x in [:Perm,Bloc:]
ex y being object st y in Onto & P[x,y]
proof
let x be object;
assume x in [:Perm,Bloc:];
then consider p9,f9 be object such that
A13: p9 in Perm and
A14: f9 in Bloc and
A15: x=[p9,f9] by ZFMISC_1:def 2;
consider f be Function of Segm n,Segm k such that
A16: f=f9 and
A17: f is onto "increasing by A14;
A18: rng f=Segm k by A17,FUNCT_2:def 3;
consider p be Function of Segm k,Segm k such that
A19: p=p9 and
A20: p is Permutation of Segm k by A13;
reconsider pf=p*f as Function of Segm n,Segm k;
take pf;
A21: dom p=Segm k by A10,FUNCT_2:def 1;
rng p=k by A20,FUNCT_2:def 3;
then rng (p*f)=k by A18,A21,RELAT_1:28;
then pf is onto by FUNCT_2:def 3;
hence pf in Onto;
let p1 be Function of k,k, f1 be Function of n,k such that
A22: x=[p1,f1];
p1=p by A15,A19,A22,XTUPLE_0:1;
hence thesis by A15,A16,A22,XTUPLE_0:1;
end;
consider FP be Function of [:Perm,Bloc:],Onto such that
A23: for x being object st x in [:Perm,Bloc:] holds P[x,FP.x]
from FUNCT_2:sch 1(
A12);
A24: FP is one-to-one
proof
let x1,x2 be object such that
A25: x1 in dom FP and
A26: x2 in dom FP and
A27: FP.x1 = FP.x2;
consider p19,f19 be object such that
A28: p19 in Perm and
A29: f19 in Bloc and
A30: x1=[p19,f19] by A25,ZFMISC_1:def 2;
consider p1 be Function of k,k such that
A31: p19=p1 and
A32: p1 is Permutation of k by A28;
consider p29,f29 be object such that
A33: p29 in Perm and
A34: f29 in Bloc and
A35: x2=[p29,f29] by A26,ZFMISC_1:def 2;
FP.x1 in rng FP by A25,FUNCT_1:def 3;
then FP.x1 in Onto;
then consider fp be Function of N,K such that
A36: FP.x1=fp and
A37: fp is onto;
A38: rng fp=K by A37,FUNCT_2:def 3;
consider p2 be Function of k,k such that
A39: p29=p2 and
A40: p2 is Permutation of k by A33;
consider f2 be Function of Segm n,Segm k such that
A41: f29=f2 and
A42: f2 is onto "increasing by A34;
rng fp =K by A37,FUNCT_2:def 3;
then reconsider p199=p1,p299=p2 as Permutation of rng fp by A32,A40;
consider f1 be Function of Segm n,Segm k such that
A43: f19=f1 and
A44: f1 is onto "increasing by A29;
reconsider f199=f1,f299=f2 as Function of N,K;
A45: rng f2=K by A42,FUNCT_2:def 3;
for l,m be Nat st l in rng f1 & m in rng f1 & l < m
holds min* f1"{l} < min* f1"{m} by A44,STIRL2_1:def 1;
then
A46: f199 is 'increasing by STIRL2_1:def 3;
for l,m be Nat st l in rng f2 & m in rng f2 & l < m
holds min* f2"{l} < min* f2"{m} by A42,STIRL2_1:def 1;
then
A47: f299 is 'increasing by STIRL2_1:def 3;
A48: fp=p199*f199 by A23,A25,A30,A31,A43,A36;
A49: rng f1=K by A44,FUNCT_2:def 3;
A50: fp=p299*f299 by A23,A26,A27,A35,A39,A41,A36;
then p199=p299 by A46,A47,A49,A45,A48,A38,STIRL2_1:65;
hence thesis by A30,A31,A43,A35,A39,A41,A46,A47,A49,A45,A48,A50,A38,
STIRL2_1:65;
end;
consider h be Function of Segm n,Segm k such that
A51: h is onto "increasing by A1,A10,STIRL2_1:23;
Onto c= rng FP
proof
let x be object;
assume x in Onto;
then consider f be Function of n,k such that
A52: f=x and
A53: f is onto;
rng f=K by A53,FUNCT_2:def 3;
then consider I be Function of N,K,P be Permutation of K such that
A54: f=P*I and
A55: K=rng I and
A56: I is 'increasing by STIRL2_1:63;
set p=P;
reconsider i=I as Function of Segm n,Segm k;
for l,m be Nat st l in rng I & m in rng I & l < m
holds min* I"{l} < min* I"{m} by A56,STIRL2_1:def 3;
then
A57: i is "increasing by STIRL2_1:def 1;
i is onto by A55,FUNCT_2:def 3;
then p in Perm & i in Bloc by A57;
then
A58: [p,i] in [:Perm,Bloc:] by ZFMISC_1:def 2;
h in Onto by A51;
then
A59: [p,i] in dom FP by A58,FUNCT_2:def 1;
FP.([p,i])=f by A23,A54,A58;
hence thesis by A52,A59,FUNCT_1:def 3;
end;
then
A60: rng FP=Onto;
h in Onto by A51;
then dom FP=[:Perm,Bloc:] by FUNCT_2:def 1;
then Onto,[:Perm,Bloc:] are_equipotent by A24,A60,WELLORD2:def 4;
then
A61: card Onto=card Perm * card Bloc by A11,CARD_1:5;
A62: (k!)*card Bloc/(k!)=card Bloc*((k!)/(k!)) & (k!)/(k!)=1 by XCMPLX_1:60,74
;
consider F be XFinSequence of INT such that
A63: dom F = card k+1 and
A64: Sum F = card {f where f is Function of n,k:f is onto} and
A65: for m st m in dom F holds F.m=((-1)|^m)*(card k choose m)*((
card k-m) |^ card n) by A10,Th58;
take F;
card Perm =(card k)! by Th7;
then Sum F=(k!)*card Bloc by A64,A61;
then n block k=(Sum F*1)/(k!) by A62,STIRL2_1:def 2;
hence n block k= 1/(k!) * Sum F by XCMPLX_1:74;
thus dom F = k+1 by A63;
let m;
assume m in dom F;
hence F.m=((-1)|^m)*(k choose m)*((k-m)|^ n) by A65;
end;
suppose
n=0 & k<>0;
hence thesis by A1;
end;
end;
hence thesis;
end;
theorem Th60:
for X1,Y1,X be finite set st (Y1 is empty implies X1 is empty) &
X c= X1 for F be 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 st x in X holds f.x=F.x}
proof
let X1,Y1,X be finite set such that
A1: Y1 is empty implies X1 is empty and
A2: X c= X1;
set XX=X1\X;
let F be Function of X1,Y1 such that
A3: F is one-to-one and
A4: card X1=card Y1;
deffunc F(set)=F.$1;
defpred P[Function,set,set] means $1 is one-to-one & rng ($1|XX) =F.:XX;
reconsider FX=F.:XX as finite set;
set F1={f where f is Function of XX,F.:XX:f is one-to-one};
A5: card XX= card X1 -card X by A2,CARD_2:44;
A6: for f be Function of X1,Y1 st (for x st x in X1\XX holds F(x)=f.x)
holds P[f,X1,Y1] iff P[f|XX,XX,F.:XX]
proof
let f be Function of X1,Y1 such that
A7: for x st x in X1\XX holds F(x)=f.x;
thus P[f,X1,Y1] implies P[f|XX,XX,F.:XX] by FUNCT_1:52;
thus P[f|XX,XX,F.:XX] implies P[f,X1,Y1]
proof
F is onto by A3,A4,FINSEQ_4:63;
then
A8: rng F=Y1 by FUNCT_2:def 3;
A9: rng (f|XX)=f.:XX & F.:((X1\XX)\/XX)=F.:(X1\XX)\/F.:XX by RELAT_1:115,120;
A10: dom (F|(X1\XX))= dom F /\(X1\XX) & dom F=X1 by A1,FUNCT_2:def 1
,RELAT_1:61;
A11: dom (f|(X1\XX))=dom f /\(X1\XX) & dom f=X1 by A1,FUNCT_2:def 1,RELAT_1:61
;
now
A12: X1\XX=X/\X1 & X/\X1=X by A2,XBOOLE_1:28,48;
let x be object such that
A13: x in dom (F|(X1\XX));
f.x=(f|(X1\XX)).x by A11,A10,A13,FUNCT_1:47;
hence F.x=(f|(X1\XX)).x by A7,A10,A13,A12;
end;
then f|(X1\XX)=F|(X1\XX) by A11,A10,FUNCT_1:46;
then
A14: rng (f|(X1\XX))=F.:(X1\XX) by RELAT_1:115;
A15: (X1\XX)\/ XX= X1 & rng (f|(X1\XX))=f.:(X1\XX) by RELAT_1:115,XBOOLE_1:45;
A16: X1=dom F & X1=dom f by A1,FUNCT_2:def 1;
A17: F.:dom F=rng F by RELAT_1:113;
assume
A18: P[f|XX,XX,F.:XX];
then rng (f|XX)=F.:XX;
then F.:X1=f.:X1 by A14,A15,A9,RELAT_1:120;
then rng F=rng f by A16,A17,RELAT_1:113;
then f is onto by A8,FUNCT_2:def 3;
hence thesis by A4,A18,FINSEQ_4:63;
end;
end;
set F2={f where f is Function of X1,Y1:f is one-to-one & rng(f|XX) c= F.:XX
& for x st x in X holds f.x=F.x};
set S2={f where f is Function of X1,Y1:P[f,X1,Y1]&rng (f|XX) c=F.:XX& (for x
st x in X1\XX holds f.x=F(x))};
A19: X1\XX=X/\X1 & X/\X1=X by A2,XBOOLE_1:28,48;
A20: S2 c= F2
proof
let x be object;
assume x in S2;
then ex f be Function of X1,Y1 st x=f & P[f,X1,Y1] & rng (f|XX) c=F.:XX &
for x st x in X1\XX holds f.x=F(x);
hence thesis by A19;
end;
dom F=X1 by A1,FUNCT_2:def 1;
then XX,F.:XX are_equipotent by A3,CARD_1:33;
then
A21: card XX=card (F.:XX) by CARD_1:5;
then card F1= card XX!/((card FX-'card XX)!) & card FX-'card XX=0 by Th6,
XREAL_1:232;
then
A22: card F1=(card X1 -' card X)! by A5,NEWTON:12,XREAL_0:def 2;
set S1={f where f is Function of XX,F.:XX:P[f,XX,F.:XX]};
A23: for x st x in X1\XX holds F(x) in Y1
proof
A24: X1=dom F by A1,FUNCT_2:def 1;
let x;
assume x in X1\XX;
then F.x in rng F by A24,FUNCT_1:def 3;
hence thesis;
end;
A25: F1 c= S1
proof
let x be object;
assume x in F1;
then consider f be Function of XX,FX such that
A26: x=f and
A27: f is one-to-one;
A28: f|XX=f;
f is onto by A21,A27,FINSEQ_4:63;
then rng f=FX by FUNCT_2:def 3;
hence thesis by A26,A27,A28;
end;
S1 c= F1
proof
let x be object;
assume x in S1;
then ex f be Function of XX,FX st f=x & P[f,XX,F.:XX];
hence thesis;
end;
then
A29: F1=S1 by A25;
A30: F2 c= S2
proof
let x be object;
assume x in F2;
then consider f be Function of X1,Y1 such that
A31: x=f and
A32: f is one-to-one and
A33: rng(f|XX) c= F.:XX and
A34: for x st x in X holds f.x=F.x;
dom f=X1 by A1,FUNCT_2:def 1;
then XX,f.:XX are_equipotent by A32,CARD_1:33;
then card XX=card (f.:XX) by CARD_1:5;
then card FX=card rng(f|XX) by A21,RELAT_1:115;
then rng(f|XX)=FX by A33,CARD_2:102;
hence thesis by A19,A31,A32,A34;
end;
A35: XX c= X1 & F.:XX c= Y1;
then XX c= dom F by A1,FUNCT_2:def 1;
then
A36: F.:XX is empty implies XX is empty by RELAT_1:119;
card S1=card S2 from STIRL2_1:sch 3(A23,A35,A36,A6);
hence thesis by A20,A30,A22,A29,XBOOLE_0:def 10;
end;
Lm4: for X,Y for F be Function of X,Y st dom F=X & F is one-to-one ex XF be
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 st x in X holds h.x<>F.x}& for n
st n in dom XF holds XF.n=((-1)|^n) * (card X!) / ((n+1)!)
proof
let X,Y;
let F be Function of X,Y such that
A1: dom F=X and
A2: F is one-to-one;
deffunc fy(object)=
{h where h is Function of X,rng F:h is one-to-one&h.$1=F.$1};
A3: for x being object st x in X holds fy(x) in bool Funcs(X,rng F)
proof
let x be object such that
A4: x in X;
fy(x) c= Funcs(X,rng F)
proof
let y be object;
assume y in fy(x);
then
A5: ex h be Function of X,rng F st y=h & h is one-to-one & h.x=F.x;
rng F<>{} by A1,A4,RELAT_1:42;
hence thesis by A5,FUNCT_2:8;
end;
hence thesis;
end;
consider Fy9 be Function of X,bool Funcs(X,rng F) such that
A6: for x being object st x in X holds Fy9.x = fy(x) from FUNCT_2:sch 2(A3);
defpred xf[object,object] means
for n,k st n=$1 & k=(card X)-(n+1) holds $2=k!;
A7: for x being object st x in Segm card X
ex y being object st y in NAT & xf[x,y]
proof
let x being object such that
A8: x in Segm card X;
reconsider n=x as Element of NAT by A8;
n < card X by A8,NAT_1:44;
then n+1<=card X by NAT_1:13;
then reconsider k=(card X)-(n+1) as Element of NAT by NAT_1:21;
xf[n, k!];
hence thesis;
end;
consider XF be Function of Segm card X,NAT such that
A9: for x being object st x in Segm card X
holds xf[x,XF.x] from FUNCT_2:sch 1(A7);
for y being object st y in dom Fy9 holds Fy9.y is finite
proof
let y be object;
assume
y in dom Fy9;
then Fy9.y in rng Fy9 by FUNCT_1:def 3;
hence thesis;
end;
then reconsider Fy=Fy9 as finite-yielding Function by FINSET_1:def 4;
reconsider rngF=rng F as finite set;
A10: dom XF=card X by FUNCT_2:def 1;
then reconsider XF as XFinSequence by AFINSQ_1:5;
reconsider XF as XFinSequence of NAT;
A11: for n st n in dom XF holds ex x,y st x<>y & for f st f in Choose(X,n+1,
x,y) holds card(Intersection(Fy,f,x))=XF.n
proof
let n such that
A12: n in dom XF;
n < len XF by A12,AFINSQ_1:86;
then n<card X by A10;
then
A13: n+1<=card X by NAT_1:13;
then reconsider c = card X-(n+1) as Element of NAT by NAT_1:21;
A14: card X-'(n+1)=c by A13,XREAL_1:233;
take 0,1;
thus 0<>1;
let f9 be Function;
assume f9 in Choose(X,n+1,0,1);
then consider f be Function of X,{0,1} such that
A15: f = f9 and
A16: card (f"{0})=n+1 by 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|Xf0) c= F
.:Xf0 & for x st x in f0 holds h.x=F.x};
A17: Intersection(Fy,f,0) c= S
proof
assume not Intersection(Fy,f,0) c= S;
then consider z being object such that
A18: z in Intersection(Fy,f,0) and
A19: not z in S;
consider x9 be object such that
A20: x9 in f"{0} by A16,CARD_1:27,XBOOLE_0:def 1;
f.x9 in {0} by A20,FUNCT_1:def 7;
then
A21: f.x9=0 by TARSKI:def 1;
x9 in dom f by A20,FUNCT_1:def 7;
then 0 in rng f by A21,FUNCT_1:def 3;
then consider x such that
A22: x in dom f and
f.x=0 and
A23: z in Fy.x by A18,Th21;
z in fy(x) by A6,A22,A23;
then consider h be Function of X,rng F such that
A24: z=h and
A25: h is one-to-one and
h.x=F.x;
A26: for x1 st x1 in f0 holds h.x1=F.x1
proof
let x1 such that
A27: x1 in f0;
f.x1 in {0} by A27,FUNCT_1:def 7;
then
A28: f.x1 =0 by TARSKI:def 1;
Fy9.x1=fy(x1) & x1 in dom f by A6,A27,FUNCT_1:def 7;
then h in fy(x1) by A18,A24,A28,Def2;
then
ex h9 be Function of X,rng F st h=h9 & h9 is one-to-one & h9.x1=F .x1;
hence thesis;
end;
rng (h|Xf0) c= F.:Xf0
proof
assume not rng (h|Xf0) c= F.:Xf0;
then consider y being object such that
A29: y in rng (h|Xf0) and
A30: not y in F.:Xf0;
consider x1 being object such that
A31: x1 in dom (h|Xf0) and
A32: (h|Xf0).x1=y by A29,FUNCT_1:def 3;
A33: h.x1=y by A31,A32,FUNCT_1:47;
x1 in dom h /\ Xf0 by A31,RELAT_1:61;
then
A34: x1 in Xf0 by XBOOLE_0:def 4;
A35: F.:(X\Xf0)=F.:X\F.:Xf0 by A2,FUNCT_1:64;
rngF= F.:X by A1,RELAT_1:113;
then y in F.:X\F.:Xf0 by A29,A30,XBOOLE_0:def 5;
then consider x2 being object such that
A36: x2 in dom F and
A37: x2 in X\Xf0 and
A38: y = F.x2 by A35,FUNCT_1:def 6;
y in rng F by A36,A38,FUNCT_1:def 3;
then
A39: X=dom h by FUNCT_2:def 1;
X\Xf0=X/\f"{0} by XBOOLE_1:48;
then x2 in f"{0} by A37,XBOOLE_0:def 4;
then
A40: h.x2=y by A26,A38;
not x2 in Xf0 by A37,XBOOLE_0:def 5;
hence contradiction by A25,A36,A40,A33,A39,A34;
end;
hence thesis by A19,A24,A25,A26;
end;
A41: X,rngF are_equipotent by A1,A2,WELLORD2:def 4;
then
A42: card rngF=card X by CARD_1:5;
card rngF=card X by A41,CARD_1:5;
then
A43: rngF={} implies X is empty;
A44: F is Function of X,rngF by A1,FUNCT_2:1;
S c= Intersection(Fy,f,0)
proof
assume not S c= Intersection(Fy,f,0);
then consider z being object such that
A45: z in S and
A46: not z in Intersection(Fy,f,0);
consider h be Function of X,rng F such that
A47: h=z and
A48: h is one-to-one and
rng (h|Xf0) c= F.:Xf0 and
A49: for x st x in f0 holds h.x=F.x by A45;
consider x being object such that
A50: x in f"{0} by A16,CARD_1:27,XBOOLE_0:def 1;
x in X by A50;
then x in dom Fy9 by FUNCT_2:def 1;
then
A51: Fy9.x in rng Fy9 by FUNCT_1:def 3;
A52: Fy9.x=fy(x) by A6,A50;
h.x=F.x by A49,A50;
then h in Fy9.x by A48,A52;
then h in union rng Fy9 by A51,TARSKI:def 4;
then consider y such that
A53: y in dom f and
A54: f.y=0 and
A55: not h in Fy.y by A46,A47,Def2;
f.y in {0} by A54,TARSKI:def 1;
then y in f"{0} by A53,FUNCT_1:def 7;
then h.y=F.y by A49;
then h in fy(y) by A48;
hence contradiction by A6,A53,A55;
end;
then S = Intersection(Fy,f,0) by A17;
then card Intersection(Fy,f,0)=(card X-'(n+1))! by A2,A16,A43,A44,A42,Th60;
hence thesis by A9,A10,A12,A15,A14;
end;
A56: X,rngF are_equipotent by A1,A2,WELLORD2:def 4;
then card rngF=card X by CARD_1:5;
then
A57: (card rngF-'card X)!=1 & card {f where f is Function of X,rngF:f is
one-to-one}= card rngF!/(( card rngF-'card X)!) by Th6,NEWTON:12,XREAL_1:232;
then reconsider
One={f where f is Function of X,rng F:f is one-to-one} as finite
set;
set S={h where h is Function of X,rng F: h is one-to-one & for x st x in X
holds h.x<>F.x};
dom XF= card X & dom Fy = X by FUNCT_2:def 1;
then consider F9 be XFinSequence of INT such that
A58: dom F9=card X and
A59: card union rng Fy = Sum F9 and
A60: for n st n in dom F9 holds F9.n=((-1)|^n)*XF.n*(card X choose (n+1
)) by A11,Th57;
A61: union rng Fy9 c= One
proof
let x be object;
assume x in union rng Fy9;
then consider Fyx be set such that
A62: x in Fyx and
A63: Fyx in rng Fy9 by TARSKI:def 4;
consider x1 being object such that
A64: x1 in dom Fy9 & Fy.x1=Fyx by A63,FUNCT_1:def 3;
x in fy(x1) by A6,A62,A64;
then ex h be Function of X,rng F st h=x & h is one-to-one & h.x1=F.x1;
hence thesis;
end;
reconsider u=union rng Fy as finite set;
A65: card(One\u) = card One - card u by A61,CARD_2:44;
take F9;
thus dom F9 = card X by A58;
A66: One \ union rng Fy c= S
proof
let x be object such that
A67: x in One \ union rng Fy;
x in One by A67;
then consider f be Function of X,rng F such that
A68: f=x and
A69: f is one-to-one;
assume not x in S;
then consider x such that
A70: x in X and
A71: f.x=F.x by A68,A69;
x in dom Fy by A70,FUNCT_2:def 1;
then Fy.x in rng Fy by FUNCT_1:def 3;
then
A72: fy(x) in rng Fy by A6,A70;
f in fy(x) by A69,A71;
then f in union rng Fy by A72,TARSKI:def 4;
hence thesis by A67,A68,XBOOLE_0:def 5;
end;
A73: S c= One \ union rng Fy
proof
let x be object;
assume x in S;
then consider f be Function of X,rng F such that
A74: x=f and
A75: f is one-to-one and
A76: for x st x in X holds f.x<>F.x;
assume
A77: not x in One \ union rng Fy;
f in One by A75;
then f in union rng Fy by A74,A77,XBOOLE_0:def 5;
then consider Fyy be set such that
A78: f in Fyy and
A79: Fyy in rng Fy by TARSKI:def 4;
consider y being object such that
A80: y in dom Fy and
A81: Fy.y=Fyy by A79,FUNCT_1:def 3;
y in X by A80,FUNCT_2:def 1;
then f in fy(y) by A6,A78,A81;
then
A82: ex g be Function of X,rng F st f=g & g is one-to-one & g.y=F.y;
y in X by A80,FUNCT_2:def 1;
hence contradiction by A76,A82;
end;
card One = (card X)! by A56,A57,CARD_1:5;
hence card S=(card X)! - Sum F9 by A59,A66,A73,A65,XBOOLE_0:def 10;
let n such that
A83: n in dom F9;
n < len F9 by A83,AFINSQ_1:86;
then n<card X by A58;
then
A84: n+1 <=card X by NAT_1:13;
then reconsider c = card X-(n+1) as Element of NAT by NAT_1:21;
A85: card X choose (n+1)=((card X!))/((c!) * ((n+1)!)) by A84,NEWTON:def 3;
XF.n=c! by A9,A58,A83;
then
A87: XF.n*(card X choose (n+1))=(c! *(card X!))/((c!) * ((n+1)!)) by A85,
XCMPLX_1:74
.=(card X!)*(c!/((c!) * ((n+1)!))) by XCMPLX_1:74
.=(card X!)*((c!) / (c!) / ((n+1)!)) by XCMPLX_1:78
.=(card X!)*(1 / ((n+1)!)) by XCMPLX_1:60
.=(card X!*1)/ ((n+1)!) by XCMPLX_1:74;
F9.n=((-1)|^n)*XF.n*(card X choose (n+1)) by A60,A83
.=((-1)|^n)*(card X!/ ((n+1)!)) by A87;
hence thesis by XCMPLX_1:74;
end;
theorem Th61:
for F be Function st dom F=X & F is one-to-one ex XF be
XFinSequence of INT st Sum XF=card {h where h is Function of X,rng F: h is
one-to-one & for x st x in X holds h.x<>F.x}& dom XF = card X +1 & for n st n
in dom XF holds XF.n=((-1)|^n)*(card X!)/(n!)
proof
let F9 be Function such that
A1: dom F9=X and
A2: F9 is one-to-one;
X,rng F9 are_equipotent by A1,A2,WELLORD2:def 4;
then card X=card rng F9 by CARD_1:5;
then reconsider rngF=rng F9 as finite set;
reconsider F=F9 as Function of X,rngF by A1,FUNCT_2:1;
set S={h where h is Function of X,rng F9: h is one-to-one & for x st x in X
holds h.x<>F9.x};
rng F9=rng F;
then consider Xf be XFinSequence of INT such that
A3: dom Xf = card X and
A4: (card X)!-Sum Xf=card S and
A5: for n st n in dom Xf holds Xf.n=((-1)|^n)*(card X!)/((n+1)!) by A1,A2,Lm4;
reconsider c = (card X)! as Element of INT by INT_1:def 2;
A6: len <%c%>=1 by AFINSQ_1:33;
set F1 = (-1)(#)Xf;
A7: dom F1=card X by A3,VALUED_1:def 5;
reconsider F1 as XFinSequence of INT;
set XF=<%c%>^F1;
take XF;
(-1)*Sum Xf =Sum F1 by AFINSQ_2:64;
then c -Sum Xf=c +Sum F1 .=addint.(c,Sum F1) by BINOP_2:def 20
.=addint.(addint "**" <%c%>,Sum F1) by AFINSQ_2:37
.=addint.(addint "**" <%c%>,addint "**" F1) by AFINSQ_2:50
.=addint "**" XF by AFINSQ_2:42
.=Sum XF by AFINSQ_2:50;
hence Sum XF=card S by A4;
len F1=card X by A3,VALUED_1:def 5;
hence
A8: dom XF = card X +1 by A6,AFINSQ_1:def 3;
let n such that
A9: n in dom XF;
per cases;
suppose
A10: n=0;
then ((-1)|^n)=1 by NEWTON:4;
hence thesis by A10,AFINSQ_1:35,NEWTON:12;
end;
suppose
n>0;
then reconsider n1=n-1 as Element of NAT by NAT_1:20;
n1+1=n;
then
A11: (-1)*((-1)|^n1)=(-1)|^n by NEWTON:6;
n < len XF by A9,AFINSQ_1:86;
then n < card X +1 by A8;
then n1+1 <= card X by NAT_1:13;
then n1 < len F1 by A7,NAT_1:13;
then
A12: n1 in dom F1 by AFINSQ_1:86;
len <% c %>=1 by AFINSQ_1:33;
then XF.(n1+1)=F1.n1 by A12,AFINSQ_1:def 3;
then
A13: XF.(n1+1)=(-1)*Xf.n1 by VALUED_1:6;
Xf.n1=(((-1)|^n1)*(card X!))/((n1+1)!) by A3,A5,A7,A12;
then XF.n=((-1)*(((-1)|^n1)*(card X!)))/(n!) by A13,XCMPLX_1:74;
hence thesis by A11;
end;
end;
:: disorders
theorem
ex XF be XFinSequence of INT st Sum XF=card {h where h is Function of
X,X: h is one-to-one & for x st x in X holds h.x<>x}& dom XF = card X+1 & for n
st n in dom XF holds XF.n=((-1)|^n)*(card X!)/(n!)
proof
set S1={h where h is Function of X,X: h is one-to-one & for x st x in X
holds h.x<>(id X).x};
set S2={h where h is Function of X,X: h is one-to-one & for x st x in X
holds h.x<>x};
A1: S2 c= S1
proof
let x be object;
assume x in S2;
then consider h be Function of X,X such that
A2: h=x & h is one-to-one and
A3: for y st y in X holds h.y<>y;
for y st y in X holds (id X).y<>h.y by A3,FUNCT_1:17;
hence thesis by A2;
end;
A4: dom id X=X & rng id X=X;
S1 c= S2
proof
let x be object;
assume x in S1;
then consider h be Function of X,X such that
A5: h=x & h is one-to-one and
A6: for y st y in X holds h.y<>(id X).y;
now
let y such that
A7: y in X;
(id X).y=y by A7,FUNCT_1:17;
hence h.y<>y by A6,A7;
end;
hence thesis by A5;
end;
then S1=S2 by A1;
hence thesis by A4,Th61;
end;