hallmar1.miz



    begin

    theorem :: HALLMAR1:1

    

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

    proof

      let X,Y be finite set;

      ( card (X \/ Y)) = ((( card X) + ( card Y)) - ( card (X /\ Y))) by CARD_2: 45;

      hence thesis;

    end;

    scheme :: HALLMAR1:sch1

    Regr11 { n() -> Element of NAT , P[ set] } :

for k be Element of NAT st 1 <= k & k <= n() holds P[k]

      provided

       A1: P[n()] & n() >= 2

       and

       A2: for k be Element of NAT st 1 <= k & k < n() & P[(k + 1)] holds P[k];

      defpred X[ Nat] means 1 <= $1 & $1 <= n() & not P[$1];

      assume ex k be Element of NAT st X[k];

      then

       A3: ex k be Nat st X[k];

      

       A4: for l be Nat st X[l] holds l <= n();

      consider l be Nat such that

       A5: X[l] and

       A6: for n be Nat st X[n] holds n <= l from NAT_1:sch 6( A4, A3);

      

       A7: (l + 1) >= 1 by NAT_1: 12;

      

       A8: l < n() by A1, A5, XXREAL_0: 1;

      then

       A9: (l + 1) <= n() by NAT_1: 13;

       A10:

      now

        assume not P[(l + 1)];

        then (l + 1) <= l by A6, A9, A7;

        hence contradiction by XREAL_1: 29;

      end;

      l in NAT by ORDINAL1:def 12;

      hence contradiction by A2, A5, A8, A10;

    end;

    scheme :: HALLMAR1:sch2

    Regr2 { P[ set] } :

