:: Cardinal Arithmetics :: by Grzegorz Bancerek :: :: Received March 6, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin theorem :: CARD_2:1 for x, X, Y being set st x in X & X,Y are_equipotent holds ( Y <> {} & ex x being set st x in Y ) proofend; theorem :: CARD_2:2 for X being set holds ( bool X, bool (card X) are_equipotent & card (bool X) = card (bool (card X)) ) proofend; deffunc H1( set ) -> set = $1 `1 ; theorem :: CARD_2:3 for Z, X, Y being set st Z in Funcs (X,Y) holds ( Z,X are_equipotent & card Z = card X ) proofend; Lm1: for A, B being Ordinal for x1, x2 being set st x1 <> x2 holds ( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) ) proofend; deffunc H2( set , set ) -> set = [:$1,{0}:] \/ [:$2,{1}:]; Lm2: for X, Y being set holds ( [:X,Y:],[:Y,X:] are_equipotent & card [:X,Y:] = card [:Y,X:] ) proofend; definition let M, N be Cardinal; funcM +` N -> Cardinal equals :: CARD_2:def 1 card (M +^ N); coherence card (M +^ N) is Cardinal ; commutativity for b1, M, N being Cardinal st b1 = card (M +^ N) holds b1 = card (N +^ M) proofend; funcM *` N -> Cardinal equals :: CARD_2:def 2 card [:M,N:]; coherence card [:M,N:] is Cardinal ; commutativity for b1, M, N being Cardinal st b1 = card [:M,N:] holds b1 = card [:N,M:] by Lm2; func exp (M,N) -> Cardinal equals :: CARD_2:def 3 card (Funcs (N,M)); coherence card (Funcs (N,M)) is Cardinal ; end; :: deftheorem defines +` CARD_2:def_1_:_ for M, N being Cardinal holds M +` N = card (M +^ N); :: deftheorem defines *` CARD_2:def_2_:_ for M, N being Cardinal holds M *` N = card [:M,N:]; :: deftheorem defines exp CARD_2:def_3_:_ for M, N being Cardinal holds exp (M,N) = card (Funcs (N,M)); theorem Th4: :: CARD_2:4 for X, Y being set holds ( [:X,Y:],[:Y,X:] are_equipotent & card [:X,Y:] = card [:Y,X:] ) by Lm2; theorem Th5: :: CARD_2:5 for X, Y, Z being set holds ( [:[:X,Y:],Z:],[:X,[:Y,Z:]:] are_equipotent & card [:[:X,Y:],Z:] = card [:X,[:Y,Z:]:] ) proofend; theorem Th6: :: CARD_2:6 for X, x being set holds ( X,[:X,{x}:] are_equipotent & card X = card [:X,{x}:] ) proofend; Lm3: for X, Y being set holds [:X,Y:],[:(card X),Y:] are_equipotent proofend; theorem Th7: :: CARD_2:7 for X, Y being set holds ( [:X,Y:],[:(card X),Y:] are_equipotent & [:X,Y:],[:X,(card Y):] are_equipotent & [:X,Y:],[:(card X),(card Y):] are_equipotent & card [:X,Y:] = card [:(card X),Y:] & card [:X,Y:] = card [:X,(card Y):] & card [:X,Y:] = card [:(card X),(card Y):] ) proofend; theorem Th8: :: CARD_2:8 for X1, Y1, X2, Y2 being set st X1,Y1 are_equipotent & X2,Y2 are_equipotent holds ( [:X1,X2:],[:Y1,Y2:] are_equipotent & card [:X1,X2:] = card [:Y1,Y2:] ) proofend; theorem :: CARD_2:9 for A, B being Ordinal for x1, x2 being set st x1 <> x2 holds ( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) ) by Lm1; theorem Th10: :: CARD_2:10 for K, M being Cardinal for x1, x2 being set st x1 <> x2 holds ( K +` M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent & K +` M = card ([:K,{x1}:] \/ [:M,{x2}:]) ) proofend; theorem Th11: :: CARD_2:11 for A, B being Ordinal holds ( A *^ B,[:A,B:] are_equipotent & card (A *^ B) = card [:A,B:] ) proofend; deffunc H3( set , set ) -> set = [:$1,{0}:] \/ [:$2,{1}:]; deffunc H4( set , set , set , set ) -> set = [:$1,{$3}:] \/ [:$2,{$4}:]; theorem Th12: :: CARD_2:12 for X1, Y1, X2, Y2, x1, x2, y1, y2 being set st X1,Y1 are_equipotent & X2,Y2 are_equipotent & x1 <> x2 & y1 <> y2 holds ( [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent & card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:]) ) proofend; theorem Th13: :: CARD_2:13 for A, B being Ordinal holds card (A +^ B) = (card A) +` (card B) proofend; theorem Th14: :: CARD_2:14 for A, B being Ordinal holds card (A *^ B) = (card A) *` (card B) proofend; theorem :: CARD_2:15 for X, Y being set holds ( [:X,{0}:] \/ [:Y,{1}:],[:Y,{0}:] \/ [:X,{1}:] are_equipotent & card ([:X,{0}:] \/ [:Y,{1}:]) = card ([:Y,{0}:] \/ [:X,{1}:]) ) by Th12; theorem Th16: :: CARD_2:16 for X1, X2, Y1, Y2 being set holds ( [:X1,X2:] \/ [:Y1,Y2:],[:X2,X1:] \/ [:Y2,Y1:] are_equipotent & card ([:X1,X2:] \/ [:Y1,Y2:]) = card ([:X2,X1:] \/ [:Y2,Y1:]) ) proofend; theorem Th17: :: CARD_2:17 for x, y, X, Y being set st x <> y holds (card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:]) proofend; theorem :: CARD_2:18 for M being Cardinal holds M +` 0 = M proofend; Lm4: for x, y, X, Y being set st x <> y holds [:X,{x}:] misses [:Y,{y}:] proofend; theorem Th19: :: CARD_2:19 for K, M, N being Cardinal holds (K +` M) +` N = K +` (M +` N) proofend; theorem :: CARD_2:20 for K being Cardinal holds K *` 0 = 0 ; theorem Th21: :: CARD_2:21 for K being Cardinal holds K *` 1 = K proofend; theorem Th22: :: CARD_2:22 for K, M, N being Cardinal holds (K *` M) *` N = K *` (M *` N) proofend; theorem Th23: :: CARD_2:23 for K being Cardinal holds 2 *` K = K +` K proofend; theorem Th24: :: CARD_2:24 for K, M, N being Cardinal holds K *` (M +` N) = (K *` M) +` (K *` N) proofend; theorem :: CARD_2:25 for K being Cardinal holds exp (K,0) = 1 proofend; theorem :: CARD_2:26 for K being Cardinal st K <> 0 holds exp (0,K) = 0 ; theorem :: CARD_2:27 for K being Cardinal holds ( exp (K,1) = K & exp (1,K) = 1 ) proofend; theorem :: CARD_2:28 for K, M, N being Cardinal holds exp (K,(M +` N)) = (exp (K,M)) *` (exp (K,N)) proofend; theorem :: CARD_2:29 for K, M, N being Cardinal holds exp ((K *` M),N) = (exp (K,N)) *` (exp (M,N)) proofend; theorem :: CARD_2:30 for K, M, N being Cardinal holds exp (K,(M *` N)) = exp ((exp (K,M)),N) proofend; :: [WP: ] The_Number_of_Subsets_of_a_Set theorem :: CARD_2:31 for X being set holds exp (2,(card X)) = card (bool X) proofend; theorem :: CARD_2:32 for K being Cardinal holds exp (K,2) = K *` K by CARD_1:50, FUNCT_5:66; theorem :: CARD_2:33 for K, M being Cardinal holds exp ((K +` M),2) = ((K *` K) +` ((2 *` K) *` M)) +` (M *` M) proofend; theorem Th34: :: CARD_2:34 for X, Y being set holds card (X \/ Y) c= (card X) +` (card Y) proofend; theorem Th35: :: CARD_2:35 for X, Y being set st X misses Y holds card (X \/ Y) = (card X) +` (card Y) proofend; theorem Th36: :: CARD_2:36 for n, m being Element of NAT holds n + m = n +^ m proofend; theorem Th37: :: CARD_2:37 for n, m being Element of NAT holds n * m = n *^ m proofend; theorem Th38: :: CARD_2:38 for n, m being Element of NAT holds card (n + m) = (card n) +` (card m) proofend; theorem Th39: :: CARD_2:39 for n, m being Element of NAT holds card (n * m) = (card n) *` (card m) proofend; theorem Th40: :: CARD_2:40 for X, Y being finite set st X misses Y holds card (X \/ Y) = (card X) + (card Y) proofend; theorem Th41: :: CARD_2:41 for x being set for X being finite set st not x in X holds card (X \/ {x}) = (card X) + 1 proofend; theorem Th42: :: CARD_2:42 for X being set holds ( card X = 1 iff ex x being set st X = {x} ) proofend; theorem Th43: :: CARD_2:43 for X, Y being finite set holds card (X \/ Y) <= (card X) + (card Y) proofend; theorem Th44: :: CARD_2:44 for X, Y being finite set st Y c= X holds card (X \ Y) = (card X) - (card Y) proofend; theorem :: CARD_2:45 for X, Y being finite set holds card (X \/ Y) = ((card X) + (card Y)) - (card (X /\ Y)) proofend; theorem :: CARD_2:46 for X, Y being finite set holds card [:X,Y:] = (card X) * (card Y) proofend; theorem :: CARD_2:47 for f being finite Function holds card (rng f) <= card (dom f) by CARD_1:12, NAT_1:39; theorem :: CARD_2:48 for X, Y being finite set st X c< Y holds ( card X < card Y & card X in card Y ) proofend; theorem :: CARD_2:49 for X, Y being set st ( card X c= card Y or card X in card Y ) & Y is finite holds X is finite proofend; theorem Th50: :: CARD_2:50 for x1, x2 being set holds card {x1,x2} <= 2 proofend; theorem Th51: :: CARD_2:51 for x1, x2, x3 being set holds card {x1,x2,x3} <= 3 proofend; theorem Th52: :: CARD_2:52 for x1, x2, x3, x4 being set holds card {x1,x2,x3,x4} <= 4 proofend; theorem Th53: :: CARD_2:53 for x1, x2, x3, x4, x5 being set holds card {x1,x2,x3,x4,x5} <= 5 proofend; theorem Th54: :: CARD_2:54 for x1, x2, x3, x4, x5, x6 being set holds card {x1,x2,x3,x4,x5,x6} <= 6 proofend; theorem Th55: :: CARD_2:55 for x1, x2, x3, x4, x5, x6, x7 being set holds card {x1,x2,x3,x4,x5,x6,x7} <= 7 proofend; theorem :: CARD_2:56 for x1, x2, x3, x4, x5, x6, x7, x8 being set holds card {x1,x2,x3,x4,x5,x6,x7,x8} <= 8 proofend; theorem Th57: :: CARD_2:57 for x1, x2 being set st x1 <> x2 holds card {x1,x2} = 2 proofend; theorem Th58: :: CARD_2:58 for x1, x2, x3 being set st x1 <> x2 & x1 <> x3 & x2 <> x3 holds card {x1,x2,x3} = 3 proofend; theorem Th59: :: CARD_2:59 for x1, x2, x3, x4 being set st x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds card {x1,x2,x3,x4} = 4 proofend; begin :: from GROUP_3 theorem :: CARD_2:60 for X being set st card X = 2 holds ex x, y being set st ( x <> y & X = {x,y} ) proofend; :: from YELLOW_6, 2004.07.25 theorem :: CARD_2:61 for f being Function holds card (rng f) c= card (dom f) proofend; Lm5: now__::_thesis:_for_n_being_Element_of_NAT_st_(_for_Z_being_finite_set_st_card_Z_=_n_&_Z_<>_{}_&_(_for_X,_Y_being_set_st_X_in_Z_&_Y_in_Z_&_not_X_c=_Y_holds_ Y_c=_X_)_holds_ union_Z_in_Z_)_holds_ for_Z_being_finite_set_st_card_Z_=_n_+_1_&_Z_<>_{}_&_(_for_X,_Y_being_set_st_X_in_Z_&_Y_in_Z_&_not_X_c=_Y_holds_ Y_c=_X_)_holds_ union_Z_in_Z let n be Element of NAT ; ::_thesis: ( ( for Z being finite set st card Z = n & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds Y c= X ) holds union Z in Z ) implies for Z being finite set st card Z = n + 1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds Y c= X ) holds union b3 in b3 ) assume A1: for Z being finite set st card Z = n & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds Y c= X ) holds union Z in Z ; ::_thesis: for Z being finite set st card Z = n + 1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds Y c= X ) holds union b3 in b3 let Z be finite set ; ::_thesis: ( card Z = n + 1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds Y c= X ) implies union b2 in b2 ) assume that A2: card Z = n + 1 and A3: Z <> {} and A4: for X, Y being set st X in Z & Y in Z & not X c= Y holds Y c= X ; ::_thesis: union b2 in b2 set y = the Element of Z; percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: union b2 in b2 then consider x being set such that A5: Z = {x} by A2, Th42; union Z = x by A5, ZFMISC_1:25; hence union Z in Z by A5, TARSKI:def_1; ::_thesis: verum end; supposeA6: n <> 0 ; ::_thesis: union b2 in b2 set Y = Z \ { the Element of Z}; reconsider Y = Z \ { the Element of Z} as finite set ; { the Element of Z} c= Z by A3, ZFMISC_1:31; then A7: card Y = (n + 1) - (card { the Element of Z}) by A2, Th44 .= (n + 1) - 1 by CARD_1:30 .= n ; for a, b being set st a in Y & b in Y & not a c= b holds b c= a by A4; then A8: union Y in Y by A1, A6, A7, CARD_1:27; then A9: union Y in Z ; Z = (Z \ { the Element of Z}) \/ { the Element of Z} proof thus Z c= (Z \ { the Element of Z}) \/ { the Element of Z} :: according toXBOOLE_0:def_10 ::_thesis: (Z \ { the Element of Z}) \/ { the Element of Z} c= Z proof let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in Z or x in (Z \ { the Element of Z}) \/ { the Element of Z} ) assume x in Z ; ::_thesis: x in (Z \ { the Element of Z}) \/ { the Element of Z} then ( x in Z \ { the Element of Z} or x in { the Element of Z} ) by XBOOLE_0:def_5; hence x in (Z \ { the Element of Z}) \/ { the Element of Z} by XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in (Z \ { the Element of Z}) \/ { the Element of Z} or x in Z ) assume x in (Z \ { the Element of Z}) \/ { the Element of Z} ; ::_thesis: x in Z then A10: ( x in Z \ { the Element of Z} or x in { the Element of Z} ) by XBOOLE_0:def_3; { the Element of Z} c= Z by A3, ZFMISC_1:31; hence x in Z by A10; ::_thesis: verum end; then A11: union Z = (union Y) \/ (union { the Element of Z}) by ZFMISC_1:78 .= (union Y) \/ the Element of Z by ZFMISC_1:25 ; A12: the Element of Z in Z by A3; ( the Element of Z c= union Y or union Y c= the Element of Z ) by A4, A8; hence union Z in Z by A9, A12, A11, XBOOLE_1:12; ::_thesis: verum end; end; end; Lm6: for Z being finite set st Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds Y c= X ) holds union Z in Z proofend; theorem :: CARD_2:62 for Z being set st Z <> {} & Z is finite & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds Y c= X ) holds union Z in Z by Lm6; theorem :: CARD_2:63 for x1, x2, x3, x4, x5 being set st x1,x2,x3,x4,x5 are_mutually_different holds card {x1,x2,x3,x4,x5} = 5 proofend; :: from MATRIX_1, 2007.07.22, A.T, generalized theorem :: CARD_2:64 for M1, M2 being set st card M1 = 0 & card M2 = 0 holds M1 = M2 proofend; :: missing, 2007.06.14, A.T. registration let x, y be set ; cluster[x,y] -> non natural ; coherence not [x,y] is natural proofend; end; begin theorem :: CARD_2:65 for M, N being Cardinal holds Sum (M --> N) = M *` N proofend; theorem :: CARD_2:66 for N, M being Cardinal holds Product (N --> M) = exp (M,N) by CARD_3:11; scheme :: CARD_2:sch 1 FinRegularity{ F1() -> finite set , P1[ set , set ] } : ex x being set st ( x in F1() & ( for y being set st y in F1() & y <> x holds not P1[y,x] ) ) provided A1: F1() <> {} and A2: for x, y being set st P1[x,y] & P1[y,x] holds x = y and A3: for x, y, z being set st P1[x,y] & P1[y,z] holds P1[x,z] proofend; scheme :: CARD_2:sch 2 MaxFinSetElem{ F1() -> finite set , P1[ set , set ] } : ex x being set st ( x in F1() & ( for y being set st y in F1() holds P1[x,y] ) ) provided A1: F1() <> {} and A2: for x, y being set holds ( P1[x,y] or P1[y,x] ) and A3: for x, y, z being set st P1[x,y] & P1[y,z] holds P1[x,z] proofend; Lm7: for n being Nat st Rank n is finite holds Rank (n + 1) is finite proofend; Lm8: 1 = card 1 by CARD_1:def_2; Lm9: 2 = card 2 by CARD_1:def_2; theorem :: CARD_2:67 for n being Nat holds Rank n is finite proofend; theorem :: CARD_2:68 for M being Cardinal holds ( 0 in M iff 1 c= M ) proofend; theorem :: CARD_2:69 for M being Cardinal holds ( 1 in M iff 2 c= M ) proofend; theorem Th70: :: CARD_2:70 for A being Ordinal holds ( A is limit_ordinal iff for B being Ordinal for n being Nat st B in A holds B +^ n in A ) proofend; theorem Th71: :: CARD_2:71 for A being Ordinal for n being Nat holds ( A +^ (succ n) = (succ A) +^ n & A +^ (n + 1) = (succ A) +^ n ) proofend; theorem Th72: :: CARD_2:72 for A being Ordinal ex n being Nat st A *^ (succ 1) = A +^ n proofend; theorem Th73: :: CARD_2:73 for A being Ordinal st A is limit_ordinal holds A *^ (succ 1) = A proofend; Lm10: omega is limit_ordinal by ORDINAL1:def_11; theorem Th74: :: CARD_2:74 for A being Ordinal st omega c= A holds 1 +^ A = A proofend; registration cluster infinite cardinal -> limit_ordinal for set ; coherence for b1 being Cardinal st b1 is infinite holds b1 is limit_ordinal proofend; end; theorem Th75: :: CARD_2:75 for M being Cardinal st not M is finite holds M +` M = M proofend; theorem Th76: :: CARD_2:76 for M, N being Cardinal st not M is finite & ( N c= M or N in M ) holds ( M +` N = M & N +` M = M ) proofend; theorem :: CARD_2:77 for X, Y being set st not X is finite & ( X,Y are_equipotent or Y,X are_equipotent ) holds ( X \/ Y,X are_equipotent & card (X \/ Y) = card X ) proofend; theorem :: CARD_2:78 for X, Y being set st not X is finite & Y is finite holds ( X \/ Y,X are_equipotent & card (X \/ Y) = card X ) proofend; theorem :: CARD_2:79 for X, Y being set st not X is finite & ( card Y in card X or card Y c= card X ) holds ( X \/ Y,X are_equipotent & card (X \/ Y) = card X ) proofend; theorem :: CARD_2:80 for M, N being finite Cardinal holds M +` N is finite proofend; theorem :: CARD_2:81 for M, N being Cardinal st not M is finite holds ( not M +` N is finite & not N +` M is finite ) proofend; theorem :: CARD_2:82 for M, N being finite Cardinal holds M *` N is finite ; theorem Th83: :: CARD_2:83 for K, L, M, N being Cardinal st ( ( K in L & M in N ) or ( K c= L & M in N ) or ( K in L & M c= N ) or ( K c= L & M c= N ) ) holds ( K +` M c= L +` N & M +` K c= L +` N ) proofend; theorem :: CARD_2:84 for M, N, K being Cardinal st ( M in N or M c= N ) holds ( K +` M c= K +` N & K +` M c= N +` K & M +` K c= K +` N & M +` K c= N +` K ) by Th83; theorem Th85: :: CARD_2:85 for X, Y being set st X is countable & Y is countable holds X \/ Y is countable proofend; theorem Th86: :: CARD_2:86 for M, N being Cardinal for f being Function st card (dom f) c= M & ( for x being set st x in dom f holds card (f . x) c= N ) holds card (Union f) c= M *` N proofend; theorem :: CARD_2:87 for M, N being Cardinal for X being set st card X c= M & ( for Y being set st Y in X holds card Y c= N ) holds card (union X) c= M *` N proofend; theorem Th88: :: CARD_2:88 for f being Function st dom f is finite & ( for x being set st x in dom f holds f . x is finite ) holds Union f is finite proofend; theorem :: CARD_2:89 for n being Nat holds ( omega *` (card n) c= omega & (card n) *` omega c= omega ) proofend; theorem Th90: :: CARD_2:90 for K, L, M, N being Cardinal st ( ( K in L & M in N ) or ( K c= L & M in N ) or ( K in L & M c= N ) or ( K c= L & M c= N ) ) holds ( K *` M c= L *` N & M *` K c= L *` N ) proofend; theorem :: CARD_2:91 for M, N, K being Cardinal st ( M in N or M c= N ) holds ( K *` M c= K *` N & K *` M c= N *` K & M *` K c= K *` N & M *` K c= N *` K ) by Th90; theorem Th92: :: CARD_2:92 for K, L, M, N being Cardinal holds ( ( not ( K in L & M in N ) & not ( K c= L & M in N ) & not ( K in L & M c= N ) & not ( K c= L & M c= N ) ) or K = 0 or exp (K,M) c= exp (L,N) ) proofend; theorem :: CARD_2:93 for M, N, K being Cardinal holds ( ( not M in N & not M c= N ) or K = 0 or ( exp (K,M) c= exp (K,N) & exp (M,K) c= exp (N,K) ) ) proofend; theorem Th94: :: CARD_2:94 for M, N being Cardinal holds ( M c= M +` N & N c= M +` N ) proofend; theorem :: CARD_2:95 for N, M being Cardinal st N <> 0 holds ( M c= M *` N & M c= N *` M ) proofend; theorem Th96: :: CARD_2:96 for K, L, M, N being Cardinal st K in L & M in N holds ( K +` M in L +` N & M +` K in L +` N ) proofend; theorem :: CARD_2:97 for K, M, N being Cardinal st K +` M in K +` N holds M in N proofend; theorem :: CARD_2:98 for X, Y being set st (card X) +` (card Y) = card X & card Y in card X holds card (X \ Y) = card X proofend; theorem :: CARD_2:99 for K, M, N being Cardinal st K *` M in K *` N holds M in N proofend; theorem :: CARD_2:100 for X, Y being set st X is countable & Y is countable holds X \+\ Y is countable proofend; registration let A be finite set ; let B be set ; let f be Function of A,(Fin B); cluster Union f -> finite ; coherence Union f is finite proofend; end; registration let f be finite finite-yielding Function; cluster product f -> finite ; coherence product f is finite proofend; end; ::from COMPL_SP, 2011.07.30, A.T. theorem :: CARD_2:101 for F being Function st dom F is infinite & rng F is finite holds ex x being set st ( x in rng F & F " {x} is infinite ) proofend;