card_3.miz

    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;

    definition

      let IT be Function;

      :: CARD_3:def1

      attr IT is Cardinal-yielding means

      : Def1: for x st x in ( dom IT) holds (IT . x) is Cardinal;

    end

    registration

      cluster empty -> Cardinal-yielding for Function;

      coherence ;

    end

    registration

      cluster Cardinal-yielding for Function;

      existence

      proof

        take {} ;

        thus thesis;

      end;

    end

    definition

      mode Cardinal-Function is Cardinal-yielding Function;

    end

    reserve ff for Cardinal-Function;

    registration

      let ff, X;

      cluster (ff | X) -> Cardinal-yielding;

      coherence

      proof

        (ff | X) is Cardinal-yielding

        proof

          let x;

          assume

           A1: x in ( dom (ff | X));

          then

           A2: ((ff | X) . x) = (ff . x) by FUNCT_1: 47;

          ( dom (ff | X)) = (( dom ff) /\ X) by RELAT_1: 61;

          then x in ( dom ff) by A1, XBOOLE_0:def 4;

          hence thesis by A2, Def1;

        end;

        hence thesis;

      end;

    end

    registration

      let X, K;

      cluster (X --> K) -> Cardinal-yielding;

      coherence by FUNCOP_1: 7;

    end

    registration

      let X be object;

      let K;

      cluster (X .--> K) -> Cardinal-yielding;

      coherence ;

    end

    scheme :: CARD_3:sch1

    CFLambda { A() -> set , F( object) -> Cardinal } :

