:: Cardinal Numbers and Finite Sets :: by Karol P\c{a}k :: :: Received May 24, 2005 :: Copyright (c) 2005-2019 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, XCMPLX_0, NEWTON; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, XBOOLE_0, FUNCT_1, FINSET_1; equalities FUNCOP_1, RELAT_1, ORDINAL1, CARD_1; 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; 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,STIRL2_1:60; 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 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 Xzy 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,STIRL2_1:60; 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,STIRL2_1:60; 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; rng {} c= {} & {} c= NAT; then reconsider XFS as XFinSequence of NAT by RELAT_1:def 19; 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,STIRL2_1:60; 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,STIRL2_1:60; 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,STIRL2_1:60; 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; kX9)=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,STIRL2_1:60; 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 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: n1card 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,STIRL2_1:60; 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,STIRL2_1:60; 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,STIRL2_1:60; 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 n1; 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 nF.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;