finset_1.miz



    begin

    definition

      let IT be set;

      :: FINSET_1:def1

      attr IT is finite means

      : Def1: ex p be Function st ( rng p) = IT & ( dom p) in omega ;

    end

    notation

      let IT be set;

      antonym IT is infinite for IT is finite;

    end

    reserve A,B,X,Y,Z,x,y for set;

    reserve f for Function;

    

     Lm1: for x be object holds {x} is finite

    proof

      let x be object;

      set p = ( { {} } --> x);

      take p;

      for y be object holds y in {x} iff ex x be object st x in ( dom p) & y = (p . x)

      proof

        let y be object;

        thus y in {x} implies ex x be object st x in ( dom p) & y = (p . x)

        proof

          assume y in {x};

          then

           A2: y = x by TARSKI:def 1;

          take {} ;

          thus {} in ( dom p) by TARSKI:def 1;

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

          hence thesis by A2, FUNCOP_1: 7;

        end;

        assume ex z be object st z in ( dom p) & y = (p . z);

        then y = x by FUNCOP_1: 7;

        hence thesis by TARSKI:def 1;

      end;

      hence ( rng p) = {x} by FUNCT_1:def 3;

      thus thesis by ORDINAL3: 15;

    end;

    registration

      cluster non empty finite for set;

      existence

      proof

         { the set} is finite by Lm1;

        hence thesis;

      end;

    end

    registration

      cluster empty -> finite for set;

      coherence

      proof

        let A be set;

        assume

         A1: A is empty;

        take {} ;

        thus ( rng {} ) = A by A1;

        thus thesis by ORDINAL1:def 11;

      end;

    end

    scheme :: FINSET_1:sch1

    OLambdaC { A() -> set , C[ object], F,G( object) -> object } :

