nat_1.miz



    begin

    registration

      cluster natural for object;

      existence

      proof

        take 0 ;

        thus thesis;

      end;

    end

    definition

      mode Nat is natural number;

    end

    reserve x for Real,

p,k,l,m,n,s,h,i,j,k1,t,t1 for Nat,

X for Subset of REAL ;

    theorem :: NAT_1:1

    

     Th1: for X st 0 in X & for x st x in X holds (x + 1) in X holds for n holds n in X

    proof

      let A be Subset of REAL such that

       A1: 0 in A;

      assume x in A implies (x + 1) in A;

      then NAT c= A by A1, AXIOMS: 3;

      hence thesis by ORDINAL1:def 12;

    end;

    registration

      let n,k be natural Number;

      cluster (n + k) -> natural;

      coherence

      proof

        n in NAT & k in NAT by ORDINAL1:def 12;

        hence thesis by AXIOMS: 2;

      end;

    end

    definition

      let n be natural Number, k be Element of NAT ;

      :: original: +

      redefine

      func n + k -> Element of NAT ;

      coherence by ORDINAL1:def 12;

    end

    ::$Canceled

    ::$Notion-Name

    scheme :: NAT_1:sch2

    NatInd { P[ Nat] } :

for k be Nat holds P[k]

      provided

       A1: P[ 0 ]

       and

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

      let k be Nat;

      consider X be Subset of NAT such that

       A3: for x be Element of NAT holds x in X iff P[x] from SUBSET_1:sch 3;

      

       A4: for x st x in X holds (x + 1) in X

      proof

        let x;

        assume x in X;

        then

        consider k such that

         A5: P[k] and

         A6: k = x by A3;

        P[(k + 1)] by A2, A5;

        hence thesis by A3, A6;

      end;

      X c= NAT & NAT c= REAL by NUMBERS: 19;

      then X is Subset of REAL by XBOOLE_1: 1;

      then k in X by A1, A3, A4, Th1;

      hence thesis by A3;

    end;

    registration

      let n,k be natural Number;

      cluster (n * k) -> natural;

      coherence

      proof

        

         A0: k is Nat by TARSKI: 1;

        defpred P[ Nat] means (n * $1) is natural;

        

         A1: for m be Nat holds P[m] implies P[(m + 1)]

        proof

          let m be Nat;

          assume P[m];

          then

          reconsider k = (n * m) as Nat;

          (k + n) is Nat;

          hence thesis;

        end;

        

         A2: P[ 0 ];

        for m be Nat holds P[m] from NatInd( A2, A1);

        hence thesis by A0;

      end;

    end

    definition

      let n,k be Element of NAT ;

      :: original: *

      redefine

      func n * k -> Element of NAT ;

      coherence by ORDINAL1:def 12;

    end

    theorem :: NAT_1:2

    

     Th2: for i be natural Number holds 0 <= i

    proof

      let i be natural Number;

      

       A0: i is Nat by TARSKI: 1;

      defpred P[ natural Number] means 0 <= $1;

      

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

      

       A2: P[ 0 ];

      for k holds P[k] from NatInd( A2, A1);

      hence thesis by A0;

    end;

    theorem :: NAT_1:3

    for i be natural Number holds 0 <> i implies 0 < i by Th2;

    theorem :: NAT_1:4

    for i,j,h be natural Number holds i <= j implies (i * h) <= (j * h)

    proof

      let i,j,h be natural Number;

       0 <= h by Th2;

      hence thesis by XREAL_1: 64;

    end;

    theorem :: NAT_1:5

    for i be natural Number holds 0 < (i + 1)

    proof

      let i be natural Number;

       0 <= i by Th2;

      hence thesis;

    end;

    theorem :: NAT_1:6

    

     Th6: for i be natural Number holds i = 0 or ex k st i = (k + 1)

    proof

      let i be natural Number;

      

       A0: i is Nat by TARSKI: 1;

      defpred P[ natural Number] means $1 = 0 or ex k st $1 = (k + 1);

      

       A1: P[h] implies P[(h + 1)];

      

       A2: P[ 0 ];

      for i holds P[i] from NatInd( A2, A1);

      hence thesis by A0;

    end;

    theorem :: NAT_1:7

    

     Th7: for i,j be natural Number holds (i + j) = 0 implies i = 0 & j = 0

    proof

      let i,j be natural Number;

       0 <= i & 0 <= j by Th2;

      hence thesis;

    end;

    registration

      cluster zero natural for object;

      existence

      proof

        take 0 ;

        thus thesis;

      end;

      cluster non zero natural for object;

      existence

      proof

        take 1;

        thus thesis;

      end;

    end

    registration

      let m be natural Number, n be non zero natural Number;

      cluster (m + n) -> non zero;

      coherence by Th7;

      cluster (n + m) -> non zero;

      coherence ;

    end

    scheme :: NAT_1:sch3

    DefbyInd { N() -> Nat , F( Nat, Nat) -> Nat , P[ Nat, Nat] } :