ex ff st ( dom ff) = A() & for x be set st x in A() holds (ff . x) = F(x);

      consider f such that

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

      f is Cardinal-yielding

      proof

        let x;

        assume x in ( dom f);

        then (f . x) = F(x) by A1;

        hence thesis;

      end;

      then

      reconsider f as Cardinal-Function;

      take f;

      thus thesis by A1;

    end;

    definition

      let f;

      :: CARD_3:def2

      func Card f -> Cardinal-Function means

      : Def2: ( dom it ) = ( dom f) & for x st x in ( dom f) holds (it . x) = ( card (f . x));

      existence

      proof

        deffunc f( object) = ( card (f . $1));

        consider g be Cardinal-Function such that

         A1: ( dom g) = ( dom f) and

         A2: for x be set st x in ( dom f) holds (g . x) = f(x) from CFLambda;

        take g;

        thus ( dom g) = ( dom f) by A1;

        let x be object such that

         A3: x in ( dom f);

        reconsider x as set by TARSKI: 1;

        (g . x) = f(x) by A3, A2;

        hence thesis;

      end;

      uniqueness

      proof

        let a1,a2 be Cardinal-Function such that

         A4: ( dom a1) = ( dom f) and

         A5: for x st x in ( dom f) holds (a1 . x) = ( card (f . x)) and

         A6: ( dom a2) = ( dom f) and

         A7: for x st x in ( dom f) holds (a2 . x) = ( card (f . x));

        now

          let x be object;

          assume

           A8: x in ( dom f);

          then (a1 . x) = ( card (f . x)) by A5;

          hence (a1 . x) = (a2 . x) by A7, A8;

        end;

        hence thesis by A4, A6;

      end;

      :: CARD_3:def3

      func disjoin f -> Function means

      : Def3: ( dom it ) = ( dom f) & for x be object st x in ( dom f) holds (it . x) = [:(f . x), {x}:];

      existence

      proof

        deffunc f( object) = [:(f . $1), {$1}:];

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

      end;

      uniqueness

      proof

        let a1,a2 be Function such that

         A9: ( dom a1) = ( dom f) and

         A10: for x be object st x in ( dom f) holds (a1 . x) = [:(f . x), {x}:] and

         A11: ( dom a2) = ( dom f) and

         A12: for x be object st x in ( dom f) holds (a2 . x) = [:(f . x), {x}:];

        now

          let x be object;

          assume

           A13: x in ( dom f);

          then (a1 . x) = [:(f . x), {x}:] by A10;

          hence (a1 . x) = (a2 . x) by A12, A13;

        end;

        hence thesis by A9, A11;

      end;

      :: CARD_3:def4

      func Union f -> set equals ( union ( rng f));

      correctness ;

      defpred P[ object] means ex g st $1 = g & ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) in (f . x);

      :: CARD_3:def5

      func product f -> set means

      : Def5: for x be object holds x in it iff ex g st x = g & ( dom g) = ( dom f) & for y be object st y in ( dom f) holds (g . y) in (f . y);

      existence

      proof

        consider X such that

         A14: for x be object holds x in X iff x in ( Funcs (( dom f),( union ( rng f)))) & P[x] from XBOOLE_0:sch 1;

        take X;

        let x be object;

        thus x in X implies ex g st x = g & ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) in (f . x) by A14;

        given g such that

         A15: x = g and

         A16: ( dom g) = ( dom f) and

         A17: for x be object st x in ( dom f) holds (g . x) in (f . x);

        ( rng g) c= ( union ( rng f))

        proof

          let y be object;

          assume y in ( rng g);

          then

          consider z be object such that

           A18: z in ( dom g) and

           A19: y = (g . z) by FUNCT_1:def 3;



           A20: y in (f . z) by A16, A17, A18, A19;

          (f . z) in ( rng f) by A16, A18, FUNCT_1:def 3;

          hence thesis by A20, TARSKI:def 4;

        end;

        then x in ( Funcs (( dom f),( union ( rng f)))) by A15, A16, FUNCT_2:def 2;

        hence thesis by A14, A15, A16, A17;

      end;

      uniqueness

      proof

        let X1,X2 be set such that

         A21: for x be object holds x in X1 iff P[x] and

         A22: for x be object holds x in X2 iff P[x];

        thus thesis from XBOOLE_0:sch 2( A21, A22);

      end;

    end

    theorem :: CARD_3:1



     Th1: ( Card ff) = ff

    proof

      now

        let x;

        assume x in ( dom ff);

        then

        reconsider M = (ff . x) as Cardinal by Def1;

        ( card M) = M;

        hence (ff . x) = ( card (ff . x));

      end;

      hence thesis by Def2;

    end;

    theorem :: CARD_3:2

    ( Card (X --> Y)) = (X --> ( card Y))

    proof



       A1: ( dom ( Card (X --> Y))) = ( dom (X --> Y)) by Def2;

      then

       A2: ( dom ( Card (X --> Y))) = X;

      now

        let x be object;

        assume

         A4: x in X;

        then

         A5: (( Card (X --> Y)) . x) = ( card ((X --> Y) . x)) by A1, Def2;

        ((X --> ( card Y)) . x) = ( card Y) by A4, FUNCOP_1: 7;

        hence (( Card (X --> Y)) . x) = ((X --> ( card Y)) . x) by A4, A5, FUNCOP_1: 7;

      end;

      hence thesis by A2;

    end;

    theorem :: CARD_3:3

    ( disjoin {} ) = {} by Def3, RELAT_1: 38;

    theorem :: CARD_3:4



     Th4: ( disjoin (x .--> X)) = (x .--> [:X, {x}:])

    proof



       A1: ( dom ( disjoin ( {x} --> X))) = ( dom ( {x} --> X)) by Def3;



       A2: ( dom ( {x} --> X)) = {x};

      now

        let y be object;

        assume

         A4: y in {x};

        then

         A5: (( disjoin ( {x} --> X)) . y) = [:(( {x} --> X) . y), {y}:] by A2, Def3;



         A6: (( {x} --> X) . y) = X by A4, FUNCOP_1: 7;

        (( {x} --> [:X, {x}:]) . y) = [:X, {x}:] by A4, FUNCOP_1: 7;

        hence (( disjoin ( {x} --> X)) . y) = (( {x} --> [:X, {x}:]) . y) by A4, A5, A6, TARSKI:def 1;

      end;

      hence thesis by A1;

    end;

    theorem :: CARD_3:5

    x in ( dom f) & y in ( dom f) & x <> y implies (( disjoin f) . x) misses (( disjoin f) . y)

    proof

      assume that

       A1: x in ( dom f) and

       A2: y in ( dom f) and

       A3: x <> y;

      set z = the Element of ((( disjoin f) . x) /\ (( disjoin f) . y));

      assume

       A4: ((( disjoin f) . x) /\ (( disjoin f) . y)) <> {} ;



       A5: (( disjoin f) . x) = [:(f . x), {x}:] by A1, Def3;



       A6: (( disjoin f) . y) = [:(f . y), {y}:] by A2, Def3;



       A7: z in (( disjoin f) . x) by A4, XBOOLE_0:def 4;



       A8: z in (( disjoin f) . y) by A4, XBOOLE_0:def 4;



       A9: (z `2 ) in {x} by A5, A7, MCART_1: 10;



       A10: (z `2 ) in {y} by A6, A8, MCART_1: 10;

      (z `2 ) = x by A9, TARSKI:def 1;

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

    end;

    theorem :: CARD_3:6



     Th6: ( Union (X --> Y)) c= Y

    proof

      let x be object;

      assume x in ( Union (X --> Y));

      then

      consider Z such that

       A1: x in Z and

       A2: Z in ( rng (X --> Y)) by TARSKI:def 4;

      ex z be object st z in ( dom (X --> Y)) & Z = ((X --> Y) . z) by A2, FUNCT_1:def 3;

      hence thesis by A1, FUNCOP_1: 7;

    end;

    theorem :: CARD_3:7



     Th7: X <> {} implies ( Union (X --> Y)) = Y

    proof

      assume

       A1: X <> {} ;

      set x = the Element of X;

      thus ( Union (X --> Y)) c= Y by Th6;



       A2: ( dom (X --> Y)) = X;

      ((X --> Y) . x) = Y by A1, FUNCOP_1: 7;

      then Y in ( rng (X --> Y)) by A1, A2, FUNCT_1:def 3;

      hence thesis by ZFMISC_1: 74;

    end;

    theorem :: CARD_3:8

    ( Union (x .--> Y)) = Y by Th7;

    theorem :: CARD_3:9



     Th9: g in ( product f) iff ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) in (f . x)

    proof

      thus g in ( product f) implies ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) in (f . x)

      proof

        assume g in ( product f);

        then ex h be Function st g = h & ( dom h) = ( dom f) & for x be object st x in ( dom f) holds (h . x) in (f . x) by Def5;

        hence thesis;

      end;

      thus thesis by Def5;

    end;

    theorem :: CARD_3:10



     Th10: ( product {} ) = { {} }

    proof

      thus ( product {} ) c= { {} }

      proof

        let x be object;

        assume x in ( product {} );

        then ex g st x = g & ( dom g) = ( dom {} ) & for y be object st y in ( dom {} ) holds (g . y) in ( {} . y) by Def5;

        then x = {} ;

        hence thesis by TARSKI:def 1;

      end;

      let x be object;

      assume x in { {} };

      then

       A1: x = {} by TARSKI:def 1;

      for y be object st y in ( dom {} ) holds ( {} . y) in ( {} . y);

      hence thesis by A1, Th9;

    end;

    theorem :: CARD_3:11



     Th11: ( Funcs (X,Y)) = ( product (X --> Y))

    proof

      set f = (X --> Y);

      thus ( Funcs (X,Y)) c= ( product f)

      proof

        let x be object;

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

        then

        consider g such that

         A2: x = g and

         A3: ( dom g) = X and

         A4: ( rng g) c= Y by FUNCT_2:def 2;

        now

          let y be object;

          assume

           A5: y in ( dom f);

          then

           A6: (f . y) = Y by FUNCOP_1: 7;

          (g . y) in ( rng g) by A3, A5, FUNCT_1:def 3;

          hence (g . y) in (f . y) by A4, A6;

        end;

        hence thesis by A2, A3, Def5;

      end;

      let x be object;

      assume x in ( product f);

      then

      consider g such that

       A7: x = g and

       A8: ( dom g) = ( dom f) and

       A9: for x be object st x in ( dom f) holds (g . x) in (f . x) by Def5;

      ( rng g) c= Y

      proof

        let y be object;

        assume y in ( rng g);

        then

        consider z be object such that

         A10: z in ( dom g) and

         A11: y = (g . z) by FUNCT_1:def 3;

        y in (f . z) by A8, A9, A10, A11;

        hence thesis by A8, A10, FUNCOP_1: 7;

      end;

      hence thesis by A7, A8, FUNCT_2:def 2;

    end;

    defpred P[ object] means $1 is Function;

    definition

      let x be object;

      let X;

      defpred R[ object, object] means ex g st $1 = g & $2 = (g . x);

      :: CARD_3:def6

      func pi (X,x) -> set means

      : Def6: for y be object holds y in it iff ex f st f in X & y = (f . x);

      existence

      proof

        consider Y such that

         A1: for y be object holds y in Y iff y in X & P[y] from XBOOLE_0:sch 1;



         A2: for y be object st y in Y holds ex z be object st R[y, z]

        proof

          let y be object;

          assume y in Y;

          then

          reconsider y as Function by A1;

          take (y . x), y;

          thus thesis;

        end;

        consider f such that

         A3: ( dom f) = Y & for y be object st y in Y holds R[y, (f . y)] from CLASSES1:sch 1( A2);

        take ( rng f);

        let y be object;

        thus y in ( rng f) implies ex f st f in X & y = (f . x)

        proof

          assume y in ( rng f);

          then

          consider z be object such that

           A4: z in ( dom f) and

           A5: y = (f . z) by FUNCT_1:def 3;

          consider g such that

           A6: z = g and

           A7: (f . z) = (g . x) by A3, A4;

          take g;

          thus thesis by A1, A3, A4, A5, A6, A7;

        end;

        given g such that

         A8: g in X and

         A9: y = (g . x);



         A10: g in Y by A1, A8;

        then ex f1 st g = f1 & (f . g) = (f1 . x) by A3;

        hence thesis by A3, A9, A10, FUNCT_1:def 3;

      end;

      uniqueness

      proof

        defpred Z[ object] means ex f st f in X & $1 = (f . x);

        let X1,X2 be set such that

         A11: for y be object holds y in X1 iff Z[y] and

         A12: for y be object holds y in X2 iff Z[y];

        thus thesis from XBOOLE_0:sch 2( A11, A12);

      end;

    end

    theorem :: CARD_3:12

    x in ( dom f) & ( product f) <> {} implies ( pi (( product f),x)) = (f . x)

    proof

      assume that

       A1: x in ( dom f) and

       A2: ( product f) <> {} ;



       A3: ( pi (( product f),x)) c= (f . x)

      proof

        let y be object;

        assume y in ( pi (( product f),x));

        then ex g st g in ( product f) & y = (g . x) by Def6;

        hence thesis by A1, Th9;

      end;

      (f . x) c= ( pi (( product f),x))

      proof

        set z = the Element of ( product f);

        consider g such that z = g and

         A4: ( dom g) = ( dom f) and

         A5: for x be object st x in ( dom f) holds (g . x) in (f . x) by A2, Def5;

        let y be object;

        reconsider yy = y as set by TARSKI: 1;

        deffunc f( object) = yy;

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

        defpred C[ object] means x = $1;

        consider h be Function such that

         A6: ( dom h) = ( dom g) & for z be object st z in ( dom g) holds ( C[z] implies (h . z) = f(z)) & ( not C[z] implies (h . z) = g(z)) from PARTFUN1:sch 1;

        assume

         A7: y in (f . x);

        now

          let z be object;

          assume

           A8: z in ( dom f);

          then x <> z implies (g . z) = (h . z) by A4, A6;

          hence (h . z) in (f . z) by A4, A5, A6, A7, A8;

        end;

        then

         A9: h in ( product f) by A4, A6, Th9;

        (h . x) = y by A1, A4, A6;

        hence thesis by A9, Def6;

      end;

      hence thesis by A3;

    end;

    theorem :: CARD_3:13

    ( pi ( {} ,x)) = {}

    proof

      set y = the Element of ( pi ( {} ,x));

      assume not thesis;

      then ex f st f in {} & y = (f . x) by Def6;

      hence contradiction;

    end;

    theorem :: CARD_3:14

    ( pi ( {g},x)) = {(g . x)}

    proof

      thus ( pi ( {g},x)) c= {(g . x)}

      proof

        let y be object;

        assume y in ( pi ( {g},x));

        then

        consider f such that

         A1: f in {g} and

         A2: y = (f . x) by Def6;

        f = g by A1, TARSKI:def 1;

        hence thesis by A2, TARSKI:def 1;

      end;

      let y be object;

      assume

       A3: y in {(g . x)};



       A4: g in {g} by TARSKI:def 1;

      y = (g . x) by A3, TARSKI:def 1;

      hence thesis by A4, Def6;

    end;

    theorem :: CARD_3:15

    ( pi ( {f, g},x)) = {(f . x), (g . x)}

    proof

      thus ( pi ( {f, g},x)) c= {(f . x), (g . x)}

      proof

        let y be object;

        assume y in ( pi ( {f, g},x));

        then

        consider f1 such that

         A1: f1 in {f, g} and

         A2: y = (f1 . x) by Def6;

        f1 = f or f1 = g by A1, TARSKI:def 2;

        hence thesis by A2, TARSKI:def 2;

      end;

      let y be object;

      assume

       A3: y in {(f . x), (g . x)};



       A4: f in {f, g} by TARSKI:def 2;



       A5: g in {f, g} by TARSKI:def 2;

      y = (g . x) or y = (f . x) by A3, TARSKI:def 2;

      hence thesis by A4, A5, Def6;

    end;

    theorem :: CARD_3:16



     Th16: ( pi ((X \/ Y),x)) = (( pi (X,x)) \/ ( pi (Y,x)))

    proof

      thus ( pi ((X \/ Y),x)) c= (( pi (X,x)) \/ ( pi (Y,x)))

      proof

        let y be object;

        assume y in ( pi ((X \/ Y),x));

        then

        consider f such that

         A1: f in (X \/ Y) and

         A2: y = (f . x) by Def6;

        f in X or f in Y by A1, XBOOLE_0:def 3;

        then y in ( pi (X,x)) or y in ( pi (Y,x)) by A2, Def6;

        hence thesis by XBOOLE_0:def 3;

      end;

      let y be object;

      assume y in (( pi (X,x)) \/ ( pi (Y,x)));

      then

       A3: y in ( pi (X,x)) or y in ( pi (Y,x)) by XBOOLE_0:def 3;

       A4:

      now

        assume y in ( pi (X,x));

        then

        consider f such that

         A5: f in X and

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

        f in (X \/ Y) by A5, XBOOLE_0:def 3;

        hence thesis by A6, Def6;

      end;

      now

        assume not y in ( pi (X,x));

        then

        consider f such that

         A7: f in Y and

         A8: y = (f . x) by A3, Def6;

        f in (X \/ Y) by A7, XBOOLE_0:def 3;

        hence thesis by A8, Def6;

      end;

      hence thesis by A4;

    end;

    theorem :: CARD_3:17

    ( pi ((X /\ Y),x)) c= (( pi (X,x)) /\ ( pi (Y,x)))

    proof

      let y be object;

      assume y in ( pi ((X /\ Y),x));

      then

      consider f such that

       A1: f in (X /\ Y) and

       A2: y = (f . x) by Def6;



       A3: f in X by A1, XBOOLE_0:def 4;



       A4: f in Y by A1, XBOOLE_0:def 4;



       A5: y in ( pi (X,x)) by A2, A3, Def6;

      y in ( pi (Y,x)) by A2, A4, Def6;

      hence thesis by A5, XBOOLE_0:def 4;

    end;

    theorem :: CARD_3:18



     Th18: (( pi (X,x)) \ ( pi (Y,x))) c= ( pi ((X \ Y),x))

    proof

      let y be object;

      assume

       A1: y in (( pi (X,x)) \ ( pi (Y,x)));

      then

      consider f such that

       A2: f in X and

       A3: y = (f . x) by Def6;

       not y in ( pi (Y,x)) by A1, XBOOLE_0:def 5;

      then not f in Y by A3, Def6;

      then f in (X \ Y) by A2, XBOOLE_0:def 5;

      hence thesis by A3, Def6;

    end;

    theorem :: CARD_3:19

    (( pi (X,x)) \+\ ( pi (Y,x))) c= ( pi ((X \+\ Y),x))

    proof



       A1: (( pi (X,x)) \ ( pi (Y,x))) c= ( pi ((X \ Y),x)) by Th18;



       A2: (( pi (Y,x)) \ ( pi (X,x))) c= ( pi ((Y \ X),x)) by Th18;

      (( pi ((X \ Y),x)) \/ ( pi ((Y \ X),x))) = ( pi (((X \ Y) \/ (Y \ X)),x)) by Th16;

      hence thesis by A1, A2, XBOOLE_1: 13;

    end;

    theorem :: CARD_3:20



     Th20: ( card ( pi (X,x))) c= ( card X)

    proof

      consider Y such that

       A1: for y be object holds y in Y iff y in X & P[y] from XBOOLE_0:sch 1;

      defpred R[ object, object] means ex g st $1 = g & $2 = (g . x);



       A2: for y be object st y in Y holds ex z be object st R[y, z]

      proof

        let y be object;

        assume y in Y;

        then

        reconsider y as Function by A1;

        take (y . x), y;

        thus thesis;

      end;

      consider f such that

       A3: ( dom f) = Y & for y be object st y in Y holds R[y, (f . y)] from CLASSES1:sch 1( A2);

      now

        let y be object;

        thus y in ( rng f) implies ex f st f in X & y = (f . x)

        proof

          assume y in ( rng f);

          then

          consider z be object such that

           A4: z in ( dom f) and

           A5: y = (f . z) by FUNCT_1:def 3;

          consider g such that

           A6: z = g and

           A7: (f . z) = (g . x) by A3, A4;

          take g;

          thus thesis by A1, A3, A4, A5, A6, A7;

        end;

        given g such that

         A8: g in X and

         A9: y = (g . x);



         A10: g in Y by A1, A8;

        then ex f1 st g = f1 & (f . g) = (f1 . x) by A3;

        hence y in ( rng f) by A3, A9, A10, FUNCT_1:def 3;

      end;

      then ( rng f) = ( pi (X,x)) by Def6;

      then

       A11: ( card ( pi (X,x))) c= ( card Y) by A3, CARD_1: 12;

      Y c= X by A1;

      then ( card Y) c= ( card X) by CARD_1: 11;

      hence thesis by A11;

    end;

    theorem :: CARD_3:21



     Th21: x in ( Union ( disjoin f)) implies ex y,z be object st x = [y, z]

    proof

      assume x in ( Union ( disjoin f));

      then

      consider X such that

       A1: x in X and

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

      consider y be object such that

       A3: y in ( dom ( disjoin f)) and

       A4: X = (( disjoin f) . y) by A2, FUNCT_1:def 3;

      y in ( dom f) by A3, Def3;

      then X = [:(f . y), {y}:] by A4, Def3;

      hence thesis by A1, RELAT_1:def 1;

    end;

    theorem :: CARD_3:22



     Th22: x in ( Union ( disjoin f)) iff (x `2 ) in ( dom f) & (x `1 ) in (f . (x `2 )) & x = [(x `1 ), (x `2 )]

    proof

      thus x in ( Union ( disjoin f)) implies (x `2 ) in ( dom f) & (x `1 ) in (f . (x `2 )) & x = [(x `1 ), (x `2 )]

      proof

        assume x in ( Union ( disjoin f));

        then

        consider X such that

         A1: x in X and

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

        consider y be object such that

         A3: y in ( dom ( disjoin f)) and

         A4: X = (( disjoin f) . y) by A2, FUNCT_1:def 3;



         A5: y in ( dom f) by A3, Def3;

        then

         A6: X = [:(f . y), {y}:] by A4, Def3;

        then

         A7: (x `1 ) in (f . y) by A1, MCART_1: 10;

        (x `2 ) in {y} by A1, A6, MCART_1: 10;

        hence thesis by A1, A5, A6, A7, MCART_1: 21, TARSKI:def 1;

      end;

      assume that

       A8: (x `2 ) in ( dom f) and

       A9: (x `1 ) in (f . (x `2 )) and

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



       A11: (( disjoin f) . (x `2 )) = [:(f . (x `2 )), {(x `2 )}:] by A8, Def3;



       A12: ( dom f) = ( dom ( disjoin f)) by Def3;

      (x `2 ) in {(x `2 )} by TARSKI:def 1;

      then

       A13: x in [:(f . (x `2 )), {(x `2 )}:] by A9, A10, ZFMISC_1: 87;

       [:(f . (x `2 )), {(x `2 )}:] in ( rng ( disjoin f)) by A8, A11, A12, FUNCT_1:def 3;

      hence thesis by A13, TARSKI:def 4;

    end;

    theorem :: CARD_3:23



     Th23: f c= g implies ( disjoin f) c= ( disjoin g)

    proof

      assume

       A1: f c= g;

      then

       A2: ( dom f) c= ( dom g) by GRFUNC_1: 2;



       A3: ( dom ( disjoin f)) = ( dom f) by Def3;



       A4: ( dom ( disjoin g)) = ( dom g) by Def3;

      now

        let x be object;

        assume

         A5: x in ( dom ( disjoin f));

        then

         A6: (( disjoin f) . x) = [:(f . x), {x}:] by A3, Def3;

        (f . x) = (g . x) by A1, A3, A5, GRFUNC_1: 2;

        hence (( disjoin f) . x) = (( disjoin g) . x) by A2, A3, A5, A6, Def3;

      end;

      hence thesis by A2, A3, A4, GRFUNC_1: 2;

    end;

    theorem :: CARD_3:24



     Th24: f c= g implies ( Union f) c= ( Union g)

    proof

      assume

       A1: f c= g;

      then

       A2: ( dom f) c= ( dom g) by GRFUNC_1: 2;

      let x be object;

      assume x in ( Union f);

      then

      consider X such that

       A3: x in X and

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

      consider y be object such that

       A5: y in ( dom f) and

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

      (f . y) = (g . y) by A1, A5, GRFUNC_1: 2;

      then X in ( rng g) by A2, A5, A6, FUNCT_1:def 3;

      hence thesis by A3, TARSKI:def 4;

    end;

    theorem :: CARD_3:25

    ( Union ( disjoin (Y --> X))) = [:X, Y:]

    proof

      set f = (Y --> X);



       A1: ( dom f) = Y;

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

      proof

        let x be object;

        assume x in ( Union ( disjoin f));

        then

        consider Z such that

         A2: x in Z and

         A3: Z in ( rng ( disjoin f)) by TARSKI:def 4;

        consider y be object such that

         A4: y in ( dom ( disjoin f)) and

         A5: Z = (( disjoin f) . y) by A3, FUNCT_1:def 3;



         A6: y in Y by A1, A4, Def3;

        then

         A7: Z = [:(f . y), {y}:] by A1, A5, Def3;



         A8: (f . y) = X by A6, FUNCOP_1: 7;

         {y} c= Y by A6, ZFMISC_1: 31;

        then Z c= [:X, Y:] by A7, A8, ZFMISC_1: 95;

        hence thesis by A2;

      end;

      let x1,x2 be object;

      assume

       A9: [x1, x2] in [:X, Y:];

      then

       A10: x1 in X by ZFMISC_1: 87;



       A11: x2 in Y by A9, ZFMISC_1: 87;

      then

       A12: (f . x2) = X by FUNCOP_1: 7;



       A13: (( disjoin f) . x2) = [:(f . x2), {x2}:] by A1, A11, Def3;



       A14: x2 in ( dom ( disjoin f)) by A1, A11, Def3;

      x2 in {x2} by TARSKI:def 1;

      then

       A15: [x1, x2] in [:(f . x2), {x2}:] by A10, A12, ZFMISC_1: 87;

       [:(f . x2), {x2}:] in ( rng ( disjoin f)) by A13, A14, FUNCT_1:def 3;

      hence thesis by A15, TARSKI:def 4;

    end;

    theorem :: CARD_3:26



     Th26: ( product f) = {} iff {} in ( rng f)

    proof

      thus ( product f) = {} implies {} in ( rng f)

      proof

        assume that

         A1: ( product f) = {} and

         A2: not {} in ( rng f);

         A3:

        now

          assume ( dom f) = {} ;

          then for x be object st x in ( dom f) holds (f . x) in (f . x);

          hence thesis by A1, Def5;

        end;

        now

          assume ( dom f) <> {} ;

          then

          reconsider M = ( rng f) as non empty set by RELAT_1: 42;

          X in M implies X <> {} by A2;

          then

          consider f1 such that ( dom f1) = M and

           A4: for X st X in M holds (f1 . X) in X by FUNCT_1: 111;

          deffunc g( object) = (f1 . (f . $1));

          consider g such that

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

          now

            let x be object;

            assume

             A6: x in ( dom f);

            then

             A7: (f . x) in M by FUNCT_1:def 3;

            (g . x) = (f1 . (f . x)) by A5, A6;

            hence (g . x) in (f . x) by A4, A7;

          end;

          hence thesis by A1, A5, Def5;

        end;

        hence thesis by A3;

      end;

      assume {} in ( rng f);

      then

       A8: ex x be object st x in ( dom f) & {} = (f . x) by FUNCT_1:def 3;

      assume

       A9: ( product f) <> {} ;

      set y = the Element of ( product f);

      ex g st (y = g) & (( dom g) = ( dom f)) & (for x be object st x in ( dom f) holds (g . x) in (f . x)) by A9, Def5;

      hence contradiction by A8;

    end;

    theorem :: CARD_3:27



     Th27: ( dom f) = ( dom g) & (for x st x in ( dom f) holds (f . x) c= (g . x)) implies ( product f) c= ( product g)

    proof

      assume that

       A1: ( dom f) = ( dom g) and

       A2: for x st x in ( dom f) holds (f . x) c= (g . x);

      let x be object;

      assume x in ( product f);

      then

      consider f1 such that

       A3: x = f1 and

       A4: ( dom f1) = ( dom f) and

       A5: for x be object st x in ( dom f) holds (f1 . x) in (f . x) by Def5;

      now

        let x be object;

        assume

         A6: x in ( dom g);

        then

         A7: (f1 . x) in (f . x) by A1, A5;

        (f . x) c= (g . x) by A1, A2, A6;

        hence (f1 . x) in (g . x) by A7;

      end;

      hence thesis by A1, A3, A4, Def5;

    end;

    reserve F,G for Cardinal-Function;

    theorem :: CARD_3:28

    for x st x in ( dom F) holds ( card (F . x)) = (F . x)

    proof

      let x;

      assume x in ( dom F);

      then

      reconsider M = (F . x) as Cardinal by Def1;

      ( card M) = M;

      hence thesis;

    end;

    theorem :: CARD_3:29



     Th29: for x st x in ( dom F) holds ( card (( disjoin F) . x)) = (F . x)

    proof

      let x;

      assume

       A1: x in ( dom F);

      then

      reconsider M = (F . x) as Cardinal by Def1;

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

      then M = ( card [:M, {x}:]) by CARD_1:def 2;

      hence thesis by A1, Def3;

    end;

    definition

      let F;

      :: CARD_3:def7

      func Sum F -> Cardinal equals ( card ( Union ( disjoin F)));

      correctness ;

      :: CARD_3:def8

      func Product F -> Cardinal equals ( card ( product F));

      correctness ;

    end

    theorem :: CARD_3:30

    ( dom F) = ( dom G) & (for x st x in ( dom F) holds (F . x) c= (G . x)) implies ( Sum F) c= ( Sum G)

    proof

      assume that

       A1: ( dom F) = ( dom G) and

       A2: for x st x in ( dom F) holds (F . x) c= (G . x);

      ( Union ( disjoin F)) c= ( Union ( disjoin G))

      proof

        let x be object;

        assume x in ( Union ( disjoin F));

        then

        consider X such that

         A3: x in X and

         A4: X in ( rng ( disjoin F)) by TARSKI:def 4;

        consider y be object such that

         A5: y in ( dom ( disjoin F)) and

         A6: X = (( disjoin F) . y) by A4, FUNCT_1:def 3;



         A7: y in ( dom F) by A5, Def3;

        then

         A8: (F . y) c= (G . y) by A2;



         A9: X = [:(F . y), {y}:] by A6, A7, Def3;



         A10: (( disjoin G) . y) = [:(G . y), {y}:] by A1, A7, Def3;



         A11: y in ( dom ( disjoin G)) by A1, A7, Def3;



         A12: X c= [:(G . y), {y}:] by A8, A9, ZFMISC_1: 95;

         [:(G . y), {y}:] in ( rng ( disjoin G)) by A10, A11, FUNCT_1:def 3;

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

      end;

      hence thesis by CARD_1: 11;

    end;

    theorem :: CARD_3:31

     {} in ( rng F) iff ( Product F) = 0

    proof

      thus {} in ( rng F) implies ( Product F) = 0 by Th26, CARD_1: 27;

      assume ( Product F) = 0 ;

      then ( product F) = {} ;

      hence thesis by Th26;

    end;

    theorem :: CARD_3:32

    ( dom F) = ( dom G) & (for x st x in ( dom F) holds (F . x) c= (G . x)) implies ( Product F) c= ( Product G) by Th27, CARD_1: 11;

    theorem :: CARD_3:33

    F c= G implies ( Sum F) c= ( Sum G)

    proof

      assume F c= G;

      then ( disjoin F) c= ( disjoin G) by Th23;

      hence thesis by Th24, CARD_1: 11;

    end;

    theorem :: CARD_3:34

    F c= G & not 0 in ( rng G) implies ( Product F) c= ( Product G)

    proof

      assume

       A1: F c= G;

      then

       A2: ( dom F) c= ( dom G) by GRFUNC_1: 2;

      assume

       A3: not 0 in ( rng G);

      deffunc f( Function) = ($1 | ( dom F));

      consider f such that

       A4: ( dom f) = ( product G) & for g st g in ( product G) holds (f . g) = f(g) from FUNCT_5:sch 1;

      ( product F) c= ( rng f)

      proof

        let x be object;

        assume x in ( product F);

        then

        consider g such that

         A5: x = g and

         A6: ( dom g) = ( dom F) and

         A7: for x be object st x in ( dom F) holds (g . x) in (F . x) by Def5;



         A8: ( product G) <> {} by A3, Th26;

        set y = the Element of ( product G);

        consider h such that y = h and ( dom h) = ( dom G) and

         A9: for x be object st x in ( dom G) holds (h . x) in (G . x) by A8, Def5;

        deffunc f( object) = (g . $1);

        deffunc g( object) = (h . $1);

        defpred C[ object] means $1 in ( dom F);

        consider f1 such that

         A10: ( dom f1) = ( dom G) & for x be object st x in ( dom G) holds ( C[x] implies (f1 . x) = f(x)) & ( not C[x] implies (f1 . x) = g(x)) from PARTFUN1:sch 1;

        now

          let z be object such that

           A11: z in ( dom G);

           A12:

          now

            assume

             A13: z in ( dom F);

            then

             A14: (f1 . z) = (g . z) by A10, A11;

            (g . z) in (F . z) by A7, A13;

            hence (f1 . z) in (G . z) by A1, A13, A14, GRFUNC_1: 2;

          end;

           not z in ( dom F) implies (f1 . z) = (h . z) by A10, A11;

          hence (f1 . z) in (G . z) by A9, A11, A12;

        end;

        then

         A15: f1 in ( product G) by A10, Def5;

        then

         A16: (f . f1) = (f1 | ( dom F)) by A4;



         A17: ( dom (f1 | ( dom F))) = ( dom F) by A2, A10, RELAT_1: 62;

        now

          let z be object;

          assume

           A18: z in ( dom F);

          then ((f1 | ( dom F)) . z) = (f1 . z) by A17, FUNCT_1: 47;

          hence ((f1 | ( dom F)) . z) = (g . z) by A2, A10, A18;

        end;

        then (f . f1) = g by A6, A16, A17, FUNCT_1: 2;

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

      end;

      hence thesis by A4, CARD_1: 12;

    end;

    theorem :: CARD_3:35

    ( Sum ( {} --> K)) = 0

    proof

      ( dom ( {} --> K)) = {} ;

      then ( dom ( disjoin ( {} --> K))) = {} by Def3;

      hence thesis by CARD_1: 27, RELAT_1: 42, ZFMISC_1: 2;

    end;

    theorem :: CARD_3:36

    ( Product ( {} --> K)) = 1 by Th10, CARD_1: 30;

    theorem :: CARD_3:37

    ( Sum (x .--> K)) = K

    proof



      thus ( Sum (x .--> K)) = ( card ( Union (x .--> [:K, {x}:]))) by Th4

      .= ( card [:K, {x}:]) by Th7

      .= ( card K) by CARD_1: 69

      .= K;

    end;

    theorem :: CARD_3:38

    ( Product (x .--> K)) = K

    proof



      thus ( Product (x .--> K)) = ( card ( Funcs ( {x},K))) by Th11

      .= ( card K) by FUNCT_5: 58

      .= K;

    end;

    theorem :: CARD_3:39



     Th39: ( card ( Union f)) c= ( Sum ( Card f))

    proof

       A1:

      now

        assume ( dom f) = {} ;

        then {} = ( Union f) by RELAT_1: 42, ZFMISC_1: 2;

        hence thesis;

      end;

      now

        assume

         A2: ( dom f) <> {} ;

        defpred P[ set, object] means ex A be set st A = $2 & for x be object holds x in A iff x in ( Funcs (( card $1),$1)) & ex g st x = g & ( rng g) = $1;

        defpred W[ object, object] means P[(f . $1), $2];



         A3: for x be object st x in ( dom f) holds ex y be object st W[x, y]

        proof

          let x be object such that x in ( dom f);

          defpred A[ object] means ex g st $1 = g & ( rng g) = (f . x);

          consider Y such that

           A4: for z be object holds z in Y iff z in ( Funcs (( card (f . x)),(f . x))) & A[z] from XBOOLE_0:sch 1;

          take Y;

           P[(f . x), Y] by A4;

          hence W[x, Y];

        end;

        consider k be Function such that

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

        reconsider M = ( rng k) as non empty set by A2, A5, RELAT_1: 42;

        now

          let X;

          assume X in M;

          then

          consider x be object such that

           A6: x in ( dom k) and

           A7: X = (k . x) by FUNCT_1:def 3;

          (( card (f . x)),(f . x)) are_equipotent by CARD_1:def 2;

          then

          consider g such that g is one-to-one and

           A8: ( dom g) = ( card (f . x)) and

           A9: ( rng g) = (f . x);



           A10: g in ( Funcs (( card (f . x)),(f . x))) by A8, A9, FUNCT_2:def 2;

           W[x, (k . x)] by A5, A6;

          hence X <> {} by A7, A9, A10;

        end;

        then

        consider FF be Function such that ( dom FF) = M and

         A11: for X st X in M holds (FF . X) in X by FUNCT_1: 111;

        set DD = ( union ( rng ( disjoin ( Card f))));

        defpred S[ object, object] means ex g st g = (FF . (k . ($1 `2 ))) & $2 = (g . ($1 `1 ));



         A12: for x be object st x in DD holds ex y be object st S[x, y]

        proof

          let x be object;

          assume x in DD;

          then

          consider X such that

           A13: x in X and

           A14: X in ( rng ( disjoin ( Card f))) by TARSKI:def 4;

          consider y be object such that

           A15: y in ( dom ( disjoin ( Card f))) and

           A16: X = (( disjoin ( Card f)) . y) by A14, FUNCT_1:def 3;



           A17: ( dom ( disjoin ( Card f))) = ( dom ( Card f)) by Def3;



           A18: ( dom ( Card f)) = ( dom f) by Def2;

          X = [:(( Card f) . y), {y}:] by A15, A16, A17, Def3;

          then (x `2 ) in {y} by A13, MCART_1: 10;

          then

           A19: (x `2 ) in ( dom f) by A15, A17, A18, TARSKI:def 1;

          then (k . (x `2 )) in M by A5, FUNCT_1:def 3;

          then

           A20: (FF . (k . (x `2 ))) in (k . (x `2 )) by A11;

           W[(x `2 ), (k . (x `2 ))] by A5, A19;

          then (FF . (k . (x `2 ))) in ( Funcs (( card (f . (x `2 ))),(f . (x `2 )))) by A20;

          then

          consider g such that

           A21: (FF . (k . (x `2 ))) = g and ( dom g) = ( card (f . (x `2 ))) and ( rng g) c= (f . (x `2 )) by FUNCT_2:def 2;

          take (g . (x `1 )), g;

          thus thesis by A21;

        end;

        consider t be Function such that

         A22: ( dom t) = DD & for x be object st x in DD holds S[x, (t . x)] from CLASSES1:sch 1( A12);

        ( union ( rng f)) c= ( rng t)

        proof

          let x be object;

          assume x in ( union ( rng f));

          then

          consider X such that

           A23: x in X and

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

          consider y be object such that

           A25: y in ( dom f) and

           A26: X = (f . y) by A24, FUNCT_1:def 3;

          (k . y) in M by A5, A25, FUNCT_1:def 3;

          then

           A27: (FF . (k . y)) in (k . y) by A11;



           A28: W[y, (k . y)] by A5, A25;

          then (FF . (k . y)) in ( Funcs (( card (f . y)),(f . y))) by A27;

          then

          consider g such that

           A29: (FF . (k . y)) = g and

           A30: ( dom g) = ( card (f . y)) and ( rng g) c= (f . y) by FUNCT_2:def 2;

          ex g st (FF . (k . y)) = g & ( rng g) = (f . y) by A27, A28;

          then

          consider z be object such that

           A31: z in ( dom g) and

           A32: x = (g . z) by A23, A26, A29, FUNCT_1:def 3;



           A33: (( Card f) . y) = ( card (f . y)) by A25, Def2;



           A34: ( dom ( Card f)) = ( dom f) by Def2;

          then

           A35: (( disjoin ( Card f)) . y) = [:( dom g), {y}:] by A25, A30, A33, Def3;



           A36: y in {y} by TARSKI:def 1;



           A37: ( dom ( disjoin ( Card f))) = ( dom f) by A34, Def3;



           A38: [z, y] in [:( dom g), {y}:] by A31, A36, ZFMISC_1: 87;

           [:( dom g), {y}:] in ( rng ( disjoin ( Card f))) by A25, A35, A37, FUNCT_1:def 3;

          then

           A39: [z, y] in DD by A38, TARSKI:def 4;



           A40: ( [z, y] `1 ) = z;

          ( [z, y] `2 ) = y;

          then ex g st g = (FF . (k . y)) & (t . [z, y]) = (g . z) by A22, A39, A40;

          hence thesis by A22, A29, A32, A39, FUNCT_1:def 3;

        end;

        hence thesis by A22, CARD_1: 12;

      end;

      hence thesis by A1;

    end;

    theorem :: CARD_3:40

    ( card ( Union F)) c= ( Sum F)

    proof

      ( Card F) = F by Th1;

      hence thesis by Th39;

    end;

    ::$Notion-Name

    theorem :: CARD_3:41

    ( dom F) = ( dom G) & (for x st x in ( dom F) holds (F . x) in (G . x)) implies ( Sum F) in ( Product G)

    proof

      assume that

       A1: ( dom F) = ( dom G) and

       A2: for x st x in ( dom F) holds (F . x) in (G . x);

      deffunc f( object) = ((G . $1) \ (F . $1));

      consider f such that

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

      now

        assume {} in ( rng f);

        then

        consider x be object such that

         A4: x in ( dom f) and

         A5: {} = (f . x) by FUNCT_1:def 3;

        reconsider Fx = (F . x), Gx = (G . x) as Cardinal by A1, A3, A4, Def1;



         A6: Fx in Gx by A2, A3, A4;

         not Fx in Fx;

        then Fx in (Gx \ Fx) by A6, XBOOLE_0:def 5;

        hence contradiction by A3, A4, A5;

      end;

      then

       A7: ( product f) <> {} by Th26;

      set a = the Element of ( product f);

      consider h be Function such that a = h and ( dom h) = ( dom f) and

       A8: for x be object st x in ( dom f) holds (h . x) in (f . x) by A7, Def5;

      defpred P[ object, Function] means ( dom $2) = ( dom F) & for x st x in ( dom F) holds (($1 `2 ) = x implies ($2 . x) = ($1 `1 )) & (($1 `2 ) <> x implies ($2 . x) = (h . x));

      defpred R[ object, object] means ex g st $2 = g & P[$1, g];



       A9: for x be object st x in ( Union ( disjoin F)) holds ex y be object st R[x, y]

      proof

        let x be object such that x in ( Union ( disjoin F));

        deffunc f( object) = (x `1 );

        deffunc g( object) = (h . $1);

        defpred C[ object] means $1 = (x `2 );

        consider g such that

         A10: ( dom g) = ( dom F) & for u be object st u in ( dom F) holds ( C[u] implies (g . u) = f(u)) & ( not C[u] implies (g . u) = g(u)) from PARTFUN1:sch 1;

        reconsider y = g as object;

        take y, g;

        thus thesis by A10;

      end;

      consider f1 such that

       A11: ( dom f1) = ( Union ( disjoin F)) & for x be object st x in ( Union ( disjoin F)) holds R[x, (f1 . x)] from CLASSES1:sch 1( A9);



       A12: f1 is one-to-one

      proof

        let x,y be object;

        assume that

         A13: x in ( dom f1) and

         A14: y in ( dom f1) and

         A15: (f1 . x) = (f1 . y) and

         A16: x <> y;

        consider g1 be Function such that

         A17: (f1 . x) = g1 and

         A18: P[x, g1] by A11, A13;

        consider g2 be Function such that

         A19: (f1 . y) = g2 and

         A20: P[y, g2] by A11, A14;



         A21: (x `2 ) in ( dom F) by A11, A13, Th22;



         A22: (y `2 ) in ( dom F) by A11, A14, Th22;



         A23: (y `1 ) in (F . (y `2 )) by A11, A14, Th22;



         A24: ex x1,x2 be object st x = [x1, x2] by A11, A13, Th21;



         A25: ex x1,x2 be object st y = [x1, x2] by A11, A14, Th21;



         A26: x = [(x `1 ), (x `2 )] by A24;



         A27: y = [(y `1 ), (y `2 )] by A25;

         A28:

        now

          assume

           A29: (x `1 ) = (y `1 );



           A30: (g2 . (y `2 )) = (y `1 ) by A20, A22;



           A31: (g1 . (y `2 )) = (h . (y `2 )) by A16, A18, A22, A26, A27, A29;



           A32: (f . (y `2 )) = ((G . (y `2 )) \ (F . (y `2 ))) by A3, A22;

          (h . (y `2 )) in (f . (y `2 )) by A3, A8, A22;

          hence contradiction by A15, A17, A19, A23, A30, A31, A32, XBOOLE_0:def 5;

        end;



         A33: (x `2 ) = (y `2 ) implies (g1 . (x `2 )) = (x `1 ) & (g2 . (x `2 )) = (y `1 ) by A18, A20, A21;



         A34: (g1 . (y `2 )) = (y `1 ) by A15, A17, A19, A20, A22;



         A35: (g1 . (y `2 )) = (h . (y `2 )) by A15, A17, A18, A19, A22, A28, A33;



         A36: (f . (y `2 )) = ((G . (y `2 )) \ (F . (y `2 ))) by A3, A22;

        (h . (y `2 )) in (f . (y `2 )) by A3, A8, A22;

        hence contradiction by A23, A34, A35, A36, XBOOLE_0:def 5;

      end;

      ( rng f1) c= ( product G)

      proof

        let x be object;

        assume x in ( rng f1);

        then

        consider y be object such that

         A37: y in ( dom f1) and

         A38: x = (f1 . y) by FUNCT_1:def 3;

        consider g such that

         A39: (f1 . y) = g and

         A40: P[y, g] by A11, A37;

        now

          let x be object;

          assume

           A41: x in ( dom G);

          then

          reconsider Gx = (G . x), Fx = (F . x) as Cardinal by A1, Def1;



           A42: Fx in Gx by A1, A2, A41;



           A43: (y `2 ) = x implies (g . x) = (y `1 ) by A1, A40, A41;



           A44: (y `2 ) <> x implies (g . x) = (h . x) by A1, A40, A41;



           A45: (h . x) in (f . x) by A1, A3, A8, A41;



           A46: (f . x) = (Gx \ Fx) by A1, A3, A41;



           A47: (y `1 ) in (F . (y `2 )) by A11, A37, Th22;

          Fx c= Gx by A42, CARD_1: 3;

          hence (g . x) in (G . x) by A43, A44, A45, A46, A47;

        end;

        hence thesis by A1, A38, A39, A40, Def5;

      end;

      then

       A48: ( Sum F) c= ( Product G) by A11, A12, CARD_1: 10;

      now

        assume ( Sum F) = ( Product G);

        then (( Union ( disjoin F)),( product G)) are_equipotent by CARD_1: 5;

        then

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

         A49: ( dom f) = ( Union ( disjoin F)) and

         A50: ( rng f) = ( product G);

        deffunc f( object) = ((G . $1) \ ( pi ((f .: (( disjoin F) . $1)),$1)));

        consider K be Function such that

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

        now

          assume {} in ( rng K);

          then

          consider x be object such that

           A52: x in ( dom F) and

           A53: {} = (K . x) by A51, FUNCT_1:def 3;

          reconsider x as set by TARSKI: 1;



           A54: (K . x) = ((G . x) \ ( pi ((f .: (( disjoin F) . x)),x))) by A51, A52;

          reconsider Fx = (F . x), Gx = (G . x) as Cardinal by A1, A52, Def1;



           A55: ( card ( pi ((f .: (( disjoin F) . x)),x))) c= ( card (f .: (( disjoin F) . x))) by Th20;



           A56: ( card (f .: (( disjoin F) . x))) c= ( card (( disjoin F) . x)) by CARD_1: 67;

          ( card (( disjoin F) . x)) = Fx by A52, Th29;

          then

           A57: ( card ( pi ((f .: (( disjoin F) . x)),x))) c= Fx by A55, A56;



           A58: Fx in Gx by A2, A52;

          ( card Gx) = Gx;

          hence contradiction by A53, A54, A57, A58, CARD_1: 68, ORDINAL1: 12;

        end;

        then

         A59: ( product K) <> {} by Th26;

        set t = the Element of ( product K);

        consider g such that

         A60: t = g and ( dom g) = ( dom K) and

         A61: for x be object st x in ( dom K) holds (g . x) in (K . x) by A59, Def5;

        now

          let x;

          assume x in ( dom K);

          then (K . x) = ((G . x) \ ( pi ((f .: (( disjoin F) . x)),x))) by A51;

          hence (K . x) c= (G . x);

        end;

        then ( product K) c= ( product G) by A1, A51, Th27;

        then t in ( product G) by A59;

        then

        consider y be object such that

         A62: y in ( dom f) and

         A63: t = (f . y) by A50, FUNCT_1:def 3;

        consider X such that

         A64: y in X and

         A65: X in ( rng ( disjoin F)) by A49, A62, TARSKI:def 4;

        consider x be object such that

         A66: x in ( dom ( disjoin F)) and

         A67: X = (( disjoin F) . x) by A65, FUNCT_1:def 3;

        reconsider x as set by TARSKI: 1;

        g in (f .: X) by A60, A62, A63, A64, FUNCT_1:def 6;

        then

         A68: (g . x) in ( pi ((f .: (( disjoin F) . x)),x)) by A67, Def6;



         A69: x in ( dom F) by A66, Def3;



         A70: not (g . x) in ((G . x) \ ( pi ((f .: (( disjoin F) . x)),x))) by A68, XBOOLE_0:def 5;

        (g . x) in (K . x) by A51, A61, A69;

        hence contradiction by A51, A69, A70;

      end;

      hence thesis by A48, CARD_1: 3;

    end;

    scheme :: CARD_3:sch2

    FuncSeparation { X() -> set , F( object) -> set , P[ object, object] } :

ex f st ( dom f) = X() & for x be object st x in X() holds for y be object holds y in (f . x) iff y in F(x) & P[x, y];

      defpred Q[ object, object] means ex A be set st A = $2 & for y holds y in A iff y in F($1) & P[$1, y];



       A1: for x be object st x in X() holds ex y be object st Q[x, y]

      proof

        let x be object such that x in X();

        defpred R[ object] means P[x, $1];

        consider Y such that

         A2: for y be object holds y in Y iff y in F(x) & R[y] from XBOOLE_0:sch 1;

        take Y;

        reconsider A = Y as set;

        take A;

        thus A = Y & for y holds y in A iff y in F(x) & P[x, y] by A2;

      end;

      consider f such that

       A3: ( dom f) = X() and

       A4: for x be object st x in X() holds Q[x, (f . x)] from CLASSES1:sch 1( A1);

      take f;

      thus ( dom f) = X() by A3;

      let x be object;

      assume x in X();

      then

      consider A be set such that

       A5: A = (f . x) and

       A6: for y holds y in A iff y in F(x) & P[x, y] by A4;

      thus thesis by A5, A6;

    end;



     Lm1: x in ( field R) implies ex y be object st [x, y] in R or [y, x] in R

    proof

      assume x in ( field R);

      then x in ( dom R) or x in ( rng R) by XBOOLE_0:def 3;

      hence thesis by XTUPLE_0:def 12, XTUPLE_0:def 13;

    end;

    theorem :: CARD_3:42



     Th42: X is finite implies ( card X) in ( card omega )

    proof

      assume X is finite;

      then ex n be Nat st (( card X) = ( card n)) by CARD_1: 48;

      hence thesis;

    end;

    theorem :: CARD_3:43



     Th43: ( card A) in ( card B) implies A in B

    proof

      assume that

       A1: ( card A) in ( card B) and

       A2: not A in B;

       not ( card B) c= ( card A) by A1, CARD_1: 4;

      hence contradiction by A2, CARD_1: 11, ORDINAL1: 16;

    end;

    theorem :: CARD_3:44



     Th44: ( card A) in M implies A in M

    proof

      ( card M) = M;

      hence thesis by Th43;

    end;

    theorem :: CARD_3:45



     Th45: X is c=-linear implies ex Y st Y c= X & ( union Y) = ( union X) & for Z st Z c= Y & Z <> {} holds ex Z1 st Z1 in Z & for Z2 st Z2 in Z holds Z1 c= Z2

    proof

      assume

       A1: X is c=-linear;

      consider R such that

       A2: R well_orders X by WELLORD2: 17;



       A3: (R |_2 X) is well-ordering by A2, WELLORD2: 16;



       A4: ( field (R |_2 X)) = X by A2, WELLORD2: 16;

      ((R |_2 X),( RelIncl ( order_type_of (R |_2 X)))) are_isomorphic by A3, WELLORD2:def 2;

      then (( RelIncl ( order_type_of (R |_2 X))),(R |_2 X)) are_isomorphic by WELLORD1: 40;

      then

      consider f such that

       A5: f is_isomorphism_of (( RelIncl ( order_type_of (R |_2 X))),(R |_2 X));

      ( field ( RelIncl ( order_type_of (R |_2 X)))) = ( order_type_of (R |_2 X)) by WELLORD2:def 1;

      then

       A6: ( dom f) = ( order_type_of (R |_2 X)) by A5;



       A7: ( rng f) = X by A4, A5;

      defpred P[ object] means for A, B st B in A & $1 = A holds (f . B) c= (f . A);

      consider Y such that

       A8: for x be set holds x in Y iff x in ( dom f) & P[x] from XFAMILY:sch 1;

      take Z = (f .: Y);

      thus Z c= X by A7, RELAT_1: 111;

      thus ( union Z) c= ( union X) by A7, RELAT_1: 111, ZFMISC_1: 77;

      thus ( union X) c= ( union Z)

      proof

        let x be object;

        assume x in ( union X);

        then

        consider Z1 such that

         A9: x in Z1 and

         A10: Z1 in X by TARSKI:def 4;

        consider y be object such that

         A11: y in ( dom f) and

         A12: Z1 = (f . y) by A7, A10, FUNCT_1:def 3;

        reconsider y as Ordinal by A6, A11;

        defpred P[ Ordinal] means $1 c= y & x in (f . $1);



         A13: ex A st P[A] by A9, A12;

        consider A such that

         A14: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1( A13);



         A15: A in ( dom f) by A6, A11, A14, ORDINAL1: 12;

        now

          let B, C;

          assume that

           A16: C in B and

           A17: A = B;



           A18: C in ( dom f) by A6, A11, A14, A16, A17, ORDINAL1: 10;



           A19: not C c= y or not x in (f . C) by A14, A16, A17, ORDINAL1: 5;



           A20: (f . A) in X by A7, A15, FUNCT_1:def 3;

          (f . C) in X by A7, A18, FUNCT_1:def 3;

          then ((f . C),(f . A)) are_c=-comparable by A1, A20;

          then (f . C) c= (f . A) or (f . A) c= (f . C);

          hence (f . C) c= (f . B) by A14, A16, A17, A19, ORDINAL1:def 2;

        end;

        then A in Y by A8, A15;

        then (f . A) in Z by A15, FUNCT_1:def 6;

        hence thesis by A14, TARSKI:def 4;

      end;

      let V be set;

      assume that

       A21: V c= Z and

       A22: V <> {} ;

      set x = the Element of V;

      x in Z by A21, A22;

      then

      consider y be object such that

       A23: y in ( dom f) and

       A24: y in Y and

       A25: x = (f . y) by FUNCT_1:def 6;

      reconsider y as Ordinal by A6, A23;

      defpred P[ Ordinal] means $1 in Y & (f . $1) in V;

      y = y;

      then

       A26: ex A st P[A] by A22, A24, A25;

      consider A such that

       A27: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1( A26);

      take Z1 = (f . A);

      thus Z1 in V by A27;

      let Z2;

      assume

       A28: Z2 in V;

      then

      consider y be object such that

       A29: y in ( dom f) and

       A30: y in Y and

       A31: Z2 = (f . y) by A21, FUNCT_1:def 6;

      reconsider y as Ordinal by A6, A29;

      A c< y iff A c= y & A <> y;

      then A = y or A in y by A27, A28, A30, A31, ORDINAL1: 11;

      hence thesis by A8, A30, A31;

    end;

    theorem :: CARD_3:46

    (for Z st Z in X holds ( card Z) in M) & X is c=-linear implies ( card ( union X)) c= M

    proof

      assume that

       A1: Z in X implies ( card Z) in M and

       A2: X is c=-linear;

      consider XX be set such that

       A3: XX c= X and

       A4: ( union XX) = ( union X) and

       A5: for Z st Z c= XX & Z <> {} holds ex Z1 st Z1 in Z & for Z2 st Z2 in Z holds Z1 c= Z2 by A2, Th45;



       A6: for Z1, Z2 st Z1 in XX & Z2 in XX holds Z1 c= Z2 or Z2 c= Z1 by A2, A3, XBOOLE_0:def 9;

      consider R such that

       A7: R well_orders ( union X) by WELLORD2: 17;



       A8: R is_reflexive_in ( union X) by A7;



       A9: R is_transitive_in ( union X) by A7;



       A10: R is_antisymmetric_in ( union X) by A7;



       A11: R is_connected_in ( union X) by A7;

      defpred P[ object, object] means ((ex Z1 st Z1 in XX & $1 in Z1 & not $2 in Z1) or (for Z1 st Z1 in XX holds $1 in Z1 iff $2 in Z1) & [$1, $2] in R);

      consider Q such that

       A12: for x,y be object holds [x, y] in Q iff x in ( union X) & y in ( union X) & P[x, y] from RELAT_1:sch 1;



       A13: ( field Q) = ( union X)

      proof

        thus ( field Q) c= ( union X)

        proof

          let x be object;

          assume x in ( field Q);

          then ex y be object st [x, y] in Q or [y, x] in Q by Lm1;

          hence thesis by A12;

        end;

        let x be object;

        assume

         A14: x in ( union X);

        then

         A15: [x, x] in R by A8;

        for Z1 st Z1 in XX holds x in Z1 iff x in Z1;

        then [x, x] in Q by A12, A14, A15;

        hence thesis by RELAT_1: 15;

      end;



       A16: Q is reflexive

      proof

        let x be object;

        assume

         A17: x in ( field Q);

        then

         A18: [x, x] in R by A8, A13;

        for Z1 st Z1 in XX holds x in Z1 iff x in Z1;

        hence thesis by A12, A13, A17, A18;

      end;



       A19: Q is transitive

      proof

        let x,y,z be object such that

         A20: x in ( field Q) and

         A21: y in ( field Q) and

         A22: z in ( field Q) and

         A23: [x, y] in Q and

         A24: [y, z] in Q;

         A25:

        now

          given Z1 such that

           A26: Z1 in XX and

           A27: x in Z1 and

           A28: not y in Z1;

          given Z2 such that

           A29: Z2 in XX and

           A30: y in Z2 and

           A31: not z in Z2;

          Z1 c= Z2 or Z2 c= Z1 by A6, A26, A29;

          hence thesis by A12, A13, A20, A22, A27, A28, A29, A30, A31;

        end;

         A32:

        now

          given Z1 such that

           A33: Z1 in XX and

           A34: x in Z1 and

           A35: not y in Z1;

          assume that

           A36: for Z1 st Z1 in XX holds y in Z1 iff z in Z1 and [y, z] in R;

           not z in Z1 by A33, A35, A36;

          hence thesis by A12, A13, A20, A22, A33, A34;

        end;

         A37:

        now

          given Z1 such that

           A38: Z1 in XX and

           A39: y in Z1 and

           A40: not z in Z1;

          assume that

           A41: for Z1 st Z1 in XX holds x in Z1 iff y in Z1 and [x, y] in R;

          x in Z1 by A38, A39, A41;

          hence thesis by A12, A13, A20, A22, A38, A40;

        end;

        now

          assume that

           A42: for Z1 st Z1 in XX holds x in Z1 iff y in Z1 and

           A43: [x, y] in R and

           A44: for Z1 st Z1 in XX holds y in Z1 iff z in Z1 and

           A45: [y, z] in R;



           A46: [x, z] in R by A9, A13, A20, A21, A22, A43, A45;

          now

            let Z;

            assume

             A47: Z in XX;

            then x in Z iff y in Z by A42;

            hence x in Z iff z in Z by A44, A47;

          end;

          hence thesis by A12, A13, A20, A22, A46;

        end;

        hence thesis by A12, A23, A24, A25, A32, A37;

      end;



       A48: Q is antisymmetric

      proof

        let x,y be object;

        assume that

         A49: x in ( field Q) and

         A50: y in ( field Q) and

         A51: [x, y] in Q and

         A52: [y, x] in Q;



         A53: (ex Z1 st Z1 in XX & x in Z1 & not y in Z1) or (for Z1 st Z1 in XX holds x in Z1 iff y in Z1) & [x, y] in R by A12, A51;



         A54: (ex Z1 st Z1 in XX & y in Z1 & not x in Z1) or (for Z1 st Z1 in XX holds y in Z1 iff x in Z1) & [y, x] in R by A12, A52;

        now

          given Z1 such that

           A55: Z1 in XX and

           A56: x in Z1 and

           A57: not y in Z1;

          given Z2 such that

           A58: Z2 in XX and

           A59: y in Z2 and

           A60: not x in Z2;

          Z1 c= Z2 or Z2 c= Z1 by A6, A55, A58;

          hence thesis by A56, A57, A59, A60;

        end;

        hence thesis by A10, A13, A49, A50, A53, A54;

      end;



       A61: Q is connected

      proof

        let x,y be object such that

         A62: x in ( field Q) and

         A63: y in ( field Q) and

         A64: x <> y;

        now

          assume

           A65: for Z st Z in XX holds x in Z iff y in Z;



           A66: [x, y] in R or [y, x] in R by A11, A13, A62, A63, A64;

          for Z st Z in XX holds y in Z iff x in Z by A65;

          hence thesis by A12, A13, A62, A63, A65, A66;

        end;

        hence thesis by A12, A13, A62, A63;

      end;

      Q is well_founded

      proof

        let Y such that

         A67: Y c= ( field Q) and

         A68: Y <> {} ;

        defpred P[ set] means ($1 /\ Y) <> {} ;

        consider Z such that

         A69: for x be set holds x in Z iff x in XX & P[x] from XFAMILY:sch 1;



         A70: Z c= XX by A69;

        set x = the Element of Y;

        x in ( union XX) by A4, A13, A67, A68;

        then

        consider Z1 such that

         A71: x in Z1 and

         A72: Z1 in XX by TARSKI:def 4;

        (Z1 /\ Y) <> {} by A68, A71, XBOOLE_0:def 4;

        then Z <> {} by A69, A72;

        then

        consider Z1 such that

         A73: Z1 in Z and

         A74: for Z2 st Z2 in Z holds Z1 c= Z2 by A5, A70;



         A75: Z1 in XX by A69, A73;



         A76: (Z1 /\ Y) c= Z1 by XBOOLE_1: 17;



         A77: Z1 c= ( union X) by A3, A75, ZFMISC_1: 74;

        (Z1 /\ Y) <> {} by A69, A73;

        then

        consider x be object such that

         A78: x in (Z1 /\ Y) and

         A79: for y be object st y in (Z1 /\ Y) holds [x, y] in R by A7, A76, A77, WELLORD1: 5, XBOOLE_1: 1;

        take x;

        thus x in Y by A78, XBOOLE_0:def 4;

        assume

         A80: ((Q -Seg x) /\ Y) <> {} ;

        set y = the Element of ((Q -Seg x) /\ Y);



         A81: x in Z1 by A78, XBOOLE_0:def 4;



         A82: y in (Q -Seg x) by A80, XBOOLE_0:def 4;



         A83: y in Y by A80, XBOOLE_0:def 4;



         A84: y <> x by A82, WELLORD1: 1;



         A85: [y, x] in Q by A82, WELLORD1: 1;

         A86:

        now

          given Z2 such that

           A87: Z2 in XX and

           A88: y in Z2 and

           A89: not x in Z2;

          (Z2 /\ Y) <> {} by A83, A88, XBOOLE_0:def 4;

          then Z2 in Z by A69, A87;

          then Z1 c= Z2 by A74;

          hence contradiction by A81, A89;

        end;

        then

         A90: y in Z1 by A12, A75, A81, A85;



         A91: [y, x] in R by A12, A85, A86;

        y in (Z1 /\ Y) by A83, A90, XBOOLE_0:def 4;

        then

         A92: [x, y] in R by A79;



         A93: x in ( union X) by A12, A85;

        y in ( union X) by A12, A85;

        hence contradiction by A10, A84, A91, A92, A93;

      end;

      then Q is well-ordering by A16, A19, A48, A61;

      then (Q,( RelIncl ( order_type_of Q))) are_isomorphic by WELLORD2:def 2;

      then (( RelIncl ( order_type_of Q)),Q) are_isomorphic by WELLORD1: 40;

      then

      consider g such that

       A94: g is_isomorphism_of (( RelIncl ( order_type_of Q)),Q);



       A95: ( field ( RelIncl ( order_type_of Q))) = ( order_type_of Q) by WELLORD2:def 1;

      then

       A96: ( dom g) = ( order_type_of Q) by A94;



       A97: ( rng g) = ( union X) by A13, A94;



       A98: g is one-to-one by A94;



       A99: for Z, x st Z in XX & x in Z holds (Q -Seg x) c= Z

      proof

        let Z, x such that

         A100: Z in XX and

         A101: x in Z;

        let y be object;

        assume y in (Q -Seg x);

        then

         A102: [y, x] in Q by WELLORD1: 1;

        now

          given Z1 such that

           A103: Z1 in XX and

           A104: y in Z1 and

           A105: not x in Z1;

          Z1 c= Z or Z c= Z1 by A6, A100, A103;

          hence thesis by A101, A104, A105;

        end;

        hence thesis by A12, A100, A101, A102;

      end;



       A106: for A st A in ( order_type_of Q) holds ( card A) = ( card (Q -Seg (g . A)))

      proof

        let A such that

         A107: A in ( order_type_of Q);

        (A,(Q -Seg (g . A))) are_equipotent

        proof

          take f = (g | A);

          A c= ( dom g) by A96, A107, ORDINAL1:def 2;

          hence

           A108: f is one-to-one & ( dom f) = A by A98, FUNCT_1: 52, RELAT_1: 62;

          thus ( rng f) c= (Q -Seg (g . A))

          proof

            let x be object;

            assume x in ( rng f);

            then

            consider y be object such that

             A109: y in ( dom f) and

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

            reconsider B = y as Ordinal by A108, A109;



             A111: B in ( order_type_of Q) by A107, A108, A109, ORDINAL1: 10;

            B c= A by A108, A109, ORDINAL1:def 2;

            then

             A112: [B, A] in ( RelIncl ( order_type_of Q)) by A107, A111, WELLORD2:def 1;



             A113: x = (g . B) by A109, A110, FUNCT_1: 47;

            reconsider BB = B as set;

             not BB in BB;

            then

             A114: A <> B by A108, A109;



             A115: [x, (g . A)] in Q by A94, A112, A113;

            x <> (g . A) by A96, A98, A107, A111, A113, A114;

            hence thesis by A115, WELLORD1: 1;

          end;

          let x be object;

          assume

           A116: x in (Q -Seg (g . A));

          then

           A117: [x, (g . A)] in Q by WELLORD1: 1;

          then x in ( union X) by A12;

          then

          consider y be object such that

           A118: y in ( dom g) and

           A119: x = (g . y) by A97, FUNCT_1:def 3;

          reconsider B = y as Ordinal by A96, A118;

           [B, A] in ( RelIncl ( order_type_of Q)) by A94, A95, A107, A117, A118, A119;

          then

           A120: B c= A by A96, A107, A118, WELLORD2:def 1;

          B <> A by A116, A119, WELLORD1: 1;

          then B c< A by A120;

          hence thesis by A118, A119, FUNCT_1: 50, ORDINAL1: 11;

        end;

        hence thesis by CARD_1: 5;

      end;



       A121: ( order_type_of Q) c= M

      proof

        let x be Ordinal;

        assume

         A122: x in ( order_type_of Q);

        reconsider A = x as Ordinal;

        (g . x) in ( union X) by A96, A97, A122, FUNCT_1:def 3;

        then

        consider Z such that

         A123: (g . x) in Z and

         A124: Z in XX by A4, TARSKI:def 4;



         A125: ( card (Q -Seg (g . x))) c= ( card Z) by A99, A123, A124, CARD_1: 11;



         A126: ( card (Q -Seg (g . x))) = ( card A) by A106, A122;

        ( card (Q -Seg (g . x))) in M by A1, A3, A124, A125, ORDINAL1: 12;

        hence thesis by A126, Th44;

      end;

      (( order_type_of Q),( union X)) are_equipotent by A96, A97, A98;

      then

       A127: ( card ( order_type_of Q)) = ( card ( union X)) by CARD_1: 5;

      ( card M) = M;

      hence thesis by A121, A127, CARD_1: 11;

    end;

    begin

    registration

      let f be Function;

      cluster ( product f) -> functional;

      coherence

      proof

        set d = ( product f);

        let x be object;

        assume x in d;

        then ex g be Function st x = g & ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) in (f . x) by Def5;

        hence thesis;

      end;

    end

    registration

      let A be set;

      let B be with_non-empty_elements set;

      cluster -> non-empty for Function of A, B;

      coherence

      proof

        let f be Function of A, B;

        thus not {} in ( rng f);

      end;

    end

    registration

      let f be non-empty Function;

      cluster ( product f) -> non empty;

      coherence

      proof

         not {} in ( rng f);

        hence thesis by Th26;

      end;

    end

    theorem :: CARD_3:47

    for a,b,c,d be set st a <> b holds ( product ((a,b) --> ( {c}, {d}))) = {((a,b) --> (c,d))}

    proof

      let a,b,c,d be set such that

       A1: a <> b;

      set X = {((a,b) --> (c,d))}, f = ((a,b) --> ( {c}, {d}));



       A2: ( dom f) = {a, b} by FUNCT_4: 62;

      now

        let x be object;

        thus x in X implies ex g be Function st x = g & ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) in (f . x)

        proof

          assume

           A3: x in X;

          take g = ((a,b) --> (c,d));

          thus x = g by A3, TARSKI:def 1;

          thus ( dom g) = ( dom f) by A2, FUNCT_4: 62;

          let x be object;

          assume x in ( dom f);

          then

           A4: x = a or x = b by A2, TARSKI:def 2;



           A5: (g . a) = c by A1, FUNCT_4: 63;



           A6: (f . a) = {c} by A1, FUNCT_4: 63;



           A7: (g . b) = d by FUNCT_4: 63;

          (f . b) = {d} by FUNCT_4: 63;

          hence thesis by A4, A5, A6, A7, TARSKI:def 1;

        end;

        given g be Function such that

         A8: x = g and

         A9: ( dom g) = ( dom f) and

         A10: for x be object st x in ( dom f) holds (g . x) in (f . x);



         A11: a in ( dom f) by A2, TARSKI:def 2;



         A12: b in ( dom f) by A2, TARSKI:def 2;



         A13: (g . a) in (f . a) by A10, A11;



         A14: (g . b) in (f . b) by A10, A12;



         A15: (f . a) = {c} by A1, FUNCT_4: 63;



         A16: (f . b) = {d} by FUNCT_4: 63;



         A17: (g . a) = c by A13, A15, TARSKI:def 1;

        (g . b) = d by A14, A16, TARSKI:def 1;

        then g = ((a,b) --> (c,d)) by A2, A9, A17, FUNCT_4: 66;

        hence x in X by A8, TARSKI:def 1;

      end;

      hence thesis by Def5;

    end;

    theorem :: CARD_3:48

    x in ( product f) implies x is Function;

    begin

    reserve A,B for set;

    definition

      let f be Function;

      :: CARD_3:def9

      func sproduct f -> set means

      : Def9: for x be object holds x in it iff ex g st x = g & ( dom g) c= ( dom f) & for x be object st x in ( dom g) holds (g . x) in (f . x);

      existence

      proof

        defpred P[ object] means ex g st $1 = g & ( dom g) c= ( dom f) & for x be object st x in ( dom g) holds (g . x) in (f . x);

        consider A be set such that

         A1: for x be object holds x in A iff x in ( PFuncs (( dom f),( union ( rng f)))) & P[x] from XBOOLE_0:sch 1;

        now

          let x be object;

          thus x in A implies ex g st x = g & ( dom g) c= ( dom f) & for x be object st x in ( dom g) holds (g . x) in (f . x) by A1;

          given g such that

           A2: x = g and

           A3: ( dom g) c= ( dom f) and

           A4: for x be object st x in ( dom g) holds (g . x) in (f . x);

          ( rng g) c= ( union ( rng f))

          proof

            let y be object;

            assume y in ( rng g);

            then

            consider z be object such that

             A5: z in ( dom g) and

             A6: y = (g . z) by FUNCT_1:def 3;



             A7: (g . z) in (f . z) by A4, A5;

            (f . z) in ( rng f) by A3, A5, FUNCT_1:def 3;

            hence thesis by A6, A7, TARSKI:def 4;

          end;

          then x in ( PFuncs (( dom f),( union ( rng f)))) by A2, A3, PARTFUN1:def 3;

          hence x in A by A1, A2, A3, A4;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        defpred P[ object] means ex g st $1 = g & ( dom g) c= ( dom f) & for x be object st x in ( dom g) holds (g . x) in (f . x);

        let A,B be set such that

         A8: for x be object holds x in A iff P[x] and

         A9: for x be object holds x in B iff P[x];

        thus thesis from XBOOLE_0:sch 2( A8, A9);

      end;

    end

    registration

      let f be Function;

      cluster ( sproduct f) -> functional non empty;

      coherence

      proof

        defpred P[ object] means ex g st $1 = g & ( dom g) c= ( dom f) & for x be object st x in ( dom g) holds (g . x) in (f . x);

        consider A be set such that

         A1: for x be object holds x in A iff x in ( PFuncs (( dom f),( union ( rng f)))) & P[x] from XBOOLE_0:sch 1;

         {} is PartFunc of ( dom f), ( union ( rng f)) by RELSET_1: 12;

        then

         A2: {} in ( PFuncs (( dom f),( union ( rng f)))) by PARTFUN1: 45;



         A3: ( dom {} ) c= ( dom f);



         A4: for x be object st x in ( dom {} ) holds ( {} . x) in (f . x);

        now

          let x be object;

          assume x in A;

          then ex g st x = g & ( dom g) c= ( dom f) & for x be object st x in ( dom g) holds (g . x) in (f . x) by A1;

          hence x is Function;

        end;

        then

        reconsider A as functional non empty set by A1, A2, A3, A4, FUNCT_1:def 13;

        now

          let x be object;

          thus x in A implies ex g st x = g & ( dom g) c= ( dom f) & for x be object st x in ( dom g) holds (g . x) in (f . x) by A1;

          given g such that

           A5: x = g and

           A6: ( dom g) c= ( dom f) and

           A7: for x be object st x in ( dom g) holds (g . x) in (f . x);

          ( rng g) c= ( union ( rng f))

          proof

            let y be object;

            assume y in ( rng g);

            then

            consider z be object such that

             A8: z in ( dom g) and

             A9: y = (g . z) by FUNCT_1:def 3;



             A10: (g . z) in (f . z) by A7, A8;

            (f . z) in ( rng f) by A6, A8, FUNCT_1:def 3;

            hence thesis by A9, A10, TARSKI:def 4;

          end;

          then x in ( PFuncs (( dom f),( union ( rng f)))) by A5, A6, PARTFUN1:def 3;

          hence x in A by A1, A5, A6, A7;

        end;

        hence thesis by Def9;

      end;

    end

    theorem :: CARD_3:49



     Th49: g in ( sproduct f) implies ( dom g) c= ( dom f) & for x st x in ( dom g) holds (g . x) in (f . x)

    proof

      assume g in ( sproduct f);

      then ex h st g = h & ( dom h) c= ( dom f) & for x be object st x in ( dom h) holds (h . x) in (f . x) by Def9;

      hence thesis;

    end;

    theorem :: CARD_3:50



     Th50: {} in ( sproduct f)

    proof



       A1: ( dom {} ) c= ( dom f);

      for x be object st x in ( dom {} ) holds ( {} . x) in (f . x);

      hence thesis by A1, Def9;

    end;

    registration

      let f;

      cluster empty for Element of ( sproduct f);

      existence

      proof

         {} in ( sproduct f) by Th50;

        hence thesis;

      end;

    end

    theorem :: CARD_3:51



     Th51: ( product f) c= ( sproduct f)

    proof

      let x be object;

      assume x in ( product f);

      then ex g st x = g & ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) in (f . x) by Def5;

      hence thesis by Def9;

    end;

    theorem :: CARD_3:52



     Th52: x in ( sproduct f) implies x is PartFunc of ( dom f), ( union ( rng f))

    proof

      assume x in ( sproduct f);

      then

      consider g such that

       A1: x = g and

       A2: ( dom g) c= ( dom f) and

       A3: for x be object st x in ( dom g) holds (g . x) in (f . x) by Def9;

      ( rng g) c= ( union ( rng f))

      proof

        let y be object;

        assume y in ( rng g);

        then

        consider z be object such that

         A4: z in ( dom g) and

         A5: y = (g . z) by FUNCT_1:def 3;



         A6: (g . z) in (f . z) by A3, A4;

        (f . z) in ( rng f) by A2, A4, FUNCT_1:def 3;

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

      end;

      hence thesis by A1, A2, RELSET_1: 4;

    end;

    theorem :: CARD_3:53



     Th53: g in ( product f) & h in ( sproduct f) implies (g +* h) in ( product f)

    proof

      assume

       A1: g in ( product f);

      then

       A2: ( dom g) = ( dom f) by Th9;

      assume

       A3: h in ( sproduct f);

      then

       A4: (( dom g) \/ ( dom h)) = ( dom f) by A2, Th49, XBOOLE_1: 12;

      then

       A5: ( dom (g +* h)) = ( dom f) by FUNCT_4:def 1;

      now

        let x be object;

        assume

         A6: x in ( dom f);



         A7: ((( dom g) \ ( dom h)) \/ ( dom h)) = ( dom f) by A4, XBOOLE_1: 39;

        now

          per cases by A6, A7, XBOOLE_0:def 3;

            case

             A8: x in (( dom g) \ ( dom h));

            then not x in ( dom h) by XBOOLE_0:def 5;

            hence x in ( dom f) & ((g +* h) . x) = (g . x) by A2, A8, FUNCT_4: 11;

          end;

            case x in ( dom h);

            hence ((g +* h) . x) = (h . x) by FUNCT_4: 13;

          end;

        end;

        hence ((g +* h) . x) in (f . x) by A1, A3, Th9, Th49;

      end;

      hence thesis by A5, Th9;

    end;

    theorem :: CARD_3:54

    ( product f) <> {} implies (g in ( sproduct f) iff ex h st h in ( product f) & g c= h)

    proof

      assume

       A1: ( product f) <> {} ;

      thus g in ( sproduct f) implies ex h st h in ( product f) & g c= h

      proof

        assume

         A2: g in ( sproduct f);

        set k = the Element of ( product f);

        reconsider k as Function;

        take (k +* g);

        thus (k +* g) in ( product f) by A1, A2, Th53;

        thus thesis by FUNCT_4: 25;

      end;

      given h such that

       A3: h in ( product f) and

       A4: g c= h;



       A5: ( dom h) = ( dom f) by A3, Th9;



       A6: ( dom g) c= ( dom h) by A4, RELAT_1: 11;

      now

        let x be object;

        assume

         A7: x in ( dom g);

        then (g . x) = (h . x) by A4, GRFUNC_1: 2;

        hence (g . x) in (f . x) by A3, A5, A6, A7, Th9;

      end;

      hence thesis by A5, A6, Def9;

    end;

    theorem :: CARD_3:55



     Th55: ( sproduct f) c= ( PFuncs (( dom f),( union ( rng f))))

    proof

      let x be object;

      assume x in ( sproduct f);

      then x is PartFunc of ( dom f), ( union ( rng f)) by Th52;

      hence thesis by PARTFUN1: 45;

    end;

    theorem :: CARD_3:56



     Th56: f c= g implies ( sproduct f) c= ( sproduct g)

    proof

      assume

       A1: f c= g;

      then

       A2: ( dom f) c= ( dom g) by GRFUNC_1: 2;

      let y be object;

      assume y in ( sproduct f);

      then

      consider h such that

       A3: y = h and

       A4: ( dom h) c= ( dom f) and

       A5: for x be object st x in ( dom h) holds (h . x) in (f . x) by Def9;



       A6: ( dom h) c= ( dom g) by A2, A4;

      now

        let x be object;

        assume

         A7: x in ( dom h);

        then (f . x) = (g . x) by A1, A4, GRFUNC_1: 2;

        hence (h . x) in (g . x) by A5, A7;

      end;

      hence thesis by A3, A6, Def9;

    end;

    theorem :: CARD_3:57



     Th57: ( sproduct {} ) = { {} }

    proof

      ( sproduct {} ) c= ( PFuncs ( {} , {} )) by Th55, RELAT_1: 38, ZFMISC_1: 2;

      hence ( sproduct {} ) c= { {} } by PARTFUN1: 48;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      hence thesis by Th50;

    end;

    theorem :: CARD_3:58

    ( PFuncs (A,B)) = ( sproduct (A --> B))

    proof

      now

        per cases ;

          case A = {} ;

          then (A --> B) = ( {} --> B);

          hence thesis by Th57, PARTFUN1: 48;

        end;

          case A <> {} ;

          then

           A2: ( rng (A --> B)) = {B} by FUNCOP_1: 8;



           A3: ( dom (A --> B)) = A;



           A4: B = ( union ( rng (A --> B))) by A2, ZFMISC_1: 25;

          thus ( PFuncs (A,B)) c= ( sproduct (A --> B))

          proof

            let x be object;

            assume x in ( PFuncs (A,B));

            then

            consider f be Function such that

             A5: x = f and

             A6: ( dom f) c= A and

             A7: ( rng f) c= B by PARTFUN1:def 3;



             A8: ( dom f) c= ( dom (A --> B)) by A6;

            now

              let x be object;

              assume

               A9: x in ( dom f);

              then (f . x) in ( rng f) by FUNCT_1:def 3;

              then (f . x) in B by A7;

              hence (f . x) in ((A --> B) . x) by A6, A9, FUNCOP_1: 7;

            end;

            hence thesis by A5, A8, Def9;

          end;

          thus ( sproduct (A --> B)) c= ( PFuncs (A,B)) by A3, A4, Th55;

        end;

      end;

      hence thesis;

    end;

    theorem :: CARD_3:59

    for A,B be non empty set holds for f be Function of A, B holds ( sproduct f) = ( sproduct (f | { x where x be Element of A : (f . x) <> {} }))

    proof

      let A,B be non empty set;

      let f be Function of A, B;

      set X = { x where x be Element of A : (f . x) <> {} };

      thus ( sproduct f) c= ( sproduct (f | X))

      proof

        let x be object;

        assume x in ( sproduct f);

        then

        consider g such that

         A1: x = g and

         A2: ( dom g) c= ( dom f) and

         A3: for x be object st x in ( dom g) holds (g . x) in (f . x) by Def9;

         A4:

        now

          let x;

          assume

           A5: x in ( dom g);

          then

          reconsider a = x as Element of A by A2, FUNCT_2:def 1;

          (f . a) <> {} by A3, A5;

          hence x in X;

        end;

         A6:

        now

          let x;

          assume

           A7: x in ( dom g);

          then x in X by A4;

          hence x in (( dom f) /\ X) by A2, A7, XBOOLE_0:def 4;

        end;



         A8: ( dom g) c= ( dom (f | X))

        proof

          let x be object;

          assume x in ( dom g);

          then x in (( dom f) /\ X) by A6;

          hence thesis by RELAT_1: 61;

        end;

        now

          let x be object;

          assume

           A9: x in ( dom g);

          then (g . x) in (f . x) by A3;

          hence (g . x) in ((f | X) . x) by A6, A9, FUNCT_1: 48;

        end;

        hence thesis by A1, A8, Def9;

      end;

      thus thesis by Th56, RELAT_1: 59;

    end;

    theorem :: CARD_3:60



     Th60: x in ( dom f) & y in (f . x) implies (x .--> y) in ( sproduct f)

    proof

      assume that

       A1: x in ( dom f) and

       A2: y in (f . x);



       A3: ( dom (x .--> y)) c= ( dom f) by A1, ZFMISC_1: 31;

      now

        let z be object;

        assume z in ( dom (x .--> y));

        then z = x by TARSKI:def 1;

        hence ((x .--> y) . z) in (f . z) by A2, FUNCOP_1: 72;

      end;

      hence thesis by A3, Def9;

    end;

    theorem :: CARD_3:61

    ( sproduct f) = { {} } iff for x st x in ( dom f) holds (f . x) = {}

    proof

      thus ( sproduct f) = { {} } implies for x st x in ( dom f) holds (f . x) = {}

      proof

        assume

         A1: ( sproduct f) = { {} };

        let x;

        assume

         A2: x in ( dom f);

        assume

         A3: (f . x) <> {} ;

        set y = the Element of (f . x);

        (x .--> y) in ( sproduct f) by A2, A3, Th60;

        hence contradiction by A1, TARSKI:def 1;

      end;

      assume

       A4: for x st x in ( dom f) holds (f . x) = {} ;

      now

        let x be object;

        thus x in ( sproduct f) implies x = {}

        proof

          assume x in ( sproduct f);

          then

          consider g such that

           A5: x = g and

           A6: ( dom g) c= ( dom f) and

           A7: for y be object st y in ( dom g) holds (g . y) in (f . y) by Def9;

          assume

           A8: x <> {} ;

          set y = the Element of ( dom g);



           A9: (f . y) <> {} by A5, A7, A8;

          y in ( dom f) by A5, A6, A8;

          hence contradiction by A4, A9;

        end;

        thus x = {} implies x in ( sproduct f) by Th50;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: CARD_3:62



     Th62: A c= ( sproduct f) & (for h1,h2 be Function st h1 in A & h2 in A holds h1 tolerates h2) implies ( union A) in ( sproduct f)

    proof

      assume that

       A1: A c= ( sproduct f) and

       A2: for h1,h2 be Function st h1 in A & h2 in A holds h1 tolerates h2;

      reconsider g = ( union A) as Function by A1, A2, PARTFUN1: 78;



       A3: ( dom g) c= ( dom f)

      proof

        let x be object;

        assume x in ( dom g);

        then

        consider y be object such that

         A4: [x, y] in g by XTUPLE_0:def 12;

        consider h be set such that

         A5: [x, y] in h and

         A6: h in A by A4, TARSKI:def 4;

        reconsider h as Function by A1, A6;



         A7: x in ( dom h) by A5, XTUPLE_0:def 12;

        ( dom h) c= ( dom f) by A1, A6, Th49;

        hence thesis by A7;

      end;

      now

        let x be object;

        assume x in ( dom g);

        then

        consider y be object such that

         A8: [x, y] in g by XTUPLE_0:def 12;

        consider h be set such that

         A9: [x, y] in h and

         A10: h in A by A8, TARSKI:def 4;

        reconsider h as Function by A1, A10;



         A11: x in ( dom h) by A9, XTUPLE_0:def 12;

        (h . x) = y by A9, FUNCT_1: 1

        .= (g . x) by A8, FUNCT_1: 1;

        hence (g . x) in (f . x) by A1, A10, A11, Th49;

      end;

      hence thesis by A3, Def9;

    end;

    theorem :: CARD_3:63

    g tolerates h & g in ( sproduct f) & h in ( sproduct f) implies (g \/ h) in ( sproduct f)

    proof

      assume that

       A1: g tolerates h and

       A2: g in ( sproduct f) and

       A3: h in ( sproduct f);



       A4: {g, h} c= ( sproduct f) by A2, A3, ZFMISC_1: 32;

       A5:

      now

        let h1,h2 be Function;

        assume that

         A6: h1 in {g, h} and

         A7: h2 in {g, h};



         A8: h1 = g or h1 = h by A6, TARSKI:def 2;

        h2 = g or h2 = h by A7, TARSKI:def 2;

        hence h1 tolerates h2 by A1, A8;

      end;

      ( union {g, h}) = (g \/ h) by ZFMISC_1: 75;

      hence thesis by A4, A5, Th62;

    end;

    theorem :: CARD_3:64



     Th64: for x be set holds x c= h & h in ( sproduct f) implies x in ( sproduct f)

    proof

      let x be set;

      assume that

       A1: x c= h and

       A2: h in ( sproduct f);

      reconsider g = x as Function by A1;



       A3: ( dom g) c= ( dom h) by A1, GRFUNC_1: 2;

      ( dom h) c= ( dom f) by A2, Th49;

      then

       A4: ( dom g) c= ( dom f) by A3;

      now

        let x be object;

        assume

         A5: x in ( dom g);

        then (h . x) in (f . x) by A2, A3, Th49;

        hence (g . x) in (f . x) by A1, A5, GRFUNC_1: 2;

      end;

      hence thesis by A4, Def9;

    end;

    theorem :: CARD_3:65



     Th65: g in ( sproduct f) implies (g | A) in ( sproduct f) by Th64, RELAT_1: 59;

    theorem :: CARD_3:66



     Th66: g in ( sproduct f) implies (g | A) in ( sproduct (f | A))

    proof



       A1: ( dom (g | A)) = (( dom g) /\ A) by RELAT_1: 61;



       A2: ( dom (f | A)) = (( dom f) /\ A) by RELAT_1: 61;

      assume

       A3: g in ( sproduct f);

      then

       A4: ( dom (g | A)) c= ( dom (f | A)) by A1, A2, Th49, XBOOLE_1: 26;

      now

        let x be object;

        assume

         A5: x in ( dom (g | A));

        then

         A6: ((g | A) . x) = (g . x) by FUNCT_1: 47;



         A7: ((f | A) . x) = (f . x) by A4, A5, FUNCT_1: 47;

        x in ( dom g) by A1, A5, XBOOLE_0:def 4;

        hence ((g | A) . x) in ((f | A) . x) by A3, A6, A7, Th49;

      end;

      hence thesis by A4, Def9;

    end;

    theorem :: CARD_3:67

    h in ( sproduct (f +* g)) implies ex f9,g9 be Function st f9 in ( sproduct f) & g9 in ( sproduct g) & h = (f9 +* g9)

    proof

      assume

       A1: h in ( sproduct (f +* g));

      take (h | (( dom f) \ ( dom g))), (h | ( dom g));



       A2: (h | (( dom f) \ ( dom g))) in ( sproduct ((f +* g) | (( dom f) \ ( dom g)))) by A1, Th66;

      ( sproduct ((f +* g) | (( dom f) \ ( dom g)))) c= ( sproduct f) by Th56, FUNCT_4: 24;

      hence (h | (( dom f) \ ( dom g))) in ( sproduct f) by A2;

      ((f +* g) | ( dom g)) = g;

      hence (h | ( dom g)) in ( sproduct g) by A1, Th66;

      ( dom h) c= ( dom (f +* g)) by A1, Th49;

      then ( dom h) c= (( dom f) \/ ( dom g)) by FUNCT_4:def 1;

      then ( dom h) c= ((( dom f) \ ( dom g)) \/ ( dom g)) by XBOOLE_1: 39;

      hence thesis by FUNCT_4: 70;

    end;

    theorem :: CARD_3:68



     Th68: for f9,g9 be Function st ( dom g) misses (( dom f9) \ ( dom g9)) & f9 in ( sproduct f) & g9 in ( sproduct g) holds (f9 +* g9) in ( sproduct (f +* g))

    proof

      let f9,g9 be Function such that

       A1: ( dom g) misses (( dom f9) \ ( dom g9)) and

       A2: f9 in ( sproduct f) and

       A3: g9 in ( sproduct g);

      set h = (f9 +* g9);



       A4: ( dom f9) c= ( dom f) by A2, Th49;



       A5: ( dom g9) c= ( dom g) by A3, Th49;

      then

       A6: (( dom f9) \/ ( dom g9)) c= (( dom f) \/ ( dom g)) by A4, XBOOLE_1: 13;



       A7: ( dom h) = (( dom f9) \/ ( dom g9)) by FUNCT_4:def 1;

      then

       A8: ( dom h) c= ( dom (f +* g)) by A6, FUNCT_4:def 1;

      for x be object holds x in ( dom h) implies (h . x) in ((f +* g) . x)

      proof

        let x be object;

        assume

         A9: x in ( dom h);

        then x in ( dom (f +* g)) by A8;

        then

         A10: x in (( dom f) \/ ( dom g)) by FUNCT_4:def 1;

        x in ((( dom f9) \ ( dom g9)) \/ ( dom g9)) by A7, A9, XBOOLE_1: 39;

        then

         A11: x in (( dom f9) \ ( dom g9)) or x in ( dom g9) by XBOOLE_0:def 3;

        now

          per cases ;

            case

             A12: x in ( dom g);

            then (h . x) = (g9 . x) by A1, A7, A9, A11, FUNCT_4:def 1, XBOOLE_0: 3;

            hence (h . x) in (g . x) by A1, A3, A11, A12, Th49, XBOOLE_0: 3;

          end;

            case not x in ( dom g);

            then

             A13: not x in ( dom g9) by A5;

            then

             A14: (h . x) = (f9 . x) by A7, A9, FUNCT_4:def 1;

            x in ( dom f9) by A7, A9, A13, XBOOLE_0:def 3;

            hence (h . x) in (f . x) by A2, A14, Th49;

          end;

        end;

        hence thesis by A10, FUNCT_4:def 1;

      end;

      hence thesis by A8, Def9;

    end;

    theorem :: CARD_3:69

    for f9,g9 be Function st ( dom f9) misses (( dom g) \ ( dom g9)) & f9 in ( sproduct f) & g9 in ( sproduct g) holds (f9 +* g9) in ( sproduct (f +* g))

    proof

      let f9,g9 be Function;

      assume ( dom f9) misses (( dom g) \ ( dom g9));

      then ( dom g) misses (( dom f9) \ ( dom g9)) by XBOOLE_1: 81;

      hence thesis by Th68;

    end;

    theorem :: CARD_3:70



     Th70: g in ( sproduct f) & h in ( sproduct f) implies (g +* h) in ( sproduct f)

    proof

      assume that

       A1: g in ( sproduct f) and

       A2: h in ( sproduct f);



       A3: ( dom g) c= ( dom f) by A1, Th49;

      ( dom h) c= ( dom f) by A2, Th49;

      then (( dom g) \/ ( dom h)) c= ( dom f) by A3, XBOOLE_1: 8;

      then

       A4: ( dom (g +* h)) c= ( dom f) by FUNCT_4:def 1;

      now

        let x be object;

        assume x in ( dom (g +* h));

        then x in (( dom g) \/ ( dom h)) by FUNCT_4:def 1;

        then

         A5: x in ((( dom g) \ ( dom h)) \/ ( dom h)) by XBOOLE_1: 39;

        now

          per cases by A5, XBOOLE_0:def 3;

            suppose

             A6: x in ( dom h);

            then (h . x) in (f . x) by A2, Th49;

            hence ((g +* h) . x) in (f . x) by A6, FUNCT_4: 13;

          end;

            suppose

             A7: x in (( dom g) \ ( dom h));

            then

             A8: (g . x) in (f . x) by A1, Th49;

             not x in ( dom h) by A7, XBOOLE_0:def 5;

            hence ((g +* h) . x) in (f . x) by A8, FUNCT_4: 11;

          end;

        end;

        hence ((g +* h) . x) in (f . x);

      end;

      hence thesis by A4, Def9;

    end;

    theorem :: CARD_3:71

    for x1,x2,y1,y2 be set holds x1 in ( dom f) & y1 in (f . x1) & x2 in ( dom f) & y2 in (f . x2) implies ((x1,x2) --> (y1,y2)) in ( sproduct f)

    proof

      let x1,x2,y1,y2 be set;

      assume that

       A1: x1 in ( dom f) and

       A2: y1 in (f . x1);



       A3: (x1 .--> y1) in ( sproduct f) by A1, A2, Th60;

      assume that

       A4: x2 in ( dom f) and

       A5: y2 in (f . x2);



       A6: (x2 .--> y2) in ( sproduct f) by A4, A5, Th60;

      ((x1,x2) --> (y1,y2)) = ((x1 .--> y1) +* (x2 .--> y2)) by FUNCT_4:def 4;

      hence thesis by A3, A6, Th70;

    end;

    begin

    definition

      let IT be set;

      :: CARD_3:def10

      attr IT is with_common_domain means

      : Def10: for f,g be Function st f in IT & g in IT holds ( dom f) = ( dom g);

    end

    registration

      cluster with_common_domain functional non empty for set;

      existence

      proof

        set h = the Function;

        take A = {h};

        for f,g be Function st f in A & g in A holds ( dom f) = ( dom g)

        proof

          let f,g be Function;

          assume that

           A1: f in A and

           A2: g in A;

          f = h by A1, TARSKI:def 1;

          hence thesis by A2, TARSKI:def 1;

        end;

        hence A is with_common_domain;

        thus A is functional;

        thus thesis;

      end;

    end

    registration

      let f;

      cluster {f} -> with_common_domain;

      coherence

      proof

        let g,h be Function;

        assume g in {f};

        then g = f by TARSKI:def 1;

        hence thesis by TARSKI:def 1;

      end;

    end

    definition

      let X be functional set;

      :: CARD_3:def11

      func DOM X -> set equals ( meet the set of all ( dom f) where f be Element of X);

      coherence ;

    end



     Lm2: for X be functional with_common_domain set holds for f be Function st f in X holds ( dom f) = ( DOM X)

    proof

      let X be functional with_common_domain set;

      set A = the set of all ( dom f) where f be Element of X;

      let f be Function;

      assume

       A1: f in X;

      then ( dom f) in A;

      then

       A2: {( dom f)} c= A by ZFMISC_1: 31;

      A c= {( dom f)}

      proof

        let e be object;

        assume e in A;

        then

        consider g be Element of X such that

         A3: e = ( dom g);

        e = ( dom f) by A3, Def10, A1;

        hence e in {( dom f)} by TARSKI:def 1;

      end;

      then A = {( dom f)} by A2;

      hence ( dom f) = ( DOM X) by SETFAM_1: 10;

    end;

    theorem :: CARD_3:72



     Th72: for X be with_common_domain functional set st X = { {} } holds ( DOM X) = {}

    proof

      let X be with_common_domain functional set;

      assume

       A1: X = { {} };

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

      hence thesis by A1, Lm2, RELAT_1: 38;

    end;

    registration

      let X be empty set;

      cluster ( DOM X) -> empty;

      coherence

      proof

        set A = the set of all ( dom f) where f be Element of X;



         A1: A c= { {} }

        proof

          let e be object;

          assume e in A;

          then ex f be Element of X st e = ( dom f);

          then e = ( dom {} ) by SUBSET_1:def 1;

          hence thesis by TARSKI:def 1;

        end;

         { {} } c= A

        proof

          let e be object;

          assume e in { {} };

          then e = {} by TARSKI:def 1;

          then e = ( dom {} );

          then e = ( dom the Element of X) by SUBSET_1:def 1;

          hence thesis;

        end;

        then A = { {} } by A1;

        hence thesis by SETFAM_1: 10;

      end;

    end

    begin

    definition

      let S be functional set;

      :: CARD_3:def12

      func product" S -> Function means

      : Def12: ( dom it ) = ( DOM S) & for i be set st i in ( dom it ) holds (it . i) = ( pi (S,i));

      existence

      proof

        per cases ;

          suppose

           A1: S = {} ;

          take {} ;

          thus thesis by A1;

        end;

          suppose S <> {} ;

          then

          reconsider S1 = S as non empty functional set;

          set D = the set of all ( dom f) where f be Element of S1;

          defpred P[ object, object] means ex A be set st A = $1 & $2 = ( pi (S,A));



           A2: for e be object st e in ( meet D) holds ex u be object st P[e, u]

          proof

            let e be object;

            reconsider A = e as set by TARSKI: 1;

            assume e in ( meet D);

            take u = ( pi (S,A));

            thus thesis;

          end;

          consider g be Function such that

           A3: ( dom g) = ( meet D) and

           A4: for e be object st e in ( meet D) holds P[e, (g . e)] from CLASSES1:sch 1( A2);

          take g;

          thus ( dom g) = ( DOM S) by A3;

          let i be set;

          assume i in ( dom g);

          then P[i, (g . i)] by A3, A4;

          hence thesis;

        end;

      end;

      uniqueness

      proof

        let f,g be Function such that

         A5: ( dom f) = ( DOM S) and

         A6: for i be set st i in ( dom f) holds (f . i) = ( pi (S,i)) and

         A7: ( dom g) = ( DOM S) and

         A8: for i be set st i in ( dom g) holds (g . i) = ( pi (S,i));

        for x be object st x in ( dom f) holds (f . x) = (g . x)

        proof

          let x be object;

          assume

           A9: x in ( dom f);



          hence (f . x) = ( pi (S,x)) by A6

          .= (g . x) by A5, A7, A9, A8;

        end;

        hence f = g by A5, A7;

      end;

    end

    ::$Canceled

    theorem :: CARD_3:74



     Th73: for S be non empty functional set, i be set st i in ( dom ( product" S)) holds (( product" S) . i) = the set of all (f . i) where f be Element of S

    proof

      let S be non empty functional set, i be set;

      assume

       A1: i in ( dom ( product" S));

      hereby

        let x be object;

        assume x in (( product" S) . i);

        then x in ( pi (S,i)) by A1, Def12;

        then ex f be Function st f in S & x = (f . i) by Def6;

        hence x in the set of all (f . i) where f be Element of S;

      end;

      let x be object;

      assume x in the set of all (f . i) where f be Element of S;

      then ex f be Element of S st x = (f . i);

      then x in ( pi (S,i)) by Def6;

      hence thesis by A1, Def12;

    end;

    definition

      let S be set;

      :: CARD_3:def13

      attr S is product-like means

      : Def13: ex f be Function st S = ( product f);

    end

    registration

      let f be Function;

      cluster ( product f) -> product-like;

      coherence ;

    end

    registration

      cluster product-like -> functional with_common_domain for set;

      coherence

      proof

        let S be set;

        given f be Function such that

         A1: S = ( product f);

        thus S is functional by A1;

        let h,g be Function such that

         A2: h in S and

         A3: g in S;



        thus ( dom h) = ( dom f) by A1, A2, Th9

        .= ( dom g) by A1, A3, Th9;

      end;

    end

    registration

      cluster product-like non empty for set;

      existence

      proof

        set B = the with_non-empty_elements set, f = the Function of 0 , B;

        take ( product f);

        thus thesis;

      end;

    end

    ::$Canceled

    theorem :: CARD_3:77



     Th74: for S be functional with_common_domain set holds S c= ( product ( product" S))

    proof

      let S be functional with_common_domain set;

      let f be object;

      assume

       A1: f in S;

      then

      reconsider f as Element of S;



       A2: ( dom f) = ( DOM S) by A1, Lm2

      .= ( dom ( product" S)) by Def12;

      for i be object st i in ( dom ( product" S)) holds (f . i) in (( product" S) . i)

      proof

        let i be object;

        assume i in ( dom ( product" S));

        then (( product" S) . i) = ( pi (S,i)) by Def12;

        hence thesis by A1, Def6;

      end;

      hence thesis by A2, Th9;

    end;

    theorem :: CARD_3:78

    for S be non empty product-like set holds S = ( product ( product" S))

    proof

      let S be non empty product-like set;

      thus S c= ( product ( product" S)) by Th74;

      let x be object;

      assume x in ( product ( product" S));

      then

      consider g be Function such that

       A1: x = g and

       A2: ( dom g) = ( dom ( product" S)) and

       A3: for z be object st z in ( dom ( product" S)) holds (g . z) in (( product" S) . z) by Def5;

      consider p be Function such that

       A4: S = ( product p) by Def13;

      set s = the Element of S;



       A5: ( dom g) = ( DOM S) by A2, Def12

      .= ( dom s) by Lm2

      .= ( dom p) by A4, Th9;

      for z be object st z in ( dom p) holds (g . z) in (p . z)

      proof

        let z be object;

        assume

         A6: z in ( dom p);

        then (g . z) in (( product" S) . z) by A2, A3, A5;

        then (g . z) in ( pi (S,z)) by A2, A5, A6, Def12;

        then ex f be Function st f in S & (g . z) = (f . z) by Def6;

        hence thesis by A4, A6, Th9;

      end;

      hence thesis by A1, A4, A5, Th9;

    end;

    theorem :: CARD_3:79

    for f be Function holds for s,t be Element of ( product f), A be set holds (s +* (t | A)) is Element of ( product f)

    proof

      let f be Function;

      let s,t be Element of ( product f), A be set;

      per cases ;

        suppose f is non-empty;

        then ( product f) <> {} ;

        then

         A1: t in ( product f);

        ( product f) c= ( sproduct f) by Th51;

        hence thesis by A1, Th53, Th65;

      end;

        suppose not f is non-empty;

        then {} in ( rng f);

        then

         A2: ( product f) = {} by Th26;

        t = {} by A2, SUBSET_1:def 1;

        then (t | A) = {} ;

        hence thesis;

      end;

    end;

    theorem :: CARD_3:80

    for f be non-empty Function holds for p be Element of ( sproduct f) holds ex s be Element of ( product f) st p c= s

    proof

      let f be non-empty Function, p be Element of ( sproduct f);

      set h = the Element of ( product f);

      reconsider s = (h +* p) as Element of ( product f) by Th53;

      take s;

      thus thesis by FUNCT_4: 25;

    end;

    theorem :: CARD_3:81



     Th78: g in ( product f) implies (g | A) in ( sproduct f)

    proof



       A1: ( product f) c= ( sproduct f) by Th51;

      assume g in ( product f);

      hence thesis by A1, Th64, RELAT_1: 59;

    end;

    definition

      let f be non-empty Function;

      let g be Element of ( product f);

      let X;

      :: original: |

      redefine

      func g | X -> Element of ( sproduct f) ;

      coherence by Th78;

    end

    theorem :: CARD_3:82

    for f be non-empty Function holds for s,ss be Element of ( product f), A be set holds ((ss +* (s | A)) | A) = (s | A)

    proof

      let f be non-empty Function;

      let s,ss be Element of ( product f);

      let A be set;

      ( dom s) = ( dom f) by Th9

      .= ( dom ss) by Th9;

      then (A /\ ( dom ss)) c= (A /\ ( dom s));

      hence thesis by FUNCT_4: 88;

    end;

    theorem :: CARD_3:83

    for M,x,g be Function st x in ( product M) holds (x * g) in ( product (M * g))

    proof

      let M,x,g be Function;

      assume

       A1: x in ( product M);

      set xg = (x * g);

      set Mg = (M * g);



       A2: ex gg be Function st (x = gg) & (( dom gg) = ( dom M)) & (for x be object st x in ( dom M) holds (gg . x) in (M . x)) by A1, Def5;

      then

       A3: ( dom xg) = ( dom Mg) by RELAT_1: 163;

      now

        let y be object;

        assume

         A4: y in ( dom Mg);

        then

         A5: y in ( dom g) by FUNCT_1: 11;



         A6: (g . y) in ( dom M) by A4, FUNCT_1: 11;



         A7: (xg . y) = (x . (g . y)) by A5, FUNCT_1: 13;

        (Mg . y) = (M . (g . y)) by A5, FUNCT_1: 13;

        hence (xg . y) in (Mg . y) by A2, A6, A7;

      end;

      hence thesis by A3, Def5;

    end;

    theorem :: CARD_3:84

    X is finite iff ( card X) in omega by Th42;

    reserve A,B for Ordinal;

    theorem :: CARD_3:85



     Th82: A is infinite iff omega c= A

    proof

       omega c= A iff not A in omega by ORDINAL1: 16;

      hence thesis;

    end;

    theorem :: CARD_3:86

    N is finite & not M is finite implies N in M & N c= M

    proof

      assume that

       A1: N is finite and

       A2: not M is finite;



       A3: N in omega by A1, CARD_1: 61;

       omega c= M by A2, Th82;

      hence N in M by A3;

      thus thesis by A1, A2;

    end;

    theorem :: CARD_3:87

     not X is finite iff ex Y st Y c= X & ( card Y) = omega

    proof

      thus not X is finite implies ex Y st Y c= X & ( card Y) = omega

      proof

        assume not X is finite;

        then not ( card X) in omega ;

        then

         A1: omega c= ( card X) by CARD_1: 4;

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

        then

        consider f such that

         A2: f is one-to-one and

         A3: ( dom f) = ( card X) and

         A4: ( rng f) = X;

        take Y = (f .: omega );

        thus Y c= X by A4, RELAT_1: 111;

        ( omega ,Y) are_equipotent

        proof

          take (f | omega );

          thus thesis by A1, A2, A3, FUNCT_1: 52, RELAT_1: 62, RELAT_1: 115;

        end;

        hence thesis by CARD_1:def 2;

      end;

      given Y such that

       A5: Y c= X and

       A6: ( card Y) = omega ;

      thus thesis by A5, A6;

    end;

    theorem :: CARD_3:88



     Th85: ( card X) = ( card Y) iff ( nextcard X) = ( nextcard Y)

    proof

      thus ( card X) = ( card Y) implies ( nextcard X) = ( nextcard Y) by CARD_1: 16;

      assume that

       A1: ( nextcard X) = ( nextcard Y) and

       A2: ( card X) <> ( card Y);

      ( card X) in ( card Y) or ( card Y) in ( card X) by A2, ORDINAL1: 14;

      then ( nextcard X) c= ( card Y) & ( card Y) in ( nextcard Y) or ( nextcard Y) c= ( card X) & ( card X) in ( nextcard X) by CARD_1:def 3;

      hence thesis by A1, ORDINAL1: 12;

    end;

    theorem :: CARD_3:89

    ( nextcard N) = ( nextcard M) implies M = N

    proof



       A1: ( card N) = N;

      ( card M) = M;

      hence thesis by A1, Th85;

    end;

    theorem :: CARD_3:90



     Th87: N in M iff ( nextcard N) c= M

    proof



       A1: N in ( nextcard N) by CARD_1: 18;

      ( card N) = N;

      hence thesis by A1, CARD_1:def 3;

    end;

    theorem :: CARD_3:91

    N in ( nextcard M) iff N c= M

    proof



       A1: not N c= M iff M in N by CARD_1: 4;

      N in ( nextcard M) iff not ( nextcard M) c= N by CARD_1: 4;

      hence thesis by A1, Th87;

    end;

    theorem :: CARD_3:92

    M is finite & (N c= M or N in M) implies N is finite

    proof

      assume that

       A1: M is finite and

       A2: N c= M or N in M;

      N c= M by A2, CARD_1: 3;

      hence thesis by A1;

    end;

    reserve n,k for Nat;

    definition

      let X;

      :: CARD_3:def14

      attr X is countable means

      : Def14: ( card X) c= omega ;

      :: CARD_3:def15

      attr X is denumerable means ( card X) = omega ;

    end

    registration

      cluster denumerable -> countable infinite for set;

      coherence ;

      cluster countable infinite -> denumerable for set;

      coherence

      proof

        let X be set;

        assume

         A1: ( card X) c= omega ;

        assume X is infinite;

        then omega c= ( card X) by Th82;

        hence ( card X) = omega by A1;

      end;

    end

    registration

      cluster finite -> countable for set;

      coherence ;

    end

    registration

      cluster omega -> denumerable;

      coherence ;

    end

    registration

      cluster denumerable for set;

      existence

      proof

        take omega ;

        thus thesis;

      end;

    end

    theorem :: CARD_3:93



     Th90: X is countable iff ex f st ( dom f) = omega & X c= ( rng f) by CARD_1: 12, CARD_1: 47;

    registration

      let X be countable set;

      cluster -> countable for Subset of X;

      coherence

      proof

        let Y be Subset of X;



         A1: ( card Y) c= ( card X) by CARD_1: 11;

        ( card X) c= omega by Def14;

        hence ( card Y) c= omega by A1;

      end;

    end



     Lm3: Y c= X & X is countable implies Y is countable;

    theorem :: CARD_3:94

    X is countable implies (X /\ Y) is countable by Lm3, XBOOLE_1: 17;

    theorem :: CARD_3:95

    X is countable implies (X \ Y) is countable;

    theorem :: CARD_3:96

    for A be non empty countable set holds ex f be Function of omega , A st ( rng f) = A

    proof

      let A be non empty countable set;

      consider f be Function such that

       A1: ( dom f) = omega and

       A2: A c= ( rng f) by Th90;

      consider x be object such that

       A3: x in A by XBOOLE_0:def 1;

      set F = ((f | (f " A)) +* (( omega \ (f " A)) --> x));



       A4: ( rng F) = A & ( dom F) = omega

      proof



         A5: (f " A) c= omega by A1, RELAT_1: 132;



         A6: ( dom (f | (f " A))) = ( omega /\ (f " A)) by A1, RELAT_1: 61;

        per cases ;

          suppose

           A7: omega = (f " A);

          then

           A8: ( omega \ (f " A)) = {} by XBOOLE_1: 37;

          then (( dom (f | (f " A))) /\ ( dom (( omega \ (f " A)) --> x))) = {} ;

          then ( dom (f | (f " A))) misses ( dom (( omega \ (f " A)) --> x));

          then F = ((f | (f " A)) \/ (( omega \ (f " A)) --> x)) by FUNCT_4: 31;



          hence ( rng F) = (( rng (f | (f " A))) \/ ( rng (( omega \ (f " A)) --> x))) by RELAT_1: 12

          .= (( rng (f | (f " A))) \/ {} ) by A8

          .= (f .: (f " A)) by RELAT_1: 115

          .= A by A2, FUNCT_1: 77;



          thus ( dom F) = (( dom (f | (f " A))) \/ ( dom (( omega \ (f " A)) --> x))) by FUNCT_4:def 1

          .= (( dom (f | (f " A))) \/ {} ) by A8

          .= omega by A6, A7;

        end;

          suppose omega <> (f " A);

          then

           A9: ( omega \ (f " A)) is non empty by A5, XBOOLE_1: 37;

          ( dom (( omega \ (f " A)) --> x)) = ( omega \ (f " A));

          then F = ((f | (f " A)) \/ (( omega \ (f " A)) --> x)) by A6, FUNCT_4: 31, XBOOLE_1: 89;



          hence ( rng F) = (( rng (f | (f " A))) \/ ( rng (( omega \ (f " A)) --> x))) by RELAT_1: 12

          .= (( rng (f | (f " A))) \/ {x}) by A9, FUNCOP_1: 8

          .= ((f .: (f " A)) \/ {x}) by RELAT_1: 115

          .= (A \/ {x}) by A2, FUNCT_1: 77

          .= A by A3, ZFMISC_1: 40;



          thus ( dom F) = (( dom (f | (f " A))) \/ ( dom (( omega \ (f " A)) --> x))) by FUNCT_4:def 1

          .= (( omega /\ (f " A)) \/ ( omega \ (f " A))) by A6

          .= omega by XBOOLE_1: 51;

        end;

      end;

      then

      reconsider F as Function of omega , A by FUNCT_2:def 1, RELSET_1: 4;

      take F;

      thus thesis by A4;

    end;

    theorem :: CARD_3:97

    for f,g be non-empty Function, x be Element of ( product f), y be Element of ( product g) holds (x +* y) in ( product (f +* g))

    proof

      let f,g be non-empty Function, x be Element of ( product f);

      let y be Element of ( product g);



       A1: ( dom x) = ( dom f) by Th9;



       A2: ( dom y) = ( dom g) by Th9;

      then

       A3: ( dom (x +* y)) = (( dom f) \/ ( dom g)) by A1, FUNCT_4:def 1;



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

      now

        let z be object;

        assume

         A5: z in ( dom (f +* g));

        then z in ( dom g) or not z in ( dom g) & z in ( dom f) by A4, XBOOLE_0:def 3;

        then ((x +* y) . z) = (x . z) & ((f +* g) . z) = (f . z) & (x . z) in (f . z) or ((x +* y) . z) = (y . z) & ((f +* g) . z) = (g . z) & (y . z) in (g . z) by A1, A2, A4, A5, Th9, FUNCT_4:def 1;

        hence ((x +* y) . z) in ((f +* g) . z);

      end;

      hence thesis by A3, A4, Th9;

    end;

    theorem :: CARD_3:98

    for f,g be non-empty Function holds for x be Element of ( product (f +* g)) holds (x | ( dom g)) in ( product g)

    proof

      let f,g be non-empty Function;

      let x be Element of ( product (f +* g));



       A1: ( dom x) = ( dom (f +* g)) by Th9;



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

      then

       A3: ( dom g) c= ( dom x) by A1, XBOOLE_1: 7;



       A4: ( dom (x | ( dom g))) = ( dom g) by A1, A2, RELAT_1: 62, XBOOLE_1: 7;

      now

        let z be object;

        assume

         A5: z in ( dom (x | ( dom g)));

        then

         A6: ((x | ( dom g)) . z) = (x . z) by FUNCT_1: 47;

        ((f +* g) . z) = (g . z) by A4, A5, FUNCT_4: 13;

        hence ((x | ( dom g)) . z) in (g . z) by A1, A3, A4, A5, A6, Th9;

      end;

      hence thesis by A4, Th9;

    end;

    theorem :: CARD_3:99

    for f,g be non-empty Function st f tolerates g holds for x be Element of ( product (f +* g)) holds (x | ( dom f)) in ( product f)

    proof

      let f,g be non-empty Function such that

       A1: f tolerates g;

      let x be Element of ( product (f +* g));



       A2: ( dom x) = ( dom (f +* g)) by Th9;



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

      then

       A4: ( dom f) c= ( dom x) by A2, XBOOLE_1: 7;



       A5: ( dom (x | ( dom f))) = ( dom f) by A2, A3, RELAT_1: 62, XBOOLE_1: 7;

      now

        let z be object;

        assume

         A6: z in ( dom (x | ( dom f)));

        then

         A7: ((x | ( dom f)) . z) = (x . z) by FUNCT_1: 47;

        ((f +* g) . z) = (f . z) by A1, A5, A6, FUNCT_4: 15;

        hence ((x | ( dom f)) . z) in (f . z) by A2, A4, A5, A6, A7, Th9;

      end;

      hence thesis by A5, Th9;

    end;

    theorem :: CARD_3:100



     Th97: for S be with_common_domain functional set, f be Function st f in S holds ( dom f) = ( dom ( product" S))

    proof

      let S be with_common_domain functional set, f be Function such that

       A1: f in S;



      thus ( dom f) = ( DOM S) by A1, Lm2

      .= ( dom ( product" S)) by Def12;

    end;

    theorem :: CARD_3:101



     Th98: for S be functional set, f be Function, i be set st f in S & i in ( dom ( product" S)) holds (f . i) in (( product" S) . i)

    proof

      let S be functional set, F be Function, i be set such that

       A1: F in S;

      assume i in ( dom ( product" S));

      then (( product" S) . i) = the set of all (f . i) where f be Element of S by A1, Th73;

      hence (F . i) in (( product" S) . i) by A1;

    end;

    theorem :: CARD_3:102

    for S be with_common_domain functional set, f be Function, i be set st f in S & i in ( dom f) holds (f . i) in (( product" S) . i)

    proof

      let S be with_common_domain functional set, f be Function, i be set;

      assume that

       A1: f in S and

       A2: i in ( dom f);

      ( dom f) = ( dom ( product" S)) by A1, Th97;

      hence (f . i) in (( product" S) . i) by A1, A2, Th98;

    end;

    registration

      let X be with_common_domain set;

      cluster -> with_common_domain for Subset of X;

      coherence by Def10;

    end

    definition

      let f be Function, x be object;

      :: CARD_3:def16

      func proj (f,x) -> Function means

      : Def16: ( dom it ) = ( product f) & for y be Function st y in ( dom it ) holds (it . y) = (y . x);

      existence

      proof

        defpred P[ object, object] means for g be Function st $1 = g holds $2 = (g . x);

         A1:

        now

          let q be object;

          assume q in ( product f);

          then

          reconsider q1 = q as Function;

          reconsider y = (q1 . x) as object;

          take y;

          thus P[q, y];

        end;

        consider F be Function such that

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

        take F;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let F,G be Function such that

         A3: ( dom F) = ( product f) and

         A4: for y be Function st y in ( dom F) holds (F . y) = (y . x) and

         A5: ( dom G) = ( product f) and

         A6: for y be Function st y in ( dom G) holds (G . y) = (y . x);

        now

          let y be object;

          assume

           A7: y in ( product f);

          then

          reconsider x1 = y as Function;



          thus (F . y) = (x1 . x) by A3, A4, A7

          .= (G . y) by A5, A6, A7;

        end;

        hence thesis by A3, A5;

      end;

    end

    registration

      let f be Function, x be object;

      cluster ( proj (f,x)) -> ( product f) -defined;

      coherence by Def16;

    end

    registration

      let f be Function, x be object;

      cluster ( proj (f,x)) -> total;

      coherence by Def16;

    end

    registration

      let f be non-empty Function;

      cluster -> f -compatible for Element of ( product f);

      coherence

      proof

        let e be Element of ( product f);

        let x be object;

        assume x in ( dom e);

        then x in ( dom f) by Th9;

        hence (e . x) in (f . x) by Th9;

      end;

    end

    registration

      let I be set;

      let f be I -defined non-empty Function;

      cluster -> I -defined for Element of ( product f);

      coherence ;

    end

    registration

      let f be Function;

      cluster -> f -compatible for Element of ( sproduct f);

      coherence by Th49;

    end

    registration

      let I be set;

      let f be I -defined Function;

      cluster -> I -defined for Element of ( sproduct f);

      coherence ;

    end

    registration

      let I be set;

      let f be totalI -defined non-empty Function;

      cluster -> total for Element of ( product f);

      coherence

      proof

        let e be Element of ( product f);



        thus ( dom e) = ( dom f) by Th9

        .= I by PARTFUN1:def 2;

      end;

    end

    theorem :: CARD_3:103



     Th100: for I be set, f be non-emptyI -defined Function holds for p be f -compatibleI -defined Function holds p in ( sproduct f)

    proof

      let I be set, f be non-emptyI -defined Function;

      let p be f -compatibleI -defined Function;



       A1: ( dom p) c= ( dom f) by FUNCT_1: 105;

      for x be object st x in ( dom p) holds (p . x) in (f . x) by FUNCT_1:def 14;

      hence p in ( sproduct f) by A1, Def9;

    end;

    theorem :: CARD_3:104

    for I be set, f be non-emptyI -defined Function holds for p be f -compatibleI -defined Function holds ex s be Element of ( product f) st p c= s

    proof

      let I be set;

      let f be non-emptyI -defined Function, p be f -compatibleI -defined Function;

      reconsider p as Element of ( sproduct f) by Th100;

      set h = the Element of ( product f);

      reconsider s = (h +* p) as Element of ( product f) by Th53;

      take s;

      thus thesis by FUNCT_4: 25;

    end;

    registration

      let X be infinite set, a be set;

      cluster (X --> a) -> infinite;

      coherence ;

    end

    registration

      cluster infinite for Function;

      existence

      proof

        take ( omega --> 0 );

        thus thesis;

      end;

    end



     Lm4: ( field R) is finite implies R is finite

    proof

      assume ( field R) is finite;

      then

      reconsider A = ( field R) as finite set;

      R c= [:A, A:]

      proof

        let y,z be object;

        assume

         A1: [y, z] in R;

        then

         A2: z in ( field R) by RELAT_1: 15;

        y in ( field R) by A1, RELAT_1: 15;

        hence thesis by A2, ZFMISC_1: 87;

      end;

      hence thesis;

    end;

    registration

      let R be infinite Relation;

      cluster ( field R) -> infinite;

      coherence by Lm4;

    end

    registration

      let X be infinite set;

      cluster ( RelIncl X) -> infinite;

      coherence by CARD_1: 63;

    end

    theorem :: CARD_3:105

    for R,S be Relation st (R,S) are_isomorphic & R is finite holds S is finite

    proof

      let R,S be Relation;

      given F be Function such that

       A1: F is_isomorphism_of (R,S);

      assume R is finite;

      then ( field R) is finite;

      then ( dom F) is finite by A1;

      then ( rng F) is finite by FINSET_1: 8;

      then ( field S) is finite by A1;

      hence thesis;

    end;

    theorem :: CARD_3:106

    ( product" { {} }) = {}

    proof

      ( dom ( product" { {} })) = ( DOM { {} }) by Def12

      .= {} by Th72;

      hence thesis;

    end;

    theorem :: CARD_3:107



     Th104: for I be set, f be non-empty ManySortedSet of I holds for s be f -compatible ManySortedSet of I holds s in ( product f)

    proof

      let I be set, f be non-empty ManySortedSet of I;

      let s be f -compatible ManySortedSet of I;



       A1: ( dom s) = I by PARTFUN1:def 2

      .= ( dom f) by PARTFUN1:def 2;

      then for x be object st x in ( dom f) holds (s . x) in (f . x) by FUNCT_1:def 14;

      hence s in ( product f) by A1, Th9;

    end;

    registration

      let I be set, f be non-empty ManySortedSet of I;

      cluster -> total for Element of ( product f);

      coherence ;

    end

    definition

      let I be set, f be non-empty ManySortedSet of I;

      let M be f -compatible ManySortedSet of I;

      :: CARD_3:def17

      func down M -> Element of ( product f) equals M;

      coherence by Th104;

    end

    theorem :: CARD_3:108

    for X be functional with_common_domain set holds for f be Function st f in X holds ( dom f) = ( DOM X) by Lm2;

    theorem :: CARD_3:109

    for x be object, X be non empty functional set st for f be Function st f in X holds x in ( dom f) holds x in ( DOM X)

    proof

      let x be object, X be non empty functional set such that

       A1: for f be Function st f in X holds x in ( dom f);

      set A = the set of all ( dom f) where f be Element of X;

      consider Y be object such that

       A2: Y in X by XBOOLE_0:def 1;

      reconsider Y as Function by A2;



       A3: ( dom Y) in A by A2;

      for Y holds Y in A implies x in Y

      proof

        let Y;

        assume Y in A;

        then ex f be Element of X st Y = ( dom f);

        hence x in Y by A1;

      end;

      hence x in ( DOM X) by A3, SETFAM_1:def 1;

    end;

    scheme :: CARD_3:sch3

    FuncSepOrg { X() -> set , F( object) -> set , P[ object, object] } :

ex f st ( dom f) = X() & for x be set st x in X() holds for y be set holds y in (f . x) iff y in F(x) & P[x, y];

      consider f such that

       A1: ( dom f) = X() and

       A2: for x be object st x in X() holds for y be object holds y in (f . x) iff y in F(x) & P[x, y] from FuncSeparation;

      take f;

      thus thesis by A1, A2;

    end;

    notation

      let X be set;

      antonym X is uncountable for X is countable;

    end

    registration

      cluster uncountable -> non empty for set;

      coherence ;

    end