card_4.miz



    begin

    reserve X,Y,Z,x,y,y1,y2 for set,

D for non empty set,

k,n,n1,n2,m2,m1 for Nat,

L,K,M,N for Cardinal,

f,g for Function;

    theorem :: CARD_4:1

    X is finite implies X is countable;

    theorem :: CARD_4:2

     omega is countable;

    reserve r for Real;

    theorem :: CARD_4:3

    

     Th3: r <> 0 or n = 0 iff (r |^ n) <> 0

    proof

      defpred P[ Nat] means r <> 0 or $1 = 0 iff (r |^ $1) <> 0 ;

      

       A1: P[k] implies P[(k + 1)]

      proof

        

         A2: (r |^ (k + 1)) = ((r |^ k) * r) by NEWTON: 6;

        assume P[k];

        hence thesis by A2;

      end;

      

       A3: P[ 0 ] by NEWTON: 4;

       P[k] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    

     Lm1: ((2 |^ n1) * ((2 * m1) + 1)) = ((2 |^ n2) * ((2 * m2) + 1)) implies n1 <= n2

    proof

      assume

       A1: ((2 |^ n1) * ((2 * m1) + 1)) = ((2 |^ n2) * ((2 * m2) + 1));

      assume

       A2: n1 > n2;

      then

      consider n be Nat such that

       A3: n1 = (n2 + n) by NAT_1: 10;

      n <> 0 by A2, A3;

      then

      consider k be Nat such that

       A4: n = (k + 1) by NAT_1: 6;

      

       A5: (2 |^ n2) <> 0 by Th3;

      reconsider 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))

      .= (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;

    end;

    theorem :: CARD_4:4

    

     Th4: ((2 |^ n1) * ((2 * m1) + 1)) = ((2 |^ n2) * ((2 * m2) + 1)) implies n1 = n2 & m1 = m2

    proof

      

       A1: (2 |^ n1) <> 0 by Th3;

      assume

       A2: ((2 |^ n1) * ((2 * m1) + 1)) = ((2 |^ n2) * ((2 * m2) + 1));

      then n1 <= n2 & n2 <= n1 by Lm1;

      hence n1 = n2 by XXREAL_0: 1;

      then ((2 * m1) + 1) = ((2 * m2) + 1) by A2, A1, XCMPLX_1: 5;

      hence thesis;

    end;

    

     Lm2: x in [: NAT , NAT :] implies ex n1,n2 be Element of NAT st x = [n1, n2]

    proof

      assume

       A1: x in [: NAT , NAT :];

      then

      reconsider n1 = (x `1 ), n2 = (x `2 ) as Element of NAT by MCART_1: 10;

      take n1, n2;

      thus thesis by A1, MCART_1: 21;

    end;

    theorem :: CARD_4:5

    

     Th5: ( [: 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 f( Element of NAT , Element of NAT ) = ((2 |^ $1) * ((2 * $2) + 1));

      consider f be Function of [: NAT , NAT :], NAT such that

       A2: for n,m be Element of NAT holds (f . (n,m)) = f(n,m) from BINOP_1:sch 4;

      

       A3: f is one-to-one

      proof

        let x,y be object;

        assume x in ( dom f);

        then

        consider n1,m1 be Element of NAT such that

         A4: x = [n1, m1] by Lm2;

        assume y in ( dom f);

        then

        consider n2,m2 be Element of NAT such that

         A5: y = [n2, m2] by Lm2;

        assume

         A6: (f . x) = (f . 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 thesis by A4, A5, A7, Th4;

      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;

      hence thesis by CARD_1: 5;

    end;

    theorem :: CARD_4:6

    

     Th6: ( omega *` omega ) = omega by Th5, CARD_2:def 2;

    theorem :: CARD_4:7

    

     Th7: X is countable & Y is countable implies [:X, Y:] is countable

    proof

      assume ( card X) c= omega & ( card Y) c= omega ;

      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;

    end;

    theorem :: CARD_4:8

    

     Th8: ((1 -tuples_on D),D) are_equipotent & ( card (1 -tuples_on D)) = ( card D)

    proof

      deffunc f( object) = <*$1*>;

      consider f such that

       A1: ( dom f) = D & for x be object st x in D holds (f . x) = f(x) from FUNCT_1:sch 3;

      (D,(1 -tuples_on D)) are_equipotent

      proof

        take f;

        thus f is one-to-one

        proof

          let x,y be object;

          assume x in ( dom f) & y in ( dom f);

          then

           A2: (f . x) = <*x*> & (f . y) = <*y*> by A1;

          ( <*x*> . 1) = x by FINSEQ_1:def 8;

          hence thesis by A2, FINSEQ_1:def 8;

        end;

        thus ( dom f) = D by A1;

        thus ( rng f) c= (1 -tuples_on D)

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A3: y in ( dom f) and

           A4: x = (f . y) by FUNCT_1:def 3;

          reconsider y as Element of D by A1, A3;

          x = <*y*> by A1, A4;

          then x in the set of all <*d*> where d be Element of D;

          hence thesis by FINSEQ_2: 96;

        end;

        let x be object;

        assume x in (1 -tuples_on D);

        then

        reconsider y = x as Element of (1 -tuples_on D);

        consider z be Element of D such that

         A5: y = <*z*> by FINSEQ_2: 97;

        x = (f . z) by A1, A5;

        hence thesis by A1, FUNCT_1:def 3;

      end;

      hence thesis by CARD_1: 5;

    end;

    reserve p,q for FinSequence,

k,m,n,n1,n2,n3 for Nat;

    theorem :: CARD_4:9

    

     Th9: ( [:(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

      defpred P[ object, object] means ex p be Element of (n -tuples_on D), q be 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 be object st x in A holds ex y be object st P[x, y]

      proof

        let x be object;

        assume

         A2: x in A;

        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;

        x = [(x `1 ), (x `2 )] by A2, MCART_1: 21;

        hence thesis;

      end;

      consider f such that

       A3: ( dom f) = A & for x be object st x in A holds P[x, (f . x)] from CLASSES1:sch 1( A1);

      thus ( [:(n -tuples_on D), (m -tuples_on D):],((n + m) -tuples_on D)) are_equipotent

      proof

        take f;

        thus f is one-to-one

        proof

          let x,y be object;

          assume x in ( dom f);

          then

          consider p1 be Element of (n -tuples_on D), q1 be 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);

          then

          consider p2 be Element of (n -tuples_on D), q2 be 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);

          

           A9: ( len p1) = n & ( len p2) = n by CARD_1:def 7;

          then

          consider p such that

           A10: (p1 ^ p) = p2 by A5, A7, A8, FINSEQ_1: 47;

          consider q 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 thesis by A4, A5, A6, A7, A8, FINSEQ_1: 33;

        end;

        thus ( dom f) = A by A3;

        thus ( rng f) c= B

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A12: y in ( dom f) & x = (f . y) by FUNCT_1:def 3;

          ex p be Element of (n -tuples_on D), q be 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 thesis;

        end;

        let x be object;

        assume x in B;

        then

        reconsider x as Element of B;

        consider p be Element of (n -tuples_on D), q be Element of (m -tuples_on D) such that

         A13: x = (p ^ q) by FINSEQ_2: 106;

        consider p1 be Element of (n -tuples_on D), q1 be 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 thesis by A3, A13, A15, FUNCT_1:def 3;

      end;

      hence thesis by CARD_1: 5;

    end;

    theorem :: CARD_4:10

    

     Th10: D is countable implies (n -tuples_on D) is countable

    proof

      defpred P[ Nat] means ($1 -tuples_on D) is countable;

      assume ( card D) c= omega ;

      then ( card (1 -tuples_on D)) c= omega by Th8;

      then

       A1: (1 -tuples_on D) is countable;

      

       A2: for k be Nat holds P[k] implies P[(k + 1)]

      proof

        let k be Nat;

        assume P[k];

        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 ;

        ( card [:(k -tuples_on D), (1 -tuples_on D):]) = ( card ((k + 1) -tuples_on D)) by Th9;

        hence thesis by A3, CARD_3:def 14;

      end;

       {( <*> D)} is countable;

      then

       A4: P[ 0 ] by FINSEQ_2: 94;

      for k be Nat holds P[k] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: CARD_4:11

    

     Th11: for f st ( dom f) is countable & for x st x in ( dom f) holds (f . x) is countable holds ( Union f) is countable

    proof

      let f such that

       A1: ( card ( dom f)) c= omega and

       A2: for x st x in ( dom f) holds (f . x) is countable;

      for x be object st x in ( dom f) holds ( card (f . x)) c= omega by A2, CARD_3:def 14;

      hence ( card ( Union f)) c= omega by A1, Th6, CARD_2: 86;

    end;

    theorem :: CARD_4:12

    (X is countable & for Y st Y in X holds Y is countable) implies ( union X) is countable

    proof

      assume that

       A1: ( card X) c= omega and

       A2: for Y st Y in X holds Y is countable;

      for Y st Y in X holds ( card Y) c= omega by A2, CARD_3:def 14;

      hence ( card ( union X)) c= omega by A1, Th6, CARD_2: 87;

    end;

    theorem :: CARD_4:13

    D is countable implies (D * ) is countable

    proof

      defpred P[ object, object] means ex n st $1 = n & $2 = (n -tuples_on D);

      

       A1: for x be object st x in NAT holds ex y be object st P[x, y]

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider n = x as Element of NAT ;

        reconsider y = (n -tuples_on D) as set;

        take y, n;

        thus thesis;

      end;

      consider f such that

       A2: ( dom f) = NAT & for x be object st x in NAT holds P[x, (f . x)] from CLASSES1:sch 1( A1);

      

       A3: (D * ) = ( union the set of all (k -tuples_on D)) by FINSEQ_2: 108;

      

       A4: ( Union f) = (D * )

      proof

        thus ( Union f) c= (D * )

        proof

          let x be object;

          assume x in ( Union f);

          then

          consider X such that

           A5: x in X and

           A6: X in ( rng f) by TARSKI:def 4;

          consider y be object such that

           A7: y in ( dom f) and

           A8: X = (f . y) by A6, FUNCT_1:def 3;

          reconsider y as Element of NAT by A2, A7;

          ex n st y = n & X = (n -tuples_on D) by A2, A8;

          then X in the set of all (k -tuples_on D);

          hence thesis by A3, A5, TARSKI:def 4;

        end;

        let x be object;

        assume x in (D * );

        then

        consider X such that

         A9: x in X & X in the set of all (k -tuples_on D) by A3, TARSKI:def 4;

        consider n such that

         A10: X = (n -tuples_on D) by A9;

        

         A11: n in NAT by ORDINAL1:def 12;

        then ex k st n = k & (f . n) = (k -tuples_on D) by A2;

        then X in ( rng f) by A2, A10, FUNCT_1:def 3, A11;

        hence thesis by A9, TARSKI:def 4;

      end;

      assume

       A12: D is countable;

      now

        let x;

        assume x in ( dom f);

        then ex n st x = n & (f . x) = (n -tuples_on D) by A2;

        hence (f . x) is countable by A12, Th10;

      end;

      hence thesis by A2, A4, Th11;

    end;

    theorem :: CARD_4:14

     omega c= ( card (D * ))

    proof

      defpred P[ object, object] means ex p st $1 = p & $2 = ( len p);

      

       A1: {} in (D * ) & ( len {} ) = 0 by FINSEQ_1: 49;

      

       A2: for x be object st x in (D * ) holds ex y be object st P[x, y]

      proof

        let x be object;

        assume x in (D * );

        then

        reconsider p = x as Element of (D * );

        reconsider p as FinSequence;

        reconsider y = ( len p) as set;

        take y, p;

        thus thesis;

      end;

      consider f such that

       A3: ( dom f) = (D * ) & for x be object st x in (D * ) holds P[x, (f . x)] from CLASSES1:sch 1( A2);

      defpred P[ Nat] means $1 in (f .: (D * ));

      

       A4: for n be Nat holds P[n] implies P[(n + 1)]

      proof

        set y = the Element of D;

        let n be Nat;

        assume n in (f .: (D * ));

        then

        consider x be object such that

         A5: x in ( dom f) and

         A6: x in (D * ) and

         A7: n = (f . x) by FUNCT_1:def 6;

        consider p such that

         A8: x = p and

         A9: n = ( len p) by A3, A5, A7;

        reconsider p as FinSequence of D by A6, A8, FINSEQ_1:def 11;

        

         A10: ( len (p ^ <*y*>)) = (n + ( len <*y*>)) by A9, FINSEQ_1: 22

        .= (n + 1) by FINSEQ_1: 40;

        

         A11: (p ^ <*y*>) in (D * ) by FINSEQ_1:def 11;

        then ex q be FinSequence st (p ^ <*y*>) = q & (f . (p ^ <*y*>)) = ( len q) by A3;

        hence thesis by A3, A11, A10, FUNCT_1:def 6;

      end;

      ex p st {} = p & (f . {} ) = ( len p) by A3, FINSEQ_1: 49;

      then

       A12: P[ 0 ] by A3, A1, FUNCT_1:def 6;

      

       A13: for n be Nat holds P[n] from NAT_1:sch 2( A12, A4);

       NAT c= (f .: (D * )) by A13;

      hence thesis by CARD_1: 47, CARD_1: 66;

    end;

    scheme :: CARD_4:sch1

    FraenCoun1 { f( object) -> set , P[ set] } :

{ f(n) : P[n] } is countable;

      consider f such that

       A1: ( dom f) = NAT & for x be object st x in NAT holds (f . x) = f(x) from FUNCT_1:sch 3;

      { f(n) : P[n] } c= ( rng f)

      proof

        let x be object;

        assume x in { f(n) : P[n] };

        then

        consider n such that

         A2: x = f(n) and P[n];

        

         A3: n in NAT by ORDINAL1:def 12;

        then (f . n) = x by A1, A2;

        hence thesis by A1, FUNCT_1:def 3, A3;

      end;

      hence thesis by A1, CARD_3: 93;

    end;

    scheme :: CARD_4:sch2

    FraenCoun2 { f( object, object) -> set , P[ set, set] } :

{ f(n1,n2) : P[n1, n2] } is countable;

      consider N be 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 g( object) = f(`1,`2);

      consider f such that

       A3: ( dom f) = NAT & for x be object st x in NAT holds (f . x) = g(x) from FUNCT_1:sch 3;

      { f(n1,n2) : P[n1, n2] } c= ( rng f)

      proof

        let x be object;

        assume x in { f(n1,n2) : P[n1, n2] };

        then

        consider n1, n2 such that

         A4: x = f(n1,n2) and P[n1, n2];

        n1 in NAT & n2 in NAT by ORDINAL1:def 12;

        then [n1, n2] in [: NAT , NAT :] by ZFMISC_1: 87;

        then

        consider y be object 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 thesis by A1, A3, A5, FUNCT_1:def 3;

      end;

      hence thesis by A3, CARD_3: 93;

    end;

    scheme :: CARD_4:sch3

    FraenCoun3 { f( object, object, object) -> set , P[ set, set, set] } :

{ f(n1,n2,n3) : P[n1, n2, n3] } is countable;

      ( [: 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 be Function such that N is one-to-one and

       A2: ( dom N) = NAT and

       A3: ( rng N) = [: NAT , NAT , NAT :] by A1;

      deffunc g( object) = f(`1,`2,`2);

      consider f such that

       A4: ( dom f) = NAT & for x be object st x in NAT holds (f . x) = g(x) from FUNCT_1:sch 3;

      { f(n1,n2,n3) : P[n1, n2, n3] } c= ( rng f)

      proof

        let x be object;

        assume x in { f(n1,n2,n3) : P[n1, n2, n3] };

        then

        consider n1, n2, n3 such that

         A5: x = f(n1,n2,n3) and P[n1, n2, n3];

        reconsider n1, n2, n3 as Element of NAT by ORDINAL1:def 12;

        

         A6: ( [n1, n2, n3] `3_3 ) = n3 & ( [n1, n2, n3] `1_3 ) = (( [n1, n2, n3] `1 ) `1 );

        consider y be object such that

         A7: y in ( dom N) and

         A8: [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, A7, A8, A6;

        hence thesis by A2, A4, A7, FUNCT_1:def 3;

      end;

      hence thesis by A4, CARD_3: 93;

    end;

    reserve f,f1,f2 for Function,

X1,X2 for set;

    ::$Notion-Name

    theorem :: CARD_4:15

    

     Th15: not M is finite implies (M *` M) = M

    proof

      defpred P[ object] means ex f st f = $1 & f is one-to-one & ( dom f) = [:( rng f), ( rng f):];

      consider X such that

       A1: for x be object holds x in X iff x in ( PFuncs ( [:M, M:],M)) & P[x] from XBOOLE_0:sch 1;

      

       A2: x in X implies x is Function

      proof

        assume x in X;

        then ex f st f = x & f is one-to-one & ( dom f) = [:( rng f), ( rng f):] by A1;

        hence thesis;

      end;

      

       A3: for Z st Z <> {} & Z c= X & Z is c=-linear holds ( union Z) in X

      proof

        let Z;

        assume that Z <> {} and

         A4: Z c= X and

         A5: Z is c=-linear;

        ( union Z) is Relation-like Function-like

        proof

          set F = ( union Z);

          thus for x be object st x in F holds ex y1,y2 be object st [y1, y2] = x

          proof

            let x be object;

            assume x in F;

            then

            consider Y 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 be object st x in f holds ex y1,y2 be object st [y1, y2] = x by RELAT_1:def 1;

            hence thesis by A6;

          end;

          let x,y1,y2 be object;

          assume [x, y1] in F;

          then

          consider X1 such that

           A8: [x, y1] in X1 and

           A9: X1 in Z by TARSKI:def 4;

          assume [x, y2] in F;

          then

          consider X2 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;

          then [x, y2] in X1 & (for x,y1,y2 be object st [x, y1] in f1 & [x, y2] in f1 holds y1 = y2) or [x, y1] in X2 & for x,y1,y2 be object st [x, y1] in f2 & [x, y2] in f2 holds y1 = y2 by A8, A10, FUNCT_1:def 1;

          hence thesis by A8, A10;

        end;

        then

        reconsider f = ( union Z) as Function;

        

         A12: f is one-to-one

        proof

          let x1,x2 be object;

          assume that

           A13: x1 in ( dom f) and

           A14: x2 in ( dom f);

           [x1, (f . x1)] in f by A13, FUNCT_1: 1;

          then

          consider X1 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 such that

           A17: [x2, (f . x2)] in X2 and

           A18: X2 in Z by TARSKI:def 4;

          consider f2 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 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;

          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 thesis by A22, A20;

        end;

        

         A23: ( dom f) = [:( rng f), ( rng f):]

        proof

          thus ( dom f) c= [:( rng f), ( rng f):]

          proof

            let x be object;

            assume x in ( dom f);

            then [x, (f . x)] in f by FUNCT_1:def 2;

            then

            consider Y such that

             A24: [x, (f . x)] in Y and

             A25: Y in Z by TARSKI:def 4;

            consider g be 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 thesis by A28;

          end;

          let x1,x2 be object;

          assume

           A29: [x1, x2] in [:( rng f), ( rng f):];

          ( [x1, x2] `1 ) in ( rng f) by A29, MCART_1: 10;

          then

          consider y1 be object such that

           A30: 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 be object such that

           A31: y2 in ( dom f) & ( [x1, x2] `2 ) = (f . y2) by FUNCT_1:def 3;

           [y2, ( [x1, x2] `2 )] in f by A31, FUNCT_1: 1;

          then

          consider X2 such that

           A32: [y2, ( [x1, x2] `2 )] in X2 and

           A33: X2 in Z by TARSKI:def 4;

          consider f2 such that

           A34: f2 = X2 and f2 is one-to-one and

           A35: ( dom f2) = [:( rng f2), ( rng f2):] by A1, A4, A33;

          f2 c= f by A33, A34, ZFMISC_1: 74;

          then

           A36: ( dom f2) c= ( dom f) by RELAT_1: 11;

           [y1, ( [x1, x2] `1 )] in f by A30, FUNCT_1: 1;

          then

          consider X1 such that

           A37: [y1, ( [x1, x2] `1 )] in X1 and

           A38: X1 in Z by TARSKI:def 4;

          consider f1 such that

           A39: f1 = X1 and f1 is one-to-one and

           A40: ( dom f1) = [:( rng f1), ( rng f1):] by A1, A4, A38;

          (X1,X2) are_c=-comparable by A5, A38, A33, ORDINAL1:def 8;

          then X1 c= X2 or X2 c= X1;

          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 A37, A32, A39, A34, 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

           A41: [x1, x2] in ( dom f1) or [x1, x2] in ( dom f2) by A40, A35, ZFMISC_1: 87;

          f1 c= f by A38, A39, ZFMISC_1: 74;

          then ( dom f1) c= ( dom f) by RELAT_1: 11;

          hence thesis by A41, A36;

        end;

        

         A42: ( rng f) c= M

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A43: x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

           [x, y] in ( union Z) by A43, FUNCT_1:def 2;

          then

          consider Y such that

           A44: [x, y] in Y and

           A45: Y in Z by TARSKI:def 4;

          Y in ( PFuncs ( [:M, M:],M)) by A1, A4, A45;

          then

          consider g be Function such that

           A46: Y = g and ( dom g) c= [:M, M:] and

           A47: ( rng g) c= M by PARTFUN1:def 3;

          x in ( dom g) & (g . x) = y by A44, A46, FUNCT_1: 1;

          then y in ( rng g) by FUNCT_1:def 3;

          hence thesis by A47;

        end;

        ( dom f) c= [:M, M:]

        proof

          let x be object;

          assume x in ( dom f);

          then [x, (f . x)] in ( union Z) by FUNCT_1:def 2;

          then

          consider Y such that

           A48: [x, (f . x)] in Y and

           A49: Y in Z by TARSKI:def 4;

          Y in ( PFuncs ( [:M, M:],M)) by A1, A4, A49;

          then

          consider g be Function such that

           A50: Y = g and

           A51: ( dom g) c= [:M, M:] and ( rng g) c= M by PARTFUN1:def 3;

          x in ( dom g) by A48, A50, FUNCT_1: 1;

          hence thesis by A51;

        end;

        then f in ( PFuncs ( [:M, M:],M)) by A42, PARTFUN1:def 3;

        hence thesis by A1, A12, A23;

      end;

      consider f such that

       A52: f is one-to-one and

       A53: ( dom f) = [: omega , omega :] & ( rng f) = omega by Th5;

      assume

       A54: not M is finite;

      then not M in omega ;

      then

       A55: 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 A53, A55, PARTFUN1:def 3;

      then X <> {} by A1, A52, A53;

      then

      consider Y such that

       A56: Y in X and

       A57: for Z st Z in X & Z <> Y holds not Y c= Z by A3, ORDERS_1: 67;

      consider f such that

       A58: f = Y and

       A59: f is one-to-one and

       A60: ( dom f) = [:( rng f), ( rng f):] by A1, A56;

      set A = ( rng f);

      

       A61: ( [:A, A:],A) are_equipotent by A59, A60;

      Y in ( PFuncs ( [:M, M:],M)) by A1, A56;

      then

       A62: ex f st Y = f & ( dom f) c= [:M, M:] & ( rng f) c= M by PARTFUN1:def 3;

      set N = ( card A);

      

       A63: ( card M) = M;

      then

       A64: N c= M by A58, A62, CARD_1: 11;

       A65:

      now

        ( omega \ A) misses A by XBOOLE_1: 79;

        then

         A66: (( omega \ A) /\ A) = {} ;

        then [:(( omega \ A) /\ A), (A /\ ( omega \ A)):] = {} by ZFMISC_1: 90;

        then

         A67: ( [:( omega \ A), A:] /\ [:A, ( omega \ A):]) = {} by ZFMISC_1: 100;

         [:(( omega \ A) /\ ( omega \ A)), (( omega \ A) /\ A):] = {} by A66, ZFMISC_1: 90;

        then ( [:( omega \ A), ( omega \ A):] /\ [:( omega \ A), A:]) = {} by ZFMISC_1: 100;

        then

         A68: [:( omega \ A), ( omega \ A):] misses [:( omega \ A), A:];

         [:(A /\ A), (( omega \ A) /\ A):] = {} by A66, ZFMISC_1: 90;

        then

         A69: ( [:A, ( omega \ A):] /\ [:A, A:]) = {} by ZFMISC_1: 100;

         [:(( omega \ A) /\ A), (A /\ A):] = {} by A66, ZFMISC_1: 90;

        then

         A70: ( {} \/ {} ) = {} & ( [:( omega \ A), A:] /\ [:A, A:]) = {} by ZFMISC_1: 100;

         [:(( omega \ A) /\ A), (( omega \ A) /\ A):] = {} by A66, ZFMISC_1: 90;

        then ( [:( omega \ A), ( omega \ A):] /\ [:A, A:]) = {} by ZFMISC_1: 100;

        then

         A71: (( [:( omega \ A), ( omega \ A):] \/ [:( omega \ A), A:]) /\ [:A, A:]) = {} by A70, XBOOLE_1: 23;

        

         A72: omega c= ( omega +` N) & ( omega +` omega ) = omega by CARD_2: 75, CARD_2: 94;

        assume

         A73: A is finite;

        then N in omega by CARD_3: 42;

        then ( omega +` N) c= ( omega +` omega ) by CARD_2: 83;

        then

         A74: omega = ( omega +` N) by A72;

        N = ( card ( card A));

        then ( omega *` N) c= omega by A73, CARD_2: 89;

        then

         A75: ( omega +` ( omega *` N)) = omega by CARD_2: 76;

        

         A76: omega = ( card ( omega \ A)) by A73, A74, CARD_2: 98, CARD_3: 42;

         [:(( omega \ A) /\ A), (( omega \ A) /\ ( omega \ A)):] = {} by A66, ZFMISC_1: 90;

        then ( [:( omega \ A), ( omega \ A):] /\ [:A, ( omega \ A):]) = {} by ZFMISC_1: 100;

        

        then (( [:( omega \ A), ( omega \ A):] \/ [:( omega \ A), A:]) /\ [:A, ( omega \ A):]) = ( {} \/ {} ) by A67, XBOOLE_1: 23

        .= {} ;

        then ( [:( omega \ A), ( omega \ A):] \/ [:( omega \ A), A:]) misses [:A, ( omega \ A):];

        

        then ( card (( [:( omega \ A), ( omega \ A):] \/ [:( omega \ A), A:]) \/ [:A, ( omega \ A):])) = (( card ( [:( omega \ A), ( omega \ A):] \/ [:( omega \ A), A:])) +` ( card [:A, ( omega \ A):])) by CARD_2: 35

        .= ((( card [:( omega \ A), ( omega \ A):]) +` ( card [:( omega \ A), A:])) +` ( card [:A, ( omega \ A):])) by A68, CARD_2: 35

        .= ((( card [:( omega \ A), ( omega \ A):]) +` ( card [: omega , N:])) +` ( card [:A, ( omega \ A):])) by A76, CARD_2: 7

        .= ((( card [: omega , omega :]) +` ( card [: omega , N:])) +` ( card [:A, ( omega \ A):])) by A76, CARD_2: 7

        .= (( omega +` ( card [: omega , N:])) +` ( card [:N, omega :])) by A76, Th5, CARD_2: 7

        .= (( omega +` ( omega *` N)) +` ( card [:N, omega :])) by CARD_2:def 2

        .= (( omega +` ( omega *` N)) +` (N *` omega )) by CARD_2:def 2;

        then ((( [:( omega \ A), ( omega \ A):] \/ [:( omega \ A), A:]) \/ [:A, ( omega \ A):]),( omega \ A)) are_equipotent by A76, A75, CARD_1: 5;

        then

        consider g be Function such that

         A77: g is one-to-one and

         A78: ( dom g) = (( [:( omega \ A), ( omega \ A):] \/ [:( omega \ A), A:]) \/ [:A, ( omega \ A):]) and

         A79: ( rng g) = ( omega \ A);

        

         A80: ( dom (g +* f)) = (( dom g) \/ ( dom f)) by FUNCT_4:def 1;

        

        then

         A81: ( dom (g +* f)) = (( [:( omega \ A), (( omega \ A) \/ A):] \/ [:A, ( omega \ A):]) \/ [:A, A:]) by A60, A78, ZFMISC_1: 97

        .= ( [:( omega \ A), (( omega \ A) \/ A):] \/ ( [:A, ( omega \ A):] \/ [:A, A:])) by XBOOLE_1: 4

        .= ( [:( omega \ A), (( omega \ A) \/ A):] \/ [:A, (( omega \ A) \/ A):]) by ZFMISC_1: 97

        .= [:(( omega \ A) \/ A), (( omega \ A) \/ A):] by ZFMISC_1: 97

        .= [:( omega \/ A), (( omega \ A) \/ A):] by XBOOLE_1: 39

        .= [:( omega \/ A), ( omega \/ A):] by XBOOLE_1: 39;

        ( {} \/ {} ) = {} ;

        then (( dom g) /\ ( dom f)) = {} by A60, A78, A71, A69, XBOOLE_1: 23;

        then

         A82: ( dom g) misses ( dom f);

        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

         A83: ( rng (g +* f)) = (( rng g) \/ ( rng f))

        .= ( omega \/ A) by A79, XBOOLE_1: 39;

        

         A84: (g +* f) is one-to-one

        proof

          ( rng f) misses ( rng g) by A79, XBOOLE_1: 79;

          then

           A85: (( rng f) /\ ( rng g)) = {} ;

          let x,y be object;

          assume that

           A86: x in ( dom (g +* f)) and

           A87: y in ( dom (g +* f));

          

           A88: y in ( dom g) or y in ( dom f) by A80, A87, XBOOLE_0:def 3;

          x in ( dom f) or x in ( dom g) by A80, A86, 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 A59, A77, A82, A88, FUNCT_1:def 3, FUNCT_4: 13, FUNCT_4: 16;

          hence thesis by A85, XBOOLE_0:def 4;

        end;

        set x = the Element of ( omega \ A);

        ( omega \ A) <> {} by A73, A74, CARD_1: 68, CARD_3: 42;

        then

         A89: x in omega & not x in A by XBOOLE_0:def 5;

        

         A90: ( omega \/ A) c= M by A55, A58, A62, XBOOLE_1: 8;

        then [:( omega \/ A), ( omega \/ A):] c= [:M, M:] by ZFMISC_1: 96;

        then (g +* f) in ( PFuncs ( [:M, M:],M)) by A83, A81, A90, PARTFUN1:def 3;

        then (g +* f) in X by A1, A83, A81, A84;

        then (g +* f) = f by A57, A58, FUNCT_4: 25;

        hence contradiction by A83, A89, XBOOLE_0:def 3;

      end;

       A91:

      now

        (N *` N) = ( card [:N, N:]) by CARD_2:def 2;

        then

         A92: (N *` N) = ( card [:A, A:]) by CARD_2: 7;

        ( [:A, A:],A) are_equipotent by A59, A60;

        then

         A93: (N *` N) = N by A92, CARD_1: 5;

        assume N <> M;

        then

         A94: N in M by A64, CARD_1: 3;

        (M +` N) = M by A54, A64, CARD_2: 76;

        then ( card (M \ A)) = M by A63, A94, CARD_2: 98;

        then

        consider h be Function such that

         A95: h is one-to-one & ( dom h) = A and

         A96: ( rng h) c= (M \ A) by A64, CARD_1: 10;

        set B = ( rng h);

        (A,B) are_equipotent by A95;

        then

         A97: N = ( card B) by CARD_1: 5;

        A misses (M \ A) & (A /\ B) c= (A /\ (M \ A)) by A96, XBOOLE_1: 26, XBOOLE_1: 79;

        then (A /\ B) c= {} ;

        then (A /\ B) = {} ;

        then

         A98: A misses B;

        ((A \/ B) \ A) = (B \ A) by XBOOLE_1: 40

        .= B by A98, XBOOLE_1: 83;

        then

         A99: [:B, B:] c= [:((A \/ B) \ A), (A \/ B):] by ZFMISC_1: 96;

         [:((A \/ B) \ A), (A \/ B):] c= ( [:((A \/ B) \ A), (A \/ B):] \/ [:(A \/ B), ((A \/ B) \ A):]) & ( [:(A \/ B), (A \/ B):] \ [:A, A:]) = ( [:((A \/ B) \ A), (A \/ B):] \/ [:(A \/ B), ((A \/ B) \ A):]) by XBOOLE_1: 7, ZFMISC_1: 103;

        then

         A100: [:B, B:] c= ( [:(A \/ B), (A \/ B):] \ [:A, A:]) by A99;

        (N +` N) = N by A65, CARD_2: 75;

        then ( card (A \/ B)) = N by A97, A98, CARD_2: 35;

        

        then ( card [:(A \/ B), (A \/ B):]) = ( card [:N, N:]) by CARD_2: 7

        .= N by A93, CARD_2:def 2;

        then

         A101: ( card ( [:(A \/ B), (A \/ B):] \ [:A, A:])) c= N by CARD_1: 11;

        N = ( card [:N, N:]) by A93, CARD_2:def 2;

        then N = ( card [:B, B:]) by A97, CARD_2: 7;

        then N c= ( card ( [:(A \/ B), (A \/ B):] \ [:A, A:])) by A100, CARD_1: 11;

        then ( card ( [:(A \/ B), (A \/ B):] \ [:A, A:])) = N by A101;

        then (( [:(A \/ B), (A \/ B):] \ [:A, A:]),B) are_equipotent by A97, CARD_1: 5;

        then

        consider g such that

         A102: g is one-to-one and

         A103: ( dom g) = ( [:(A \/ B), (A \/ B):] \ [:A, A:]) and

         A104: ( rng g) = B;

        

         A105: ( dom (g +* f)) = (( dom g) \/ ( dom f)) by FUNCT_4:def 1;

        then A c= (A \/ B) & ( dom (g +* f)) = ( [:(A \/ B), (A \/ B):] \/ [:A, A:]) by A60, A103, XBOOLE_1: 7, XBOOLE_1: 39;

        then

         A106: ( dom (g +* f)) = [:(A \/ B), (A \/ B):] by XBOOLE_1: 12, ZFMISC_1: 96;

        

         A107: ( [:(A \/ B), (A \/ B):] \ [:A, A:]) misses [:( rng f), ( rng f):] by XBOOLE_1: 79;

        

         A108: (g +* f) is one-to-one

        proof

          let x,y be object;

          assume that

           A109: x in ( dom (g +* f)) and

           A110: y in ( dom (g +* f));

          

           A111: y in ( dom g) or y in ( dom f) by A105, A110, XBOOLE_0:def 3;

          x in ( dom f) or x in ( dom g) by A105, A109, XBOOLE_0:def 3;

          then

           A112: ((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 A59, A60, A102, A103, A107, A111, FUNCT_1:def 3, FUNCT_4: 13, FUNCT_4: 16;

          A misses (M \ A) & (A /\ B) c= (A /\ (M \ A)) by A96, XBOOLE_1: 26, XBOOLE_1: 79;

          then

           A113: (( rng f) /\ ( rng g)) c= {} by A104;

          assume ((g +* f) . x) = ((g +* f) . y);

          hence thesis by A113, A112, XBOOLE_0:def 4;

        end;

        set x = the Element of B;

        

         A114: B <> {} by A65, A97;

        then x in (M \ A) by A96;

        then

         A115: not x in ( rng f) by XBOOLE_0:def 5;

        g c= (g +* f) by A60, A103, 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

         A116: (( 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

         A117: ( rng (g +* f)) = (( rng g) \/ ( rng f)) by A116;

        B c= M by A96, XBOOLE_1: 1;

        then

         A118: (A \/ B) c= M by A58, A62, XBOOLE_1: 8;

        then [:(A \/ B), (A \/ B):] c= [:M, M:] by ZFMISC_1: 96;

        then (g +* f) in ( PFuncs ( [:M, M:],M)) by A104, A117, A106, A118, PARTFUN1:def 3;

        then

         A119: (g +* f) in X by A1, A104, A117, A106, A108;

        x in ( rng (g +* f)) by A104, A117, A114, XBOOLE_0:def 3;

        hence contradiction by A57, A58, A119, A115, FUNCT_4: 25;

      end;

      

      then (M *` M) = ( card [:N, N:]) by CARD_2:def 2

      .= ( card [:A, A:]) by CARD_2: 7;

      hence thesis by A91, A61, CARD_1: 5;

    end;

    theorem :: CARD_4:16

    

     Th16: not M is finite & 0 in N & (N c= M or N in M) implies (M *` N) = M & (N *` M) = M

    proof

      

       A1: (1 *` M) = M by CARD_2: 21;

      assume not M is finite;

      then

       A2: (M *` M) = M by Th15;

      assume 0 in N;

      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;

      then (N *` M) c= (M *` M) by CARD_2: 90;

      hence thesis by A2, A3, A1;

    end;

    theorem :: CARD_4:17

    

     Th17: not M is finite & (N c= M or N in M) implies (M *` N) c= M & (N *` M) c= M

    proof

      assume not M is finite & (N c= M or N in 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;

      hence thesis;

    end;

    theorem :: CARD_4:18

     not X is finite implies ( [:X, X:],X) are_equipotent & ( card [:X, X:]) = ( card X)

    proof

      assume not X is finite;

      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 thesis by CARD_1: 5;

    end;

    theorem :: CARD_4:19

     not X is finite & Y is finite & Y <> {} implies ( [:X, Y:],X) are_equipotent & ( card [:X, Y:]) = ( card X)

    proof

      assume that

       A1: not X is finite and

       A2: Y is finite & Y <> {} ;

      ( 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 thesis by CARD_1: 5;

    end;

    theorem :: CARD_4:20

    K in L & M in N implies (K *` M) in (L *` N) & (M *` K) in (L *` N)

    proof

      

       A1: for K, L, M, N st K in L & M in N & L c= N holds (K *` M) in (L *` N)

      proof

        let K, L, M, N;

        assume that

         A2: K in L and

         A3: M in N and

         A4: L c= N;

         A5:

        now

          assume

           A6: N is finite;

          then

          reconsider N as finite Cardinal;

          reconsider L, M, K as finite Cardinal by A2, A3, A4, A6, CARD_3: 92;

          

           A7: ( card ( Segm N)) = N;

          ( card ( Segm M)) = M;

          then ( card M) < ( card N) by A3, A7, NAT_1: 41;

          then

           A8: (( card K) * ( card M)) <= (( card K) * ( card N)) by XREAL_1: 64;

          

           A9: ( card ( Segm L)) = L;

          

           A10: (L *` N) = ( card ( Segm (( card L) * ( card N)))) by CARD_2: 39;

          ( card ( Segm K)) = K;

          then ( card K) < ( card L) by A2, A9, NAT_1: 41;

          then (( card K) * ( card N)) < (( card L) * ( card N)) by A3, XREAL_1: 68;

          then

           A11: (( card K) * ( card M)) < (( card L) * ( card N)) by A8, XXREAL_0: 2;

          (K *` M) = ( card ( Segm (( card K) * ( card M)))) by CARD_2: 39;

          hence thesis by A10, A11, NAT_1: 41;

        end;

        

         A12: 0 in L by A2, ORDINAL3: 8;

        now

          assume

           A13: not N is finite;

          then

           A14: (L *` N) = N by A4, A12, Th16;

          

           A15: omega c= N by A13, CARD_3: 85;

           A16:

          now

            assume K is finite & M is finite;

            then

            reconsider K, M as finite Cardinal;

            (K *` M) = ( card (( card K) * ( card M))) by CARD_2: 39

            .= (( card K) * ( card M));

            hence thesis by A14, A15;

          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 thesis by A3, A14, A16, ORDINAL1: 12;

        end;

        hence thesis by A5;

      end;

      L c= N or N c= L;

      hence thesis by A1;

    end;

    theorem :: CARD_4:21

    

     Th21: not X is finite implies ( card X) = ( omega *` ( card X))

    proof

      assume

       A1: not X is finite;

      then omega c= ( card X) by CARD_3: 85;

      hence thesis by A1, Th16;

    end;

    theorem :: CARD_4:22

    X <> {} & X is finite & not Y is finite implies (( card Y) *` ( card X)) = ( card Y)

    proof

      assume that

       A1: X <> {} & X is finite and

       A2: not Y is finite;

      ( card X) in ( card Y) & 0 in ( card X) by A1, A2, CARD_3: 86, ORDINAL3: 8;

      hence thesis by A2, Th16;

    end;

    theorem :: CARD_4:23

    

     Th23: not D is finite & n <> 0 implies ((n -tuples_on D),D) are_equipotent & ( card (n -tuples_on D)) = ( card D)

    proof

      assume that

       A1: not D is finite and

       A2: n <> 0 ;

      defpred P[ Nat] means $1 <> 0 implies ( card ($1 -tuples_on D)) = ( card D);

      

       A3: for k be Nat holds P[k] implies P[(k + 1)]

      proof

        let k be Nat;

        ( 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;

        

         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 P[k];

        hence thesis by A1, A5, A4, Th16;

      end;

      

       A6: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A6, A3);

      then ( card (n -tuples_on D)) = ( card D) by A2;

      hence thesis by CARD_1: 5;

    end;

    theorem :: CARD_4:24

     not D is finite implies ( card D) = ( card (D * ))

    proof

      defpred P[ set] means not contradiction;

      deffunc f( Nat) = ($1 -tuples_on D);

      

       A1: (D * ) = ( union the set of all (k -tuples_on D)) by FINSEQ_2: 108;

      assume

       A2: not D is finite;

      

       A3: for X st X in the set of all (k -tuples_on D) holds ( card X) c= ( card D)

      proof

        let X;

        assume X in the set of all (k -tuples_on D);

        then

        consider k 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 thesis by A2, A4, Th23;

      end;

      (1 -tuples_on D) in the set of all (k -tuples_on D);

      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;

      { f(k) : P[k] } is countable from FraenCoun1;

      then ( card the set of all (k -tuples_on D)) c= omega ;

      then ( card ( union the set of all (k -tuples_on D))) c= ( omega *` ( card D)) by A3, CARD_2: 87;

      then ( card (D * )) c= ( card D) by A2, A1, Th21;

      hence thesis by A5;

    end;