(for k be Nat holds ex n be Nat st P[k, n]) & for k,n,m be Nat st P[k, n] & P[k, m] holds n = m

      provided

       A1: for k,n be Nat holds P[k, n] iff k = 0 & n = N() or ex m,l be Nat st k = (m + 1) & P[m, l] & n = F(k,l);

      reconsider N = N() as Element of NAT by ORDINAL1:def 12;

      defpred P[ Nat] means ex n be Nat st P[$1, n];

      

       A2: for k be Nat holds P[k] implies P[(k + 1)]

      proof

        let k be Nat;

        given n be Nat such that

         A3: P[k, n];

        reconsider F = F(+,n) as Element of NAT by ORDINAL1:def 12;

        take F;

        thus thesis by A1, A3;

      end;

      P[ 0 , N] by A1;

      then

       A4: P[ 0 ];

      thus for k be Nat holds P[k] from NatInd( A4, A2);

      defpred P[ Nat] means for n,m be Nat st P[$1, n] & P[$1, m] holds n = m;

      

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

      proof

        let k be Nat such that

         A6: for n,m be Nat st P[k, n] & P[k, m] holds n = m;

        let n,m be Nat;

        assume P[(k + 1), n] & P[(k + 1), m];

        then (ex l,u be Nat st (k + 1) = (l + 1) & P[l, u] & n = F(+,u)) & ex v,w be Nat st (k + 1) = (v + 1) & P[v, w] & m = F(+,w) by A1;

        hence thesis by A6;

      end;

      

       A7: P[ 0 ]

      proof

        let n,m be Nat such that

         A8: P[ 0 , n] and

         A9: P[ 0 , m];

         not ex m,l be Nat st 0 = (m + 1) & P[m, l] & n = F(0,l);

        then ( not ex n,l be Nat st 0 = (n + 1) & P[n, l] & m = F(0,l)) & n = N() by A1, A8;

        hence thesis by A1, A9;

      end;

      thus for k be Nat holds P[k] from NatInd( A7, A5);

    end;

    theorem :: NAT_1:8

    

     Th8: for i,j be natural Number holds i <= (j + 1) implies i <= j or i = (j + 1)

    proof

      let i,j be natural Number;

      

       A0: i is Nat & j is Nat by TARSKI: 1;

      defpred P[ natural Number] means for j holds $1 <= (j + 1) implies $1 <= j or $1 = (j + 1);

      

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

      proof

        let i such that

         A2: for j holds i <= (j + 1) implies i <= j or i = (j + 1);

        let j;

        assume

         A3: (i + 1) <= (j + 1);

         A4:

        now

          given k such that

           A5: j = (k + 1);

          i <= (k + 1) by A3, A5, XREAL_1: 6;

          hence thesis by A2, A5, XREAL_1: 6;

        end;

        now

          

           A6: 0 <= i by Th2;

          assume

           A7: j = 0 ;

          then i <= 0 by A3, XREAL_1: 6;

          hence thesis by A7, A6;

        end;

        hence thesis by A4, Th6;

      end;

      

       A8: P[ 0 ] by Th2;

      for i holds P[i] from NatInd( A8, A1);

      hence thesis by A0;

    end;

    theorem :: NAT_1:9

    for i,j be natural Number holds i <= j & j <= (i + 1) implies i = j or j = (i + 1)

    proof

      let i,j be natural Number;

      assume that

       A1: i <= j and

       A2: j <= (i + 1);

      j <= i or j = (i + 1) by A2, Th8;

      hence thesis by A1, XXREAL_0: 1;

    end;

    theorem :: NAT_1:10

    

     Th10: for i,j be natural Number holds i <= j implies ex k st j = (i + k)

    proof

      let i,j be natural Number;

      

       A0: j is Nat by TARSKI: 1;

      defpred P[ Nat] means i <= $1 implies ex k st $1 = (i + k);

      

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

      proof

        let j such that

         A2: i <= j implies ex k st j = (i + k);

         A3:

        now

          assume i <= j;

          then

          consider k such that

           A4: j = (i + k) by A2;

          ((i + k) + 1) = (i + (k + 1));

          hence thesis by A4;

        end;

         A5:

        now

          assume i = (j + 1);

          then (j + 1) = (i + 0 );

          hence thesis;

        end;

        assume i <= (j + 1);

        hence thesis by A3, A5, Th8;

      end;

      

       A6: P[ 0 ]

      proof

        assume

         A7: i <= 0 ;

        take 0 ;

        thus thesis by A7, Th2;

      end;

      for j holds P[j] from NatInd( A6, A1);

      hence thesis by A0;

    end;

    theorem :: NAT_1:11

    

     Th11: for i,j be natural Number holds i <= (i + j)

    proof

      let i,j be natural Number;

      ( 0 + i) = i & 0 <= j by Th2;

      hence thesis by XREAL_1: 7;

    end;

    scheme :: NAT_1:sch4

    CompInd { P[ Nat] } :

for k be Nat holds P[k]

      provided

       A1: for k be Nat st for n be Nat st n < k holds P[n] holds P[k];

      let k be Nat;

      defpred P1[ Nat] means for n be Nat st n < $1 holds P[n];

      

       A2: for k be Nat holds P1[k] implies P1[(k + 1)]

      proof

        let k be Nat;

        assume

         A3: for n be Nat st n < k holds P[n];

        let n be Nat;

        assume n < (k + 1);

        then n <= k by Th8;

        then n < k or n = k & n <= k by XXREAL_0: 1;

        hence thesis by A1, A3;

      end;

      

       A4: P1[ 0 ] by Th2;

      for k be Nat holds P1[k] from NatInd( A4, A2);

      then for n be Nat st n < k holds P[n];

      hence thesis by A1;

    end;

    scheme :: NAT_1:sch5

    Min { P[ Nat] } :

ex k be Nat st P[k] & for n be Nat st P[n] holds k <= n

      provided

       A1: ex k be Nat st P[k];

      defpred P1[ Nat] means not P[$1];

      assume

       A2: not thesis;

      

       A3: for k be Nat st for n be Nat st n < k holds P1[n] holds P1[k]

      proof

        let k be Nat;

        assume

         A4: for n be Nat st n < k holds not P[n];

         not (ex n be Nat st P[n] & not k <= n) implies not P[k] by A2;

        hence thesis by A4;

      end;

      for k be Nat holds P1[k] from CompInd( A3);

      hence contradiction by A1;

    end;

    scheme :: NAT_1:sch6

    Max { P[ Nat], N() -> Nat } :

ex k be Nat st P[k] & for n be Nat st P[n] holds n <= k

      provided

       A1: for k be Nat st P[k] holds k <= N()

       and

       A2: ex k be Nat st P[k];

      defpred P1[ Nat] means for n be Nat st P[n] holds n <= $1;

      

       A3: ex k be Nat st P1[k] by A1;

      consider k be Nat such that

       A4: P1[k] and

       A5: for m be Nat st P1[m] holds k <= m from Min( A3);

      take k;

      thus P[k]

      proof

        consider n be Nat such that

         A6: P[n] by A2;

        

         A7: n <= k by A4, A6;

        assume

         A8: not P[k];

        then n <> k by A6;

        then k <> 0 by A7, Th2;

        then

        consider m such that

         A9: k = (m + 1) by Th6;

        

         A10: for n be Nat st P[n] holds n <= m by A4, A8, A9, Th8;

        ((( - m) + m) + 1) = (( - m) + (m + 1));

        hence contradiction by A5, A9, A10, XREAL_1: 6;

      end;

      thus thesis by A4;

    end;

    theorem :: NAT_1:12

    

     Th12: for i,j,h be natural Number holds i <= j implies i <= (j + h)

    proof

      let i,j,h be natural Number;

      assume i <= j;

      then

       A1: (i + h) <= (j + h) by XREAL_1: 7;

       0 <= h by Th2;

      then (i + 0 ) <= (i + h) by XREAL_1: 7;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: NAT_1:13

    

     Th13: for i,j be natural Number holds i < (j + 1) iff i <= j

    proof

      let i,j be natural Number;

      thus i < (j + 1) implies i <= j by Th8;

      assume

       A1: i <= j;

       A2:

      now

        

         A3: (j + ( - j)) = 0 & ((j + 1) + ( - j)) = 1;

        assume i = (j + 1);

        hence contradiction by A1, A3, XREAL_1: 6;

      end;

      i <= (j + 1) by A1, Th12;

      hence thesis by A2, XXREAL_0: 1;

    end;

    theorem :: NAT_1:14

    

     Th14: for i be natural Number holds i < 1 implies i = 0

    proof

      let i be natural Number;

      assume i < 1;

      then i < ( 0 + 1);

      then i <= 0 by Th13;

      hence thesis by Th2;

    end;

    theorem :: NAT_1:15

    for i,j be natural Number holds (i * j) = 1 implies i = 1

    proof

      let i,j be natural Number;

      assume

       A1: (i * j) = 1;

      then i <> 0 ;

      then

      consider m such that

       A2: i = (m + 1) by Th6;

      j <> 0 by A1;

      then

      consider l such that

       A3: j = (l + 1) by Th6;

      

       A4: ((((m * l) + m) + l) + 1) = ( 0 + 1) by A1, A2, A3;

      then ((m * l) + m) = 0 ;

      hence thesis by A2, A4;

    end;

    theorem :: NAT_1:16

    

     Th16: for n,k be natural Number holds k <> 0 implies n < (n + k)

    proof

      let n,k be natural Number;

      assume k <> 0 ;

      then

       A1: n <> (n + k);

      n <= (n + k) by Th12;

      hence thesis by A1, XXREAL_0: 1;

    end;

    scheme :: NAT_1:sch7

    Regr { P[ Nat] } :

