:: CARD_4 semantic presentation begin theorem :: CARD_4:1 for X being set st X is finite holds X is countable ; theorem :: CARD_4:2 omega is countable ; theorem Th3: :: CARD_4:3 for n being Nat for r being Real holds ( ( r <> 0 or n = 0 ) iff r |^ n <> 0 ) proof let n be Nat; ::_thesis: for r being Real holds ( ( r <> 0 or n = 0 ) iff r |^ n <> 0 ) let r be Real; ::_thesis: ( ( r <> 0 or n = 0 ) iff r |^ n <> 0 ) defpred S1[ Nat] means ( ( r <> 0 or \$1 = 0 ) iff r |^ \$1 <> 0 ); A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) A2: r |^ (k + 1) = (r |^ k) * r by NEWTON:6; assume S1[k] ; ::_thesis: S1[k + 1] hence S1[k + 1] by A2; ::_thesis: verum end; A3: S1[ 0 ] by NEWTON:4; for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1); hence ( ( r <> 0 or n = 0 ) iff r |^ n <> 0 ) ; ::_thesis: verum end; Lm1: for n1, m1, n2, m2 being Nat st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds n1 <= n2 proof let n1, m1, n2, m2 be Nat; ::_thesis: ( (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) implies n1 <= n2 ) assume A1: (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) ; ::_thesis: n1 <= n2 assume A2: n1 > n2 ; ::_thesis: contradiction then consider n being Nat such that A3: n1 = n2 + n by NAT_1:10; n <> 0 by A2, A3; then consider k being Nat such that A4: n = k + 1 by NAT_1:6; A5: 2 |^ n2 <> 0 by Th3; reconsider k = k as Element of NAT by ORDINAL1:def_12; 2 |^ n1 = (2 |^ n2) * (2 |^ (k + 1)) by A3, A4, NEWTON:8; then (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 |^ (k + 1)) * ((2 * m1) + 1)) ; then (2 |^ (k + 1)) * ((2 * m1) + 1) = (2 * m2) + 1 by A1, A5, XCMPLX_1:5; then (2 * m2) + 1 = ((2 |^ k) * (2 |^ 1)) * ((2 * m1) + 1) by NEWTON:8 .= (2 * (2 |^ k)) * ((2 * m1) + 1) by NEWTON:5 .= 2 * ((2 |^ k) * ((2 * m1) + 1)) ; then A6: 2 divides (2 * m2) + 1 by NAT_D:def_3; 2 divides 2 * m2 by NAT_D:def_3; hence contradiction by A6, NAT_D:7, NAT_D:10; ::_thesis: verum end; theorem Th4: :: CARD_4:4 for n1, m1, n2, m2 being Nat st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds ( n1 = n2 & m1 = m2 ) proof let n1, m1, n2, m2 be Nat; ::_thesis: ( (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) implies ( n1 = n2 & m1 = m2 ) ) A1: 2 |^ n1 <> 0 by Th3; assume A2: (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) ; ::_thesis: ( n1 = n2 & m1 = m2 ) then ( n1 <= n2 & n2 <= n1 ) by Lm1; hence n1 = n2 by XXREAL_0:1; ::_thesis: m1 = m2 then (2 * m1) + 1 = (2 * m2) + 1 by A2, A1, XCMPLX_1:5; hence m1 = m2 ; ::_thesis: verum end; Lm2: for x being set st x in [:NAT,NAT:] holds ex n1, n2 being Element of NAT st x = [n1,n2] proof let x be set ; ::_thesis: ( x in [:NAT,NAT:] implies ex n1, n2 being Element of NAT st x = [n1,n2] ) assume A1: x in [:NAT,NAT:] ; ::_thesis: ex n1, n2 being Element of NAT st x = [n1,n2] then reconsider n1 = x `1 , n2 = x `2 as Element of NAT by MCART_1:10; take n1 ; ::_thesis: ex n2 being Element of NAT st x = [n1,n2] take n2 ; ::_thesis: x = [n1,n2] thus x = [n1,n2] by A1, MCART_1:21; ::_thesis: verum end; theorem Th5: :: CARD_4:5 ( [:NAT,NAT:], NAT are_equipotent & card NAT = card [:NAT,NAT:] ) proof [:NAT,{0}:] c= [:NAT,NAT:] by ZFMISC_1:95; then card [:NAT,{0}:] c= card [:NAT,NAT:] by CARD_1:11; then A1: card NAT c= card [:NAT,NAT:] by CARD_1:69; deffunc H1( Element of NAT , Element of NAT ) -> Element of NAT = (2 |^ \$1) * ((2 * \$2) + 1); consider f being Function of [:NAT,NAT:],NAT such that A2: for n, m being Element of NAT holds f . (n,m) = H1(n,m) from BINOP_1:sch_4(); A3: f is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume x in dom f ; ::_thesis: ( not y in dom f or not f . x = f . y or x = y ) then consider n1, m1 being Element of NAT such that A4: x = [n1,m1] by Lm2; assume y in dom f ; ::_thesis: ( not f . x = f . y or x = y ) then consider n2, m2 being Element of NAT such that A5: y = [n2,m2] by Lm2; assume A6: f . x = f . y ; ::_thesis: x = y A7: (2 |^ n1) * ((2 * m1) + 1) = f . (n1,m1) by A2 .= f . (n2,m2) by A4, A5, A6 .= (2 |^ n2) * ((2 * m2) + 1) by A2 ; then n1 = n2 by Th4; hence x = y by A4, A5, A7, Th4; ::_thesis: verum end; ( dom f = [:NAT,NAT:] & rng f c= NAT ) by FUNCT_2:def_1; then card [:NAT,NAT:] c= card NAT by A3, CARD_1:10; then card NAT = card [:NAT,NAT:] by A1, XBOOLE_0:def_10; hence ( [:NAT,NAT:], NAT are_equipotent & card NAT = card [:NAT,NAT:] ) by CARD_1:5; ::_thesis: verum end; theorem Th6: :: CARD_4:6 omega *` omega = omega by Th5, CARD_1:47, CARD_2:def_2; theorem Th7: :: CARD_4:7 for X, Y being set st X is countable & Y is countable holds [:X,Y:] is countable proof let X, Y be set ; ::_thesis: ( X is countable & Y is countable implies [:X,Y:] is countable ) assume ( card X c= omega & card Y c= omega ) ; :: according to CARD_3:def_14 ::_thesis: [:X,Y:] is countable then [:(card X),(card Y):] c= [:omega,omega:] by ZFMISC_1:96; then card [:(card X),(card Y):] c= card [:omega,omega:] by CARD_1:11; then card [:(card X),(card Y):] c= omega *` omega by CARD_2:def_2; hence card [:X,Y:] c= omega by Th6, CARD_2:7; :: according to CARD_3:def_14 ::_thesis: verum end; theorem Th8: :: CARD_4:8 for D being non empty set holds ( 1 -tuples_on D,D are_equipotent & card (1 -tuples_on D) = card D ) proof let D be non empty set ; ::_thesis: ( 1 -tuples_on D,D are_equipotent & card (1 -tuples_on D) = card D ) deffunc H1( set ) -> set = <*\$1*>; consider f being Function such that A1: ( dom f = D & ( for x being set st x in D holds f . x = H1(x) ) ) from FUNCT_1:sch_3(); D,1 -tuples_on D are_equipotent proof take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = D & rng f = 1 -tuples_on D ) thus f is one-to-one ::_thesis: ( dom f = D & rng f = 1 -tuples_on D ) proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume ( x in dom f & y in dom f ) ; ::_thesis: ( not f . x = f . y or x = y ) then A2: ( f . x = <*x*> & f . y = <*y*> ) by A1; <*x*> . 1 = x by FINSEQ_1:def_8; hence ( not f . x = f . y or x = y ) by A2, FINSEQ_1:def_8; ::_thesis: verum end; thus dom f = D by A1; ::_thesis: rng f = 1 -tuples_on D thus rng f c= 1 -tuples_on D :: according to XBOOLE_0:def_10 ::_thesis: 1 -tuples_on D c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in 1 -tuples_on D ) assume x in rng f ; ::_thesis: x in 1 -tuples_on D then consider y being set such that A3: y in dom f and A4: x = f . y by FUNCT_1:def_3; reconsider y = y as Element of D by A1, A3; x = <*y*> by A1, A4; then x in { <*d*> where d is Element of D : verum } ; hence x in 1 -tuples_on D by FINSEQ_2:96; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in 1 -tuples_on D or x in rng f ) assume x in 1 -tuples_on D ; ::_thesis: x in rng f then reconsider y = x as Element of 1 -tuples_on D ; consider z being Element of D such that A5: y = <*z*> by FINSEQ_2:97; x = f . z by A1, A5; hence x in rng f by A1, FUNCT_1:def_3; ::_thesis: verum end; hence ( 1 -tuples_on D,D are_equipotent & card (1 -tuples_on D) = card D ) by CARD_1:5; ::_thesis: verum end; theorem Th9: :: CARD_4:9 for D being non empty set for n, m being Element of NAT holds ( [:(n -tuples_on D),(m -tuples_on D):],(n + m) -tuples_on D are_equipotent & card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D) ) proof let D be non empty set ; ::_thesis: for n, m being Element of NAT holds ( [:(n -tuples_on D),(m -tuples_on D):],(n + m) -tuples_on D are_equipotent & card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D) ) let n, m be Element of NAT ; ::_thesis: ( [:(n -tuples_on D),(m -tuples_on D):],(n + m) -tuples_on D are_equipotent & card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D) ) defpred S1[ set , set ] means ex p being Element of n -tuples_on D ex q being Element of m -tuples_on D st ( \$1 = [p,q] & \$2 = p ^ q ); set A = [:(n -tuples_on D),(m -tuples_on D):]; set B = (n + m) -tuples_on D; A1: for x being set st x in [:(n -tuples_on D),(m -tuples_on D):] holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in [:(n -tuples_on D),(m -tuples_on D):] implies ex y being set st S1[x,y] ) assume A2: x in [:(n -tuples_on D),(m -tuples_on D):] ; ::_thesis: ex y being set st S1[x,y] then reconsider p = x `1 as Element of n -tuples_on D by MCART_1:10; reconsider q = x `2 as Element of m -tuples_on D by A2, MCART_1:10; reconsider y = p ^ q as set ; take y ; ::_thesis: S1[x,y] x = [(x `1),(x `2)] by A2, MCART_1:21; hence S1[x,y] ; ::_thesis: verum end; consider f being Function such that A3: ( dom f = [:(n -tuples_on D),(m -tuples_on D):] & ( for x being set st x in [:(n -tuples_on D),(m -tuples_on D):] holds S1[x,f . x] ) ) from CLASSES1:sch_1(A1); thus [:(n -tuples_on D),(m -tuples_on D):],(n + m) -tuples_on D are_equipotent ::_thesis: card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D) proof take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = [:(n -tuples_on D),(m -tuples_on D):] & rng f = (n + m) -tuples_on D ) thus f is one-to-one ::_thesis: ( dom f = [:(n -tuples_on D),(m -tuples_on D):] & rng f = (n + m) -tuples_on D ) proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume x in dom f ; ::_thesis: ( not y in dom f or not f . x = f . y or x = y ) then consider p1 being Element of n -tuples_on D, q1 being Element of m -tuples_on D such that A4: x = [p1,q1] and A5: f . x = p1 ^ q1 by A3; assume y in dom f ; ::_thesis: ( not f . x = f . y or x = y ) then consider p2 being Element of n -tuples_on D, q2 being Element of m -tuples_on D such that A6: y = [p2,q2] and A7: f . y = p2 ^ q2 by A3; assume A8: f . x = f . y ; ::_thesis: x = y A9: ( len p1 = n & len p2 = n ) by CARD_1:def_7; then consider p being FinSequence such that A10: p1 ^ p = p2 by A5, A7, A8, FINSEQ_1:47; consider q being FinSequence such that A11: p2 ^ q = p1 by A5, A7, A8, A9, FINSEQ_1:47; (len p1) + 0 = (len (p1 ^ p)) + (len q) by A10, A11, FINSEQ_1:22 .= ((len p1) + (len p)) + (len q) by FINSEQ_1:22 .= (len p1) + ((len p) + (len q)) ; then p = {} ; then p1 = p2 by A10, FINSEQ_1:34; hence x = y by A4, A5, A6, A7, A8, FINSEQ_1:33; ::_thesis: verum end; thus dom f = [:(n -tuples_on D),(m -tuples_on D):] by A3; ::_thesis: rng f = (n + m) -tuples_on D thus rng f c= (n + m) -tuples_on D :: according to XBOOLE_0:def_10 ::_thesis: (n + m) -tuples_on D c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in (n + m) -tuples_on D ) assume x in rng f ; ::_thesis: x in (n + m) -tuples_on D then consider y being set such that A12: ( y in dom f & x = f . y ) by FUNCT_1:def_3; ex p being Element of n -tuples_on D ex q being Element of m -tuples_on D st ( y = [p,q] & x = p ^ q ) by A3, A12; then x is Tuple of n + m,D ; then x is Element of (n + m) -tuples_on D by FINSEQ_2:131; hence x in (n + m) -tuples_on D ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (n + m) -tuples_on D or x in rng f ) assume x in (n + m) -tuples_on D ; ::_thesis: x in rng f then reconsider x = x as Element of (n + m) -tuples_on D ; consider p being Element of n -tuples_on D, q being Element of m -tuples_on D such that A13: x = p ^ q by FINSEQ_2:106; consider p1 being Element of n -tuples_on D, q1 being Element of m -tuples_on D such that A14: [p,q] = [p1,q1] and A15: f . [p,q] = p1 ^ q1 by A3; ( p1 = p & q1 = q ) by A14, XTUPLE_0:1; hence x in rng f by A3, A13, A15, FUNCT_1:def_3; ::_thesis: verum end; hence card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D) by CARD_1:5; ::_thesis: verum end; theorem Th10: :: CARD_4:10 for D being non empty set for n being Element of NAT st D is countable holds n -tuples_on D is countable proof let D be non empty set ; ::_thesis: for n being Element of NAT st D is countable holds n -tuples_on D is countable let n be Element of NAT ; ::_thesis: ( D is countable implies n -tuples_on D is countable ) defpred S1[ Nat] means \$1 -tuples_on D is countable ; assume card D c= omega ; :: according to CARD_3:def_14 ::_thesis: n -tuples_on D is countable then card (1 -tuples_on D) c= omega by Th8; then A1: 1 -tuples_on D is countable by CARD_3:def_14; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] then [:(k -tuples_on D),(1 -tuples_on D):] is countable by A1, Th7; then A3: card [:(k -tuples_on D),(1 -tuples_on D):] c= omega by CARD_3:def_14; k in NAT by ORDINAL1:def_12; then card [:(k -tuples_on D),(1 -tuples_on D):] = card ((k + 1) -tuples_on D) by Th9; hence S1[k + 1] by A3, CARD_3:def_14; ::_thesis: verum end; {(<*> D)} is countable ; then A4: S1[ 0 ] by FINSEQ_2:94; for k being Nat holds S1[k] from NAT_1:sch_2(A4, A2); hence n -tuples_on D is countable ; ::_thesis: verum end; theorem Th11: :: CARD_4:11 for f being Function st dom f is countable & ( for x being set st x in dom f holds f . x is countable ) holds Union f is countable proof let f be Function; ::_thesis: ( dom f is countable & ( for x being set st x in dom f holds f . x is countable ) implies Union f is countable ) assume that A1: card (dom f) c= omega and A2: for x being set st x in dom f holds f . x is countable ; :: according to CARD_3:def_14 ::_thesis: Union f is countable now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ card_(f_._x)_c=_omega let x be set ; ::_thesis: ( x in dom f implies card (f . x) c= omega ) assume x in dom f ; ::_thesis: card (f . x) c= omega then f . x is countable by A2; hence card (f . x) c= omega by CARD_3:def_14; ::_thesis: verum end; hence card (Union f) c= omega by A1, Th6, CARD_2:86; :: according to CARD_3:def_14 ::_thesis: verum end; theorem :: CARD_4:12 for X being set st X is countable & ( for Y being set st Y in X holds Y is countable ) holds union X is countable proof let X be set ; ::_thesis: ( X is countable & ( for Y being set st Y in X holds Y is countable ) implies union X is countable ) assume that A1: card X c= omega and A2: for Y being set st Y in X holds Y is countable ; :: according to CARD_3:def_14 ::_thesis: union X is countable now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_ card_Y_c=_omega let Y be set ; ::_thesis: ( Y in X implies card Y c= omega ) assume Y in X ; ::_thesis: card Y c= omega then Y is countable by A2; hence card Y c= omega by CARD_3:def_14; ::_thesis: verum end; hence card (union X) c= omega by A1, Th6, CARD_2:87; :: according to CARD_3:def_14 ::_thesis: verum end; theorem :: CARD_4:13 for D being non empty set st D is countable holds D * is countable proof let D be non empty set ; ::_thesis: ( D is countable implies D * is countable ) defpred S1[ set , set ] means ex n being Element of NAT st ( \$1 = n & \$2 = n -tuples_on D ); A1: for x being set st x in NAT holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in NAT implies ex y being set st S1[x,y] ) assume x in NAT ; ::_thesis: ex y being set st S1[x,y] then reconsider n = x as Element of NAT ; reconsider y = n -tuples_on D as set ; take y ; ::_thesis: S1[x,y] take n ; ::_thesis: ( x = n & y = n -tuples_on D ) thus ( x = n & y = n -tuples_on D ) ; ::_thesis: verum end; consider f being Function such that A2: ( dom f = NAT & ( for x being set st x in NAT holds S1[x,f . x] ) ) from CLASSES1:sch_1(A1); A3: D * = union { (k -tuples_on D) where k is Element of NAT : verum } by FINSEQ_2:108; A4: Union f = D * proof thus Union f c= D * :: according to XBOOLE_0:def_10 ::_thesis: D * c= Union f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union f or x in D * ) assume x in Union f ; ::_thesis: x in D * then consider X being set such that A5: x in X and A6: X in rng f by TARSKI:def_4; consider y being set such that A7: y in dom f and A8: X = f . y by A6, FUNCT_1:def_3; reconsider y = y as Element of NAT by A2, A7; ex n being Element of NAT st ( y = n & X = n -tuples_on D ) by A2, A8; then X in { (k -tuples_on D) where k is Element of NAT : verum } ; hence x in D * by A3, A5, TARSKI:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D * or x in Union f ) assume x in D * ; ::_thesis: x in Union f then consider X being set such that A9: ( x in X & X in { (k -tuples_on D) where k is Element of NAT : verum } ) by A3, TARSKI:def_4; consider n being Element of NAT such that A10: X = n -tuples_on D by A9; ex k being Element of NAT st ( n = k & f . n = k -tuples_on D ) by A2; then X in rng f by A2, A10, FUNCT_1:def_3; hence x in Union f by A9, TARSKI:def_4; ::_thesis: verum end; assume A11: D is countable ; ::_thesis: D * is countable now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_is_countable let x be set ; ::_thesis: ( x in dom f implies f . x is countable ) assume x in dom f ; ::_thesis: f . x is countable then ex n being Element of NAT st ( x = n & f . x = n -tuples_on D ) by A2; hence f . x is countable by A11, Th10; ::_thesis: verum end; hence D * is countable by A2, A4, Th11; ::_thesis: verum end; theorem :: CARD_4:14 for D being non empty set holds omega c= card (D *) proof let D be non empty set ; ::_thesis: omega c= card (D *) defpred S1[ set , set ] means ex p being FinSequence st ( \$1 = p & \$2 = len p ); A1: ( {} in D * & len {} = 0 ) by FINSEQ_1:49; A2: for x being set st x in D * holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in D * implies ex y being set st S1[x,y] ) assume x in D * ; ::_thesis: ex y being set st S1[x,y] then reconsider p = x as Element of D * ; reconsider p = p as FinSequence ; reconsider y = len p as set ; take y ; ::_thesis: S1[x,y] take p ; ::_thesis: ( x = p & y = len p ) thus ( x = p & y = len p ) ; ::_thesis: verum end; consider f being Function such that A3: ( dom f = D * & ( for x being set st x in D * holds S1[x,f . x] ) ) from CLASSES1:sch_1(A2); defpred S2[ Nat] means \$1 in f .: (D *); A4: for n being Nat st S2[n] holds S2[n + 1] proof set y = the Element of D; let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] ) assume n in f .: (D *) ; ::_thesis: S2[n + 1] then consider x being set such that A5: x in dom f and A6: x in D * and A7: n = f . x by FUNCT_1:def_6; consider p being FinSequence such that A8: x = p and A9: n = len p by A3, A5, A7; reconsider p = p as FinSequence of D by A6, A8, FINSEQ_1:def_11; A10: len (p ^ <* the Element of D*>) = n + (len <* the Element of D*>) by A9, FINSEQ_1:22 .= n + 1 by FINSEQ_1:40 ; A11: p ^ <* the Element of D*> in D * by FINSEQ_1:def_11; then ex q being FinSequence st ( p ^ <* the Element of D*> = q & f . (p ^ <* the Element of D*>) = len q ) by A3; hence S2[n + 1] by A3, A11, A10, FUNCT_1:def_6; ::_thesis: verum end; ex p being FinSequence st ( {} = p & f . {} = len p ) by A3, FINSEQ_1:49; then A12: S2[ 0 ] by A3, A1, FUNCT_1:def_6; A13: for n being Nat holds S2[n] from NAT_1:sch_2(A12, A4); NAT c= f .: (D *) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NAT or x in f .: (D *) ) assume x in NAT ; ::_thesis: x in f .: (D *) then reconsider n = x as Element of NAT ; n in f .: (D *) by A13; hence x in f .: (D *) ; ::_thesis: verum end; hence omega c= card (D *) by CARD_1:47, CARD_1:66; ::_thesis: verum end; scheme :: CARD_4:sch 1 FraenCoun1{ F1( set ) -> set , P1[ set ] } : { F1(n) where n is Element of NAT : P1[n] } is countable proof consider f being Function such that A1: ( dom f = NAT & ( for x being set st x in NAT holds f . x = F1(x) ) ) from FUNCT_1:sch_3(); { F1(n) where n is Element of NAT : P1[n] } c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F1(n) where n is Element of NAT : P1[n] } or x in rng f ) assume x in { F1(n) where n is Element of NAT : P1[n] } ; ::_thesis: x in rng f then consider n being Element of NAT such that A2: x = F1(n) and P1[n] ; f . n = x by A1, A2; hence x in rng f by A1, FUNCT_1:def_3; ::_thesis: verum end; hence { F1(n) where n is Element of NAT : P1[n] } is countable by A1, CARD_3:93; ::_thesis: verum end; scheme :: CARD_4:sch 2 FraenCoun2{ F1( set , set ) -> set , P1[ set , set ] } : { F1(n1,n2) where n1, n2 is Element of NAT : P1[n1,n2] } is countable proof consider N being Function such that N is one-to-one and A1: dom N = NAT and A2: rng N = [:NAT,NAT:] by Th5, WELLORD2:def_4; deffunc H1( set ) -> set = F1(((N . \$1) `1),((N . \$1) `2)); consider f being Function such that A3: ( dom f = NAT & ( for x being set st x in NAT holds f . x = H1(x) ) ) from FUNCT_1:sch_3(); { F1(n1,n2) where n1, n2 is Element of NAT : P1[n1,n2] } c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F1(n1,n2) where n1, n2 is Element of NAT : P1[n1,n2] } or x in rng f ) assume x in { F1(n1,n2) where n1, n2 is Element of NAT : P1[n1,n2] } ; ::_thesis: x in rng f then consider n1, n2 being Element of NAT such that A4: x = F1(n1,n2) and P1[n1,n2] ; consider y being set such that A5: y in dom N and A6: [n1,n2] = N . y by A2, FUNCT_1:def_3; ( [n1,n2] `1 = n1 & [n1,n2] `2 = n2 ) ; then x = f . y by A1, A3, A4, A5, A6; hence x in rng f by A1, A3, A5, FUNCT_1:def_3; ::_thesis: verum end; hence { F1(n1,n2) where n1, n2 is Element of NAT : P1[n1,n2] } is countable by A3, CARD_3:93; ::_thesis: verum end; scheme :: CARD_4:sch 3 FraenCoun3{ F1( set , set , set ) -> set , P1[ set , set , set ] } : { F1(n1,n2,n3) where n1, n2, n3 is Element of NAT : P1[n1,n2,n3] } is countable proof [:NAT,NAT:],[:[:NAT,NAT:],NAT:] are_equipotent by Th5, CARD_2:8; then A1: NAT ,[:[:NAT,NAT:],NAT:] are_equipotent by Th5, WELLORD2:15; [:[:NAT,NAT:],NAT:] = [:NAT,NAT,NAT:] by ZFMISC_1:def_3; then consider N being Function such that N is one-to-one and A2: dom N = NAT and A3: rng N = [:NAT,NAT,NAT:] by A1, WELLORD2:def_4; deffunc H1( set ) -> set = F1((((N . \$1) `1) `1),(((N . \$1) `1) `2),((N . \$1) `2)); consider f being Function such that A4: ( dom f = NAT & ( for x being set st x in NAT holds f . x = H1(x) ) ) from FUNCT_1:sch_3(); { F1(n1,n2,n3) where n1, n2, n3 is Element of NAT : P1[n1,n2,n3] } c= rng f proof reconsider NAT9 = NAT as non empty set ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F1(n1,n2,n3) where n1, n2, n3 is Element of NAT : P1[n1,n2,n3] } or x in rng f ) assume x in { F1(n1,n2,n3) where n1, n2, n3 is Element of NAT : P1[n1,n2,n3] } ; ::_thesis: x in rng f then consider n1, n2, n3 being Element of NAT such that A5: x = F1(n1,n2,n3) and P1[n1,n2,n3] ; reconsider n1 = n1, n2 = n2, n3 = n3 as Element of NAT9 ; A6: ( [n1,n2,n3] `3_3 = n3 & [n1,n2,n3] `1_3 = ([n1,n2,n3] `1) `1 ) ; consider y being set such that A8: y in dom N and A9: [n1,n2,n3] = N . y by A3, FUNCT_1:def_3; ( [n1,n2,n3] `1_3 = n1 & [n1,n2,n3] `2_3 = n2 ) ; then x = f . y by A2, A4, A5, A8, A9, A6; hence x in rng f by A2, A4, A8, FUNCT_1:def_3; ::_thesis: verum end; hence { F1(n1,n2,n3) where n1, n2, n3 is Element of NAT : P1[n1,n2,n3] } is countable by A4, CARD_3:93; ::_thesis: verum end; theorem Th15: :: CARD_4:15 for M being Cardinal st not M is finite holds M *` M = M proof let M be Cardinal; ::_thesis: ( not M is finite implies M *` M = M ) defpred S1[ set ] means ex f being Function st ( f = \$1 & f is one-to-one & dom f = [:(rng f),(rng f):] ); consider X being set such that A1: for x being set holds ( x in X iff ( x in PFuncs ([:M,M:],M) & S1[x] ) ) from XBOOLE_0:sch_1(); A2: for x being set st x in X holds x is Function proof let x be set ; ::_thesis: ( x in X implies x is Function ) assume x in X ; ::_thesis: x is Function then ex f being Function st ( f = x & f is one-to-one & dom f = [:(rng f),(rng f):] ) by A1; hence x is Function ; ::_thesis: verum end; A3: for Z being set st Z <> {} & Z c= X & Z is c=-linear holds union Z in X proof let Z be set ; ::_thesis: ( Z <> {} & Z c= X & Z is c=-linear implies union Z in X ) assume that Z <> {} and A4: Z c= X and A5: Z is c=-linear ; ::_thesis: union Z in X ( union Z is Relation-like & union Z is Function-like ) proof set F = union Z; thus for x being set st x in union Z holds ex y1, y2 being set st [y1,y2] = x :: according to RELAT_1:def_1 ::_thesis: union Z is Function-like proof let x be set ; ::_thesis: ( x in union Z implies ex y1, y2 being set st [y1,y2] = x ) assume x in union Z ; ::_thesis: ex y1, y2 being set st [y1,y2] = x then consider Y being set such that A6: x in Y and A7: Y in Z by TARSKI:def_4; reconsider f = Y as Function by A2, A4, A7; for x being set st x in f holds ex y1, y2 being set st [y1,y2] = x by RELAT_1:def_1; hence ex y1, y2 being set st [y1,y2] = x by A6; ::_thesis: verum end; let x be set ; :: according to FUNCT_1:def_1 ::_thesis: for b1, b2 being set holds ( not [x,b1] in union Z or not [x,b2] in union Z or b1 = b2 ) let y1, y2 be set ; ::_thesis: ( not [x,y1] in union Z or not [x,y2] in union Z or y1 = y2 ) assume [x,y1] in union Z ; ::_thesis: ( not [x,y2] in union Z or y1 = y2 ) then consider X1 being set such that A8: [x,y1] in X1 and A9: X1 in Z by TARSKI:def_4; assume [x,y2] in union Z ; ::_thesis: y1 = y2 then consider X2 being set such that A10: [x,y2] in X2 and A11: X2 in Z by TARSKI:def_4; reconsider f1 = X1, f2 = X2 as Function by A2, A4, A9, A11; X1,X2 are_c=-comparable by A5, A9, A11, ORDINAL1:def_8; then ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9; then ( ( [x,y2] in X1 & ( for x, y1, y2 being set st [x,y1] in f1 & [x,y2] in f1 holds y1 = y2 ) ) or ( [x,y1] in X2 & ( for x, y1, y2 being set st [x,y1] in f2 & [x,y2] in f2 holds y1 = y2 ) ) ) by A8, A10, FUNCT_1:def_1; hence y1 = y2 by A8, A10; ::_thesis: verum end; then reconsider f = union Z as Function ; A12: f is one-to-one proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 ) assume that A13: x1 in dom f and A14: x2 in dom f ; ::_thesis: ( not f . x1 = f . x2 or x1 = x2 ) [x1,(f . x1)] in f by A13, FUNCT_1:1; then consider X1 being set such that A15: [x1,(f . x1)] in X1 and A16: X1 in Z by TARSKI:def_4; [x2,(f . x2)] in f by A14, FUNCT_1:1; then consider X2 being set such that A17: [x2,(f . x2)] in X2 and A18: X2 in Z by TARSKI:def_4; consider f2 being Function such that A19: f2 = X2 and A20: f2 is one-to-one and dom f2 = [:(rng f2),(rng f2):] by A1, A4, A18; consider f1 being Function such that A21: f1 = X1 and A22: f1 is one-to-one and dom f1 = [:(rng f1),(rng f1):] by A1, A4, A16; X1,X2 are_c=-comparable by A5, A16, A18, ORDINAL1:def_8; then ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9; then ( ( x1 in dom f1 & x2 in dom f1 & f . x1 = f1 . x1 & f . x2 = f1 . x2 ) or ( x1 in dom f2 & x2 in dom f2 & f . x1 = f2 . x1 & f . x2 = f2 . x2 ) ) by A15, A17, A21, A19, FUNCT_1:1; hence ( not f . x1 = f . x2 or x1 = x2 ) by A22, A20, FUNCT_1:def_4; ::_thesis: verum end; A23: dom f = [:(rng f),(rng f):] proof thus dom f c= [:(rng f),(rng f):] :: according to XBOOLE_0:def_10 ::_thesis: [:(rng f),(rng f):] c= dom f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in [:(rng f),(rng f):] ) assume x in dom f ; ::_thesis: x in [:(rng f),(rng f):] then [x,(f . x)] in f by FUNCT_1:def_2; then consider Y being set such that A24: [x,(f . x)] in Y and A25: Y in Z by TARSKI:def_4; consider g being Function such that A26: g = Y and g is one-to-one and A27: dom g = [:(rng g),(rng g):] by A1, A4, A25; g c= f by A25, A26, ZFMISC_1:74; then rng g c= rng f by RELAT_1:11; then A28: dom g c= [:(rng f),(rng f):] by A27, ZFMISC_1:96; x in dom g by A24, A26, FUNCT_1:1; hence x in [:(rng f),(rng f):] by A28; ::_thesis: verum end; let x1, x2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x1,x2] in [:(rng f),(rng f):] or [x1,x2] in dom f ) assume A29: [x1,x2] in [:(rng f),(rng f):] ; ::_thesis: [x1,x2] in dom f [x1,x2] `1 in rng f by A29, MCART_1:10; then consider y1 being set such that A31: ( y1 in dom f & [x1,x2] `1 = f . y1 ) by FUNCT_1:def_3; [x1,x2] `2 in rng f by A29, MCART_1:10; then consider y2 being set such that A32: ( y2 in dom f & [x1,x2] `2 = f . y2 ) by FUNCT_1:def_3; [y2,([x1,x2] `2)] in f by A32, FUNCT_1:1; then consider X2 being set such that A33: [y2,([x1,x2] `2)] in X2 and A34: X2 in Z by TARSKI:def_4; consider f2 being Function such that A35: f2 = X2 and f2 is one-to-one and A36: dom f2 = [:(rng f2),(rng f2):] by A1, A4, A34; f2 c= f by A34, A35, ZFMISC_1:74; then A37: dom f2 c= dom f by RELAT_1:11; [y1,([x1,x2] `1)] in f by A31, FUNCT_1:1; then consider X1 being set such that A38: [y1,([x1,x2] `1)] in X1 and A39: X1 in Z by TARSKI:def_4; consider f1 being Function such that A40: f1 = X1 and f1 is one-to-one and A41: dom f1 = [:(rng f1),(rng f1):] by A1, A4, A39; X1,X2 are_c=-comparable by A5, A39, A34, ORDINAL1:def_8; then ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9; then ( ( y1 in dom f1 & y2 in dom f1 & f1 . y1 = [x1,x2] `1 & f1 . y2 = [x1,x2] `2 ) or ( y1 in dom f2 & y2 in dom f2 & f2 . y1 = [x1,x2] `1 & f2 . y2 = [x1,x2] `2 ) ) by A38, A33, A40, A35, FUNCT_1:1; then ( ( [x1,x2] `1 in rng f1 & [x1,x2] `2 in rng f1 ) or ( [x1,x2] `1 in rng f2 & [x1,x2] `2 in rng f2 ) ) by FUNCT_1:def_3; then A42: ( [x1,x2] in dom f1 or [x1,x2] in dom f2 ) by A41, A36, ZFMISC_1:87; f1 c= f by A39, A40, ZFMISC_1:74; then dom f1 c= dom f by RELAT_1:11; hence [x1,x2] in dom f by A42, A37; ::_thesis: verum end; A43: rng f c= M proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in M ) assume y in rng f ; ::_thesis: y in M then consider x being set such that A44: ( x in dom f & y = f . x ) by FUNCT_1:def_3; [x,y] in union Z by A44, FUNCT_1:def_2; then consider Y being set such that A45: [x,y] in Y and A46: Y in Z by TARSKI:def_4; Y in PFuncs ([:M,M:],M) by A1, A4, A46; then consider g being Function such that A47: Y = g and dom g c= [:M,M:] and A48: rng g c= M by PARTFUN1:def_3; ( x in dom g & g . x = y ) by A45, A47, FUNCT_1:1; then y in rng g by FUNCT_1:def_3; hence y in M by A48; ::_thesis: verum end; dom f c= [:M,M:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in [:M,M:] ) assume x in dom f ; ::_thesis: x in [:M,M:] then [x,(f . x)] in union Z by FUNCT_1:def_2; then consider Y being set such that A49: [x,(f . x)] in Y and A50: Y in Z by TARSKI:def_4; Y in PFuncs ([:M,M:],M) by A1, A4, A50; then consider g being Function such that A51: Y = g and A52: dom g c= [:M,M:] and rng g c= M by PARTFUN1:def_3; x in dom g by A49, A51, FUNCT_1:1; hence x in [:M,M:] by A52; ::_thesis: verum end; then f in PFuncs ([:M,M:],M) by A43, PARTFUN1:def_3; hence union Z in X by A1, A12, A23; ::_thesis: verum end; consider f being Function such that A53: f is one-to-one and A54: ( dom f = [:omega,omega:] & rng f = omega ) by Th5, WELLORD2:def_4; assume A55: not M is finite ; ::_thesis: M *` M = M then not M in omega ; then A56: omega c= M by CARD_1:4; then [:omega,omega:] c= [:M,M:] by ZFMISC_1:96; then f in PFuncs ([:M,M:],M) by A54, A56, PARTFUN1:def_3; then X <> {} by A1, A53, A54; then consider Y being set such that A57: Y in X and A58: for Z being set st Z in X & Z <> Y holds not Y c= Z by A3, ORDERS_1:67; consider f being Function such that A59: f = Y and A60: f is one-to-one and A61: dom f = [:(rng f),(rng f):] by A1, A57; set A = rng f; A62: [:(rng f),(rng f):], rng f are_equipotent by A60, A61, WELLORD2:def_4; Y in PFuncs ([:M,M:],M) by A1, A57; then A63: ex f being Function st ( Y = f & dom f c= [:M,M:] & rng f c= M ) by PARTFUN1:def_3; set N = card (rng f); A64: card M = M by CARD_1:def_2; then A65: card (rng f) c= M by A59, A63, CARD_1:11; A66: now__::_thesis:_not_rng_f_is_finite omega \ (rng f) misses rng f by XBOOLE_1:79; then A67: (omega \ (rng f)) /\ (rng f) = {} by XBOOLE_0:def_7; then [:((omega \ (rng f)) /\ (rng f)),((rng f) /\ (omega \ (rng f))):] = {} by ZFMISC_1:90; then A68: [:(omega \ (rng f)),(rng f):] /\ [:(rng f),(omega \ (rng f)):] = {} by ZFMISC_1:100; [:((omega \ (rng f)) /\ (omega \ (rng f))),((omega \ (rng f)) /\ (rng f)):] = {} by A67, ZFMISC_1:90; then [:(omega \ (rng f)),(omega \ (rng f)):] /\ [:(omega \ (rng f)),(rng f):] = {} by ZFMISC_1:100; then A69: [:(omega \ (rng f)),(omega \ (rng f)):] misses [:(omega \ (rng f)),(rng f):] by XBOOLE_0:def_7; [:((rng f) /\ (rng f)),((omega \ (rng f)) /\ (rng f)):] = {} by A67, ZFMISC_1:90; then A70: [:(rng f),(omega \ (rng f)):] /\ [:(rng f),(rng f):] = {} by ZFMISC_1:100; [:((omega \ (rng f)) /\ (rng f)),((rng f) /\ (rng f)):] = {} by A67, ZFMISC_1:90; then A71: ( {} \/ {} = {} & [:(omega \ (rng f)),(rng f):] /\ [:(rng f),(rng f):] = {} ) by ZFMISC_1:100; [:((omega \ (rng f)) /\ (rng f)),((omega \ (rng f)) /\ (rng f)):] = {} by A67, ZFMISC_1:90; then [:(omega \ (rng f)),(omega \ (rng f)):] /\ [:(rng f),(rng f):] = {} by ZFMISC_1:100; then A72: ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) /\ [:(rng f),(rng f):] = {} by A71, XBOOLE_1:23; A73: ( omega c= omega +` (card (rng f)) & omega +` omega = omega ) by CARD_2:75, CARD_2:94; assume A74: rng f is finite ; ::_thesis: contradiction then card (rng f) in omega by CARD_1:47, CARD_3:42; then omega +` (card (rng f)) c= omega +` omega by CARD_2:83; then A75: omega = omega +` (card (rng f)) by A73, XBOOLE_0:def_10; card (rng f) = card (card (rng f)) ; then omega *` (card (rng f)) c= omega by A74, CARD_2:89; then A76: omega +` (omega *` (card (rng f))) = omega by CARD_2:76; card omega = omega by CARD_1:def_2; then A77: omega = card (omega \ (rng f)) by A74, A75, CARD_2:98, CARD_3:42; [:((omega \ (rng f)) /\ (rng f)),((omega \ (rng f)) /\ (omega \ (rng f))):] = {} by A67, ZFMISC_1:90; then [:(omega \ (rng f)),(omega \ (rng f)):] /\ [:(rng f),(omega \ (rng f)):] = {} by ZFMISC_1:100; then ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) /\ [:(rng f),(omega \ (rng f)):] = {} \/ {} by A68, XBOOLE_1:23 .= {} ; then [:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):] misses [:(rng f),(omega \ (rng f)):] by XBOOLE_0:def_7; then card (([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) \/ [:(rng f),(omega \ (rng f)):]) = (card ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):])) +` (card [:(rng f),(omega \ (rng f)):]) by CARD_2:35 .= ((card [:(omega \ (rng f)),(omega \ (rng f)):]) +` (card [:(omega \ (rng f)),(rng f):])) +` (card [:(rng f),(omega \ (rng f)):]) by A69, CARD_2:35 .= ((card [:(omega \ (rng f)),(omega \ (rng f)):]) +` (card [:omega,(card (rng f)):])) +` (card [:(rng f),(omega \ (rng f)):]) by A77, CARD_2:7 .= ((card [:omega,omega:]) +` (card [:omega,(card (rng f)):])) +` (card [:(rng f),(omega \ (rng f)):]) by A77, CARD_2:7 .= (omega +` (card [:omega,(card (rng f)):])) +` (card [:(card (rng f)),omega:]) by A77, Th5, CARD_2:7 .= (omega +` (omega *` (card (rng f)))) +` (card [:(card (rng f)),omega:]) by CARD_2:def_2 .= (omega +` (omega *` (card (rng f)))) +` ((card (rng f)) *` omega) by CARD_2:def_2 ; then ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) \/ [:(rng f),(omega \ (rng f)):],omega \ (rng f) are_equipotent by A77, A76, CARD_1:5; then consider g being Function such that A78: g is one-to-one and A79: dom g = ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) \/ [:(rng f),(omega \ (rng f)):] and A80: rng g = omega \ (rng f) by WELLORD2:def_4; A81: dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def_1; then A82: dom (g +* f) = ([:(omega \ (rng f)),((omega \ (rng f)) \/ (rng f)):] \/ [:(rng f),(omega \ (rng f)):]) \/ [:(rng f),(rng f):] by A61, A79, ZFMISC_1:97 .= [:(omega \ (rng f)),((omega \ (rng f)) \/ (rng f)):] \/ ([:(rng f),(omega \ (rng f)):] \/ [:(rng f),(rng f):]) by XBOOLE_1:4 .= [:(omega \ (rng f)),((omega \ (rng f)) \/ (rng f)):] \/ [:(rng f),((omega \ (rng f)) \/ (rng f)):] by ZFMISC_1:97 .= [:((omega \ (rng f)) \/ (rng f)),((omega \ (rng f)) \/ (rng f)):] by ZFMISC_1:97 .= [:(omega \/ (rng f)),((omega \ (rng f)) \/ (rng f)):] by XBOOLE_1:39 .= [:(omega \/ (rng f)),(omega \/ (rng f)):] by XBOOLE_1:39 ; {} \/ {} = {} ; then (dom g) /\ (dom f) = {} by A61, A79, A72, A70, XBOOLE_1:23; then A83: dom g misses dom f by XBOOLE_0:def_7; then g c= g +* f by FUNCT_4:32; then ( rng f c= rng (g +* f) & rng g c= rng (g +* f) ) by FUNCT_4:18, RELAT_1:11; then ( rng (g +* f) c= (rng g) \/ (rng f) & (rng g) \/ (rng f) c= rng (g +* f) ) by FUNCT_4:17, XBOOLE_1:8; then A84: rng (g +* f) = (rng g) \/ (rng f) by XBOOLE_0:def_10 .= omega \/ (rng f) by A80, XBOOLE_1:39 ; A85: g +* f is one-to-one proof rng f misses rng g by A80, XBOOLE_1:79; then A86: (rng f) /\ (rng g) = {} by XBOOLE_0:def_7; let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom (g +* f) or not b1 in dom (g +* f) or not (g +* f) . x = (g +* f) . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom (g +* f) or not y in dom (g +* f) or not (g +* f) . x = (g +* f) . y or x = y ) assume that A87: x in dom (g +* f) and A88: y in dom (g +* f) ; ::_thesis: ( not (g +* f) . x = (g +* f) . y or x = y ) A89: ( y in dom g or y in dom f ) by A81, A88, XBOOLE_0:def_3; ( x in dom f or x in dom g ) by A81, A87, XBOOLE_0:def_3; then ( ( (g +* f) . x = f . x & (g +* f) . y = f . y & ( f . x = f . y implies x = y ) ) or ( (g +* f) . x = g . x & (g +* f) . y = g . y & ( g . x = g . y implies x = y ) ) or ( (g +* f) . x = f . x & (g +* f) . y = g . y & f . x in rng f & g . y in rng g ) or ( (g +* f) . x = g . x & (g +* f) . y = f . y & g . x in rng g & f . y in rng f ) ) by A60, A78, A83, A89, FUNCT_1:def_3, FUNCT_1:def_4, FUNCT_4:13, FUNCT_4:16; hence ( not (g +* f) . x = (g +* f) . y or x = y ) by A86, XBOOLE_0:def_4; ::_thesis: verum end; set x = the Element of omega \ (rng f); omega \ (rng f) <> {} by A74, A75, CARD_1:68, CARD_3:42; then A90: ( the Element of omega \ (rng f) in omega & not the Element of omega \ (rng f) in rng f ) by XBOOLE_0:def_5; A91: omega \/ (rng f) c= M by A56, A59, A63, XBOOLE_1:8; then [:(omega \/ (rng f)),(omega \/ (rng f)):] c= [:M,M:] by ZFMISC_1:96; then g +* f in PFuncs ([:M,M:],M) by A84, A82, A91, PARTFUN1:def_3; then g +* f in X by A1, A84, A82, A85; then g +* f = f by A58, A59, FUNCT_4:25; hence contradiction by A84, A90, XBOOLE_0:def_3; ::_thesis: verum end; A92: now__::_thesis:_not_card_(rng_f)_<>_M (card (rng f)) *` (card (rng f)) = card [:(card (rng f)),(card (rng f)):] by CARD_2:def_2; then A93: (card (rng f)) *` (card (rng f)) = card [:(rng f),(rng f):] by CARD_2:7; [:(rng f),(rng f):], rng f are_equipotent by A60, A61, WELLORD2:def_4; then A94: (card (rng f)) *` (card (rng f)) = card (rng f) by A93, CARD_1:5; assume card (rng f) <> M ; ::_thesis: contradiction then A95: card (rng f) in M by A65, CARD_1:3; M +` (card (rng f)) = M by A55, A65, CARD_2:76; then card (M \ (rng f)) = M by A64, A95, CARD_2:98; then consider h being Function such that A96: ( h is one-to-one & dom h = rng f ) and A97: rng h c= M \ (rng f) by A65, CARD_1:10; set B = rng h; rng f, rng h are_equipotent by A96, WELLORD2:def_4; then A98: card (rng f) = card (rng h) by CARD_1:5; ( rng f misses M \ (rng f) & (rng f) /\ (rng h) c= (rng f) /\ (M \ (rng f)) ) by A97, XBOOLE_1:26, XBOOLE_1:79; then (rng f) /\ (rng h) c= {} by XBOOLE_0:def_7; then (rng f) /\ (rng h) = {} ; then A99: rng f misses rng h by XBOOLE_0:def_7; ((rng f) \/ (rng h)) \ (rng f) = (rng h) \ (rng f) by XBOOLE_1:40 .= rng h by A99, XBOOLE_1:83 ; then A100: [:(rng h),(rng h):] c= [:(((rng f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] by ZFMISC_1:96; ( [:(((rng f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] c= [:(((rng f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] \/ [:((rng f) \/ (rng h)),(((rng f) \/ (rng h)) \ (rng f)):] & [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] = [:(((rng f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] \/ [:((rng f) \/ (rng h)),(((rng f) \/ (rng h)) \ (rng f)):] ) by XBOOLE_1:7, ZFMISC_1:103; then A101: [:(rng h),(rng h):] c= [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] by A100, XBOOLE_1:1; (card (rng f)) +` (card (rng f)) = card (rng f) by A66, CARD_2:75; then card ((rng f) \/ (rng h)) = card (rng f) by A98, A99, CARD_2:35; then card [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] = card [:(card (rng f)),(card (rng f)):] by CARD_2:7 .= card (rng f) by A94, CARD_2:def_2 ; then A102: card ([:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):]) c= card (rng f) by CARD_1:11; card (rng f) = card [:(card (rng f)),(card (rng f)):] by A94, CARD_2:def_2; then card (rng f) = card [:(rng h),(rng h):] by A98, CARD_2:7; then card (rng f) c= card ([:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):]) by A101, CARD_1:11; then card ([:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):]) = card (rng f) by A102, XBOOLE_0:def_10; then [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):], rng h are_equipotent by A98, CARD_1:5; then consider g being Function such that A103: g is one-to-one and A104: dom g = [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] and A105: rng g = rng h by WELLORD2:def_4; A106: dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def_1; then ( rng f c= (rng f) \/ (rng h) & dom (g +* f) = [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \/ [:(rng f),(rng f):] ) by A61, A104, XBOOLE_1:7, XBOOLE_1:39; then A107: dom (g +* f) = [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] by XBOOLE_1:12, ZFMISC_1:96; A108: [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] misses [:(rng f),(rng f):] by XBOOLE_1:79; A109: g +* f is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom (g +* f) or not b1 in dom (g +* f) or not (g +* f) . x = (g +* f) . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom (g +* f) or not y in dom (g +* f) or not (g +* f) . x = (g +* f) . y or x = y ) assume that A110: x in dom (g +* f) and A111: y in dom (g +* f) ; ::_thesis: ( not (g +* f) . x = (g +* f) . y or x = y ) A112: ( y in dom g or y in dom f ) by A106, A111, XBOOLE_0:def_3; ( x in dom f or x in dom g ) by A106, A110, XBOOLE_0:def_3; then A113: ( ( (g +* f) . x = f . x & (g +* f) . y = f . y & ( f . x = f . y implies x = y ) ) or ( (g +* f) . x = g . x & (g +* f) . y = g . y & ( g . x = g . y implies x = y ) ) or ( (g +* f) . x = f . x & (g +* f) . y = g . y & f . x in rng f & g . y in rng g ) or ( (g +* f) . x = g . x & (g +* f) . y = f . y & g . x in rng g & f . y in rng f ) ) by A60, A61, A103, A104, A108, A112, FUNCT_1:def_3, FUNCT_1:def_4, FUNCT_4:13, FUNCT_4:16; ( rng f misses M \ (rng f) & (rng f) /\ (rng h) c= (rng f) /\ (M \ (rng f)) ) by A97, XBOOLE_1:26, XBOOLE_1:79; then A114: (rng f) /\ (rng g) c= {} by A105, XBOOLE_0:def_7; assume (g +* f) . x = (g +* f) . y ; ::_thesis: x = y hence x = y by A114, A113, XBOOLE_0:def_4; ::_thesis: verum end; set x = the Element of rng h; A115: rng h <> {} by A66, A98; then the Element of rng h in M \ (rng f) by A97, TARSKI:def_3; then A116: not the Element of rng h in rng f by XBOOLE_0:def_5; g c= g +* f by A61, A104, FUNCT_4:32, XBOOLE_1:79; then ( rng f c= rng (g +* f) & rng g c= rng (g +* f) ) by FUNCT_4:18, RELAT_1:11; then A117: (rng g) \/ (rng f) c= rng (g +* f) by XBOOLE_1:8; rng (g +* f) c= (rng g) \/ (rng f) by FUNCT_4:17; then A118: rng (g +* f) = (rng g) \/ (rng f) by A117, XBOOLE_0:def_10; rng h c= M by A97, XBOOLE_1:1; then A119: (rng f) \/ (rng h) c= M by A59, A63, XBOOLE_1:8; then [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] c= [:M,M:] by ZFMISC_1:96; then g +* f in PFuncs ([:M,M:],M) by A105, A118, A107, A119, PARTFUN1:def_3; then A120: g +* f in X by A1, A105, A118, A107, A109; the Element of rng h in rng (g +* f) by A105, A118, A115, XBOOLE_0:def_3; hence contradiction by A58, A59, A120, A116, FUNCT_4:25; ::_thesis: verum end; then M *` M = card [:(card (rng f)),(card (rng f)):] by CARD_2:def_2 .= card [:(rng f),(rng f):] by CARD_2:7 ; hence M *` M = M by A92, A62, CARD_1:5; ::_thesis: verum end; theorem Th16: :: CARD_4:16 for M, N being Cardinal st not M is finite & 0 in N & ( N c= M or N in M ) holds ( M *` N = M & N *` M = M ) proof let M, N be Cardinal; ::_thesis: ( not M is finite & 0 in N & ( N c= M or N in M ) implies ( M *` N = M & N *` M = M ) ) A1: 1 *` M = M by CARD_2:21; assume not M is finite ; ::_thesis: ( not 0 in N or ( not N c= M & not N in M ) or ( M *` N = M & N *` M = M ) ) then A2: M *` M = M by Th15; assume 0 in N ; ::_thesis: ( ( not N c= M & not N in M ) or ( M *` N = M & N *` M = M ) ) then 1 c= N by CARD_2:68; then A3: 1 *` M c= N *` M by CARD_2:90; assume ( N c= M or N in M ) ; ::_thesis: ( M *` N = M & N *` M = M ) then N *` M c= M *` M by CARD_2:90; hence ( M *` N = M & N *` M = M ) by A2, A3, A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th17: :: CARD_4:17 for M, N being Cardinal st not M is finite & ( N c= M or N in M ) holds ( M *` N c= M & N *` M c= M ) proof let M, N be Cardinal; ::_thesis: ( not M is finite & ( N c= M or N in M ) implies ( M *` N c= M & N *` M c= M ) ) assume ( not M is finite & ( N c= M or N in M ) ) ; ::_thesis: ( M *` N c= M & N *` M c= M ) then ( M *` N = M or not 0 in N ) by Th16; then ( M *` N c= M or ( N = 0 & M *` 0 = 0 & 0 c= M ) ) by CARD_2:20, ORDINAL3:8, XBOOLE_1:2; hence ( M *` N c= M & N *` M c= M ) ; ::_thesis: verum end; theorem :: CARD_4:18 for X being set st not X is finite holds ( [:X,X:],X are_equipotent & card [:X,X:] = card X ) proof let X be set ; ::_thesis: ( not X is finite implies ( [:X,X:],X are_equipotent & card [:X,X:] = card X ) ) assume not X is finite ; ::_thesis: ( [:X,X:],X are_equipotent & card [:X,X:] = card X ) then (card X) *` (card X) = card X by Th15; then card [:(card X),(card X):] = card X by CARD_2:def_2; then card [:X,X:] = card X by CARD_2:7; hence ( [:X,X:],X are_equipotent & card [:X,X:] = card X ) by CARD_1:5; ::_thesis: verum end; theorem :: CARD_4:19 for X, Y being set st not X is finite & Y is finite & Y <> {} holds ( [:X,Y:],X are_equipotent & card [:X,Y:] = card X ) proof let X, Y be set ; ::_thesis: ( not X is finite & Y is finite & Y <> {} implies ( [:X,Y:],X are_equipotent & card [:X,Y:] = card X ) ) assume that A1: not X is finite and A2: ( Y is finite & Y <> {} ) ; ::_thesis: ( [:X,Y:],X are_equipotent & card [:X,Y:] = card X ) ( card Y c= card X & 0 in card Y ) by A1, A2, ORDINAL3:8; then (card X) *` (card Y) = card X by A1, Th16; then card [:(card X),(card Y):] = card X by CARD_2:def_2; then card [:X,Y:] = card X by CARD_2:7; hence ( [:X,Y:],X are_equipotent & card [:X,Y:] = card X ) by CARD_1:5; ::_thesis: verum end; theorem :: CARD_4:20 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 ) proof let K, L, M, N be Cardinal; ::_thesis: ( K in L & M in N implies ( K *` M in L *` N & M *` K in L *` N ) ) A1: for K, L, M, N being Cardinal st K in L & M in N & L c= N holds K *` M in L *` N proof let K, L, M, N be Cardinal; ::_thesis: ( K in L & M in N & L c= N implies K *` M in L *` N ) assume that A2: K in L and A3: M in N and A4: L c= N ; ::_thesis: K *` M in L *` N A5: now__::_thesis:_(_N_is_finite_implies_K_*`_M_in_L_*`_N_) assume A6: N is finite ; ::_thesis: K *` M in L *` N then reconsider N = N as finite Cardinal ; reconsider L = L, M = M, K = K as finite Cardinal by A2, A3, A4, A6, CARD_3:92; A7: card N = N by CARD_1:def_2; A8: card M = M by CARD_1:def_2; then card M < card N by A3, A7, NAT_1:41; then A9: (card K) * (card M) <= (card K) * (card N) by XREAL_1:64; A10: card L = L by CARD_1:def_2; then A11: L *` N = card ((card L) * (card N)) by A7, CARD_2:39; A12: card K = K by CARD_1:def_2; then card K < card L by A2, A10, NAT_1:41; then (card K) * (card N) < (card L) * (card N) by A3, XREAL_1:68; then A13: (card K) * (card M) < (card L) * (card N) by A9, XXREAL_0:2; K *` M = card ((card K) * (card M)) by A12, A8, CARD_2:39; hence K *` M in L *` N by A11, A13, NAT_1:41; ::_thesis: verum end; A14: 0 in L by A2, ORDINAL3:8; now__::_thesis:_(_not_N_is_finite_implies_K_*`_M_in_L_*`_N_) assume A15: not N is finite ; ::_thesis: K *` M in L *` N then A16: L *` N = N by A4, A14, Th16; A17: omega c= N by A15, CARD_3:85; A18: now__::_thesis:_(_K_is_finite_&_M_is_finite_implies_K_*`_M_in_L_*`_N_) assume ( K is finite & M is finite ) ; ::_thesis: K *` M in L *` N then reconsider K = K, M = M as finite Cardinal ; ( card K = K & card M = M ) by CARD_1:def_2; then K *` M = card ((card K) * (card M)) by CARD_2:39 .= (card K) * (card M) by CARD_1:def_2 ; hence K *` M in L *` N by A16, A17, TARSKI:def_3; ::_thesis: verum end; ( ( K c= M & ( M is finite or not M is finite ) ) or ( M c= K & ( K is finite or not K is finite ) ) ) ; then ( ( K is finite & M is finite ) or K *` M c= M or ( K *` M c= K & K in N ) ) by A2, A4, Th17; hence K *` M in L *` N by A3, A16, A18, ORDINAL1:12; ::_thesis: verum end; hence K *` M in L *` N by A5; ::_thesis: verum end; ( L c= N or N c= L ) ; hence ( K in L & M in N implies ( K *` M in L *` N & M *` K in L *` N ) ) by A1; ::_thesis: verum end; theorem Th21: :: CARD_4:21 for X being set st not X is finite holds card X = omega *` (card X) proof let X be set ; ::_thesis: ( not X is finite implies card X = omega *` (card X) ) assume A1: not X is finite ; ::_thesis: card X = omega *` (card X) then omega c= card X by CARD_3:85; hence card X = omega *` (card X) by A1, Th16; ::_thesis: verum end; theorem :: CARD_4:22 for X, Y being set st X <> {} & X is finite & not Y is finite holds (card Y) *` (card X) = card Y proof let X, Y be set ; ::_thesis: ( X <> {} & X is finite & not Y is finite implies (card Y) *` (card X) = card Y ) assume that A1: ( X <> {} & X is finite ) and A2: not Y is finite ; ::_thesis: (card Y) *` (card X) = card Y ( card X in card Y & 0 in card X ) by A1, A2, CARD_3:86, ORDINAL3:8; hence (card Y) *` (card X) = card Y by A2, Th16; ::_thesis: verum end; theorem Th23: :: CARD_4:23 for D being non empty set for n being Element of NAT st not D is finite & n <> 0 holds ( n -tuples_on D,D are_equipotent & card (n -tuples_on D) = card D ) proof let D be non empty set ; ::_thesis: for n being Element of NAT st not D is finite & n <> 0 holds ( n -tuples_on D,D are_equipotent & card (n -tuples_on D) = card D ) let n be Element of NAT ; ::_thesis: ( not D is finite & n <> 0 implies ( n -tuples_on D,D are_equipotent & card (n -tuples_on D) = card D ) ) assume that A1: not D is finite and A2: n <> 0 ; ::_thesis: ( n -tuples_on D,D are_equipotent & card (n -tuples_on D) = card D ) defpred S1[ Nat] means ( \$1 <> 0 implies card (\$1 -tuples_on D) = card D ); A3: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) 0 -tuples_on D = {(<*> D)} by FINSEQ_2:94; then A4: ( 0 in card (0 -tuples_on D) & card (0 -tuples_on D) c= card D ) by A1, ORDINAL3:8; k in NAT by ORDINAL1:def_12; then A5: card ((k + 1) -tuples_on D) = card [:(k -tuples_on D),(1 -tuples_on D):] by Th9 .= card [:(card (k -tuples_on D)),(card (1 -tuples_on D)):] by CARD_2:7 .= card [:(card (k -tuples_on D)),(card D):] by Th8 .= (card (k -tuples_on D)) *` (card D) by CARD_2:def_2 ; assume S1[k] ; ::_thesis: S1[k + 1] hence S1[k + 1] by A1, A5, A4, Th16; ::_thesis: verum end; A6: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A6, A3); then card (n -tuples_on D) = card D by A2; hence ( n -tuples_on D,D are_equipotent & card (n -tuples_on D) = card D ) by CARD_1:5; ::_thesis: verum end; theorem :: CARD_4:24 for D being non empty set st not D is finite holds card D = card (D *) proof let D be non empty set ; ::_thesis: ( not D is finite implies card D = card (D *) ) defpred S1[ set ] means verum; deffunc H1( Element of NAT ) -> FinSequenceSet of D = \$1 -tuples_on D; A1: D * = union { (k -tuples_on D) where k is Element of NAT : verum } by FINSEQ_2:108; assume A2: not D is finite ; ::_thesis: card D = card (D *) A3: for X being set st X in { (k -tuples_on D) where k is Element of NAT : verum } holds card X c= card D proof let X be set ; ::_thesis: ( X in { (k -tuples_on D) where k is Element of NAT : verum } implies card X c= card D ) assume X in { (k -tuples_on D) where k is Element of NAT : verum } ; ::_thesis: card X c= card D then consider k being Element of NAT such that A4: X = k -tuples_on D ; 0 -tuples_on D = {(<*> D)} by FINSEQ_2:94; then ( ( card (0 -tuples_on D) c= card D & k = 0 ) or k <> 0 ) by A2; hence card X c= card D by A2, A4, Th23; ::_thesis: verum end; 1 -tuples_on D in { (k -tuples_on D) where k is Element of NAT : verum } ; then card (1 -tuples_on D) c= card (D *) by A1, CARD_1:11, ZFMISC_1:74; then A5: card D c= card (D *) by Th8; { H1(k) where k is Element of NAT : S1[k] } is countable from CARD_4:sch_1(); then card { (k -tuples_on D) where k is Element of NAT : verum } c= omega by CARD_3:def_14; then card (union { (k -tuples_on D) where k is Element of NAT : verum } ) c= omega *` (card D) by A3, CARD_2:87; then card (D *) c= card D by A2, A1, Th21; hence card D = card (D *) by A5, XBOOLE_0:def_10; ::_thesis: verum end;