ex f be Function st ( dom f) = A() & for x be Ordinal st x in A() holds (C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x));

      consider f be Function such that

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

      take f;

      thus thesis by A1;

    end;

    

     Lm2: A is finite & B is finite implies (A \/ B) is finite

    proof

      given p be Function such that

       A1: ( rng p) = A and

       A2: ( dom p) in omega ;

      given q be Function such that

       A3: ( rng q) = B and

       A4: ( dom q) in omega ;

      reconsider domp = ( dom p), domq = ( dom q) as Ordinal by A2, A4;

      deffunc F( Ordinal) = (p . $1);

      deffunc G( Ordinal) = (q . ($1 -^ domp));

      defpred P[ set] means $1 in domp;

      consider f such that

       A5: ( dom f) = (domp +^ domq) and

       A6: for x be Ordinal st x in (domp +^ domq) holds ( P[x] implies (f . x) = F(x)) & ( not P[x] implies (f . x) = G(x)) from OLambdaC;

      take f;

      reconsider domp, domq as natural Ordinal by A2, A4;

      thus ( rng f) = (A \/ B)

      proof

        thus ( rng f) c= (A \/ B)

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A7: x in ( dom f) and

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

          reconsider x as Ordinal by A5, A7;

          per cases ;

            suppose

             A9: x in domp;

            then

             A10: y = (p . x) by A5, A6, A7, A8;

            (p . x) in ( rng p) by A9, FUNCT_1:def 3;

            hence thesis by A1, A10, XBOOLE_0:def 3;

          end;

            suppose

             A11: not x in domp;

            then

             A12: domp c= x by ORDINAL1: 16;

            

             A13: y = (q . (x -^ domp)) by A5, A6, A7, A8, A11;

            (domp +^ (x -^ domp)) = x by A12, ORDINAL3:def 5;

            then (x -^ domp) in ( dom q) by A5, A7, ORDINAL3: 22;

            then y in B by A3, A13, FUNCT_1:def 3;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

        let x be object;

        assume

         A14: x in (A \/ B);

        per cases by A1, A3, A14, XBOOLE_0:def 3;

          suppose x in ( rng p);

          then

          consider y be object such that

           A15: y in ( dom p) and

           A16: x = (p . y) by FUNCT_1:def 3;

          

           A17: ( dom p) c= ( dom f) by A5, ORDINAL3: 24;

          then x = (f . y) by A5, A6, A15, A16;

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

        end;

          suppose x in ( rng q);

          then

          consider y be object such that

           A18: y in domq and

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

          reconsider y as Ordinal by A18;

          set z = (domp +^ y);

          domp c= z by ORDINAL3: 24;

          then

           A20: not z in domp by ORDINAL1: 5;

          

           A21: z in ( dom f) by A5, A18, ORDINAL3: 17;

          x = (q . (z -^ domp)) by A19, ORDINAL3: 52

          .= (f . z) by A5, A6, A20, A21;

          hence thesis by A21, FUNCT_1:def 3;

        end;

      end;

      (domp +^ domq) is natural;

      hence thesis by A5;

    end;

    registration

      let x be object;

      cluster {x} -> finite;

      coherence by Lm1;

    end

    registration

      let x,y be object;

      cluster {x, y} -> finite;

      coherence

      proof

         {x, y} = ( {x} \/ {y}) by ENUMSET1: 1;

        hence thesis by Lm2;

      end;

    end

    registration

      let x,y,z be object;

      cluster {x, y, z} -> finite;

      coherence

      proof

         {x, y, z} = ( {x} \/ {y, z}) by ENUMSET1: 2;

        hence thesis by Lm2;

      end;

    end

    registration

      let x1,x2,x3,x4 be object;

      cluster {x1, x2, x3, x4} -> finite;

      coherence

      proof

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

        hence thesis by Lm2;

      end;

    end

    registration

      let x1,x2,x3,x4,x5 be object;

      cluster {x1, x2, x3, x4, x5} -> finite;

      coherence

      proof

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

        hence thesis by Lm2;

      end;

    end

    registration

      let x1,x2,x3,x4,x5,x6 be object;

      cluster {x1, x2, x3, x4, x5, x6} -> finite;

      coherence

      proof

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

        hence thesis by Lm2;

      end;

    end

    registration

      let x1,x2,x3,x4,x5,x6,x7 be object;

      cluster {x1, x2, x3, x4, x5, x6, x7} -> finite;

      coherence

      proof

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

        hence thesis by Lm2;

      end;

    end

    registration

      let x1,x2,x3,x4,x5,x6,x7,x8 be object;

      cluster {x1, x2, x3, x4, x5, x6, x7, x8} -> finite;

      coherence

      proof

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

        hence thesis by Lm2;

      end;

    end

    registration

      let B be finite set;

      cluster -> finite for Subset of B;

      coherence

      proof

        let A be Subset of B;

        per cases ;

          suppose A is empty;

          hence thesis;

        end;

          suppose A is non empty;

          then

          consider x1 be object such that

           A1: x1 in A;

          consider p be Function such that

           A2: ( rng p) = B and

           A3: ( dom p) in omega by Def1;

          deffunc F( object) = (p . $1);

          deffunc G( object) = x1;

          defpred P[ object] means (p . $1) in A;

          consider q be Function such that

           A4: ( dom q) = ( dom p) and

           A5: for x be object st x in ( dom p) holds ( P[x] implies (q . x) = F(x)) & ( not P[x] implies (q . x) = G(x)) from PARTFUN1:sch 1;

          now

            let y be object;

            thus y in A implies ex x be object st x in ( dom q) & y = (q . x)

            proof

              assume

               A6: y in A;

              then

              consider x be object such that

               A7: x in ( dom p) and

               A8: (p . x) = y by A2, FUNCT_1:def 3;

              take x;

              thus x in ( dom q) by A4, A7;

              thus thesis by A5, A6, A7, A8;

            end;

            given x be object such that

             A9: x in ( dom q) and

             A10: y = (q . x);

            per cases ;

              suppose (p . x) in A;

              hence y in A by A4, A5, A9, A10;

            end;

              suppose not (p . x) in A;

              hence y in A by A1, A4, A5, A9, A10;

            end;

          end;

          then ( rng q) = A by FUNCT_1:def 3;

          hence thesis by A3, A4;

        end;

      end;

    end

    registration

      let X,Y be finite set;

      cluster (X \/ Y) -> finite;

      coherence by Lm2;

    end

    theorem :: FINSET_1:1

    A c= B & B is finite implies A is finite;

    theorem :: FINSET_1:2

    A is finite & B is finite implies (A \/ B) is finite;

    registration

      let A be set, B be finite set;

      cluster (A /\ B) -> finite;

      coherence

      proof

        (A /\ B) c= B by XBOOLE_1: 17;

        hence thesis;

      end;

    end

    registration

      let A be finite set, B be set;

      cluster (A /\ B) -> finite;

      coherence ;

      cluster (A \ B) -> finite;

      coherence ;

    end

    theorem :: FINSET_1:3

    A is finite implies (A /\ B) is finite;

    theorem :: FINSET_1:4

    A is finite implies (A \ B) is finite;

    registration

      let f be Function, A be finite set;

      cluster (f .: A) -> finite;

      coherence

      proof

        set B = (( dom f) /\ A);

        consider p be Function such that

         A1: ( rng p) = B and

         A2: ( dom p) in omega by Def1;

        take (f * p);

        ( rng (f * p)) = (f .: B) by A1, RELAT_1: 127;

        hence ( rng (f * p)) = (f .: A) by RELAT_1: 112;

        thus thesis by A1, A2, RELAT_1: 27, XBOOLE_1: 17;

      end;

    end

    theorem :: FINSET_1:5

    A is finite implies (f .: A) is finite;

    reserve O for Ordinal;

    theorem :: FINSET_1:6

    

     Th6: A is finite implies for X be Subset-Family of A st X <> {} holds ex x be set st x in X & for B be set st B in X holds x c= B implies B = x

    proof

      assume

       A1: A is finite;

      let X be Subset-Family of A such that

       A2: X <> {} ;

      consider p be Function such that

       A3: ( rng p) = A and

       A4: ( dom p) in omega by A1;

      defpred P[ set] means (p .: $1) in X;

      consider G be set such that

       A5: for x holds x in G iff x in ( bool ( dom p)) & P[x] from XFAMILY:sch 1;

      G c= ( bool ( dom p)) by A5;

      then

      reconsider GX = G as Subset-Family of ( dom p);

      set x = the Element of X;

      x is Subset of A by A2, TARSKI:def 3;

      then

       A6: (p .: (p " x)) = x by A3, FUNCT_1: 77;

      (p " x) c= ( dom p) by RELAT_1: 132;

      then

       A7: GX <> {} by A2, A5, A6;

      defpred P[ set] means $1 in omega implies for X be Subset-Family of $1 st X <> {} holds ex x be set st x in X & for B be set st B in X holds x c= B implies B = x;

      

       A8: P[ 0 ]

      proof

        assume 0 in omega ;

        let X be Subset-Family of 0 ;

        assume X <> {} ;

        then

         A9: X = { {} } by ZFMISC_1: 1, ZFMISC_1: 33;

        take {} ;

        thus thesis by A9, TARSKI:def 1;

      end;

      

       A10: P[O] implies P[( succ O)]

      proof

        assume

         A11: O in omega implies for X be Subset-Family of O st X <> {} holds ex x be set st x in X & for B be set st B in X holds x c= B implies B = x;

        thus ( succ O) in omega implies for X be Subset-Family of ( succ O) st X <> {} holds ex x be set st x in X & for B be set st B in X holds x c= B implies B = x

        proof

          assume ( succ O) in omega ;

          then

           A12: ( succ O) c= omega by ORDINAL1:def 2;

          let X be Subset-Family of ( succ O) such that

           A13: X <> {} ;

          defpred P[ set] means ex A st A in X & $1 = (A \ {O});

          consider X1 be set such that

           A14: for x holds x in X1 iff x in ( bool O) & P[x] from XFAMILY:sch 1;

          X1 c= ( bool O) by A14;

          then

          reconsider X2 = X1 as Subset-Family of O;

          set y = the Element of X;

          y is Subset of ( succ O) by A13, TARSKI:def 3;

          then (y \ {O}) c= ((O \/ {O}) \ {O}) by XBOOLE_1: 33;

          then

           A15: (y \ {O}) c= (O \ {O}) by XBOOLE_1: 40;

          

           A16: O in ( succ O) by ORDINAL1: 6;

          

           A17: not O in O;

          then (y \ {O}) c= O by A15, ZFMISC_1: 57;

          then X2 <> {} by A13, A14;

          then

          consider Z such that

           A18: Z in X2 and

           A19: for B be set st B in X2 holds Z c= B implies B = Z by A11, A12, A16;

          consider X1 be set such that

           A20: X1 in X and

           A21: Z = (X1 \ {O}) by A14, A18;

          

           A22: O in {O} by TARSKI:def 1;

          then

           A23: not O in Z by A21, XBOOLE_0:def 5;

           A24:

          now

            assume

             A25: (Z \/ {O}) in X;

            take A = (Z \/ {O});

            for B be set st B in X holds A c= B implies B = A

            proof

              let B such that

               A26: B in X;

              assume

               A27: A c= B;

               A28:

              now

                assume

                 A29: O in B;

                set Y = (B \ {O});

                 {O} c= B by A29, ZFMISC_1: 31;

                then

                 A30: B = (Y \/ {O}) by XBOOLE_1: 45;

                (A \ {O}) c= Y by A27, XBOOLE_1: 33;

                then

                 A31: (Z \ {O}) c= Y by XBOOLE_1: 40;

                 not O in Z by A21, A22, XBOOLE_0:def 5;

                then

                 A32: Z c= Y by A31, ZFMISC_1: 57;

                Y c= ((O \/ {O}) \ {O}) by A26, XBOOLE_1: 33;

                then Y c= (O \ {O}) by XBOOLE_1: 40;

                then Y c= O by A17, ZFMISC_1: 57;

                then Y in X2 by A14, A26;

                hence thesis by A19, A30, A32;

              end;

              now

                assume

                 A33: not O in B;

                O in {O} by TARSKI:def 1;

                then O in A by XBOOLE_0:def 3;

                hence contradiction by A27, A33;

              end;

              hence thesis by A28;

            end;

            hence thesis by A25;

          end;

          now

            assume

             A34: not (Z \/ {O}) in X;

            take A = Z;

            now

              assume O in X1;

              

              then X1 = (X1 \/ {O}) by ZFMISC_1: 40

              .= (Z \/ {O}) by A21, XBOOLE_1: 39;

              hence contradiction by A20, A34;

            end;

            then

             A35: A in X by A20, A21, ZFMISC_1: 57;

            for B be set st B in X holds A c= B implies B = A

            proof

              let B;

              assume

               A36: B in X;

              then (B \ {O}) c= ((O \/ {O}) \ {O}) by XBOOLE_1: 33;

              then (B \ {O}) c= (O \ {O}) by XBOOLE_1: 40;

              then (B \ {O}) c= O by A17, ZFMISC_1: 57;

              then

               A37: (B \ {O}) in X2 by A14, A36;

              assume

               A38: A c= B;

              then (A \ {O}) c= (B \ {O}) by XBOOLE_1: 33;

              then

               A39: A c= (B \ {O}) by A23, ZFMISC_1: 57;

               A40:

              now

                assume

                 A41: O in B;

                (A \/ {O}) = ((B \ {O}) \/ {O}) by A19, A37, A39

                .= (B \/ {O}) by XBOOLE_1: 39

                .= B by A41, ZFMISC_1: 40;

                hence contradiction by A34, A36;

              end;

              

               A42: B c= O

              proof

                let x be object such that

                 A43: x in B;

                x in O or x in {O} by A36, A43, XBOOLE_0:def 3;

                hence thesis by A40, A43, TARSKI:def 1;

              end;

              (B \ {O}) = B by A40, ZFMISC_1: 57;

              then B in X2 by A14, A36, A42;

              hence thesis by A19, A38;

            end;

            hence thesis by A35;

          end;

          hence thesis by A24;

        end;

      end;

      

       A44: O <> 0 & O is limit_ordinal & (for B be Ordinal st B in O holds P[B]) implies P[O]

      proof

        assume that

         A45: O <> 0 and

         A46: O is limit_ordinal and for B be Ordinal st B in O holds P[B] and

         A47: O in omega ;

         {} in O by A45, ORDINAL1: 14;

        then omega c= O by A46, ORDINAL1:def 11;

        then O in O by A47;

        hence thesis;

      end;

       P[O] from ORDINAL2:sch 1( A8, A10, A44);

      then

      consider g be set such that

       A48: g in GX and

       A49: for B be set st B in GX holds g c= B implies B = g by A4, A7;

      take (p .: g);

      for B st B in X holds (p .: g) c= B implies B = (p .: g)

      proof

        let B;

        assume

         A50: B in X;

        assume (p .: g) c= B;

        then

         A51: (p " (p .: g)) c= (p " B) by RELAT_1: 143;

        

         A52: g c= (p " (p .: g)) by A48, FUNCT_1: 76;

        

         A53: (p .: (p " B)) = B by A3, A50, FUNCT_1: 77;

        (p " B) c= ( dom p) by RELAT_1: 132;

        then (p " B) in GX by A5, A50, A53;

        hence thesis by A49, A51, A52, A53, XBOOLE_1: 1;

      end;

      hence thesis by A5, A48;

    end;

    scheme :: FINSET_1:sch2

    Finite { A() -> set , P[ set] } :

P[A()]

      provided

       A1: A() is finite

       and

       A2: P[ {} ]

       and

       A3: for x,B be set st x in A() & B c= A() & P[B] holds P[(B \/ {x})];

      now

        assume A() <> {} ;

        defpred R[ set] means ex B st B = $1 & P[B];

        consider G be set such that

         A4: for x holds x in G iff x in ( bool A()) & R[x] from XFAMILY:sch 1;

        G c= ( bool A()) by A4;

        then

        reconsider GA = G as Subset-Family of A();

         {} c= A();

        then GA <> {} by A2, A4;

        then

        consider B such that

         A5: B in GA and

         A6: for X be set st X in GA holds B c= X implies B = X by A1, Th6;

        

         A7: ex A st A = B & P[A] by A4, A5;

        now

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

          assume B <> A();

          then not A() c= B by A5;

          then

           A8: (A() \ B) <> {} by XBOOLE_1: 37;

          then

           A9: x in A() by XBOOLE_0:def 5;

          then

           A10: P[(B \/ {x})] by A3, A5, A7;

           {x} c= A() by A9, ZFMISC_1: 31;

          then (B \/ {x}) c= A() by A5, XBOOLE_1: 8;

          then

           A11: (B \/ {x}) in GA by A4, A10;

           not x in B by A8, XBOOLE_0:def 5;

          then not {x} c= B by ZFMISC_1: 31;

          then (B \/ {x}) <> B by XBOOLE_1: 7;

          hence contradiction by A6, A11, XBOOLE_1: 7;

        end;

        hence thesis by A7;

      end;

      hence thesis by A2;

    end;

    

     Lm3: A is finite & (for X st X in A holds X is finite) implies ( union A) is finite

    proof

      assume that

       A1: A is finite and

       A2: for X st X in A holds X is finite;

      defpred P[ set] means ex B st B = $1 & ( union B) is finite;

      consider G be set such that

       A3: for x holds x in G iff x in ( bool A) & P[x] from XFAMILY:sch 1;

      defpred P[ set] means $1 in G;

       {} c= A;

      then

       A4: P[ {} ] by A3, ZFMISC_1: 2;

      

       A5: for x,B be set st x in A & B c= A & P[B] holds P[(B \/ {x})]

      proof

        let x,B be set;

        assume that

         A6: x in A and B c= A and

         A7: B in G;

        

         A8: ex X st X = B & ( union X) is finite by A3, A7;

        

         A9: x is finite by A2, A6;

        

         A10: ( union (B \/ {x})) = (( union B) \/ ( union {x})) by ZFMISC_1: 78

        .= (( union B) \/ x) by ZFMISC_1: 25;

        

         A11: {x} c= A by A6, ZFMISC_1: 31;

        B in ( bool A) by A3, A7;

        then (B \/ {x}) c= A by A11, XBOOLE_1: 8;

        hence thesis by A3, A8, A9, A10;

      end;

       P[A] from Finite( A1, A4, A5);

      then ex X st X = A & ( union X) is finite by A3;

      hence thesis;

    end;

    registration

      let A,B be finite set;

      cluster [:A, B:] -> finite;

      coherence

      proof

        

         A1: for y holds [:A, {y}:] is finite

        proof

          let y;

          deffunc F( object) = [$1, y];

          consider f such that

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

          for x be object holds x in ( rng f) iff x in [:A, {y}:]

          proof

            let x be object;

            thus x in ( rng f) implies x in [:A, {y}:]

            proof

              assume x in ( rng f);

              then

              consider z be object such that

               A3: z in ( dom f) and

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

              x = [z, y] by A2, A3, A4;

              hence thesis by A2, A3, ZFMISC_1: 106;

            end;

            thus x in [:A, {y}:] implies x in ( rng f)

            proof

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

              then

              consider x1,x2 be object such that

               A5: x1 in A and

               A6: x2 in {y} and

               A7: x = [x1, x2] by ZFMISC_1:def 2;

              x2 = y by A6, TARSKI:def 1;

              then x = (f . x1) by A2, A5, A7;

              hence thesis by A2, A5, FUNCT_1:def 3;

            end;

          end;

          then ( rng f) = [:A, {y}:] by TARSKI: 2;

          then (f .: A) = [:A, {y}:] by A2, RELAT_1: 113;

          hence thesis;

        end;

        defpred P[ set] means ex y st y in B & $1 = [:A, {y}:];

        consider G be set such that

         A8: for x holds x in G iff x in ( bool [:A, B:]) & P[x] from XFAMILY:sch 1;

        for x be object holds x in ( union G) iff x in [:A, B:]

        proof

          let x be object;

          thus x in ( union G) implies x in [:A, B:]

          proof

            assume x in ( union G);

            then

            consider X such that

             A9: x in X and

             A10: X in G by TARSKI:def 4;

            X in ( bool [:A, B:]) by A8, A10;

            hence thesis by A9;

          end;

          assume x in [:A, B:];

          then

          consider y,z be object such that

           A11: y in A and

           A12: z in B and

           A13: x = [y, z] by ZFMISC_1:def 2;

          

           A14: [y, z] in [:A, {z}:] by A11, ZFMISC_1: 106;

           {z} c= B by A12, ZFMISC_1: 31;

          then [:A, {z}:] c= [:A, B:] by ZFMISC_1: 95;

          then [:A, {z}:] in G by A8, A12;

          hence thesis by A13, A14, TARSKI:def 4;

        end;

        then

         A15: ( union G) = [:A, B:] by TARSKI: 2;

        deffunc F( object) = [:A, {$1}:];

        consider g be Function such that

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

        for x be object holds x in ( rng g) iff x in G

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          thus x in ( rng g) implies x in G

          proof

            assume x in ( rng g);

            then

            consider y be object such that

             A17: y in ( dom g) and

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

            

             A19: x = [:A, {y}:] by A16, A17, A18;

             {y} c= B by A16, A17, ZFMISC_1: 31;

            then xx c= [:A, B:] by A19, ZFMISC_1: 95;

            hence thesis by A8, A16, A17, A19;

          end;

          assume x in G;

          then

          consider y such that

           A20: y in B and

           A21: x = [:A, {y}:] by A8;

          x = (g . y) by A16, A20, A21;

          hence thesis by A16, A20, FUNCT_1:def 3;

        end;

        then ( rng g) = G by TARSKI: 2;

        then

         A22: (g .: B) = G by A16, RELAT_1: 113;

        for X st X in G holds X is finite

        proof

          let X;

          assume X in G;

          then ex y st y in B & X = [:A, {y}:] by A8;

          hence thesis by A1;

        end;

        hence thesis by A15, A22, Lm3;

      end;

    end

    registration

      let A,B,C be finite set;

      cluster [:A, B, C:] -> finite;

      coherence

      proof

         [: [:A, B:], C:] is finite;

        hence thesis by ZFMISC_1:def 3;

      end;

    end

    registration

      let A,B,C,D be finite set;

      cluster [:A, B, C, D:] -> finite;

      coherence

      proof

         [: [:A, B, C:], D:] is finite;

        hence thesis by ZFMISC_1:def 4;

      end;

    end

    registration

      let A be finite set;

      cluster ( bool A) -> finite;

      coherence

      proof

        

         A1: A is finite;

        defpred P[ set] means ( bool $1) is finite;

        consider G be set such that

         A2: for x holds x in G iff x in ( bool A) & P[x] from XFAMILY:sch 1;

        defpred P[ set] means $1 in G;

        

         A3: ( bool {} ) is finite by ZFMISC_1: 1;

         {} c= A;

        then

         A4: P[ {} ] by A3, A2;

        

         A5: for x,B be set st x in A & B c= A & P[B] holds P[(B \/ {x})]

        proof

          let x,B be set;

          assume that

           A6: x in A and B c= A and

           A7: B in G;

          

           A8: x in B implies thesis by A7, XBOOLE_1: 12, ZFMISC_1: 31;

          now

            assume

             A9: not x in B;

            defpred P[ object, object] means ex Y st Y = $1 & $2 = (Y \/ {x});

            

             A10: for y,y1,y2 be object st y in ( bool B) & P[y, y1] & P[y, y2] holds y1 = y2;

            

             A11: for y be object st y in ( bool B) holds ex z be object st P[y, z]

            proof

              let y be object such that y in ( bool B);

              reconsider y as set by TARSKI: 1;

              ex Y st Y = y & (y \/ {x}) = (Y \/ {x});

              hence thesis;

            end;

            consider f such that

             A12: ( dom f) = ( bool B) and

             A13: for y be object st y in ( bool B) holds P[y, (f . y)] from FUNCT_1:sch 2( A10, A11);

            

             A14: ( bool B) is finite by A2, A7;

            for y be object holds y in ( rng f) iff y in (( bool (B \/ {x})) \ ( bool B))

            proof

              let y be object;

              reconsider yy = y as set by TARSKI: 1;

              thus y in ( rng f) implies y in (( bool (B \/ {x})) \ ( bool B))

              proof

                assume y in ( rng f);

                then

                consider x1 be object such that

                 A15: x1 in ( dom f) and

                 A16: (f . x1) = y by FUNCT_1:def 3;

                consider X1 be set such that

                 A17: X1 = x1 and

                 A18: (f . x1) = (X1 \/ {x}) by A12, A13, A15;

                

                 A19: (X1 \/ {x}) c= (B \/ {x}) by A12, A15, A17, XBOOLE_1: 13;

                x in {x} by TARSKI:def 1;

                then x in yy by A16, A18, XBOOLE_0:def 3;

                then not y in ( bool B) by A9;

                hence thesis by A16, A18, A19, XBOOLE_0:def 5;

              end;

              assume

               A20: y in (( bool (B \/ {x})) \ ( bool B));

              set Z = (yy \ {x});

               A21:

              now

                assume

                 A22: not x in yy;

                yy c= B

                proof

                  let z be object;

                  assume

                   A23: z in yy;

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

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

                end;

                hence contradiction by A20, XBOOLE_0:def 5;

              end;

              

               A24: Z c= B by A20, XBOOLE_1: 43;

              then

              consider X such that

               A25: X = Z and

               A26: (f . Z) = (X \/ {x}) by A13;

              (X \/ {x}) = (yy \/ {x}) by A25, XBOOLE_1: 39

              .= y by A21, ZFMISC_1: 40;

              hence thesis by A12, A24, A26, FUNCT_1:def 3;

            end;

            then ( rng f) = (( bool (B \/ {x})) \ ( bool B)) by TARSKI: 2;

            then

             A27: (f .: ( bool B)) = (( bool (B \/ {x})) \ ( bool B)) by A12, RELAT_1: 113;

            

             A28: ( bool B) c= ( bool (B \/ {x})) by XBOOLE_1: 7, ZFMISC_1: 67;

            

             A29: ((( bool (B \/ {x})) \ ( bool B)) \/ ( bool B)) = (( bool (B \/ {x})) \/ ( bool B)) by XBOOLE_1: 39

            .= ( bool (B \/ {x})) by A28, XBOOLE_1: 12;

            

             A30: {x} c= A by A6, ZFMISC_1: 31;

            B in ( bool A) by A2, A7;

            then (B \/ {x}) c= A by A30, XBOOLE_1: 8;

            hence thesis by A2, A14, A27, A29;

          end;

          hence thesis by A8;

        end;

         P[A] from Finite( A1, A4, A5);

        hence thesis by A2;

      end;

    end

    theorem :: FINSET_1:7

    

     Th7: A is finite & (for X st X in A holds X is finite) iff ( union A) is finite

    proof

      thus A is finite & (for X st X in A holds X is finite) implies ( union A) is finite by Lm3;

      thus ( union A) is finite implies A is finite & for X st X in A holds X is finite

      proof

        assume

         A1: ( union A) is finite;

        A c= ( bool ( union A)) by ZFMISC_1: 82;

        hence A is finite by A1;

        let X;

        assume X in A;

        then X c= ( union A) by ZFMISC_1: 74;

        hence thesis by A1;

      end;

    end;

    theorem :: FINSET_1:8

    

     Th8: ( dom f) is finite implies ( rng f) is finite

    proof

      assume ( dom f) is finite;

      then (f .: ( dom f)) is finite;

      hence thesis by RELAT_1: 113;

    end;

    theorem :: FINSET_1:9

    Y c= ( rng f) & (f " Y) is finite implies Y is finite

    proof

      assume Y c= ( rng f);

      then (f .: (f " Y)) = Y by FUNCT_1: 77;

      hence thesis;

    end;

    registration

      let X,Y be finite set;

      cluster (X \+\ Y) -> finite;

      coherence ;

    end

    registration

      let X be set;

      cluster finite for Subset of X;

      existence

      proof

        take IT = ( {} X);

        thus IT is finite;

      end;

    end

    registration

      let X be non empty set;

      cluster finite non empty for Subset of X;

      existence

      proof

        take { the Element of X};

        thus thesis;

      end;

    end

    begin

    theorem :: FINSET_1:10

    

     Th10: for f be Function holds ( dom f) is finite iff f is finite

    proof

      let f be Function;

      thus ( dom f) is finite implies f is finite

      proof

        assume

         A1: ( dom f) is finite;

        then

         A2: ( rng f) is finite by Th8;

        f c= [:( dom f), ( rng f):] by RELAT_1: 7;

        hence thesis by A1, A2;

      end;

      (( pr1 (( dom f),( rng f))) .: f) = ( dom f) by FUNCT_3: 79;

      hence thesis;

    end;

    theorem :: FINSET_1:11

    for F be set st F is finite & F <> {} & F is c=-linear holds ex m be set st m in F & for C be set st C in F holds m c= C

    proof

      defpred P[ set] means $1 <> {} implies ex m be set st m in $1 & for C be set st C in $1 holds m c= C;

      let F be set such that

       A1: F is finite and

       A2: F <> {} and

       A3: F is c=-linear;

      

       A4: P[ {} ];

       A5:

      now

        let x,B be set such that

         A6: x in F and

         A7: B c= F and

         A8: P[B];

        now

          per cases ;

            suppose

             A9: not ex y be set st y in B & y c= x;

            assume (B \/ {x}) <> {} ;

            take m = x;

            x in {x} by TARSKI:def 1;

            hence m in (B \/ {x}) by XBOOLE_0:def 3;

            let C be set;

            assume C in (B \/ {x});

            then

             A10: C in B or C in {x} by XBOOLE_0:def 3;

            then (C,x) are_c=-comparable by A3, A6, A7, TARSKI:def 1;

            then C c= x or x c= C;

            hence m c= C by A9, A10, TARSKI:def 1;

          end;

            suppose ex y be set st y in B & y c= x;

            then

            consider y be set such that

             A11: y in B and

             A12: y c= x;

            assume (B \/ {x}) <> {} ;

            consider m be set such that

             A13: m in B and

             A14: for C be set st C in B holds m c= C by A8, A11;

            m c= y by A11, A14;

            then

             A15: m c= x by A12;

            take m;

            thus m in (B \/ {x}) by A13, XBOOLE_0:def 3;

            let C be set;

            assume C in (B \/ {x});

            then C in B or C in {x} by XBOOLE_0:def 3;

            hence m c= C by A14, A15, TARSKI:def 1;

          end;

        end;

        hence P[(B \/ {x})];

      end;

       P[F] from Finite( A1, A4, A5);

      hence thesis by A2;

    end;

    theorem :: FINSET_1:12

    for F be set st F is finite & F <> {} & F is c=-linear holds ex m be set st m in F & for C be set st C in F holds C c= m

    proof

      defpred P[ set] means $1 <> {} implies ex m be set st m in $1 & for C be set st C in $1 holds C c= m;

      let F be set such that

       A1: F is finite and

       A2: F <> {} and

       A3: F is c=-linear;

      

       A4: P[ {} ];

       A5:

      now

        let x,B be set such that

         A6: x in F and

         A7: B c= F and

         A8: P[B];

        now

          per cases ;

            suppose

             A9: not ex y be set st y in B & x c= y;

            assume (B \/ {x}) <> {} ;

            take m = x;

            x in {x} by TARSKI:def 1;

            hence m in (B \/ {x}) by XBOOLE_0:def 3;

            let C be set;

            assume C in (B \/ {x});

            then

             A10: C in B or C in {x} by XBOOLE_0:def 3;

            then (C,x) are_c=-comparable by A3, A6, A7, TARSKI:def 1;

            then C c= x or x c= C;

            hence C c= m by A9, A10, TARSKI:def 1;

          end;

            suppose ex y be set st y in B & x c= y;

            then

            consider y be set such that

             A11: y in B and

             A12: x c= y;

            assume (B \/ {x}) <> {} ;

            consider m be set such that

             A13: m in B and

             A14: for C be set st C in B holds C c= m by A8, A11;

            y c= m by A11, A14;

            then

             A15: x c= m by A12;

            take m;

            thus m in (B \/ {x}) by A13, XBOOLE_0:def 3;

            let C be set;

            assume C in (B \/ {x});

            then C in B or C in {x} by XBOOLE_0:def 3;

            hence C c= m by A14, A15, TARSKI:def 1;

          end;

        end;

        hence P[(B \/ {x})];

      end;

       P[F] from Finite( A1, A4, A5);

      hence thesis by A2;

    end;

    definition

      let R be Relation;

      :: FINSET_1:def2

      attr R is finite-yielding means

      : Def2: for x be set st x in ( rng R) holds x is finite;

    end

    reserve a for set;

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

    theorem :: FINSET_1:13

    X is finite & X c= [:Y, Z:] implies ex A,B be set st A is finite & A c= Y & B is finite & B c= Z & X c= [:A, B:]

    proof

      deffunc G( object) = ($1 `2 );

      assume that

       A1: X is finite and

       A2: X c= [:Y, Z:];

      consider f be Function such that

       A3: ( dom f) = X and

       A4: for a be object st a in X holds (f . a) = F(a) from FUNCT_1:sch 3;

      consider g be Function such that

       A5: ( dom g) = X and

       A6: for a be object st a in X holds (g . a) = G(a) from FUNCT_1:sch 3;

      take A = ( rng f), B = ( rng g);

      thus A is finite by A1, A3, Th8;

      thus A c= Y

      proof

        let a be object;

        assume a in A;

        then

        consider x be object such that

         A7: x in ( dom f) and

         A8: (f . x) = a by FUNCT_1:def 3;

        consider y,z be object such that

         A9: y in Y and z in Z and

         A10: x = [y, z] by A2, A3, A7, ZFMISC_1:def 2;

        (f . x) = (x `1 ) by A3, A4, A7

        .= y by A10;

        hence thesis by A8, A9;

      end;

      thus B is finite by A1, A5, Th8;

      thus B c= Z

      proof

        let a be object;

        assume a in B;

        then

        consider x be object such that

         A11: x in ( dom g) and

         A12: (g . x) = a by FUNCT_1:def 3;

        consider y,z be object such that y in Y and

         A13: z in Z and

         A14: x = [y, z] by A2, A5, A11, ZFMISC_1:def 2;

        (g . x) = (x `2 ) by A5, A6, A11

        .= z by A14;

        hence thesis by A12, A13;

      end;

      thus X c= [:A, B:]

      proof

        let a be object;

        assume

         A15: a in X;

        then

        consider x,y be object such that x in Y and y in Z and

         A16: a = [x, y] by A2, ZFMISC_1:def 2;

        

         A17: (g . a) = (a `2 ) by A6, A15

        .= y by A16;

        (f . a) = (a `1 ) by A4, A15

        .= x by A16;

        then

         A18: x in A by A3, A15, FUNCT_1:def 3;

        y in B by A5, A15, A17, FUNCT_1:def 3;

        hence thesis by A16, A18, ZFMISC_1: 87;

      end;

    end;

    theorem :: FINSET_1:14

    X is finite & X c= [:Y, Z:] implies ex A be set st A is finite & A c= Y & X c= [:A, Z:]

    proof

      assume that

       A1: X is finite and

       A2: X c= [:Y, Z:];

      consider f be Function such that

       A3: ( dom f) = X and

       A4: for a be object st a in X holds (f . a) = F(a) from FUNCT_1:sch 3;

      take A = ( rng f);

      thus A is finite by A1, A3, Th8;

      thus A c= Y

      proof

        let a be object;

        assume a in A;

        then

        consider x be object such that

         A5: x in ( dom f) and

         A6: (f . x) = a by FUNCT_1:def 3;

        consider y,z be object such that

         A7: y in Y and z in Z and

         A8: x = [y, z] by A2, A3, A5, ZFMISC_1:def 2;

        (f . x) = (x `1 ) by A3, A4, A5

        .= y by A8;

        hence thesis by A6, A7;

      end;

      thus X c= [:A, Z:]

      proof

        let a be object;

        assume

         A9: a in X;

        then

        consider x,y be object such that x in Y and

         A10: y in Z and

         A11: a = [x, y] by A2, ZFMISC_1:def 2;

        (f . a) = (a `1 ) by A4, A9

        .= x by A11;

        then x in A by A3, A9, FUNCT_1:def 3;

        hence thesis by A10, A11, ZFMISC_1: 87;

      end;

    end;

    registration

      cluster finite non empty for Function;

      existence

      proof

         { [ {} , {} ]} is Function;

        hence thesis;

      end;

    end

    registration

      let R be finite Relation;

      cluster ( dom R) -> finite;

      coherence

      proof

        consider f be Function such that

         A1: ( dom f) = R and

         A2: for x be object st x in R holds (f . x) = (x `1 ) from FUNCT_1:sch 3;

        now

          let x be object;

          thus x in ( rng f) implies ex y be object st [x, y] in R

          proof

            assume x in ( rng f);

            then

            consider a be object such that

             A3: a in ( dom f) and

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

            take (a `2 );

            

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

            x = (a `1 ) by A1, A2, A3, A4;

            hence thesis by A1, A3, A5;

          end;

          given y be object such that

           A6: [x, y] in R;

          (f . [x, y]) = ( [x, y] `1 ) by A2, A6

          .= x;

          hence x in ( rng f) by A1, A6, FUNCT_1: 3;

        end;

        then ( rng f) = ( dom R) by XTUPLE_0:def 12;

        hence thesis by A1, Th8;

      end;

    end

    registration

      let f be Function, g be finite Function;

      cluster (f * g) -> finite;

      coherence

      proof

        ( dom (f * g)) c= ( dom g) by RELAT_1: 25;

        hence thesis by Th10;

      end;

    end

    registration

      let A be finite set, B be set;

      cluster -> finite for Function of A, B;

      coherence

      proof

        let f be Function of A, B;

        ( dom f) is finite;

        hence thesis by Th10;

      end;

    end

    registration

      let x,y be object;

      cluster (x .--> y) -> finite;

      coherence ;

    end

    registration

      let R be finite Relation;

      cluster ( rng R) -> finite;

      coherence

      proof

        consider f be Function such that

         A1: ( dom f) = R and

         A2: for x be object st x in R holds (f . x) = (x `2 ) from FUNCT_1:sch 3;

        now

          let y be object;

          thus y in ( rng f) implies ex x be object st [x, y] in R

          proof

            assume y in ( rng f);

            then

            consider a be object such that

             A3: a in ( dom f) and

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

            take (a `1 );

            

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

            y = (a `2 ) by A1, A2, A3, A4;

            hence thesis by A1, A3, A5;

          end;

          given x be object such that

           A6: [x, y] in R;

          (f . [x, y]) = ( [x, y] `2 ) by A2, A6

          .= y;

          hence y in ( rng f) by A1, A6, FUNCT_1: 3;

        end;

        then ( rng f) = ( rng R) by XTUPLE_0:def 13;

        hence thesis by A1, Th8;

      end;

    end

    registration

      let f be finite Function, x be set;

      cluster (f " x) -> finite;

      coherence

      proof

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

        hence thesis;

      end;

    end

    registration

      let f,g be finite Function;

      cluster (f +* g) -> finite;

      coherence

      proof

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

        hence thesis by Th10;

      end;

    end

    definition

      let F be set;

      :: FINSET_1:def3

      attr F is centered means F <> {} & for G be set st G <> {} & G c= F & G is finite holds ( meet G) <> {} ;

    end

    definition

      let f be Function;

      :: original: finite-yielding

      redefine

      :: FINSET_1:def4

      attr f is finite-yielding means

      : Def4: for i be object st i in ( dom f) holds (f . i) is finite;

      compatibility

      proof

        hereby

          assume

           A1: f is finite-yielding;

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

          per cases ;

            suppose i in ( dom f);

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

            hence (f . i) is finite by A1;

          end;

            suppose not i in ( dom f);

            hence (f . i) is finite by FUNCT_1:def 2;

          end;

        end;

        assume

         A2: for i be object st i in ( dom f) holds (f . i) is finite;

        let i be set;

        assume i in ( rng f);

        then ex x be object st x in ( dom f) & i = (f . x) by FUNCT_1:def 3;

        hence thesis by A2;

      end;

    end

    definition

      let I be set;

      let IT be I -defined Function;

      :: original: finite-yielding

      redefine

      :: FINSET_1:def5

      attr IT is finite-yielding means for i be object st i in I holds (IT . i) is finite;

      compatibility

      proof

        hereby

          assume

           A1: IT is finite-yielding;

          let i be object such that i in I;

          per cases ;

            suppose i in ( dom IT);

            hence (IT . i) is finite by A1;

          end;

            suppose not i in ( dom IT);

            hence (IT . i) is finite by FUNCT_1:def 2;

          end;

        end;

        assume

         A2: for i be object st i in I holds (IT . i) is finite;

        let i be object;

        ( dom IT) c= I;

        hence thesis by A2;

      end;

    end

    theorem :: FINSET_1:15

    B is infinite implies not B in [:A, B:]

    proof

      assume that

       A1: B is infinite and

       A2: B in [:A, B:];

      ex x be object st x in A & B = [x, {x}] by A2, ZFMISC_1: 129;

      hence thesis by A1;

    end;

    registration

      let I be set, f be I -defined Function;

      cluster finiteI -definedf -compatible for Function;

      existence

      proof

        take {} ;

        thus thesis by FUNCT_1: 104, RELAT_1: 171;

      end;

    end

    registration

      let X,Y be set;

      cluster finiteX -definedY -valued for Function;

      existence

      proof

        take {} ;

        thus thesis by RELAT_1: 171;

      end;

    end

    registration

      let X,Y be non empty set;

      cluster X -definedY -valued non empty finite for Function;

      existence

      proof

        set x = the Element of X, y = the Element of Y;

        take F = (x .--> y);

        thus F is X -defined;

        thus F is Y -valued;

        thus thesis;

      end;

    end

    registration

      let A be set, F be finite Relation;

      cluster (A |` F) -> finite;

      coherence

      proof

        (A |` F) c= F by RELAT_1: 86;

        hence thesis;

      end;

    end

    registration

      let A be set, F be finite Relation;

      cluster (F | A) -> finite;

      coherence

      proof

        (F | A) c= F by RELAT_1: 59;

        hence thesis;

      end;

    end

    registration

      let A be finite set, F be Function;

      cluster (F | A) -> finite;

      coherence

      proof

        ( dom (F | A)) c= A by RELAT_1: 58;

        hence thesis by Th10;

      end;

    end

    registration

      let R be finite Relation;

      cluster ( field R) -> finite;

      coherence ;

    end

    registration

      cluster trivial -> finite for set;

      coherence

      proof

        let S be set such that

         A1: S is trivial;

        per cases by A1, ZFMISC_1: 131;

          suppose S is empty;

          hence thesis;

        end;

          suppose ex x be object st S = {x};

          hence thesis;

        end;

      end;

    end

    registration

      cluster infinite -> non trivial for set;

      coherence ;

    end

    registration

      let X be non trivial set;

      cluster finite non trivial for Subset of X;

      existence

      proof

        consider a1,a2 be object such that

         A1: a1 in X & a2 in X & a1 <> a2 by ZFMISC_1:def 10;

        reconsider A = {a1, a2} as Subset of X by A1, ZFMISC_1: 32;

        take A;

        thus A is finite;

        a1 in A & a2 in A by TARSKI:def 2;

        hence thesis by A1, ZFMISC_1:def 10;

      end;

    end

    registration

      let x,y,a,b be object;

      cluster ((x,y) --> (a,b)) -> finite;

      coherence ;

    end

    definition

      let A be set;

      :: FINSET_1:def6

      attr A is finite-membered means

      : Def6: for B be set st B in A holds B is finite;

    end

    registration

      cluster empty -> finite-membered for set;

      coherence ;

    end

    registration

      let A be finite-membered set;

      cluster -> finite for Element of A;

      coherence

      proof

        let B be Element of A;

        per cases ;

          suppose A is empty;

          hence thesis by SUBSET_1:def 1;

        end;

          suppose not A is empty;

          hence thesis by Def6;

        end;

      end;

    end

    registration

      cluster non empty finite finite-membered for set;

      existence

      proof

        take x = { { {} }};

        thus x is non empty finite;

        let y be set;

        thus thesis by TARSKI:def 1;

      end;

    end

    registration

      let X be finite set;

      cluster {X} -> finite-membered;

      coherence by TARSKI:def 1;

      cluster ( bool X) -> finite-membered;

      coherence ;

      let Y be finite set;

      cluster {X, Y} -> finite-membered;

      coherence by TARSKI:def 2;

    end

    registration

      let X be finite-membered set;

      cluster -> finite-membered for Subset of X;

      coherence ;

      let Y be finite-membered set;

      cluster (X \/ Y) -> finite-membered;

      coherence

      proof

        let x be set;

        assume x in (X \/ Y);

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

        hence thesis;

      end;

    end

    registration

      let X be finite finite-membered set;

      cluster ( union X) -> finite;

      coherence

      proof

        for x st x in X holds x is finite;

        hence thesis by Th7;

      end;

    end

    registration

      cluster non empty finite-yielding for Function;

      existence

      proof

        take F = ( { {} } .--> { {} });

        thus F is non empty;

        let x be object;

        assume x in { { {} }};

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

        hence (F . x) is finite by FUNCOP_1: 72;

      end;

      cluster empty -> finite-yielding for Relation;

      coherence ;

    end

    registration

      let F be finite-yielding Function, x be object;

      cluster (F . x) -> finite;

      coherence

      proof

        per cases ;

          suppose x in ( dom F);

          hence thesis by Def4;

        end;

          suppose not x in ( dom F);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let F be finite-yielding Relation;

      cluster ( rng F) -> finite-membered;

      coherence by Def2;

    end