P[ 0 ]

      provided

       A1: ex k be Nat st P[k]

       and

       A2: for k be Nat st k <> 0 & P[k] holds ex n be Nat st n < k & P[n];

      consider k be Nat such that

       A3: P[k] & for n be Nat st P[n] holds k <= n from Min( A1);

      now

        assume k <> 0 ;

        then ex n be Nat st n < k & P[n] by A2, A3;

        hence contradiction by A3;

      end;

      hence thesis by A3;

    end;

    theorem :: NAT_1:17

     0 < m implies for n holds ex k, t st n = ((m * k) + t) & t < m

    proof

      defpred P[ Nat] means ex k, t st $1 = ((m * k) + t) & t < m;

      assume

       A1: 0 < m;

      

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

      proof

        let n;

        given k1, t1 such that

         A3: n = ((m * k1) + t1) and

         A4: t1 < m;

        

         A5: (t1 + 1) < m implies ex k, t st (n + 1) = ((m * k) + t) & t < m

        proof

          assume

           A6: (t1 + 1) < m;

          take k = k1, t = (t1 + 1);

          thus (n + 1) = ((m * k) + t) by A3;

          thus thesis by A6;

        end;

        

         A7: (t1 + 1) = m implies ex k, t st (n + 1) = ((m * k) + t) & t < m

        proof

          assume

           A8: (t1 + 1) = m;

          take k = (k1 + 1), t = 0 ;

          thus (n + 1) = ((m * k) + t) by A3, A8;

          thus thesis by A1;

        end;

        (t1 + 1) <= m by A4, Th13;

        hence thesis by A5, A7, XXREAL_0: 1;

      end;

       0 = ((m * 0 ) + 0 );

      then

       A9: P[ 0 ] by A1;

      thus for n holds P[n] from NatInd( A9, A2);

    end;

    theorem :: NAT_1:18

    for n,m,k,t,k1,t1 be natural Number holds n = ((m * k) + t) & t < m & n = ((m * k1) + t1) & t1 < m implies k = k1 & t = t1

    proof

      let n,m,k,t,k1,t1 be natural Number;

      assume that

       A1: n = ((m * k) + t) and

       A2: t < m and

       A3: n = ((m * k1) + t1) and

       A4: t1 < m;

       A5:

      now

        assume k1 <= k;

        then

        consider u be Nat such that

         A6: k = (k1 + u) by Th10;

        ((m * (k1 + u)) + t) = ((m * k1) + ((m * u) + t));

        then

         A7: ((m * u) + t) = t1 by A1, A3, A6, XCMPLX_1: 2;

        now

          given w be Nat such that

           A8: u = (w + 1);

          ((m * u) + t) = (m + ((m * w) + t)) by A8;

          hence contradiction by A4, A7, Th11;

        end;

        then

         A9: u = 0 by Th6;

        hence k = k1 by A6;

        thus t = t1 by A1, A3, A6, A9, XCMPLX_1: 2;

      end;

      now

        assume k <= k1;

        then

        consider u be Nat such that

         A10: k1 = (k + u) by Th10;

        ((m * (k + u)) + t1) = ((m * k) + ((m * u) + t1));

        then

         A11: ((m * u) + t1) = t by A1, A3, A10, XCMPLX_1: 2;

        now

          given w be Nat such that

           A12: u = (w + 1);

          ((m * u) + t1) = (m + ((m * w) + t1)) by A12;

          hence contradiction by A2, A11, Th11;

        end;

        then

         A13: u = 0 by Th6;

        hence k = k1 by A10;

        thus t = t1 by A1, A3, A10, A13, XCMPLX_1: 2;

      end;

      hence thesis by A5;

    end;

    registration

      cluster -> ordinal for natural Number;

      coherence

      proof

        let o be natural Number;

        o in omega by ORDINAL1:def 12;

        hence thesis;

      end;

    end

    registration

      cluster non empty ordinal for Subset of REAL ;

      existence by NUMBERS: 19;

    end

    theorem :: NAT_1:19

    for k,n be natural Number holds k < (k + n) iff 1 <= n

    proof

      let k,n be natural Number;

      thus k < (k + n) implies 1 <= n

      proof

        assume

         A1: k < (k + n);

        assume not 1 <= n;

        then n = 0 by Th14;

        hence thesis by A1;

      end;

      assume 1 <= n;

      hence thesis by Th16;

    end;

    theorem :: NAT_1:20

    for k,n be natural Number holds k < n implies (n - 1) is Element of NAT

    proof

      let k,n be natural Number;

      assume k < n;

      then (k + 1) <= n by Th13;

      then

      consider j be Nat such that

       A1: n = ((k + 1) + j) by Th10;

      (n - 1) = (k + j) by A1;

      hence thesis by ORDINAL1:def 12;

    end;

    theorem :: NAT_1:21

    for k,n be natural Number holds k <= n implies (n - k) is Element of NAT

    proof

      let k,n be natural Number;

      assume

       A1: k <= n;

      per cases by A1, XXREAL_0: 1;

        suppose k < n;

        then (k + 1) <= n by Th13;

        then

        consider j be Nat such that

         A2: n = ((k + 1) + j) by Th10;

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

        (n - k) = (1 + j) by A2;

        hence thesis;

      end;

        suppose k = n;

        then (n - k) = 0 ;

        hence thesis;

      end;

    end;

    begin

    theorem :: NAT_1:22

    

     Th22: for m,n be natural Number holds m < (n + 1) implies m < n or m = n

    proof

      let m,n be natural Number;

      assume m < (n + 1);

      then m <= n by Th13;

      hence thesis by XXREAL_0: 1;

    end;

    theorem :: NAT_1:23

    for k be natural Number holds k < 2 implies k = 0 or k = 1

    proof

      let k be natural Number;

      assume k < 2;

      then k < (1 + 1);

      hence thesis by Th14, Th22;

    end;

    registration

      cluster non zero for Element of NAT ;

      existence

      proof

        take 1;

        thus thesis;

      end;

    end

    registration

      cluster -> non negative for Element of NAT ;

      coherence by Th2;

    end

    registration

      cluster -> non negative for natural Number;

      coherence by Th2;

    end

    theorem :: NAT_1:24

    for i,j,h be natural Number holds i <> 0 & h = (j * i) implies j <= h

    proof

      let i,j,h be natural Number;

      assume i <> 0 ;

      then

      consider k such that

       A1: i = (k + 1) by Th6;

      assume h = (j * i);

      then h = ((j * k) + (j * 1)) by A1;

      hence thesis by Th11;

    end;

    scheme :: NAT_1:sch8

    Ind1 { M() -> Nat , P[ Nat] } :