P[1]

      provided

       A1: ex n be Element of NAT st n > 1 & P[n]

       and

       A2: for k be Element of NAT st k >= 1 & P[(k + 1)] holds P[k];

      consider n be Element of NAT such that

       A3: n > 1 and

       A4: P[n] by A1;

      n >= (1 + 1) by A3, NAT_1: 13;

      then

       A5: P[n] & n >= 2 by A4;

      

       A6: for k be Element of NAT st 1 <= k & k < n & P[(k + 1)] holds P[k] by A2;

      for k be Element of NAT st 1 <= k & k <= n holds P[k] from Regr11( A5, A6);

      hence thesis by A3;

    end;

    registration

      let F be non empty set;

      cluster non empty non-empty for FinSequence of ( bool F);

      existence

      proof

        set x = the non empty Subset of F;

        take v = <*x*>;

        thus v is non empty;

        ( rng v) = {x} by FINSEQ_1: 39;

        then not {} in ( rng v) by TARSKI:def 1;

        hence thesis by RELAT_1:def 9;

      end;

    end

    theorem :: HALLMAR1:2

    

     Th2: for F be non empty set, f be non-empty FinSequence of ( bool F), i be Element of NAT st i in ( dom f) holds (f . i) <> {}

    proof

      let F be non empty set, f be non-empty FinSequence of ( bool F), i be Element of NAT ;

      assume

       A1: i in ( dom f);

      assume (f . i) = {} ;

      then {} in ( rng f) by A1, FUNCT_1: 3;

      hence thesis by RELAT_1:def 9;

    end;

    registration

      let F be finite set, A be FinSequence of ( bool F);

      let i be Element of NAT ;

      cluster (A . i) -> finite;

      coherence

      proof

        per cases ;

          suppose i in ( dom A);

          then (A . i) in ( bool F) by PARTFUN1: 4;

          hence thesis;

        end;

          suppose not i in ( dom A);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    begin

    definition

      let F be set;

      let A be FinSequence of ( bool F);

      let J be set;

      :: HALLMAR1:def1

      func union (A,J) -> set means

      : Def1: for x be object holds x in it iff ex j be set st j in J & j in ( dom A) & x in (A . j);

      existence

      proof

        defpred P[ object] means ex j be set st j in J & j in ( dom A) & $1 in (A . j);

        consider X be set such that

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

        take X;

        let x be object;

        thus x in X implies ex j be set st j in J & j in ( dom A) & x in (A . j) by A1;

        given j be set such that

         A2: j in J and

         A3: j in ( dom A) and

         A4: x in (A . j);

        ( rng A) c= ( bool F) & (A . j) in ( rng A) by A3, FINSEQ_1:def 4, FUNCT_1: 3;

        hence thesis by A1, A2, A3, A4;

      end;

      uniqueness

      proof

        defpred P[ object] means ex j be set st j in J & j in ( dom A) & $1 in (A . j);

        let A1,A2 be set such that

         A5: for x be object holds x in A1 iff ex j be set st j in J & j in ( dom A) & x in (A . j) and

         A6: for x be object holds x in A2 iff ex j be set st j in J & j in ( dom A) & x in (A . j);

        

         A7: for x be object holds x in A2 iff P[x] by A6;

        

         A8: for x be object holds x in A1 iff P[x] by A5;

        A1 = A2 from XBOOLE_0:sch 2( A8, A7);

        hence thesis;

      end;

    end

    theorem :: HALLMAR1:3

    

     Th3: for F be set, A be FinSequence of ( bool F), J be set holds ( union (A,J)) c= F

    proof

      let F be set, A be FinSequence of ( bool F), J be set;

      let x be object;

      assume x in ( union (A,J));

      then

      consider j be set such that j in J and

       A1: j in ( dom A) and

       A2: x in (A . j) by Def1;

      ( rng A) c= ( bool F) & (A . j) in ( rng A) by A1, FINSEQ_1:def 4, FUNCT_1: 3;

      hence thesis by A2;

    end;

    theorem :: HALLMAR1:4

    for F be finite set, A be FinSequence of ( bool F), J,K be set st J c= K holds ( union (A,J)) c= ( union (A,K))

    proof

      let F be finite set, A be FinSequence of ( bool F), J,K be set;

      assume

       A1: J c= K;

      thus ( union (A,J)) c= ( union (A,K))

      proof

        let a be object;

        assume a in ( union (A,J));

        then ex j be set st j in J & j in ( dom A) & a in (A . j) by Def1;

        hence thesis by A1, Def1;

      end;

    end;

    registration

      let F be finite set;

      let A be FinSequence of ( bool F);

      let J be set;

      cluster ( union (A,J)) -> finite;

      coherence by Th3, FINSET_1: 1;

    end

    theorem :: HALLMAR1:5

    

     Th5: for F be finite set, A be FinSequence of ( bool F), i be Element of NAT st i in ( dom A) holds ( union (A, {i})) = (A . i)

    proof

      let F be finite set, A be FinSequence of ( bool F), i be Element of NAT such that

       A1: i in ( dom A);

      thus ( union (A, {i})) c= (A . i)

      proof

        let x be object;

        assume x in ( union (A, {i}));

        then ex j be set st j in {i} & j in ( dom A) & x in (A . j) by Def1;

        hence thesis by TARSKI:def 1;

      end;

      thus (A . i) c= ( union (A, {i}))

      proof

        let x be object;

        

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

        assume x in (A . i);

        hence thesis by A1, A2, Def1;

      end;

    end;

    theorem :: HALLMAR1:6

    

     Th6: for F be finite set, A be FinSequence of ( bool F), i,j be Element of NAT st i in ( dom A) & j in ( dom A) holds ( union (A, {i, j})) = ((A . i) \/ (A . j))

    proof

      let F be finite set, A be FinSequence of ( bool F), i,j be Element of NAT such that

       A1: i in ( dom A) and

       A2: j in ( dom A);

      thus ( union (A, {i, j})) c= ((A . i) \/ (A . j))

      proof

        let x be object;

        assume x in ( union (A, {i, j}));

        then

        consider k be set such that

         A3: k in {i, j} & k in ( dom A) & x in (A . k) by Def1;

        per cases by A3, TARSKI:def 2;

          suppose k = i & k in ( dom A) & x in (A . k);

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose k = j & k in ( dom A) & x in (A . k);

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      thus ((A . i) \/ (A . j)) c= ( union (A, {i, j}))

      proof

        let x be object;

        assume

         A4: x in ((A . i) \/ (A . j));

        per cases by A4, XBOOLE_0:def 3;

          suppose

           A5: x in (A . i);

          i in {i, j} by TARSKI:def 2;

          hence thesis by A1, A5, Def1;

        end;

          suppose

           A6: x in (A . j);

          j in {i, j} by TARSKI:def 2;

          hence thesis by A2, A6, Def1;

        end;

      end;

    end;

    theorem :: HALLMAR1:7

    

     Th7: for J be set, F be finite set, A be FinSequence of ( bool F), i be Element of NAT st i in J & i in ( dom A) holds (A . i) c= ( union (A,J)) by Def1;

    theorem :: HALLMAR1:8

    

     Th8: for J be set, F be finite set, i be Element of NAT , A be FinSequence of ( bool F) st i in J & i in ( dom A) holds ( union (A,J)) = (( union (A,(J \ {i}))) \/ (A . i))

    proof

      let J be set;

      let F be finite set;

      let i be Element of NAT ;

      let A be FinSequence of ( bool F);

      assume i in J & i in ( dom A);

      then

       A1: (A . i) c= ( union (A,J)) by Th7;

      thus ( union (A,J)) c= (( union (A,(J \ {i}))) \/ (A . i))

      proof

        let x be object;

        assume x in ( union (A,J));

        then

        consider j be set such that

         A2: j in J and

         A3: j in ( dom A) and

         A4: x in (A . j) by Def1;

        per cases ;

          suppose i = j;

          hence thesis by A4, XBOOLE_0:def 3;

        end;

          suppose i <> j;

          then not j in {i} by TARSKI:def 1;

          then j in (J \ {i}) by A2, XBOOLE_0:def 5;

          then x in ( union (A,(J \ {i}))) by A3, A4, Def1;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      thus (( union (A,(J \ {i}))) \/ (A . i)) c= ( union (A,J))

      proof

        let x be object;

        assume x in (( union (A,(J \ {i}))) \/ (A . i));

        then

         A5: x in ( union (A,(J \ {i}))) or x in (A . i) by XBOOLE_0:def 3;

        per cases by A1, A5;

          suppose x in ( union (A,(J \ {i})));

          then ex j be set st j in (J \ {i}) & j in ( dom A) & x in (A . j) by Def1;

          hence thesis by Def1;

        end;

          suppose x in ( union (A,J));

          hence thesis;

        end;

      end;

    end;

    theorem :: HALLMAR1:9

    

     Th9: for J1,J2 be set, F be finite set, i be Element of NAT , A be FinSequence of ( bool F) st i in ( dom A) holds ( union (A,(( {i} \/ J1) \/ J2))) = ((A . i) \/ ( union (A,(J1 \/ J2))))

    proof

      let J1,J2 be set;

      let F be finite set;

      let i be Element of NAT ;

      let A be FinSequence of ( bool F);

      assume i in ( dom A);

      then

       A1: ( union (A, {i})) = (A . i) by Th5;

      thus ( union (A,(( {i} \/ J1) \/ J2))) c= ((A . i) \/ ( union (A,(J1 \/ J2))))

      proof

        let x be object;

        assume x in ( union (A,(( {i} \/ J1) \/ J2)));

        then

        consider j be set such that

         A2: j in (( {i} \/ J1) \/ J2) and

         A3: j in ( dom A) and

         A4: x in (A . j) by Def1;

        per cases ;

          suppose i = j;

          hence thesis by A4, XBOOLE_0:def 3;

        end;

          suppose

           A5: i <> j;

          j in ( {i} \/ (J1 \/ J2)) by A2, XBOOLE_1: 4;

          then j in {i} or j in (J1 \/ J2) by XBOOLE_0:def 3;

          then x in ( union (A,(J1 \/ J2))) by A3, A4, A5, Def1, TARSKI:def 1;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      thus ((A . i) \/ ( union (A,(J1 \/ J2)))) c= ( union (A,(( {i} \/ J1) \/ J2)))

      proof

        let x be object;

        assume

         A6: x in ((A . i) \/ ( union (A,(J1 \/ J2))));

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

          suppose x in ( union (A, {i}));

          then

          consider j be set such that

           A7: j in {i} and

           A8: j in ( dom A) & x in (A . j) by Def1;

          j in ( {i} \/ (J1 \/ J2)) by A7, XBOOLE_0:def 3;

          then j in (( {i} \/ J1) \/ J2) by XBOOLE_1: 4;

          hence thesis by A8, Def1;

        end;

          suppose x in ( union (A,(J1 \/ J2)));

          then

          consider j be set such that

           A9: j in (J1 \/ J2) and

           A10: j in ( dom A) & x in (A . j) by Def1;

          j in ( {i} \/ (J1 \/ J2)) by A9, XBOOLE_0:def 3;

          then j in (( {i} \/ J1) \/ J2) by XBOOLE_1: 4;

          hence thesis by A10, Def1;

        end;

      end;

    end;

    theorem :: HALLMAR1:10

    

     Th10: for F be finite set, A be FinSequence of ( bool F) holds for i be Element of NAT holds for x,y be set st x <> y & x in (A . i) & y in (A . i) holds (((A . i) \ {x}) \/ ((A . i) \ {y})) = (A . i)

    proof

      let F be finite set;

      let A be FinSequence of ( bool F);

      let i be Element of NAT ;

      let x,y be set such that

       A1: x <> y and

       A2: x in (A . i) and

       A3: y in (A . i);

      (A . i) c= (((A . i) \ {x}) \/ ((A . i) \ {y}))

      proof

         {} = ( {y} \ ( {y} \/ {} )) by XBOOLE_1: 46;

        then (A . i) = ((A . i) \ ( {y} \ {y}));

        then (A . i) = (((A . i) \ {y}) \/ ((A . i) /\ {y})) by XBOOLE_1: 52;

        then

         A4: (A . i) = (((A . i) \ {y}) \/ {y}) by A3, ZFMISC_1: 46;

        let z be object;

         not x in {y} by A1, TARSKI:def 1;

        then

         A5: x in ((A . i) \ {y}) by A2, XBOOLE_0:def 5;

        assume z in (A . i);

        then z in ((((A . i) \ {x}) \/ {x}) \/ (((A . i) \ {y}) \/ {y})) by A4, XBOOLE_0:def 3;

        then z in (((A . i) \ {x}) \/ ( {x} \/ ( {y} \/ ((A . i) \ {y})))) by XBOOLE_1: 4;

        then z in (((A . i) \ {x}) \/ (( {x} \/ {y}) \/ ((A . i) \ {y}))) by XBOOLE_1: 4;

        then z in ((((A . i) \ {x}) \/ ( {y} \/ {x})) \/ ((A . i) \ {y})) by XBOOLE_1: 4;

        then z in (((((A . i) \ {x}) \/ {y}) \/ {x}) \/ ((A . i) \ {y})) by XBOOLE_1: 4;

        then

         A6: z in ((((A . i) \ {x}) \/ {y}) \/ ( {x} \/ ((A . i) \ {y}))) by XBOOLE_1: 4;

         not y in {x} by A1, TARSKI:def 1;

        then y in ((A . i) \ {x}) by A3, XBOOLE_0:def 5;

        then z in (((A . i) \ {x}) \/ ( {x} \/ ((A . i) \ {y}))) by A6, ZFMISC_1: 40;

        hence thesis by A5, ZFMISC_1: 40;

      end;

      hence thesis;

    end;

    begin

    definition

      let F be finite set;

      let A be FinSequence of ( bool F);

      let i be Element of NAT ;

      let x be set;

      :: HALLMAR1:def2

      func Cut (A,i,x) -> FinSequence of ( bool F) means

      : Def2: ( dom it ) = ( dom A) & for k be Element of NAT st k in ( dom it ) holds (i = k implies (it . k) = ((A . k) \ {x})) & (i <> k implies (it . k) = (A . k));

      existence

      proof

        (A . i) c= F

        proof

          per cases ;

            suppose i in ( dom A);

            then (A . i) in ( bool F) by FINSEQ_2: 11;

            hence thesis;

          end;

            suppose not i in ( dom A);

            then (A . i) = {} by FUNCT_1:def 2;

            hence thesis;

          end;

        end;

        then

        reconsider EX = ((A . i) \ {x}) as Subset of F by XBOOLE_1: 1;

        set XX = (A +* (i,EX));

        reconsider XX as FinSequence of ( bool F);

        take XX;

        ( dom XX) = ( dom A) by FUNCT_7: 30;

        hence thesis by FUNCT_7: 31, FUNCT_7: 32;

      end;

      uniqueness

      proof

        let f1,f2 be FinSequence of ( bool F);

        assume that

         A1: ( dom f1) = ( dom A) and

         A2: for k be Element of NAT st k in ( dom f1) holds (i = k implies (f1 . k) = ((A . k) \ {x})) & (i <> k implies (f1 . k) = (A . k)) and

         A3: ( dom f2) = ( dom A) and

         A4: for k be Element of NAT st k in ( dom f2) holds (i = k implies (f2 . k) = ((A . k) \ {x})) & (i <> k implies (f2 . k) = (A . k));

        for z be Nat st z in ( dom f1) holds (f1 . z) = (f2 . z)

        proof

          let z be Nat;

          assume

           A5: z in ( dom f1);

          per cases ;

            suppose

             A6: z = i;

            

            then (f1 . z) = ((A . i) \ {x}) by A2, A5

            .= (f2 . z) by A1, A3, A4, A5, A6;

            hence thesis;

          end;

            suppose

             A7: z <> i;

            

            then (f1 . z) = (A . z) by A2, A5

            .= (f2 . z) by A1, A3, A4, A5, A7;

            hence thesis;

          end;

        end;

        hence thesis by A1, A3, FINSEQ_1: 13;

      end;

    end

    theorem :: HALLMAR1:11

    

     Th11: for F be finite set, A be FinSequence of ( bool F), i be Element of NAT , x be set st i in ( dom A) & x in (A . i) holds ( card (( Cut (A,i,x)) . i)) = (( card (A . i)) - 1)

    proof

      let F be finite set, A be FinSequence of ( bool F), i be Element of NAT , x be set;

      set f = ( Cut (A,i,x));

      assume that

       A1: i in ( dom A) and

       A2: x in (A . i);

      i in ( dom f) by A1, Def2;

      then

       A3: (f . i) = ((A . i) \ {x}) by Def2;

       {x} c= (A . i) by A2, ZFMISC_1: 31;

      

      then ( card (f . i)) = (( card (A . i)) - ( card {x})) by A3, CARD_2: 44

      .= (( card (A . i)) - 1) by CARD_2: 42;

      hence thesis;

    end;

    theorem :: HALLMAR1:12

    

     Th12: for F be finite set, A be FinSequence of ( bool F), i be Element of NAT , x,J be set holds ( union (( Cut (A,i,x)),(J \ {i}))) = ( union (A,(J \ {i})))

    proof

      let F be finite set, A be FinSequence of ( bool F), i be Element of NAT , x,J be set;

      thus ( union (( Cut (A,i,x)),(J \ {i}))) c= ( union (A,(J \ {i})))

      proof

        let z be object;

        assume z in ( union (( Cut (A,i,x)),(J \ {i})));

        then

        consider j be set such that

         A1: j in (J \ {i}) and

         A2: j in ( dom ( Cut (A,i,x))) and

         A3: z in (( Cut (A,i,x)) . j) by Def1;

         not j in {i} by A1, XBOOLE_0:def 5;

        then i <> j by TARSKI:def 1;

        then

         A4: z in (A . j) by A2, A3, Def2;

        j in ( dom A) by A2, Def2;

        hence thesis by A1, A4, Def1;

      end;

      

       A5: ( dom ( Cut (A,i,x))) = ( dom A) by Def2;

      thus ( union (A,(J \ {i}))) c= ( union (( Cut (A,i,x)),(J \ {i})))

      proof

        let z be object;

        assume z in ( union (A,(J \ {i})));

        then

        consider j be set such that

         A6: j in (J \ {i}) and

         A7: j in ( dom A) and

         A8: z in (A . j) by Def1;

         not j in {i} by A6, XBOOLE_0:def 5;

        then i <> j by TARSKI:def 1;

        then (( Cut (A,i,x)) . j) = (A . j) by A5, A7, Def2;

        hence thesis by A5, A6, A7, A8, Def1;

      end;

    end;

    theorem :: HALLMAR1:13

    

     Th13: for F be finite set, A be FinSequence of ( bool F), i be Element of NAT , x,J be set st not i in J holds ( union (A,J)) = ( union (( Cut (A,i,x)),J))

    proof

      let F be finite set, A be FinSequence of ( bool F), i be Element of NAT , x,J be set;

      assume

       A1: not i in J;

      thus ( union (A,J)) c= ( union (( Cut (A,i,x)),J))

      proof

        let z be object;

        assume z in ( union (A,J));

        then

        consider j be set such that

         A2: j in J and

         A3: j in ( dom A) and

         A4: z in (A . j) by Def1;

        

         A5: j in ( dom ( Cut (A,i,x))) by A3, Def2;

        per cases ;

          suppose i = j;

          hence thesis by A1, A2;

        end;

          suppose i <> j;

          then (( Cut (A,i,x)) . j) = (A . j) by A5, Def2;

          hence thesis by A2, A4, A5, Def1;

        end;

      end;

      let z be object;

      assume z in ( union (( Cut (A,i,x)),J));

      then

      consider j be set such that

       A6: j in J and

       A7: j in ( dom ( Cut (A,i,x))) and

       A8: z in (( Cut (A,i,x)) . j) by Def1;

      

       A9: j in ( dom A) by A7, Def2;

      per cases ;

        suppose i = j;

        hence thesis by A1, A6;

      end;

        suppose i <> j;

        then (( Cut (A,i,x)) . j) = (A . j) by A7, Def2;

        hence thesis by A6, A8, A9, Def1;

      end;

    end;

    theorem :: HALLMAR1:14

    

     Th14: for F be finite set, A be FinSequence of ( bool F), i be Element of NAT , x,J be set st i in ( dom ( Cut (A,i,x))) & i in J holds ( union (( Cut (A,i,x)),J)) = (( union (A,(J \ {i}))) \/ ((A . i) \ {x}))

    proof

      let F be finite set, A be FinSequence of ( bool F), i be Element of NAT , x,J be set such that

       A1: i in ( dom ( Cut (A,i,x))) and

       A2: i in J;

      ( union (( Cut (A,i,x)),J)) = (( union (( Cut (A,i,x)),(J \ {i}))) \/ (( Cut (A,i,x)) . i)) by A1, A2, Th8

      .= (( union (A,(J \ {i}))) \/ (( Cut (A,i,x)) . i)) by Th12

      .= (( union (A,(J \ {i}))) \/ ((A . i) \ {x})) by A1, Def2;

      hence thesis;

    end;

    begin

    definition

      let F be finite set;

      let X be FinSequence of ( bool F);

      let A be set;

      :: HALLMAR1:def3

      pred A is_a_system_of_different_representatives_of X means ex f be FinSequence of F st f = A & ( dom X) = ( dom f) & (for i be Element of NAT st i in ( dom f) holds (f . i) in (X . i)) & f is one-to-one;

    end

    definition

      let F be finite set;

      let A be FinSequence of ( bool F);

      :: HALLMAR1:def4

      attr A is Hall means for J be finite set st J c= ( dom A) holds ( card J) <= ( card ( union (A,J)));

    end

    registration

      let F be finite non empty set;

      cluster Hall non empty for FinSequence of ( bool F);

      existence

      proof

        set c = the Element of F;

        reconsider b = {c} as Element of ( bool F) by ZFMISC_1: 31;

        reconsider f = <*b*> as FinSequence of ( bool F);

        for J be finite set st J c= ( dom f) holds ( card J) <= ( card ( union (f,J)))

        proof

          let J be finite set;

          assume

           A1: J c= ( dom f);

          

           A2: ( dom f) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

          then

           A3: J = {} or J = {1} by A1, ZFMISC_1: 33;

          per cases by A3;

            suppose J = {} ;

            then ( card J) = 0 ;

            hence thesis by NAT_1: 2;

          end;

            suppose

             A4: J = {1};

            1 in ( dom f) & 1 in NAT by A2, TARSKI:def 1;

            

            then ( union (f, {1})) = (f . 1) by Th5

            .= b by FINSEQ_1: 40;

            then ( card ( union (f,J))) = 1 by A4, CARD_1: 30;

            hence thesis by A4, CARD_1: 30;

          end;

        end;

        then f is Hall;

        hence thesis;

      end;

    end

    registration

      let F be finite set;

      cluster Hall for FinSequence of ( bool F);

      existence

      proof

        reconsider f = ( <*> ( bool F)) as FinSequence of ( bool F);

        for J be finite set st J c= ( dom f) holds ( card J) <= ( card ( union (f,J)))

        proof

          let J be finite set;

          assume J c= ( dom f);

          then ( card J) = 0 ;

          hence thesis by NAT_1: 2;

        end;

        then

         A1: f is Hall;

        take f;

        thus thesis by A1;

      end;

    end

    theorem :: HALLMAR1:15

    

     Th15: for F be finite set, A be non empty FinSequence of ( bool F) st A is Hall holds A is non-empty

    proof

      let F be finite set, A be non empty FinSequence of ( bool F);

      assume

       A1: A is Hall;

      assume A is non non-empty;

      then {} in ( rng A) by RELAT_1:def 9;

      then

      consider i be object such that

       A2: i in ( dom A) & (A . i) = {} by FUNCT_1:def 3;

      set J = {i};

      

       A3: ( card J) = 1 by CARD_2: 42;

      J c= ( dom A) & ( card ( union (A,J))) = 0 by A2, Th5, CARD_1: 27, ZFMISC_1: 31;

      hence thesis by A1, A3;

    end;

    registration

      let F be finite set;

      cluster Hall -> non-empty for non empty FinSequence of ( bool F);

      coherence by Th15;

    end

    theorem :: HALLMAR1:16

    

     Th16: for F be finite set, A be FinSequence of ( bool F), i be Element of NAT st i in ( dom A) & A is Hall holds ( card (A . i)) >= 1

    proof

      let F be finite set, A be FinSequence of ( bool F), i be Element of NAT ;

      assume that

       A1: i in ( dom A) and

       A2: A is Hall;

      set J = {i};

      J c= ( dom A) by A1, ZFMISC_1: 31;

      then

       A3: ( card J) <= ( card ( union (A,J))) by A2;

      assume

       A4: ( card (A . i)) < 1;

      ( union (A,J)) = (A . i) by A1, Th5;

      hence thesis by A4, A3, CARD_2: 42;

    end;

    theorem :: HALLMAR1:17

    

     Th17: for F be non empty finite set, A be non empty FinSequence of ( bool F) st (for i be Element of NAT st i in ( dom A) holds ( card (A . i)) = 1) & A is Hall holds ex X be set st X is_a_system_of_different_representatives_of A

    proof

      let F be non empty finite set, A be non empty FinSequence of ( bool F);

      assume

       A1: for i be Element of NAT st i in ( dom A) holds ( card (A . i)) = 1;

      reconsider dA = ( dom A) as non empty set;

      deffunc F( Element of dA) = (A . $1);

      assume

       A2: A is Hall;

      

       A3: for a be Element of dA holds F meets F(a)

      proof

        let a be Element of dA;

        set z = the Element of (A . a);

        (A . a) <> {} by A2;

        then

         A4: z in (A . a);

        ( rng A) c= ( bool F) & (A . a) in ( rng A) by FINSEQ_1:def 4, FUNCT_1: 3;

        hence thesis by A4, XBOOLE_0: 3;

      end;

      ex f be Function of dA, F st for a be Element of dA holds (f . a) in F(a) from FUNCT_2:sch 10( A3);

      then

      consider f be Function of dA, F such that

       A5: for a be Element of dA holds (f . a) in F(a);

      

       A6: ( dom f) = ( dom A) by FUNCT_2:def 1;

      

       A7: ( rng f) c= F

      proof

        let x be object;

        

         A8: ( rng A) c= ( bool F) by FINSEQ_1:def 4;

        assume x in ( rng f);

        then

        consider y be object such that

         A9: y in ( dom f) and

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

        (f . y) in (A . y) & (A . y) in ( rng A) by A5, A6, A9, FUNCT_1: 3;

        hence thesis by A10, A8;

      end;

      ex n be Nat st ( dom A) = ( Seg n) by FINSEQ_1:def 2;

      then f is FinSequence by A6, FINSEQ_1:def 2;

      then

      reconsider f as FinSequence of F by A7, FINSEQ_1:def 4;

      

       A11: ( dom A) = ( dom f) by FUNCT_2:def 1;

      

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

      for i,j be Element of NAT st i in ( dom f) & j in ( dom f) & i <> j holds (f . i) <> (f . j)

      proof

        let i,j be Element of NAT ;

        assume that

         A13: i in ( dom f) and

         A14: j in ( dom f) and

         A15: i <> j;

        thus (f . i) <> (f . j)

        proof

          ( card (A . i)) = ( card { {} }) by A1, A12, A11, A13;

          then

          consider y be object such that

           A16: (A . i) = {y} by CARD_1: 29;

          

           A17: (A . i) = {(f . i)}

          proof

            thus (A . i) c= {(f . i)}

            proof

              let x be object;

              assume

               A18: x in (A . i);

              x = (f . i)

              proof

                (f . i) in (A . i) by A5, A6, A13;

                then

                 A19: (f . i) = y by A16, TARSKI:def 1;

                assume x <> (f . i);

                hence thesis by A16, A18, A19, TARSKI:def 1;

              end;

              hence thesis by TARSKI:def 1;

            end;

            let x be object;

            assume x in {(f . i)};

            then x = (f . i) by TARSKI:def 1;

            hence thesis by A5, A6, A13;

          end;

          

           A20: j in ( dom A) by A14, FUNCT_2:def 1;

          then ( card (A . j)) = ( card { {} }) by A1, A12;

          then

          consider z be object such that

           A21: (A . j) = {z} by CARD_1: 29;

          

           A22: (A . j) = {(f . j)}

          proof

            thus (A . j) c= {(f . j)}

            proof

              let x be object;

              assume

               A23: x in (A . j);

              x = (f . j)

              proof

                (f . j) in (A . j) by A5, A6, A14;

                then

                 A24: (f . j) = z by A21, TARSKI:def 1;

                assume x <> (f . j);

                hence thesis by A21, A23, A24, TARSKI:def 1;

              end;

              hence thesis by TARSKI:def 1;

            end;

            let x be object;

            assume x in {(f . j)};

            then x = (f . j) by TARSKI:def 1;

            hence thesis by A5, A6, A14;

          end;

          set J = {i, j};

          assume (f . i) = (f . j);

          then

           A25: {(f . i), (f . j)} = {(f . i)} by ENUMSET1: 29;

          

           A26: ( card J) = 2 by A15, CARD_2: 57;

          

           A27: i in ( dom A) by A13, FUNCT_2:def 1;

          then

           A28: J c= ( dom A) by A20, ZFMISC_1: 32;

          ( card ( union (A,J))) = ( card ((A . i) \/ (A . j))) by A27, A20, Th6

          .= ( card {(f . i), (f . j)}) by A17, A22, ENUMSET1: 1

          .= 1 by A25, CARD_1: 30;

          hence contradiction by A2, A26, A28;

        end;

      end;

      then for i,j be object st i in ( dom f) & j in ( dom f) & (f . i) = (f . j) holds i = j;

      then

       A29: f is one-to-one by FUNCT_1:def 4;

      for i be Element of NAT st i in ( dom f) holds (f . i) in (A . i) by A5, A6;

      then f is_a_system_of_different_representatives_of A by A11, A29;

      hence thesis;

    end;

    theorem :: HALLMAR1:18

    

     Th18: for F be finite set, A be FinSequence of ( bool F) holds (ex X be set st X is_a_system_of_different_representatives_of A) implies A is Hall

    proof

      let F be finite set, A be FinSequence of ( bool F);

      given X be set such that

       A1: X is_a_system_of_different_representatives_of A;

      consider f be FinSequence of F such that f = X and

       A2: ( dom A) = ( dom f) and

       A3: for i be Element of NAT st i in ( dom f) holds (f . i) in (A . i) and

       A4: f is one-to-one by A1;

      for J be finite set st J c= ( dom A) holds ( card J) <= ( card ( union (A,J)))

      proof

        let J be finite set;

        set X = J;

        set Y = ( union (A,J));

        set g = (f | X);

        assume

         A5: J c= ( dom A);

        then

         A6: ( dom g) = X by A2, RELAT_1: 62;

        

         A7: ( dom g) c= ( dom f) by RELAT_1: 60;

        

         A8: ( rng g) c= Y

        proof

          let x be object;

          assume x in ( rng g);

          then

          consider a be object such that

           A9: a in ( dom g) and

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

          a in ( dom f) by A7, A9;

          then

          reconsider a as Element of NAT ;

          (f . a) in (A . a) by A2, A3, A5, A6, A9;

          then (g . a) in (A . a) by A9, FUNCT_1: 47;

          hence thesis by A5, A6, A9, A10, Def1;

        end;

        g is one-to-one by A4, FUNCT_1: 52;

        then ( Segm ( card X)) c= ( Segm ( card Y)) by A6, A8, CARD_1: 10;

        hence thesis by NAT_1: 39;

      end;

      hence thesis;

    end;

    begin

    definition

      let F be set, A be FinSequence of ( bool F), i be Element of NAT ;

      :: HALLMAR1:def5

      mode Reduction of A,i -> FinSequence of ( bool F) means

      : Def5: ( dom it ) = ( dom A) & (for j be Element of NAT st j in ( dom A) & j <> i holds (A . j) = (it . j)) & (it . i) c= (A . i);

      existence

      proof

        take A;

        thus thesis;

      end;

    end

    definition

      let F be set, A be FinSequence of ( bool F);

      :: HALLMAR1:def6

      mode Reduction of A -> FinSequence of ( bool F) means

      : Def6: ( dom it ) = ( dom A) & for i be Element of NAT st i in ( dom A) holds (it . i) c= (A . i);

      existence

      proof

        for i be Element of NAT st i in ( dom A) holds (A . i) c= (A . i);

        hence thesis;

      end;

    end

    definition

      let F be set, A be FinSequence of ( bool F), i be Nat;

      assume that

       A1: i in ( dom A) and

       A2: (A . i) <> {} ;

      :: HALLMAR1:def7

      mode Singlification of A,i -> Reduction of A means

      : Def7: ( card (it . i)) = 1;

      existence

      proof

        set x = the Element of (A . i);

        (A . i) in ( bool F) & x in (A . i) by A1, A2, PARTFUN1: 4;

        then

        reconsider E = {x} as Subset of F by ZFMISC_1: 31;

        reconsider G = (A +* (i,E)) as FinSequence of ( bool F);

        

         A3: for j be Element of NAT st j in ( dom A) holds (G . j) c= (A . j)

        proof

          let j be Element of NAT ;

          assume j in ( dom A);

          per cases ;

            suppose

             A4: j = i;

            (G . i) = {x} by A1, FUNCT_7: 31;

            hence thesis by A2, A4, ZFMISC_1: 31;

          end;

            suppose j <> i;

            hence thesis by FUNCT_7: 32;

          end;

        end;

        (G . i) = {x} by A1, FUNCT_7: 31;

        then

         A5: ( card (G . i)) = 1 by CARD_2: 42;

        ( dom G) = ( dom A) by FUNCT_7: 30;

        then G is Reduction of A by A3, Def6;

        hence thesis by A5;

      end;

    end

    theorem :: HALLMAR1:19

    

     Th19: for F be finite set, A be FinSequence of ( bool F), i be Element of NAT , C be Reduction of A, i holds C is Reduction of A

    proof

      let F be finite set, A be FinSequence of ( bool F), i be Element of NAT , C be Reduction of A, i;

      

       A1: ( dom C) = ( dom A) by Def5;

      for j be Element of NAT st j in ( dom C) holds (C . j) c= (A . j)

      proof

        let j be Element of NAT ;

        assume

         A2: j in ( dom C);

        per cases ;

          suppose j = i;

          hence thesis by Def5;

        end;

          suppose j <> i;

          hence thesis by A1, A2, Def5;

        end;

      end;

      hence thesis by A1, Def6;

    end;

    theorem :: HALLMAR1:20

    

     Th20: for F be finite set, A be FinSequence of ( bool F), i be Element of NAT , x be set st i in ( dom A) holds ( Cut (A,i,x)) is Reduction of A, i

    proof

      let F be finite set, A be FinSequence of ( bool F), i be Element of NAT , x be set;

      set f = ( Cut (A,i,x));

      

       A1: ( dom f) = ( dom A) by Def2;

      then

       A2: for j be Element of NAT st j in ( dom A) & j <> i holds (A . j) = (f . j) by Def2;

      assume i in ( dom A);

      then (f . i) = ((A . i) \ {x}) by A1, Def2;

      hence thesis by A1, A2, Def5;

    end;

    theorem :: HALLMAR1:21

    

     Th21: for F be finite set, A be FinSequence of ( bool F), i be Element of NAT , x be set st i in ( dom A) holds ( Cut (A,i,x)) is Reduction of A

    proof

      let F be finite set, A be FinSequence of ( bool F), i be Element of NAT , x be set;

      assume i in ( dom A);

      then ( Cut (A,i,x)) is Reduction of A, i by Th20;

      hence thesis by Th19;

    end;

    theorem :: HALLMAR1:22

    

     Th22: for F be finite set, A be FinSequence of ( bool F), B be Reduction of A holds for C be Reduction of B holds C is Reduction of A

    proof

      let F be finite set, A be FinSequence of ( bool F), B be Reduction of A;

      let C be Reduction of B;

      

       A1: for i be Element of NAT st i in ( dom A) holds (C . i) c= (A . i)

      proof

        let i be Element of NAT ;

        assume

         A2: i in ( dom A);

        then i in ( dom B) by Def6;

        then

         A3: (C . i) c= (B . i) by Def6;

        (B . i) c= (A . i) by A2, Def6;

        hence thesis by A3;

      end;

      ( dom B) = ( dom C) by Def6;

      hence thesis by A1, Def6;

    end;

    theorem :: HALLMAR1:23

    for F be non empty finite set, A be non-empty FinSequence of ( bool F), i be Element of NAT , B be Singlification of A, i st i in ( dom A) holds (B . i) <> {}

    proof

      let F be non empty finite set, A be non-empty FinSequence of ( bool F), i be Element of NAT , B be Singlification of A, i;

      assume

       A1: i in ( dom A);

      then (A . i) <> {} by Th2;

      hence thesis by A1, Def7, CARD_1: 27;

    end;

    theorem :: HALLMAR1:24

    

     Th24: for F be non empty finite set, A be non-empty FinSequence of ( bool F), i,j be Element of NAT , B be Singlification of A, i, C be Singlification of B, j st i in ( dom A) & j in ( dom A) & (C . i) <> {} & (B . j) <> {} holds C is Singlification of A, j & C is Singlification of A, i

    proof

      let F be non empty finite set, A be non-empty FinSequence of ( bool F), i,j be Element of NAT , B be Singlification of A, i, C be Singlification of B, j;

      assume that

       A1: i in ( dom A) and

       A2: j in ( dom A) and

       A3: (C . i) <> {} and

       A4: (B . j) <> {} ;

      

       A5: ( dom B) = ( dom A) by Def6;

      then

       A6: (C . i) c= (B . i) by A1, Def6;

      

       A7: (A . i) <> {} by A1, Th2;

      then ( card (B . i)) = 1 by A1, Def7;

      then

       A8: ( card (C . i)) = 1 by A3, A6, NAT_1: 25, NAT_1: 43;

      

       A9: (A . j) <> {} by A2, Th2;

      

       A10: C is Reduction of A by Th22;

      ( card (C . j)) = 1 by A2, A4, A5, Def7;

      hence thesis by A1, A2, A7, A9, A10, A8, Def7;

    end;

    theorem :: HALLMAR1:25

    for F be set, A be FinSequence of ( bool F), i be Element of NAT holds A is Reduction of A, i

    proof

      let F be set, A be FinSequence of ( bool F), i be Element of NAT ;

      (for j be Element of NAT st j in ( dom A) & j <> i holds (A . j) = (A . j)) & (A . i) c= (A . i);

      hence thesis by Def5;

    end;

    theorem :: HALLMAR1:26

    

     Th26: for F be set, A be FinSequence of ( bool F) holds A is Reduction of A

    proof

      let F be set, A be FinSequence of ( bool F);

      for i be Element of NAT st i in ( dom A) holds (A . i) c= (A . i);

      hence thesis by Def6;

    end;

    definition

      let F be non empty set, A be FinSequence of ( bool F);

      assume

       A1: A is non-empty;

      :: HALLMAR1:def8

      mode Singlification of A -> Reduction of A means

      : Def8: for i be Element of NAT st i in ( dom A) holds ( card (it . i)) = 1;

      existence

      proof

        deffunc F( object) = { the Element of (A . $1)};

        

         A2: for x be object st x in ( dom A) holds F(x) in ( bool F)

        proof

          let x be object;

          assume

           A3: x in ( dom A);

          then (A . x) <> {} by A1, Th2;

          then

           A4: { the Element of (A . x)} c= (A . x) by ZFMISC_1: 31;

          (A . x) in ( bool F) by A3, PARTFUN1: 4;

          then { the Element of (A . x)} c= F by A4, XBOOLE_1: 1;

          hence thesis;

        end;

        ex f be Function of ( dom A), ( bool F) st for x be object st x in ( dom A) holds (f . x) = F(x) from FUNCT_2:sch 2( A2);

        then

        consider f be Function of ( dom A), ( bool F) such that

         A5: for x be object st x in ( dom A) holds (f . x) = F(x);

        

         A6: for i be Element of NAT st i in ( dom f) holds (f . i) = { the Element of (A . i)}

        proof

          let i be Element of NAT ;

          assume i in ( dom f);

          then i in ( dom A) by FUNCT_2:def 1;

          hence thesis by A5;

        end;

        

         A7: ( dom f) = ( dom A) by FUNCT_2:def 1;

        

         A8: for i be Element of NAT st i in ( dom A) holds (f . i) c= (A . i)

        proof

          let i be Element of NAT ;

          assume

           A9: i in ( dom A);

          then (A . i) <> {} by A1, Th2;

          then { the Element of (A . i)} c= (A . i) by ZFMISC_1: 31;

          hence thesis by A7, A6, A9;

        end;

        ( dom f) = ( dom A) by FUNCT_2:def 1

        .= ( Seg ( len A)) by FINSEQ_1:def 3;

        then

         A10: f is FinSequence by FINSEQ_1:def 2;

        ( rng f) c= ( bool F) by RELAT_1:def 19;

        then f is FinSequence of ( bool F) by A10, FINSEQ_1:def 4;

        then

        reconsider f as Reduction of A by A7, A8, Def6;

        for i be Element of NAT st i in ( dom A) holds ( card (f . i)) = 1

        proof

          let i be Element of NAT ;

          assume i in ( dom A);

          then i in ( dom f) by FUNCT_2:def 1;

          then (f . i) = { the Element of (A . i)} by A6;

          hence thesis by CARD_2: 42;

        end;

        hence thesis;

      end;

    end

    theorem :: HALLMAR1:27

    

     Th27: for F be non empty finite set, A be non empty non-empty FinSequence of ( bool F), f be Function holds f is Singlification of A iff (( dom f) = ( dom A) & for i be Element of NAT st i in ( dom A) holds f is Singlification of A, i)

    proof

      let F be non empty finite set, A be non empty non-empty FinSequence of ( bool F), f be Function;

      hereby

        assume f is Singlification of A;

        then

        reconsider f9 = f as Singlification of A;

        f9 is Reduction of A;

        hence ( dom f) = ( dom A) by Def6;

        let i be Element of NAT ;

        assume

         A1: i in ( dom A);

        then ( card (f9 . i)) = 1 & (A . i) <> {} by Def8;

        hence f is Singlification of A, i by A1, Def7;

      end;

      assume that

       A2: ( dom f) = ( dom A) and

       A3: for i be Element of NAT st i in ( dom A) holds f is Singlification of A, i;

      reconsider f as FinSequence of ( bool F) by A3, FINSEQ_5: 6;

      for i be Element of NAT st i in ( dom A) holds (f . i) c= (A . i)

      proof

        let i be Element of NAT ;

        assume

         A4: i in ( dom A);

        then f is Singlification of A, i by A3;

        hence thesis by A4, Def6;

      end;

      then

      reconsider f9 = f as Reduction of A by A2, Def6;

      for i be Element of NAT st i in ( dom A) holds ( card (f9 . i)) = 1

      proof

        let i be Element of NAT ;

        assume

         A5: i in ( dom A);

        then f is Singlification of A, i & (A . i) <> {} by A3;

        hence thesis by A5, Def7;

      end;

      hence thesis by Def8;

    end;

    registration

      let F be non empty finite set, A be non empty FinSequence of ( bool F), k be Element of NAT ;

      cluster -> non empty for Singlification of A, k;

      coherence

      proof

        let G be Singlification of A, k;

        ( dom G) = ( dom A) by Def6;

        hence thesis;

      end;

    end

    registration

      let F be non empty finite set, A be non empty FinSequence of ( bool F);

      cluster -> non empty for Singlification of A;

      coherence

      proof

        let G be Singlification of A;

        ( dom G) = ( dom A) by Def6;

        hence thesis;

      end;

    end

    begin

    theorem :: HALLMAR1:28

    

     Th28: for F be non empty finite set, A be non empty FinSequence of ( bool F), X be set, B be Reduction of A st X is_a_system_of_different_representatives_of B holds X is_a_system_of_different_representatives_of A

    proof

      let F be non empty finite set, A be non empty FinSequence of ( bool F), X be set, B be Reduction of A such that

       A1: X is_a_system_of_different_representatives_of B;

      X is_a_system_of_different_representatives_of A

      proof

        consider f be FinSequence of F such that

         A2: f = X and

         A3: ( dom B) = ( dom f) and

         A4: for i be Element of NAT st i in ( dom f) holds (f . i) in (B . i) and

         A5: f is one-to-one by A1;

        

         A6: for i be Element of NAT st i in ( dom f) holds (f . i) in (A . i)

        proof

          let i be Element of NAT such that

           A7: i in ( dom f);

          

           A8: (f . i) in (B . i) by A4, A7;

          ( dom B) = ( dom A) by Def6;

          then (B . i) c= (A . i) by A3, A7, Def6;

          hence thesis by A8;

        end;

        ( dom A) = ( dom B) by Def6;

        hence thesis by A2, A3, A5, A6;

      end;

      hence thesis;

    end;

    theorem :: HALLMAR1:29

    

     Th29: for F be finite set, A be FinSequence of ( bool F) st A is Hall holds for i be Element of NAT st ( card (A . i)) >= 2 holds ex x be set st x in (A . i) & ( Cut (A,i,x)) is Hall

    proof

      let F be finite set;

      let A be FinSequence of ( bool F) such that

       A1: A is Hall;

      let i be Element of NAT such that

       A2: ( card (A . i)) >= 2;

      ( Segm 2) c= ( Segm ( card (A . i))) by A2, NAT_1: 39;

      then

      reconsider Ai = (A . i) as non trivial finite set by PENCIL_1: 4;

      consider x,y be object such that

       A3: x in Ai and

       A4: y in Ai and

       A5: x <> y by ZFMISC_1:def 10;

      assume

       A6: for z be set st z in (A . i) holds not ( Cut (A,i,z)) is Hall;

      reconsider x, y as set by TARSKI: 1;

       not ( Cut (A,i,x)) is Hall by A3, A6;

      then

      consider JJ1 be finite set such that

       A7: JJ1 c= ( dom ( Cut (A,i,x))) and

       A8: ( card JJ1) > ( card ( union (( Cut (A,i,x)),JJ1)));

      ex J1 be finite set st not i in J1 & J1 c= ( dom ( Cut (A,i,x))) & ( card J1) >= ( card (( union (A,J1)) \/ ((A . i) \ {x})))

      proof

        per cases ;

          suppose

           A9: i in JJ1;

          set J1 = (JJ1 \ {i});

          

           A10: ( card J1) = (( card JJ1) - ( card {i})) by A9, EULER_1: 4

          .= (( card JJ1) - 1) by CARD_1: 30;

          

           A11: J1 c= ( dom ( Cut (A,i,x))) & {i} misses J1 by A7, XBOOLE_1: 79;

          ( union (( Cut (A,i,x)),JJ1)) = (( union (A,(JJ1 \ {i}))) \/ ((A . i) \ {x})) by A7, A9, Th14;

          then ( card J1) >= ( card (( union (A,J1)) \/ ((A . i) \ {x}))) by A8, A10, SPPOL_1: 1;

          hence thesis by A11, ZFMISC_1: 48;

        end;

          suppose

           A12: not i in JJ1;

          take J1 = JJ1;

          

           A13: J1 c= ( dom A) by A7, Def2;

          ( card J1) > ( card ( union (A,J1))) by A8, A12, Th13;

          hence thesis by A1, A13;

        end;

      end;

      then

      consider J1 be finite set such that

       A14: not i in J1 and

       A15: J1 c= ( dom ( Cut (A,i,x))) and

       A16: ( card J1) >= ( card (( union (A,J1)) \/ ((A . i) \ {x})));

       not ( Cut (A,i,y)) is Hall by A4, A6;

      then

      consider JJ2 be finite set such that

       A17: JJ2 c= ( dom ( Cut (A,i,y))) and

       A18: ( card JJ2) > ( card ( union (( Cut (A,i,y)),JJ2)));

      ex J2 be finite set st not i in J2 & J2 c= ( dom ( Cut (A,i,y))) & ( card J2) >= ( card (( union (A,J2)) \/ ((A . i) \ {y})))

      proof

        per cases ;

          suppose

           A19: i in JJ2;

          set J2 = (JJ2 \ {i});

          

           A20: ( card J2) = (( card JJ2) - ( card {i})) by A19, EULER_1: 4

          .= (( card JJ2) - 1) by CARD_1: 30;

          

           A21: J2 c= ( dom ( Cut (A,i,y))) & {i} misses J2 by A17, XBOOLE_1: 79;

          ( union (( Cut (A,i,y)),JJ2)) = (( union (A,(JJ2 \ {i}))) \/ ((A . i) \ {y})) by A17, A19, Th14;

          then ( card J2) >= ( card (( union (A,J2)) \/ ((A . i) \ {y}))) by A18, A20, SPPOL_1: 1;

          hence thesis by A21, ZFMISC_1: 48;

        end;

          suppose

           A22: not i in JJ2;

          set J2 = JJ2;

          take J2;

          

           A23: J2 c= ( dom A) by A17, Def2;

          ( card J2) > ( card ( union (A,J2))) by A18, A22, Th13;

          hence thesis by A1, A23;

        end;

      end;

      then

      consider J2 be finite set such that

       A24: not i in J2 and

       A25: J2 c= ( dom ( Cut (A,i,y))) and

       A26: ( card J2) >= ( card (( union (A,J2)) \/ ((A . i) \ {y})));

      reconsider L = ( {i} \/ (J1 \/ J2)) as finite set;

      

       A27: J2 c= ( dom A) by A25, Def2;

      (( union (A,(J1 \/ J2))) \/ Ai) c= ((( union (A,J1)) \/ (Ai \ {x})) \/ (( union (A,J2)) \/ (Ai \ {y})))

      proof

        let a be object;

        assume

         A28: a in (( union (A,(J1 \/ J2))) \/ Ai);

        per cases by A28, XBOOLE_0:def 3;

          suppose a in ( union (A,(J1 \/ J2)));

          then

          consider j be set such that

           A29: j in (J1 \/ J2) and

           A30: j in ( dom A) & a in (A . j) by Def1;

          j in J1 or j in J2 by A29, XBOOLE_0:def 3;

          then a in ( union (A,J1)) or a in ( union (A,J2)) by A30, Def1;

          then a in (( union (A,J1)) \/ ( union (A,J2))) by XBOOLE_0:def 3;

          then a in ((( union (A,J1)) \/ ( union (A,J2))) \/ ((Ai \ {x}) \/ (Ai \ {y}))) by XBOOLE_0:def 3;

          then a in (((( union (A,J1)) \/ ( union (A,J2))) \/ (Ai \ {x})) \/ (Ai \ {y})) by XBOOLE_1: 4;

          then a in (((( union (A,J1)) \/ (Ai \ {x})) \/ ( union (A,J2))) \/ (Ai \ {y})) by XBOOLE_1: 4;

          hence thesis by XBOOLE_1: 4;

        end;

          suppose a in Ai;

          then a in ((Ai \ {x}) \/ (Ai \ {y})) or a in ( union (A,J1)) or a in ( union (A,J2)) by A3, A4, A5, Th10;

          then a in (((Ai \ {x}) \/ (Ai \ {y})) \/ ( union (A,J1))) or a in ( union (A,J2)) by XBOOLE_0:def 3;

          then a in ((((Ai \ {x}) \/ (Ai \ {y})) \/ ( union (A,J1))) \/ ( union (A,J2))) by XBOOLE_0:def 3;

          then a in ((( union (A,J1)) \/ ( union (A,J2))) \/ ((Ai \ {x}) \/ (Ai \ {y}))) by XBOOLE_1: 4;

          then a in (((( union (A,J1)) \/ ( union (A,J2))) \/ (Ai \ {x})) \/ (Ai \ {y})) by XBOOLE_1: 4;

          then a in (((( union (A,J1)) \/ (Ai \ {x})) \/ ( union (A,J2))) \/ (Ai \ {y})) by XBOOLE_1: 4;

          hence thesis by XBOOLE_1: 4;

        end;

      end;

      then

       A31: ( card ((( union (A,J1)) \/ (Ai \ {x})) \/ (( union (A,J2)) \/ (Ai \ {y})))) >= ( card (( union (A,(J1 \/ J2))) \/ Ai)) by NAT_1: 43;

      ( union (A,(J1 /\ J2))) c= (( union (A,J1)) /\ ( union (A,J2)))

      proof

        let x be object;

        assume x in ( union (A,(J1 /\ J2)));

        then

        consider j be set such that

         A32: j in (J1 /\ J2) and

         A33: j in ( dom A) & x in (A . j) by Def1;

        j in J2 by A32, XBOOLE_0:def 4;

        then

         A34: x in ( union (A,J2)) by A33, Def1;

        j in J1 by A32, XBOOLE_0:def 4;

        then x in ( union (A,J1)) by A33, Def1;

        hence thesis by A34, XBOOLE_0:def 4;

      end;

      then ( card (( union (A,J1)) /\ ( union (A,J2)))) >= ( card ( union (A,(J1 /\ J2)))) by NAT_1: 43;

      then

       A35: (( card (( union (A,(J1 \/ J2))) \/ Ai)) + ( card (( union (A,J1)) /\ ( union (A,J2))))) >= (( card (Ai \/ ( union (A,(J1 \/ J2))))) + ( card ( union (A,(J1 /\ J2))))) by XREAL_1: 7;

      J1 c= ( dom A) by A15, Def2;

      then

       A36: (J1 \/ J2) c= ( dom A) by A27, XBOOLE_1: 8;

      

       A37: i in ( dom A) by A2, CARD_1: 27, FUNCT_1:def 2;

      then {i} c= ( dom A) by ZFMISC_1: 31;

      then L c= ( dom A) by A36, XBOOLE_1: 8;

      then ( card ( union (A,( {i} \/ (J1 \/ J2))))) >= ( card ( {i} \/ (J1 \/ J2))) by A1;

      then

       A38: ( card ( union (A,(( {i} \/ J1) \/ J2)))) >= ( card ( {i} \/ (J1 \/ J2))) by XBOOLE_1: 4;

       not i in (J1 \/ J2) by A14, A24, XBOOLE_0:def 3;

      then

       A39: ( card ( {i} \/ (J1 \/ J2))) = (( card {i}) + ( card (J1 \/ J2))) by CARD_2: 40, ZFMISC_1: 50;

      (J1 /\ J2) c= J1 & J1 c= ( dom A) by A15, Def2, XBOOLE_1: 17;

      then (J1 /\ J2) c= ( dom A);

      then

       A40: ( card ( union (A,(J1 /\ J2)))) >= ( card (J1 /\ J2)) by A1;

      set S2 = (( union (A,J2)) \/ ((A . i) \ {y}));

      set S1 = (( union (A,J1)) \/ ((A . i) \ {x}));

      (( card J1) + ( card J2)) >= (( card S1) + ( card S2)) by A16, A26, XREAL_1: 7;

      then

       A41: (( card J1) + ( card J2)) >= (( card ((( union (A,J1)) \/ (Ai \ {x})) \/ (( union (A,J2)) \/ (Ai \ {y})))) + ( card ((( union (A,J1)) \/ (Ai \ {x})) /\ (( union (A,J2)) \/ (Ai \ {y}))))) by Th1;

      (( union (A,J1)) /\ ( union (A,J2))) c= ((( union (A,J1)) \/ (Ai \ {x})) /\ (( union (A,J2)) \/ (Ai \ {y})))

      proof

        let a be object;

        assume

         A42: a in (( union (A,J1)) /\ ( union (A,J2)));

        then a in ( union (A,J2)) by XBOOLE_0:def 4;

        then

         A43: a in (( union (A,J2)) \/ (Ai \ {y})) by XBOOLE_0:def 3;

        a in ( union (A,J1)) by A42, XBOOLE_0:def 4;

        then a in (( union (A,J1)) \/ (Ai \ {x})) by XBOOLE_0:def 3;

        hence thesis by A43, XBOOLE_0:def 4;

      end;

      then ( card ((( union (A,J1)) \/ (Ai \ {x})) /\ (( union (A,J2)) \/ (Ai \ {y})))) >= ( card (( union (A,J1)) /\ ( union (A,J2)))) by NAT_1: 43;

      then (( card ((( union (A,J1)) \/ (Ai \ {x})) \/ (( union (A,J2)) \/ (Ai \ {y})))) + ( card ((( union (A,J1)) \/ (Ai \ {x})) /\ (( union (A,J2)) \/ (Ai \ {y}))))) >= (( card (( union (A,(J1 \/ J2))) \/ Ai)) + ( card (( union (A,J1)) /\ ( union (A,J2))))) by A31, XREAL_1: 7;

      then (( card J1) + ( card J2)) >= (( card (( union (A,(J1 \/ J2))) \/ Ai)) + ( card (( union (A,J1)) /\ ( union (A,J2))))) by A41, XXREAL_0: 2;

      then

       A44: (( card J1) + ( card J2)) >= (( card (Ai \/ ( union (A,(J1 \/ J2))))) + ( card ( union (A,(J1 /\ J2))))) by A35, XXREAL_0: 2;

      ( card ( union (A,(( {i} \/ J1) \/ J2)))) = ( card (Ai \/ ( union (A,(J1 \/ J2))))) by A37, Th9;

      then ( card (Ai \/ ( union (A,(J1 \/ J2))))) >= (1 + ( card (J1 \/ J2))) by A38, A39, CARD_1: 30;

      then

       A45: (( card (Ai \/ ( union (A,(J1 \/ J2))))) + ( card ( union (A,(J1 /\ J2))))) >= ((1 + ( card (J1 \/ J2))) + ( card (J1 /\ J2))) by A40, XREAL_1: 7;

      (( card (J1 \/ J2)) + ( card (J1 /\ J2))) = (( card J1) + ( card J2)) by Th1;

      then ((1 + ( card (J1 \/ J2))) + ( card (J1 /\ J2))) = (1 + (( card J1) + ( card J2)));

      hence thesis by A44, A45, NAT_1: 13;

    end;

    theorem :: HALLMAR1:30

    

     Th30: for F be finite set, A be FinSequence of ( bool F), i be Element of NAT st i in ( dom A) & A is Hall holds ex G be Singlification of A, i st G is Hall

    proof

      let F be finite set, A be FinSequence of ( bool F), i be Element of NAT such that

       A1: i in ( dom A) and

       A2: A is Hall;

      

       A3: (A . i) <> {} by A1, A2, Th16, CARD_1: 27;

      set n = ( card (A . i));

      

       A4: n >= 1 by A1, A2, Th16;

      defpred P[ Element of NAT ] means ex G be Reduction of A st G is Hall & ( card (G . i)) = $1;

      

       A5: A is Reduction of A by Th26;

      per cases by A4, XXREAL_0: 1;

        suppose n = 1;

        then A is Singlification of A, i by A1, A5, Def7, CARD_1: 27;

        hence thesis by A2;

      end;

        suppose

         A6: n > 1;

        

         A7: for k be Element of NAT st k >= 1 & P[(k + 1)] holds P[k]

        proof

          let k be Element of NAT ;

          assume that

           A8: k >= 1 and

           A9: P[(k + 1)];

          consider G be Reduction of A such that

           A10: G is Hall and

           A11: ( card (G . i)) = (k + 1) by A9;

          (1 + 1) <= (k + 1) by A8, XREAL_1: 6;

          then

          consider x be set such that

           A12: x in (G . i) and

           A13: ( Cut (G,i,x)) is Hall by A10, A11, Th29;

          set H = ( Cut (G,i,x));

          

           A14: ( dom G) = ( dom A) by Def6;

          then H is Reduction of G by A1, Th21;

          then

           A15: H is Reduction of A by Th22;

          ( card (H . i)) = ((k + 1) - 1) by A1, A11, A14, A12, Th11

          .= k;

          hence thesis by A13, A15;

        end;

        A is Reduction of A by Th26;

        then

         A16: ex n be Element of NAT st n > 1 & P[n] by A2, A6;

         P[1] from Regr2( A16, A7);

        then

        consider G be Reduction of A such that

         A17: G is Hall and

         A18: ( card (G . i)) = 1;

        G is Singlification of A, i by A1, A3, A18, Def7;

        hence thesis by A17;

      end;

    end;

    theorem :: HALLMAR1:31

    

     Th31: for F be non empty finite set, A be non empty FinSequence of ( bool F) st A is Hall holds ex G be Singlification of A st G is Hall

    proof

      let F be non empty finite set, A be non empty FinSequence of ( bool F);

      defpred P[ Nat] means $1 in ( dom A) implies ex g be Singlification of A, $1 st g is Hall & for k be Element of NAT st 1 <= k & k <= $1 holds g is Singlification of A, k;

      assume

       A1: A is Hall;

      then

       A2: A is non-empty;

      

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

      proof

        let k be Nat;

        assume

         A4: P[k];

        (k + 1) in ( dom A) implies ex g be Singlification of A, (k + 1) st g is Hall & for l be Element of NAT st 1 <= l & l <= (k + 1) holds g is Singlification of A, l

        proof

          assume

           A5: (k + 1) in ( dom A);

          per cases by A5, TAXONOM1: 1;

            suppose

             A6: k = 0 ;

            consider g be Singlification of A, (k + 1) such that

             A7: g is Hall by A1, A5, Th30;

            for l be Element of NAT st 1 <= l & l <= (k + 1) holds g is Singlification of A, l by A6, XXREAL_0: 1;

            hence thesis by A7;

          end;

            suppose

             A8: k in ( dom A);

            then

            consider g be Singlification of A, k such that

             A9: g is Hall and

             A10: for l be Element of NAT st 1 <= l & l <= k holds g is Singlification of A, l by A4;

            (k + 1) in ( dom g) by A5, Def6;

            then

            consider G be Singlification of g, (k + 1) such that

             A11: G is Hall by A9, Th30;

            

             A12: ( dom g) = ( dom A) by Def6;

            then

             A13: ( dom G) = ( dom A) by Def6;

            then

             A14: (G . k) <> {} by A8, A11;

            k in NAT by ORDINAL1:def 12;

            then

             A15: (g . (k + 1)) <> {} by A9, A5, A12;

            then

            reconsider G as Singlification of A, (k + 1) by A2, A5, A8, A14, Th24;

            for l be Element of NAT st 1 <= l & l <= (k + 1) holds G is Singlification of A, l

            proof

              let l be Element of NAT ;

              assume that

               A16: 1 <= l and

               A17: l <= (k + 1);

              (k + 1) <= ( len A) by A5, FINSEQ_3: 25;

              then l <= ( len A) by A17, XXREAL_0: 2;

              then

               A18: l in ( dom A) by A16, FINSEQ_3: 25;

              then

               A19: (G . l) <> {} by A13, A11;

              per cases by A17, NAT_1: 8;

                suppose l <= k;

                then g is Singlification of A, l by A10, A16;

                hence thesis by A2, A5, A15, A18, A19, Th24;

              end;

                suppose l = (k + 1);

                hence thesis;

              end;

            end;

            hence thesis by A11;

          end;

        end;

        hence thesis;

      end;

      

       A20: P[ 0 ]

      proof

        assume 0 in ( dom A);

        then

        consider G be Singlification of A, 0 such that

         A21: G is Hall by A1, Th30;

        for k be Element of NAT st 1 <= k & k <= 0 holds G is Singlification of A, k;

        hence thesis by A21;

      end;

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

      then ( len A) in ( dom A) implies ex g be Singlification of A, ( len A) st g is Hall & for l be Element of NAT st 1 <= l & l <= ( len A) holds g is Singlification of A, l;

      then

      consider G be Singlification of A, ( len A) such that

       A22: G is Hall and

       A23: for l be Element of NAT st 1 <= l & l <= ( len A) holds G is Singlification of A, l by FINSEQ_5: 6;

      

       A24: for i be Element of NAT st i in ( dom A) holds G is Singlification of A, i

      proof

        let i be Element of NAT ;

        assume i in ( dom A);

        then 1 <= i & i <= ( len A) by FINSEQ_3: 25;

        hence thesis by A23;

      end;

      ( dom G) = ( dom A) by Def6;

      then G is Singlification of A by A2, A24, Th27;

      hence thesis by A22;

    end;

    ::$Notion-Name

    theorem :: HALLMAR1:32

    for F be non empty finite set, A be non empty FinSequence of ( bool F) holds (ex X be set st X is_a_system_of_different_representatives_of A) iff A is Hall

    proof

      let F be non empty finite set, A be non empty FinSequence of ( bool F);

      thus (ex X be set st X is_a_system_of_different_representatives_of A) implies A is Hall by Th18;

      assume

       A1: A is Hall;

      then

      consider G be Singlification of A such that

       A2: G is Hall by Th31;

      for i be Element of NAT st i in ( dom G) holds ( card (G . i)) = 1

      proof

        let i be Element of NAT ;

        assume

         A3: i in ( dom G);

        ( dom G) = ( dom A) by Def6;

        hence thesis by A1, A3, Def8;

      end;

      then ex X be set st X is_a_system_of_different_representatives_of G by A2, Th17;

      hence thesis by Th28;

    end;