seqm_3.miz



    begin

    reserve n,m,k for Nat;

    reserve r,r1 for Real;

    reserve f,seq,seq1 for Real_Sequence;

    reserve x,y for set;

    

     Lm1: n < m implies ex k st m = ((n + 1) + k)

    proof

      assume

       A1: n < m;

      then

      consider k1 be Nat such that

       A2: m = (n + k1) by NAT_1: 10;

      k1 <> 0 by A1, A2;

      then

      consider n1 be Nat such that

       A3: k1 = (n1 + 1) by NAT_1: 6;

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

      take n1;

      thus thesis by A2, A3;

    end;

    

     Lm2: ((for n holds (seq . n) < (seq . (n + 1))) implies for n, k holds (seq . n) < (seq . ((n + 1) + k))) & ((for n, k holds (seq . n) < (seq . ((n + 1) + k))) implies for n, m st n < m holds (seq . n) < (seq . m)) & ((for n, m st n < m holds (seq . n) < (seq . m)) implies for n holds (seq . n) < (seq . (n + 1)))

    proof

      thus (for n holds (seq . n) < (seq . (n + 1))) implies for n, k holds (seq . n) < (seq . ((n + 1) + k))

      proof

        assume

         A1: for n holds (seq . n) < (seq . (n + 1));

        let n;

        defpred X[ Nat] means (seq . n) < (seq . ((n + 1) + $1));

         A2:

        now

          let k such that

           A3: X[k];

          (seq . ((n + 1) + k)) < (seq . (((n + 1) + k) + 1)) by A1;

          hence X[(k + 1)] by A3, XXREAL_0: 2;

        end;

        

         A4: X[ 0 ] by A1;

        thus for k holds X[k] from NAT_1:sch 2( A4, A2);

      end;

      thus (for n, k holds (seq . n) < (seq . ((n + 1) + k))) implies for n, m st n < m holds (seq . n) < (seq . m)

      proof

        assume

         A5: for n, k holds (seq . n) < (seq . ((n + 1) + k));

        let n, m;

        assume n < m;

        then ex k st m = ((n + 1) + k) by Lm1;

        hence thesis by A5;

      end;

      assume

       A6: for n, m st n < m holds (seq . n) < (seq . m);

      let n;

      n < (n + 1) by NAT_1: 13;

      hence thesis by A6;

    end;

    

     Lm3: ((for n holds (seq . (n + 1)) < (seq . n)) implies for n, k holds (seq . ((n + 1) + k)) < (seq . n)) & ((for n, k holds (seq . ((n + 1) + k)) < (seq . n)) implies for n, m st n < m holds (seq . m) < (seq . n)) & ((for n, m st n < m holds (seq . m) < (seq . n)) implies for n holds (seq . (n + 1)) < (seq . n))

    proof

      thus (for n holds (seq . (n + 1)) < (seq . n)) implies for n, k holds (seq . ((n + 1) + k)) < (seq . n)

      proof

        assume

         A1: for n holds (seq . (n + 1)) < (seq . n);

        let n;

        defpred X[ Nat] means (seq . ((n + 1) + $1)) < (seq . n);

         A2:

        now

          let k such that

           A3: X[k];

          (seq . (((n + 1) + k) + 1)) < (seq . ((n + 1) + k)) by A1;

          hence X[(k + 1)] by A3, XXREAL_0: 2;

        end;

        

         A4: X[ 0 ] by A1;

        thus for k holds X[k] from NAT_1:sch 2( A4, A2);

      end;

      thus (for n, k holds (seq . ((n + 1) + k)) < (seq . n)) implies for n, m st n < m holds (seq . m) < (seq . n)

      proof

        assume

         A5: for n, k holds (seq . ((n + 1) + k)) < (seq . n);

        let n, m;

        assume n < m;

        then ex k st m = ((n + 1) + k) by Lm1;

        hence thesis by A5;

      end;

      assume

       A6: for n, m st n < m holds (seq . m) < (seq . n);

      let n;

      n < (n + 1) by NAT_1: 13;

      hence thesis by A6;

    end;

    

     Lm4: ((for n holds (seq . n) <= (seq . (n + 1))) implies for n, k holds (seq . n) <= (seq . (n + k))) & ((for n, k holds (seq . n) <= (seq . (n + k))) implies for n, m st n <= m holds (seq . n) <= (seq . m)) & ((for n, m st n <= m holds (seq . n) <= (seq . m)) implies for n holds (seq . n) <= (seq . (n + 1)))

    proof

      thus (for n holds (seq . n) <= (seq . (n + 1))) implies for n, k holds (seq . n) <= (seq . (n + k))

      proof

        assume

         A1: for n holds (seq . n) <= (seq . (n + 1));

        let n;

        defpred X[ Nat] means (seq . n) <= (seq . (n + $1));

         A2:

        now

          let k such that

           A3: X[k];

          (seq . (n + k)) <= (seq . ((n + k) + 1)) by A1;

          hence X[(k + 1)] by A3, XXREAL_0: 2;

        end;

        

         A4: X[ 0 ];

        thus for k holds X[k] from NAT_1:sch 2( A4, A2);

      end;

      thus (for n, k holds (seq . n) <= (seq . (n + k))) implies for n, m st n <= m holds (seq . n) <= (seq . m)

      proof

        assume

         A5: for n, k holds (seq . n) <= (seq . (n + k));

        let n, m;

        assume n <= m;

        then

        consider k1 be Nat such that

         A6: m = (n + k1) by NAT_1: 10;

        thus thesis by A5, A6;

      end;

      assume

       A7: for n, m st n <= m holds (seq . n) <= (seq . m);

      let n;

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

      hence thesis by A7;

    end;

    

     Lm5: ((for n holds (seq . (n + 1)) <= (seq . n)) implies for n, k holds (seq . (n + k)) <= (seq . n)) & ((for n, k holds (seq . (n + k)) <= (seq . n)) implies for n, m st n <= m holds (seq . m) <= (seq . n)) & ((for n, m st n <= m holds (seq . m) <= (seq . n)) implies for n holds (seq . (n + 1)) <= (seq . n))

    proof

      thus (for n holds (seq . (n + 1)) <= (seq . n)) implies for n, k holds (seq . (n + k)) <= (seq . n)

      proof

        assume

         A1: for n holds (seq . (n + 1)) <= (seq . n);

        let n;

        defpred X[ Nat] means (seq . (n + $1)) <= (seq . n);

         A2:

        now

          let k such that

           A3: X[k];

          (seq . ((n + k) + 1)) <= (seq . (n + k)) by A1;

          hence X[(k + 1)] by A3, XXREAL_0: 2;

        end;

        

         A4: X[ 0 ];

        thus for k holds X[k] from NAT_1:sch 2( A4, A2);

      end;

      thus (for n, k holds (seq . (n + k)) <= (seq . n)) implies for n, m st n <= m holds (seq . m) <= (seq . n)

      proof

        assume

         A5: for n, k holds (seq . (n + k)) <= (seq . n);

        let n, m;

        assume n <= m;

        then

        consider k1 be Nat such that

         A6: m = (n + k1) by NAT_1: 10;

        thus thesis by A5, A6;

      end;

      assume

       A7: for n, m st n <= m holds (seq . m) <= (seq . n);

      let n;

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

      hence thesis by A7;

    end;

    reserve e1,e2 for ExtReal;

    definition

      let f be NAT -defined real-valued Function;

      :: original: increasing

      redefine

      :: SEQM_3:def1

      attr f is increasing means for m, n st m in ( dom f) & n in ( dom f) & m < n holds (f . m) < (f . n);

      compatibility ;

      :: original: decreasing

      redefine

      :: SEQM_3:def2

      attr f is decreasing means for m, n st m in ( dom f) & n in ( dom f) & m < n holds (f . m) > (f . n);

      compatibility ;

      :: original: non-decreasing

      redefine

      :: SEQM_3:def3

      attr f is non-decreasing means for m, n st m in ( dom f) & n in ( dom f) & m <= n holds (f . m) <= (f . n);

      compatibility ;

      :: original: non-increasing

      redefine

      :: SEQM_3:def4

      attr f is non-increasing means for m, n st m in ( dom f) & n in ( dom f) & m <= n holds (f . m) >= (f . n);

      compatibility ;

    end

    definition

      let seq;

      :: SEQM_3:def5

      attr seq is monotone means seq is non-decreasing or seq is non-increasing;

    end

    theorem :: SEQM_3:1

    

     Th1: seq is increasing iff for n, m st n < m holds (seq . n) < (seq . m)

    proof

      thus seq is increasing implies for n, m st n < m holds (seq . n) < (seq . m)

      proof

        assume seq is increasing;

        then for n holds (seq . n) < (seq . (n + 1));

        then for n, k holds (seq . n) < (seq . ((n + 1) + k)) by Lm2;

        hence thesis by Lm2;

      end;

      assume

       A1: for n, m st n < m holds (seq . n) < (seq . m);

      let n, m;

      assume that n in ( dom seq) and m in ( dom seq) and

       A2: n < m;

      thus thesis by A1, A2;

    end;

    theorem :: SEQM_3:2

    seq is increasing iff for n, k holds (seq . n) < (seq . ((n + 1) + k)) by Lm2;

    theorem :: SEQM_3:3

    

     Th3: seq is decreasing iff for n, k holds (seq . ((n + 1) + k)) < (seq . n) by Lm3;

    theorem :: SEQM_3:4

    

     Th4: seq is decreasing iff for n, m st n < m holds (seq . m) < (seq . n)

    proof

      thus seq is decreasing implies for n, m st n < m holds (seq . m) < (seq . n)

      proof

        assume seq is decreasing;

        then for n, k holds (seq . ((n + 1) + k)) < (seq . n) by Th3;

        hence thesis by Lm3;

      end;

      assume

       A1: for n, m st n < m holds (seq . m) < (seq . n);

      let n, m;

      assume that n in ( dom seq) and m in ( dom seq) and

       A2: n < m;

      thus thesis by A1, A2;

    end;

    theorem :: SEQM_3:5

    

     Th5: seq is non-decreasing iff for n, k holds (seq . n) <= (seq . (n + k)) by Lm4;

    theorem :: SEQM_3:6

    

     Th6: seq is non-decreasing iff for n, m st n <= m holds (seq . n) <= (seq . m)

    proof

      thus seq is non-decreasing implies for n, m st n <= m holds (seq . n) <= (seq . m)

      proof

        assume seq is non-decreasing;

        then for n, k holds (seq . n) <= (seq . (n + k)) by Th5;

        hence thesis by Lm4;

      end;

      assume

       A1: for n, m st n <= m holds (seq . n) <= (seq . m);

      let n, m;

      assume that n in ( dom seq) and m in ( dom seq) and

       A2: n <= m;

      thus thesis by A1, A2;

    end;

    theorem :: SEQM_3:7

    

     Th7: seq is non-increasing iff for n, k holds (seq . (n + k)) <= (seq . n) by Lm5;

    theorem :: SEQM_3:8

    

     Th8: seq is non-increasing iff for n, m st n <= m holds (seq . m) <= (seq . n)

    proof

      thus seq is non-increasing implies for n, m st n <= m holds (seq . m) <= (seq . n)

      proof

        assume seq is non-increasing;

        then for n, k holds (seq . (n + k)) <= (seq . n) by Th7;

        hence thesis by Lm5;

      end;

      assume

       A1: for n, m st n <= m holds (seq . m) <= (seq . n);

      let n, m;

      assume that n in ( dom seq) and m in ( dom seq) and

       A2: n <= m;

      thus thesis by A1, A2;

    end;

    theorem :: SEQM_3:9

    seq is increasing implies for n st 0 < n holds (seq . 0 ) < (seq . n) by Th1;

    theorem :: SEQM_3:10

    seq is decreasing implies for n st 0 < n holds (seq . n) < (seq . 0 ) by Th4;

    theorem :: SEQM_3:11

    

     Th11: seq is non-decreasing implies for n holds (seq . 0 ) <= (seq . n) by Th6;

    theorem :: SEQM_3:12

    

     Th12: seq is non-increasing implies for n holds (seq . n) <= (seq . 0 ) by Th8;

    registration

      cluster constant -> non-decreasing non-increasing for PartFunc of NAT , REAL ;

      coherence ;

      cluster non-decreasing non-increasing -> constant for PartFunc of NAT , REAL ;

      coherence

      proof

        let f be PartFunc of NAT , REAL such that

         A1: f is non-decreasing non-increasing;

        let x,y be object;

        assume

         A2: x in ( dom f) & y in ( dom f);

        ( dom f) c= NAT by RELAT_1:def 18;

        then

        reconsider m = x, n = y as Element of NAT by A2;

        m <= n or n <= m;

        then (f . m) <= (f . n) & (f . n) <= (f . m) by A1, A2;

        hence thesis by XXREAL_0: 1;

      end;

    end

    

     Lm6: ( id NAT ) is increasing natural-valued;

    registration

      cluster increasing natural-valued for Real_Sequence;

      existence

      proof

        reconsider i = ( id NAT ) as Real_Sequence by FUNCT_2: 7, NUMBERS: 19;

        take i;

        thus thesis;

      end;

    end

    registration

      cluster increasing for sequence of NAT ;

      existence by Lm6;

    end

    

     Lm7: for f be sequence of NAT holds f is increasing iff for n be Nat holds (f . n) < (f . (n + 1));

    reserve Nseq for increasing sequence of NAT ;

    theorem :: SEQM_3:13

    seq is sequence of NAT iff for n holds (seq . n) is Element of NAT

    proof

      thus seq is sequence of NAT implies for n holds (seq . n) is Element of NAT by ORDINAL1:def 12;

      assume

       A1: for n holds (seq . n) is Element of NAT ;

      ( rng seq) c= NAT

      proof

        let x be object;

        assume x in ( rng seq);

        then

        consider y be object such that

         A2: y in ( dom seq) and

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

        reconsider y as Element of NAT by A2, FUNCT_2:def 1;

        x = (seq . y) by A3;

        then x is Element of NAT by A1;

        hence thesis;

      end;

      hence thesis by FUNCT_2: 6;

    end;

    registration

      let Nseq, k;

      cluster (Nseq ^\ k) -> increasing natural-valued;

      coherence

      proof

        now

          let n;

          (Nseq . (n + k)) < (Nseq . ((n + k) + 1)) by Lm7;

          then ((Nseq ^\ k) . n) < (Nseq . ((n + 1) + k)) by NAT_1:def 3;

          hence ((Nseq ^\ k) . n) < ((Nseq ^\ k) . (n + 1)) by NAT_1:def 3;

        end;

        hence thesis by Lm7;

      end;

    end

    definition

      let f be Real_Sequence;

      :: original: increasing

      redefine

      :: SEQM_3:def6

      attr f is increasing means for n be Nat holds (f . n) < (f . (n + 1));

      compatibility ;

      :: original: decreasing

      redefine

      :: SEQM_3:def7

      attr f is decreasing means for n be Nat holds (f . n) > (f . (n + 1));

      compatibility ;

      :: original: non-decreasing

      redefine

      :: SEQM_3:def8

      attr f is non-decreasing means for n be Nat holds (f . n) <= (f . (n + 1));

      compatibility ;

      :: original: non-increasing

      redefine

      :: SEQM_3:def9

      attr f is non-increasing means for n be Nat holds (f . n) >= (f . (n + 1));

      compatibility ;

    end

    theorem :: SEQM_3:14

    for n holds n <= (Nseq . n)

    proof

      defpred X[ Nat] means $1 <= (Nseq . $1);

       A1:

      now

        let k such that

         A2: X[k];

        (Nseq . k) < (Nseq . (k + 1)) by Lm7;

        then k < (Nseq . (k + 1)) by A2, XXREAL_0: 2;

        hence X[(k + 1)] by NAT_1: 13;

      end;

      

       A3: X[ 0 ];

      thus for k holds X[k] from NAT_1:sch 2( A3, A1);

    end;

    registration

      let s be Real_Sequence, k be Nat;

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

      coherence ;

    end

    theorem :: SEQM_3:15

    

     Th15: ((seq + seq1) ^\ k) = ((seq ^\ k) + (seq1 ^\ k))

    proof

      now

        let n be Element of NAT ;

        

        thus (((seq + seq1) ^\ k) . n) = ((seq + seq1) . (n + k)) by NAT_1:def 3

        .= ((seq . (n + k)) + (seq1 . (n + k))) by SEQ_1: 7

        .= (((seq ^\ k) . n) + (seq1 . (n + k))) by NAT_1:def 3

        .= (((seq ^\ k) . n) + ((seq1 ^\ k) . n)) by NAT_1:def 3

        .= (((seq ^\ k) + (seq1 ^\ k)) . n) by SEQ_1: 7;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQM_3:16

    

     Th16: (( - seq) ^\ k) = ( - (seq ^\ k))

    proof

      now

        let n be Element of NAT ;

        

        thus ((( - seq) ^\ k) . n) = (( - seq) . (n + k)) by NAT_1:def 3

        .= ( - (seq . (n + k))) by SEQ_1: 10

        .= ( - ((seq ^\ k) . n)) by NAT_1:def 3

        .= (( - (seq ^\ k)) . n) by SEQ_1: 10;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQM_3:17

    ((seq - seq1) ^\ k) = ((seq ^\ k) - (seq1 ^\ k))

    proof

      

      thus ((seq - seq1) ^\ k) = ((seq ^\ k) + (( - seq1) ^\ k)) by Th15

      .= ((seq ^\ k) - (seq1 ^\ k)) by Th16;

    end;

    theorem :: SEQM_3:18

    

     Th18: ((seq " ) ^\ k) = ((seq ^\ k) " )

    proof

      now

        let n be Element of NAT ;

        

        thus (((seq " ) ^\ k) . n) = ((seq " ) . (n + k)) by NAT_1:def 3

        .= ((seq . (n + k)) " ) by VALUED_1: 10

        .= (((seq ^\ k) . n) " ) by NAT_1:def 3

        .= (((seq ^\ k) " ) . n) by VALUED_1: 10;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQM_3:19

    

     Th19: ((seq (#) seq1) ^\ k) = ((seq ^\ k) (#) (seq1 ^\ k))

    proof

      now

        let n be Element of NAT ;

        

        thus (((seq (#) seq1) ^\ k) . n) = ((seq (#) seq1) . (n + k)) by NAT_1:def 3

        .= ((seq . (n + k)) * (seq1 . (n + k))) by SEQ_1: 8

        .= (((seq ^\ k) . n) * (seq1 . (n + k))) by NAT_1:def 3

        .= (((seq ^\ k) . n) * ((seq1 ^\ k) . n)) by NAT_1:def 3

        .= (((seq ^\ k) (#) (seq1 ^\ k)) . n) by SEQ_1: 8;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQM_3:20

    ((seq /" seq1) ^\ k) = ((seq ^\ k) /" (seq1 ^\ k))

    proof

      

      thus ((seq /" seq1) ^\ k) = ((seq ^\ k) (#) ((seq1 " ) ^\ k)) by Th19

      .= ((seq ^\ k) /" (seq1 ^\ k)) by Th18;

    end;

    theorem :: SEQM_3:21

    ((r (#) seq) ^\ k) = (r (#) (seq ^\ k))

    proof

      now

        let n be Element of NAT ;

        

        thus (((r (#) seq) ^\ k) . n) = ((r (#) seq) . (n + k)) by NAT_1:def 3

        .= (r * (seq . (n + k))) by SEQ_1: 9

        .= (r * ((seq ^\ k) . n)) by NAT_1:def 3

        .= ((r (#) (seq ^\ k)) . n) by SEQ_1: 9;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQM_3:22

    seq is increasing & seq1 is subsequence of seq implies seq1 is increasing

    proof

      assume that

       A1: seq is increasing and

       A2: seq1 is subsequence of seq;

      let n;

      consider Nseq such that

       A3: seq1 = (seq * Nseq) by A2, VALUED_0:def 17;

      

       A4: n in NAT by ORDINAL1:def 12;

      (Nseq . n) < (Nseq . (n + 1)) by Lm7;

      then (seq . (Nseq . n)) < (seq . (Nseq . (n + 1))) by A1, Th1;

      then ((seq * Nseq) . n) < (seq . (Nseq . (n + 1))) by FUNCT_2: 15, A4;

      hence thesis by A3, FUNCT_2: 15;

    end;

    theorem :: SEQM_3:23

    seq is decreasing & seq1 is subsequence of seq implies seq1 is decreasing

    proof

      assume that

       A1: seq is decreasing and

       A2: seq1 is subsequence of seq;

      let n;

      consider Nseq such that

       A3: seq1 = (seq * Nseq) by A2, VALUED_0:def 17;

      

       A4: n in NAT by ORDINAL1:def 12;

      (Nseq . n) < (Nseq . (n + 1)) by Lm7;

      then (seq . (Nseq . (n + 1))) < (seq . (Nseq . n)) by A1, Th4;

      then ((seq * Nseq) . (n + 1)) < (seq . (Nseq . n)) by FUNCT_2: 15;

      hence thesis by A3, FUNCT_2: 15, A4;

    end;

    theorem :: SEQM_3:24

    

     Th24: seq is non-decreasing & seq1 is subsequence of seq implies seq1 is non-decreasing

    proof

      assume that

       A1: seq is non-decreasing and

       A2: seq1 is subsequence of seq;

      let n;

      consider Nseq such that

       A3: seq1 = (seq * Nseq) by A2, VALUED_0:def 17;

      

       A4: n in NAT by ORDINAL1:def 12;

      (Nseq . n) <= (Nseq . (n + 1)) by Lm7;

      then (seq . (Nseq . n)) <= (seq . (Nseq . (n + 1))) by A1, Th6;

      then ((seq * Nseq) . n) <= (seq . (Nseq . (n + 1))) by FUNCT_2: 15, A4;

      hence thesis by A3, FUNCT_2: 15;

    end;

    theorem :: SEQM_3:25

    

     Th25: seq is non-increasing & seq1 is subsequence of seq implies seq1 is non-increasing

    proof

      assume that

       A1: seq is non-increasing and

       A2: seq1 is subsequence of seq;

      let n;

      consider Nseq such that

       A3: seq1 = (seq * Nseq) by A2, VALUED_0:def 17;

      

       A4: n in NAT by ORDINAL1:def 12;

      (Nseq . n) <= (Nseq . (n + 1)) by Lm7;

      then (seq . (Nseq . (n + 1))) <= (seq . (Nseq . n)) by A1, Th8;

      then ((seq * Nseq) . (n + 1)) <= (seq . (Nseq . n)) by FUNCT_2: 15;

      hence thesis by A3, FUNCT_2: 15, A4;

    end;

    theorem :: SEQM_3:26

    seq is monotone & seq1 is subsequence of seq implies seq1 is monotone by Th25, Th24;

    theorem :: SEQM_3:27

    

     Th27: seq is bounded_above & seq1 is subsequence of seq implies seq1 is bounded_above

    proof

      assume that

       A1: seq is bounded_above and

       A2: seq1 is subsequence of seq;

      consider r1 such that

       A3: for n holds (seq . n) < r1 by A1;

      consider Nseq such that

       A4: seq1 = (seq * Nseq) by A2, VALUED_0:def 17;

      take r = r1;

      let n be Nat;

      n in NAT by ORDINAL1:def 12;

      then (seq1 . n) = (seq . (Nseq . n)) by A4, FUNCT_2: 15;

      hence (seq1 . n) < r by A3;

    end;

    theorem :: SEQM_3:28

    

     Th28: seq is bounded_below & seq1 is subsequence of seq implies seq1 is bounded_below

    proof

      assume that

       A1: seq is bounded_below and

       A2: seq1 is subsequence of seq;

      consider r1 such that

       A3: for n holds r1 < (seq . n) by A1;

      consider Nseq such that

       A4: seq1 = (seq * Nseq) by A2, VALUED_0:def 17;

      take r = r1;

      let n be Nat;

      n in NAT by ORDINAL1:def 12;

      then (seq1 . n) = (seq . (Nseq . n)) by A4, FUNCT_2: 15;

      hence r < (seq1 . n) by A3;

    end;

    theorem :: SEQM_3:29

    seq is bounded & seq1 is subsequence of seq implies seq1 is bounded by Th27, Th28;

    theorem :: SEQM_3:30

    (seq is increasing & 0 < r implies (r (#) seq) is increasing) & ( 0 = r implies (r (#) seq) is constant) & (seq is increasing & r < 0 implies (r (#) seq) is decreasing)

    proof

      thus seq is increasing & 0 < r implies (r (#) seq) is increasing

      proof

        assume that

         A1: seq is increasing and

         A2: 0 < r;

        let n;

        (seq . n) < (seq . (n + 1)) by A1;

        then (r * (seq . n)) < (r * (seq . (n + 1))) by A2, XREAL_1: 68;

        then ((r (#) seq) . n) < (r * (seq . (n + 1))) by SEQ_1: 9;

        hence thesis by SEQ_1: 9;

      end;

      thus 0 = r implies (r (#) seq) is constant

      proof

        assume

         A3: 0 = r;

        now

          let n be Nat;

          n in NAT & (r * (seq . n)) = (r * (seq . (n + 1))) by A3, ORDINAL1:def 12;

          then ((r (#) seq) . n) = (r * (seq . (n + 1))) by SEQ_1: 9;

          hence ((r (#) seq) . n) = ((r (#) seq) . (n + 1)) by SEQ_1: 9;

        end;

        hence thesis by VALUED_0: 25;

      end;

      assume that

       A4: seq is increasing and

       A5: r < 0 ;

      let n;

      (seq . n) < (seq . (n + 1)) by A4;

      then (r * (seq . (n + 1))) < (r * (seq . n)) by A5, XREAL_1: 69;

      then ((r (#) seq) . (n + 1)) < (r * (seq . n)) by SEQ_1: 9;

      hence thesis by SEQ_1: 9;

    end;

    theorem :: SEQM_3:31

    (seq is decreasing & 0 < r implies (r (#) seq) is decreasing) & (seq is decreasing & r < 0 implies (r (#) seq) is increasing)

    proof

      thus seq is decreasing & 0 < r implies (r (#) seq) is decreasing

      proof

        assume that

         A1: seq is decreasing and

         A2: 0 < r;

        let n;

        (seq . (n + 1)) < (seq . n) by A1;

        then (r * (seq . (n + 1))) < (r * (seq . n)) by A2, XREAL_1: 68;

        then ((r (#) seq) . (n + 1)) < (r * (seq . n)) by SEQ_1: 9;

        hence thesis by SEQ_1: 9;

      end;

      assume that

       A3: seq is decreasing and

       A4: r < 0 ;

      let n;

      (seq . (n + 1)) < (seq . n) by A3;

      then (r * (seq . n)) < (r * (seq . (n + 1))) by A4, XREAL_1: 69;

      then ((r (#) seq) . n) < (r * (seq . (n + 1))) by SEQ_1: 9;

      hence thesis by SEQ_1: 9;

    end;

    theorem :: SEQM_3:32

    (seq is non-decreasing & 0 <= r implies (r (#) seq) is non-decreasing) & (seq is non-decreasing & r <= 0 implies (r (#) seq) is non-increasing)

    proof

      thus seq is non-decreasing & 0 <= r implies (r (#) seq) is non-decreasing

      proof

        assume that

         A1: seq is non-decreasing and

         A2: 0 <= r;

        let n;

        (seq . n) <= (seq . (n + 1)) by A1;

        then (r * (seq . n)) <= (r * (seq . (n + 1))) by A2, XREAL_1: 64;

        then ((r (#) seq) . n) <= (r * (seq . (n + 1))) by SEQ_1: 9;

        hence thesis by SEQ_1: 9;

      end;

      assume that

       A3: seq is non-decreasing and

       A4: r <= 0 ;

      let n;

      (seq . n) <= (seq . (n + 1)) by A3;

      then (r * (seq . (n + 1))) <= (r * (seq . n)) by A4, XREAL_1: 65;

      then ((r (#) seq) . (n + 1)) <= (r * (seq . n)) by SEQ_1: 9;

      hence thesis by SEQ_1: 9;

    end;

    theorem :: SEQM_3:33

    (seq is non-increasing & 0 <= r implies (r (#) seq) is non-increasing) & (seq is non-increasing & r <= 0 implies (r (#) seq) is non-decreasing)

    proof

      thus seq is non-increasing & 0 <= r implies (r (#) seq) is non-increasing

      proof

        assume that

         A1: seq is non-increasing and

         A2: 0 <= r;

        let n;

        (seq . (n + 1)) <= (seq . n) by A1;

        then (r * (seq . (n + 1))) <= (r * (seq . n)) by A2, XREAL_1: 64;

        then ((r (#) seq) . (n + 1)) <= (r * (seq . n)) by SEQ_1: 9;

        hence thesis by SEQ_1: 9;

      end;

      assume that

       A3: seq is non-increasing and

       A4: r <= 0 ;

      let n;

      (seq . (n + 1)) <= (seq . n) by A3;

      then (r * (seq . n)) <= (r * (seq . (n + 1))) by A4, XREAL_1: 65;

      then ((r (#) seq) . n) <= (r * (seq . (n + 1))) by SEQ_1: 9;

      hence thesis by SEQ_1: 9;

    end;

    theorem :: SEQM_3:34

    

     Th34: (seq is increasing & seq1 is increasing implies (seq + seq1) is increasing) & (seq is decreasing & seq1 is decreasing implies (seq + seq1) is decreasing) & (seq is non-decreasing & seq1 is non-decreasing implies (seq + seq1) is non-decreasing) & (seq is non-increasing & seq1 is non-increasing implies (seq + seq1) is non-increasing)

    proof

      thus seq is increasing & seq1 is increasing implies (seq + seq1) is increasing

      proof

        assume

         A1: seq is increasing & seq1 is increasing;

        let n;

        (seq . n) < (seq . (n + 1)) & (seq1 . n) < (seq1 . (n + 1)) by A1;

        then ((seq . n) + (seq1 . n)) < ((seq . (n + 1)) + (seq1 . (n + 1))) by XREAL_1: 8;

        then ((seq + seq1) . n) < ((seq . (n + 1)) + (seq1 . (n + 1))) by SEQ_1: 7;

        hence thesis by SEQ_1: 7;

      end;

      thus seq is decreasing & seq1 is decreasing implies (seq + seq1) is decreasing

      proof

        assume

         A2: seq is decreasing & seq1 is decreasing;

        let n;

        (seq . (n + 1)) < (seq . n) & (seq1 . (n + 1)) < (seq1 . n) by A2;

        then ((seq . (n + 1)) + (seq1 . (n + 1))) < ((seq . n) + (seq1 . n)) by XREAL_1: 8;

        then ((seq + seq1) . (n + 1)) < ((seq . n) + (seq1 . n)) by SEQ_1: 7;

        hence thesis by SEQ_1: 7;

      end;

      thus seq is non-decreasing & seq1 is non-decreasing implies (seq + seq1) is non-decreasing

      proof

        assume

         A3: seq is non-decreasing & seq1 is non-decreasing;

        let n;

        (seq . n) <= (seq . (n + 1)) & (seq1 . n) <= (seq1 . (n + 1)) by A3;

        then ((seq . n) + (seq1 . n)) <= ((seq . (n + 1)) + (seq1 . (n + 1))) by XREAL_1: 7;

        then ((seq + seq1) . n) <= ((seq . (n + 1)) + (seq1 . (n + 1))) by SEQ_1: 7;

        hence thesis by SEQ_1: 7;

      end;

      assume

       A4: seq is non-increasing & seq1 is non-increasing;

      let n;

      (seq . (n + 1)) <= (seq . n) & (seq1 . (n + 1)) <= (seq1 . n) by A4;

      then ((seq . (n + 1)) + (seq1 . (n + 1))) <= ((seq . n) + (seq1 . n)) by XREAL_1: 7;

      then ((seq + seq1) . (n + 1)) <= ((seq . n) + (seq1 . n)) by SEQ_1: 7;

      hence thesis by SEQ_1: 7;

    end;

    theorem :: SEQM_3:35

    (seq is increasing & seq1 is constant implies (seq + seq1) is increasing) & (seq is decreasing & seq1 is constant implies (seq + seq1) is decreasing) & (seq is non-decreasing & seq1 is constant implies (seq + seq1) is non-decreasing) & (seq is non-increasing & seq1 is constant implies (seq + seq1) is non-increasing)

    proof

      thus seq is increasing & seq1 is constant implies (seq + seq1) is increasing

      proof

        assume that

         A1: seq is increasing and

         A2: seq1 is constant;

        let n;

        consider r1 be Element of REAL such that

         A3: for n be Nat holds (seq1 . n) = r1 by A2;

        (seq . n) < (seq . (n + 1)) by A1;

        then ((seq . n) + r1) < ((seq . (n + 1)) + r1) by XREAL_1: 6;

        then ((seq . n) + (seq1 . n)) < ((seq . (n + 1)) + r1) by A3;

        then ((seq . n) + (seq1 . n)) < ((seq . (n + 1)) + (seq1 . (n + 1))) by A3;

        then ((seq + seq1) . n) < ((seq . (n + 1)) + (seq1 . (n + 1))) by SEQ_1: 7;

        hence thesis by SEQ_1: 7;

      end;

      thus seq is decreasing & seq1 is constant implies (seq + seq1) is decreasing

      proof

        assume that

         A4: seq is decreasing and

         A5: seq1 is constant;

        let n;

        consider r1 be Element of REAL such that

         A6: for n be Nat holds (seq1 . n) = r1 by A5;

        (seq . (n + 1)) < (seq . n) by A4;

        then ((seq . (n + 1)) + r1) < ((seq . n) + r1) by XREAL_1: 6;

        then ((seq . (n + 1)) + (seq1 . (n + 1))) < ((seq . n) + r1) by A6;

        then ((seq . (n + 1)) + (seq1 . (n + 1))) < ((seq . n) + (seq1 . n)) by A6;

        then ((seq + seq1) . (n + 1)) < ((seq . n) + (seq1 . n)) by SEQ_1: 7;

        hence thesis by SEQ_1: 7;

      end;

      thus seq is non-decreasing & seq1 is constant implies (seq + seq1) is non-decreasing by Th34;

      assume seq is non-increasing & seq1 is constant;

      hence thesis by Th34;

    end;

    theorem :: SEQM_3:36

    

     Th36: (seq is bounded_above & 0 < r implies (r (#) seq) is bounded_above) & ( 0 = r implies (r (#) seq) is bounded) & (seq is bounded_above & r < 0 implies (r (#) seq) is bounded_below)

    proof

      thus seq is bounded_above & 0 < r implies (r (#) seq) is bounded_above;

      thus 0 = r implies (r (#) seq) is bounded

      proof

        assume

         A1: 0 = r;

        now

          let n;

          ((r (#) seq) . n) = ( 0 * (seq . n)) by A1, SEQ_1: 9;

          hence ((r (#) seq) . n) < 1;

        end;

        hence (r (#) seq) is bounded_above;

        take p = ( - 1);

        let n be Nat;

        ( - 1) < 0 & (r * (seq . n)) = 0 by A1;

        hence p < ((r (#) seq) . n) by SEQ_1: 9;

      end;

      assume that

       A2: seq is bounded_above and

       A3: r < 0 ;

      consider r1 such that

       A4: for n holds (seq . n) < r1 by A2;

      take p = (r * |.r1.|);

      let n be Nat;

      r1 <= |.r1.| by ABSVALUE: 4;

      then (seq . n) < |.r1.| by A4, XXREAL_0: 2;

      then (r * |.r1.|) < (r * (seq . n)) by A3, XREAL_1: 69;

      hence p < ((r (#) seq) . n) by SEQ_1: 9;

    end;

    theorem :: SEQM_3:37

    (seq is bounded implies for r holds (r (#) seq) is bounded) & (seq is bounded implies ( - seq) is bounded) & (seq is bounded iff ( abs seq) is bounded)

    proof

      thus seq is bounded implies for r holds (r (#) seq) is bounded

      proof

        assume

         A1: seq is bounded;

        let r;

        per cases ;

          suppose 0 < r;

          hence thesis by A1;

        end;

          suppose 0 = r;

          hence thesis by Th36;

        end;

          suppose r < 0 ;

          hence thesis by A1;

        end;

      end;

      thus seq is bounded implies ( - seq) is bounded;

      thus seq is bounded implies ( abs seq) is bounded;

      assume ( abs seq) is bounded;

      then

      consider r be Real such that

       A2: 0 < r and

       A3: for n be Nat holds |.(( abs seq) . n).| < r by SEQ_2: 3;

      now

        let n be Nat;

         |.(( abs seq) . n).| = |. |.(seq . n).|.| by SEQ_1: 12

        .= |.(seq . n).|;

        hence |.(seq . n).| < r by A3;

      end;

      hence thesis by A2, SEQ_2: 3;

    end;

    theorem :: SEQM_3:38

    seq is bounded_above & seq1 is non-increasing implies (seq + seq1) is bounded_above

    proof

      assume that

       A1: seq is bounded_above and

       A2: seq1 is non-increasing;

      consider r1 such that

       A3: for n holds (seq . n) < r1 by A1;

      take r = (r1 + (seq1 . 0 ));

      let n be Nat;

      (seq1 . n) <= (seq1 . 0 ) by A2, Th12;

      then ((seq . n) + (seq1 . n)) < (r1 + (seq1 . 0 )) by A3, XREAL_1: 8;

      hence ((seq + seq1) . n) < r by SEQ_1: 7;

    end;

    theorem :: SEQM_3:39

    seq is bounded_below & seq1 is non-decreasing implies (seq + seq1) is bounded_below

    proof

      assume that

       A1: seq is bounded_below and

       A2: seq1 is non-decreasing;

      consider r1 such that

       A3: for n holds r1 < (seq . n) by A1;

      take r = (r1 + (seq1 . 0 ));

      let n be Nat;

      (seq1 . 0 ) <= (seq1 . n) by A2, Th11;

      then (r1 + (seq1 . 0 )) < ((seq . n) + (seq1 . n)) by A3, XREAL_1: 8;

      hence r < ((seq + seq1) . n) by SEQ_1: 7;

    end;

    registration

      cluster -> natural-valued for FinSequence of NAT ;

      coherence ;

    end

    begin

    reserve v for FinSequence of REAL ,

r,s for Real,

n,m,i,j,k for Nat;

    ::$Canceled

    theorem :: SEQM_3:41

    

     Th40: |.(r - s).| = 1 iff r > s & r = (s + 1) or r < s & s = (r + 1)

    proof

      thus |.(r - s).| = 1 implies r > s & r = (s + 1) or r < s & s = (r + 1)

      proof

        assume

         A1: |.(r - s).| = 1;

        now

          per cases by XXREAL_0: 1;

            case

             A2: r > s;

            then 0 < (r - s) by XREAL_1: 50;

            then (r - s) = 1 by A1, ABSVALUE:def 1;

            hence thesis by A2;

          end;

            case r = s;

            hence contradiction by A1, ABSVALUE: 2;

          end;

            case

             A3: r < s;

            then

             A4: 0 < (s - r) by XREAL_1: 50;

            1 = |.( - (r - s)).| by A1, COMPLEX1: 52

            .= (s - r) by A4, ABSVALUE:def 1;

            hence thesis by A3;

          end;

        end;

        hence thesis;

      end;

      assume

       A5: r > s & r = (s + 1) or r < s & s = (r + 1);

      per cases by A5;

        suppose r > s & r = (s + 1);

        hence thesis by ABSVALUE:def 1;

      end;

        suppose

         A6: s > r & s = (r + 1);

        

        thus |.(r - s).| = |.( - (r - s)).| by COMPLEX1: 52

        .= 1 by A6, ABSVALUE:def 1;

      end;

    end;

    theorem :: SEQM_3:42

    ( |.(i - j).| + |.(n - m).|) = 1 iff |.(i - j).| = 1 & n = m or |.(n - m).| = 1 & i = j

    proof

      thus ( |.(i - j).| + |.(n - m).|) = 1 implies |.(i - j).| = 1 & n = m or |.(n - m).| = 1 & i = j

      proof

        assume

         A1: ( |.(i - j).| + |.(n - m).|) = 1;

        now

          per cases ;

            suppose

             A2: n = m;

            

            then 1 = ( |.(i - j).| + |. 0 .|) by A1

            .= ( |.(i - j).| + 0 qua Real) by ABSVALUE: 2

            .= |.(i - j).|;

            hence thesis by A2;

          end;

            suppose

             A3: n <> m;

            now

              per cases by A3, XXREAL_0: 1;

                suppose

                 A4: n < m;

                reconsider l = (m - n) as Element of NAT by INT_1: 5, A4;

                 0 < l by A4, XREAL_1: 50;

                then

                 A5: ( 0 + 1) <= l by NAT_1: 13;

                

                 A6: |.( - (m - n)).| = |.l.| by COMPLEX1: 52;

                then

                 A7: |.(n - m).| = |.l.|;

                

                 A8: |.l.| = l by ABSVALUE:def 1;

                then

                 A9: l <= 1 by A1, A6, COMPLEX1: 46, XREAL_1: 31;

                then l = 1 by A5, XXREAL_0: 1;

                then (i - j) = 0 by A1, A8, A7, ABSVALUE: 2;

                hence thesis by A6, A5, A8, A9, XXREAL_0: 1;

              end;

                suppose

                 A10: n > m;

                then

                reconsider l = (n - m) as Element of NAT by INT_1: 5;

                 0 < l by A10, XREAL_1: 50;

                then

                 A11: ( 0 + 1) <= l by NAT_1: 13;

                

                 A12: |.(n - m).| = l by ABSVALUE:def 1;

                then

                 A13: l <= 1 by A1, COMPLEX1: 46, XREAL_1: 31;

                then l = 1 by A11, XXREAL_0: 1;

                then (i - j) = 0 by A1, A12, ABSVALUE: 2;

                hence thesis by A11, A12, A13, XXREAL_0: 1;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      assume

       A14: |.(i - j).| = 1 & n = m or |.(n - m).| = 1 & i = j;

      now

        per cases by A14;

          suppose

           A15: |.(i - j).| = 1 & n = m;

          then |.(n - m).| = 0 by ABSVALUE: 2;

          hence thesis by A15;

        end;

          suppose

           A16: |.(n - m).| = 1 & i = j;

          then |.(i - j).| = 0 by ABSVALUE: 2;

          hence thesis by A16;

        end;

      end;

      hence thesis;

    end;

    theorem :: SEQM_3:43

    n > 1 iff ex m st n = (m + 1) & m > 0

    proof

      thus n > 1 implies ex m st n = (m + 1) & m > 0

      proof

        assume

         A1: 1 < n;

        then

        consider m be Nat such that

         A2: n = (m + 1) by NAT_1: 6;

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

        take m;

        m <> 0 by A1, A2;

        hence thesis by A2;

      end;

      given m such that

       A3: n = (m + 1) & m > 0 ;

      ( 0 + 1) < n by A3, XREAL_1: 6;

      hence thesis;

    end;

    theorem :: SEQM_3:44

    for f be FinSequence, n, m, k st ( len f) = (m + 1) & n in ( dom f) & k in ( Seg m) holds (( Del (f,n)) . k) = (f . k) or (( Del (f,n)) . k) = (f . (k + 1))

    proof

      let f be FinSequence, n, m, k such that

       A1: ( len f) = (m + 1) & n in ( dom f) and

       A2: k in ( Seg m);

      set X = (( dom f) \ {n});

      

       A3: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

      then

       A4: n <= k & k <= m implies (( Sgm X) . k) = (k + 1) by A1, A2, FINSEQ_3: 108;

      X c= ( Seg ( len f)) by A3, XBOOLE_1: 36;

      then ( rng ( Sgm X)) = X by FINSEQ_1:def 13;

      then

       A5: ( dom (f * ( Sgm X))) = ( dom ( Sgm X)) by RELAT_1: 27, XBOOLE_1: 36;

      

       A6: ( dom ( Sgm X)) = ( Seg ( len ( Sgm X))) & ( Del (f,n)) = (f * ( Sgm X)) by FINSEQ_1:def 3, FINSEQ_3:def 2;

      

       A7: ( len ( Sgm X)) = m by A1, A3, FINSEQ_3: 107;

      1 <= k & k < n implies (( Sgm X) . k) = k by A1, A2, A3, FINSEQ_3: 108;

      hence thesis by A2, A6, A5, A7, A4, FINSEQ_3: 25, FUNCT_1: 12;

    end;

    definition

      let f be FinSequence;

      :: original: constant

      redefine

      :: SEQM_3:def10

      attr f is constant means for n, m st n in ( dom f) & m in ( dom f) holds (f . n) = (f . m);

      compatibility ;

    end

    registration

      cluster -> real-valued for FinSequence of REAL ;

      coherence ;

    end

    registration

      cluster non empty increasing for FinSequence of REAL ;

      existence

      proof

        take v = <*( In ( 0 , REAL ))*>;

        thus v is non empty;

        let n, m;

        assume that

         A1: n in ( dom v) and

         A2: m in ( dom v);

        

         A3: ( dom <* 0 *>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then n = 1 by A1, TARSKI:def 1;

        hence thesis by A3, A2, TARSKI:def 1;

      end;

    end

    registration

      cluster constant for FinSequence of REAL ;

      existence

      proof

        take v = ( <*> REAL );

        let n, m;

        assume that n in ( dom v) and m in ( dom v);

        thus thesis;

      end;

    end

    theorem :: SEQM_3:45

    

     Th44: v <> {} & ( rng v) c= ( Seg n) & (v . ( len v)) = n & (for k st 1 <= k & k <= (( len v) - 1) holds for r, s st r = (v . k) & s = (v . (k + 1)) holds |.(r - s).| = 1 or r = s) & i in ( Seg n) & (i + 1) in ( Seg n) & m in ( dom v) & (v . m) = i & (for k st k in ( dom v) & (v . k) = i holds k <= m) implies (m + 1) in ( dom v) & (v . (m + 1)) = (i + 1)

    proof

      assume that

       A1: v <> {} and

       A2: ( rng v) c= ( Seg n) and

       A3: (v . ( len v)) = n and

       A4: for k st 1 <= k & k <= (( len v) - 1) holds for r, s st r = (v . k) & s = (v . (k + 1)) holds |.(r - s).| = 1 or r = s and

       A5: i in ( Seg n) and

       A6: (i + 1) in ( Seg n) and

       A7: m in ( dom v) and

       A8: (v . m) = i and

       A9: for k st k in ( dom v) & (v . k) = i holds k <= m;

      

       A10: m <= ( len v) by A7, FINSEQ_3: 25;

      ( 0 + 1) <= ( len v) by A1, NAT_1: 13;

      then

       A11: ( len v) in ( dom v) by FINSEQ_3: 25;

      reconsider r = (v . (m + 1)) as Real;

      

       A12: i <= n by A5, FINSEQ_1: 1;

      

       A13: 1 <= m by A7, FINSEQ_3: 25;

      

       A14: (i + 1) <= n by A6, FINSEQ_1: 1;

       A15:

      now

        assume not (m + 1) in ( dom v);

        then 1 > (m + 1) or (m + 1) > ( len v) by FINSEQ_3: 25;

        then

         A16: ( len v) <= m by NAT_1: 11, NAT_1: 13;

        i < n by A14, NAT_1: 13;

        hence contradiction by A3, A8, A10, A16, XXREAL_0: 1;

      end;

      then

       A17: (m + 1) <= ( len v) by FINSEQ_3: 25;

      then

       A18: m < ( len v) by NAT_1: 13;

      

       A19: m <= (( len v) - 1) by A17, XREAL_1: 19;

      now

        per cases by A4, A8, A13, A19;

          case

           A20: |.(i - r).| = 1;

          now

            per cases by A20, Th40;

              case

               A21: i > r & i = (r + 1);

              defpred P[ set] means for k, r st k = $1 & k > 0 & (m + k) in ( dom v) & r = (v . (m + k)) holds r < i;

              

               A22: for k st P[k] holds P[(k + 1)]

              proof

                let k such that

                 A23: P[k];

                let j, s such that

                 A24: j = (k + 1) and

                 A25: j > 0 and

                 A26: (m + j) in ( dom v) and

                 A27: s = (v . (m + j));

                now

                  per cases ;

                    suppose k = 0 ;

                    hence thesis by A21, A24, A27;

                  end;

                    suppose

                     A28: k <> 0 ;

                    

                     A29: (m + k) <= ((m + k) + 1) by NAT_1: 11;

                    m <= (m + k) by NAT_1: 11;

                    then

                     A30: 1 <= (m + k) by A13, XXREAL_0: 2;

                    

                     A31: (m + (k + 1)) <= ( len v) by A24, A26, FINSEQ_3: 25;

                    then (m + k) <= ( len v) by A29, XXREAL_0: 2;

                    then

                     A32: (m + k) in ( dom v) by A30, FINSEQ_3: 25;

                    then (v . (m + k)) in ( rng v) by FUNCT_1:def 3;

                    then (v . (m + k)) in ( Seg n) by A2;

                    then

                    reconsider r1 = (v . (m + k)) as Element of NAT ;

                    

                     A33: r1 < i by A23, A28, A32;

                    

                     A34: (m + k) <= (( len v) - 1) by A29, A31, XREAL_1: 19;

                    now

                      per cases by A4, A24, A27, A29, A30, A34;

                        suppose

                         A35: |.(r1 - s).| = 1;

                        now

                          per cases by A35, Th40;

                            suppose r1 > s & r1 = (s + 1);

                            hence thesis by A33, XXREAL_0: 2;

                          end;

                            suppose r1 < s & s = (r1 + 1);

                            then

                             A36: s <= i by A33, NAT_1: 13;

                            now

                              per cases by A36, XXREAL_0: 1;

                                case s < i;

                                hence thesis;

                              end;

                                case s = i;

                                then (m + j) <= m by A9, A26, A27;

                                then j <= (m - m) by XREAL_1: 19;

                                hence contradiction by A25;

                              end;

                            end;

                            hence thesis;

                          end;

                        end;

                        hence thesis;

                      end;

                        suppose r1 = s;

                        hence thesis by A23, A28, A32;

                      end;

                    end;

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

              reconsider l = (( len v) - m) as Element of NAT by A18, INT_1: 5;

              

               A37: 0 < (( len v) - m) & (m + l) = ( len v) by A17, XREAL_1: 19;

              

               A38: P[ 0 ];

              for k holds P[k] from NAT_1:sch 2( A38, A22);

              hence contradiction by A3, A11, A12, A37;

            end;

              case i < r & r = (i + 1);

              hence thesis by A15;

            end;

          end;

          hence thesis;

        end;

          case i = r;

          then (m + 1) <= m by A9, A15;

          then 1 <= (m - m) by XREAL_1: 19;

          then 1 <= 0 ;

          hence contradiction;

        end;

      end;

      hence thesis;

    end;

    theorem :: SEQM_3:46

    v <> {} & ( rng v) c= ( Seg n) & (v . 1) = 1 & (v . ( len v)) = n & (for k st 1 <= k & k <= (( len v) - 1) holds for r, s st r = (v . k) & s = (v . (k + 1)) holds |.(r - s).| = 1 or r = s) implies (for i st i in ( Seg n) holds ex k st k in ( dom v) & (v . k) = i) & for m, k, i, r st m in ( dom v) & (v . m) = i & (for j st j in ( dom v) & (v . j) = i holds j <= m) & m < k & k in ( dom v) & r = (v . k) holds i < r

    proof

      assume that

       A1: v <> {} and

       A2: ( rng v) c= ( Seg n) and

       A3: (v . 1) = 1 and

       A4: (v . ( len v)) = n and

       A5: for k st 1 <= k & k <= (( len v) - 1) holds for r, s st r = (v . k) & s = (v . (k + 1)) holds |.(r - s).| = 1 or r = s;

      defpred P[ Nat] means $1 in ( Seg n) implies ex k st k in ( dom v) & (v . k) = $1;

      

       A6: ( 0 + 1) <= ( len v) by A1, NAT_1: 13;

      then

       A7: ( len v) in ( dom v) by FINSEQ_3: 25;

      

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

      proof

        let i such that

         A9: i in ( Seg n) implies ex k st k in ( dom v) & (v . k) = i;

        assume

         A10: (i + 1) in ( Seg n);

        now

          per cases ;

            suppose

             A11: i = 0 ;

            take k = 1;

            thus k in ( dom v) & (v . k) = (i + 1) by A3, A6, A11, FINSEQ_3: 25;

          end;

            suppose

             A12: i <> 0 ;

            defpred R[ set] means $1 in ( dom v) & (v . $1) = i;

            

             A13: for k be Nat holds R[k] implies k <= ( len v) by FINSEQ_3: 25;

            (i + 1) <= n by A10, FINSEQ_1: 1;

            then

             A14: i <= n by NAT_1: 13;

            

             A15: ( 0 + 1) <= i by A12, NAT_1: 13;

            then

             A16: ex k be Nat st R[k] by A9, A14, FINSEQ_1: 1;

            consider m be Nat such that

             A17: R[m] & for k be Nat st R[k] holds k <= m from NAT_1:sch 6( A13, A16);

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

            take k = (m + 1);

            i in ( Seg n) by A15, A14, FINSEQ_1: 1;

            hence k in ( dom v) & (v . k) = (i + 1) by A1, A2, A4, A5, A10, A17, Th44;

          end;

        end;

        hence thesis;

      end;

      

       A18: P[ 0 ] by FINSEQ_1: 1;

      thus for i holds P[i] from NAT_1:sch 2( A18, A8);

      let m, k, i, r;

      assume that

       A19: m in ( dom v) and

       A20: (v . m) = i and

       A21: for j st j in ( dom v) & (v . j) = i holds j <= m and

       A22: m < k and

       A23: k in ( dom v) and

       A24: r = (v . k);

      

       A25: m <= ( len v) & k <= ( len v) by A19, A23, FINSEQ_3: 25;

      

       A26: 1 <= m by A19, FINSEQ_3: 25;

      

       A27: i in ( rng v) by A19, A20, FUNCT_1:def 3;

      then

       A28: i <= n by A2, FINSEQ_1: 1;

      now

        per cases ;

          suppose i = n;

          then ( len v) <= m by A4, A7, A21;

          hence thesis by A22, A25, XXREAL_0: 1;

        end;

          suppose

           A29: i <> n;

          defpred P[ set] means for j, s st j = $1 & j > 0 & (m + j) in ( dom v) & s = (v . (m + j)) holds i < s;

          i < n by A28, A29, XXREAL_0: 1;

          then 1 <= (i + 1) & (i + 1) <= n by NAT_1: 11, NAT_1: 13;

          then (i + 1) in ( Seg n) by FINSEQ_1: 1;

          then

           A30: (v . (m + 1)) = (i + 1) by A1, A2, A4, A5, A19, A20, A21, A27, Th44;

          

           A31: for k st P[k] holds P[(k + 1)]

          proof

            let k such that

             A32: P[k];

            let j, s such that

             A33: j = (k + 1) and

             A34: j > 0 and

             A35: (m + j) in ( dom v) and

             A36: s = (v . (m + j));

            per cases ;

              suppose k = 0 ;

              hence thesis by A30, A33, A36, NAT_1: 13;

            end;

              suppose

               A37: k <> 0 ;

              m <= (m + k) by NAT_1: 11;

              then

               A38: 1 <= (m + k) by A26, XXREAL_0: 2;

              s in ( rng v) by A35, A36, FUNCT_1:def 3;

              then s in ( Seg n) by A2;

              then

              reconsider s1 = s as Element of NAT ;

              

               A39: (m + (k + 1)) <= ( len v) by A33, A35, FINSEQ_3: 25;

              (m + k) <= ((m + k) + 1) by NAT_1: 11;

              then (m + k) <= ( len v) by A39, XXREAL_0: 2;

              then

               A40: (m + k) in ( dom v) by A38, FINSEQ_3: 25;

              then (v . (m + k)) in ( rng v) by FUNCT_1:def 3;

              then (v . (m + k)) in ( Seg n) by A2;

              then

              reconsider r1 = (v . (m + k)) as Element of NAT ;

              

               A41: i < r1 by A32, A37, A40;

              

               A42: ((m + k) + 1) = (m + (k + 1));

              then

               A43: (m + k) <= (( len v) - 1) by A39, XREAL_1: 19;

              now

                per cases by A5, A33, A36, A42, A38, A43;

                  suppose

                   A44: |.(r1 - s).| = 1;

                  now

                    per cases by A44, Th40;

                      suppose r1 > s & r1 = (s + 1);

                      then

                       A45: i <= s1 by A41, NAT_1: 13;

                      now

                        per cases by A45, XXREAL_0: 1;

                          case i < s;

                          hence thesis;

                        end;

                          case s = i;

                          then (m + j) <= m by A21, A35, A36;

                          then j <= (m - m) by XREAL_1: 19;

                          hence contradiction by A34;

                        end;

                      end;

                      hence thesis;

                    end;

                      suppose r1 < s & s = (r1 + 1);

                      hence thesis by A41, XXREAL_0: 2;

                    end;

                  end;

                  hence thesis;

                end;

                  suppose r1 = s;

                  hence thesis by A32, A37, A40;

                end;

              end;

              hence thesis;

            end;

          end;

          reconsider l = (k - m) as Element of NAT by A22, INT_1: 5;

          

           A46: 0 < (k - m) & (m + l) = k by A22, XREAL_1: 50;

          

           A47: P[ 0 ];

          for k holds P[k] from NAT_1:sch 2( A47, A31);

          hence thesis by A23, A24, A46;

        end;

      end;

      hence thesis;

    end;