for i be Nat st M() <= i holds P[i]

      provided

       A1: P[M()]

       and

       A2: for j be Nat st M() <= j holds P[j] implies P[(j + 1)];

      defpred Q[ Nat] means P[(M() + $1)];

       A3:

      now

        let m be Nat;

        assume Q[m];

        then P[((M() + m) + 1)] by A2, Th11;

        hence Q[(m + 1)];

      end;

      let i;

      assume M() <= i;

      then

      consider m be Nat such that

       A4: i = (M() + m) by Th10;

      

       A5: Q[ 0 ] by A1;

      for m be Nat holds Q[m] from NatInd( A5, A3);

      hence thesis by A4;

    end;

    scheme :: NAT_1:sch9

    CompInd1 { a() -> Nat , P[ Nat] } :

for k be Nat st k >= a() holds P[k]

      provided

       A1: for k be Nat st k >= a() & (for n be Nat st n >= a() & n < k holds P[n]) holds P[k];

      defpred P1[ Nat] means for n be Nat st (n >= a() & n < $1) holds P[n];

      

       A2: for k be Nat st k >= a() holds P1[k] implies P1[(k + 1)]

      proof

        let k be Nat;

        assume k >= a();

        assume

         A3: for n be Nat st n >= a() & n < k holds P[n];

        let n be Nat;

        assume that

         A4: n >= a() and

         A5: n < (k + 1);

        n <= k by A5, Th13;

        then n < k or n = k by XXREAL_0: 1;

        hence thesis by A1, A3, A4;

      end;

      let k be Nat;

      assume

       A6: k >= a();

      

       A7: P1[a()];

      for k be Nat st k >= a() holds P1[k] from Ind1( A7, A2);

      then for n be Nat st n >= a() & n < k holds P[n] by A6;

      hence thesis by A1, A6;

    end;

    theorem :: NAT_1:25

    for n be natural Number holds n <= 1 implies n = 0 or n = 1

    proof

      let n be natural Number;

      assume

       A1: n <= 1;

      assume that

       A2: not n = 0 and

       A3: not n = 1;

      n < ( 0 + 1) by A1, A3, XXREAL_0: 1;

      hence contradiction by A2, Th13;

    end;

    scheme :: NAT_1:sch10

    Indfrom1 { P[ Nat] } :

for k be non zero Nat holds P[k]

      provided

       A1: P[1]

       and

       A2: for k be non zero Nat st P[k] holds P[(k + 1)];

      defpred P[ Nat] means $1 is non zero implies P[$1];

       A3:

      now

        let k be Nat;

        assume

         A4: P[k];

        now

          assume (k + 1) is non zero;

          k = 0 or k is non zero;

          hence P[(k + 1)] by A1, A2, A4;

        end;

        hence P[(k + 1)];

      end;

      

       A5: P[ 0 ];

      for k be Nat holds P[k] from NatInd( A5, A3);

      hence thesis;

    end;

    definition

      let A be set;

      :: NAT_1:def1

      func min* A -> Element of NAT means

      : Def1: it in A & for k st k in A holds it <= k if A is non empty Subset of NAT

      otherwise it = 0 ;

      existence

      proof

        A is non empty Subset of NAT implies ex i st i in A & for k be Nat st k in A holds i <= k

        proof

          defpred P[ Nat] means $1 in A;

          set x = the Element of A;

          assume

           A1: A is non empty Subset of NAT ;

          then x is Element of NAT by TARSKI:def 3;

          then

           A2: ex k be Nat st P[k] by A1;

          ex k be Nat st P[k] & for i be Nat st P[i] holds k <= i from Min( A2);

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let i,n be Element of NAT ;

        A is non empty Subset of NAT & (i in A & for k st k in A holds i <= k) & (n in A & for k st k in A holds n <= k) implies i = n

        proof

          assume that A is non empty Subset of NAT and

           A3: i in A & (for k st k in A holds i <= k) & n in A & for k st k in A holds n <= k;

          i <= n & n <= i by A3;

          hence thesis by XXREAL_0: 1;

        end;

        hence thesis;

      end;

      consistency ;

    end

    reserve x for object,

