abian.miz



    begin

    reserve x,y,z,E,E1,E2,E3 for set,

sE for Subset-Family of E,

f for Function of E, E,

k,l,m,n for Nat;

    definition

      let i be Integer;

      :: ABIAN:def1

      attr i is even means 2 divides i;

    end

    notation

      let i be Integer;

      antonym i is odd for i is even;

    end

    

     Lm1: for i be Integer holds i is even iff ex j be Integer st i = (2 * j) by INT_1:def 3;

    definition

      let n be Nat;

      :: original: even

      redefine

      :: ABIAN:def2

      attr n is even means ex k st n = (2 * k);

      compatibility

      proof

        hereby

          assume n is even;

          then 2 divides n;

          then

          consider k be Integer such that

           A1: n = (2 * k);

           0 <= k by A1, XREAL_1: 132;

          then k in NAT by INT_1: 3;

          then

          reconsider k as Nat;

          take k;

          thus n = (2 * k) by A1;

        end;

        thus thesis by Lm1;

      end;

    end

    registration

      cluster even for Nat;

      existence

      proof

        take 0 , 0 ;

        thus thesis;

      end;

      cluster odd for Nat;

      existence

      proof

        take 1;

        let k be Nat;

        thus thesis by NAT_1: 15;

      end;

      cluster even for Element of NAT ;

      existence

      proof

        take 0 , 0 ;

        thus thesis;

      end;

      cluster odd for Element of NAT ;

      existence

      proof

        take 1;

        let k be Nat;

        thus thesis by NAT_1: 15;

      end;

      cluster even for Integer;

      existence

      proof

        take 0 , 0 ;

        thus thesis;

      end;

      cluster odd for Integer;

      existence

      proof

        take 1;

        assume 1 is even;

        then ex k be Integer st 1 = (2 * k);

        hence contradiction by INT_1: 9;

      end;

    end

    theorem :: ABIAN:1

    

     Th1: for i be Integer holds i is odd iff ex j be Integer st i = ((2 * j) + 1)

    proof

      let i be Integer;

      hereby

        consider k such that

         A1: i = k or i = ( - k) by INT_1: 2;

        consider m be Element of NAT such that

         A2: k = (2 * m) or k = ((2 * m) + 1) by SCHEME1: 1;

        assume

         A3: i is odd;

        assume

         A4: for j be Integer holds i <> ((2 * j) + 1);

        per cases by A1, A2;

          suppose i = k & k = (2 * m);

          hence contradiction by A3, Lm1;

        end;

          suppose i = ( - k) & k = (2 * m);

          then i = (2 * ( - m));

          hence contradiction by A3, Lm1;

        end;

          suppose i = k & k = ((2 * m) + 1);

          hence contradiction by A4;

        end;

          suppose i = ( - k) & k = ((2 * m) + 1);

          then i = ((2 * ( - (m + 1))) + 1);

          hence contradiction by A4;

        end;

      end;

      given j be Integer such that

       A5: i = ((2 * j) + 1);

      given k be Integer such that

       A6: i = (2 * k);

      1 = (2 * (k - j)) by A5, A6;

      hence contradiction by INT_1: 9;

    end;

    registration

      let i be Integer;

      cluster (2 * i) -> even;

      coherence by Lm1;

    end

    registration

      let i be even Integer;

      cluster (i + 1) -> odd;

      coherence

      proof

        ex j be Integer st i = (2 * j) by Lm1;

        hence thesis by Th1;

      end;

    end

    registration

      let i be odd Integer;

      cluster (i + 1) -> even;

      coherence

      proof

        consider j be Integer such that

         A1: i = ((2 * j) + 1) by Th1;

        (i + 1) = (2 * (j + 1)) by A1;

        hence thesis;

      end;

    end

    registration

      let i be even Integer;

      cluster (i - 1) -> odd;

      coherence

      proof

        consider j be Integer such that

         A1: i = (2 * j) by Lm1;

        (i - 1) = ((2 * (j - 1)) + 1) by A1;

        hence thesis;

      end;

    end

    registration

      let i be odd Integer;

      cluster (i - 1) -> even;

      coherence

      proof

        ex j be Integer st i = ((2 * j) + 1) by Th1;

        hence thesis;

      end;

    end

    registration

      let i be even Integer, j be Integer;

      cluster (i * j) -> even;

      coherence

      proof

        consider k be Integer such that

         A1: i = (2 * k) by Lm1;

        (i * j) = (2 * (k * j)) by A1;

        hence thesis;

      end;

      cluster (j * i) -> even;

      coherence ;

    end

    registration

      let i,j be odd Integer;

      cluster (i * j) -> odd;

      coherence

      proof

        consider l be Integer such that

         A1: j = ((2 * l) + 1) by Th1;

        consider k be Integer such that

         A2: i = ((2 * k) + 1) by Th1;

        (i * j) = ((2 * (((k * (2 * l)) + (k * 1)) + (l * 1))) + 1) by A2, A1;

        hence thesis;

      end;

    end

    registration

      let i,j be even Integer;

      cluster (i + j) -> even;

      coherence

      proof

        consider l be Integer such that

         A1: j = (2 * l) by Lm1;

        consider k be Integer such that

         A2: i = (2 * k) by Lm1;

        (i + j) = (2 * (k + l)) by A2, A1;

        hence thesis;

      end;

    end

    registration

      let i be even Integer, j be odd Integer;

      cluster (i + j) -> odd;

      coherence

      proof

        consider l be Integer such that

         A1: j = ((2 * l) + 1) by Th1;

        consider k be Integer such that

         A2: i = (2 * k) by Lm1;

        (i + j) = ((2 * (k + l)) + 1) by A2, A1;

        hence thesis;

      end;

      cluster (j + i) -> odd;

      coherence ;

    end

    registration

      let i,j be odd Integer;

      cluster (i + j) -> even;

      coherence

      proof

        consider l be Integer such that

         A1: j = ((2 * l) + 1) by Th1;

        consider k be Integer such that

         A2: i = ((2 * k) + 1) by Th1;

        (j + i) = (2 * ((k + l) + 1)) by A2, A1;

        hence thesis;

      end;

    end

    registration

      let i be even Integer, j be odd Integer;

      cluster (i - j) -> odd;

      coherence

      proof

        consider l be Integer such that

         A1: j = ((2 * l) + 1) by Th1;

        consider k be Integer such that

         A2: i = (2 * k) by Lm1;

        (i - j) = ((2 * (k - l)) - 1) by A2, A1;

        hence thesis;

      end;

      cluster (j - i) -> odd;

      coherence

      proof

        consider l be Integer such that

         A3: j = ((2 * l) + 1) by Th1;

        consider k be Integer such that

         A4: i = (2 * k) by Lm1;

        (j - i) = ((2 * (l - k)) + 1) by A4, A3;

        hence thesis;

      end;

    end

    registration

      let i,j be odd Integer;

      cluster (i - j) -> even;

      coherence

      proof

        consider l be Integer such that

         A1: j = ((2 * l) + 1) by Th1;

        consider k be Integer such that

         A2: i = ((2 * k) + 1) by Th1;

        (i - j) = (2 * (k - l)) by A2, A1;

        hence thesis;

      end;

    end

    registration

      let m be even Integer;

      cluster (m + 2) -> even;

      coherence

      proof

        2 = (2 * 1);

        then

        reconsider t = 2 as even Integer;

        (m + t) is even;

        hence thesis;

      end;

    end

    registration

      let m be odd Integer;

      cluster (m + 2) -> odd;

      coherence

      proof

        2 = (2 * 1);

        then

        reconsider t = 2 as even Integer;

        (m + t) is odd;

        hence thesis;

      end;

    end

    definition

      let E, f;

      let n be Nat;

      :: original: iter

      redefine

      func iter (f,n) -> Function of E, E ;

      coherence by FUNCT_7: 83;

    end

    theorem :: ABIAN:2

    

     Th2: for S be non empty Subset of NAT st 0 in S holds ( min S) = 0 by XXREAL_2:def 7;

    theorem :: ABIAN:3

    

     Th3: for E be non empty set, f be Function of E, E, x be Element of E holds (( iter (f, 0 )) . x) = x

    proof

      let E be non empty set, f be Function of E, E, x be Element of E;

      ( dom f) = E by FUNCT_2:def 1;

      then

       A1: x in (( dom f) \/ ( rng f)) by XBOOLE_0:def 3;

      

      thus (( iter (f, 0 )) . x) = (( id ( field f)) . x) by FUNCT_7: 68

      .= x by A1, FUNCT_1: 17;

    end;

    definition

      let x be object, f be Function;

      :: ABIAN:def3

      pred x is_a_fixpoint_of f means x in ( dom f) & x = (f . x);

    end

    definition

      let A be non empty set, a be Element of A, f be Function of A, A;

      :: original: is_a_fixpoint_of

      redefine

      :: ABIAN:def4

      pred a is_a_fixpoint_of f means a = (f . a);

      compatibility

      proof

        thus a is_a_fixpoint_of f implies a = (f . a);

        assume

         A1: a = (f . a);

        a in A;

        hence a in ( dom f) by FUNCT_2: 52;

        thus a = (f . a) by A1;

      end;

    end

    definition

      let f be Function;

      :: ABIAN:def5

      attr f is with_fixpoint means ex x be object st x is_a_fixpoint_of f;

    end

    notation

      let f be Function;

      antonym f is without_fixpoints for f is with_fixpoint;

    end

    definition

      let X be set, x be Element of X;

      :: ABIAN:def6

      attr x is covering means ( union x) = ( union ( union X));

    end

    theorem :: ABIAN:4

    

     Th4: sE is covering iff ( union sE) = E

    proof

      ( union ( union ( bool ( bool E)))) = ( union ( bool E)) by ZFMISC_1: 81

      .= E by ZFMISC_1: 81;

      hence thesis;

    end;

    registration

      let E;

      cluster non empty finite covering for Subset-Family of E;

      existence

      proof

        reconsider sE = {E} as Subset-Family of E by ZFMISC_1: 68;

        take sE;

        thus sE is non empty finite;

        ( union sE) = E by ZFMISC_1: 25;

        hence thesis by Th4;

      end;

    end

    theorem :: ABIAN:5

    for E be set, f be Function of E, E, sE be non empty covering Subset-Family of E st for X be Element of sE holds X misses (f .: X) holds f is without_fixpoints

    proof

      let E be set, f be Function of E, E, sE be non empty covering Subset-Family of E;

      assume

       A1: for X be Element of sE holds X misses (f .: X);

      given x be object such that

       A2: x is_a_fixpoint_of f;

      

       A3: (f . x) = x by A2;

      

       A4: x in ( dom f) by A2;

      ( dom f) = E by FUNCT_2: 52;

      then x in ( union sE) by A4, Th4;

      then

      consider X be set such that

       A5: x in X and

       A6: X in sE by TARSKI:def 4;

      (f . x) in (f .: X) by A4, A5, FUNCT_1:def 6;

      then X meets (f .: X) by A3, A5, XBOOLE_0: 3;

      hence contradiction by A1, A6;

    end;

    definition

      let E, f;

      :: ABIAN:def7

      func =_ f -> Equivalence_Relation of E means

      : Def7: for x, y st x in E & y in E holds [x, y] in it iff ex k, l st (( iter (f,k)) . x) = (( iter (f,l)) . y);

      existence

      proof

        defpred P[ object, object] means $1 in E & $2 in E & ex k, l st (( iter (f,k)) . $1) = (( iter (f,l)) . $2);

         A1:

        now

          let x be object;

          

           A2: (( iter (f, 0 )) . x) = (( iter (f, 0 )) . x);

          assume x in E;

          hence P[x, x] by A2;

        end;

         A3:

        now

          let x,y,z be object;

          assume that

           A4: P[x, y] and

           A5: P[y, z];

          consider k, l such that

           A6: (( iter (f,k)) . x) = (( iter (f,l)) . y) by A4;

          consider m, n such that

           A7: (( iter (f,m)) . y) = (( iter (f,n)) . z) by A5;

          

           A8: ( dom ( iter (f,m))) = E by FUNCT_2: 52;

          

           A9: ( dom ( iter (f,l))) = E by FUNCT_2: 52;

          

           A10: ( dom ( iter (f,k))) = E by FUNCT_2: 52;

          

           A11: ( dom ( iter (f,n))) = E by FUNCT_2: 52;

          (( iter (f,(k + m))) . x) = ((( iter (f,m)) * ( iter (f,k))) . x) by FUNCT_7: 77

          .= (( iter (f,m)) . (( iter (f,l)) . y)) by A4, A6, A10, FUNCT_1: 13

          .= ((( iter (f,m)) * ( iter (f,l))) . y) by A4, A9, FUNCT_1: 13

          .= (( iter (f,(m + l))) . y) by FUNCT_7: 77

          .= ((( iter (f,l)) * ( iter (f,m))) . y) by FUNCT_7: 77

          .= (( iter (f,l)) . (( iter (f,n)) . z)) by A4, A7, A8, FUNCT_1: 13

          .= ((( iter (f,l)) * ( iter (f,n))) . z) by A5, A11, FUNCT_1: 13

          .= (( iter (f,(l + n))) . z) by FUNCT_7: 77;

          hence P[x, z] by A4, A5;

        end;

        

         A12: for x,y be object st P[x, y] holds P[y, x];

        consider EqR be Equivalence_Relation of E such that

         A13: for x,y be object holds [x, y] in EqR iff x in E & y in E & P[x, y] from EQREL_1:sch 1( A1, A12, A3);

        take EqR;

        let x, y;

        assume x in E & y in E;

        hence thesis by A13;

      end;

      uniqueness

      proof

        let IT1,IT2 be Equivalence_Relation of E such that

         A14: for x, y st x in E & y in E holds [x, y] in IT1 iff ex k, l st (( iter (f,k)) . x) = (( iter (f,l)) . y) and

         A15: for x, y st x in E & y in E holds [x, y] in IT2 iff ex k, l st (( iter (f,k)) . x) = (( iter (f,l)) . y);

        let a,b be object;

        hereby

          assume

           A16: [a, b] in IT1;

          then

           A17: a in E & b in E by ZFMISC_1: 87;

          then ex k, l st (( iter (f,k)) . a) = (( iter (f,l)) . b) by A14, A16;

          hence [a, b] in IT2 by A15, A17;

        end;

        assume

         A18: [a, b] in IT2;

        then

         A19: a in E & b in E by ZFMISC_1: 87;

        then ex k, l st (( iter (f,k)) . a) = (( iter (f,l)) . b) by A15, A18;

        hence thesis by A14, A19;

      end;

    end

    theorem :: ABIAN:6

    

     Th6: for E be non empty set, f be Function of E, E, c be Element of ( Class ( =_ f)), e be Element of c holds (f . e) in c

    proof

      let E be non empty set, f be Function of E, E;

      let c be Element of ( Class ( =_ f)), e be Element of c;

      ( dom f) = E by FUNCT_2:def 1;

      then

       A1: (f . e) in (( dom f) \/ ( rng f)) by XBOOLE_0:def 3;

      ex x9 be object st x9 in E & c = ( Class (( =_ f),x9)) by EQREL_1:def 3;

      then

       A2: c = ( Class (( =_ f),e)) by EQREL_1: 23;

      (( iter (f,1)) . e) = (f . e) by FUNCT_7: 70

      .= (( id ( field f)) . (f . e)) by A1, FUNCT_1: 17

      .= (( iter (f, 0 )) . (f . e)) by FUNCT_7: 68;

      then [(f . e), e] in ( =_ f) by Def7;

      hence thesis by A2, EQREL_1: 19;

    end;

    theorem :: ABIAN:7

    

     Th7: for E be non empty set, f be Function of E, E, c be Element of ( Class ( =_ f)), e be Element of c, n holds (( iter (f,n)) . e) in c

    proof

      let E be non empty set, f be Function of E, E;

      let c be Element of ( Class ( =_ f)), e be Element of c, n;

      ( dom f) = E by FUNCT_2:def 1;

      then (( iter (f,n)) . e) in (( dom f) \/ ( rng f)) by XBOOLE_0:def 3;

      

      then (( iter (f,n)) . e) = (( id ( field f)) . (( iter (f,n)) . e)) by FUNCT_1: 17

      .= (( iter (f, 0 )) . (( iter (f,n)) . e)) by FUNCT_7: 68;

      then

       A1: [(( iter (f,n)) . e), e] in ( =_ f) by Def7;

      ex x9 be object st x9 in E & c = ( Class (( =_ f),x9)) by EQREL_1:def 3;

      then c = ( Class (( =_ f),e)) by EQREL_1: 23;

      hence thesis by A1, EQREL_1: 19;

    end;

    registration

      cluster empty-membered -> trivial for set;

      coherence ;

    end

    registration

      let A be set, B be with_non-empty_element set;

      cluster non-empty for Function of A, B;

      existence

      proof

        consider X be non empty set such that

         A1: X in B by SETFAM_1:def 10;

        reconsider f = (A --> X) as Function of A, B by A1, FUNCOP_1: 45;

        take f;

        let n be object;

        assume n in ( dom f);

        then n in A by FUNCOP_1: 13;

        hence thesis by FUNCOP_1: 7;

      end;

    end

    registration

      let A be non empty set, B be with_non-empty_element set, f be non-empty Function of A, B, a be Element of A;

      cluster (f . a) -> non empty;

      coherence

      proof

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

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

        hence thesis;

      end;

    end

    registration

      let X be non empty set;

      cluster ( bool X) -> with_non-empty_element;

      coherence

      proof

        take X;

        thus thesis by ZFMISC_1:def 1;

      end;

    end

    theorem :: ABIAN:8

    for E be non empty set, f be Function of E, E st f is without_fixpoints holds ex E1, E2, E3 st ((E1 \/ E2) \/ E3) = E & (f .: E1) misses E1 & (f .: E2) misses E2 & (f .: E3) misses E3

    proof

      let E be non empty set, f be Function of E, E;

      defpred P[ set, Element of [:( bool E) qua set, ( bool E), ( bool E):]] means ((($2 `1_3 ) \/ ($2 `2_3 )) \/ ($2 `3_3 )) = $1 & (f .: ($2 `1_3 )) misses ($2 `1_3 ) & (f .: ($2 `2_3 )) misses ($2 `2_3 ) & (f .: ($2 `3_3 )) misses ($2 `3_3 );

      deffunc i( Nat) = ( iter (f,$1));

      assume

       A1: f is without_fixpoints;

      

       A2: for a be Element of ( Class ( =_ f)) holds ex b be Element of [:( bool E), ( bool E), ( bool E):] st P[a, b]

      proof

        reconsider c3 = {} as Subset of E by XBOOLE_1: 2;

        let c be Element of ( Class ( =_ f));

        consider x0 be object such that

         A3: x0 in E and

         A4: c = ( Class (( =_ f),x0)) by EQREL_1:def 3;

        reconsider x0 as Element of c by A3, A4, EQREL_1: 20;

        defpred P[ set] means ex k, l st ( i(k) . $1) = ( i(l) . x0) & k is even & l is even;

        set c1 = { x where x be Element of c : P[x] };

        c1 is Subset of c from DOMAIN_1:sch 7;

        then

        reconsider c1 as Subset of E by XBOOLE_1: 1;

        defpred P[ set] means ex k, l st ( i(k) . $1) = ( i(l) . x0) & k is odd & l is even;

        set c2 = { x where x be Element of c : P[x] };

        c2 is Subset of c from DOMAIN_1:sch 7;

        then

        reconsider c2 as Subset of E by XBOOLE_1: 1;

        per cases ;

          suppose

           A5: c1 misses c2;

          take b = [c1, c2, c3];

          

           A6: (b `2_3 ) = c2 by MCART_1:def 6;

          

           A7: (b `3_3 ) = c3 by MCART_1:def 7;

          

           A8: (b `1_3 ) = c1 by MCART_1:def 5;

          thus (((b `1_3 ) \/ (b `2_3 )) \/ (b `3_3 )) = c

          proof

            hereby

              let x be object;

              assume

               A9: x in (((b `1_3 ) \/ (b `2_3 )) \/ (b `3_3 ));

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

                suppose x in c1;

                then ex xx be Element of c st x = xx & ex k, l st ( i(k) . xx) = ( i(l) . x0) & k is even & l is even;

                hence x in c;

              end;

                suppose x in c2;

                then ex xx be Element of c st x = xx & ex k, l st ( i(k) . xx) = ( i(l) . x0) & k is odd & l is even;

                hence x in c;

              end;

                suppose x in c3;

                hence x in c;

              end;

            end;

            let x be object;

            assume x in c;

            then

            reconsider xc = x as Element of c;

             [xc, x0] in ( =_ f) by A4, EQREL_1: 19;

            then

            consider k, l such that

             A10: ( i(k) . xc) = ( i(l) . x0) by Def7;

            

             A11: ( dom i(l)) = E by FUNCT_2:def 1;

            

             A12: ( dom i(k)) = E by FUNCT_2:def 1;

            per cases ;

              suppose

               A13: k is even;

              then

              reconsider k as even Nat;

              thus x in (((b `1_3 ) \/ (b `2_3 )) \/ (b `3_3 ))

              proof

                per cases ;

                  suppose l is even;

                  then xc in c1 by A10, A13;

                  hence thesis by A8, A7, XBOOLE_0:def 3;

                end;

                  suppose l is odd;

                  then

                  reconsider l as odd Nat;

                  ( i(+) . xc) = ((f * i(k)) . xc) by FUNCT_7: 71

                  .= (f . ( i(l) . x0)) by A10, A12, FUNCT_1: 13

                  .= ((f * i(l)) . x0) by A11, FUNCT_1: 13

                  .= ( i(+) . x0) by FUNCT_7: 71;

                  then xc in c2;

                  hence thesis by A6, A7, XBOOLE_0:def 3;

                end;

              end;

            end;

              suppose

               A14: k is odd;

              then

              reconsider k as odd Nat;

              thus x in (((b `1_3 ) \/ (b `2_3 )) \/ (b `3_3 ))

              proof

                per cases ;

                  suppose l is even;

                  then xc in c2 by A10, A14;

                  hence thesis by A6, A7, XBOOLE_0:def 3;

                end;

                  suppose l is odd;

                  then

                  reconsider l as odd Nat;

                  ( i(+) . xc) = ((f * i(k)) . xc) by FUNCT_7: 71

                  .= (f . ( i(l) . x0)) by A10, A12, FUNCT_1: 13

                  .= ((f * i(l)) . x0) by A11, FUNCT_1: 13

                  .= ( i(+) . x0) by FUNCT_7: 71;

                  then xc in c1;

                  hence thesis by A8, A7, XBOOLE_0:def 3;

                end;

              end;

            end;

          end;

          (f .: c1) c= c2

          proof

            let y be object;

            

             A15: ( dom f) = E by FUNCT_2:def 1;

            assume y in (f .: c1);

            then

            consider x be object such that x in ( dom f) and

             A16: x in c1 and

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

            consider xx be Element of c such that

             A18: x = xx and

             A19: ex k, l st ( i(k) . xx) = ( i(l) . x0) & k is even & l is even by A16;

            consider k, l such that

             A20: ( i(k) . xx) = ( i(l) . x0) and

             A21: k is even & l is even by A19;

            reconsider k, l as even Nat by A21;

            reconsider k1 = (k + 1) as odd Element of NAT ;

            reconsider l1 = (l + 1) as odd Element of NAT ;

            reconsider l2 = (l1 + 1) as even Element of NAT ;

            

             A22: ( dom i(k)) = E by FUNCT_2:def 1;

            reconsider yc = y as Element of c by A17, A18, Th6;

            

             A23: ( dom i(l)) = E by FUNCT_2:def 1;

            

             A24: ( dom i(k1)) = E by FUNCT_2:def 1;

            

             A25: ( i(+) . xx) = (( i(k1) * f) . xx) by FUNCT_7: 69

            .= ( i(k1) . (f . xx)) by A15, FUNCT_1: 13;

            

             A26: ( dom i(l1)) = E by FUNCT_2:def 1;

            ( i(+) . xx) = ((f * i(k1)) . xx) by FUNCT_7: 71

            .= (f . ( i(k1) . xx)) by A24, FUNCT_1: 13

            .= (f . ((f * i(k)) . xx)) by FUNCT_7: 71

            .= (f . (f . ( i(l) . x0))) by A20, A22, FUNCT_1: 13

            .= (f . ((f * i(l)) . x0)) by A23, FUNCT_1: 13

            .= (f . ( i(l1) . x0)) by FUNCT_7: 71

            .= ((f * i(l1)) . x0) by A26, FUNCT_1: 13

            .= ( i(l2) . x0) by FUNCT_7: 71;

            then yc in c2 by A17, A18, A25;

            hence thesis;

          end;

          hence (f .: (b `1_3 )) misses (b `1_3 ) by A5, A8, XBOOLE_1: 63;

          (f .: c2) c= c1

          proof

            let y be object;

            

             A27: ( dom f) = E by FUNCT_2:def 1;

            assume y in (f .: c2);

            then

            consider x be object such that x in ( dom f) and

             A28: x in c2 and

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

            consider xx be Element of c such that

             A30: x = xx and

             A31: ex k, l st ( i(k) . xx) = ( i(l) . x0) & k is odd & l is even by A28;

            consider k, l such that

             A32: ( i(k) . xx) = ( i(l) . x0) and

             A33: k is odd and

             A34: l is even by A31;

            reconsider l as even Nat by A34;

            reconsider k as odd Nat by A33;

            reconsider k1 = (k + 1) as even Element of NAT ;

            reconsider l1 = (l + 1) as odd Element of NAT ;

            reconsider l2 = (l1 + 1) as even Element of NAT ;

            

             A35: ( dom i(k)) = E by FUNCT_2:def 1;

            reconsider yc = y as Element of c by A29, A30, Th6;

            

             A36: ( dom i(l)) = E by FUNCT_2:def 1;

            

             A37: ( dom i(k1)) = E by FUNCT_2:def 1;

            

             A38: ( i(+) . xx) = (( i(k1) * f) . xx) by FUNCT_7: 69

            .= ( i(k1) . (f . xx)) by A27, FUNCT_1: 13;

            

             A39: ( dom i(l1)) = E by FUNCT_2:def 1;

            ( i(+) . xx) = ((f * i(k1)) . xx) by FUNCT_7: 71

            .= (f . ( i(k1) . xx)) by A37, FUNCT_1: 13

            .= (f . ((f * i(k)) . xx)) by FUNCT_7: 71

            .= (f . (f . ( i(l) . x0))) by A32, A35, FUNCT_1: 13

            .= (f . ((f * i(l)) . x0)) by A36, FUNCT_1: 13

            .= (f . ( i(l1) . x0)) by FUNCT_7: 71

            .= ((f * i(l1)) . x0) by A39, FUNCT_1: 13

            .= ( i(l2) . x0) by FUNCT_7: 71;

            then yc in c1 by A29, A30, A38;

            hence thesis;

          end;

          hence (f .: (b `2_3 )) misses (b `2_3 ) by A5, A6, XBOOLE_1: 63;

          thus thesis by A7;

        end;

          suppose c1 meets c2;

          then

          consider x1 be object such that

           A40: x1 in c1 and

           A41: x1 in c2 by XBOOLE_0: 3;

          consider x11 be Element of c such that

           A42: x1 = x11 and

           A43: ex k, l st ( i(k) . x11) = ( i(l) . x0) & k is even & l is even by A40;

          consider x12 be Element of c such that

           A44: x1 = x12 and

           A45: ex k, l st ( i(k) . x12) = ( i(l) . x0) & k is odd & l is even by A41;

          consider k2,l2 be Nat such that

           A46: ( i(k2) . x12) = ( i(l2) . x0) and

           A47: k2 is odd and

           A48: l2 is even by A45;

          reconsider x1 as Element of c by A42;

          consider k1,l1 be Nat such that

           A49: ( i(k1) . x11) = ( i(l1) . x0) and

           A50: k1 is even & l1 is even by A43;

          

           A51: ( dom i(k1)) = E by FUNCT_2:def 1;

          

           A52: ( dom i(l1)) = E by FUNCT_2:def 1;

          

           A53: ( i(+) . x1) = (( i(l2) * i(k1)) . x1) by FUNCT_7: 77

          .= ( i(l2) . ( i(l1) . x0)) by A42, A49, A51, FUNCT_1: 13

          .= (( i(l2) * i(l1)) . x0) by A52, FUNCT_1: 13

          .= ( i(+) . x0) by FUNCT_7: 77;

          

           A54: ( dom i(l2)) = E by FUNCT_2:def 1;

          

           A55: ( dom i(k2)) = E by FUNCT_2:def 1;

          

           A56: ( i(+) . x1) = (( i(l1) * i(k2)) . x1) by FUNCT_7: 77

          .= ( i(l1) . ( i(l2) . x0)) by A44, A46, A55, FUNCT_1: 13

          .= (( i(l1) * i(l2)) . x0) by A54, FUNCT_1: 13

          .= ( i(+) . x0) by FUNCT_7: 77;

          ex r be Element of E, k be odd Element of NAT st ( i(k) . r) = r & r in c

          proof

            reconsider k2 as odd Nat by A47;

            reconsider k1, l1, l2 as even Nat by A50, A48;

            

             A57: ( dom i(+)) = E by FUNCT_2:def 1;

            

             A58: ( dom i(+)) = E by FUNCT_2:def 1;

            per cases by XXREAL_0: 1;

              suppose (k1 + l2) < (k2 + l1);

              then

              reconsider k = ((k2 + l1) - (k1 + l2)) as Element of NAT by INT_1: 5;

              take r = ( i(+) . x1);

              reconsider k as odd Element of NAT ;

              take k;

              ( i(k) . ( i(+) . x1)) = (( i(k) * i(+)) . x1) by A57, FUNCT_1: 13

              .= ( i(+) . x1) by FUNCT_7: 77

              .= ( i(+) . x1) by A56, A53;

              hence ( i(k) . r) = r;

              thus thesis by Th7;

            end;

              suppose (k1 + l2) > (k2 + l1);

              then

              reconsider k = ((k1 + l2) - (k2 + l1)) as Element of NAT by INT_1: 5;

              take r = ( i(+) . x1);

              reconsider k as odd Element of NAT ;

              take k;

              ( i(k) . ( i(+) . x1)) = (( i(k) * i(+)) . x1) by A58, FUNCT_1: 13

              .= ( i(+) . x1) by FUNCT_7: 77

              .= ( i(+) . x1) by A56, A53;

              hence ( i(k) . r) = r;

              thus thesis by Th7;

            end;

          end;

          then

          consider r be Element of E, k be odd Element of NAT such that

           A59: ( i(k) . r) = r and

           A60: r in c;

          reconsider r as Element of c by A60;

          deffunc F( set) = { l where l be Element of NAT : ( i(l) . $1) = r };

          

           A61: for x be Element of c holds F(x) in ( bool NAT )

          proof

            let x be Element of c;

            defpred P1[ Element of NAT ] means ( i($1) . x) = r;

            { l where l be Element of NAT : P1[l] } is Subset of NAT from DOMAIN_1:sch 7;

            hence thesis;

          end;

          consider Odl be Function of c, ( bool NAT ) such that

           A62: for x be Element of c holds (Odl . x) = F(x) from FUNCT_2:sch 8( A61);

          now

            defpred P[ Nat] means ( i(*) . r) = r;

            let n be object;

            assume n in ( dom Odl);

            then

            reconsider nc = n as Element of c by FUNCT_2:def 1;

            

             A63: (Odl . nc) = { l where l be Element of NAT : ( i(l) . nc) = r } by A62;

             A64:

            now

              let i be Nat;

              assume

               A65: P[i];

              

               A66: ( dom i(k)) = E by FUNCT_2:def 1;

              ( i(*) . r) = ( i(+) . r)

              .= (( i(*) * i(k)) . r) by FUNCT_7: 77

              .= r by A59, A65, A66, FUNCT_1: 13;

              hence P[(i + 1)];

            end;

            

             A67: P[ 0 ] by Th3;

            

             A68: for i be Nat holds P[i] from NAT_1:sch 2( A67, A64);

            ex x9 be object st x9 in E & c = ( Class (( =_ f),x9)) by EQREL_1:def 3;

            then [nc, r] in ( =_ f) by EQREL_1: 22;

            then

            consider kn,ln be Nat such that

             A69: (( iter (f,kn)) . nc) = (( iter (f,ln)) . r) by Def7;

            

             A70: ( dom i(ln)) = E by FUNCT_2:def 1;

            set mk = (ln mod k);

            set dk = (ln div k);

            

             A71: ( dom i(kn)) = E by FUNCT_2:def 1;

            

             A72: (2 * 0 ) <> k;

            then mk < k by NAT_D: 1;

            then

            reconsider kmk = (k - mk) as Element of NAT by INT_1: 5;

            ln = ((k * dk) + mk) by A72, NAT_D: 2;

            then

             A73: (ln + kmk) = (k * (dk + 1));

            ( i(+) . nc) = (( i(kmk) * i(kn)) . nc) by FUNCT_7: 77

            .= ( i(kmk) . ( i(ln) . r)) by A69, A71, FUNCT_1: 13

            .= (( i(kmk) * i(ln)) . r) by A70, FUNCT_1: 13

            .= ( i(*) . r) by A73, FUNCT_7: 77

            .= r by A68;

            then (kn + kmk) in (Odl . n) by A63;

            hence (Odl . n) is non empty;

          end;

          then

          reconsider Odl as non-empty Function of c, ( bool NAT ) by FUNCT_1:def 9;

          deffunc F( Element of c) = ( min (Odl . $1));

          consider odl be Function of c, NAT such that

           A74: for x be Element of c holds (odl . x) = F(x) from FUNCT_2:sch 4;

          defpred P1[ Element of c] means (odl . $1) is even;

          set c1 = { x where x be Element of c : P1[x] };

          set d1 = (c1 \ {r});

          c1 is Subset of c from DOMAIN_1:sch 7;

          then

           A75: d1 c= c by XBOOLE_1: 1;

          ( i(0) . r) = r by Th3;

          then 0 in { l where l be Element of NAT : ( i(l) . r) = r };

          then 0 in (Odl . r) by A62;

          then ( min (Odl . r)) = 0 by Th2;

          then

           A76: (odl . r) = (2 * 0 ) by A74;

          then

           A77: r in c1;

          reconsider d1 as Subset of E by A75, XBOOLE_1: 1;

          defpred P2[ Element of c] means (odl . $1) is odd;

          set d2 = { x where x be Element of c : P2[x] };

          d2 is Subset of c from DOMAIN_1:sch 7;

          then

          reconsider d2 as Subset of E by XBOOLE_1: 1;

          

           A78: for x be Element of c st x <> r holds (odl . (f . x)) = ((odl . x) qua Element of NAT - 1)

          proof

            let x be Element of c;

            reconsider fx = (f . x) as Element of c by Th6;

            reconsider ofx = (odl . fx), ox = (odl . x) as Element of NAT ;

            assume

             A79: x <> r;

            now

              assume (odl . x) = 0 ;

              then 0 = ( min (Odl . x)) by A74;

              then 0 in (Odl . x) by XXREAL_2:def 7;

              then 0 in { l where l be Element of NAT : ( i(l) . x) = r } by A62;

              then ex l be Element of NAT st l = 0 & ( i(l) . x) = r;

              hence contradiction by A79, Th3;

            end;

            then

            reconsider ox1 = (ox - 1) as Element of NAT by INT_1: 5, NAT_1: 14;

            ox = ( min (Odl . x)) by A74;

            then ox in (Odl . x) by XXREAL_2:def 7;

            then ox in { l where l be Element of NAT : ( i(l) . x) = r } by A62;

            then

             A80: ex l be Element of NAT st l = ox & ( i(l) . x) = r;

            

             A81: ( dom f) = E by FUNCT_2:def 1;

            

            then ( i(ox1) . fx) = (( i(ox1) * f) . x) by FUNCT_1: 13

            .= ( i(+) . x) by FUNCT_7: 69

            .= ( i(ox) . x);

            then ox1 in { l where l be Element of NAT : ( i(l) . fx) = r } by A80;

            then

             A82: ox1 in (Odl . fx) by A62;

            ofx = ( min (Odl . fx)) by A74;

            then ofx in (Odl . fx) by XXREAL_2:def 7;

            then ofx in { l where l be Element of NAT : ( i(l) . fx) = r } by A62;

            then

             A83: ex l be Element of NAT st l = ofx & ( i(l) . fx) = r;

            ( i(+) . x) = (( i(ofx) * f) . x) by FUNCT_7: 69

            .= ( i(ofx) . fx) by A81, FUNCT_1: 13;

            then (ofx + 1) in { l where l be Element of NAT : ( i(l) . x) = r } by A83;

            then

             A84: (ofx + 1) in (Odl . x) by A62;

            ox = ( min (Odl . x)) by A74;

            then (ofx + 1) >= ox by A84, XXREAL_2:def 7;

            then

             A85: ofx >= (ox - 1) by XREAL_1: 20;

            ofx = ( min (Odl . fx)) by A74;

            then ofx <= (ox - 1) by A82, XXREAL_2:def 7;

            hence thesis by A85, XXREAL_0: 1;

          end;

          

           A86: (f .: d1) c= d2

          proof

            let y be object;

            assume y in (f .: d1);

            then

            consider x be object such that x in ( dom f) and

             A87: x in d1 and

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

            x in c1 by A87;

            then

            consider xx be Element of c such that

             A89: x = xx and

             A90: (odl . xx) is even;

            reconsider ox = (odl . xx) as even Element of NAT by A90;

            reconsider yc = y as Element of c by A88, A89, Th6;

            r <> xx by A87, A89, ZFMISC_1: 56;

            then (odl . yc) = (ox - 1) by A78, A88, A89;

            hence thesis;

          end;

          

           A91: (c1 \/ d2) = c

          proof

            hereby

              let x be object;

              assume

               A92: x in (c1 \/ d2);

              per cases by A92, XBOOLE_0:def 3;

                suppose x in c1;

                then ex xc be Element of c st xc = x & (odl . xc) is even;

                hence x in c;

              end;

                suppose x in d2;

                then ex xc be Element of c st xc = x & (odl . xc) is odd;

                hence x in c;

              end;

            end;

            let x be object;

            assume x in c;

            then

            reconsider xc = x as Element of c;

            (odl . xc) is even or (odl . xc) is odd;

            then x in c1 or x in d2;

            hence thesis by XBOOLE_0:def 3;

          end;

          reconsider d3 = {r} as Subset of E by ZFMISC_1: 31;

          take b = [d1, d2, d3];

          

           A93: (b `1_3 ) = d1 by MCART_1:def 5;

          

           A94: (b `2_3 ) = d2 by MCART_1:def 6;

          

           A95: (b `3_3 ) = d3 by MCART_1:def 7;

          (d1 \/ d3) = (c1 \/ d3) by XBOOLE_1: 39

          .= c1 by A77, ZFMISC_1: 40;

          hence (((b `1_3 ) \/ (b `2_3 )) \/ (b `3_3 )) = c by A93, A94, A95, A91, XBOOLE_1: 4;

          

           A96: c1 misses d2

          proof

            assume c1 meets d2;

            then

            consider z be object such that

             A97: z in c1 & z in d2 by XBOOLE_0: 3;

            (ex x be Element of c st z = x & (odl . x) is even) & ex x be Element of c st z = x & (odl . x) is odd by A97;

            hence contradiction;

          end;

          then d1 misses d2 by XBOOLE_1: 63;

          hence (f .: (b `1_3 )) misses (b `1_3 ) by A93, A86, XBOOLE_1: 63;

          (f .: d2) c= c1

          proof

            let y be object;

            assume y in (f .: d2);

            then

            consider x be object such that x in ( dom f) and

             A98: x in d2 and

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

            consider xx be Element of c such that

             A100: x = xx and

             A101: (odl . xx) is odd by A98;

            reconsider ox = (odl . xx) as odd Element of NAT by A101;

            reconsider yc = y as Element of c by A99, A100, Th6;

            (odl . yc) = (ox - 1) by A76, A78, A99, A100;

            hence thesis;

          end;

          hence (f .: (b `2_3 )) misses (b `2_3 ) by A94, A96, XBOOLE_1: 63;

          thus (f .: (b `3_3 )) misses (b `3_3 )

          proof

            assume (f .: (b `3_3 )) meets (b `3_3 );

            then

            consider y be object such that

             A102: y in (f .: (b `3_3 )) and

             A103: y in (b `3_3 ) by XBOOLE_0: 3;

            

             A104: y = r by A95, A103, TARSKI:def 1;

            consider x be object such that x in ( dom f) and

             A105: x in {r} and

             A106: y = (f . x) by A95, A102, FUNCT_1:def 6;

            x = r by A105, TARSKI:def 1;

            then r is_a_fixpoint_of f by A104, A106;

            hence contradiction by A1;

          end;

        end;

      end;

      consider F be Function of ( Class ( =_ f)), [:( bool E), ( bool E), ( bool E):] such that

       A107: for a be Element of ( Class ( =_ f)) holds P[a, (F . a)] from FUNCT_2:sch 3( A2);

      set E3c = the set of all ((F . c) `3_3 ) where c be Element of ( Class ( =_ f));

      set E2c = the set of all ((F . c) `2_3 ) where c be Element of ( Class ( =_ f));

      set E1c = the set of all ((F . c) `1_3 ) where c be Element of ( Class ( =_ f));

      set E1 = ( union E1c);

      set E2 = ( union E2c);

      set E3 = ( union E3c);

      take E1, E2, E3;

      thus ((E1 \/ E2) \/ E3) = E

      proof

        hereby

          let x be object;

          assume x in ((E1 \/ E2) \/ E3);

          then

           A108: x in (E1 \/ E2) or x in E3 by XBOOLE_0:def 3;

          per cases by A108, XBOOLE_0:def 3;

            suppose x in E1;

            then

            consider Y be set such that

             A109: x in Y and

             A110: Y in E1c by TARSKI:def 4;

            ex c be Element of ( Class ( =_ f)) st Y = ((F . c) `1_3 ) by A110;

            hence x in E by A109;

          end;

            suppose x in E2;

            then

            consider Y be set such that

             A111: x in Y and

             A112: Y in E2c by TARSKI:def 4;

            ex c be Element of ( Class ( =_ f)) st Y = ((F . c) `2_3 ) by A112;

            hence x in E by A111;

          end;

            suppose x in E3;

            then

            consider Y be set such that

             A113: x in Y and

             A114: Y in E3c by TARSKI:def 4;

            ex c be Element of ( Class ( =_ f)) st Y = ((F . c) `3_3 ) by A114;

            hence x in E by A113;

          end;

        end;

        let x be object;

        set c = ( Class (( =_ f),x));

        assume

         A115: x in E;

        then

         A116: x in c by EQREL_1: 20;

        reconsider c as Element of ( Class ( =_ f)) by A115, EQREL_1:def 3;

        x in ((((F . c) `1_3 ) \/ ((F . c) `2_3 )) \/ ((F . c) `3_3 )) by A107, A116;

        then

         A117: x in (((F . c) `1_3 ) \/ ((F . c) `2_3 )) or x in ((F . c) `3_3 ) by XBOOLE_0:def 3;

        per cases by A117, XBOOLE_0:def 3;

          suppose

           A118: x in ((F . c) `1_3 );

          ((F . c) `1_3 ) in E1c;

          then x in E1 by A118, TARSKI:def 4;

          then x in (E1 \/ E2) by XBOOLE_0:def 3;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose

           A119: x in ((F . c) `2_3 );

          ((F . c) `2_3 ) in E2c;

          then x in E2 by A119, TARSKI:def 4;

          then x in (E1 \/ E2) by XBOOLE_0:def 3;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose

           A120: x in ((F . c) `3_3 );

          ((F . c) `3_3 ) in E3c;

          then x in E3 by A120, TARSKI:def 4;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      thus (f .: E1) misses E1

      proof

        assume not thesis;

        then

        consider x be object such that

         A121: x in (f .: E1) and

         A122: x in E1 by XBOOLE_0: 3;

        consider Y be set such that

         A123: x in Y and

         A124: Y in E1c by A122, TARSKI:def 4;

        consider c be Element of ( Class ( =_ f)) such that

         A125: Y = ((F . c) `1_3 ) by A124;

        x in (((F . c) `1_3 ) \/ ((F . c) `2_3 )) by A123, A125, XBOOLE_0:def 3;

        then x in ((((F . c) `1_3 ) \/ ((F . c) `2_3 )) \/ ((F . c) `3_3 )) by XBOOLE_0:def 3;

        then

         A126: x in c by A107;

        ex x9 be object st x9 in E & c = ( Class (( =_ f),x9)) by EQREL_1:def 3;

        then

         A127: c = ( Class (( =_ f),x)) by A126, EQREL_1: 23;

        ( dom f) = E by FUNCT_2:def 1;

        then

         A128: x in (( dom f) \/ ( rng f)) by A123, A125, XBOOLE_0:def 3;

        consider xx be object such that

         A129: xx in ( dom f) and

         A130: xx in E1 and

         A131: x = (f . xx) by A121, FUNCT_1:def 6;

        consider YY be set such that

         A132: xx in YY and

         A133: YY in E1c by A130, TARSKI:def 4;

        consider cc be Element of ( Class ( =_ f)) such that

         A134: YY = ((F . cc) `1_3 ) by A133;

        xx in (((F . cc) `1_3 ) \/ ((F . cc) `2_3 )) by A132, A134, XBOOLE_0:def 3;

        then xx in ((((F . cc) `1_3 ) \/ ((F . cc) `2_3 )) \/ ((F . cc) `3_3 )) by XBOOLE_0:def 3;

        then

         A135: xx in cc by A107;

        ex xx9 be object st xx9 in E & cc = ( Class (( =_ f),xx9)) by EQREL_1:def 3;

        then

         A136: cc = ( Class (( =_ f),xx)) by A135, EQREL_1: 23;

        (( iter (f,1)) . xx) = x by A131, FUNCT_7: 70

        .= (( id ( field f)) . x) by A128, FUNCT_1: 17

        .= (( iter (f, 0 )) . x) by FUNCT_7: 68;

        then [x, xx] in ( =_ f) by A123, A125, A132, A134, Def7;

        then

         A137: ( Class (( =_ f),x)) = ( Class (( =_ f),xx)) by A123, A125, EQREL_1: 35;

        

         A138: (f . xx) in (f .: YY) by A129, A132, FUNCT_1:def 6;

        (f .: YY) misses YY by A107, A134;

        hence contradiction by A123, A125, A131, A134, A127, A136, A137, A138, XBOOLE_0: 3;

      end;

      thus (f .: E2) misses E2

      proof

        assume not thesis;

        then

        consider x be object such that

         A139: x in (f .: E2) and

         A140: x in E2 by XBOOLE_0: 3;

        consider Y be set such that

         A141: x in Y and

         A142: Y in E2c by A140, TARSKI:def 4;

        consider c be Element of ( Class ( =_ f)) such that

         A143: Y = ((F . c) `2_3 ) by A142;

        x in (((F . c) `1_3 ) \/ ((F . c) `2_3 )) by A141, A143, XBOOLE_0:def 3;

        then x in ((((F . c) `1_3 ) \/ ((F . c) `2_3 )) \/ ((F . c) `3_3 )) by XBOOLE_0:def 3;

        then

         A144: x in c by A107;

        ex x9 be object st x9 in E & c = ( Class (( =_ f),x9)) by EQREL_1:def 3;

        then

         A145: c = ( Class (( =_ f),x)) by A144, EQREL_1: 23;

        ( dom f) = E by FUNCT_2:def 1;

        then

         A146: x in (( dom f) \/ ( rng f)) by A141, A143, XBOOLE_0:def 3;

        consider xx be object such that

         A147: xx in ( dom f) and

         A148: xx in E2 and

         A149: x = (f . xx) by A139, FUNCT_1:def 6;

        consider YY be set such that

         A150: xx in YY and

         A151: YY in E2c by A148, TARSKI:def 4;

        consider cc be Element of ( Class ( =_ f)) such that

         A152: YY = ((F . cc) `2_3 ) by A151;

        xx in (((F . cc) `1_3 ) \/ ((F . cc) `2_3 )) by A150, A152, XBOOLE_0:def 3;

        then xx in ((((F . cc) `1_3 ) \/ ((F . cc) `2_3 )) \/ ((F . cc) `3_3 )) by XBOOLE_0:def 3;

        then

         A153: xx in cc by A107;

        ex xx9 be object st xx9 in E & cc = ( Class (( =_ f),xx9)) by EQREL_1:def 3;

        then

         A154: cc = ( Class (( =_ f),xx)) by A153, EQREL_1: 23;

        (( iter (f,1)) . xx) = x by A149, FUNCT_7: 70

        .= (( id ( field f)) . x) by A146, FUNCT_1: 17

        .= (( iter (f, 0 )) . x) by FUNCT_7: 68;

        then [x, xx] in ( =_ f) by A141, A143, A150, A152, Def7;

        then

         A155: ( Class (( =_ f),x)) = ( Class (( =_ f),xx)) by A141, A143, EQREL_1: 35;

        

         A156: (f . xx) in (f .: YY) by A147, A150, FUNCT_1:def 6;

        (f .: YY) misses YY by A107, A152;

        hence contradiction by A141, A143, A149, A152, A145, A154, A155, A156, XBOOLE_0: 3;

      end;

      thus (f .: E3) misses E3

      proof

        assume not thesis;

        then

        consider x be object such that

         A157: x in (f .: E3) and

         A158: x in E3 by XBOOLE_0: 3;

        consider Y be set such that

         A159: x in Y and

         A160: Y in E3c by A158, TARSKI:def 4;

        consider c be Element of ( Class ( =_ f)) such that

         A161: Y = ((F . c) `3_3 ) by A160;

        x in ((((F . c) `1_3 ) \/ ((F . c) `2_3 )) \/ ((F . c) `3_3 )) by A159, A161, XBOOLE_0:def 3;

        then

         A162: x in c by A107;

        ex x9 be object st x9 in E & c = ( Class (( =_ f),x9)) by EQREL_1:def 3;

        then

         A163: c = ( Class (( =_ f),x)) by A162, EQREL_1: 23;

        ( dom f) = E by FUNCT_2:def 1;

        then

         A164: x in (( dom f) \/ ( rng f)) by A159, A161, XBOOLE_0:def 3;

        consider xx be object such that

         A165: xx in ( dom f) and

         A166: xx in E3 and

         A167: x = (f . xx) by A157, FUNCT_1:def 6;

        consider YY be set such that

         A168: xx in YY and

         A169: YY in E3c by A166, TARSKI:def 4;

        consider cc be Element of ( Class ( =_ f)) such that

         A170: YY = ((F . cc) `3_3 ) by A169;

        xx in ((((F . cc) `1_3 ) \/ ((F . cc) `2_3 )) \/ ((F . cc) `3_3 )) by A168, A170, XBOOLE_0:def 3;

        then

         A171: xx in cc by A107;

        ex xx9 be object st xx9 in E & cc = ( Class (( =_ f),xx9)) by EQREL_1:def 3;

        then

         A172: cc = ( Class (( =_ f),xx)) by A171, EQREL_1: 23;

        (( iter (f,1)) . xx) = x by A167, FUNCT_7: 70

        .= (( id ( field f)) . x) by A164, FUNCT_1: 17

        .= (( iter (f, 0 )) . x) by FUNCT_7: 68;

        then [x, xx] in ( =_ f) by A159, A161, A168, A170, Def7;

        then

         A173: ( Class (( =_ f),x)) = ( Class (( =_ f),xx)) by A159, A161, EQREL_1: 35;

        

         A174: (f . xx) in (f .: YY) by A165, A168, FUNCT_1:def 6;

        (f .: YY) misses YY by A107, A170;

        hence contradiction by A159, A161, A167, A170, A163, A172, A173, A174, XBOOLE_0: 3;

      end;

    end;

    begin

    theorem :: ABIAN:9

    for n be Nat holds n is odd iff ex k be Nat st n = ((2 * k) + 1)

    proof

      let n be Nat;

      hereby

        assume

         A1: n is odd;

        then

        consider j be Integer such that

         A2: n = ((2 * j) + 1) by Th1;

        now

          assume j < 0 ;

          then

           A3: ((2 * j) + 1) <= (2 * 0 ) by INT_1: 7, XREAL_1: 68;

          per cases by A3;

            suppose ((2 * j) + 1) < 0 ;

            hence contradiction by A2;

          end;

            suppose ((2 * j) + 1) = 0 ;

            then n = (2 * 0 );

            hence contradiction by A1;

          end;

        end;

        then j in NAT by INT_1: 3;

        then

        reconsider j as Nat;

        take j;

        thus n = ((2 * j) + 1) by A2;

      end;

      thus thesis;

    end;

    theorem :: ABIAN:10

    for A be non empty set, f be Function of A, A, x be Element of A holds (( iter (f,(n + 1))) . x) = (f . (( iter (f,n)) . x))

    proof

      let A be non empty set, f be Function of A, A, x be Element of A;

      

      thus (( iter (f,(n + 1))) . x) = ((f * ( iter (f,n))) . x) by FUNCT_7: 71

      .= (f . (( iter (f,n)) . x)) by FUNCT_2: 15;

    end;

    theorem :: ABIAN:11

    for i be Integer holds i is even iff ex j be Integer st i = (2 * j) by Lm1;

    registration

      cluster odd for Nat;

      existence

      proof

        take 1;

        1 = ((2 * 0 ) + 1);

        hence thesis;

      end;

      cluster even for Nat;

      existence

      proof

        take 0 ;

         0 = (2 * 0 );

        hence thesis;

      end;

    end

    theorem :: ABIAN:12

    

     Th12: for n be odd Nat holds 1 <= n

    proof

      let n be odd Nat;

      (2 * 0 ) < n;

      then ( 0 + 1) <= n by NAT_1: 13;

      hence thesis;

    end;

    registration

      cluster odd -> non zero for Integer;

      coherence by Th12;

    end