card_2.miz



    begin

    reserve A,B for Ordinal,

K,M,N for Cardinal,

x,x1,x2,y,y1,y2,z,u for object,

X,Y,Z,X1,X2,Y1,Y2 for set,

f,g for Function;

    theorem :: CARD_2:1

    x in X & (X,Y) are_equipotent implies Y <> {} & ex x st x in Y

    proof

      assume

       A1: x in X;

      given f such that f is one-to-one and

       A2: ( dom f) = X & ( rng f) = Y;

      (f . x) in Y by A1, A2, FUNCT_1:def 3;

      hence Y <> {} ;

      take (f . x);

      thus thesis by A1, A2, FUNCT_1:def 3;

    end;

    theorem :: CARD_2:2

    (( bool X),( bool ( card X))) are_equipotent & ( card ( bool X)) = ( card ( bool ( card X)))

    proof

      consider f such that

       A1: f is one-to-one and

       A2: ( dom f) = X and

       A3: ( rng f) = ( card X) by CARD_1:def 2, WELLORD2:def 4;

      deffunc g( set) = (f .: $1);

      consider g such that

       A4: ( dom g) = ( bool X) & for x be set st x in ( bool X) holds (g . x) = g(x) from FUNCT_1:sch 5;

      thus (( bool X),( bool ( card X))) are_equipotent

      proof

        take g;

        thus g is one-to-one

        proof

          let x,y be object;

          assume that

           A5: x in ( dom g) and

           A6: y in ( dom g) and

           A7: (g . x) = (g . y);

          reconsider xx = x, yy = y as set by TARSKI: 1;

          

           A8: (g . x) = (f .: xx) & (g . y) = (f .: yy) by A4, A5, A6;

          

           A9: yy c= xx

          proof

            let z be object;

            assume

             A10: z in yy;

            then (f . z) in (f .: yy) by A2, A4, A6, FUNCT_1:def 6;

            then ex u be object st u in ( dom f) & u in xx & (f . z) = (f . u) by A7, A8, FUNCT_1:def 6;

            hence thesis by A1, A2, A4, A6, A10;

          end;

          xx c= yy

          proof

            let z be object;

            assume

             A11: z in xx;

            then (f . z) in (f .: xx) by A2, A4, A5, FUNCT_1:def 6;

            then ex u be object st u in ( dom f) & u in yy & (f . z) = (f . u) by A7, A8, FUNCT_1:def 6;

            hence thesis by A1, A2, A4, A5, A11;

          end;

          hence thesis by A9, XBOOLE_0:def 10;

        end;

        thus ( dom g) = ( bool X) by A4;

        thus ( rng g) c= ( bool ( card X))

        proof

          let x be object;

          assume x in ( rng g);

          then

          consider y be object such that

           A12: y in ( dom g) and

           A13: x = (g . y) by FUNCT_1:def 3;

          reconsider y as set by TARSKI: 1;

          

           A14: (f .: y) c= ( rng f) by RELAT_1: 111;

          (g . y) = (f .: y) by A4, A12;

          hence thesis by A3, A13, A14;

        end;

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        

         A15: (f " xx) c= ( dom f) by RELAT_1: 132;

        assume x in ( bool ( card X));

        then (f .: (f " xx)) = x by A3, FUNCT_1: 77;

        then (g . (f " xx)) = x by A2, A4, A15;

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

      end;

      hence thesis by CARD_1: 5;

    end;

    deffunc g( object) = ($1 `1 );

    theorem :: CARD_2:3

    Z in ( Funcs (X,Y)) implies (Z,X) are_equipotent & ( card Z) = ( card X)

    proof

      assume Z in ( Funcs (X,Y));

      then

      consider f such that

       A1: Z = f and

       A2: ( dom f) = X and ( rng f) c= Y by FUNCT_2:def 2;

      thus (Z,X) are_equipotent

      proof

        consider g such that

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

        take g;

        thus g is one-to-one

        proof

          let x,y be object;

          assume that

           A4: x in ( dom g) and

           A5: y in ( dom g);

          

           A6: (g . x) = (x `1 ) & (g . y) = (y `1 ) by A3, A4, A5;

          ex x1,x2 be object st [x1, x2] = y by A1, A3, A5, RELAT_1:def 1;

          then

           A7: y = [(y `1 ), (y `2 )];

          ex x1,x2 be object st [x1, x2] = x by A1, A3, A4, RELAT_1:def 1;

          then

           A8: x = [(x `1 ), (x `2 )];

          then (x `2 ) = (f . (x `1 )) by A1, A3, A4, FUNCT_1: 1;

          hence thesis by A1, A3, A5, A8, A7, A6, FUNCT_1: 1;

        end;

        thus ( dom g) = Z by A3;

        thus ( rng g) c= X

        proof

          let x be object;

          assume x in ( rng g);

          then

          consider y be object such that

           A9: y in ( dom g) and

           A10: x = (g . y) by FUNCT_1:def 3;

          ex x1,x2 be object st [x1, x2] = y by A1, A3, A9, RELAT_1:def 1;

          then

           A11: y = [(y `1 ), (y `2 )];

          x = (y `1 ) by A3, A9, A10;

          hence thesis by A1, A2, A3, A9, A11, FUNCT_1: 1;

        end;

        let x be object;

        assume x in X;

        then

         A12: [x, (f . x)] in Z by A1, A2, FUNCT_1:def 2;

        

        then (g . [x, (f . x)]) = ( [x, (f . x)] `1 ) by A3

        .= x;

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

      end;

      hence thesis by CARD_1: 5;

    end;

    

     Lm1: x1 <> x2 implies ((A +^ B),( [:A, {x1}:] \/ [:B, {x2}:])) are_equipotent & ( card (A +^ B)) = ( card ( [:A, {x1}:] \/ [:B, {x2}:]))

    proof

      defpred C[ set] means $1 in A;

      deffunc F( set) = [$1, x1];

      deffunc G( Ordinal) = [($1 -^ A), x2];

      consider f such that

       A1: ( dom f) = (A +^ B) and

       A2: for x be Ordinal holds x in (A +^ B) implies ( C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x)) from FINSET_1:sch 1;

      assume

       A3: x1 <> x2;

      thus ((A +^ B),( [:A, {x1}:] \/ [:B, {x2}:])) are_equipotent

      proof

        take f;

        thus f is one-to-one

        proof

          let x,y be object;

          assume that

           A4: x in ( dom f) & y in ( dom f) and

           A5: (f . x) = (f . y);

          reconsider C1 = x, C2 = y as Ordinal by A1, A4;

          per cases ;

            suppose

             A6: x in A & y in A;

            

             A7: ( [x, x1] `1 ) = C1 & ( [y, x1] `1 ) = C2;

            (f . C1) = [x, x1] & (f . C2) = [y, x1] by A1, A2, A4, A6;

            hence thesis by A5, A7;

          end;

            suppose

             A8: not x in A & not y in A;

            

             A9: ( [(C1 -^ A), x2] `1 ) = (C1 -^ A) & ( [(C2 -^ A), x2] `1 ) = (C2 -^ A);

            (f . x) = [(C1 -^ A), x2] & (f . y) = [(C2 -^ A), x2] by A1, A2, A4, A8;

            then

             A10: (C1 -^ A) = (C2 -^ A) by A5, A9;

            A c= C1 by A8, ORDINAL1: 16;

            then

             A11: C1 = (A +^ (C1 -^ A)) by ORDINAL3:def 5;

            A c= C2 by A8, ORDINAL1: 16;

            hence thesis by A10, A11, ORDINAL3:def 5;

          end;

            suppose

             A12: x in A & not y in A;

            

             A13: ( [x, x1] `2 ) = x1 & ( [(C2 -^ A), x2] `2 ) = x2;

            (f . x) = [x, x1] & (f . y) = [(C2 -^ A), x2] by A1, A2, A4, A12;

            hence thesis by A3, A5, A13;

          end;

            suppose

             A14: not x in A & y in A;

            

             A15: ( [y, x1] `2 ) = x1 & ( [(C1 -^ A), x2] `2 ) = x2;

            (f . y) = [y, x1] & (f . x) = [(C1 -^ A), x2] by A1, A2, A4, A14;

            hence thesis by A3, A5, A15;

          end;

        end;

        thus ( dom f) = (A +^ B) by A1;

        thus ( rng f) c= ( [:A, {x1}:] \/ [:B, {x2}:])

        proof

          let x be object;

          

           A16: x1 in {x1} by TARSKI:def 1;

          

           A17: x2 in {x2} by TARSKI:def 1;

          assume x in ( rng f);

          then

          consider y be object such that

           A18: y in ( dom f) and

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

          reconsider C = y as Ordinal by A1, A18;

          per cases ;

            suppose y in A;

            then x = [C, x1] & [C, x1] in [:A, {x1}:] by A1, A2, A18, A19, A16, ZFMISC_1: 87;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose

             A20: not y in A;

            then A c= C by ORDINAL1: 16;

            then (A +^ (C -^ A)) = C by ORDINAL3:def 5;

            then (C -^ A) in B by A1, A18, ORDINAL3: 22;

            then

             A21: [(C -^ A), x2] in [:B, {x2}:] by A17, ZFMISC_1: 87;

            x = [(C -^ A), x2] by A1, A2, A18, A19, A20;

            hence thesis by A21, XBOOLE_0:def 3;

          end;

        end;

        let x be object such that

         A22: x in ( [:A, {x1}:] \/ [:B, {x2}:]);

         A23:

        now

          assume x in [:B, {x2}:];

          then

          consider y,z be object such that

           A24: y in B and

           A25: z in {x2} and

           A26: x = [y, z] by ZFMISC_1: 84;

          reconsider y as Ordinal by A24;

          

           A27: (A +^ y) in (A +^ B) by A24, ORDINAL2: 32;

          

           A28: not (A +^ y) in A by ORDINAL1: 5, ORDINAL3: 24;

          ((A +^ y) -^ A) = y & z = x2 by A25, ORDINAL3: 52, TARSKI:def 1;

          then x = (f . (A +^ y)) by A2, A26, A27, A28;

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

        end;

        now

          assume x in [:A, {x1}:];

          then

          consider y,z be object such that

           A29: y in A and

           A30: z in {x1} and

           A31: x = [y, z] by ZFMISC_1: 84;

          

           A32: A c= (A +^ B) by ORDINAL3: 24;

          z = x1 by A30, TARSKI:def 1;

          then x = (f . y) by A2, A29, A31, A32;

          hence thesis by A1, A29, A32, FUNCT_1:def 3;

        end;

        hence thesis by A22, A23, XBOOLE_0:def 3;

      end;

      hence thesis by CARD_1: 5;

    end;

    deffunc plus( set, set) = ( [:$1, { 0 }:] \/ [:$2, {1}:]);

    

     Lm2: ( [:X, Y:], [:Y, X:]) are_equipotent & ( card [:X, Y:]) = ( card [:Y, X:])

    proof

      deffunc f( object) = [($1 `2 ), ($1 `1 )];

      consider f such that

       A1: ( dom f) = [:X, Y:] & for x be object st x in [:X, Y:] holds (f . x) = f(x) from FUNCT_1:sch 3;

      thus ( [:X, Y:], [:Y, X:]) are_equipotent

      proof

        take f;

        thus f is one-to-one

        proof

          let x,y be object;

          assume

           A2: x in ( dom f) & y in ( dom f);

          then

           A3: x = [(x `1 ), (x `2 )] & y = [(y `1 ), (y `2 )] by A1, MCART_1: 21;

          assume

           A4: (f . x) = (f . y);

          

           A5: (f . x) = [(x `2 ), (x `1 )] & (f . y) = [(y `2 ), (y `1 )] by A1, A2;

          then (x `1 ) = (y `1 ) by A4, XTUPLE_0: 1;

          hence thesis by A3, A5, A4, XTUPLE_0: 1;

        end;

        thus ( dom f) = [:X, Y:] by A1;

        thus ( rng f) c= [:Y, X:]

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A6: y in ( dom f) and

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

          

           A8: (y `2 ) in Y by A1, A6, MCART_1: 10;

          x = [(y `2 ), (y `1 )] & (y `1 ) in X by A1, A6, A7, MCART_1: 10;

          hence thesis by A8, ZFMISC_1: 87;

        end;

        let x be object;

        

         A9: ( [(x `2 ), (x `1 )] `1 ) = (x `2 ) & ( [(x `2 ), (x `1 )] `2 ) = (x `1 );

        assume

         A10: x in [:Y, X:];

        then

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

        

         A12: (x `1 ) in Y & (x `2 ) in X by A10, MCART_1: 10;

        then [(x `2 ), (x `1 )] in [:X, Y:] by ZFMISC_1: 87;

        then (f . [(x `2 ), (x `1 )]) in ( rng f) by A1, FUNCT_1:def 3;

        hence thesis by A1, A11, A12, A9, ZFMISC_1: 87;

      end;

      hence thesis by CARD_1: 5;

    end;

    definition

      let M, N;

      :: CARD_2:def1

      func M +` N -> Cardinal equals ( card (M +^ N));

      coherence ;

      commutativity

      proof

        let C be Cardinal;

        let M, N;

        assume C = ( card (M +^ N));

        

        hence C = ( card plus(N,M)) by Lm1

        .= ( card (N +^ M)) by Lm1;

      end;

      :: CARD_2:def2

      func M *` N -> Cardinal equals ( card [:M, N:]);

      coherence ;

      commutativity by Lm2;

      :: CARD_2:def3

      func exp (M,N) -> Cardinal equals ( card ( Funcs (N,M)));

      coherence ;

    end

    theorem :: CARD_2:4

    

     Th4: ( [:X, Y:], [:Y, X:]) are_equipotent & ( card [:X, Y:]) = ( card [:Y, X:]) by Lm2;

    theorem :: CARD_2:5

    

     Th5: ( [: [:X, Y:], Z:], [:X, [:Y, Z:]:]) are_equipotent & ( card [: [:X, Y:], Z:]) = ( card [:X, [:Y, Z:]:])

    proof

      deffunc f( object) = [(($1 `1 ) `1 ), [(($1 `1 ) `2 ), ($1 `2 )]];

      consider f such that

       A1: ( dom f) = [: [:X, Y:], Z:] & for x be object st x in [: [:X, Y:], Z:] holds (f . x) = f(x) from FUNCT_1:sch 3;

      thus ( [: [:X, Y:], Z:], [:X, [:Y, Z:]:]) are_equipotent

      proof

        take f;

        thus f is one-to-one

        proof

          let x,y be object;

          assume that

           A2: x in ( dom f) and

           A3: y in ( dom f);

          assume

           A4: (f . x) = (f . y);

          

           A5: x = [(x `1 ), (x `2 )] & y = [(y `1 ), (y `2 )] by A1, A2, A3, MCART_1: 21;

          (x `1 ) in [:X, Y:] by A1, A2, MCART_1: 10;

          then

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

          

           A7: (f . x) = [((x `1 ) `1 ), [((x `1 ) `2 ), (x `2 )]] & (f . y) = [((y `1 ) `1 ), [((y `1 ) `2 ), (y `2 )]] by A1, A2, A3;

          then

           A8: ((x `1 ) `1 ) = ((y `1 ) `1 ) by A4, XTUPLE_0: 1;

          (y `1 ) in [:X, Y:] by A1, A3, MCART_1: 10;

          then

           A9: (y `1 ) = [((y `1 ) `1 ), ((y `1 ) `2 )] by MCART_1: 21;

          

           A10: [((x `1 ) `2 ), (x `2 )] = [((y `1 ) `2 ), (y `2 )] by A7, A4, XTUPLE_0: 1;

          then ((x `1 ) `2 ) = ((y `1 ) `2 ) by XTUPLE_0: 1;

          hence thesis by A5, A8, A10, A6, A9, XTUPLE_0: 1;

        end;

        thus ( dom f) = [: [:X, Y:], Z:] by A1;

        thus ( rng f) c= [:X, [:Y, Z:]:]

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A11: y in ( dom f) and

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

          

           A13: (y `1 ) in [:X, Y:] by A1, A11, MCART_1: 10;

          then

           A14: ((y `1 ) `2 ) in Y by MCART_1: 10;

          (y `2 ) in Z by A1, A11, MCART_1: 10;

          then

           A15: [((y `1 ) `2 ), (y `2 )] in [:Y, Z:] by A14, ZFMISC_1: 87;

          

           A16: ((y `1 ) `1 ) in X by A13, MCART_1: 10;

          x = [((y `1 ) `1 ), [((y `1 ) `2 ), (y `2 )]] by A1, A11, A12;

          hence thesis by A16, A15, ZFMISC_1: 87;

        end;

        let x be object;

        

         A17: ( [(x `1 ), ((x `2 ) `1 )] `1 ) = (x `1 ) & ( [(x `1 ), ((x `2 ) `1 )] `2 ) = ((x `2 ) `1 );

        

         A18: ( [ [(x `1 ), ((x `2 ) `1 )], ((x `2 ) `2 )] `1 ) = [(x `1 ), ((x `2 ) `1 )] & ( [ [(x `1 ), ((x `2 ) `1 )], ((x `2 ) `2 )] `2 ) = ((x `2 ) `2 );

        assume

         A19: x in [:X, [:Y, Z:]:];

        then

         A20: (x `2 ) in [:Y, Z:] by MCART_1: 10;

        then

         A21: ((x `2 ) `1 ) in Y by MCART_1: 10;

        

         A22: ((x `2 ) `2 ) in Z by A20, MCART_1: 10;

        (x `1 ) in X by A19, MCART_1: 10;

        then

         A23: [(x `1 ), ((x `2 ) `1 )] in [:X, Y:] by A21, ZFMISC_1: 87;

        then

         A24: [ [(x `1 ), ((x `2 ) `1 )], ((x `2 ) `2 )] in [: [:X, Y:], Z:] by A22, ZFMISC_1: 87;

        

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

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

        then x = (f . [ [(x `1 ), ((x `2 ) `1 )], ((x `2 ) `2 )]) by A1, A25, A17, A23, A18, A22, ZFMISC_1: 87;

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

      end;

      hence thesis by CARD_1: 5;

    end;

    

     Lm3: ( [:X, Y:], [:( card X), Y:]) are_equipotent

    proof

      consider f such that

       A1: f is one-to-one and

       A2: ( dom f) = X and

       A3: ( rng f) = ( card X) by CARD_1:def 2, WELLORD2:def 4;

      deffunc g( object) = [(f . ($1 `1 )), ($1 `2 )];

      consider g such that

       A4: ( dom g) = [:X, Y:] & for x be object st x in [:X, Y:] holds (g . x) = g(x) from FUNCT_1:sch 3;

      take g;

      thus g is one-to-one

      proof

        let x,y be object;

        assume

         A5: x in ( dom g) & y in ( dom g);

        then

         A6: (x `1 ) in X & (y `1 ) in X by A4, MCART_1: 10;

        assume

         A7: (g . x) = (g . y);

        (g . x) = [(f . (x `1 )), (x `2 )] & (g . y) = [(f . (y `1 )), (y `2 )] by A4, A5;

        then

         A8: (f . (x `1 )) = (f . (y `1 )) & (x `2 ) = (y `2 ) by A7, XTUPLE_0: 1;

        x = [(x `1 ), (x `2 )] & y = [(y `1 ), (y `2 )] by A4, A5, MCART_1: 21;

        hence thesis by A1, A2, A6, A8;

      end;

      thus ( dom g) = [:X, Y:] by A4;

      thus ( rng g) c= [:( card X), Y:]

      proof

        let y be object;

        assume y in ( rng g);

        then

        consider x be object such that

         A9: x in ( dom g) and

         A10: y = (g . x) by FUNCT_1:def 3;

        (x `1 ) in X by A4, A9, MCART_1: 10;

        then

         A11: (f . (x `1 )) in ( card X) by A2, A3, FUNCT_1:def 3;

        y = [(f . (x `1 )), (x `2 )] & (x `2 ) in Y by A4, A9, A10, MCART_1: 10;

        hence thesis by A11, ZFMISC_1: 87;

      end;

      let y be object;

      assume

       A12: y in [:( card X), Y:];

      then (y `1 ) in ( card X) by MCART_1: 10;

      then

      consider x be object such that

       A13: x in X and

       A14: (y `1 ) = (f . x) by A2, A3, FUNCT_1:def 3;

      

       A15: y = [(y `1 ), (y `2 )] by A12, MCART_1: 21;

      

       A16: (y `2 ) in Y by A12, MCART_1: 10;

      then

       A17: [x, (y `2 )] in [:X, Y:] by A13, ZFMISC_1: 87;

      ( [x, (y `2 )] `1 ) = x & ( [x, (y `2 )] `2 ) = (y `2 );

      then (g . [x, (y `2 )]) = y by A4, A15, A14, A16, A13, ZFMISC_1: 87;

      hence thesis by A4, A17, FUNCT_1:def 3;

    end;

    ::$Canceled

    theorem :: CARD_2:7

    

     Th6: ( [:X, Y:], [:( card X), Y:]) are_equipotent & ( [:X, Y:], [:X, ( card Y):]) are_equipotent & ( [:X, Y:], [:( card X), ( card Y):]) are_equipotent & ( card [:X, Y:]) = ( card [:( card X), Y:]) & ( card [:X, Y:]) = ( card [:X, ( card Y):]) & ( card [:X, Y:]) = ( card [:( card X), ( card Y):])

    proof

      ( [:Y, X:], [:( card Y), X:]) are_equipotent & ( [:X, Y:], [:Y, X:]) are_equipotent by Lm2, Lm3;

      then

       A1: ( [:X, Y:], [:( card Y), X:]) are_equipotent by WELLORD2: 15;

      

       A2: ( [:( card Y), X:], [:X, ( card Y):]) are_equipotent by Lm2;

      hence

       A3: ( [:X, Y:], [:( card X), Y:]) are_equipotent & ( [:X, Y:], [:X, ( card Y):]) are_equipotent by A1, Lm3, WELLORD2: 15;

      ( [:X, ( card Y):], [:( card X), ( card Y):]) are_equipotent by Lm3;

      hence ( [:X, Y:], [:( card X), ( card Y):]) are_equipotent by A3, WELLORD2: 15;

      hence thesis by A2, A1, Lm3, CARD_1: 5, WELLORD2: 15;

    end;

    theorem :: CARD_2:8

    

     Th7: (X1,Y1) are_equipotent & (X2,Y2) are_equipotent implies ( [:X1, X2:], [:Y1, Y2:]) are_equipotent & ( card [:X1, X2:]) = ( card [:Y1, Y2:])

    proof

      assume (X1,Y1) are_equipotent & (X2,Y2) are_equipotent ;

      then

       A1: ( card X1) = ( card Y1) & ( card X2) = ( card Y2) by CARD_1: 5;

      ( [:X1, X2:], [:( card X1), ( card X2):]) are_equipotent & ( [:Y1, Y2:], [:( card Y1), ( card Y2):]) are_equipotent by Th6;

      hence ( [:X1, X2:], [:Y1, Y2:]) are_equipotent by A1, WELLORD2: 15;

      hence thesis by CARD_1: 5;

    end;

    theorem :: CARD_2:9

    x1 <> x2 implies ((A +^ B),( [:A, {x1}:] \/ [:B, {x2}:])) are_equipotent & ( card (A +^ B)) = ( card ( [:A, {x1}:] \/ [:B, {x2}:])) by Lm1;

    theorem :: CARD_2:10

    

     Th9: x1 <> x2 implies ((K +` M),( [:K, {x1}:] \/ [:M, {x2}:])) are_equipotent & (K +` M) = ( card ( [:K, {x1}:] \/ [:M, {x2}:]))

    proof

      assume x1 <> x2;

      then ( card ( [:K, {x1}:] \/ [:M, {x2}:])) = (K +` M) by Lm1;

      hence thesis by CARD_1:def 2;

    end;

    theorem :: CARD_2:11

    

     Th10: ((A *^ B), [:A, B:]) are_equipotent & ( card (A *^ B)) = ( card [:A, B:])

    proof

      defpred P[ object, object] means ex O1,O2 be Ordinal st O1 = ($1 `1 ) & O2 = ($1 `2 ) & $2 = ((O1 *^ B) +^ O2);

      

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

      proof

        let x be object;

        assume x in [:A, B:];

        then (x `1 ) in A & (x `2 ) in B by MCART_1: 10;

        then

        reconsider x1 = (x `1 ), x2 = (x `2 ) as Ordinal;

        take ((x1 *^ B) +^ x2);

        take x1, x2;

        thus thesis;

      end;

      consider f such that

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

      

       A3: ( [:A, B:],(A *^ B)) are_equipotent

      proof

        take f;

        thus f is one-to-one

        proof

          let x,y be object;

          assume

           A4: x in ( dom f) & y in ( dom f);

          then

           A5: (x `2 ) in B & (y `2 ) in B by A2, MCART_1: 10;

          (x `1 ) in A & (y `1 ) in A by A2, A4, MCART_1: 10;

          then

          reconsider x1 = (x `1 ), y1 = (y `1 ) as Ordinal;

          assume

           A6: (f . x) = (f . y);

          

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

          

           A8: (ex O1,O2 be Ordinal st O1 = (x `1 ) & O2 = (x `2 ) & (f . x) = ((O1 *^ B) +^ O2)) & ex O3,O4 be Ordinal st O3 = (y `1 ) & O4 = (y `2 ) & (f . y) = ((O3 *^ B) +^ O4) by A2, A4;

          then x1 = y1 by A5, A6, ORDINAL3: 48;

          hence thesis by A7, A5, A8, A6, ORDINAL3: 48;

        end;

        thus ( dom f) = [:A, B:] by A2;

        thus ( rng f) c= (A *^ B)

        proof

          let y be object;

          

           A9: (1 *^ B) = B by ORDINAL2: 39;

          assume y in ( rng f);

          then

          consider x be object such that

           A10: x in ( dom f) and

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

          consider x1,x2 be Ordinal such that

           A12: x1 = (x `1 ) and

           A13: x2 = (x `2 ) & (f . x) = ((x1 *^ B) +^ x2) by A2, A10;

          (x1 +^ 1) = ( succ x1) by ORDINAL2: 31;

          then

           A14: ((x1 *^ B) +^ (1 *^ B)) = (( succ x1) *^ B) by ORDINAL3: 46;

          ( succ x1) c= A by A12, A2, A10, MCART_1: 10, ORDINAL1: 21;

          then

           A15: ((x1 *^ B) +^ (1 *^ B)) c= (A *^ B) by A14, ORDINAL2: 41;

          y in ((x1 *^ B) +^ (1 *^ B)) by A11, A13, A9, A2, A10, MCART_1: 10, ORDINAL2: 32;

          hence thesis by A15;

        end;

        let y be object;

        assume

         A16: y in (A *^ B);

        then

        reconsider C = y as Ordinal;

        

         A17: C = (((C div^ B) *^ B) +^ (C mod^ B)) & ( [(C div^ B), (C mod^ B)] `1 ) = (C div^ B) by ORDINAL3: 65;

        (C div^ B) in A & (C mod^ B) in B by A16, ORDINAL3: 67;

        then

         A18: [(C div^ B), (C mod^ B)] in [:A, B:] by ZFMISC_1: 87;

        then ( [(C div^ B), (C mod^ B)] `2 ) = (C mod^ B) & ex O1,O2 be Ordinal st O1 = ( [(C div^ B), (C mod^ B)] `1 ) & O2 = ( [(C div^ B), (C mod^ B)] `2 ) & (f . [(C div^ B), (C mod^ B)]) = ((O1 *^ B) +^ O2) by A2;

        hence thesis by A2, A18, A17, FUNCT_1:def 3;

      end;

      hence ((A *^ B), [:A, B:]) are_equipotent ;

      thus thesis by A3, CARD_1: 5;

    end;

    deffunc plus( set, set) = ( [:$1, { 0 }:] \/ [:$2, {1}:]);

    deffunc plus( set, set, object, object) = ( [:$1, {$3}:] \/ [:$2, {$4}:]);

    theorem :: CARD_2:12

    

     Th11: (X1,Y1) are_equipotent & (X2,Y2) are_equipotent & x1 <> x2 & y1 <> y2 implies (( [:X1, {x1}:] \/ [:X2, {x2}:]),( [:Y1, {y1}:] \/ [:Y2, {y2}:])) are_equipotent & ( card ( [:X1, {x1}:] \/ [:X2, {x2}:])) = ( card ( [:Y1, {y1}:] \/ [:Y2, {y2}:]))

    proof

      assume that

       A1: (X1,Y1) are_equipotent and

       A2: (X2,Y2) are_equipotent and

       A3: x1 <> x2 and

       A4: y1 <> y2;

      ( {x2}, {y2}) are_equipotent by CARD_1: 28;

      then

       A5: ( [:X2, {x2}:], [:Y2, {y2}:]) are_equipotent by A2, Th7;

       A6:

      now

        assume [:Y1, {y1}:] meets [:Y2, {y2}:];

        then

        consider y be object such that

         A7: y in [:Y1, {y1}:] and

         A8: y in [:Y2, {y2}:] by XBOOLE_0: 3;

        (y `2 ) in {y1} by A7, MCART_1: 10;

        then

         A9: (y `2 ) = y1 by TARSKI:def 1;

        (y `2 ) in {y2} by A8, MCART_1: 10;

        hence contradiction by A4, A9, TARSKI:def 1;

      end;

       A10:

      now

        assume [:X1, {x1}:] meets [:X2, {x2}:];

        then

        consider x be object such that

         A11: x in [:X1, {x1}:] and

         A12: x in [:X2, {x2}:] by XBOOLE_0: 3;

        (x `2 ) in {x1} by A11, MCART_1: 10;

        then

         A13: (x `2 ) = x1 by TARSKI:def 1;

        (x `2 ) in {x2} by A12, MCART_1: 10;

        hence contradiction by A3, A13, TARSKI:def 1;

      end;

      ( {x1}, {y1}) are_equipotent by CARD_1: 28;

      then ( [:X1, {x1}:], [:Y1, {y1}:]) are_equipotent by A1, Th7;

      hence (( [:X1, {x1}:] \/ [:X2, {x2}:]),( [:Y1, {y1}:] \/ [:Y2, {y2}:])) are_equipotent by A5, A10, A6, CARD_1: 31;

      hence thesis by CARD_1: 5;

    end;

    theorem :: CARD_2:13

    

     Th12: ( card (A +^ B)) = (( card A) +` ( card B))

    proof

      

       A1: ((A +^ B), plus(A,B)) are_equipotent by Lm1;

      (A,( card A)) are_equipotent & (B,( card B)) are_equipotent by CARD_1:def 2;

      then

       A2: ( plus(A,B), plus(card,card)) are_equipotent by Th11;

      ( plus(card,card),(( card A) +^ ( card B))) are_equipotent by Lm1;

      then ( plus(A,B),(( card A) +^ ( card B))) are_equipotent by A2, WELLORD2: 15;

      then ((A +^ B),(( card A) +^ ( card B))) are_equipotent by A1, WELLORD2: 15;

      hence thesis by CARD_1: 5;

    end;

    theorem :: CARD_2:14

    

     Th13: ( card (A *^ B)) = (( card A) *` ( card B))

    proof

      

      thus ( card (A *^ B)) = ( card [:A, B:]) by Th10

      .= (( card A) *` ( card B)) by Th6;

    end;

    theorem :: CARD_2:15

    (( [:X, { 0 }:] \/ [:Y, {1}:]),( [:Y, { 0 }:] \/ [:X, {1}:])) are_equipotent & ( card ( [:X, { 0 }:] \/ [:Y, {1}:])) = ( card ( [:Y, { 0 }:] \/ [:X, {1}:])) by Th11;

    theorem :: CARD_2:16

    

     Th15: (( [:X1, X2:] \/ [:Y1, Y2:]),( [:X2, X1:] \/ [:Y2, Y1:])) are_equipotent & ( card ( [:X1, X2:] \/ [:Y1, Y2:])) = ( card ( [:X2, X1:] \/ [:Y2, Y1:]))

    proof

      deffunc f( object) = [($1 `2 ), ($1 `1 )];

      consider f such that

       A1: ( dom f) = ( [:X1, X2:] \/ [:Y1, Y2:]) & for x be object st x in ( [:X1, X2:] \/ [:Y1, Y2:]) holds (f . x) = f(x) from FUNCT_1:sch 3;

      thus (( [:X1, X2:] \/ [:Y1, Y2:]),( [:X2, X1:] \/ [:Y2, Y1:])) are_equipotent

      proof

        take f;

        thus f is one-to-one

        proof

          let x1,x2 be object;

          assume that

           A2: x1 in ( dom f) and

           A3: x2 in ( dom f) and

           A4: (f . x1) = (f . x2);

          x1 in [:X1, X2:] or x1 in [:Y1, Y2:] by A1, A2, XBOOLE_0:def 3;

          then

           A5: x1 = [(x1 `1 ), (x1 `2 )] by MCART_1: 21;

          x2 in [:X1, X2:] or x2 in [:Y1, Y2:] by A1, A3, XBOOLE_0:def 3;

          then

           A6: x2 = [(x2 `1 ), (x2 `2 )] by MCART_1: 21;

          

           A7: (f . x1) = [(x1 `2 ), (x1 `1 )] & (f . x2) = [(x2 `2 ), (x2 `1 )] by A1, A2, A3;

          then (x1 `1 ) = (x2 `1 ) by A4, XTUPLE_0: 1;

          hence thesis by A4, A7, A5, A6, XTUPLE_0: 1;

        end;

        thus ( dom f) = ( [:X1, X2:] \/ [:Y1, Y2:]) by A1;

        thus ( rng f) c= ( [:X2, X1:] \/ [:Y2, Y1:])

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A8: y in ( dom f) and

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

          y in [:X1, X2:] or y in [:Y1, Y2:] by A1, A8, XBOOLE_0:def 3;

          then

           A10: (y `1 ) in X1 & (y `2 ) in X2 or (y `1 ) in Y1 & (y `2 ) in Y2 by MCART_1: 10;

          x = [(y `2 ), (y `1 )] by A1, A8, A9;

          then x in [:X2, X1:] or x in [:Y2, Y1:] by A10, ZFMISC_1: 87;

          hence thesis by XBOOLE_0:def 3;

        end;

        let x be object;

        

         A11: ( [(x `2 ), (x `1 )] `1 ) = (x `2 ) & ( [(x `2 ), (x `1 )] `2 ) = (x `1 );

        assume x in ( [:X2, X1:] \/ [:Y2, Y1:]);

        then

         A12: x in [:X2, X1:] or x in [:Y2, Y1:] by XBOOLE_0:def 3;

        then (x `1 ) in X2 & (x `2 ) in X1 or (x `1 ) in Y2 & (x `2 ) in Y1 by MCART_1: 10;

        then [(x `2 ), (x `1 )] in [:X1, X2:] or [(x `2 ), (x `1 )] in [:Y1, Y2:] by ZFMISC_1: 87;

        then

         A13: [(x `2 ), (x `1 )] in ( [:X1, X2:] \/ [:Y1, Y2:]) by XBOOLE_0:def 3;

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

        then (f . [(x `2 ), (x `1 )]) = x by A1, A13, A11;

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

      end;

      hence thesis by CARD_1: 5;

    end;

    theorem :: CARD_2:17

    

     Th16: x <> y implies (( card X) +` ( card Y)) = ( card ( [:X, {x}:] \/ [:Y, {y}:]))

    proof

      assume

       A1: x <> y;

      (X,( card X)) are_equipotent & (Y,( card Y)) are_equipotent by CARD_1:def 2;

      then ( card plus(X,Y,x,y)) = ( card plus(card,card,x,y)) by A1, Th11;

      hence thesis by A1, Lm1;

    end;

    theorem :: CARD_2:18

    (M +` 0 ) = M

    proof

      

      thus (M +` 0 ) = ( card plus(M,{})) by Lm1

      .= ( card M) by CARD_1: 69

      .= M;

    end;

    

     Lm4: x <> y implies [:X, {x}:] misses [:Y, {y}:]

    proof

      assume

       A1: x <> y;

      assume not thesis;

      then

      consider z be object such that

       A2: z in [:X, {x}:] and

       A3: z in [:Y, {y}:] by XBOOLE_0: 3;

      (z `2 ) = x by A2, MCART_1: 13;

      hence contradiction by A1, A3, MCART_1: 13;

    end;

    theorem :: CARD_2:19

    

     Th18: ((K +` M) +` N) = (K +` (M +` N))

    proof

      

       A1: ( card ((K +` M) +` N)) = ((K +` M) +` N);

      

       A2: (((K +` M) +` N),( [:(K +` M), { 0 }:] \/ [:N, {2}:])) are_equipotent by Th9;

       [:M, {1}:] misses [:N, {2}:] by Lm4;

      then

       A3: ( [:M, {1}:] /\ [:N, {2}:]) = {} ;

       [:K, { 0 }:] misses [:N, {2}:] by Lm4;

      then ( [:K, { 0 }:] /\ [:N, {2}:]) = {} ;

      

      then (( [:K, { 0 }:] \/ [:M, {1}:]) /\ [:N, {2}:]) = ( {} \/ {} ) by A3, XBOOLE_1: 23

      .= {} ;

      then

       A4: ( [:K, { 0 }:] \/ [:M, {1}:]) misses [:N, {2}:];

      ((K +` M),( [:K, { 0 }:] \/ [:M, {1}:])) are_equipotent & ((K +` M), [:(K +` M), { 0 }:]) are_equipotent by CARD_1: 69, Th9;

      then

       A5: ( [:(K +` M), { 0 }:],( [:K, { 0 }:] \/ [:M, {1}:])) are_equipotent by WELLORD2: 15;

       [:K, { 0 }:] misses [:N, {2}:] by Lm4;

      then

       A6: ( [:K, { 0 }:] /\ [:N, {2}:]) = {} ;

       [:K, { 0 }:] misses [:M, {1}:] by Lm4;

      then ( [:K, { 0 }:] /\ [:M, {1}:]) = {} ;

      

      then ( [:K, { 0 }:] /\ ( [:M, {1}:] \/ [:N, {2}:])) = ( {} \/ {} ) by A6, XBOOLE_1: 23

      .= {} ;

      then

       A7: [:K, { 0 }:] misses ( [:M, {1}:] \/ [:N, {2}:]);

      ((M +` N),( [:M, {1}:] \/ [:N, {2}:])) are_equipotent & ((M +` N), [:(M +` N), {2}:]) are_equipotent by CARD_1: 69, Th9;

      then

       A8: ( [:(M +` N), {2}:],( [:M, {1}:] \/ [:N, {2}:])) are_equipotent by WELLORD2: 15;

       [:K, { 0 }:] misses [:(M +` N), {2}:] by Lm4;

      then

       A9: (( [:K, { 0 }:] \/ ( [:M, {1}:] \/ [:N, {2}:])),( [:K, { 0 }:] \/ [:(M +` N), {2}:])) are_equipotent by A7, A8, CARD_1: 31;

       [:(K +` M), { 0 }:] misses [:N, {2}:] by Lm4;

      then

       A10: (( [:(K +` M), { 0 }:] \/ [:N, {2}:]),(( [:K, { 0 }:] \/ [:M, {1}:]) \/ [:N, {2}:])) are_equipotent by A4, A5, CARD_1: 31;

      ( [:K, { 0 }:] \/ ( [:M, {1}:] \/ [:N, {2}:])) = (( [:K, { 0 }:] \/ [:M, {1}:]) \/ [:N, {2}:]) by XBOOLE_1: 4;

      then (( [:(K +` M), { 0 }:] \/ [:N, {2}:]),( [:K, { 0 }:] \/ [:(M +` N), {2}:])) are_equipotent by A10, A9, WELLORD2: 15;

      then

       A11: (((K +` M) +` N),( [:K, { 0 }:] \/ [:(M +` N), {2}:])) are_equipotent by A2, WELLORD2: 15;

      (( [:K, { 0 }:] \/ [:(M +` N), {2}:]),(K +` (M +` N))) are_equipotent by Th9;

      then (((K +` M) +` N),(K +` (M +` N))) are_equipotent by A11, WELLORD2: 15;

      hence thesis by A1, CARD_1:def 2;

    end;

    theorem :: CARD_2:20

    (K *` 0 ) = 0 ;

    theorem :: CARD_2:21

    

     Th20: (K *` 1) = K

    proof

      K = ( card K);

      hence thesis by CARD_1: 69, ORDINAL3: 15;

    end;

    theorem :: CARD_2:22

    

     Th21: ((K *` M) *` N) = (K *` (M *` N))

    proof

      

      thus ((K *` M) *` N) = ( card [: [:K, M:], N:]) by Th6

      .= ( card [:K, [:M, N:]:]) by Th5

      .= (K *` (M *` N)) by Th6;

    end;

    theorem :: CARD_2:23

    

     Th22: (2 *` K) = (K +` K)

    proof

      

      thus (2 *` K) = ( card ( [: { {} }, K:] \/ [: {1}, K:])) by CARD_1: 50, ZFMISC_1: 109

      .= ( card ( [:K, { {} }:] \/ [:K, {1}:])) by Th15

      .= (( card K) +` ( card K)) by Th16

      .= (K +` ( card K))

      .= (K +` K);

    end;

    theorem :: CARD_2:24

    

     Th23: (K *` (M +` N)) = ((K *` M) +` (K *` N))

    proof

      

       A1: ( [:( card [:K, M:]), { 0 }:], [: [:K, M:], { 0 }:]) are_equipotent by Th6;

      (M, [:M, { 0 }:]) are_equipotent by CARD_1: 69;

      then

       A2: ( [:K, M:], [:K, [:M, { 0 }:]:]) are_equipotent by Th7;

      ( [: [:K, M:], { 0 }:], [:K, M:]) are_equipotent by CARD_1: 69;

      then ( [: [:K, M:], { 0 }:], [:K, [:M, { 0 }:]:]) are_equipotent by A2, WELLORD2: 15;

      then

       A3: ( [:( card [:K, M:]), { 0 }:], [:K, [:M, { 0 }:]:]) are_equipotent by A1, WELLORD2: 15;

      

       A4: ( [:( card [:K, N:]), {1}:], [: [:K, N:], {1}:]) are_equipotent by Th6;

       [:M, { 0 }:] misses [:N, {1}:] by Lm4;

      then

       A5: [:K, [:M, { 0 }:]:] misses [:K, [:N, {1}:]:] by ZFMISC_1: 104;

      (N, [:N, {1}:]) are_equipotent by CARD_1: 69;

      then

       A6: ( [:K, N:], [:K, [:N, {1}:]:]) are_equipotent by Th7;

      

       A7: (K *` (M +` N)) = ( card [:K, ( card plus(M,N)):]) by Th9

      .= ( card [:K, plus(M,N):]) by Th6

      .= ( card ( [:K, [:M, { 0 }:]:] \/ [:K, [:N, {1}:]:])) by ZFMISC_1: 97;

      ( [: [:K, N:], {1}:], [:K, N:]) are_equipotent by CARD_1: 69;

      then ( [: [:K, N:], {1}:], [:K, [:N, {1}:]:]) are_equipotent by A6, WELLORD2: 15;

      then

       A8: ( [:( card [:K, N:]), {1}:], [:K, [:N, {1}:]:]) are_equipotent by A4, WELLORD2: 15;

       [:( card [:K, M:]), { 0 }:] misses [:( card [:K, N:]), {1}:] by Lm4;

      then (( [:( card [:K, M:]), { 0 }:] \/ [:( card [:K, N:]), {1}:]),( [:K, [:M, { 0 }:]:] \/ [:K, [:N, {1}:]:])) are_equipotent by A3, A8, A5, CARD_1: 31;

      

      hence (K *` (M +` N)) = ( card ( [:( card [:K, M:]), { 0 }:] \/ [:( card [:K, N:]), {1}:])) by A7, CARD_1: 5

      .= ((K *` M) +` (K *` N)) by Th9;

    end;

    theorem :: CARD_2:25

    ( exp (K, 0 )) = 1

    proof

      

      thus ( exp (K, 0 )) = ( card { {} }) by FUNCT_5: 57

      .= 1 by CARD_1: 30;

    end;

    theorem :: CARD_2:26

    K <> 0 implies ( exp ( 0 ,K)) = 0 ;

    theorem :: CARD_2:27

    ( exp (K,1)) = K & ( exp (1,K)) = 1

    proof

      

      thus ( exp (K,1)) = ( card K) by FUNCT_5: 58, ORDINAL3: 15

      .= K;

      

      thus ( exp (1,K)) = ( card {(K --> {} )}) by FUNCT_5: 59, ORDINAL3: 15

      .= 1 by CARD_1: 30;

    end;

    theorem :: CARD_2:28

    ( exp (K,(M +` N))) = (( exp (K,M)) *` ( exp (K,N)))

    proof

      

       A1: [:M, { 0 }:] misses [:N, {1}:] by ZFMISC_1: 108;

      ( [:M, { 0 }:],M) are_equipotent by CARD_1: 69;

      then

       A2: (( Funcs ( [:M, { 0 }:],K)),( Funcs (M,K))) are_equipotent by FUNCT_5: 60;

      ( [:N, {1}:],N) are_equipotent by CARD_1: 69;

      then

       A3: (( Funcs ( [:N, {1}:],K)),( Funcs (N,K))) are_equipotent by FUNCT_5: 60;

      ((M +` N),( [:M, { 0 }:] \/ [:N, {1}:])) are_equipotent by Th9;

      

      hence ( exp (K,(M +` N))) = ( card ( Funcs (( [:M, { 0 }:] \/ [:N, {1}:]),K))) by FUNCT_5: 60

      .= ( card [:( Funcs ( [:M, { 0 }:],K)), ( Funcs ( [:N, {1}:],K)):]) by A1, FUNCT_5: 62

      .= ( card [:( Funcs (M,K)), ( Funcs (N,K)):]) by A2, A3, Th7

      .= (( exp (K,M)) *` ( exp (K,N))) by Th6;

    end;

    theorem :: CARD_2:29

    ( exp ((K *` M),N)) = (( exp (K,N)) *` ( exp (M,N)))

    proof

      ( card (K *` M)) = (K *` M) & ( card N) = ( card N);

      

      hence ( exp ((K *` M),N)) = ( card ( Funcs (N, [:K, M:]))) by FUNCT_5: 61

      .= ( card [:( Funcs (N,K)), ( Funcs (N,M)):]) by FUNCT_5: 64

      .= (( exp (K,N)) *` ( exp (M,N))) by Th6;

    end;

    theorem :: CARD_2:30

    ( exp (K,(M *` N))) = ( exp (( exp (K,M)),N))

    proof

      

       A1: (( Funcs (M,K)),( card ( Funcs (M,K)))) are_equipotent by CARD_1:def 2;

      ( [:M, N:],(M *` N)) are_equipotent & ( [:N, M:], [:M, N:]) are_equipotent by Lm2, CARD_1:def 2;

      then ( [:N, M:],(M *` N)) are_equipotent by WELLORD2: 15;

      

      hence ( exp (K,(M *` N))) = ( card ( Funcs ( [:N, M:],K))) by FUNCT_5: 60

      .= ( card ( Funcs (N,( Funcs (M,K))))) by FUNCT_5: 63

      .= ( exp (( exp (K,M)),N)) by A1, FUNCT_5: 60;

    end;

    ::$Notion-Name

    theorem :: CARD_2:31

    ( exp (2,( card X))) = ( card ( bool X))

    proof

      ( card ( card X)) = ( card X) & ( card 2) = ( card { {} , 1}) by CARD_1: 50;

      

      hence ( exp (2,( card X))) = ( card ( Funcs (X, { {} , 1}))) by FUNCT_5: 61

      .= ( card ( bool X)) by FUNCT_5: 65;

    end;

    theorem :: CARD_2:32

    ( exp (K,2)) = (K *` K) by CARD_1: 50, FUNCT_5: 66;

    theorem :: CARD_2:33

    ( exp ((K +` M),2)) = (((K *` K) +` ((2 *` K) *` M)) +` (M *` M))

    proof

      

      thus ( exp ((K +` M),2)) = ((K +` M) *` (K +` M)) by CARD_1: 50, FUNCT_5: 66

      .= ((K *` (K +` M)) +` (M *` (K +` M))) by Th23

      .= (((K *` K) +` (K *` M)) +` (M *` (K +` M))) by Th23

      .= (((K *` K) +` (K *` M)) +` ((M *` K) +` (M *` M))) by Th23

      .= ((((K *` K) +` (K *` M)) +` (K *` M)) +` (M *` M)) by Th18

      .= (((K *` K) +` ((K *` M) +` (K *` M))) +` (M *` M)) by Th18

      .= (((K *` K) +` (2 *` (K *` M))) +` (M *` M)) by Th22

      .= (((K *` K) +` ((2 *` K) *` M)) +` (M *` M)) by Th21;

    end;

    theorem :: CARD_2:34

    

     Th33: ( card (X \/ Y)) c= (( card X) +` ( card Y))

    proof

      consider f such that

       A1: ( dom f) = plus(X,Y) & for x be object st x in plus(X,Y) holds (f . x) = g(x) from FUNCT_1:sch 3;

      (X \/ Y) c= ( rng f)

      proof

        let x be object;

        assume x in (X \/ Y);

        then

         A2: x in X or x in Y by XBOOLE_0:def 3;

        per cases ;

          suppose x in X;

          then [x, 0 ] in [:X, { 0 }:] by ZFMISC_1: 106;

          then

           A3: [x, 0 ] in plus(X,Y) by XBOOLE_0:def 3;

          ( [x, 0 ] `1 ) = x;

          then x = (f . [x, 0 ]) by A1, A3;

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

        end;

          suppose not x in X;

          then [x, 1] in [:Y, {1}:] by A2, ZFMISC_1: 106;

          then

           A4: [x, 1] in plus(X,Y) by XBOOLE_0:def 3;

          ( [x, 1] `1 ) = x;

          then x = (f . [x, 1]) by A1, A4;

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

        end;

      end;

      then ( card (X \/ Y)) c= ( card plus(X,Y)) by A1, CARD_1: 12;

      hence thesis by Th16;

    end;

    theorem :: CARD_2:35

    

     Th34: X misses Y implies ( card (X \/ Y)) = (( card X) +` ( card Y))

    proof

      assume

       A1: X misses Y;

      (X, [:X, { 0 }:]) are_equipotent & ( [:X, { 0 }:], [:( card X), { 0 }:]) are_equipotent by CARD_1: 69, Th6;

      then

       A2: (X, [:( card X), { 0 }:]) are_equipotent by WELLORD2: 15;

      (Y, [:Y, {1}:]) are_equipotent & ( [:Y, {1}:], [:( card Y), {1}:]) are_equipotent by CARD_1: 69, Th6;

      then

       A3: (Y, [:( card Y), {1}:]) are_equipotent by WELLORD2: 15;

       [:( card X), { 0 }:] misses [:( card Y), {1}:] by Lm4;

      then ((X \/ Y),( [:( card X), { 0 }:] \/ [:( card Y), {1}:])) are_equipotent by A1, A2, A3, CARD_1: 31;

      

      hence ( card (X \/ Y)) = ( card ( [:( card X), { 0 }:] \/ [:( card Y), {1}:])) by CARD_1: 5

      .= (( card X) +` ( card Y)) by Th9;

    end;

    reserve m,n for Nat;

    theorem :: CARD_2:36

    

     Th35: (n + m) = (n +^ m)

    proof

      defpred P[ Nat] means (n + $1) = (n +^ $1);

      

       A1: for m st P[m] holds P[(m + 1)]

      proof

        let m such that

         A2: P[m];

        

        thus (n + (m + 1)) = ( Segm ((n + m) + 1))

        .= ( succ ( Segm (n + m))) by NAT_1: 38

        .= ( succ (n +^ m)) by A2

        .= (n +^ ( succ ( Segm m))) by ORDINAL2: 28

        .= (n +^ ( Segm (m + 1))) by NAT_1: 38

        .= (n +^ (m + 1));

      end;

      

       A3: P[ 0 ] by ORDINAL2: 27;

      for m holds P[m] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: CARD_2:37

    

     Th36: (n * m) = (n *^ m)

    proof

      defpred P[ Nat] means ($1 * m) = ($1 *^ m);

      

       A1: for n st P[n] holds P[(n + 1)]

      proof

        let n such that

         A2: P[n];

        

        thus ((n + 1) * m) = ((n * m) + (1 * m))

        .= ((n *^ m) +^ m) by A2, Th35

        .= ((n *^ m) +^ (1 *^ m)) by ORDINAL2: 39

        .= ((n +^ 1) *^ m) by ORDINAL3: 46

        .= (( succ ( Segm n)) *^ m) by ORDINAL2: 31

        .= (( Segm (n + 1)) *^ m) by NAT_1: 38

        .= ((n + 1) *^ m);

      end;

      

       A3: P[ 0 ] by ORDINAL2: 35;

      for n holds P[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: CARD_2:38

    

     Th37: ( card (n + m)) = (( card n) +` ( card m)) by Th35;

    theorem :: CARD_2:39

    

     Th38: ( card (n * m)) = (( card n) *` ( card m))

    proof

      

      thus ( card (n * m)) = ( card (n *^ m)) by Th36

      .= (( card n) *` ( card m)) by Th13;

    end;

    theorem :: CARD_2:40

    

     Th39: for X,Y be finite set st X misses Y holds ( card (X \/ Y)) = (( card X) + ( card Y))

    proof

      let X,Y be finite set;

      assume X misses Y;

      

      then ( card ( card (X \/ Y))) = (( card ( card X)) +` ( card ( card Y))) by Th34

      .= ( card (( card X) + ( card Y))) by Th37;

      hence thesis;

    end;

    theorem :: CARD_2:41

    

     Th40: for X be finite set st not x in X holds ( card (X \/ {x})) = (( card X) + 1)

    proof

      let X be finite set;

      

       A1: ( card {x}) = 1 by CARD_1: 30;

      assume not x in X;

      hence thesis by A1, Th39, ZFMISC_1: 50;

    end;

    theorem :: CARD_2:42

    

     Th41: for X be set holds ( card X) = 1 iff ex x be object st X = {x}

    proof

      let X be set;

      ( card { 0 }) = 1 by CARD_1: 30;

      hence ( card X) = 1 implies ex x be object st X = {x} by CARD_1: 29;

      given x be object such that

       A1: X = {x};

      thus thesis by A1, CARD_1: 30;

    end;

    theorem :: CARD_2:43

    

     Th42: for X,Y be finite set holds ( card (X \/ Y)) <= (( card X) + ( card Y))

    proof

      let X,Y be finite set;

      ( card X) = ( card ( card X)) & ( card Y) = ( card ( card Y));

      then (( card X) +` ( card Y)) = ( card (( card X) + ( card Y))) by Th37;

      then ( card ( Segm ( card (X \/ Y)))) = ( card (X \/ Y)) & ( card (X \/ Y)) c= ( card ( Segm (( card X) + ( card Y)))) by Th33;

      hence thesis by NAT_1: 40;

    end;

    theorem :: CARD_2:44

    

     Th43: for X,Y be finite set st Y c= X holds ( card (X \ Y)) = (( card X) - ( card Y))

    proof

      let X,Y be finite set;

      defpred P[ set] means ex S be finite set st S = $1 & ( card (X \ S)) = (( card X) - ( card S));

      (( card X) - 0 ) = ( card X) & (X \ {} ) = X;

      then

       A1: P[ {} ] by CARD_1: 27;

      assume

       A2: Y c= X;

      

       A3: for X1,Z be set st X1 in Y & Z c= Y & P[Z] holds P[(Z \/ {X1})]

      proof

        let X1,Z be set such that

         A4: X1 in Y and

         A5: Z c= Y and

         A6: P[Z] and

         A7: not P[(Z \/ {X1})];

        

         A8: ( card {X1}) = 1 by CARD_1: 30;

         A9:

        now

          assume X1 in Z;

          then {X1} c= Z by ZFMISC_1: 31;

          then Z = (Z \/ {X1}) by XBOOLE_1: 12;

          hence P[(Z \/ {X1})] by A6;

        end;

        then

         A10: X1 in (X \ Z) by A2, A4, A7, XBOOLE_0:def 5;

        then

        consider m be Nat such that

         A11: ( card (X \ Z)) = (m + 1) by NAT_1: 6;

        reconsider Z1 = Z as finite set by A5;

        

         A12: ((X \ Z),( card (X \ Z))) are_equipotent & (X \ (Z \/ {X1})) = ((X \ Z) \ {X1}) by CARD_1:def 2, XBOOLE_1: 41;

        ( card {X1}) = 1 by CARD_1: 30;

        then

         A13: (( card Z1) + ( card {X1})) = ( card (Z1 \/ {X1})) by A7, A9, Th40;

        ( Segm (m + 1)) = ( succ ( Segm m)) by NAT_1: 38;

        then m in (m + 1) & m = ((m + 1) \ {m}) by ORDINAL1: 6, ORDINAL1: 37;

        then ((X \ (Z \/ {X1})),m) are_equipotent by A10, A11, A12, CARD_1: 34;

        then ( card (X \ (Z \/ {X1}))) = (( card X) - ( card (Z1 \/ {X1}))) by A6, A13, A11, A8, CARD_1:def 2;

        hence contradiction by A7;

      end;

      

       A14: Y is finite;

       P[Y] from FINSET_1:sch 2( A14, A1, A3);

      hence thesis;

    end;

    theorem :: CARD_2:45

    for X,Y be finite set holds ( card (X \/ Y)) = ((( card X) + ( card Y)) - ( card (X /\ Y)))

    proof

      let X,Y be finite set;

      (Y \ X) = (Y \ (X /\ Y)) by XBOOLE_1: 47;

      then

       A1: ( card (Y \ X)) = (( card Y) - ( card (X /\ Y))) by Th43, XBOOLE_1: 17;

      ( card (X \/ (Y \ X))) = (( card X) + ( card (Y \ X))) by Th39, XBOOLE_1: 79;

      hence thesis by A1, XBOOLE_1: 39;

    end;

    theorem :: CARD_2:46

    for X,Y be finite set holds ( card [:X, Y:]) = (( card X) * ( card Y))

    proof

      let X,Y be finite set;

      ( card ( card [:X, Y:])) = (( card ( card X)) *` ( card ( card Y))) by Th6

      .= ( card (( card X) * ( card Y))) by Th38;

      hence thesis;

    end;

    theorem :: CARD_2:47

    for f be finite Function holds ( card ( rng f)) <= ( card ( dom f))

    proof

      let f be finite Function;

      ( Segm ( card ( rng f))) c= ( Segm ( card ( dom f))) by CARD_1: 12;

      hence thesis by NAT_1: 39;

    end;

    theorem :: CARD_2:48

    for X,Y be finite set st X c< Y holds ( card X) < ( card Y) & ( card X) in ( Segm ( card Y))

    proof

      let X,Y be finite set;

      assume

       A1: X c< Y;

      then X c= Y;

      then

       A2: Y = (X \/ (Y \ X)) by XBOOLE_1: 45;

      then

       A3: ( card Y) = (( card X) + ( card (Y \ X))) by Th39, XBOOLE_1: 79;

      then

       A4: ( card X) <= ( card Y) by NAT_1: 11;

      now

        assume ( card (Y \ X)) = 0 ;

        then (Y \ X) = {} ;

        hence contradiction by A1, A2;

      end;

      then ( card X) <> ( card Y) by A3;

      hence ( card X) < ( card Y) by A4, XXREAL_0: 1;

      hence thesis by NAT_1: 44;

    end;

    theorem :: CARD_2:49

    (( card X) c= ( card Y) or ( card X) in ( card Y)) & Y is finite implies X is finite

    proof

      assume that

       A1: ( card X) c= ( card Y) or ( card X) in ( card Y) and

       A2: Y is finite;

      ( card X) c= ( card Y) by A1, ORDINAL1:def 2;

      hence thesis by A2;

    end;

    reserve x1,x2,x3,x4,x5,x6,x7,x8 for object;

    theorem :: CARD_2:50

    

     Th49: ( card {x1, x2}) <= 2

    proof

      

       A1: {x1, x2} = ( {x1} \/ {x2}) & (1 + 1) = 2 by ENUMSET1: 1;

      ( card {x1}) = 1 & ( card {x2}) = 1 by CARD_1: 30;

      hence thesis by A1, Th42;

    end;

    theorem :: CARD_2:51

    

     Th50: ( card {x1, x2, x3}) <= 3

    proof

      ( card {x2, x3}) <= 2 by Th49;

      then

       A1: (1 + ( card {x2, x3})) <= (1 + 2) by XREAL_1: 7;

      ( card {x1}) = 1 & {x1, x2, x3} = ( {x1} \/ {x2, x3}) by CARD_1: 30, ENUMSET1: 2;

      then ( card {x1, x2, x3}) <= (1 + ( card {x2, x3})) by Th42;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: CARD_2:52

    

     Th51: ( card {x1, x2, x3, x4}) <= 4

    proof

      ( card {x2, x3, x4}) <= 3 by Th50;

      then

       A1: (1 + ( card {x2, x3, x4})) <= (1 + 3) by XREAL_1: 7;

      ( card {x1}) = 1 & {x1, x2, x3, x4} = ( {x1} \/ {x2, x3, x4}) by CARD_1: 30, ENUMSET1: 4;

      then ( card {x1, x2, x3, x4}) <= (1 + ( card {x2, x3, x4})) by Th42;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: CARD_2:53

    

     Th52: ( card {x1, x2, x3, x4, x5}) <= 5

    proof

      ( card {x2, x3, x4, x5}) <= 4 by Th51;

      then

       A1: (1 + ( card {x2, x3, x4, x5})) <= (1 + 4) by XREAL_1: 7;

      ( card {x1}) = 1 & {x1, x2, x3, x4, x5} = ( {x1} \/ {x2, x3, x4, x5}) by CARD_1: 30, ENUMSET1: 7;

      then ( card {x1, x2, x3, x4, x5}) <= (1 + ( card {x2, x3, x4, x5})) by Th42;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: CARD_2:54

    

     Th53: ( card {x1, x2, x3, x4, x5, x6}) <= 6

    proof

      ( card {x2, x3, x4, x5, x6}) <= 5 by Th52;

      then

       A1: (1 + ( card {x2, x3, x4, x5, x6})) <= (1 + 5) by XREAL_1: 7;

      ( card {x1}) = 1 & {x1, x2, x3, x4, x5, x6} = ( {x1} \/ {x2, x3, x4, x5, x6}) by CARD_1: 30, ENUMSET1: 11;

      then ( card {x1, x2, x3, x4, x5, x6}) <= (1 + ( card {x2, x3, x4, x5, x6})) by Th42;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: CARD_2:55

    

     Th54: ( card {x1, x2, x3, x4, x5, x6, x7}) <= 7

    proof

      ( card {x2, x3, x4, x5, x6, x7}) <= 6 by Th53;

      then

       A1: (1 + ( card {x2, x3, x4, x5, x6, x7})) <= (1 + 6) by XREAL_1: 7;

      ( card {x1}) = 1 & {x1, x2, x3, x4, x5, x6, x7} = ( {x1} \/ {x2, x3, x4, x5, x6, x7}) by CARD_1: 30, ENUMSET1: 16;

      then ( card {x1, x2, x3, x4, x5, x6, x7}) <= (1 + ( card {x2, x3, x4, x5, x6, x7})) by Th42;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: CARD_2:56

    ( card {x1, x2, x3, x4, x5, x6, x7, x8}) <= 8

    proof

      ( card {x2, x3, x4, x5, x6, x7, x8}) <= 7 by Th54;

      then

       A1: (1 + ( card {x2, x3, x4, x5, x6, x7, x8})) <= (1 + 7) by XREAL_1: 7;

       {x1, x2, x3, x4, x5, x6, x7, x8} = ( {x1} \/ {x2, x3, x4, x5, x6, x7, x8}) & ( card {x1}) = 1 by CARD_1: 30, ENUMSET1: 22;

      then ( card {x1, x2, x3, x4, x5, x6, x7, x8}) <= (1 + ( card {x2, x3, x4, x5, x6, x7, x8})) by Th42;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: CARD_2:57

    

     Th56: x1 <> x2 implies ( card {x1, x2}) = 2

    proof

      

       A1: ( card {x1}) = 1 & ( card {x2}) = 1 by CARD_1: 30;

      

       A2: {x1, x2} = ( {x1} \/ {x2}) & (1 + 1) = 2 by ENUMSET1: 1;

      assume x1 <> x2;

      hence thesis by A1, A2, Th39, ZFMISC_1: 11;

    end;

    theorem :: CARD_2:58

    

     Th57: x1 <> x2 & x1 <> x3 & x2 <> x3 implies ( card {x1, x2, x3}) = 3

    proof

      assume x1 <> x2 & x1 <> x3 & x2 <> x3;

      then

       A1: ( card {x1, x2}) = 2 & not x3 in {x1, x2} by Th56, TARSKI:def 2;

       {x1, x2, x3} = ( {x1, x2} \/ {x3}) by ENUMSET1: 3;

      

      hence ( card {x1, x2, x3}) = (2 + 1) by A1, Th40

      .= 3;

    end;

    theorem :: CARD_2:59

    

     Th58: x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 implies ( card {x1, x2, x3, x4}) = 4

    proof

      assume x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4;

      then

       A1: ( card {x1, x2, x3}) = 3 & not x4 in {x1, x2, x3} by Th57, ENUMSET1:def 1;

       {x1, x2, x3, x4} = ( {x1, x2, x3} \/ {x4}) by ENUMSET1: 6;

      

      hence ( card {x1, x2, x3, x4}) = (3 + 1) by A1, Th40

      .= 4;

    end;

    begin

    theorem :: CARD_2:60

    for X be set st ( card X) = 2 holds ex x,y be object st x <> y & X = {x, y}

    proof

      let X be set;

      assume

       A1: ( card X) = 2;

      then

      consider x be object such that

       A2: x in X by CARD_1: 27, XBOOLE_0:def 1;

      X is finite by A1;

      then

      reconsider Y = X as finite set;

       {x} c= X by A2, ZFMISC_1: 31;

      

      then ( card (X \ {x})) = (( card Y) - ( card {x})) by Th43

      .= (2 - 1) by A1, CARD_1: 30;

      then

      consider y be object such that

       A3: (X \ {x}) = {y} by Th41;

      take x, y;

      x in {x} by TARSKI:def 1;

      hence x <> y by A3, XBOOLE_0:def 5;

      thus X c= {x, y}

      proof

        let z be object;

        assume

         A4: z in X;

        per cases ;

          suppose z = x;

          hence thesis by TARSKI:def 2;

        end;

          suppose z <> x;

          then not z in {x} by TARSKI:def 1;

          then z in {y} by A3, A4, XBOOLE_0:def 5;

          then z = y by TARSKI:def 1;

          hence thesis by TARSKI:def 2;

        end;

      end;

      let z be object;

      assume z in {x, y};

      then

       A5: z = x or z = y by TARSKI:def 2;

      y in (X \ {x}) by A3, TARSKI:def 1;

      hence thesis by A2, A5;

    end;

    theorem :: CARD_2:61

    for f be Function holds ( card ( rng f)) c= ( card ( dom f))

    proof

      let f be Function;

      ( rng f) = (f .: ( dom f)) by RELAT_1: 113;

      hence thesis by CARD_1: 66;

    end;

     Lm5:

    now

      let n;

      assume

       A1: for Z be finite set holds ( card Z) = n & Z <> {} & (for X, Y st X in Z & Y in Z holds X c= Y or Y c= X) implies ( union Z) in Z;

      let Z be finite set;

      assume that

       A2: ( card Z) = (n + 1) and

       A3: Z <> {} and

       A4: for X, Y st X in Z & Y in Z holds X c= Y or Y c= X;

      set y = the Element of Z;

      per cases ;

        suppose n = 0 ;

        then

        consider x be object such that

         A5: Z = {x} by A2, Th41;

        thus ( union Z) in Z by A5, TARSKI:def 1;

      end;

        suppose

         A6: n <> 0 ;

        set Y = (Z \ {y});

        reconsider Y as finite set;

         {y} c= Z by A3, ZFMISC_1: 31;

        

        then

         A7: ( card Y) = ((n + 1) - ( card {y})) by A2, Th43

        .= ((n + 1) - 1) by CARD_1: 30

        .= n;

        for a,b be set st a in Y & b in Y holds a c= b or b c= a by A4;

        then

         A8: ( union Y) in Y by A1, A6, A7, CARD_1: 27;

        then

         A9: ( union Y) in Z;

        Z = ((Z \ {y}) \/ {y})

        proof

          thus Z c= ((Z \ {y}) \/ {y})

          proof

            let x be object;

            assume x in Z;

            then x in (Z \ {y}) or x in {y} by XBOOLE_0:def 5;

            hence thesis by XBOOLE_0:def 3;

          end;

          let x be object;

          assume x in ((Z \ {y}) \/ {y});

          then

           A10: x in (Z \ {y}) or x in {y} by XBOOLE_0:def 3;

           {y} c= Z by A3, ZFMISC_1: 31;

          hence thesis by A10;

        end;

        

        then

         A11: ( union Z) = (( union Y) \/ ( union {y})) by ZFMISC_1: 78

        .= (( union Y) \/ y);

        

         A12: y in Z by A3;

        y c= ( union Y) or ( union Y) c= y by A4, A8;

        hence ( union Z) in Z by A9, A12, A11, XBOOLE_1: 12;

      end;

    end;

    

     Lm6: for Z be finite set holds Z <> {} & (for X, Y st X in Z & Y in Z holds X c= Y or Y c= X) implies ( union Z) in Z

    proof

      defpred P[ Nat] means for Z be finite set st ( card Z) = $1 & Z <> {} & (for X, Y st X in Z & Y in Z holds X c= Y or Y c= X) holds ( union Z) in Z;

      let Z be finite set;

      

       A1: ( card Z) = ( card Z);

      

       A2: P[ 0 ];

      

       A3: for k be Nat st P[k] holds P[(k + 1)] by Lm5;

      for n holds P[n] from NAT_1:sch 2( A2, A3);

      hence thesis by A1;

    end;

    theorem :: CARD_2:62

    Z <> {} & Z is finite & (for X, Y st X in Z & Y in Z holds X c= Y or Y c= X) implies ( union Z) in Z by Lm6;

    theorem :: CARD_2:63

    (x1,x2,x3,x4,x5) are_mutually_distinct implies ( card {x1, x2, x3, x4, x5}) = 5

    proof

      

       A1: {x1, x2, x3, x4, x5} = ( {x1, x2, x3, x4} \/ {x5}) by ENUMSET1: 10;

      assume

       A2: (x1,x2,x3,x4,x5) are_mutually_distinct ;

      then

       A3: x3 <> x5 & x4 <> x5 by ZFMISC_1:def 7;

      

       A4: x2 <> x4 & x3 <> x4 by A2, ZFMISC_1:def 7;

      

       A5: x1 <> x4 & x2 <> x3 by A2, ZFMISC_1:def 7;

      x1 <> x5 & x2 <> x5 by A2, ZFMISC_1:def 7;

      then

       A6: not x5 in {x1, x2, x3, x4} by A3, ENUMSET1:def 2;

      x1 <> x2 & x1 <> x3 by A2, ZFMISC_1:def 7;

      then ( card {x1, x2, x3, x4}) = 4 by A5, A4, Th58;

      

      hence ( card {x1, x2, x3, x4, x5}) = (4 + 1) by A6, A1, Th40

      .= 5;

    end;

    theorem :: CARD_2:64

    for M1,M2 be set st ( card M1) = 0 & ( card M2) = 0 holds M1 = M2

    proof

      let M1,M2 be set;

      assume that

       A1: ( card M1) = 0 and

       A2: ( card M2) = 0 ;

      M1 = {} by A1;

      hence thesis by A2;

    end;

    registration

      let x, y;

      cluster [x, y] -> non natural;

      coherence

      proof

        assume [x, y] is natural;

        then

        reconsider n = [x, y] as Nat;

        ( card n) <= 2 by Th49;

        then n <= 2;

        then n = 0 or ... or n = 2;

        per cases ;

          suppose n = 0 ;

          hence contradiction;

        end;

          suppose n = 1;

          hence contradiction by CARD_1: 49, ZFMISC_1: 4;

        end;

          suppose n = 2;

          hence contradiction by CARD_1: 50, ZFMISC_1: 6;

        end;

      end;

    end

    begin

    reserve A,B,C for Ordinal,

K,L,M,N for Cardinal,

x,y,y1,y2,z,u for object,

X,Y,Z,Z1,Z2 for set,

n for Nat,

f,f1,g,h for Function,

Q,R for Relation;

    theorem :: CARD_2:65

    ( Sum (M --> N)) = (M *` N)

    proof

      

      thus ( Sum (M --> N)) = ( card [:N, M:]) by CARD_3: 25

      .= (M *` N) by Lm2;

    end;

    theorem :: CARD_2:66

    ( Product (N --> M)) = ( exp (M,N)) by CARD_3: 11;

    scheme :: CARD_2:sch1

    FinRegularity { X() -> finite set , P[ object, object] } :

ex x st x in X() & for y st y in X() & y <> x holds not P[y, x]

      provided

       A1: X() <> {}

       and

       A2: for x, y st P[x, y] & P[y, x] holds x = y

       and

       A3: for x, y, z st P[x, y] & P[y, z] holds P[x, z];

      defpred Q[ Nat] means for X be finite set st ( card X) = $1 & X <> {} holds ex x st x in X & for y st y in X & y <> x holds not P[y, x];

      

       A4: Q[ 0 ];

      

       A5: Q[n] implies Q[(n + 1)]

      proof

        assume

         A6: for X be finite set st ( card X) = n & X <> {} holds ex x st x in X & for y st y in X & y <> x holds not P[y, x];

        let X be finite set;

        assume that

         A7: ( card X) = (n + 1) and

         A8: X <> {} ;

        set x = the Element of X;

         A9:

        now

          assume (X \ {x}) = {} ;

          then

           A10: X c= {x} by XBOOLE_1: 37;

          thus thesis

          proof

            take x;

            thus x in X by A8;

            thus thesis by A10, TARSKI:def 1;

          end;

        end;

        now

          assume

           A11: (X \ {x}) <> {} ;

           {x} c= X by A8, ZFMISC_1: 31;

          then

           A12: ( card (X \ {x})) = ((n + 1) - ( card {x})) by A7, Th43;

          ( card {x}) = 1 by CARD_1: 30;

          then

          consider y such that

           A13: y in (X \ {x}) and

           A14: for z st z in (X \ {x}) & z <> y holds not P[z, y] by A6, A11, A12;

           A15:

          now

            assume

             A16: P[x, y];

            thus thesis

            proof

              take x;

              thus x in X by A8;

              let z;

              assume that

               A17: z in X and

               A18: z <> x and

               A19: P[z, x];

               not z in {x} by A18, TARSKI:def 1;

              then

               A20: z in (X \ {x}) by A17, XBOOLE_0:def 5;

              

               A21: not y in {x} by A13, XBOOLE_0:def 5;

              

               A22: z = y by A3, A14, A16, A19, A20;

              y <> x by A21, TARSKI:def 1;

              hence contradiction by A2, A16, A19, A22;

            end;

          end;

          now

            assume

             A23: not P[x, y];

            thus thesis

            proof

              take y;

              thus y in X by A13;

              let z such that

               A24: z in X and

               A25: z <> y;

              z in {x} or not z in {x};

              then z = x or z in (X \ {x}) by A24, TARSKI:def 1, XBOOLE_0:def 5;

              hence thesis by A14, A23, A25;

            end;

          end;

          hence thesis by A15;

        end;

        hence thesis by A9;

      end;

      

       A26: Q[n] from NAT_1:sch 2( A4, A5);

      ( card X()) = ( card X());

      hence thesis by A1, A26;

    end;

    scheme :: CARD_2:sch2

    MaxFinSetElem { X() -> finite set , P[ object, object] } :

ex x st x in X() & for y st y in X() holds P[x, y]

      provided

       A1: X() <> {}

       and

       A2: for x, y holds P[x, y] or P[y, x]

       and

       A3: for x, y, z st P[x, y] & P[y, z] holds P[x, z];

      defpred Q[ Nat] means for X be finite set st ( card X) = $1 & X <> {} holds ex x st x in X & for y st y in X holds P[x, y];

      

       A4: Q[ 0 ];

      

       A5: Q[n] implies Q[(n + 1)]

      proof

        assume

         A6: for X be finite set st ( card X) = n & X <> {} holds ex x st x in X & for y st y in X holds P[x, y];

        let X be finite set;

        assume that

         A7: ( card X) = (n + 1) and

         A8: X <> {} ;

        set x = the Element of X;

         A9:

        now

          assume (X \ {x}) = {} ;

          then

           A10: X c= {x} by XBOOLE_1: 37;

          thus thesis

          proof

            take x;

            thus x in X by A8;

            let y;

            assume y in X;

            then y = x by A10, TARSKI:def 1;

            hence thesis by A2;

          end;

        end;

        now

          assume

           A11: (X \ {x}) <> {} ;

           {x} c= X by A8, ZFMISC_1: 31;

          then

           A12: ( card (X \ {x})) = ((n + 1) - ( card {x})) by A7, Th43;

          ( card {x}) = 1 by CARD_1: 30;

          then

          consider y such that

           A13: y in (X \ {x}) and

           A14: for z st z in (X \ {x}) holds P[y, z] by A6, A11, A12;

          

           A15: P[x, y] or P[y, x] by A2;

          

           A16: P[x, x] by A2;

          P[y, y] by A2;

          then

          consider z such that

           A17: z = x or z = y and

           A18: P[z, x] and

           A19: P[z, y] by A15, A16;

          thus thesis

          proof

            take z;

            thus z in X by A13, A17;

            let u;

            

             A20: u in {x} or not u in {x};

            assume u in X;

            then u = x or u in (X \ {x}) by A20, TARSKI:def 1, XBOOLE_0:def 5;

            then P[z, u] or P[y, u] by A14, A18;

            hence thesis by A3, A19;

          end;

        end;

        hence thesis by A9;

      end;

      

       A21: Q[n] from NAT_1:sch 2( A4, A5);

      ( card X()) = ( card X());

      hence thesis by A1, A21;

    end;

    

     Lm7: ( Rank n) is finite implies ( Rank (n + 1)) is finite

    proof

      ( Segm (n + 1)) = ( succ ( Segm n)) by NAT_1: 38;

      then ( Rank (n + 1)) = ( bool ( Rank n)) by CLASSES1: 30;

      hence thesis;

    end;

    

     Lm8: 1 = ( card 1);

    theorem :: CARD_2:67

    ( Rank n) is finite

    proof

      defpred P[ Nat] means ( Rank $1) is finite;

      

       A1: P[ 0 ] by CLASSES1: 29;

      

       A2: for n st P[n] holds P[(n + 1)] by Lm7;

      for n holds P[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: CARD_2:68

     0 in M iff 1 c= M

    proof

      ( 0 + 1) = 1;

      then ( nextcard ( card ( Segm 0 ))) = ( card ( Segm 1)) by NAT_1: 42;

      hence thesis by CARD_3: 90;

    end;

    theorem :: CARD_2:69

    1 in M iff 2 c= M

    proof

      (1 + 1) = 2;

      then ( nextcard ( card ( Segm 1))) = ( card ( Segm 2)) by NAT_1: 42;

      hence thesis by CARD_3: 90;

    end;

    reserve n,k for Nat;

    theorem :: CARD_2:70

    

     Th69: A is limit_ordinal iff for B, n st B in A holds (B +^ n) in A

    proof

      thus A is limit_ordinal implies for B, n st B in A holds (B +^ n) in A

      proof

        assume

         A1: A is limit_ordinal;

        let B, n;

        defpred P[ Nat] means (B +^ $1) in A;

        assume B in A;

        then

         A2: P[ 0 ] by ORDINAL2: 27;

        

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

        proof

          ( Segm (k + 1)) = ( succ ( Segm k)) by NAT_1: 38;

          then (B +^ (k + 1)) = ( succ (B +^ k)) by ORDINAL2: 28;

          hence thesis by A1, ORDINAL1: 28;

        end;

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

        hence thesis;

      end;

      assume

       A4: for B, n st B in A holds (B +^ n) in A;

      now

        let B;

        assume B in A;

        then (B +^ 1) in A by A4;

        hence ( succ B) in A by ORDINAL2: 31;

      end;

      hence thesis by ORDINAL1: 28;

    end;

    theorem :: CARD_2:71

    

     Th70: (A +^ ( succ n)) = (( succ A) +^ n) & (A +^ (n + 1)) = (( succ A) +^ n)

    proof

      defpred P[ Nat] means (A +^ ( succ $1)) = (( succ A) +^ $1);

      (A +^ ( succ 0 )) = ( succ A) by ORDINAL2: 31

      .= (( succ A) +^ 0 ) by ORDINAL2: 27;

      then

       A1: P[ 0 ];

      

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

      proof

        assume

         A3: P[k];

        

         A4: ( Segm (k + 1)) = ( succ ( Segm k)) by NAT_1: 38;

        

        hence (A +^ ( succ (k + 1))) = ( succ (( succ A) +^ k)) by A3, ORDINAL2: 28

        .= ((( succ A) +^ k) +^ 1) by ORDINAL2: 31

        .= (( succ A) +^ (k +^ 1)) by ORDINAL3: 30

        .= (( succ A) +^ (k + 1)) by A4, ORDINAL2: 31;

      end;

      

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

      thus

       A6: (A +^ ( succ n)) = (( succ A) +^ n) by A5;

      ( Segm (n + 1)) = ( succ ( Segm n)) by NAT_1: 38;

      hence thesis by A6;

    end;

    theorem :: CARD_2:72

    

     Th71: ex n st (A *^ ( succ 1)) = (A +^ n)

    proof

      defpred P[ Ordinal] means ex n st ($1 *^ 2) = ($1 +^ n);

      ( {} +^ {} ) = {} by ORDINAL2: 27;

      then

       A1: P[ 0 ] by ORDINAL2: 35;

      

       A2: for A st P[A] holds P[( succ A)]

      proof

        let A;

        given n such that

         A3: (A *^ 2) = (A +^ n);

        take (n + 1);

        (( succ A) *^ 2) = ((A *^ 2) +^ 2) by ORDINAL2: 36

        .= ( succ ((A *^ ( succ 1)) +^ 1)) by ORDINAL2: 28

        .= ( succ ( succ (A +^ n))) by A3, ORDINAL2: 31

        .= ( succ (A +^ ( succ ( Segm n)))) by ORDINAL2: 28

        .= ( succ (A +^ ( Segm (n + 1)))) by NAT_1: 38

        .= (A +^ ( succ (n + 1))) by ORDINAL2: 28;

        hence thesis by Th70;

      end;

      

       A4: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds P[A]

      proof

        let A;

        assume that

         A5: A <> 0 and

         A6: A is limit_ordinal and

         A7: for B st B in A holds P[B];

        take 0 ;

        deffunc f( Ordinal) = ($1 *^ 2);

        consider phi be Ordinal-Sequence such that

         A8: ( dom phi) = A and

         A9: for B st B in A holds (phi . B) = f(B) from ORDINAL2:sch 3;

        

         A10: (A *^ 2) = ( union ( sup phi)) by A5, A6, A8, A9, ORDINAL2: 37

        .= ( union ( sup ( rng phi))) by ORDINAL2: 26;

        thus (A *^ 2) c= (A +^ 0 )

        proof

          let B;

          assume B in (A *^ 2);

          then

          consider X such that

           A11: B in X and

           A12: X in ( sup ( rng phi)) by A10, TARSKI:def 4;

          reconsider X as Ordinal by A12;

          consider C be Ordinal such that

           A13: C in ( rng phi) and

           A14: X c= C by A12, ORDINAL2: 21;

          consider x be object such that

           A15: x in ( dom phi) and

           A16: C = (phi . x) by A13, FUNCT_1:def 3;

          reconsider x as Ordinal by A15;

          

           A17: ex n st (x *^ 2) = (x +^ n) by A7, A8, A15;

          C = (x *^ 2) by A8, A9, A15, A16;

          then

           A18: C in A by A6, A8, A15, A17, Th69;

          (A +^ {} ) = A by ORDINAL2: 27;

          hence thesis by A11, A14, A18, ORDINAL1: 10;

        end;

        

         A19: 1 in ( succ 1) by ORDINAL1: 6;

        

         A20: (A +^ 0 ) = A by ORDINAL2: 27;

        

         A21: A = (A *^ 1) by ORDINAL2: 39;

        1 c= 2 by A19, ORDINAL1:def 2;

        hence thesis by A20, A21, ORDINAL2: 42;

      end;

      for A holds P[A] from ORDINAL2:sch 1( A1, A2, A4);

      hence thesis;

    end;

    theorem :: CARD_2:73

    

     Th72: A is limit_ordinal implies (A *^ ( succ 1)) = A

    proof

      consider n such that

       A1: (A *^ 2) = (A +^ n) by Th71;

      assume A is limit_ordinal;

      then

       A2: (A +^ n) is limit_ordinal by A1, ORDINAL3: 40;

      now

        assume n <> 0 ;

        then

        consider k be Nat such that

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

        reconsider k as Element of NAT by ORDINAL1:def 12;

        ( Segm n) = ( succ ( Segm k)) by A3, NAT_1: 38;

        then (A +^ n) = ( succ (A +^ k)) by ORDINAL2: 28;

        hence contradiction by A2, ORDINAL1: 29;

      end;

      hence thesis by A1, ORDINAL2: 27;

    end;

    

     Lm9: omega is limit_ordinal by ORDINAL1:def 11;

    theorem :: CARD_2:74

    

     Th73: omega c= A implies (1 +^ A) = A

    proof

      deffunc f( Ordinal) = (1 +^ $1);

      consider phi be Ordinal-Sequence such that

       A1: ( dom phi) = omega & for B st B in omega holds (phi . B) = f(B) from ORDINAL2:sch 3;

      

       A2: (1 +^ omega ) = ( sup phi) by A1, Lm9, ORDINAL2: 29

      .= ( sup ( rng phi)) by ORDINAL2: 26;

      

       A3: (1 +^ omega ) c= omega

      proof

        let B;

        assume B in (1 +^ omega );

        then

        consider C be Ordinal such that

         A4: C in ( rng phi) and

         A5: B c= C by A2, ORDINAL2: 21;

        consider x be object such that

         A6: x in ( dom phi) and

         A7: C = (phi . x) by A4, FUNCT_1:def 3;

        reconsider x as Ordinal by A6;

        reconsider x9 = x as Cardinal by A1, A6;

        reconsider x as finite Ordinal by A1, A6;

        

         A8: C = (1 +^ x) by A1, A6, A7;

        ( succ x) in omega by A1, A6, Lm9, ORDINAL1: 28;

        then C in omega by A8, ORDINAL2: 31;

        hence thesis by A5, ORDINAL1: 12;

      end;

      assume omega c= A;

      then

       A9: ex B st A = ( omega +^ B) by ORDINAL3: 27;

       omega c= (1 +^ omega ) by ORDINAL3: 24;

      then omega = (1 +^ omega ) by A3;

      hence thesis by A9, ORDINAL3: 30;

    end;

    registration

      cluster infinite -> limit_ordinal for Cardinal;

      coherence

      proof

        let M be Cardinal;

        assume M is infinite;

        then

         A1: not M in omega ;

        assume not thesis;

        then

        consider A such that

         A2: M = ( succ A) by ORDINAL1: 29;

         omega = ( succ A) or omega in ( succ A) by A1, A2, CARD_1: 4;

        then

         A3: omega c= A by Lm9, ORDINAL1: 22, ORDINAL1: 29;

        ( card (A +^ 1)) = (( card 1) +` ( card A)) by Th12

        .= ( card (1 +^ A)) by Th12

        .= ( card A) by A3, Th73;

        then ( card ( succ A)) = ( card A) by ORDINAL2: 31;

        then

         A4: (A,( succ A)) are_equipotent by CARD_1: 5;

        

         A5: not ( succ A) c= A by ORDINAL1: 5, ORDINAL1: 6;

        ex B st ( succ A) = B & for A st (A,B) are_equipotent holds B c= A by A2, CARD_1:def 1;

        hence contradiction by A4, A5;

      end;

    end

    theorem :: CARD_2:75

    

     Th74: not M is finite implies (M +` M) = M

    proof

      assume not M is finite;

      then (M *^ ( succ 1)) = M by Th72;

      

      then ( card M) = (( card 2) *` ( card M)) by Th13

      .= ( card (( succ 1) *^ M)) by Th13

      .= ( card ((1 *^ M) +^ M)) by ORDINAL2: 36

      .= (M +` M) by ORDINAL2: 39;

      hence thesis;

    end;

    theorem :: CARD_2:76

    

     Th75: not M is finite & (N c= M or N in M) implies (M +` N) = M & (N +` M) = M

    proof

      assume that

       A1: not M is finite and

       A2: N c= M or N in M;

      

       A3: (M +` M) = M by A1, Th74;

      N c= M by A2, CARD_1: 3;

      then

       A4: (M +^ N) c= (M +^ M) by ORDINAL2: 33;

      

       A5: M c= (M +^ N) by ORDINAL3: 24;

      

       A6: ( card M) = M;

      

       A7: (M +` N) c= M by A3, A4, CARD_1: 11;

      M c= (M +` N) by A5, A6, CARD_1: 11;

      hence thesis by A7;

    end;

    theorem :: CARD_2:77

     not X is finite & ((X,Y) are_equipotent or (Y,X) are_equipotent ) implies ((X \/ Y),X) are_equipotent & ( card (X \/ Y)) = ( card X)

    proof

      assume that

       A1: not X is finite and

       A2: (X,Y) are_equipotent or (Y,X) are_equipotent ;

      

       A3: ( card X) = ( card Y) by A2, CARD_1: 5;

      

       A4: ( card X) c= ( card (X \/ Y)) by CARD_1: 11, XBOOLE_1: 7;

      

       A5: ( card (X \/ Y)) c= (( card X) +` ( card Y)) by Th33;

      (( card X) +` ( card Y)) = ( card X) by A1, A3, Th74;

      then ( card X) = ( card (X \/ Y)) by A4, A5;

      hence thesis by CARD_1: 5;

    end;

    theorem :: CARD_2:78

     not X is finite & Y is finite implies ((X \/ Y),X) are_equipotent & ( card (X \/ Y)) = ( card X)

    proof

      assume that

       A1: not X is finite and

       A2: Y is finite;

      ( card Y) in ( card X) by A1, A2, CARD_3: 86;

      then

       A3: (( card X) +` ( card Y)) = ( card X) by A1, Th75;

      

       A4: ( card (X \/ Y)) c= (( card X) +` ( card Y)) by Th33;

      ( card X) c= ( card (X \/ Y)) by CARD_1: 11, XBOOLE_1: 7;

      then ( card X) = ( card (X \/ Y)) by A3, A4;

      hence thesis by CARD_1: 5;

    end;

    theorem :: CARD_2:79

     not X is finite & (( card Y) in ( card X) or ( card Y) c= ( card X)) implies ((X \/ Y),X) are_equipotent & ( card (X \/ Y)) = ( card X)

    proof

      assume that

       A1: not X is finite and

       A2: ( card Y) in ( card X) or ( card Y) c= ( card X);

      

       A3: (( card X) +` ( card Y)) = ( card X) by A1, A2, Th75;

      

       A4: ( card (X \/ Y)) c= (( card X) +` ( card Y)) by Th33;

      ( card X) c= ( card (X \/ Y)) by CARD_1: 11, XBOOLE_1: 7;

      then ( card X) = ( card (X \/ Y)) by A3, A4;

      hence thesis by CARD_1: 5;

    end;

    registration

      let M,N be finite Cardinal;

      cluster (M +` N) -> finite;

      coherence

      proof

        (M +` N) = ( card (( card M) + ( card N))) by Th37;

        hence thesis;

      end;

    end

    theorem :: CARD_2:80

    for M,N be finite Cardinal holds (M +` N) is finite;

    theorem :: CARD_2:81

     not M is finite implies not (M +` N) is finite & not (N +` M) is finite

    proof

      assume

       A1: not M is finite;

      M c= N or N c= M;

      then M c= N & not N is finite or (M +` N) = M & (N +` M) = M by A1, Th75;

      hence thesis by A1, Th75;

    end;

    theorem :: CARD_2:82

    for M,N be finite Cardinal holds (M *` N) is finite;

    theorem :: CARD_2:83

    

     Th82: K in L & M in N or K c= L & M in N or K in L & M c= N or K c= L & M c= N implies (K +` M) c= (L +` N) & (M +` K) c= (L +` N)

    proof

      assume that

       A1: K in L & M in N or K c= L & M in N or K in L & M c= N or K c= L & M c= N;

      

       A2: K c= L by A1, CARD_1: 3;

      

       A3: M c= N by A1, CARD_1: 3;

      

       A4: (K +` M) = ( card (K +^ M));

      

       A5: (K +^ M) c= (L +^ N) by A2, A3, ORDINAL3: 18;

      hence (K +` M) c= (L +` N) by CARD_1: 11;

      thus thesis by A4, A5, CARD_1: 11;

    end;

    theorem :: CARD_2:84

    M in N or M c= N implies (K +` M) c= (K +` N) & (K +` M) c= (N +` K) & (M +` K) c= (K +` N) & (M +` K) c= (N +` K) by Th82;

    theorem :: CARD_2:85

    

     Th84: X is countable & Y is countable implies (X \/ Y) is countable

    proof

      assume that

       A1: ( card X) c= omega and

       A2: ( card Y) c= omega ;

      

       A3: ( card (X \/ Y)) c= (( card X) +` ( card Y)) by Th33;

      

       A4: ( omega +` omega ) = omega by Th74;

      (( card X) +` ( card Y)) c= ( omega +` omega ) by A1, A2, Th82;

      hence ( card (X \/ Y)) c= omega by A3, A4;

    end;

    theorem :: CARD_2:86

    

     Th85: (( card ( dom f)) c= M & for x st x in ( dom f) holds ( card (f . x)) c= N) implies ( card ( Union f)) c= (M *` N)

    proof

      assume that

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

       A2: for x st x in ( dom f) holds ( card (f . x)) c= N;

      

       A3: ( card ( Union f)) c= ( Sum ( Card f)) by CARD_3: 39;

      

       A4: ( dom ( Card f)) = ( dom f) by CARD_3:def 2;

      

       A5: ( dom (( dom f) --> N)) = ( dom f) by FUNCOP_1: 13;

      now

        let x be object;

        assume

         A6: x in ( dom ( Card f));

        then

         A7: (( Card f) . x) = ( card (f . x)) by A4, CARD_3:def 2;

        ((( dom f) --> N) . x) = N by A4, A6, FUNCOP_1: 7;

        hence (( Card f) . x) c= ((( dom f) --> N) . x) by A2, A4, A6, A7;

      end;

      then ( Sum ( Card f)) c= ( Sum (( dom f) --> N)) by A4, A5, CARD_3: 30;

      then

       A8: ( card ( Union f)) c= ( Sum (( dom f) --> N)) by A3;

      

       A9: [:( card ( dom f)), N:] c= [:M, N:] by A1, ZFMISC_1: 95;

      ( Sum (( dom f) --> N)) = ( card [:N, ( dom f):]) by CARD_3: 25

      .= ( card [:N, ( card ( dom f)):]) by Th6

      .= ( card [:( card ( dom f)), N:]) by Th4;

      then

       A10: ( Sum (( dom f) --> N)) c= ( card [:M, N:]) by A9, CARD_1: 11;

      thus thesis by A8, A10;

    end;

    theorem :: CARD_2:87

    (( card X) c= M & for Y st Y in X holds ( card Y) c= N) implies ( card ( union X)) c= (M *` N)

    proof

      assume that

       A1: ( card X) c= M and

       A2: for Y st Y in X holds ( card Y) c= N;

      now

        let x;

        assume x in ( dom ( id X));

        then (( id X) . x) in X by FUNCT_1: 18;

        hence ( card (( id X) . x)) c= N by A2;

      end;

      then ( card ( Union ( id X))) c= (M *` N) by A1, Th85;

      hence thesis;

    end;

    theorem :: CARD_2:88

    

     Th87: for f st ( dom f) is finite & for x st x in ( dom f) holds (f . x) is finite holds ( Union f) is finite

    proof

      let f;

      assume that

       A1: ( dom f) is finite and

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

      reconsider df = ( dom f) as finite set by A1;

      now

        assume ( dom f) <> {} ;

        then

         A3: df <> {} ;

        defpred P[ object, object] means ( card (f . $2)) c= ( card (f . $1));

        

         A4: for x, y holds P[x, y] or P[y, x];

        

         A5: for x,y,z be object st P[x, y] & P[y, z] holds P[x, z] by XBOOLE_1: 1;

        consider x such that

         A6: x in df & for y st y in df holds P[x, y] from MaxFinSetElem( A3, A4, A5);

        reconsider fx = (f . x) as finite set by A2, A6;

        

         A7: ( card ( Union f)) c= (( card ( card df)) *` ( card (f . x))) by A6, Th85;

        ( card (f . x)) = ( card ( card fx));

        then ( card ( Union f)) c= ( card (( card df) * ( card fx))) by A7, Th38;

        hence thesis;

      end;

      hence thesis by RELAT_1: 42, ZFMISC_1: 2;

    end;

    theorem :: CARD_2:89

    ( omega *` ( card n)) c= omega & (( card n) *` omega ) c= omega

    proof

      defpred P[ Nat] means ( omega *` ( card $1)) c= omega ;

      

       A1: P[ 0 ];

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        ( card (k + 1)) = ( Segm (k + 1))

        .= ( succ ( Segm k)) by NAT_1: 38;

        then ( card (k + 1)) = ( card ( succ k));

        

        then ( omega *` ( card (k + 1))) = ( card (( succ k) *^ omega )) by Th13, CARD_1: 47

        .= ( card ((k *^ omega ) +^ omega )) by ORDINAL2: 36

        .= (( card (k *^ omega )) +` omega ) by Th12, CARD_1: 47

        .= (( omega *` ( card k)) +` omega ) by Th13, CARD_1: 47

        .= omega by A3, Th75;

        hence thesis;

      end;

      

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

      hence ( omega *` ( card n)) c= omega ;

      thus thesis by A4;

    end;

    theorem :: CARD_2:90

    

     Th89: K in L & M in N or K c= L & M in N or K in L & M c= N or K c= L & M c= N implies (K *` M) c= (L *` N) & (M *` K) c= (L *` N)

    proof

      assume that

       A1: K in L & M in N or K c= L & M in N or K in L & M c= N or K c= L & M c= N;

      

       A2: K c= L by A1, CARD_1: 3;

      

       A3: M c= N by A1, CARD_1: 3;

      

       A4: (K *` M) = ( card [:K, M:]);

      

       A5: [:K, M:] c= [:L, N:] by A2, A3, ZFMISC_1: 96;

      hence (K *` M) c= (L *` N) by CARD_1: 11;

      thus thesis by A4, A5, CARD_1: 11;

    end;

    theorem :: CARD_2:91

    M in N or M c= N implies (K *` M) c= (K *` N) & (K *` M) c= (N *` K) & (M *` K) c= (K *` N) & (M *` K) c= (N *` K) by Th89;

    theorem :: CARD_2:92

    

     Th91: K in L & M in N or K c= L & M in N or K in L & M c= N or K c= L & M c= N implies K = 0 or ( exp (K,M)) c= ( exp (L,N))

    proof

      assume that

       A1: K in L & M in N or K c= L & M in N or K in L & M c= N or K c= L & M c= N;

      

       A2: K c= L by A1, CARD_1: 3;

      

       A3: M c= N by A1, CARD_1: 3;

      now

        assume L <> {} ;

        then

         A4: ( Funcs ((N \ M),L)) <> {} ;

         0 c= ( card ( Funcs ((N \ M),L)));

        then 0 in ( card ( Funcs ((N \ M),L))) by A4, CARD_1: 3;

        then

         A5: ( nextcard ( Segm ( card 0 ))) c= ( card ( Funcs ((N \ M),L))) by CARD_1:def 3;

        ( 0 + 1) = 1;

        then

         A6: ( Segm 1) c= ( card ( Funcs ((N \ M),L))) by A5, Lm8, NAT_1: 42;

        

         A7: M misses (N \ M) by XBOOLE_1: 79;

        

         A8: N = (M \/ (N \ M)) by A3, XBOOLE_1: 45;

        ( Funcs (M,K)) c= ( Funcs (M,L)) by A2, FUNCT_5: 56;

        then

         A9: ( exp (K,M)) c= ( card ( Funcs (M,L))) by CARD_1: 11;

        

         A10: ( exp (L,N)) = ( card [:( Funcs (M,L)), ( Funcs ((N \ M),L)):]) by A7, A8, FUNCT_5: 62;

        

         A11: ( card [:( Funcs (M,L)), ( Funcs ((N \ M),L)):]) = ( card [:( card ( Funcs (M,L))), ( card ( Funcs ((N \ M),L))):]) by Th6;

        (( card ( Funcs (M,L))) *` ( card ( Funcs ((N \ M),L)))) = ( card [:( card ( Funcs (M,L))), ( card ( Funcs ((N \ M),L))):]);

        then (1 *` ( card ( Funcs (M,L)))) c= ( exp (L,N)) by A6, A10, A11, Th89;

        then ( card ( Funcs (M,L))) c= ( exp (L,N)) by Th20;

        hence thesis by A9;

      end;

      hence thesis by A1;

    end;

    theorem :: CARD_2:93

    M in N or M c= N implies K = 0 or ( exp (K,M)) c= ( exp (K,N)) & ( exp (M,K)) c= ( exp (N,K))

    proof

      assume that

       A1: M in N or M c= N and

       A2: K <> 0 ;

      thus ( exp (K,M)) c= ( exp (K,N)) by A1, A2, Th91;

      M = 0 implies ( exp (M,K)) = 0 by A2;

      hence thesis by A1, Th91;

    end;

    theorem :: CARD_2:94

    

     Th93: M c= (M +` N) & N c= (M +` N)

    proof

      

       A1: M c= (M +^ N) by ORDINAL3: 24;

      

       A2: N c= (M +^ N) by ORDINAL3: 24;

      

       A3: ( card N) = N;

      ( card M) = M;

      then

       A4: M c= ( card (M +^ N)) by A1, CARD_1: 11;

      N c= ( card (M +^ N)) by A2, A3, CARD_1: 11;

      hence thesis by A4;

    end;

    theorem :: CARD_2:95

    N <> 0 implies M c= (M *` N) & M c= (N *` M)

    proof

      assume

       A1: N <> 0 ;

      

       A2: ( card M) = M;

      ( card N) = N;

      then

       A3: (M *` N) = ( card (M *^ N)) by A2, Th13;

      M c= (M *^ N) by A1, ORDINAL3: 36;

      hence thesis by A2, A3, CARD_1: 11;

    end;

    theorem :: CARD_2:96

    

     Th95: 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 such that

         A2: K in L and

         A3: M in N and

         A4: L c= N;

        per cases ;

          suppose

           A5: N is finite;

          then

          reconsider N as finite Cardinal;

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

          

           A6: ( card ( Segm K)) = K;

          

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

          

           A8: ( card ( Segm M)) = M;

          

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

          

           A10: (K +` M) = ( card ( Segm (( card K) + ( card M)))) by Th37;

          

           A11: (L +` N) = ( card ( Segm (( card L) + ( card N)))) by Th37;

          

           A12: ( card K) < ( card L) by A2, A6, A7, NAT_1: 41;

          ( card M) < ( card N) by A3, A8, A9, NAT_1: 41;

          then (( card K) + ( card M)) < (( card L) + ( card N)) by A12, XREAL_1: 8;

          hence thesis by A10, A11, NAT_1: 41;

        end;

          suppose

           A13: not N is finite;

          then

           A14: (L +` N) = N by A4, Th75;

          

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

          K c= M & (M is finite or not M is finite) or M c= K & (K is finite or not K is finite);

          then

           A16: K is finite & M is finite or (K +` M) = M or (K +` M) = K & K in N by A2, A4, Th75;

          K is finite & M is finite implies thesis by A14, A15, CARD_1: 61;

          hence thesis by A3, A4, A13, A16, Th75;

        end;

      end;

      L c= N or N c= L;

      hence thesis by A1;

    end;

    theorem :: CARD_2:97

    (K +` M) in (K +` N) implies M in N

    proof

      assume that

       A1: (K +` M) in (K +` N) and

       A2: not M in N;

      N c= M by A2, CARD_1: 4;

      then (K +` N) c= (K +` M) by Th82;

      hence thesis by A1, CARD_1: 4;

    end;

    theorem :: CARD_2:98

    (( card X) +` ( card Y)) = ( card X) & ( card Y) in ( card X) implies ( card (X \ Y)) = ( card X)

    proof

      assume that

       A1: (( card X) +` ( card Y)) = ( card X) and

       A2: ( card Y) in ( card X);

      

       A3: ( card X) c= ( card (X \/ Y)) by CARD_1: 11, XBOOLE_1: 7;

      ( card (X \/ Y)) c= ( card X) by A1, Th33;

      then

       A4: ( card (X \/ Y)) = ( card X) by A3;

      ((X \ Y) \/ Y) = (X \/ Y) by XBOOLE_1: 39;

      then

       A5: ( card X) = (( card (X \ Y)) +` ( card Y)) by A4, Th34, XBOOLE_1: 79;

      then

       A6: ( card (X \ Y)) c= ( card X) by Th93;

       A7:

      now

        assume not ( card X) is finite;

        then

         A8: (( card X) +` ( card X)) = ( card X) by Th74;

        assume not thesis;

        then ( card (X \ Y)) in ( card X) by A6, CARD_1: 3;

        then ( card X) in ( card X) by A2, A5, A8, Th95;

        hence contradiction;

      end;

      now

        assume ( card X) is finite;

        then

        reconsider X, Y as finite set by A2, CARD_3: 92;

        ( card Y) = ( card ( card Y));

        then ( card (( card X) + ( card Y))) = ( card ( card X)) by A1, Th37;

        then (( card X) + ( card Y)) = (( card X) + 0 );

        then Y = {} ;

        hence thesis;

      end;

      hence thesis by A7;

    end;

    theorem :: CARD_2:99

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

    proof

      assume that

       A1: (K *` M) in (K *` N) and

       A2: not M in N;

      N c= M by A2, CARD_1: 4;

      then (K *` N) c= (K *` M) by Th89;

      hence thesis by A1, CARD_1: 4;

    end;

    theorem :: CARD_2:100

    X is countable & Y is countable implies (X \+\ Y) is countable

    proof

      assume that

       A1: X is countable and

       A2: Y is countable;

      

       A3: (X \ Y) is countable by A1;

      (Y \ X) is countable by A2;

      hence thesis by A3, Th84;

    end;

    registration

      let A be finite set, B be set, f be Function of A, ( Fin B);

      cluster ( Union f) -> finite;

      coherence

      proof

        now

          let x be object;

          assume

           A1: x in ( dom f);

          then

          reconsider A as non empty set;

          reconsider x9 = x as Element of A by A1;

          reconsider f9 = f as Function of A, ( Fin B);

          (f9 . x9) is finite;

          hence (f . x) is finite;

        end;

        hence thesis by Th87;

      end;

    end

    registration

      let f be finite finite-yielding Function;

      cluster ( product f) -> finite;

      coherence

      proof

        ( Funcs (( dom f),( Union f))) is finite by FRAENKEL: 6;

        hence thesis by FINSET_1: 1, FUNCT_6: 1;

      end;

    end

    theorem :: CARD_2:101

    for F be Function st ( dom F) is infinite & ( rng F) is finite holds ex x st x in ( rng F) & (F " {x}) is infinite

    proof

      let F be Function such that

       A1: ( dom F) is infinite and

       A2: ( rng F) is finite;

      deffunc f( object) = (F " {$1});

      consider g be Function such that

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

      

       A4: ( dom F) c= ( Union g)

      proof

        let x be object such that

         A5: x in ( dom F);

        

         A6: (F . x) in ( rng F) by A5, FUNCT_1:def 3;

        then

         A7: (g . (F . x)) in ( rng g) by A3, FUNCT_1:def 3;

        (F . x) in {(F . x)} by TARSKI:def 1;

        then

         A8: x in (F " {(F . x)}) by A5, FUNCT_1:def 7;

        (g . (F . x)) = (F " {(F . x)}) by A3, A6;

        then x in ( union ( rng g)) by A8, A7, TARSKI:def 4;

        hence thesis;

      end;

      assume

       A9: for x st x in ( rng F) holds (F " {x}) is finite;

      now

        let x such that

         A10: x in ( dom g);

        (g . x) = (F " {x}) by A3, A10;

        hence (g . x) is finite by A9, A3, A10;

      end;

      then ( Union g) is finite by A2, A3, Th87;

      hence thesis by A1, A4;

    end;

    theorem :: CARD_2:102

    for X,Y be finite set st X c= Y & ( card X) = ( card Y) holds X = Y

    proof

      let X,Y be finite set such that

       A1: X c= Y and

       A2: ( card X) = ( card Y);

      ( card (Y \ X)) = (( card Y) - ( card X)) by A1, Th43;

      then (Y \ X) = {} by A2;

      then Y c= X by XBOOLE_1: 37;

      hence thesis by A1;

    end;

    scheme :: CARD_2:sch3

     { X() -> finite set , P[ object, object] } :

ex x be set st x in X() & for y be set st y in X() & y <> x holds not P[y, x]

      provided

       A1: X() <> {}

       and

       A2: for x,y be set st P[x, y] & P[y, x] holds x = y

       and

       A3: for x,y,z be set st P[x, y] & P[y, z] holds P[x, z];

      

       A4: for x,y be object st P[x, y] & P[y, x] holds x = y

      proof

        let x,y be object;

        reconsider x, y as set by TARSKI: 1;

        P[x, y] & P[y, x] implies x = y by A2;

        hence thesis;

      end;

      

       A5: for x,y,z be object st P[x, y] & P[y, z] holds P[x, z]

      proof

        let x,y,z be object;

        reconsider x, y, z as set by TARSKI: 1;

        P[x, y] & P[y, z] implies P[x, z] by A3;

        hence thesis;

      end;

      consider x be object such that

       A6: x in X() and

       A7: for y be object st y in X() & y <> x holds not P[y, x] from FinRegularity( A1, A4, A5);

      reconsider x as set by TARSKI: 1;

      take x;

      thus thesis by A6, A7;

    end;