X,Y,Z for set;

    ::$Canceled

    theorem :: NAT_1:38

    

     Th26: for n be Nat holds ( succ ( Segm n)) = ( Segm (n + 1))

    proof

      let n be Nat;

      

       A1: (n + 1) = { L where L be Nat : L < (n + 1) } by AXIOMS: 4;

      

       A2: n = { K where K be Nat : K < n } by AXIOMS: 4;

      thus ( succ ( Segm n)) c= ( Segm (n + 1))

      proof

        let x be object such that

         A3: x in ( succ ( Segm n));

        per cases by A3, ORDINAL1: 8;

          suppose x in ( Segm n);

          then

          consider K be Nat such that

           A4: x = K and

           A5: K < n by A2;

          K < (n + 1) by A5, Th13;

          hence thesis by A1, A4;

        end;

          suppose

           A6: x = n;

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

          n < (n + 1) by Th13;

          hence thesis by A1, A6;

        end;

      end;

      let x be object;

      assume x in ( Segm (n + 1));

      then

      consider K be Nat such that

       A7: x = K and

       A8: K < (n + 1) by A1;

      K <= n by A8, Th13;

      then K = n or K < n by XXREAL_0: 1;

      then x = n or x in ( Segm n) by A2, A7;

      hence thesis by ORDINAL1: 8;

    end;

    theorem :: NAT_1:39

    

     Th27: n <= m iff ( Segm n) c= ( Segm m)

    proof

      defpred P[ Nat] means for m holds $1 <= m iff ( Segm $1) c= ( Segm m);

      

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

      proof

        let n such that

         A2: P[n];

        let m;

        thus (n + 1) <= m implies ( Segm (n + 1)) c= ( Segm m)

        proof

          assume (n + 1) <= m;

          then

          consider k be Nat such that

           A3: m = ((n + 1) + k) by Th10;

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

          ( Segm n) c= ( Segm (n + k)) by A2, Th11;

          then

           A4: ( succ ( Segm n)) c= ( succ ( Segm (n + k))) by ORDINAL2: 1;

          ( Segm ((n + k) + 1)) = ( succ ( Segm (n + k))) by Th26;

          hence thesis by A3, A4, Th26;

        end;

        assume

         A5: ( Segm (n + 1)) c= ( Segm m);

        ( Segm (n + 1)) = ( succ ( Segm n)) by Th26;

        then

         A6: n in ( Segm m) by A5, ORDINAL1: 21;

        then

         A7: n <= m by A2, ORDINAL1:def 2;

        reconsider nn = n as set;

        n <> m by A6;

        then n < m by A7, XXREAL_0: 1;

        hence thesis by Th13;

      end;

      

       A8: P[ 0 ];

      for n holds P[n] from NatInd( A8, A1);

      hence thesis;

    end;

    theorem :: NAT_1:40

    ( card ( Segm n)) c= ( card ( Segm m)) iff n <= m by Th27;

    theorem :: NAT_1:41

    

     Th29: ( card ( Segm n)) in ( card ( Segm m)) iff n < m

    proof

      ( card ( Segm n)) c< ( card ( Segm m)) iff ( card ( Segm n)) c= ( card ( Segm m)) & ( card ( Segm n)) <> ( card ( Segm m));

      hence thesis by Th27, ORDINAL1: 11, ORDINAL1:def 2;

    end;

    reserve M,N for Cardinal;

    theorem :: NAT_1:42

    ( nextcard ( card ( Segm n))) = ( card ( Segm (n + 1)))

    proof

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

      

       A1: for M st ( card ( card n)) in M holds ( card (n + 1)) c= M

      proof

        let M;

        assume

         A2: ( card ( card n)) in M;

        ( Segm (n + 1)) = ( succ ( Segm n)) by Th26;

        hence thesis by A2, ORDINAL1: 21;

      end;

      n < (n + 1) by Th13;

      hence thesis by A1, Th29, CARD_1:def 3;

    end;

    ::$Canceled

    theorem :: NAT_1:43

    for X,Y be finite set holds X c= Y implies ( card X) <= ( card Y)

    proof

      let X,Y be finite set;

      assume X c= Y;

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

      hence ( card X) <= ( card Y) by Th27;

    end;

    theorem :: NAT_1:44

    

     Th32: for k,n be natural Number holds k in ( Segm n) iff k < n

    proof

      let k,n be natural Number;

      hereby

        assume k in ( Segm n);

        then k in { l where l be Nat : l < n } by AXIOMS: 4;

        then ex l be Nat st k = l & l < n;

        hence k < n;

      end;

      assume

       A1: k < n;

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

      k in { l where l be Nat : l < n } by A1;

      hence thesis by AXIOMS: 4;

    end;

    theorem :: NAT_1:45

    for n be natural Number holds n in ( Segm (n + 1))

    proof

      let n be natural Number;

      

       A1: n is Nat by TARSKI: 1;

      n < (n + 1) by XREAL_1: 29;

      then n in { l where l be Nat : l < (n + 1) } by A1;

      hence thesis by AXIOMS: 4;

    end;

    ::$Canceled

    definition

      let X be set;

      mode sequence of X is Function of NAT , X;

    end

    scheme :: NAT_1:sch11

    LambdaRecEx { A() -> object , G( object, object) -> object } :

ex f be Function st ( dom f) = NAT & (f . 0 ) = A() & for n be Nat holds (f . (n + 1)) = G(n,.);

      deffunc D( set, set) = {} ;

      consider L be Sequence such that

       A1: ( dom L) = NAT and

       A2: 0 in NAT implies (L . 0 ) = A() and

       A3: for A be Ordinal st ( succ A) in NAT holds (L . ( succ A)) = G(A,.) and for A be Ordinal st A in NAT & A <> 0 & A is limit_ordinal holds (L . A) = D(A,|) from ORDINAL2:sch 5;

      take L;

      thus ( dom L) = NAT by A1;

      thus (L . 0 ) = A() by A2;

      let n be Nat;

      

      thus (L . (n + 1)) = (L . ( Segm (n + 1)))

      .= (L . ( succ ( Segm n))) by Th26

      .= G(n,.) by A3, ORDINAL1:def 12;

    end;

    scheme :: NAT_1:sch12

    LambdaRecExD { D() -> non empty set , A() -> Element of D() , G( object, object) -> Element of D() } :

ex f be sequence of D() st (f . 0 ) = A() & for n be Nat holds (f . (n + 1)) = G(n,.);

      consider f be Function such that

       A1: ( dom f) = NAT and

       A2: (f . 0 ) = A() and

       A3: for n be Nat holds (f . (n + 1)) = G(n,.) from LambdaRecEx;

      for x be object st x in NAT holds (f . x) in D()

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider n = x as Nat;

        per cases by Th6;

          suppose n = 0 ;

          hence thesis by A2;

        end;

          suppose ex k st n = (k + 1);

          then

          consider k such that

           A4: n = (k + 1);

          (f . n) = G(k,.) by A3, A4;

          hence thesis;

        end;

      end;

      then

      reconsider f as sequence of D() by A1, FUNCT_2: 3;

      take f;

      thus thesis by A2, A3;

    end;

    scheme :: NAT_1:sch13

    RecUn { A() -> object , F,G() -> Function , P[ object, object, object] } :

F() = G()

      provided

       A1: ( dom F()) = NAT

       and

       A2: (F() . 0 ) = A()

       and

       A3: for n holds P[n, (F() . n), (F() . (n + 1))]

       and

       A4: ( dom G()) = NAT

       and

       A5: (G() . 0 ) = A()

       and

       A6: for n holds P[n, (G() . n), (G() . (n + 1))]

       and

       A7: for n holds for x,y1,y2 be set st P[n, x, y1] & P[n, x, y2] holds y1 = y2;

      defpred P[ Nat] means (F() . $1) = (G() . $1);

      

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

      proof

        let n;

        assume (F() . n) = (G() . n);

        then

         A9: P[n, (F() . n), (G() . (n + 1))] by A6;

        P[n, (F() . n), (F() . (n + 1))] by A3;

        hence thesis by A7, A9;

      end;

      

       A10: P[ 0 ] by A2, A5;

      for n holds P[n] from NatInd( A10, A8);

      then for x be object st x in NAT holds (F() . x) = (G() . x);

      hence thesis by A1, A4, FUNCT_1: 2;

    end;

    scheme :: NAT_1:sch14

    RecUnD { D() -> non empty set , A() -> Element of D() , P[ object, object, object], F,G() -> sequence of D() } :

F() = G()

      provided

       A1: (F() . 0 ) = A()

       and

       A2: for n holds P[n, (F() . n), (F() . (n + 1))]

       and

       A3: (G() . 0 ) = A()

       and

       A4: for n holds P[n, (G() . n), (G() . (n + 1))]

       and

       A5: for n be Nat, x,y1,y2 be Element of D() st P[n, x, y1] & P[n, x, y2] holds y1 = y2;

      defpred Q[ Nat] means (F() . $1) <> (G() . $1);

      

       A6: ( dom F()) = NAT & ( dom G()) = NAT by FUNCT_2:def 1;

      assume F() <> G();

      then ex x be object st x in NAT & (F() . x) <> (G() . x) by A6, FUNCT_1: 2;

      then

       A7: ex k be Nat st Q[k];

      consider m be Nat such that

       A8: Q[m] & for n be Nat st Q[n] holds m <= n from Min( A7);

      now

        assume m <> 0 ;

        then

        consider k be Nat such that

         A9: m = (k + 1) by Th6;

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

        k < m by A9, Th13;

        then

         A10: (F() . k) = (G() . k) by A8;

        P[k, (F() . k), (F() . (k + 1))] & P[k, (G() . k), (G() . (k + 1))] by A2, A4;

        hence contradiction by A5, A8, A9, A10;

      end;

      hence contradiction by A1, A3, A8;

    end;

    scheme :: NAT_1:sch15

    LambdaRecUn { A() -> object , RecFun( object, object) -> object , F,G() -> Function } :

F() = G()

      provided

       A1: ( dom F()) = NAT

       and

       A2: (F() . 0 ) = A()

       and

       A3: for n holds (F() . (n + 1)) = RecFun(n,.)

       and

       A4: ( dom G()) = NAT

       and

       A5: (G() . 0 ) = A()

       and

       A6: for n holds (G() . (n + 1)) = RecFun(n,.);

      defpred P[ Nat, set, set] means $3 = RecFun($1,$2);

      

       A7: for n holds P[n, (G() . n), (G() . (n + 1))] by A6;

      

       A8: for n be Nat, x,y1,y2 be set st P[n, x, y1] & P[n, x, y2] holds y1 = y2;

      

       A9: for n holds P[n, (F() . n), (F() . (n + 1))] by A3;

      thus F() = G() from RecUn( A1, A2, A9, A4, A5, A7, A8);

    end;

    scheme :: NAT_1:sch16

    LambdaRecUnD { D() -> non empty set , A() -> Element of D() , RecFun( object, object) -> Element of D() , F,G() -> sequence of D() } :

F() = G()

      provided

       A1: (F() . 0 ) = A()

       and

       A2: for n holds (F() . (n + 1)) = RecFun(n,.)

       and

       A3: (G() . 0 ) = A()

       and

       A4: for n holds (G() . (n + 1)) = RecFun(n,.);

      defpred P[ Nat, set, set] means $3 = RecFun($1,$2);

      

       A5: for n holds P[n, (G() . n), (G() . (n + 1))] by A4;

      

       A6: for n be Nat, x,y1,y2 be Element of D() st P[n, x, y1] & P[n, x, y2] holds y1 = y2;

      

       A7: for n holds P[n, (F() . n), (F() . (n + 1))] by A2;

      thus F() = G() from RecUnD( A1, A7, A3, A5, A6);

    end;

    registration

      let x,y be natural Number;

      cluster ( min (x,y)) -> natural;

      coherence by XXREAL_0: 15;

      cluster ( max (x,y)) -> natural;

      coherence by XXREAL_0: 16;

    end

    definition

      let x,y be Element of NAT ;

      :: original: min

      redefine

      func min (x,y) -> Element of NAT ;

      coherence by XXREAL_0: 15;

      :: original: max

      redefine

      func max (x,y) -> Element of NAT ;

      coherence by XXREAL_0: 16;

    end

    scheme :: NAT_1:sch17

    MinIndex { F( Nat) -> Nat } :

ex k st F(k) = 0 & for n st F(n) = 0 holds k <= n

      provided

       A1: for k holds (F(+) < F(k) or F(k) = 0 );

      defpred X[ Nat] means F($1) = 0 ;

      defpred P[ Nat] means ex n be Nat st $1 = F(n);

      

       A2: for k be Nat st k <> 0 & P[k] holds ex m be Nat st m < k & P[m]

      proof

        let k be Nat;

        assume that

         A3: k <> 0 and

         A4: P[k];

        consider n be Nat such that

         A5: k = F(n) by A4;

        take IT = F(+);

        thus thesis by A1, A3, A5;

      end;

      F(0) is Nat;

      then

       A6: ex k be Nat st P[k];

       P[ 0 ] from Regr( A6, A2);

      then

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

      consider k be Nat such that

       A8: X[k] & for n be Nat st X[n] holds k <= n from Min( A7);

      take k;

      thus thesis by A8;

    end;

    definition

      let s be ManySortedSet of NAT , k be natural Number;

      :: NAT_1:def2

      func s ^\ k -> ManySortedSet of NAT means

      : Def2: for n be Nat holds (it . n) = (s . (n + k));

      existence

      proof

        defpred P[ object, object] means ex n be Element of NAT st n = $1 & $2 = (s . (n + k));

        

         A1: for i be object st i in NAT holds ex j be object st P[i, j]

        proof

          let i be object;

          assume i in NAT ;

          then

          reconsider n = i as Element of NAT ;

          take j = (s . (n + k));

          thus P[i, j];

        end;

        consider f be ManySortedSet of NAT such that

         A2: for i be object st i in NAT holds P[i, (f . i)] from PBOOLE:sch 3( A1);

        take f;

        let n be Nat;

         P[n, (f . n)] by A2, ORDINAL1:def 12;

        hence thesis;

      end;

      uniqueness

      proof

        let s1,s2 be ManySortedSet of NAT ;

        assume that

         A3: for n holds (s1 . n) = (s . (n + k)) and

         A4: for n holds (s2 . n) = (s . (n + k));

        now

          let n be object;

          assume n in NAT ;

          then

          reconsider nn = n as Element of NAT ;

          

          thus (s1 . n) = (s . (nn + k)) by A3

          .= (s2 . n) by A4;

        end;

        hence s1 = s2 by PBOOLE: 3;

      end;

    end

    

     Lm1: for s be ManySortedSet of NAT , k be natural Number holds ( rng (s ^\ k)) c= ( rng s)

    proof

      let s be ManySortedSet of NAT , k be natural Number;

      let i be object;

      assume i in ( rng (s ^\ k));

      then

      consider u be object such that

       A1: u in ( dom (s ^\ k)) and

       A2: i = ((s ^\ k) . u) by FUNCT_1:def 3;

      reconsider n = u as Element of NAT by A1, PARTFUN1:def 2;

      

       A3: ( dom s) = NAT by PARTFUN1:def 2;

      i = (s . (n + k)) by A2, Def2;

      hence i in ( rng s) by A3, FUNCT_1: 3, ORDINAL1:def 12;

    end;

    registration

      let X be non empty set, s be X -valued ManySortedSet of NAT , k be natural Number;

      cluster (s ^\ k) -> X -valued;

      coherence

      proof

        

         A1: ( rng (s ^\ k)) c= ( rng s) by Lm1;

        ( rng s) c= X by RELAT_1:def 19;

        hence ( rng (s ^\ k)) c= X by A1;

      end;

    end

    definition

      let X be non empty set, s be sequence of X, k be Nat;

      :: original: ^\

      redefine

      func s ^\ k -> sequence of X ;

      coherence

      proof

        ( rng (s ^\ k)) c= X & ( dom (s ^\ k)) = NAT by PARTFUN1:def 2, RELAT_1:def 19;

        hence (s ^\ k) is sequence of X by RELSET_1: 4;

      end;

    end

    reserve X for non empty set,

s for sequence of X;

    theorem :: NAT_1:47

    (s ^\ 0 ) = s

    proof

      now

        let n be Element of NAT ;

        

        thus ((s ^\ 0 ) . n) = (s . (n + 0 )) by Def2

        .= (s . n);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: NAT_1:48

    

     Th35: ((s ^\ k) ^\ m) = (s ^\ (k + m))

    proof

      now

        let n be Element of NAT ;

        

        thus (((s ^\ k) ^\ m) . n) = ((s ^\ k) . (n + m)) by Def2

        .= (s . ((n + m) + k)) by Def2

        .= (s . (n + (k + m)))

        .= ((s ^\ (k + m)) . n) by Def2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: NAT_1:49

    ((s ^\ k) ^\ m) = ((s ^\ m) ^\ k)

    proof

      

      thus ((s ^\ k) ^\ m) = (s ^\ (k + m)) by Th35

      .= ((s ^\ m) ^\ k) by Th35;

    end;

    registration

      let N be sequence of NAT ;

      let X, s;

      cluster (s * N) -> Function-like NAT -definedX -valued;

      coherence ;

    end

    registration

      let N be sequence of NAT ;

      let X, s;

      cluster (s * N) -> total;

      coherence ;

    end

    theorem :: NAT_1:50

    for N be sequence of NAT holds ((s * N) ^\ k) = (s * (N ^\ k))

    proof

      let N be sequence of NAT ;

      now

        let n be Element of NAT ;

        

        thus (((s * N) ^\ k) . n) = ((s * N) . (n + k)) by Def2

        .= (s . (N . (n + k))) by FUNCT_2: 15, ORDINAL1:def 12

        .= (s . ((N ^\ k) . n)) by Def2

        .= ((s * (N ^\ k)) . n) by FUNCT_2: 15;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: NAT_1:51

    (s . n) in ( rng s)

    proof

      n in NAT by ORDINAL1:def 12;

      then n in ( dom s) by FUNCT_2:def 1;

      hence thesis by FUNCT_1: 3;

    end;

    theorem :: NAT_1:52

    (for n holds (s . n) in Y) implies ( rng s) c= Y

    proof

      assume

       A1: for n holds (s . n) in Y;

      let y be object;

      assume y in ( rng s);

      then

      consider x be object such that

       A2: x in ( dom s) and

       A3: y = (s . x) by FUNCT_1:def 3;

      x in NAT by A2, FUNCT_2:def 1;

      hence thesis by A1, A3;

    end;

    theorem :: NAT_1:53

    for n be natural Number holds n is non zero implies n = 1 or n > 1

    proof

      let n be natural Number;

      assume n is non zero;

      then ( 0 + 1) <= n by Th13;

      hence n = 1 or n > 1 by XXREAL_0: 1;

    end;

    theorem :: NAT_1:54

    ( succ ( Segm n)) = { l where l be Nat : l <= n }

    proof

      thus ( succ ( Segm n)) c= { k : k <= n }

      proof

        let x be object;

        assume

         A1: x in ( succ ( Segm n));

        then x in ( Segm ( succ ( Segm n)));

        then

        reconsider k = x as Nat;

        x in ( Segm n) or x in {n} by A1, XBOOLE_0:def 3;

        then k < n or k = n by Th32, TARSKI:def 1;

        hence thesis;

      end;

      let x be object;

      assume x in { k : k <= n };

      then

      consider k such that

       A2: x = k and

       A3: k <= n;

      k < n or k = n by A3, XXREAL_0: 1;

      then k in ( Segm n) or k in {n} by Th32, TARSKI:def 1;

      hence thesis by A2, XBOOLE_0:def 3;

    end;

    registration

      let n be natural Number;

      reduce ( In (n, NAT )) to n;

      reducibility by ORDINAL1:def 12, SUBSET_1:def 8;

    end

    scheme :: NAT_1:sch18

    MinPred { F( Nat) -> Nat , P[ object] } :

ex k be Nat st P[k] & for n be Nat st P[n] holds k <= n

      provided

       A1: for k be Nat holds F(+) < F(k) or P[k];

      now

        deffunc G( Nat) = ( In (F($1), NAT ));

        consider f be sequence of NAT such that

         A2: for k be Element of NAT holds (f . k) = G(k) from FUNCT_2:sch 4;

        

         A3: (f . 0 ) in ( rng f) by FUNCT_2: 4;

        ( rng f) c= NAT

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A4: y in ( dom f) & x = (f . y) by FUNCT_1:def 3;

          reconsider y1 = y as Element of NAT by A4, FUNCT_2:def 1;

          x = G(y1) by A4, A2;

          hence thesis;

        end;

        then

        reconsider rf = ( rng f) as non empty Subset of NAT by A3;

        set m = ( min* rf);

        m in rf by Def1;

        then

        consider x be object such that

         A5: x in ( dom f) and

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

        reconsider x as Element of NAT by A5, FUNCT_2:def 1;

        (f . x) = G(x) & (f . (x + 1)) = G(+) by A2;

        then

         A7: (f . (x + 1)) < (f . x) or P[x] by A1;

        assume

         A8: for k holds not P[k];

        (f . (x + 1)) in rf by FUNCT_2: 4;

        hence contradiction by Def1, A8, A6, A7;

      end;

      then

       A9: ex k be Nat st P[k];

      consider k be Nat such that

       A10: P[k] & for n be Nat st P[n] holds k <= n from Min( A9);

      take k;

      thus thesis by A10;

    end;

    registration

      let k be Ordinal, x be object;

      cluster (k --> x) -> Sequence-like;

      coherence by FUNCOP_1: 13;

    end

    theorem :: NAT_1:55

    for s be ManySortedSet of NAT , k be natural Number holds ( rng (s ^\ k)) c= ( rng s) by Lm1;

    ::$Canceled

    theorem :: NAT_1:59

    for X be finite set st 1 < ( card X) holds ex x1,x2 be set st x1 in X & x2 in X & x1 <> x2

    proof

      let X be finite set;

      set x1 = the Element of X;

      assume

       A1: 1 < ( card X);

      then X <> {} ;

      then

       A2: x1 in X;

      now

        assume

         A3: for x2 be set st x2 in X holds x2 = x1;

        now

          let x be object;

          hereby

            assume x in X;

            then x = x1 by A3;

            hence x in {x1} by TARSKI:def 1;

          end;

          assume x in {x1};

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

        end;

        then X = {x1} by TARSKI: 2;

        hence contradiction by A1, CARD_1: 30;

      end;

      hence thesis;

    end;

    theorem :: NAT_1:60

    k <= n implies k = 0 or ... or k = n

    proof

      thus thesis;

    end;

    theorem :: NAT_1:61

    x in ( Segm (n + 1)) implies x = 0 or ... or x = n

    proof

      assume

       A1: x in ( Segm (n + 1));

      then

      reconsider k = x as Nat;

      k < (n + 1) by A1, Th32;

      then k <= n by Th13;

      hence thesis;

    end;

    theorem :: NAT_1:62

    m <= i & i <= (m + k) implies i = (m + 0 ) or ... or i = (m + k)

    proof

      assume that

       A1: m <= i and

       A2: i <= (m + k);

      take j = i;

      thus thesis by A1, A2;

    end;

    definition

      let D be set;

      let s be sequence of D, n be natural Number;

      :: original: .

      redefine

      func s . n -> Element of D ;

      coherence

      proof

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

        (s . n) is Element of D;

        hence thesis;

      end;

    end

    registration

      cluster zero -> non positive for natural Number;

      coherence ;

    end

    registration

      let A be non zero object;

      cluster {A} -> with_non-empty_elements;

      coherence by TARSKI:def 1;

      let B be non zero object;

      cluster {A, B} -> with_non-empty_elements;

      coherence by TARSKI:def 2;

      let C be non zero object;

      cluster {A, B, C} -> with_non-empty_elements;

      coherence by ENUMSET1:def 1;

      let D be non zero object;

      cluster {A, B, C, D} -> with_non-empty_elements;

      coherence by ENUMSET1:def 2;

      let E be non zero object;

      cluster {A, B, C, D, E} -> with_non-empty_elements;

      coherence by ENUMSET1:def 3;

      let F be non zero object;

      cluster {A, B, C, D, E, F} -> with_non-empty_elements;

      coherence by ENUMSET1:def 4;

      let G be non zero object;

      cluster {A, B, C, D, E, F, G} -> with_non-empty_elements;

      coherence by ENUMSET1:def 5;

      let H be non zero object;

      cluster {A, B, C, D, E, F, G, H} -> with_non-empty_elements;

      coherence by ENUMSET1:def 6;

      let I be non zero object;

      cluster {A, B, C, D, E, F, G, H, I} -> with_non-empty_elements;

      coherence by ENUMSET1:def 7;

      let J be non zero object;

      cluster {A, B, C, D, E, F, G, H, I, J} -> with_non-empty_elements;

      coherence by ENUMSET1:def 8;

    end

    registration

      cluster empty -> zero for set;

      coherence ;

      cluster non zero -> non empty for set;

      coherence ;

    end

    definition

      let G be non empty set;

      let B be Function of [:G, NAT :], G;

      let g be Element of G, i be Nat;

      :: original: .

      redefine

      func B . (g,i) -> Element of G ;

      coherence

      proof

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

        (B . (g,i)) is Element of G;

        hence thesis;

      end;

    end

    definition

      let G be non empty set;

      let B be Function of [: NAT , G:], G;

      let i be Nat, g be Element of G;

      :: original: .

      redefine

      func B . (i,g) -> Element of G ;

      coherence

      proof

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

        (B . (i,g)) is Element of G;

        hence thesis;

      end;

    end

    scheme :: NAT_1:sch19

    SeqEx2D { X,Z() -> non empty set , P[ set, set, set] } :

ex f be Function of [:X(), NAT :], Z() st for x be Element of X(), y be Nat holds P[x, y, (f . (x,y))]

      provided

       A1: for x be Element of X(), y be Nat holds ex z be Element of Z() st P[x, y, z];

      

       A2: for x be Element of X(), y be Element of NAT holds ex z be Element of Z() st P[x, y, z] by A1;

      consider f be Function of [:X(), NAT :], Z() such that

       A3: for x be Element of X(), y be Element of NAT holds P[x, y, (f . (x,y))] from BINOP_1:sch 3( A2);

      take f;

      let x be Element of X(), y be Nat;

      y in NAT by ORDINAL1:def 12;

      hence thesis by A3;

    end;

    theorem :: NAT_1:63

    for n be Nat holds ( Segm n) c= ( Segm (n + 1)) by Th11, Th27;