seq_4.miz



    begin

    reserve n,k,k1,m,m1,n1,n2,l for Nat;

    reserve r,r1,r2,p,p1,g,g1,g2,s,s1,s2,t for Real;

    reserve seq,seq1,seq2 for Real_Sequence;

    reserve Nseq for increasing sequence of NAT ;

    reserve x for set;

    reserve X,Y for Subset of REAL ;

    theorem :: SEQ_4:1

    

     Th1: for X, Y st for r, p st r in X & p in Y holds r < p holds ex g st for r, p st r in X & p in Y holds r <= g & g <= p

    proof

      let X, Y;

      assume for r, p st r in X & p in Y holds r < p;

      then for r, p st r in X & p in Y holds r <= p;

      then

      consider g such that

       A1: for r, p st r in X & p in Y holds r <= g & g <= p by AXIOMS: 1;

      reconsider g as Real;

      take g;

      thus thesis by A1;

    end;

    theorem :: SEQ_4:2

    

     Th2: 0 < p & (ex r st r in X) & (for r st r in X holds (r + p) in X) implies for g holds ex r st r in X & g < r

    proof

      assume that

       A1: 0 < p and

       A2: ex r st r in X and

       A3: for r st r in X holds (r + p) in X and

       A4: ex g st for r st r in X holds not g < r;

      defpred X[ Real] means for r st r in X holds not $1 < r;

      consider Y such that

       A5: for p1 be Element of REAL holds p1 in Y iff X[p1] from SUBSET_1:sch 3;

      now

        let r, p1 such that

         A6: r in X and

         A7: p1 in Y;

        (r + p) in X by A3, A6;

        then

         A8: (r + p) <= p1 by A5, A7;

        (r + 0 qua Nat) < (r + p) by A1, XREAL_1: 8;

        hence r < p1 by A8, XXREAL_0: 2;

      end;

      then

      consider g2 such that

       A9: for r, p1 st r in X & p1 in Y holds r <= g2 & g2 <= p1 by Th1;

      consider g1 such that

       A10: for r st r in X holds not g1 < r by A4;

      g1 in REAL by XREAL_0:def 1;

      then

       A11: g1 in Y by A10, A5;

      reconsider g2p = (g2 - p) as Element of REAL by XREAL_0:def 1;

       A12:

      now

        assume not (g2 - p) in Y;

        then not X[g2p] by A5;

        then

        consider r1 be Real such that

         A13: r1 in X & g2p < r1;

        ((g2 - p) + p) < (r1 + p) & (r1 + p) in X by A3, A13, XREAL_1: 6;

        hence contradiction by A11, A9;

      end;

      ( - p) < ( - 0 qua Nat) by A1;

      then (g2 + ( - p)) < (g2 + 0 qua Nat) by XREAL_1: 6;

      hence contradiction by A2, A9, A12;

    end;

    theorem :: SEQ_4:3

    

     Th3: for r holds ex n st r < n

    proof

      let r;

      for r st r in NAT holds (r + 1) in NAT by AXIOMS: 2;

      then

      consider p such that

       A1: p in NAT and

       A2: r < p by Th2, NUMBERS: 19;

      consider n1 such that

       A3: n1 = p by A1;

      take n1;

      thus thesis by A2, A3;

    end;

    theorem :: SEQ_4:4

    X is real-bounded iff ex s st 0 < s & for r st r in X holds |.r.| < s

    proof

      thus X is real-bounded implies ex s st 0 < s & for r st r in X holds |.r.| < s

      proof

        assume

         A1: X is real-bounded;

        then

        consider s1 such that

         A2: s1 is UpperBound of X by XXREAL_2:def 10;

        

         A3: for r st r in X holds r <= s1 by A2, XXREAL_2:def 1;

        consider s2 such that

         A4: s2 is LowerBound of X by A1, XXREAL_2:def 9;

        

         A5: for r st r in X holds s2 <= r by A4, XXREAL_2:def 2;

        take s = (( |.s1.| + |.s2.|) + 1);

        

         A6: 0 <= |.s1.| by COMPLEX1: 46;

        

         A7: 0 <= |.s2.| by COMPLEX1: 46;

        hence 0 < s by A6;

        let r such that

         A8: r in X;

        s1 <= |.s1.| & r <= s1 by A3, A8, ABSVALUE: 4;

        then r <= |.s1.| by XXREAL_0: 2;

        then (r + 0 qua Nat) <= ( |.s1.| + |.s2.|) by A7, XREAL_1: 7;

        then

         A9: r < s by XREAL_1: 8;

        ( - |.s2.|) <= s2 & s2 <= r by A5, A8, ABSVALUE: 4;

        then ( - |.s2.|) <= r by XXREAL_0: 2;

        then (( - |.s1.|) + ( - |.s2.|)) <= ( 0 qua Nat + r) by A6, XREAL_1: 7;

        then

         A10: ((( - |.s1.|) - |.s2.|) + ( - 1)) < (r + 0 qua Nat) by XREAL_1: 8;

        ((( - |.s1.|) - |.s2.|) - 1) = ( - (( |.s1.| + |.s2.|) + 1));

        hence thesis by A9, A10, SEQ_2: 1;

      end;

      given s such that 0 < s and

       A11: for r st r in X holds |.r.| < s;

      thus X is bounded_below

      proof

        take ( - s);

        let r be ExtReal;

        assume

         A12: r in X;

        then

        reconsider r as Real;

         |.r.| < s by A11, A12;

        then

         A13: ( - s) < ( - |.r.|) by XREAL_1: 24;

        ( - |.r.|) <= r by ABSVALUE: 4;

        hence thesis by A13, XXREAL_0: 2;

      end;

      take s;

      let r be ExtReal;

      assume

       A14: r in X;

      then

      reconsider r as Real;

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

      hence thesis by A11, A14, XXREAL_0: 2;

    end;

    definition

      let r;

      :: original: {

      redefine

      func {r} -> Subset of REAL ;

      coherence

      proof

         {r} c= REAL by XREAL_0:def 1;

        hence thesis;

      end;

    end

    theorem :: SEQ_4:5

    

     Th5: for X be real-membered set holds X is non empty bounded_above implies ex g st (for r st r in X holds r <= g) & for s st 0 < s holds ex r st r in X & (g - s) < r

    proof

      let X be real-membered set;

      assume that

       A1: X is non empty and

       A2: X is bounded_above;

      consider p1 such that

       A3: p1 is UpperBound of X by A2;

      

       A4: for r st r in X holds r <= p1 by A3, XXREAL_2:def 1;

      defpred X[ Real] means for r st r in X holds r <= $1;

      consider Y such that

       A5: for p be Element of REAL holds p in Y iff X[p] from SUBSET_1:sch 3;

      X is Subset of REAL & for r, p st r in X & p in Y holds r <= p by A5, MEMBERED: 3;

      then

      consider g1 such that

       A6: for r, p st r in X & p in Y holds r <= g1 & g1 <= p by AXIOMS: 1;

      reconsider g1 as Real;

      take g = g1;

      

       A7: ex r1 be Real st r1 in X by A1;

       A8:

      now

        given s1 such that

         A9: 0 < s1 and

         A10: for r st r in X holds not (g - s1) < r;

        reconsider gs1 = (g - s1) as Element of REAL by XREAL_0:def 1;

        gs1 in Y by A5, A10;

        then g <= (g - s1) by A7, A6;

        then (g - (g - s1)) <= ((g - s1) - (g - s1)) by XREAL_1: 9;

        hence contradiction by A9;

      end;

      p1 in REAL by XREAL_0:def 1;

      then p1 in Y by A4, A5;

      hence thesis by A6, A8;

    end;

    theorem :: SEQ_4:6

    

     Th6: for X be real-membered set holds (for r st r in X holds r <= g1) & (for s st 0 < s holds ex r st (r in X & (g1 - s) < r)) & (for r st r in X holds r <= g2) & (for s st 0 < s holds ex r st (r in X & (g2 - s) < r)) implies g1 = g2

    proof

      let X be real-membered set;

      assume that

       A1: for r st r in X holds r <= g1 and

       A2: for s st 0 < s holds ex r st r in X & (g1 - s) < r and

       A3: for r st r in X holds r <= g2 and

       A4: for s st 0 < s holds ex r st r in X & (g2 - s) < r;

       A5:

      now

        assume g2 < g1;

        then ex r1 st r1 in X & (g1 - (g1 - g2)) < r1 by A2, XREAL_1: 50;

        hence contradiction by A3;

      end;

      now

        assume g1 < g2;

        then ex r1 st r1 in X & (g2 - (g2 - g1)) < r1 by A4, XREAL_1: 50;

        hence contradiction by A1;

      end;

      hence thesis by A5, XXREAL_0: 1;

    end;

    theorem :: SEQ_4:7

    

     Th7: for X be real-membered set holds X is non empty bounded_below implies ex g st (for r st r in X holds g <= r) & for s st 0 < s holds ex r st r in X & r < (g + s)

    proof

      let X be real-membered set;

      assume that

       A1: X is non empty and

       A2: X is bounded_below;

      

       A3: ex r1 be Real st r1 in X by A1;

      consider p1 such that

       A4: p1 is LowerBound of X by A2;

      

       A5: for r st r in X holds p1 <= r by A4, XXREAL_2:def 2;

      reconsider X as Subset of REAL by MEMBERED: 3;

      defpred X[ Real] means for r st r in X holds $1 <= r;

      consider Y such that

       A6: for p be Element of REAL holds p in Y iff X[p] from SUBSET_1:sch 3;

      for p, r st p in Y & r in X holds p <= r by A6;

      then

      consider g1 such that

       A7: for p, r st p in Y & r in X holds p <= g1 & g1 <= r by AXIOMS: 1;

      reconsider g1 as Real;

      take g = g1;

       A8:

      now

        given s1 such that

         A9: 0 < s1 and

         A10: for r st r in X holds not r < (g + s1);

        reconsider gs1 = (g + s1) as Element of REAL by XREAL_0:def 1;

        gs1 in Y by A6, A10;

        then (g + s1) <= g by A3, A7;

        then ((g + s1) - g) <= (g - g) by XREAL_1: 9;

        hence contradiction by A9;

      end;

      p1 in REAL by XREAL_0:def 1;

      then p1 in Y by A5, A6;

      hence thesis by A7, A8;

    end;

    theorem :: SEQ_4:8

    

     Th8: for X be real-membered set holds (for r st r in X holds g1 <= r) & (for s st 0 < s holds ex r st (r in X & r < (g1 + s))) & (for r st r in X holds g2 <= r) & (for s st 0 < s holds ex r st (r in X & r < (g2 + s))) implies g1 = g2

    proof

      let X be real-membered set;

      assume that

       A1: for r st r in X holds g1 <= r and

       A2: for s st 0 < s holds ex r st r in X & r < (g1 + s) and

       A3: for r st r in X holds g2 <= r and

       A4: for s st 0 < s holds ex r st r in X & r < (g2 + s);

       A5:

      now

        assume g2 < g1;

        then ex r1 st r1 in X & r1 < (g2 + (g1 - g2)) by A4, XREAL_1: 50;

        hence contradiction by A1;

      end;

      now

        assume g1 < g2;

        then ex r1 st r1 in X & r1 < (g1 + (g2 - g1)) by A2, XREAL_1: 50;

        hence contradiction by A3;

      end;

      hence thesis by A5, XXREAL_0: 1;

    end;

    definition

      let X be real-membered set;

      assume

       A1: X is non empty bounded_above;

      :: SEQ_4:def1

      func upper_bound X -> Real means

      : Def1: (for r st r in X holds r <= it ) & for s st 0 < s holds ex r st r in X & (it - s) < r;

      existence by A1, Th5;

      uniqueness by Th6;

    end

    definition

      let X be real-membered set;

      assume

       A1: X is non empty bounded_below;

      :: SEQ_4:def2

      func lower_bound X -> Real means

      : Def2: (for r st r in X holds it <= r) & for s st 0 < s holds ex r st r in X & r < (it + s);

      existence by A1, Th7;

      uniqueness by Th8;

    end

    

     Lm1: for X be non empty real-membered set st (for s st s in X holds s >= r) & for t st for s st s in X holds s >= t holds r >= t holds r = ( lower_bound X)

    proof

      let X be non empty real-membered set;

      assume that

       A1: for s st s in X holds s >= r and

       A2: for t st for s st s in X holds s >= t holds r >= t;

      

       A3: for s be Real st 0 < s holds not for t be Real st t in X holds t >= (r + s) by A2, XREAL_1: 29;

      X is bounded_below

      proof

        take r;

        let s be ExtReal;

        assume s in X;

        hence thesis by A1;

      end;

      hence thesis by A1, A3, Def2;

    end;

    

     Lm2: for X be non empty real-membered set, r st (for s st s in X holds s <= r) & for t st for s st s in X holds s <= t holds r <= t holds r = ( upper_bound X)

    proof

      let X be non empty real-membered set, r;

      assume that

       A1: for s st s in X holds s <= r and

       A2: for t st for s st s in X holds s <= t holds r <= t;

       A3:

      now

        let s be Real such that

         A4: 0 < s;

        assume for t be Real st t in X holds (r - s) >= t;

        then r <= (r - s) by A2;

        then (r + s) <= r by XREAL_1: 19;

        hence contradiction by A4, XREAL_1: 29;

      end;

      X is bounded_above

      proof

        take r;

        let s be ExtReal;

        assume s in X;

        hence thesis by A1;

      end;

      hence thesis by A1, A3, Def1;

    end;

    registration

      let X be non empty bounded_below real-membered set;

      identify inf X with lower_bound X;

      compatibility

      proof

         A1:

        now

          let t;

          assume for s st s in X holds s >= t;

          then for x be ExtReal st x in X holds t <= x;

          then t is LowerBound of X by XXREAL_2:def 2;

          hence ( inf X) >= t by XXREAL_2:def 4;

        end;

        for s st s in X holds s >= ( inf X) by XXREAL_2: 3;

        hence thesis by A1, Lm1;

      end;

    end

    registration

      let X be non empty bounded_above real-membered set;

      identify sup X with upper_bound X;

      compatibility

      proof

         A1:

        now

          let t;

          assume for s st s in X holds t >= s;

          then for x be ExtReal st x in X holds x <= t;

          then t is UpperBound of X by XXREAL_2:def 1;

          hence t >= ( sup X) by XXREAL_2:def 3;

        end;

        for s st s in X holds s <= ( sup X) by XXREAL_2: 4;

        hence thesis by A1, Lm2;

      end;

    end

    theorem :: SEQ_4:9

    

     Th9: ( lower_bound {r}) = r & ( upper_bound {r}) = r by XXREAL_2: 11, XXREAL_2: 13;

    theorem :: SEQ_4:10

    

     Th10: ( lower_bound {r}) = ( upper_bound {r})

    proof

      ( lower_bound {r}) = r by XXREAL_2: 13;

      hence thesis by XXREAL_2: 11;

    end;

    theorem :: SEQ_4:11

    X is real-bounded non empty implies ( lower_bound X) <= ( upper_bound X)

    proof

      assume X is real-bounded non empty;

      then

      reconsider X as real-bounded non empty real-membered set;

      ( lower_bound X) <= ( upper_bound X) by XXREAL_2: 40;

      hence thesis;

    end;

    theorem :: SEQ_4:12

    X is real-bounded non empty implies ((ex r, p st r in X & p in X & p <> r) iff ( lower_bound X) < ( upper_bound X))

    proof

      assume that

       A1: X is real-bounded and

       A2: X is non empty;

      thus (ex r, p st r in X & p in X & p <> r) implies ( lower_bound X) < ( upper_bound X)

      proof

        given r, p such that

         A3: r in X and

         A4: p in X and

         A5: p <> r;

         A6:

        now

          assume

           A7: r < p;

          ( lower_bound X) <= r by A1, A3, Def2;

          then

           A8: ( lower_bound X) < p by A7, XXREAL_0: 2;

          p <= ( upper_bound X) by A1, A4, Def1;

          hence thesis by A8, XXREAL_0: 2;

        end;

        now

          assume

           A9: p < r;

          ( lower_bound X) <= p by A1, A4, Def2;

          then

           A10: ( lower_bound X) < r by A9, XXREAL_0: 2;

          r <= ( upper_bound X) by A1, A3, Def1;

          hence thesis by A10, XXREAL_0: 2;

        end;

        hence thesis by A5, A6, XXREAL_0: 1;

      end;

      consider r be Element of REAL such that

       A11: r in X by A2;

      assume that

       A12: ( lower_bound X) < ( upper_bound X) and

       A13: for r, p st r in X & p in X holds p = r;

      for x be object holds x in X iff x = r by A13, A11;

      then X = {r} by TARSKI:def 1;

      hence contradiction by A12, Th10;

    end;

    theorem :: SEQ_4:13

    

     Th13: seq is convergent implies ( abs seq) is convergent

    proof

      assume seq is convergent;

      then

      consider g1 such that

       A1: for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - g1).| < p;

      reconsider g1 as Real;

      take g = |.g1.|;

      let p;

      assume 0 < p;

      then

      consider n1 such that

       A2: for m st n1 <= m holds |.((seq . m) - g1).| < p by A1;

      take n = n1;

      let m;

       |.(g1 - (seq . m)).| = |.( - ((seq . m) - g1)).|

      .= |.((seq . m) - g1).| by COMPLEX1: 52;

      then (g - |.(seq . m).|) <= |.((seq . m) - g1).| by COMPLEX1: 59;

      then ( |.(seq . m).| - g) <= |.((seq . m) - g1).| & ( - |.((seq . m) - g1).|) <= ( - (g - |.(seq . m).|)) by COMPLEX1: 59, XREAL_1: 24;

      then |.( |.(seq . m).| - g).| <= |.((seq . m) - g1).| by ABSVALUE: 5;

      then

       A3: |.((( abs seq) . m) - g).| <= |.((seq . m) - g1).| by SEQ_1: 12;

      assume n <= m;

      then |.((seq . m) - g1).| < p by A2;

      hence thesis by A3, XXREAL_0: 2;

    end;

    registration

      let seq be convergent Real_Sequence;

      cluster ( abs seq) -> convergent;

      coherence by Th13;

    end

    theorem :: SEQ_4:14

    seq is convergent implies ( lim ( abs seq)) = |.( lim seq).|

    proof

      assume

       A1: seq is convergent;

      now

        let p;

        assume 0 < p;

        then

        consider n1 such that

         A2: for m st n1 <= m holds |.((seq . m) - ( lim seq)).| < p by A1, SEQ_2:def 7;

        take n = n1;

        let m;

         |.(( lim seq) - (seq . m)).| = |.( - ((seq . m) - ( lim seq))).|

        .= |.((seq . m) - ( lim seq)).| by COMPLEX1: 52;

        then ( |.( lim seq).| - |.(seq . m).|) <= |.((seq . m) - ( lim seq)).| by COMPLEX1: 59;

        then ( |.(seq . m).| - |.( lim seq).|) <= |.((seq . m) - ( lim seq)).| & ( - |.((seq . m) - ( lim seq)).|) <= ( - ( |.( lim seq).| - |.(seq . m).|)) by COMPLEX1: 59, XREAL_1: 24;

        then |.( |.(seq . m).| - |.( lim seq).|).| <= |.((seq . m) - ( lim seq)).| by ABSVALUE: 5;

        then

         A3: |.((( abs seq) . m) - |.( lim seq).|).| <= |.((seq . m) - ( lim seq)).| by SEQ_1: 12;

        assume n <= m;

        then |.((seq . m) - ( lim seq)).| < p by A2;

        hence |.((( abs seq) . m) - |.( lim seq).|).| < p by A3, XXREAL_0: 2;

      end;

      hence thesis by A1, SEQ_2:def 7;

    end;

    theorem :: SEQ_4:15

    ( abs seq) is convergent & ( lim ( abs seq)) = 0 implies seq is convergent & ( lim seq) = 0

    proof

      assume that

       A1: ( abs seq) is convergent and

       A2: ( lim ( abs seq)) = 0 ;

       A3:

      now

        let n;

        ( - |.(seq . n).|) <= (seq . n) by ABSVALUE: 4;

        then

         A4: ( - (( abs seq) . n)) <= (seq . n) by SEQ_1: 12;

        (seq . n) <= |.(seq . n).| by ABSVALUE: 4;

        hence (( - ( abs seq)) . n) <= (seq . n) & (seq . n) <= (( abs seq) . n) by A4, SEQ_1: 10, SEQ_1: 12;

      end;

      

       A5: ( - ( abs seq)) is convergent & ( lim ( - ( abs seq))) = ( - ( lim ( abs seq))) by A1, SEQ_2: 10;

      hence seq is convergent by A1, A2, A3, SEQ_2: 19;

      thus thesis by A1, A2, A5, A3, SEQ_2: 20;

    end;

    theorem :: SEQ_4:16

    

     Th16: seq1 is subsequence of seq & seq is convergent implies seq1 is convergent

    proof

      assume that

       A1: seq1 is subsequence of seq and

       A2: seq is convergent;

      consider g1 such that

       A3: for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - g1).| < p by A2;

      take g1;

      let p;

      assume 0 < p;

      then

      consider n1 such that

       A4: for m st n1 <= m holds |.((seq . m) - g1).| < p by A3;

      take n = n1;

      let m such that

       A5: n <= m;

      consider Nseq such that

       A6: seq1 = (seq * Nseq) by A1, VALUED_0:def 17;

      m <= (Nseq . m) by SEQM_3: 14;

      then

       A7: n <= (Nseq . m) by A5, XXREAL_0: 2;

      m in NAT by ORDINAL1:def 12;

      then (seq1 . m) = (seq . (Nseq . m)) by A6, FUNCT_2: 15;

      hence thesis by A4, A7;

    end;

    theorem :: SEQ_4:17

    

     Th17: seq1 is subsequence of seq & seq is convergent implies ( lim seq1) = ( lim seq)

    proof

      assume that

       A1: seq1 is subsequence of seq and

       A2: seq is convergent;

      consider Nseq such that

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

       A4:

      now

        let p;

        assume 0 < p;

        then

        consider n1 such that

         A5: for m st n1 <= m holds |.((seq . m) - ( lim seq)).| < p by A2, SEQ_2:def 7;

        take n = n1;

        let m such that

         A6: n <= m;

        m <= (Nseq . m) by SEQM_3: 14;

        then

         A7: n <= (Nseq . m) by A6, XXREAL_0: 2;

        m in NAT by ORDINAL1:def 12;

        then (seq1 . m) = (seq . (Nseq . m)) by A3, FUNCT_2: 15;

        hence |.((seq1 . m) - ( lim seq)).| < p by A5, A7;

      end;

      seq1 is convergent by A1, A2, Th16;

      hence thesis by A4, SEQ_2:def 7;

    end;

    theorem :: SEQ_4:18

    

     Th18: seq is convergent & (ex k st for n st k <= n holds (seq1 . n) = (seq . n)) implies seq1 is convergent

    proof

      assume that

       A1: seq is convergent and

       A2: ex k st for n st k <= n holds (seq1 . n) = (seq . n);

      consider g1 such that

       A3: for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - g1).| < p by A1;

      consider k such that

       A4: for n st k <= n holds (seq1 . n) = (seq . n) by A2;

      take g = g1;

      let p;

      assume 0 < p;

      then

      consider n1 such that

       A5: for m st n1 <= m holds |.((seq . m) - g1).| < p by A3;

       A6:

      now

        assume

         A7: n1 <= k;

        take n = k;

        let m;

        assume

         A8: n <= m;

        then n1 <= m by A7, XXREAL_0: 2;

        then |.((seq . m) - g1).| < p by A5;

        hence |.((seq1 . m) - g).| < p by A4, A8;

      end;

      now

        assume

         A9: k <= n1;

        take n = n1;

        let m;

        assume

         A10: n <= m;

        then (seq1 . m) = (seq . m) by A4, A9, XXREAL_0: 2;

        hence |.((seq1 . m) - g).| < p by A5, A10;

      end;

      hence thesis by A6;

    end;

    theorem :: SEQ_4:19

    seq is convergent & (ex k st for n st k <= n holds (seq1 . n) = (seq . n)) implies ( lim seq) = ( lim seq1)

    proof

      assume that

       A1: seq is convergent;

      given k such that

       A2: for n st k <= n holds (seq1 . n) = (seq . n);

       A3:

      now

        let p;

        assume 0 < p;

        then

        consider n1 such that

         A4: for m st n1 <= m holds |.((seq . m) - ( lim seq)).| < p by A1, SEQ_2:def 7;

         A5:

        now

          assume

           A6: n1 <= k;

          take n = k;

          let m;

          assume

           A7: n <= m;

          then n1 <= m by A6, XXREAL_0: 2;

          then |.((seq . m) - ( lim seq)).| < p by A4;

          hence |.((seq1 . m) - ( lim seq)).| < p by A2, A7;

        end;

        now

          assume

           A8: k <= n1;

          take n = n1;

          let m;

          assume

           A9: n <= m;

          then (seq1 . m) = (seq . m) by A2, A8, XXREAL_0: 2;

          hence |.((seq1 . m) - ( lim seq)).| < p by A4, A9;

        end;

        hence ex n st for m st n <= m holds |.((seq1 . m) - ( lim seq)).| < p by A5;

      end;

      seq1 is convergent by A1, A2, Th18;

      hence thesis by A3, SEQ_2:def 7;

    end;

    registration

      let seq be convergent Real_Sequence;

      let k;

      cluster (seq ^\ k) -> convergent;

      coherence by Th16;

    end

    theorem :: SEQ_4:20

    seq is convergent implies ( lim (seq ^\ k)) = ( lim seq) by Th17;

    theorem :: SEQ_4:21

    

     Th21: (seq ^\ k) is convergent implies seq is convergent

    proof

      assume (seq ^\ k) is convergent;

      then

      consider g1 such that

       A1: for p st 0 < p holds ex n st for m st n <= m holds |.(((seq ^\ k) . m) - g1).| < p;

      take g1;

      let p;

      assume 0 < p;

      then

      consider n1 such that

       A2: for m st n1 <= m holds |.(((seq ^\ k) . m) - g1).| < p by A1;

      take n = (n1 + k);

      let m;

      assume

       A3: n <= m;

      then

      consider l be Nat such that

       A4: m = ((n1 + k) + l) by NAT_1: 10;

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

      (m - k) = (((n1 + l) + k) + ( - k)) by A4;

      then

      consider m1 be Element of NAT such that

       A5: m1 = (m - k);

      now

        assume not n1 <= m1;

        then (m1 + k) < (n1 + k) by XREAL_1: 6;

        hence contradiction by A3, A5;

      end;

      then

       A6: |.(((seq ^\ k) . m1) - g1).| < p by A2;

      (m1 + k) = m by A5;

      hence thesis by A6, NAT_1:def 3;

    end;

    theorem :: SEQ_4:22

    (seq ^\ k) is convergent implies ( lim seq) = ( lim (seq ^\ k))

    proof

      assume

       A1: (seq ^\ k) is convergent;

       A2:

      now

        let p;

        assume 0 < p;

        then

        consider n1 such that

         A3: for m st n1 <= m holds |.(((seq ^\ k) . m) - ( lim (seq ^\ k))).| < p by A1, SEQ_2:def 7;

        take n = (n1 + k);

        let m;

        assume

         A4: n <= m;

        then

        consider l be Nat such that

         A5: m = ((n1 + k) + l) by NAT_1: 10;

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

        (m - k) = (((n1 + l) + k) + ( - k)) by A5;

        then

        consider m1 such that

         A6: m1 = (m - k);

        now

          assume not n1 <= m1;

          then (m1 + k) < (n1 + k) by XREAL_1: 6;

          hence contradiction by A4, A6;

        end;

        then

         A7: |.(((seq ^\ k) . m1) - ( lim (seq ^\ k))).| < p by A3;

        (m1 + k) = m by A6;

        hence |.((seq . m) - ( lim (seq ^\ k))).| < p by A7, NAT_1:def 3;

      end;

      seq is convergent by A1, Th21;

      hence thesis by A2, SEQ_2:def 7;

    end;

    theorem :: SEQ_4:23

    

     Th23: seq is convergent & ( lim seq) <> 0 implies ex k st (seq ^\ k) is non-zero

    proof

      assume that

       A1: seq is convergent and

       A2: ( lim seq) <> 0 ;

      consider n1 such that

       A3: for m st n1 <= m holds ( |.( lim seq).| / 2) < |.(seq . m).| by A1, A2, SEQ_2: 16;

      take k = n1;

      now

        let n;

        ( 0 qua Nat + k) <= (n + k) by XREAL_1: 7;

        then ( |.( lim seq).| / 2) < |.(seq . (n + k)).| by A3;

        then

         A4: ( |.( lim seq).| / 2) < |.((seq ^\ k) . n).| by NAT_1:def 3;

         0 < |.( lim seq).| by A2, COMPLEX1: 47;

        then ( 0 / 2) < ( |.( lim seq).| / 2);

        hence ((seq ^\ k) . n) <> 0 by A4, ABSVALUE: 2;

      end;

      hence thesis by SEQ_1: 5;

    end;

    theorem :: SEQ_4:24

    seq is convergent & ( lim seq) <> 0 implies ex seq1 st seq1 is subsequence of seq & seq1 is non-zero

    proof

      assume seq is convergent & ( lim seq) <> 0 ;

      then

      consider k such that

       A1: (seq ^\ k) is non-zero by Th23;

      take (seq ^\ k);

      thus thesis by A1;

    end;

    theorem :: SEQ_4:25

    

     Th25: seq is constant & (r in ( rng seq) or ex n st (seq . n) = r) implies ( lim seq) = r

    proof

      assume

       A1: seq is constant;

      then

      consider r1 be Element of REAL such that

       A2: ( rng seq) = {r1} by FUNCT_2: 111;

       A3:

      now

        assume that

         A4: r in ( rng seq);

        consider r2 be Element of REAL such that

         A5: for n be Nat holds (seq . n) = r2 by A1, VALUED_0:def 18;

        

         A6: r = r1 by A4, A2, TARSKI:def 1;

        reconsider zz = 0 as Nat;

        now

          let p such that

           A7: 0 < p;

          take n = zz;

          let m such that n <= m;

          m in NAT by ORDINAL1:def 12;

          then m in ( dom seq) by FUNCT_2:def 1;

          then (seq . m) in ( rng seq) by FUNCT_1:def 3;

          then r2 in ( rng seq) by A5;

          then r2 = r by A2, A6, TARSKI:def 1;

          then (seq . m) = r by A5;

          hence |.((seq . m) - r).| < p by A7, ABSVALUE: 2;

        end;

        hence thesis by A1, SEQ_2:def 7;

      end;

       A8:

      now

        assume that

         A9: ex n st (seq . n) = r;

        consider n such that

         A10: (seq . n) = r by A9;

        n in NAT by ORDINAL1:def 12;

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

        hence thesis by A3, A10, FUNCT_1:def 3;

      end;

      assume r in ( rng seq) or ex n st (seq . n) = r;

      hence thesis by A3, A8;

    end;

    theorem :: SEQ_4:26

    seq is constant implies for n holds ( lim seq) = (seq . n) by Th25;

    theorem :: SEQ_4:27

    seq is convergent & ( lim seq) <> 0 implies for seq1 st seq1 is subsequence of seq & seq1 is non-zero holds ( lim (seq1 " )) = (( lim seq) " )

    proof

      assume that

       A1: seq is convergent and

       A2: ( lim seq) <> 0 ;

      let seq1 such that

       A3: seq1 is subsequence of seq and

       A4: seq1 is non-zero;

      ( lim seq1) = ( lim seq) by A1, A3, Th17;

      hence thesis by A1, A2, A3, A4, Th16, SEQ_2: 22;

    end;

    ::$Canceled

    

     LmTh28: (for n holds (seq . n) = (1 / (n + r))) implies for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - 0 ).| < p

    proof

      assume

       A0: for n holds (seq . n) = (1 / (n + r));

      let p such that

       A1: 0 < p;

      consider n such that

       A3: n > ((1 / p) - r) by Th3;

      take n;

      let m such that

       A2: n <= m;

      

       B0: (seq . m) = (1 / (m + r)) by A0;

      ((1 / p) - r) < m by A3, A2, XXREAL_0: 2;

      then

       A4: (((1 / p) - r) + r) < (m + r) by XREAL_1: 8;

      then ((p " ) " ) > ((m + r) " ) by A1, XREAL_1: 88;

      then

       B1: (1 / (m + r)) < p;

      

       B2: ( - p) < ( - 0 ) by A1;

       0 <= (m + r) by A1, A4;

      then ( - p) < (1 / (m + r)) by B2;

      hence thesis by B0, B1, SEQ_2: 1;

    end;

    

     Th28: (for n holds (seq . n) = (1 / (n + r))) implies seq is convergent

    proof

      assume

       A0: for n holds (seq . n) = (1 / (n + r));

      take 0 ;

      let p;

      assume 0 < p;

      then

      consider n such that

       A2: for m st n <= m holds |.((seq . m) - 0 ).| < p by A0, LmTh28;

      take n;

      thus thesis by A2;

    end;

    

     Th29: (for n holds (seq . n) = (1 / (n + r))) implies ( lim seq) = 0

    proof

      assume

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

      then

       A2: seq is convergent by Th28;

      for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - 0 ).| < p by A1, LmTh28;

      hence thesis by A2, SEQ_2:def 7;

    end;

    theorem :: SEQ_4:31

    (for n holds (seq . n) = (g / (n + r))) implies seq is convergent & ( lim seq) = 0

    proof

      assume

       A2: for n holds (seq . n) = (g / (n + r));

      reconsider r1 = r as Real;

      deffunc U( Nat) = (1 / ($1 + r1));

      consider seq1 such that

       A3: for n holds (seq1 . n) = U(n) from SEQ_1:sch 1;

       A4:

      now

        let n be Element of NAT ;

        

        thus ((g (#) seq1) . n) = (g * (seq1 . n)) by SEQ_1: 9

        .= (g * (1 / (n + r))) by A3

        .= (g * (1 * ((n + r) " )))

        .= (g / (n + r))

        .= (seq . n) by A2;

      end;

      

       A5: (g (#) seq1) is convergent by A3, Th28, SEQ_2: 7;

      ( lim (g (#) seq1)) = (g * ( lim seq1)) by A3, Th28, SEQ_2: 8

      .= (g * 0 qua Nat) by A3, Th29

      .= 0 ;

      hence thesis by A5, A4, FUNCT_2: 63;

    end;

    ::$Canceled

    

     LmTh32: 0 <= r & (for n holds (seq . n) = (1 / ((n * n) + r))) implies for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - 0 ).| < p

    proof

      assume that

       A1: 0 <= r and

       A2: for n holds (seq . n) = (1 / ((n * n) + r));

      let p;

      consider k1 such that

       A3: (p " ) < k1 by Th3;

      assume

       A4: 0 < p;

      then

       A5: k1 > 0 by A3;

      then k1 >= (1 + 0 qua Nat) by NAT_1: 13;

      then k1 <= (k1 * k1) by XREAL_1: 151;

      then

       A6: (k1 + r) <= ((k1 * k1) + r) by XREAL_1: 6;

      take n = k1;

      let m such that

       A7: n <= m;

      (n * n) <= (m * m) by A7, XREAL_1: 66;

      then

       A8: ((n * n) + r) <= ((m * m) + r) by XREAL_1: 6;

      ((p " ) + 0 qua Nat) < (k1 + r) by A1, A3, XREAL_1: 8;

      then ((p " ) + 0 qua Nat) < ((k1 * k1) + r) by A6, XXREAL_0: 2;

      then (1 / ((k1 * k1) + r)) < (1 / (p " )) by A4, XREAL_1: 76;

      then

       A9: (1 / ((k1 * k1) + r)) < (1 * ((p " ) " ));

       0 < (n ^2 ) by A5;

      then (1 / ((m * m) + r)) <= (1 / ((n * n) + r)) by A1, A8, XREAL_1: 118;

      then

       A10: (1 / ((m * m) + r)) < p by A9, XXREAL_0: 2;

      (seq . m) = (1 / ((m * m) + r)) by A2;

      hence thesis by A1, A10, ABSVALUE:def 1;

    end;

    

     Th32: 0 <= r & (for n holds (seq . n) = (1 / ((n * n) + r))) implies seq is convergent

    proof

      assume that

       A1: 0 <= r and

       A2: for n holds (seq . n) = (1 / ((n * n) + r));

      take 0 ;

      let p;

      assume 0 < p;

      then

      consider n such that

       A3: for m st n <= m holds |.((seq . m) - 0 ).| < p by A1, A2, LmTh32;

      take n;

      thus thesis by A3;

    end;

    

     Th33: 0 <= r & (for n holds (seq . n) = (1 / ((n * n) + r))) implies ( lim seq) = 0

    proof

      assume that

       A1: 0 <= r and

       A2: for n holds (seq . n) = (1 / ((n * n) + r));

      

       A3: seq is convergent by A1, A2, Th32;

      for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - 0 ).| < p by A1, A2, LmTh32;

      hence thesis by A3, SEQ_2:def 7;

    end;

    theorem :: SEQ_4:35

     0 <= r & (for n holds (seq . n) = (g / ((n * n) + r))) implies seq is convergent & ( lim seq) = 0

    proof

      assume that

       A1: 0 <= r and

       A2: for n holds (seq . n) = (g / ((n * n) + r));

      reconsider r1 = r as Real;

      deffunc U( Nat) = (1 / (($1 * $1) + r1));

      consider seq1 such that

       A3: for n holds (seq1 . n) = U(n) from SEQ_1:sch 1;

       A4:

      now

        let n be Element of NAT ;

        

        thus ((g (#) seq1) . n) = (g * (seq1 . n)) by SEQ_1: 9

        .= (g * (1 / ((n * n) + r))) by A3

        .= (g * (1 * (((n * n) + r) " )))

        .= (g / ((n * n) + r))

        .= (seq . n) by A2;

      end;

      

       A5: (g (#) seq1) is convergent by A1, A3, Th32, SEQ_2: 7;

      ( lim (g (#) seq1)) = (g * ( lim seq1)) by A1, A3, Th32, SEQ_2: 8

      .= (g * 0 qua Nat) by A1, A3, Th33

      .= 0 ;

      hence thesis by A5, A4, FUNCT_2: 63;

    end;

    registration

      cluster non-decreasing bounded_above -> convergent for Real_Sequence;

      coherence

      proof

        let seq be Real_Sequence;

        assume that

         A1: seq is non-decreasing and

         A2: seq is bounded_above;

        consider r2 such that

         A3: for n holds (seq . n) < r2 by A2;

        defpred X[ Real] means ex n st $1 = (seq . n);

        consider X such that

         A4: for p be Element of REAL holds p in X iff X[p] from SUBSET_1:sch 3;

         A5:

        now

          take r = r2;

          let p;

          assume p in X;

          then ex n1 st p = (seq . n1) by A4;

          hence p <= r by A3;

        end;

        

         A6: (ex r st for p be Real st p in X holds p <= r) implies X is bounded_above

        proof

          given r such that

           A7: for p be Real st p in X holds p <= r;

          take r;

          let p be ExtReal;

          thus thesis by A7;

        end;

        take g = ( upper_bound X);

        let s;

        assume

         A8: 0 < s;

        (seq . 0 ) in X by A4;

        then

        consider p1 such that

         A9: p1 in X and

         A10: (( upper_bound X) - s) < p1 by A6, A8, Def1;

        consider n1 such that

         A11: p1 = (seq . n1) by A4, A9;

        take n = n1;

        let m;

        assume n <= m;

        then (seq . n) <= (seq . m) by A1, SEQM_3: 6;

        then (g + ( - s)) < (seq . m) by A10, A11, XXREAL_0: 2;

        then

         A12: ( - s) < ((seq . m) - g) by XREAL_1: 20;

        (seq . m) in X by A4;

        then (seq . m) <= g by A6, A5, Def1;

        then ((seq . m) + 0 qua Nat) < (g + s) by A8, XREAL_1: 8;

        then ((seq . m) - g) < s by XREAL_1: 19;

        hence thesis by A12, SEQ_2: 1;

      end;

    end

    registration

      cluster non-increasing bounded_below -> convergent for Real_Sequence;

      coherence

      proof

        let seq be Real_Sequence;

        assume that

         A1: seq is non-increasing and

         A2: seq is bounded_below;

        defpred X[ Real] means ex n st $1 = (seq . n);

        consider X such that

         A3: for p be Element of REAL holds p in X iff X[p] from SUBSET_1:sch 3;

        take g = ( lower_bound X);

        let s;

        assume

         A4: 0 < s;

        

         A5: (ex r st for p be Real st p in X holds r <= p) implies X is bounded_below

        proof

          given r such that

           A6: for p be Real st p in X holds r <= p;

          take r;

          let p be ExtReal;

          thus thesis by A6;

        end;

        (seq . 0 ) in X by A3;

        then

        consider p1 such that

         A7: p1 in X and

         A8: p1 < (( lower_bound X) + s) by A5, A4, Def2;

        consider n1 such that

         A9: p1 = (seq . n1) by A3, A7;

        take n = n1;

        let m;

        consider r1 such that

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

         A11:

        now

          take r = r1;

          let p;

          assume p in X;

          then ex n1 st p = (seq . n1) by A3;

          hence r <= p by A10;

        end;

        (seq . m) in X by A3;

        then ( 0 qua Nat + g) <= (seq . m) by A5, A11, Def2;

        then

         A12: 0 <= ((seq . m) - g) by XREAL_1: 19;

        assume n <= m;

        then (seq . m) <= (seq . n) by A1, SEQM_3: 8;

        then (seq . m) < (g + s) by A8, A9, XXREAL_0: 2;

        then

         A13: ((seq . m) - g) < s by XREAL_1: 19;

        ( - s) < ( - 0 qua Nat) by A4;

        hence thesis by A13, A12, SEQ_2: 1;

      end;

    end

    registration

      cluster monotone bounded -> convergent for Real_Sequence;

      coherence

      proof

        let seq be Real_Sequence;

        assume that

         A1: seq is monotone and

         A2: seq is bounded;

        

         A3: seq is non-increasing implies thesis by A2;

        seq is non-decreasing implies thesis by A2;

        hence thesis by A1, A3, SEQM_3:def 5;

      end;

    end

    theorem :: SEQ_4:36

    

     Th36: seq is monotone & seq is bounded implies seq is convergent;

    theorem :: SEQ_4:37

    seq is bounded_above & seq is non-decreasing implies for n holds (seq . n) <= ( lim seq)

    proof

      assume that

       A1: seq is bounded_above and

       A2: seq is non-decreasing;

      let m;

      set seq1 = ( NAT --> (seq . m));

      deffunc U( Nat) = (seq . ($1 + m));

      consider seq2 such that

       A3: for n holds (seq2 . n) = U(n) from SEQ_1:sch 1;

       A4:

      now

        let n;

        n in NAT by ORDINAL1:def 12;

        then (seq1 . n) = (seq . m) & (seq2 . n) = (seq . (m + n)) by A3, FUNCOP_1: 7;

        hence (seq1 . n) <= (seq2 . n) by A2, SEQM_3: 5;

      end;

      (seq1 . 0 ) = (seq . m);

      then

       A5: ( lim seq1) = (seq . m) by Th25;

      for n be Nat holds (seq2 . n) = U(n) by A3;

      then

       A6: seq2 = (seq ^\ m) by NAT_1:def 3;

      then ( lim seq2) = ( lim seq) by A1, A2, Th17;

      hence thesis by A1, A2, A5, A6, A4, SEQ_2: 18;

    end;

    theorem :: SEQ_4:38

    seq is bounded_below & seq is non-increasing implies for n holds ( lim seq) <= (seq . n)

    proof

      assume that

       A1: seq is bounded_below and

       A2: seq is non-increasing;

      let m;

      set seq1 = ( NAT --> (seq . m));

      deffunc U( Nat) = (seq . ($1 + m));

      consider seq2 such that

       A3: for n holds (seq2 . n) = U(n) from SEQ_1:sch 1;

       A4:

      now

        let n;

        n in NAT by ORDINAL1:def 12;

        then (seq1 . n) = (seq . m) & (seq2 . n) = (seq . (m + n)) by A3, FUNCOP_1: 7;

        hence (seq2 . n) <= (seq1 . n) by A2, SEQM_3: 7;

      end;

      (seq1 . 0 ) = (seq . m);

      then

       A5: ( lim seq1) = (seq . m) by Th25;

      for n be Nat holds (seq2 . n) = U(n) by A3;

      then

       A6: seq2 = (seq ^\ m) by NAT_1:def 3;

      then ( lim seq2) = ( lim seq) by A1, A2, Th17;

      hence thesis by A1, A2, A5, A6, A4, SEQ_2: 18;

    end;

    theorem :: SEQ_4:39

    

     Th39: for seq holds ex Nseq st (seq * Nseq) is monotone

    proof

      let seq;

      defpred X[ Nat] means for m st $1 < m holds (seq . $1) < (seq . m);

      consider XN be Subset of NAT such that

       A1: for n be Element of NAT holds n in XN iff X[n] from SUBSET_1:sch 3;

       A2:

      now

        given k1 such that

         A3: for n st n in XN holds n <= k1;

        set seq1 = (seq ^\ (1 + k1));

        defpred P[ set, set, set] means for k, l st k = $2 & l = $3 holds k < l & (seq1 . l) <= (seq1 . k) & for m st k < m & (seq1 . m) <= (seq1 . k) holds l <= m;

         A4:

        now

          let k;

          

           A5: k in NAT by ORDINAL1:def 12;

          assume k1 < k;

          then not k in XN by A3;

          then

          consider m such that

           A6: k < m and

           A7: not (seq . k) < (seq . m) by A1, A5;

          take n = m;

          thus k < n by A6;

          thus (seq . n) <= (seq . k) by A7;

        end;

         A8:

        now

          let k;

          ( 0 qua Nat + k1) < ((k + 1) + k1) by XREAL_1: 8;

          then

          consider n such that

           A9: ((k + 1) + k1) < n and

           A10: (seq . n) <= (seq . ((k + 1) + k1)) by A4;

          consider m be Nat such that

           A11: n = (((k + 1) + k1) + m) by A9, NAT_1: 10;

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

          (n - (1 + k1)) = ((k + 0 qua Nat) + m) by A11;

          then

          consider n1 be Element of NAT such that

           A12: n1 = (n - (1 + k1));

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

          then

           A13: (seq . n) <= (seq1 . k) by NAT_1:def 3;

          take l = n1;

          now

            assume not k < l;

            then ((n - (1 + k1)) + (1 + k1)) <= (k + (1 + k1)) by A12, XREAL_1: 6;

            hence contradiction by A9;

          end;

          hence k < l;

          n = (l + (1 + k1)) by A12;

          hence (seq1 . l) <= (seq1 . k) by A13, NAT_1:def 3;

        end;

        

         A14: for n be Nat holds for x be Element of NAT holds ex y be Element of NAT st P[n, x, y]

        proof

          let n be Nat, x be Element of NAT ;

          defpred X[ Nat] means x < $1 & (seq1 . $1) <= (seq1 . x);

          ex n be Element of NAT st X[n] by A8;

          then

           A15: ex n be Nat st X[n];

          ex l be Nat st X[l] & for m be Nat st X[m] holds l <= m from NAT_1:sch 5( A15);

          then

          consider l be Nat such that

           A16: x < l & (seq1 . l) <= (seq1 . x) & for m be Nat st x < m & (seq1 . m) <= (seq1 . x) holds l <= m;

          take l;

          l in NAT by ORDINAL1:def 12;

          hence thesis by A16;

        end;

        consider f be sequence of NAT such that (f . 0 ) = 0 and

         A17: for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A14);

        

         A18: ( dom f) = NAT by FUNCT_2:def 1;

        ( rng f) c= REAL ;

        then

        reconsider f as Real_Sequence by A18, RELSET_1: 4;

        for n holds (f . n) < (f . (n + 1)) by A17;

        then

        reconsider f as increasing sequence of NAT by SEQM_3:def 6;

        consider Nseq such that

         A19: seq1 = (seq * Nseq) by VALUED_0:def 17;

        reconsider Nseq1 = (Nseq * f) as increasing sequence of NAT ;

        take Nseq1;

        now

          let n;

          

           A20: n in NAT & (n + 1) in NAT by ORDINAL1:def 12;

          (seq1 . (f . (n + 1))) <= (seq1 . (f . n)) by A17;

          then ((seq1 * f) . (n + 1)) <= (seq1 . (f . n)) by FUNCT_2: 15;

          then (((seq * Nseq) * f) . (n + 1)) <= ((seq1 * f) . n) by A19, FUNCT_2: 15, A20;

          then ((seq * Nseq1) . (n + 1)) <= (((seq * Nseq) * f) . n) by A19, RELAT_1: 36;

          hence ((seq * Nseq1) . (n + 1)) <= ((seq * Nseq1) . n) by RELAT_1: 36;

        end;

        then (seq * Nseq1) is non-increasing;

        hence (seq * Nseq1) is monotone by SEQM_3:def 5;

      end;

      now

        defpred P[ set, set, set] means for k,l be Element of NAT st k = $2 & l = $3 holds l in XN & k < l & for m st m in XN & k < m holds l <= m;

        assume

         A21: for l holds ex n st n in XN & not n <= l;

        then

        consider n1 such that

         A22: n1 in XN and not n1 <= 0 ;

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

        

         A23: for n be Nat holds for x be Element of NAT holds ex y be Element of NAT st P[n, x, y]

        proof

          let n be Nat, x be Element of NAT ;

          defpred X[ Nat] means $1 in XN & x < $1;

          ex n be Nat st X[n] by A21;

          then ex n be Element of NAT st X[n];

          then

           A24: ex n be Nat st X[n];

          ex l be Nat st X[l] & for m be Nat st X[m] holds l <= m from NAT_1:sch 5( A24);

          then

          consider l be Nat such that

           A25: l in XN & x < l & for m be Nat st m in XN & x < m holds l <= m;

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

          take l;

          thus thesis by A25;

        end;

        consider f be sequence of NAT such that

         A26: (f . 0 ) = O9 and

         A27: for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A23);

        

         A28: ( dom f) = NAT by FUNCT_2:def 1;

        ( rng f) c= REAL ;

        then

        reconsider f as Real_Sequence by A28, RELSET_1: 4;

        

         A29: for n holds n is Element of NAT & (f . n) is Element of NAT by ORDINAL1:def 12;

         A30:

        now

          let n;

          (f . n) is Element of NAT & (f . (n + 1)) is Element of NAT by A29;

          hence (f . n) < (f . (n + 1)) by A27;

        end;

         A31:

        now

          defpred X[ Nat] means (f . $1) in XN;

          let n;

           A32:

          now

            let k such that X[k];

            (f . k) is Element of NAT & (f . (k + 1)) is Element of NAT by A29;

            hence X[(k + 1)] by A27;

          end;

          

           A33: X[ 0 ] by A22, A26;

          thus for n holds X[n] from NAT_1:sch 2( A33, A32);

        end;

        reconsider f as increasing sequence of NAT by A30, SEQM_3:def 6;

        take Nseq = f;

        now

          let n;

          

           A34: n in NAT by ORDINAL1:def 12;

          (Nseq . n) in XN & (Nseq . n) < (Nseq . (n + 1)) by A31, A30;

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

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

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

        end;

        then (seq * Nseq) is increasing;

        hence (seq * Nseq) is monotone by SEQM_3:def 5;

      end;

      hence thesis by A2;

    end;

    ::$Notion-Name

    theorem :: SEQ_4:40

    

     Th40: seq is bounded implies ex seq1 st seq1 is subsequence of seq & seq1 is convergent

    proof

      assume

       A1: seq is bounded;

      consider Nseq such that

       A2: (seq * Nseq) is monotone by Th39;

      take seq1 = (seq * Nseq);

      thus seq1 is subsequence of seq;

      thus thesis by A1, A2, Th36, SEQM_3: 29;

    end;

    ::$Notion-Name

    theorem :: SEQ_4:41

    seq is convergent iff for s st 0 < s holds ex n st for m st n <= m holds |.((seq . m) - (seq . n)).| < s

    proof

      thus seq is convergent implies for s st 0 < s holds ex n st for m st n <= m holds |.((seq . m) - (seq . n)).| < s

      proof

        assume seq is convergent;

        then

        consider g1 such that

         A1: for s st 0 < s holds ex n st for m st n <= m holds |.((seq . m) - g1).| < s;

        let s;

        assume 0 < s;

        then

        consider n1 such that

         A2: for m st n1 <= m holds |.((seq . m) - g1).| < (s / 2) by A1;

        take n = n1;

        let m;

        assume n <= m;

        then

         A3: |.((seq . m) - g1).| < (s / 2) by A2;

        

         A4: |.(((seq . m) - g1) + (g1 - (seq . n))).| <= ( |.((seq . m) - g1).| + |.(g1 - (seq . n)).|) by COMPLEX1: 56;

         |.((seq . n) - g1).| < (s / 2) by A2;

        then |.( - (g1 - (seq . n))).| < (s / 2);

        then |.(g1 - (seq . n)).| < (s / 2) by COMPLEX1: 52;

        then ( |.((seq . m) - g1).| + |.(g1 - (seq . n)).|) < ((s / 2) + (s / 2)) by A3, XREAL_1: 8;

        hence thesis by A4, XXREAL_0: 2;

      end;

      assume

       A5: for s st 0 < s holds ex n st for m st n <= m holds |.((seq . m) - (seq . n)).| < s;

      then

      consider n1 such that

       A6: for m st n1 <= m holds |.((seq . m) - (seq . n1)).| < 1;

      consider r1 such that

       A7: 0 < r1 and

       A8: for m st m <= n1 holds |.(seq . m).| < r1 by SEQ_2: 4;

      now

        take r = ((r1 + |.(seq . n1).|) + 1);

        ( 0 qua Nat + 0 qua Nat) < (r1 + |.(seq . n1).|) by A7, COMPLEX1: 46, XREAL_1: 8;

        hence 0 < r;

        let m;

         A9:

        now

          assume n1 <= m;

          then

           A10: |.((seq . m) - (seq . n1)).| < 1 by A6;

          ( |.(seq . m).| - |.(seq . n1).|) <= |.((seq . m) - (seq . n1)).| by COMPLEX1: 59;

          then ( |.(seq . m).| - |.(seq . n1).|) < 1 by A10, XXREAL_0: 2;

          then (( |.(seq . m).| - |.(seq . n1).|) + |.(seq . n1).|) < (1 + |.(seq . n1).|) by XREAL_1: 6;

          then ( 0 qua Nat + |.(seq . m).|) < (r1 + ( |.(seq . n1).| + 1)) by A7, XREAL_1: 8;

          hence |.(seq . m).| < r;

        end;

        now

          assume m <= n1;

          then |.(seq . m).| < r1 by A8;

          then ( |.(seq . m).| + 0 qua Nat) < (r1 + |.(seq . n1).|) by COMPLEX1: 46, XREAL_1: 8;

          hence |.(seq . m).| < r by XREAL_1: 8;

        end;

        hence |.(seq . m).| < r by A9;

      end;

      then seq is bounded by SEQ_2: 3;

      then

      consider seq1 such that

       A11: seq1 is subsequence of seq and

       A12: seq1 is convergent by Th40;

      consider g1 such that

       A13: for s st 0 < s holds ex n st for m st n <= m holds |.((seq1 . m) - g1).| < s by A12;

      take g1;

      let s;

      assume

       A14: 0 < s;

      then

      consider n1 such that

       A15: for m st n1 <= m holds |.((seq1 . m) - g1).| < (s / 3) by A13;

      consider n2 such that

       A16: for m st n2 <= m holds |.((seq . m) - (seq . n2)).| < (s / 3) by A5, A14;

      take n = (n1 + n2);

      let m such that

       A17: n <= m;

      consider Nseq such that

       A18: seq1 = (seq * Nseq) by A11, VALUED_0:def 17;

      

       A19: m in NAT by ORDINAL1:def 12;

      n1 <= n by NAT_1: 12;

      then n1 <= m by A17, XXREAL_0: 2;

      then |.(((seq * Nseq) . m) - g1).| < (s / 3) by A18, A15;

      then

       A20: |.((seq . (Nseq . m)) - g1).| < (s / 3) by FUNCT_2: 15, A19;

      n2 <= n by NAT_1: 12;

      then

       A21: n2 <= m by A17, XXREAL_0: 2;

      m <= (Nseq . m) by SEQM_3: 14;

      then n2 <= (Nseq . m) by A21, XXREAL_0: 2;

      then |.((seq . (Nseq . m)) - (seq . n2)).| < (s / 3) by A16;

      then |.( - ((seq . n2) - (seq . (Nseq . m)))).| < (s / 3);

      then

       A22: |.((seq . n2) - (seq . (Nseq . m))).| < (s / 3) by COMPLEX1: 52;

       |.((seq . m) - (seq . n2)).| < (s / 3) by A16, A21;

      then

       A23: ( |.((seq . m) - (seq . n2)).| + |.((seq . n2) - (seq . (Nseq . m))).|) < ((s / 3) + (s / 3)) by A22, XREAL_1: 8;

       |.(((seq . m) - (seq . n2)) + ((seq . n2) - (seq . (Nseq . m)))).| <= ( |.((seq . m) - (seq . n2)).| + |.((seq . n2) - (seq . (Nseq . m))).|) by COMPLEX1: 56;

      then |.((seq . m) - (seq . (Nseq . m))).| < ((s / 3) + (s / 3)) by A23, XXREAL_0: 2;

      then

       A24: ( |.((seq . m) - (seq . (Nseq . m))).| + |.((seq . (Nseq . m)) - g1).|) < (((s / 3) + (s / 3)) + (s / 3)) by A20, XREAL_1: 8;

       |.(((seq . m) - (seq . (Nseq . m))) + ((seq . (Nseq . m)) - g1)).| <= ( |.((seq . m) - (seq . (Nseq . m))).| + |.((seq . (Nseq . m)) - g1).|) by COMPLEX1: 56;

      hence thesis by A24, XXREAL_0: 2;

    end;

    theorem :: SEQ_4:42

    seq is constant & seq1 is convergent implies ( lim (seq + seq1)) = ((seq . 0 ) + ( lim seq1)) & ( lim (seq - seq1)) = ((seq . 0 ) - ( lim seq1)) & ( lim (seq1 - seq)) = (( lim seq1) - (seq . 0 )) & ( lim (seq (#) seq1)) = ((seq . 0 ) * ( lim seq1))

    proof

      assume that

       A1: seq is constant and

       A2: seq1 is convergent;

      

      thus ( lim (seq + seq1)) = (( lim seq) + ( lim seq1)) by A1, A2, SEQ_2: 6

      .= ((seq . 0 ) + ( lim seq1)) by A1, Th25;

      

      thus ( lim (seq - seq1)) = (( lim seq) - ( lim seq1)) by A1, A2, SEQ_2: 12

      .= ((seq . 0 ) - ( lim seq1)) by A1, Th25;

      

      thus ( lim (seq1 - seq)) = (( lim seq1) - ( lim seq)) by A1, A2, SEQ_2: 12

      .= (( lim seq1) - (seq . 0 )) by A1, Th25;

      

      thus ( lim (seq (#) seq1)) = (( lim seq) * ( lim seq1)) by A1, A2, SEQ_2: 15

      .= ((seq . 0 ) * ( lim seq1)) by A1, Th25;

    end;

    begin

    theorem :: SEQ_4:43

    

     Th43: for X be non empty real-membered set holds for t st for s st s in X holds s >= t holds ( lower_bound X) >= t

    proof

      let X be non empty real-membered set;

      set r = ( lower_bound X);

      let t;

      assume

       A1: for s st s in X holds s >= t;

      set s = (t - r);

      assume r < t;

      then

       A2: s > 0 by XREAL_1: 50;

      X is bounded_below

      proof

        take t;

        let s be ExtReal;

        thus thesis by A1;

      end;

      then ex t9 be Real st t9 in X & t9 < (r + s) by A2, Def2;

      hence contradiction by A1;

    end;

    theorem :: SEQ_4:44

    

     Th44: for X be non empty real-membered set st (for s st s in X holds s >= r) & for t st for s st s in X holds s >= t holds r >= t holds r = ( lower_bound X) by Lm1;

    theorem :: SEQ_4:45

    

     Th45: for X be non empty real-membered set, r holds for t st for s st s in X holds s <= t holds ( upper_bound X) <= t

    proof

      let X be non empty real-membered set, r;

      set r = ( upper_bound X);

      let t;

      assume

       A1: for s st s in X holds s <= t;

      set s = (r - t);

      assume r > t;

      then

       A2: s > 0 by XREAL_1: 50;

      X is bounded_above

      proof

        take t;

        let s be ExtReal;

        thus thesis by A1;

      end;

      then ex t9 be Real st t9 in X & (r - s) < t9 by A2, Def1;

      hence contradiction by A1;

    end;

    theorem :: SEQ_4:46

    

     Th46: for X be non empty real-membered set, r st (for s st s in X holds s <= r) & for t st for s st s in X holds s <= t holds r <= t holds r = ( upper_bound X) by Lm2;

    theorem :: SEQ_4:47

    for X be non empty real-membered set, Y be real-membered set st X c= Y & Y is bounded_below holds ( lower_bound Y) <= ( lower_bound X)

    proof

      let X be non empty real-membered set, Y be real-membered set;

      assume X c= Y & Y is bounded_below;

      then t in X implies t >= ( lower_bound Y) by Def2;

      hence thesis by Th43;

    end;

    theorem :: SEQ_4:48

    for X be non empty real-membered set, Y be real-membered set st X c= Y & Y is bounded_above holds ( upper_bound X) <= ( upper_bound Y)

    proof

      let X be non empty real-membered set, Y be real-membered set;

      assume X c= Y & Y is bounded_above;

      then t in X implies t <= ( upper_bound Y) by Def1;

      hence thesis by Th45;

    end;

    definition

      let A be non empty natural-membered set;

      :: original: min

      redefine

      func min A -> Element of NAT ;

      coherence by ORDINAL1:def 12;

    end

    begin

    reserve k,n for Nat,

r,r9,r1,r2 for Real,

c,c9,c1,c2,c3 for Element of COMPLEX ;

    theorem :: SEQ_4:49

     0c is_a_unity_wrt addcomplex by BINOP_2: 1, SETWISEO: 14;

    theorem :: SEQ_4:50

    

     Th50: compcomplex is_an_inverseOp_wrt addcomplex

    proof

      let c;

      

      thus ( addcomplex . (c,( compcomplex . c))) = (c + ( compcomplex . c)) by BINOP_2:def 3

      .= (c + ( - c)) by BINOP_2:def 1

      .= ( the_unity_wrt addcomplex ) by BINOP_2: 1;

      

      thus ( addcomplex . (( compcomplex . c),c)) = (( compcomplex . c) + c) by BINOP_2:def 3

      .= (( - c) + c) by BINOP_2:def 1

      .= ( the_unity_wrt addcomplex ) by BINOP_2: 1;

    end;

    theorem :: SEQ_4:51

    

     Th51: addcomplex is having_an_inverseOp by Th50;

    theorem :: SEQ_4:52

    

     Th52: ( the_inverseOp_wrt addcomplex ) = compcomplex by Th50, Th51, FINSEQOP:def 3;

    definition

      :: original: diffcomplex

      redefine

      :: SEQ_4:def3

      func diffcomplex equals ( addcomplex * (( id COMPLEX ), compcomplex ));

      compatibility

      proof

        let b be BinOp of COMPLEX ;

        now

          let c1, c2;

          

          thus ( diffcomplex . (c1,c2)) = (c1 - c2) by BINOP_2:def 4

          .= (c1 + ( - c2))

          .= ( addcomplex . (c1,( - c2))) by BINOP_2:def 3

          .= ( addcomplex . (c1,( compcomplex . c2))) by BINOP_2:def 1

          .= (( addcomplex * (( id COMPLEX ), compcomplex )) . (c1,c2)) by FINSEQOP: 82;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    theorem :: SEQ_4:53

     1r is_a_unity_wrt multcomplex by BINOP_2: 6, SETWISEO: 14;

    theorem :: SEQ_4:54

    

     Th54: multcomplex is_distributive_wrt addcomplex

    proof

      now

        let c1, c2, c3;

        

        thus ( multcomplex . (c1,( addcomplex . (c2,c3)))) = ( multcomplex . (c1,(c2 + c3))) by BINOP_2:def 3

        .= (c1 * (c2 + c3)) by BINOP_2:def 5

        .= ((c1 * c2) + (c1 * c3))

        .= ( addcomplex . ((c1 * c2),(c1 * c3))) by BINOP_2:def 3

        .= ( addcomplex . (( multcomplex . (c1,c2)),(c1 * c3))) by BINOP_2:def 5

        .= ( addcomplex . (( multcomplex . (c1,c2)),( multcomplex . (c1,c3)))) by BINOP_2:def 5;

        

        thus ( multcomplex . (( addcomplex . (c1,c2)),c3)) = ( multcomplex . ((c1 + c2),c3)) by BINOP_2:def 3

        .= ((c1 + c2) * c3) by BINOP_2:def 5

        .= ((c1 * c3) + (c2 * c3))

        .= ( addcomplex . ((c1 * c3),(c2 * c3))) by BINOP_2:def 3

        .= ( addcomplex . (( multcomplex . (c1,c3)),(c2 * c3))) by BINOP_2:def 5

        .= ( addcomplex . (( multcomplex . (c1,c3)),( multcomplex . (c2,c3)))) by BINOP_2:def 5;

      end;

      hence thesis by BINOP_1: 11;

    end;

    definition

      let c be Complex;

      :: SEQ_4:def4

      func c multcomplex -> UnOp of COMPLEX equals ( multcomplex [;] (c,( id COMPLEX )));

      coherence

      proof

        reconsider c9 = c as Element of COMPLEX by XCMPLX_0:def 2;

        ( multcomplex [;] (c9,( id COMPLEX ))) is UnOp of COMPLEX ;

        hence thesis;

      end;

    end

    

     Lm3: (( multcomplex [;] (c,( id COMPLEX ))) . c9) = (c * c9)

    proof

      

      thus (( multcomplex [;] (c,( id COMPLEX ))) . c9) = ( multcomplex . (c,(( id COMPLEX ) . c9))) by FUNCOP_1: 53

      .= ( multcomplex . (c,c9))

      .= (c * c9) by BINOP_2:def 5;

    end;

    theorem :: SEQ_4:55

    ((c multcomplex ) . c9) = (c * c9) by Lm3;

    theorem :: SEQ_4:56

    (c multcomplex ) is_distributive_wrt addcomplex by Th54, FINSEQOP: 54;

    definition

      :: SEQ_4:def5

      func abscomplex -> Function of COMPLEX , REAL means

      : Def5: for c holds (it . c) = |.c.|;

      existence

      proof

        deffunc F( Element of COMPLEX ) = ( In ( |.$1.|, REAL ));

        consider F be Function of COMPLEX , REAL such that

         A1: for c holds (F . c) = F(c) from FUNCT_2:sch 4;

        take F;

        let c;

        

        thus (F . c) = F(c) by A1

        .= |.c.|;

      end;

      uniqueness from BINOP_2:sch 1;

    end

    reserve z,z1,z2 for FinSequence of COMPLEX ;

    definition

      let z1, z2;

      :: original: +

      redefine

      :: SEQ_4:def6

      func z1 + z2 -> FinSequence of COMPLEX equals ( addcomplex .: (z1,z2));

      coherence

      proof

        thus ( rng (z1 + z2)) c= COMPLEX ;

      end;

      compatibility

      proof

        set g = ( addcomplex .: (z1,z2));

        ( dom addcomplex ) = [: COMPLEX , COMPLEX :] by FUNCT_2:def 1;

        then [:( rng z1), ( rng z2):] c= ( dom addcomplex ) by ZFMISC_1: 96;

        then

         A1: ( dom (z1 + z2)) = (( dom z1) /\ ( dom z2)) & ( dom g) = (( dom z1) /\ ( dom z2)) by FUNCOP_1: 69, VALUED_1:def 1;

        now

          let x be object;

          assume

           A2: x in ( dom (z1 + z2));

          

          hence ((z1 + z2) . x) = ((z1 . x) + (z2 . x)) by VALUED_1:def 1

          .= ( addcomplex . ((z1 . x),(z2 . x))) by BINOP_2:def 3

          .= (g . x) by A1, A2, FUNCOP_1: 22;

        end;

        hence thesis by A1, FUNCT_1: 2;

      end;

      :: original: -

      redefine

      :: SEQ_4:def7

      func z1 - z2 -> FinSequence of COMPLEX equals ( diffcomplex .: (z1,z2));

      coherence

      proof

        thus ( rng (z1 - z2)) c= COMPLEX ;

      end;

      compatibility

      proof

        set g = ( diffcomplex .: (z1,z2));

        ( dom diffcomplex ) = [: COMPLEX , COMPLEX :] by FUNCT_2:def 1;

        then [:( rng z1), ( rng z2):] c= ( dom diffcomplex ) by ZFMISC_1: 96;

        then

         A3: ( dom g) = (( dom z1) /\ ( dom z2)) by FUNCOP_1: 69;

        

         A4: ( dom (z1 - z2)) = (( dom z1) /\ ( dom z2)) by VALUED_1: 12;

        now

          let x be object;

          assume

           A5: x in ( dom (z1 - z2));

          

          hence ((z1 - z2) . x) = ((z1 . x) - (z2 . x)) by VALUED_1: 13

          .= ( diffcomplex . ((z1 . x),(z2 . x))) by BINOP_2:def 4

          .= (g . x) by A4, A3, A5, FUNCOP_1: 22;

        end;

        hence thesis by A3, FUNCT_1: 2, VALUED_1: 12;

      end;

    end

    definition

      let z;

      :: original: -

      redefine

      :: SEQ_4:def8

      func - z -> FinSequence of COMPLEX equals ( compcomplex * z);

      coherence

      proof

        thus ( rng ( - z)) c= COMPLEX ;

      end;

      compatibility

      proof

        set g = ( compcomplex * z);

        ( dom compcomplex ) = COMPLEX by FUNCT_2:def 1;

        then ( rng z) c= ( dom compcomplex );

        then

         A1: ( dom g) = ( dom z) by RELAT_1: 27;

        

         A2: ( dom ( - z)) = ( dom z) by VALUED_1: 8;

        now

          let x be object;

          assume

           A3: x in ( dom ( - z));

          

          thus (( - z) . x) = ( - (z . x)) by VALUED_1: 8

          .= ( compcomplex . (z . x)) by BINOP_2:def 1

          .= (g . x) by A2, A1, A3, FUNCT_1: 12;

        end;

        hence thesis by A1, FUNCT_1: 2, VALUED_1: 8;

      end;

    end

    notation

      let z;

      let c be Complex;

      synonym c * z for c (#) z;

    end

    definition

      let z;

      let c be Complex;

      :: original: *

      redefine

      :: SEQ_4:def9

      func c * z -> FinSequence of COMPLEX equals ((c multcomplex ) * z);

      coherence

      proof

        thus ( rng (c (#) z)) c= COMPLEX ;

      end;

      compatibility

      proof

        set g = ((c multcomplex ) * z);

        ( dom (c multcomplex )) = COMPLEX by FUNCT_2:def 1;

        then ( rng z) c= ( dom (c multcomplex ));

        then

         A1: ( dom (c (#) z)) = ( dom z) & ( dom g) = ( dom z) by RELAT_1: 27, VALUED_1:def 5;

        now

          let x be object;

          assume

           A2: x in ( dom (c (#) z));

          

           A3: c is Element of COMPLEX & (z . x) is Element of COMPLEX by XCMPLX_0:def 2;

          

          thus ((c (#) z) . x) = (c * (z . x)) by VALUED_1: 6

          .= ((c multcomplex ) . (z . x)) by A3, Lm3

          .= (g . x) by A1, A2, FUNCT_1: 12;

        end;

        hence thesis by A1, FUNCT_1: 2;

      end;

    end

    definition

      let z;

      :: original: abs

      redefine

      :: SEQ_4:def10

      func abs z -> FinSequence of REAL equals ( abscomplex * z);

      coherence

      proof

        thus ( rng ( abs z)) c= REAL ;

      end;

      compatibility

      proof

        set g = ( abscomplex * z);

        ( dom abscomplex ) = COMPLEX by FUNCT_2:def 1;

        then ( rng z) c= ( dom abscomplex );

        then

         A1: ( dom ( abs z)) = ( dom z) & ( dom g) = ( dom z) by RELAT_1: 27, VALUED_1:def 11;

        now

          let x be object;

          assume

           A2: x in ( dom ( abs z));

          

           A3: (z . x) is Element of COMPLEX by XCMPLX_0:def 2;

          

          thus (( abs z) . x) = |.(z . x).| by VALUED_1: 18

          .= ( abscomplex . (z . x)) by A3, Def5

          .= (g . x) by A1, A2, FUNCT_1: 12;

        end;

        hence thesis by A1, FUNCT_1: 2;

      end;

    end

    definition

      let n;

      :: SEQ_4:def11

      func COMPLEX n -> FinSequenceSet of COMPLEX equals (n -tuples_on COMPLEX );

      correctness ;

    end

    registration

      let n;

      cluster ( COMPLEX n) -> non empty;

      coherence ;

    end

    reserve x,z,z1,z2,z3 for Element of ( COMPLEX n),

A,B for Subset of ( COMPLEX n);

    

     Lm4: ( dom z) = ( Seg n)

    proof

      ( len z) = n by CARD_1:def 7;

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: SEQ_4:57

    

     Th57: k in ( Seg n) implies (z . k) in COMPLEX

    proof

      ( len z) = n by CARD_1:def 7;

      then ( Seg n) = ( dom z) by FINSEQ_1:def 3;

      hence thesis by FINSEQ_2: 11;

    end;

    definition

      let n, z1, z2;

      :: original: +

      redefine

      func z1 + z2 -> Element of ( COMPLEX n) ;

      coherence by FINSEQ_2: 120;

    end

    theorem :: SEQ_4:58

    

     Th58: k in ( Seg n) & c1 = (z1 . k) & c2 = (z2 . k) implies ((z1 + z2) . k) = (c1 + c2)

    proof

      assume that

       A1: k in ( Seg n) and

       A2: c1 = (z1 . k) & c2 = (z2 . k);

      k in ( dom (z1 + z2)) by A1, Lm4;

      

      hence ((z1 + z2) . k) = ( addcomplex . (c1,c2)) by A2, FUNCOP_1: 22

      .= (c1 + c2) by BINOP_2:def 3;

    end;

    definition

      let n;

      :: SEQ_4:def12

      func 0c n -> FinSequence of COMPLEX equals (n |-> 0c );

      correctness ;

    end

    definition

      let n;

      :: original: 0c

      redefine

      func 0c n -> Element of ( COMPLEX n) ;

      coherence ;

    end

    theorem :: SEQ_4:59

    (z + ( 0c n)) = z & z = (( 0c n) + z) by BINOP_2: 1, FINSEQOP: 56;

    definition

      let n, z;

      :: original: -

      redefine

      func - z -> Element of ( COMPLEX n) ;

      coherence by FINSEQ_2: 113;

    end

    theorem :: SEQ_4:60

    

     Th60: k in ( Seg n) & c = (z . k) implies (( - z) . k) = ( - c)

    proof

      assume that

       A1: k in ( Seg n) and

       A2: c = (z . k);

      k in ( dom ( - z)) by A1, Lm4;

      

      hence (( - z) . k) = ( compcomplex . c) by A2, FUNCT_1: 12

      .= ( - c) by BINOP_2:def 1;

    end;

    

     Lm5: ( - ( 0c n)) = ( 0c n)

    proof

      

      thus ( - ( 0c n)) = (n |-> ( compcomplex . 0c )) by FINSEQOP: 16

      .= (n |-> ( - 0c qua Complex)) by BINOP_2:def 1

      .= ( 0c n);

    end;

    theorem :: SEQ_4:61

    (z + ( - z)) = ( 0c n) & (( - z) + z) = ( 0c n) by Th51, Th52, BINOP_2: 1, FINSEQOP: 73;

    theorem :: SEQ_4:62

    (z1 + z2) = ( 0c n) implies z1 = ( - z2) & z2 = ( - z1) by Th51, Th52, BINOP_2: 1, FINSEQOP: 74;

    ::$Canceled

    theorem :: SEQ_4:64

    ( - z1) = ( - z2) implies z1 = z2

    proof

      assume ( - z1) = ( - z2);

      

      hence z1 = ( - ( - z2))

      .= z2;

    end;

    

     Lm6: (z1 + z) = (z2 + z) implies z1 = z2

    proof

      assume (z1 + z) = (z2 + z);

      then (z1 + (z + ( - z))) = ((z2 + z) + ( - z)) by FINSEQOP: 28;

      then

       A1: (z1 + (z + ( - z))) = (z2 + (z + ( - z))) by FINSEQOP: 28;

      (z + ( - z)) = ( 0c n) by Th51, Th52, BINOP_2: 1, FINSEQOP: 73;

      then z1 = (z2 + ( 0c n)) by A1, BINOP_2: 1, FINSEQOP: 56;

      hence thesis by BINOP_2: 1, FINSEQOP: 56;

    end;

    theorem :: SEQ_4:65

    (z1 + z) = (z2 + z) or (z1 + z) = (z + z2) implies z1 = z2 by Lm6;

    theorem :: SEQ_4:66

    

     Th65: ( - (z1 + z2)) = (( - z1) + ( - z2))

    proof

      ((z1 + z2) + (( - z1) + ( - z2))) = (((z2 + z1) + ( - z1)) + ( - z2)) by FINSEQOP: 28

      .= ((z2 + (z1 + ( - z1))) + ( - z2)) by FINSEQOP: 28

      .= ((z2 + ( 0c n)) + ( - z2)) by Th51, Th52, BINOP_2: 1, FINSEQOP: 73

      .= (z2 + ( - z2)) by BINOP_2: 1, FINSEQOP: 56

      .= ( 0c n) by Th51, Th52, BINOP_2: 1, FINSEQOP: 73;

      hence thesis by Th51, Th52, BINOP_2: 1, FINSEQOP: 74;

    end;

    definition

      let n, z1, z2;

      :: original: -

      redefine

      func z1 - z2 -> Element of ( COMPLEX n) ;

      coherence by FINSEQ_2: 120;

    end

    theorem :: SEQ_4:67

    k in ( Seg n) implies ((z1 - z2) . k) = ((z1 . k) - (z2 . k))

    proof

      assume that

       A1: k in ( Seg n);

      set c1 = (z1 . k), c2 = (z2 . k);

      k in ( dom (z1 - z2)) by A1, Lm4;

      

      hence ((z1 - z2) . k) = ( diffcomplex . (c1,c2)) by FUNCOP_1: 22

      .= (c1 - c2) by BINOP_2:def 4;

    end;

    theorem :: SEQ_4:68

    (z - ( 0c n)) = z

    proof

      

      thus (z - ( 0c n)) = (z + ( 0c n)) by Lm5

      .= z by BINOP_2: 1, FINSEQOP: 56;

    end;

    theorem :: SEQ_4:69

    (( 0c n) - z) = ( - z)

    proof

      

      thus (( 0c n) - z) = (( 0c n) + ( - z))

      .= ( - z) by BINOP_2: 1, FINSEQOP: 56;

    end;

    theorem :: SEQ_4:70

    (z1 - ( - z2)) = (z1 + z2);

    theorem :: SEQ_4:71

    

     Th70: ( - (z1 - z2)) = (z2 - z1)

    proof

      

      thus ( - (z1 - z2)) = (( - z1) + ( - ( - z2))) by Th65

      .= (z2 - z1);

    end;

    theorem :: SEQ_4:72

    

     Th71: ( - (z1 - z2)) = (( - z1) + z2)

    proof

      

      thus ( - (z1 - z2)) = (( - z1) + ( - ( - z2))) by Th65

      .= (( - z1) + z2);

    end;

    theorem :: SEQ_4:73

    

     Th72: (z - z) = ( 0c n)

    proof

      

      thus (z - z) = (z + ( - z))

      .= ( 0c n) by Th51, Th52, BINOP_2: 1, FINSEQOP: 73;

    end;

    theorem :: SEQ_4:74

    

     Th73: (z1 - z2) = ( 0c n) implies z1 = z2

    proof

      assume (z1 - z2) = ( 0c n);

      then (z1 + ( - z2)) = ( 0c n);

      then z1 = ( - ( - z2)) by Th51, Th52, BINOP_2: 1, FINSEQOP: 74;

      hence thesis;

    end;

    theorem :: SEQ_4:75

    

     Th74: ((z1 - z2) - z3) = (z1 - (z2 + z3))

    proof

      

      thus ((z1 - z2) - z3) = ((z1 + ( - z2)) + ( - z3))

      .= (z1 + (( - z2) + ( - z3))) by FINSEQOP: 28

      .= (z1 - (z2 + z3)) by Th65;

    end;

    theorem :: SEQ_4:76

    

     Th75: (z1 + (z2 - z3)) = ((z1 + z2) - z3)

    proof

      

      thus (z1 + (z2 - z3)) = (z1 + (z2 + ( - z3)))

      .= ((z1 + z2) + ( - z3)) by FINSEQOP: 28

      .= ((z1 + z2) - z3);

    end;

    theorem :: SEQ_4:77

    (z1 - (z2 - z3)) = ((z1 - z2) + z3)

    proof

      

      thus (z1 - (z2 - z3)) = (z1 + (( - z2) + z3)) by Th71

      .= ((z1 + ( - z2)) + z3) by FINSEQOP: 28

      .= ((z1 - z2) + z3);

    end;

    theorem :: SEQ_4:78

    ((z1 - z2) + z3) = ((z1 + z3) - z2) by Th75;

    theorem :: SEQ_4:79

    

     Th78: z1 = ((z1 + z) - z)

    proof

      

      thus z1 = (z1 + ( 0c n)) by BINOP_2: 1, FINSEQOP: 56

      .= (z1 + (z - z)) by Th72

      .= ((z1 + z) - z) by Th75;

    end;

    theorem :: SEQ_4:80

    

     Th79: (z1 + (z2 - z1)) = z2

    proof

      

      thus (z1 + (z2 - z1)) = ((z2 + ( - z1)) + z1)

      .= (z2 + (( - z1) + z1)) by FINSEQOP: 28

      .= (z2 + ( 0c n)) by Th51, Th52, BINOP_2: 1, FINSEQOP: 73

      .= z2 by BINOP_2: 1, FINSEQOP: 56;

    end;

    theorem :: SEQ_4:81

    

     Th80: z1 = ((z1 - z) + z)

    proof

      

      thus z1 = (z1 + ( 0c n)) by BINOP_2: 1, FINSEQOP: 56

      .= (z1 + (( - z) + z)) by Th51, Th52, BINOP_2: 1, FINSEQOP: 73

      .= ((z1 + ( - z)) + z) by FINSEQOP: 28

      .= ((z1 - z) + z);

    end;

    definition

      let n, z, c;

      :: original: *

      redefine

      func c * z -> Element of ( COMPLEX n) ;

      coherence by FINSEQ_2: 113;

    end

    theorem :: SEQ_4:82

    

     Th81: k in ( Seg n) & c9 = (z . k) implies ((c * z) . k) = (c * c9)

    proof

      assume that

       A1: k in ( Seg n) and

       A2: c9 = (z . k);

      k in ( dom (c * z)) by A1, Lm4;

      

      hence ((c * z) . k) = ((c multcomplex ) . c9) by A2, FUNCT_1: 12

      .= (c * c9) by Lm3;

    end;

    theorem :: SEQ_4:83

    (c1 * (c2 * z)) = ((c1 * c2) * z)

    proof

      

      thus ((c1 * c2) * z) = (( multcomplex [;] (( multcomplex . (c1,c2)),( id COMPLEX ))) * z) by BINOP_2:def 5

      .= (( multcomplex [;] (c1,( multcomplex [;] (c2,( id COMPLEX ))))) * z) by FUNCOP_1: 62

      .= ((( multcomplex [;] (c1,( id COMPLEX ))) * ( multcomplex [;] (c2,( id COMPLEX )))) * z) by FUNCOP_1: 55

      .= (c1 * (c2 * z)) by RELAT_1: 36;

    end;

    theorem :: SEQ_4:84

    ((c1 + c2) * z) = ((c1 * z) + (c2 * z))

    proof

      set c1M = ( multcomplex [;] (c1,( id COMPLEX ))), c2M = ( multcomplex [;] (c2,( id COMPLEX )));

      

      thus ((c1 + c2) * z) = (( multcomplex [;] (( addcomplex . (c1,c2)),( id COMPLEX ))) * z) by BINOP_2:def 3

      .= (( addcomplex .: (c1M,c2M)) * z) by Th54, FINSEQOP: 35

      .= ((c1 * z) + (c2 * z)) by FUNCOP_1: 25;

    end;

    theorem :: SEQ_4:85

    (c * (z1 + z2)) = ((c * z1) + (c * z2)) by Th54, FINSEQOP: 51, FINSEQOP: 54;

    theorem :: SEQ_4:86

    ( 1r * z) = z

    proof

      

       A1: ( rng z) c= COMPLEX ;

      

      thus ( 1r * z) = (( id COMPLEX ) * z) by BINOP_2: 6, FINSEQOP: 44

      .= z by A1, RELAT_1: 53;

    end;

    theorem :: SEQ_4:87

    ( 0c * z) = ( 0c n)

    proof

      

       A1: ( rng z) c= COMPLEX ;

      

      thus ( 0c * z) = ( multcomplex [;] ( 0c ,(( id COMPLEX ) * z))) by FUNCOP_1: 34

      .= ( multcomplex [;] ( 0c ,z)) by A1, RELAT_1: 53

      .= ( 0c n) by Th51, Th54, BINOP_2: 1, FINSEQOP: 76;

    end;

    theorem :: SEQ_4:88

    (( - 1r ) * z) = ( - z);

    definition

      let n, z;

      :: original: abs

      redefine

      func abs z -> Element of (n -tuples_on REAL ) ;

      correctness by FINSEQ_2: 113;

    end

    theorem :: SEQ_4:89

    

     Th88: k in ( Seg n) & c = (z . k) implies (( abs z) . k) = |.c.|

    proof

      assume that

       A1: k in ( Seg n) and

       A2: c = (z . k);

      ( len ( abs z)) = n by CARD_1:def 7;

      then k in ( dom ( abs z)) by A1, FINSEQ_1:def 3;

      

      hence (( abs z) . k) = ( abscomplex . c) by A2, FUNCT_1: 12

      .= |.c.| by Def5;

    end;

    theorem :: SEQ_4:90

    

     Th89: ( abs ( 0c n)) = (n |-> 0 )

    proof

      

      thus ( abs ( 0c n)) = (n |-> ( abscomplex . 0c )) by FINSEQOP: 16

      .= (n |-> 0 ) by Def5, COMPLEX1: 44;

    end;

    theorem :: SEQ_4:91

    

     Th90: ( abs ( - z)) = ( abs z)

    proof

      now

        let j be Nat;

        assume

         A1: j in ( Seg n);

        then

        reconsider c = (z . j), c9 = (( - z) . j) as Element of COMPLEX by Th57;

        

        thus (( abs ( - z)) . j) = |.c9.| by A1, Th88

        .= |.( - c).| by A1, Th60

        .= |.c.| by COMPLEX1: 52

        .= (( abs z) . j) by A1, Th88;

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    theorem :: SEQ_4:92

    

     Th91: ( abs (c * z)) = ( |.c.| * ( abs z))

    proof

      now

        let j be Nat;

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

        assume

         A1: j in ( Seg n);

        then

        reconsider c9 = (z . j), cc = ((c * z) . j) as Element of COMPLEX by Th57;

        reconsider ac = (( abs z) . w) as Real;

        

        thus (( abs (c * z)) . j) = |.cc.| by A1, Th88

        .= |.(c * c9).| by A1, Th81

        .= ( |.c.| * |.c9.|) by COMPLEX1: 65

        .= ( |.c.| * ac) by A1, Th88

        .= (( |.c.| * ( abs z)) . j) by RVSUM_1: 45;

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    definition

      let z be FinSequence of COMPLEX ;

      :: SEQ_4:def13

      func |.z.| -> Real equals ( sqrt ( Sum ( sqr ( abs z))));

      correctness ;

    end

    theorem :: SEQ_4:93

    

     Th92: |.( 0c n).| = 0

    proof

      

      thus |.( 0c n).| = ( sqrt ( Sum ( sqr (n |-> 0 qua Real)))) by Th89

      .= ( sqrt ( Sum (n |-> ( 0 qua Real ^2 )))) by RVSUM_1: 56

      .= ( sqrt (n * 0 qua Nat)) by RVSUM_1: 80

      .= 0 by SQUARE_1: 17;

    end;

    theorem :: SEQ_4:94

    

     Th93: |.z.| = 0 implies z = ( 0c n)

    proof

      assume

       A1: |.z.| = 0 ;

      now

        let j be Nat;

        assume

         A2: j in ( Seg n);

        then

        reconsider c = (z . j) as Element of COMPLEX by Th57;

         0 <= ( Sum ( sqr ( abs z))) by RVSUM_1: 86;

        then (( abs z) . j) = ((n |-> 0 ) . j) by A1, RVSUM_1: 91, SQUARE_1: 24;

        then |.c.| = ((n |-> 0 ) . j) by A2, Th88;

        then c = 0c by COMPLEX1: 45;

        hence (z . j) = ((n |-> 0c ) . j);

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    theorem :: SEQ_4:95

    

     Th94: 0 <= |.z.|

    proof

       0 <= ( Sum ( sqr ( abs z))) by RVSUM_1: 86;

      hence thesis by SQUARE_1:def 2;

    end;

    theorem :: SEQ_4:96

     |.( - z).| = |.z.| by Th90;

    theorem :: SEQ_4:97

     |.(c * z).| = ( |.c.| * |.z.|)

    proof

      

       A1: 0 <= ( |.c.| ^2 ) & 0 <= ( Sum ( sqr ( abs z))) by RVSUM_1: 86, XREAL_1: 63;

      

      thus |.(c * z).| = ( sqrt ( Sum ( sqr ( |.c.| * ( abs z))))) by Th91

      .= ( sqrt ( Sum (( |.c.| ^2 ) * ( sqr ( abs z))))) by RVSUM_1: 58

      .= ( sqrt (( |.c.| ^2 ) * ( Sum ( sqr ( abs z))))) by RVSUM_1: 87

      .= (( sqrt ( |.c.| ^2 )) * ( sqrt ( Sum ( sqr ( abs z))))) by A1, SQUARE_1: 29

      .= ( |.c.| * |.z.|) by COMPLEX1: 46, SQUARE_1: 22;

    end;

    theorem :: SEQ_4:98

    

     Th97: |.(z1 + z2).| <= ( |.z1.| + |.z2.|)

    proof

      

       A1: 0 <= ( Sum ( sqr ( abs (z1 + z2)))) by RVSUM_1: 86;

      

       A2: 0 <= ( Sum ( sqr ( abs z1))) by RVSUM_1: 86;

      then

       A3: 0 <= ( sqrt ( Sum ( sqr ( abs z1)))) by SQUARE_1:def 2;

      

       A4: for k be Nat holds k in ( Seg n) implies 0 <= (( mlt (( abs z1),( abs z2))) . k)

      proof

        let k be Nat;

        set r = (( mlt (( abs z1),( abs z2))) . k);

        assume

         A5: k in ( Seg n);

        then

        reconsider c1 = (z1 . k), c2 = (z2 . k) as Element of COMPLEX by Th57;

        (( abs z1) . k) = |.c1.| & (( abs z2) . k) = |.c2.| by A5, Th88;

        then

         A6: r = ( |.c1.| * |.c2.|) by RVSUM_1: 60;

         0 <= |.c1.| & 0 <= |.c2.| by COMPLEX1: 46;

        hence thesis by A6;

      end;

       0 <= (( Sum ( mlt (( abs z1),( abs z2)))) ^2 ) by XREAL_1: 63;

      then

       A7: ( sqrt (( Sum ( mlt (( abs z1),( abs z2)))) ^2 )) <= ( sqrt (( Sum ( sqr ( abs z1))) * ( Sum ( sqr ( abs z2))))) by RVSUM_1: 92, SQUARE_1: 26;

      ( len ( mlt (( abs z1),( abs z2)))) = n by CARD_1:def 7;

      then ( dom ( mlt (( abs z1),( abs z2)))) = ( Seg n) by FINSEQ_1:def 3;

      then ( Sum ( mlt (( abs z1),( abs z2)))) <= ( sqrt (( Sum ( sqr ( abs z1))) * ( Sum ( sqr ( abs z2))))) by A4, A7, RVSUM_1: 84, SQUARE_1: 22;

      then (2 * ( Sum ( mlt (( abs z1),( abs z2))))) <= (2 * ( sqrt (( Sum ( sqr ( abs z1))) * ( Sum ( sqr ( abs z2)))))) by XREAL_1: 64;

      then (( Sum ( sqr ( abs z1))) + (2 * ( Sum ( mlt (( abs z1),( abs z2)))))) <= (( Sum ( sqr ( abs z1))) + (2 * ( sqrt (( Sum ( sqr ( abs z1))) * ( Sum ( sqr ( abs z2))))))) by XREAL_1: 7;

      then

       A8: ((( Sum ( sqr ( abs z1))) + (2 * ( Sum ( mlt (( abs z1),( abs z2)))))) + ( Sum ( sqr ( abs z2)))) <= ((( Sum ( sqr ( abs z1))) + (2 * ( sqrt (( Sum ( sqr ( abs z1))) * ( Sum ( sqr ( abs z2))))))) + ( Sum ( sqr ( abs z2)))) by XREAL_1: 7;

      

       A9: for k be Nat holds k in ( Seg n) implies (( sqr ( abs (z1 + z2))) . k) <= (( sqr (( abs z1) + ( abs z2))) . k)

      proof

        let k be Nat;

        set r2 = (( sqr (( abs z1) + ( abs z2))) . k);

        ( len (( abs z1) + ( abs z2))) = n by CARD_1:def 7;

        then

         A10: ( dom (( abs z1) + ( abs z2))) = ( Seg n) by FINSEQ_1:def 3;

        assume

         A11: k in ( Seg n);

        then

        reconsider c12 = ((z1 + z2) . k) as Element of COMPLEX by Th57;

        reconsider abs912 = (( abs (z1 + z2)) . k) as Real;

         0 <= |.c12.| by COMPLEX1: 46;

        then

         A12: 0 <= abs912 by A11, Th88;

        reconsider abs1 = (( abs z1) . k), abs2 = (( abs z2) . k) as Real;

        reconsider c1 = (z1 . k), c2 = (z2 . k) as Element of COMPLEX by A11, Th57;

        reconsider abs12 = ((( abs z1) + ( abs z2)) . k) as Real;

         |.(c1 + c2).| <= ( |.c1.| + |.c2.|) by COMPLEX1: 56;

        then |.c12.| <= ( |.c1.| + |.c2.|) by A11, Th58;

        then |.c12.| <= ( |.c1.| + abs2) by A11, Th88;

        then |.c12.| <= (abs1 + abs2) by A11, Th88;

        then |.c12.| <= abs12 by A11, A10, VALUED_1:def 1;

        then abs912 <= abs12 by A11, Th88;

        then (abs912 ^2 ) <= (abs12 ^2 ) by A12, SQUARE_1: 15;

        then (abs912 ^2 ) <= r2 by VALUED_1: 11;

        hence thesis by VALUED_1: 11;

      end;

      

       A13: 0 <= ( Sum ( sqr ( abs z2))) by RVSUM_1: 86;

      then

       A14: 0 <= ( sqrt ( Sum ( sqr ( abs z2)))) by SQUARE_1:def 2;

      

       A15: ( Sum ( sqr ( abs z1))) = (( sqrt ( Sum ( sqr ( abs z1)))) ^2 ) by A2, SQUARE_1:def 2;

      

       A16: (( sqrt ( Sum ( sqr ( abs z2)))) ^2 ) = ( Sum ( sqr ( abs z2))) by A13, SQUARE_1:def 2;

      ( Sum ( sqr (( abs z1) + ( abs z2)))) = ( Sum ((( sqr ( abs z1)) + (2 * ( mlt (( abs z1),( abs z2))))) + ( sqr ( abs z2)))) by RVSUM_1: 68

      .= (( Sum (( sqr ( abs z1)) + (2 * ( mlt (( abs z1),( abs z2)))))) + ( Sum ( sqr ( abs z2)))) by RVSUM_1: 89

      .= ((( Sum ( sqr ( abs z1))) + ( Sum (2 * ( mlt (( abs z1),( abs z2)))))) + ( Sum ( sqr ( abs z2)))) by RVSUM_1: 89

      .= ((( Sum ( sqr ( abs z1))) + (2 * ( Sum ( mlt (( abs z1),( abs z2)))))) + ( Sum ( sqr ( abs z2)))) by RVSUM_1: 87;

      then ( Sum ( sqr ( abs (z1 + z2)))) <= ((( Sum ( sqr ( abs z1))) + (2 * ( Sum ( mlt (( abs z1),( abs z2)))))) + ( Sum ( sqr ( abs z2)))) by A9, RVSUM_1: 82;

      then ( Sum ( sqr ( abs (z1 + z2)))) <= ((( Sum ( sqr ( abs z1))) + (2 * ( sqrt (( Sum ( sqr ( abs z1))) * ( Sum ( sqr ( abs z2))))))) + ( Sum ( sqr ( abs z2)))) by A8, XXREAL_0: 2;

      then ( Sum ( sqr ( abs (z1 + z2)))) <= ((( Sum ( sqr ( abs z1))) + (2 * (( sqrt ( Sum ( sqr ( abs z1)))) * ( sqrt ( Sum ( sqr ( abs z2))))))) + ( Sum ( sqr ( abs z2)))) by A2, A13, SQUARE_1: 29;

      then ( sqrt ( Sum ( sqr ( abs (z1 + z2))))) <= ( sqrt ((( sqrt ( Sum ( sqr ( abs z1)))) + ( sqrt ( Sum ( sqr ( abs z2))))) ^2 )) by A15, A16, A1, SQUARE_1: 26;

      hence thesis by A3, A14, SQUARE_1: 22;

    end;

    theorem :: SEQ_4:99

    

     Th98: |.(z1 - z2).| <= ( |.z1.| + |.z2.|)

    proof

       |.(z1 - z2).| <= ( |.z1.| + |.( - z2).|) by Th97;

      hence thesis by Th90;

    end;

    theorem :: SEQ_4:100

    ( |.z1.| - |.z2.|) <= |.(z1 + z2).|

    proof

      z1 = ((z1 + z2) - z2) by Th78;

      then |.z1.| <= ( |.(z1 + z2).| + |.z2.|) by Th98;

      hence thesis by XREAL_1: 20;

    end;

    theorem :: SEQ_4:101

    ( |.z1.| - |.z2.|) <= |.(z1 - z2).|

    proof

      z1 = ((z1 - z2) + z2) by Th80;

      then |.z1.| <= ( |.(z1 - z2).| + |.z2.|) by Th97;

      hence thesis by XREAL_1: 20;

    end;

    theorem :: SEQ_4:102

    

     Th101: |.(z1 - z2).| = 0 iff z1 = z2

    proof

      thus |.(z1 - z2).| = 0 implies z1 = z2

      proof

        assume |.(z1 - z2).| = 0 ;

        then (z1 - z2) = ( 0c n) by Th93;

        hence thesis by Th73;

      end;

      assume z1 = z2;

      then (z1 - z2) = ( 0c n) by Th72;

      hence thesis by Th92;

    end;

    theorem :: SEQ_4:103

    z1 <> z2 implies 0 < |.(z1 - z2).|

    proof

      assume z1 <> z2;

      then 0 <> |.(z1 - z2).| by Th101;

      hence thesis by Th94;

    end;

    theorem :: SEQ_4:104

    

     Th103: |.(z1 - z2).| = |.(z2 - z1).|

    proof

      

      thus |.(z1 - z2).| = |.( - (z2 - z1)).| by Th70

      .= |.(z2 - z1).| by Th90;

    end;

    theorem :: SEQ_4:105

    

     Th104: |.(z1 - z2).| <= ( |.(z1 - z).| + |.(z - z2).|)

    proof

       |.(z1 - z2).| = |.(((z1 - z) + z) - z2).| by Th80

      .= |.((z1 - z) + (z - z2)).| by Th75;

      hence thesis by Th97;

    end;

    definition

      let n;

      let A be Subset of ( COMPLEX n);

      :: SEQ_4:def14

      attr A is open means for x st x in A holds ex r st 0 < r & for z st |.z.| < r holds (x + z) in A;

    end

    definition

      let n;

      let A be Subset of ( COMPLEX n);

      :: SEQ_4:def15

      attr A is closed means for x st for r st r > 0 holds ex z st |.z.| < r & (x + z) in A holds x in A;

    end

    theorem :: SEQ_4:106

    for A be Subset of ( COMPLEX n) st A = {} holds A is open;

    theorem :: SEQ_4:107

    for A be Subset of ( COMPLEX n) st A = ( COMPLEX n) holds A is open

    proof

      let A be Subset of ( COMPLEX n);

      assume

       A1: A = ( COMPLEX n);

      let x such that x in A;

      reconsider j = 1 as Element of REAL by NUMBERS: 19;

      take j;

      thus 0 < j;

      let z such that |.z.| < j;

      thus thesis by A1;

    end;

    theorem :: SEQ_4:108

    for AA be Subset-Family of ( COMPLEX n) st for A be Subset of ( COMPLEX n) st A in AA holds A is open holds for A be Subset of ( COMPLEX n) st A = ( union AA) holds A is open

    proof

      let AA be Subset-Family of ( COMPLEX n) such that

       A1: for A be Subset of ( COMPLEX n) st A in AA holds A is open;

      let A be Subset of ( COMPLEX n) such that

       A2: A = ( union AA);

      let x;

      assume x in A;

      then

      consider B be set such that

       A3: x in B and

       A4: B in AA by A2, TARSKI:def 4;

      reconsider B as Subset of ( COMPLEX n) by A4;

      B is open by A1, A4;

      then

      consider r such that

       A5: 0 < r and

       A6: for z st |.z.| < r holds (x + z) in B by A3;

      take r;

      thus 0 < r by A5;

      let z;

      assume |.z.| < r;

      then (x + z) in B by A6;

      hence thesis by A2, A4, TARSKI:def 4;

    end;

    theorem :: SEQ_4:109

    for A,B be Subset of ( COMPLEX n) st A is open & B is open holds for C be Subset of ( COMPLEX n) st C = (A /\ B) holds C is open

    proof

      let A,B be Subset of ( COMPLEX n) such that

       A1: A is open and

       A2: B is open;

      let C be Subset of ( COMPLEX n) such that

       A3: C = (A /\ B);

      let x;

      assume

       A4: x in C;

      then x in A by A3, XBOOLE_0:def 4;

      then

      consider r1 such that

       A5: 0 < r1 and

       A6: for z st |.z.| < r1 holds (x + z) in A by A1;

      x in B by A3, A4, XBOOLE_0:def 4;

      then

      consider r2 such that

       A7: 0 < r2 and

       A8: for z st |.z.| < r2 holds (x + z) in B by A2;

      take ( min (r1,r2));

      thus 0 < ( min (r1,r2)) by A5, A7, XXREAL_0: 15;

      let z;

      assume

       A9: |.z.| < ( min (r1,r2));

      ( min (r1,r2)) <= r2 by XXREAL_0: 17;

      then |.z.| < r2 by A9, XXREAL_0: 2;

      then

       A10: (x + z) in B by A8;

      ( min (r1,r2)) <= r1 by XXREAL_0: 17;

      then |.z.| < r1 by A9, XXREAL_0: 2;

      then (x + z) in A by A6;

      hence thesis by A3, A10, XBOOLE_0:def 4;

    end;

    definition

      let n, x, r;

      :: SEQ_4:def16

      func Ball (x,r) -> Subset of ( COMPLEX n) equals { z : |.(z - x).| < r };

      coherence

      proof

        defpred P[ FinSequence of COMPLEX ] means |.($1 - x).| < r;

        { z : P[z] } c= ( COMPLEX n) from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    theorem :: SEQ_4:110

    

     Th109: z in ( Ball (x,r)) iff |.(x - z).| < r

    proof

      

       A1: z in { z2 : |.(z2 - x).| < r } iff ex z1 st z = z1 & |.(z1 - x).| < r;

       |.(z - x).| = |.(x - z).| by Th103;

      hence thesis by A1;

    end;

    theorem :: SEQ_4:111

     0 < r implies x in ( Ball (x,r))

    proof

      assume

       A1: 0 < r;

       |.(x - x).| = 0 by Th101;

      hence thesis by A1;

    end;

    theorem :: SEQ_4:112

    ( Ball (z1,r1)) is open

    proof

      let x;

      assume x in ( Ball (z1,r1));

      then

       A1: |.(z1 - x).| < r1 by Th109;

      take r = (r1 - |.(z1 - x).|);

      thus 0 < r by A1, XREAL_1: 50;

      let z;

      assume |.z.| < r;

      then

       A2: ( |.z.| + |.(z1 - x).|) < (r + |.(z1 - x).|) by XREAL_1: 6;

      ((z1 - x) - z) = (z1 - (x + z)) by Th74;

      then |.(z1 - (x + z)).| <= ( |.z.| + |.(z1 - x).|) by Th98;

      then |.(z1 - (x + z)).| < (r + |.(z1 - x).|) by A2, XXREAL_0: 2;

      hence thesis by Th109;

    end;

    definition

      let n, x, A;

      :: SEQ_4:def17

      func dist (x,A) -> Real means

      : Def17: for X be Subset of REAL st X = { |.(x - z).| : z in A } holds it = ( lower_bound X);

      existence

      proof

        deffunc f( Element of ( COMPLEX n)) = ( In ( |.(x - $1).|, REAL ));

        deffunc g( Element of ( COMPLEX n)) = |.(x - $1).|;

        defpred P[ set] means $1 in A;

        reconsider X = { f(z) where z be Element of ( COMPLEX n) : P[z] } as Subset of REAL from DOMAIN_1:sch 8;

        

         A1: f(z) = g(z);

        

         A2: { f(z1) where z1 be Element of ( COMPLEX n) : P[z1] } = { g(z2) where z2 be Element of ( COMPLEX n) : P[z2] } from FRAENKEL:sch 5( A1);

        take L = ( lower_bound X);

        thus thesis by A2;

      end;

      uniqueness

      proof

        let r1,r2 be Real such that

         A3: for X be Subset of REAL st X = { |.(x - z).| : z in A } holds r1 = ( lower_bound X) and

         A4: for X be Subset of REAL st X = { |.(x - z).| : z in A } holds r2 = ( lower_bound X);

        deffunc f( Element of ( COMPLEX n)) = ( In ( |.(x - $1).|, REAL ));

        deffunc g( Element of ( COMPLEX n)) = |.(x - $1).|;

        defpred P[ set] means $1 in A;

        reconsider X = { f(z) where z be Element of ( COMPLEX n) : P[z] } as Subset of REAL from DOMAIN_1:sch 8;

        

         A1: f(z) = g(z);

        

         A2: { f(z1) where z1 be Element of ( COMPLEX n) : P[z1] } = { g(z2) where z2 be Element of ( COMPLEX n) : P[z2] } from FRAENKEL:sch 5( A1);

        r1 = ( lower_bound X) by A3, A2;

        hence thesis by A4, A2;

      end;

    end

    definition

      let n, A, r;

      :: SEQ_4:def18

      func Ball (A,r) -> Subset of ( COMPLEX n) equals { z : ( dist (z,A)) < r };

      coherence

      proof

        defpred P[ Element of ( COMPLEX n)] means ( dist ($1,A)) < r;

        { z : P[z] } c= ( COMPLEX n) from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    theorem :: SEQ_4:113

    

     Th112: for X be Subset of REAL , r st X <> {} & for r9 st r9 in X holds r <= r9 holds ( lower_bound X) >= r

    proof

      let X be Subset of REAL , r such that

       A1: X <> {} and

       A2: for r9 st r9 in X holds r <= r9;

      for r9 be ExtReal st r9 in X holds r <= r9 by A2;

      then r is LowerBound of X by XXREAL_2:def 2;

      then

       A3: X is bounded_below;

      now

        let r9 be Real;

        assume r9 > 0 ;

        then

        consider r1 be Real such that

         A4: r1 in X and

         A5: r1 < (( lower_bound X) + r9) by A1, A3, Def2;

        r <= r1 by A2, A4;

        hence (( lower_bound X) + r9) >= r by A5, XXREAL_0: 2;

      end;

      hence thesis by XREAL_1: 41;

    end;

    theorem :: SEQ_4:114

    

     Th113: A <> {} implies ( dist (x,A)) >= 0

    proof

      defpred P[ set] means $1 in A;

      deffunc f( Element of ( COMPLEX n)) = ( In ( |.(x - $1).|, REAL ));

      deffunc g( Element of ( COMPLEX n)) = |.(x - $1).|;

      reconsider X = { f(z) : P[z] } as Subset of REAL from DOMAIN_1:sch 8;

      

       A1: f(z) = g(z);

      

       A2: { f(z1) where z1 be Element of ( COMPLEX n) : P[z1] } = { g(z2) where z2 be Element of ( COMPLEX n) : P[z2] } from FRAENKEL:sch 5( A1);

      assume A <> {} ;

      then

      consider z1 such that

       A3: z1 in A by SUBSET_1: 4;

      

       A4: |.(x - z1).| in X by A3, A2;

       A5:

      now

        let r9;

        assume r9 in X;

        then ex z st r9 = f(z) & z in A;

        hence r9 >= 0 by Th94;

      end;

      ( dist (x,A)) = ( lower_bound X) by Def17, A2;

      hence thesis by A4, A5, Th112;

    end;

    theorem :: SEQ_4:115

    

     Th114: A <> {} implies ( dist ((x + z),A)) <= (( dist (x,A)) + |.z.|)

    proof

      defpred P[ set] means $1 in A;

      deffunc g( Element of ( COMPLEX n)) = ( In ( |.((x + z) - $1).|, REAL ));

      deffunc h( Element of ( COMPLEX n)) = |.((x + z) - $1).|;

      reconsider Y = { g(z1) : P[z1] } as Subset of REAL from DOMAIN_1:sch 8;

      deffunc f( Element of ( COMPLEX n)) = ( In ( |.(x - $1).|, REAL ));

      deffunc f1( Element of ( COMPLEX n)) = |.(x - $1).|;

      

       A1: for z1 be Element of ( COMPLEX n) holds h(z1) = g(z1);

      

       A2: { h(z1) : P[z1] } = { g(z2) where z2 be Element of ( COMPLEX n) : P[z2] } from FRAENKEL:sch 5( A1);

      

       A3: for z1 be Element of ( COMPLEX n) holds f(z1) = f1(z1);

      

       A4: { f(z1) : P[z1] } = { f1(z2) where z2 be Element of ( COMPLEX n) : P[z2] } from FRAENKEL:sch 5( A3);

      

       A5: Y is bounded_below

      proof

        take 0 ;

        let r be ExtReal;

        assume r in Y;

        then ex z1 st r = |.((x + z) - z1).| & z1 in A by A2;

        hence thesis by Th94;

      end;

      reconsider X = { f(z1) : P[z1] } as Subset of REAL from DOMAIN_1:sch 8;

      assume A <> {} ;

      then

      consider z2 such that

       A6: z2 in A by SUBSET_1: 4;

      

       A7: ( dist ((x + z),A)) = ( lower_bound Y) by Def17, A2;

       A8:

      now

        let r9;

        assume r9 in X;

        then

        consider z3 such that

         A9: r9 = |.(x - z3).| and

         A10: z3 in A by A4;

         |.((x + z) - z3).| = |.((x - z3) + z).| by Th75;

        then

         A11: |.((x + z) - z3).| <= (r9 + |.z.|) by A9, Th97;

         |.((x + z) - z3).| in Y by A10, A2;

        then |.((x + z) - z3).| >= ( dist ((x + z),A)) by A7, A5, Def2;

        then (r9 + |.z.|) >= ( dist ((x + z),A)) by A11, XXREAL_0: 2;

        hence r9 >= (( dist ((x + z),A)) - |.z.|) by XREAL_1: 20;

      end;

      

       A12: |.(x - z2).| in X by A6, A4;

      ( dist (x,A)) = ( lower_bound X) by Def17, A4;

      then (( dist ((x + z),A)) - |.z.|) <= ( dist (x,A)) by A12, A8, Th112;

      hence thesis by XREAL_1: 20;

    end;

    theorem :: SEQ_4:116

    

     Th115: x in A implies ( dist (x,A)) = 0

    proof

      defpred P[ set] means $1 in A;

      deffunc f( Element of ( COMPLEX n)) = ( In ( |.(x - $1).|, REAL ));

      deffunc g( Element of ( COMPLEX n)) = |.(x - $1).|;

      reconsider X = { f(z) : P[z] } as Subset of REAL from DOMAIN_1:sch 8;

      

       A1: f(z) = g(z);

      

       A2: { f(z1) where z1 be Element of ( COMPLEX n) : P[z1] } = { g(z2) where z2 be Element of ( COMPLEX n) : P[z2] } from FRAENKEL:sch 5( A1);

      assume

       A3: x in A;

      then

       A4: |.(x - x).| in X by A2;

       A5:

      now

        reconsider r = |.(x - x).| as Real;

        let r1 be Real such that

         A6: 0 < r1;

        take r;

        thus r in X by A3, A2;

        thus r < ( 0 qua Nat + r1) by A6, Th101;

      end;

       A7:

      now

        let r be Real;

        assume r in X;

        then ex z st r = |.(x - z).| & z in A by A2;

        hence 0 <= r by Th94;

      end;

      

       A8: X is bounded_below

      proof

        take 0 ;

        let x be ExtReal;

        thus thesis by A7;

      end;

      

      thus ( dist (x,A)) = ( lower_bound X) by Def17, A2

      .= 0 by A4, A7, A8, A5, Def2;

    end;

    theorem :: SEQ_4:117

     not x in A & A <> {} & A is closed implies ( dist (x,A)) > 0

    proof

      assume that

       A1: not x in A and

       A2: A <> {} and

       A3: for x st for r st r > 0 holds ex z st |.z.| < r & (x + z) in A holds x in A and

       A4: ( dist (x,A)) <= 0 ;

      

       A5: ( dist (x,A)) = 0 by A2, A4, Th113;

      now

        deffunc f( Element of ( COMPLEX n)) = ( In ( |.(x - $1).|, REAL ));

        deffunc g( Element of ( COMPLEX n)) = |.(x - $1).|;

        defpred P[ set] means $1 in A;

        

         A6: f(z) = g(z);

        

         A7: { f(z1) where z1 be Element of ( COMPLEX n) : P[z1] } = { g(z2) where z2 be Element of ( COMPLEX n) : P[z2] } from FRAENKEL:sch 5( A6);

        reconsider X = { f(z) : P[z] } as Subset of REAL from DOMAIN_1:sch 8;

        let r such that

         A8: r > 0 ;

        consider z such that

         A9: z in A by A2, SUBSET_1: 4;

        

         A10: X is bounded_below

        proof

          take 0 ;

          let r be ExtReal;

          assume r in X;

          then ex z st r = |.(x - z).| & z in A by A7;

          hence thesis by Th94;

        end;

        

         A11: |.(x - z).| in X by A9, A7;

        ( dist (x,A)) = ( lower_bound X) & ( 0 qua Nat + r) = r by Def17, A7;

        then

        consider r9 be Real such that

         A12: r9 in X and

         A13: r9 < r by A5, A8, A11, A10, Def2;

        consider z1 such that

         A14: r9 = |.(x - z1).| & z1 in A by A12, A7;

        take z = (z1 - x);

        thus |.z.| < r & (x + z) in A by A13, A14, Th79, Th103;

      end;

      hence contradiction by A1, A3;

    end;

    theorem :: SEQ_4:118

    A <> {} implies ( |.(z1 - x).| + ( dist (x,A))) >= ( dist (z1,A))

    proof

      (x + (z1 - x)) = z1 by Th79;

      hence thesis by Th114;

    end;

    theorem :: SEQ_4:119

    

     Th118: z in ( Ball (A,r)) iff ( dist (z,A)) < r

    proof

      z in { z2 : ( dist (z2,A)) < r } iff ex z1 st z = z1 & ( dist (z1,A)) < r;

      hence thesis;

    end;

    theorem :: SEQ_4:120

    

     Th119: 0 < r & x in A implies x in ( Ball (A,r))

    proof

      assume that

       A1: 0 < r and

       A2: x in A;

      ( dist (x,A)) = 0 by A2, Th115;

      hence thesis by A1;

    end;

    theorem :: SEQ_4:121

     0 < r implies A c= ( Ball (A,r)) by Th119;

    theorem :: SEQ_4:122

    A <> {} implies ( Ball (A,r1)) is open

    proof

      assume

       A1: A <> {} ;

      let x;

      assume x in ( Ball (A,r1));

      then

       A2: ( dist (x,A)) < r1 by Th118;

      take r = (r1 - ( dist (x,A)));

      thus 0 < r by A2, XREAL_1: 50;

      let z;

      assume |.z.| < r;

      then

       A3: ( |.z.| + ( dist (x,A))) < (r + ( dist (x,A))) by XREAL_1: 6;

      ( dist ((x + z),A)) <= ( |.z.| + ( dist (x,A))) by A1, Th114;

      then ( dist ((x + z),A)) < (r + ( dist (x,A))) by A3, XXREAL_0: 2;

      hence thesis;

    end;

    definition

      let n, A, B;

      :: SEQ_4:def19

      func dist (A,B) -> Real means

      : Def19: for X be Subset of REAL st X = { |.(x - z).| : x in A & z in B } holds it = ( lower_bound X);

      existence

      proof

        deffunc f( Element of ( COMPLEX n), Element of ( COMPLEX n)) = ( In ( |.($1 - $2).|, REAL ));

        deffunc g( Element of ( COMPLEX n), Element of ( COMPLEX n)) = |.($1 - $2).|;

        defpred P[ set, set] means $1 in A & $2 in B;

        reconsider X = { f(x,z) : P[x, z] } as Subset of REAL from DOMAIN_1:sch 9;

        

         A1: for z1,z2 be Element of ( COMPLEX n) holds f(z1,z2) = g(z1,z2);

        

         A2: { f(z1,z2) where z1,z2 be Element of ( COMPLEX n) : P[z1, z2] } = { g(z1,z2) where z1,z2 be Element of ( COMPLEX n) : P[z1, z2] } from FRAENKEL:sch 7( A1);

        take L = ( lower_bound X);

        thus thesis by A2;

      end;

      uniqueness

      proof

        let r1,r2 be Real such that

         A3: for X be Subset of REAL st X = { |.(x - z).| : x in A & z in B } holds r1 = ( lower_bound X) and

         A4: for X be Subset of REAL st X = { |.(x - z).| : x in A & z in B } holds r2 = ( lower_bound X);

        deffunc f( Element of ( COMPLEX n), Element of ( COMPLEX n)) = ( In ( |.($1 - $2).|, REAL ));

        deffunc g( Element of ( COMPLEX n), Element of ( COMPLEX n)) = |.($1 - $2).|;

        defpred P[ set, set] means $1 in A & $2 in B;

        reconsider X = { f(x,z) : P[x, z] } as Subset of REAL from DOMAIN_1:sch 9;

        

         A1: for z1,z2 be Element of ( COMPLEX n) holds f(z1,z2) = g(z1,z2);

        

         A2: { f(z1,z2) where z1,z2 be Element of ( COMPLEX n) : P[z1, z2] } = { g(z1,z2) where z1,z2 be Element of ( COMPLEX n) : P[z1, z2] } from FRAENKEL:sch 7( A1);

        r1 = ( lower_bound X) by A3, A2;

        hence thesis by A4, A2;

      end;

    end

    theorem :: SEQ_4:123

    for X,Y be Subset of REAL holds X <> {} & Y <> {} implies (X ++ Y) <> {} ;

    theorem :: SEQ_4:124

    

     Th123: for X,Y be Subset of REAL holds X is bounded_below & Y is bounded_below implies (X ++ Y) is bounded_below

    proof

      let X,Y be Subset of REAL ;

      assume X is bounded_below;

      then

      consider r1 be Real such that

       A1: r1 is LowerBound of X;

      

       A2: for r be Real st r in X holds r1 <= r by A1, XXREAL_2:def 2;

      assume Y is bounded_below;

      then

      consider r2 be Real such that

       A3: r2 is LowerBound of Y;

      

       A4: for r be Real st r in Y holds r2 <= r by A3, XXREAL_2:def 2;

      take (r1 + r2);

      let r be ExtReal;

      assume r in (X ++ Y);

      then r in { (r22 + r12) where r22,r12 be Complex : r22 in X & r12 in Y } by MEMBER_1:def 6;

      then

      consider r22,r12 be Complex such that

       A5: r = (r22 + r12) and

       A6: r22 in X and

       A7: r12 in Y;

      reconsider r9 = r22, r99 = r12 as Real by A6, A7;

      

       A8: r2 <= r99 by A4, A7;

      r1 <= r9 by A2, A6;

      hence thesis by A5, A8, XREAL_1: 7;

    end;

    theorem :: SEQ_4:125

    

     Th124: for X,Y be Subset of REAL st X <> {} & X is bounded_below & Y <> {} & Y is bounded_below holds ( lower_bound (X ++ Y)) = (( lower_bound X) + ( lower_bound Y))

    proof

      let X,Y be Subset of REAL such that

       A1: X <> {} and

       A2: X is bounded_below and

       A3: Y <> {} and

       A4: Y is bounded_below;

       A5:

      now

        let r9 be Real;

        assume 0 < r9;

        then

         A6: (r9 / 2) > 0 ;

        then

        consider r1 be Real such that

         A7: r1 in X and

         A8: r1 < (( lower_bound X) + (r9 / 2)) by A1, A2, Def2;

        consider r2 be Real such that

         A9: r2 in Y and

         A10: r2 < (( lower_bound Y) + (r9 / 2)) by A3, A4, A6, Def2;

        reconsider r = (r1 + r2) as Real;

        take r;

        thus r in (X ++ Y) by A7, A9, MEMBER_1: 46;

        ((( lower_bound X) + (r9 / 2)) + (( lower_bound Y) + (r9 / 2))) = ((( lower_bound X) + ( lower_bound Y)) + r9);

        hence r < ((( lower_bound X) + ( lower_bound Y)) + r9) by A8, A10, XREAL_1: 8;

      end;

       A11:

      now

        let r be Real;

        assume r in (X ++ Y);

        then r in { (r22 + r12) where r22,r12 be Complex : r22 in X & r12 in Y } by MEMBER_1:def 6;

        then

        consider r11,r22 be Complex such that

         A12: r = (r11 + r22) and

         A13: r11 in X & r22 in Y;

        reconsider r1 = r11, r2 = r22 as Real by A13;

        r1 >= ( lower_bound X) & r2 >= ( lower_bound Y) by A2, A4, A13, Def2;

        hence (( lower_bound X) + ( lower_bound Y)) <= r by A12, XREAL_1: 7;

      end;

      (X ++ Y) <> {} & (X ++ Y) is bounded_below by A1, A2, A3, A4, Th123;

      hence thesis by A11, A5, Def2;

    end;

    theorem :: SEQ_4:126

    

     Th125: for X,Y be Subset of REAL st Y is bounded_below & X <> {} & for r st r in X holds ex r1 st r1 in Y & r1 <= r holds ( lower_bound X) >= ( lower_bound Y)

    proof

      let X,Y be Subset of REAL such that

       A1: Y is bounded_below and

       A2: X <> {} and

       A3: for r st r in X holds ex r1 st r1 in Y & r1 <= r;

      now

        let r1;

        assume r1 in X;

        then

        consider r2 such that

         A4: r2 in Y and

         A5: r2 <= r1 by A3;

        ( lower_bound Y) <= r2 by A1, A4, Def2;

        hence r1 >= ( lower_bound Y) by A5, XXREAL_0: 2;

      end;

      hence thesis by A2, Th112;

    end;

    theorem :: SEQ_4:127

    

     Th126: A <> {} & B <> {} implies ( dist (A,B)) >= 0

    proof

      defpred P[ set, set] means $1 in A & $2 in B;

      deffunc f( Element of ( COMPLEX n), Element of ( COMPLEX n)) = |.($1 - $2).|;

      deffunc g( Element of ( COMPLEX n), Element of ( COMPLEX n)) = ( In ( |.($1 - $2).|, REAL ));

      

       A1: for z1,z2 be Element of ( COMPLEX n) holds f(z1,z2) = g(z1,z2);

      

       A2: { f(z1,z2) where z1,z2 be Element of ( COMPLEX n) : P[z1, z2] } = { g(z1,z2) where z1,z2 be Element of ( COMPLEX n) : P[z1, z2] } from FRAENKEL:sch 7( A1);

      reconsider Z = { g(z1,z) where z1,z be Element of ( COMPLEX n) : P[z1, z] } as Subset of REAL from DOMAIN_1:sch 9;

      assume that

       A3: A <> {} and

       A4: B <> {} ;

      consider z1 such that

       A5: z1 in A by A3, SUBSET_1: 4;

       A6:

      now

        let r9;

        assume r9 in Z;

        then ex z1, z st r9 = |.(z1 - z).| & z1 in A & z in B by A2;

        hence r9 >= 0 by Th94;

      end;

      consider z2 such that

       A7: z2 in B by A4, SUBSET_1: 4;

      

       A8: ( dist (A,B)) = ( lower_bound Z) by Def19, A2;

       |.(z1 - z2).| in Z by A5, A7, A2;

      hence thesis by A8, A6, Th112;

    end;

    theorem :: SEQ_4:128

    ( dist (A,B)) = ( dist (B,A))

    proof

      defpred R[ set, set] means $1 in B & $2 in A;

      deffunc f( Element of ( COMPLEX n), Element of ( COMPLEX n)) = ( In ( |.($1 - $2).|, REAL ));

      deffunc f1( Element of ( COMPLEX n), Element of ( COMPLEX n)) = |.($1 - $2).|;

      reconsider Y = { f(z,z1) where z,z1 be Element of ( COMPLEX n) : R[z, z1] } as Subset of REAL from DOMAIN_1:sch 9;

      defpred P[ set, set] means $1 in A & $2 in B;

      reconsider X = { f(z1,z) where z1,z be Element of ( COMPLEX n) : P[z1, z] } as Subset of REAL from DOMAIN_1:sch 9;

       A1:

      now

        let r be Element of REAL ;

         A2:

        now

          given z, z1 such that

           A3: r = f(z,z1) & z in B & z1 in A;

          take z1, z;

          thus r = f(z1,z) & z1 in A & z in B by A3, Th103;

        end;

        now

          given z1, z such that

           A4: r = f(z1,z) & z1 in A & z in B;

          take z, z1;

          thus r = f(z,z1) & z in B & z1 in A by A4, Th103;

        end;

        hence r in X iff r in Y by A2;

      end;

      

       A5: f(z,z1) = f1(z,z1);

      

       A6: { f(z,z1) where z,z1 be Element of ( COMPLEX n) : R[z, z1] } = { f1(z,z1) where z,z1 be Element of ( COMPLEX n) : R[z, z1] } from FRAENKEL:sch 7( A5);

      { f(z1,z) where z1,z be Element of ( COMPLEX n) : P[z1, z] } = { f1(z1,z) where z1,z be Element of ( COMPLEX n) : P[z1, z] } from FRAENKEL:sch 7( A5);

      then ( dist (A,B)) = ( lower_bound X) & ( dist (B,A)) = ( lower_bound Y) by Def19, A6;

      hence thesis by A1, SUBSET_1: 3;

    end;

    theorem :: SEQ_4:129

    

     Th128: A <> {} & B <> {} implies (( dist (x,A)) + ( dist (x,B))) >= ( dist (A,B))

    proof

      defpred Y[ set] means $1 in B;

      deffunc g( Element of ( COMPLEX n)) = |.(x - $1).|;

      deffunc g1( Element of ( COMPLEX n)) = ( In ( |.(x - $1).|, REAL ));

      reconsider Y = { g1(z) : Y[z] } as Subset of REAL from DOMAIN_1:sch 8;

      defpred P[ set, set] means $1 in A & $2 in B;

      defpred X[ set] means $1 in A;

      deffunc f( Element of ( COMPLEX n), Element of ( COMPLEX n)) = ( In ( |.($1 - $2).|, REAL ));

      deffunc f1( Element of ( COMPLEX n), Element of ( COMPLEX n)) = |.($1 - $2).|;

      reconsider X = { g1(z) : X[z] } as Subset of REAL from DOMAIN_1:sch 8;

      assume that

       A1: A <> {} and

       A2: B <> {} ;

      consider z2 such that

       A3: z2 in B by A2, SUBSET_1: 4;

      

       A4: Y <> {} & Y is bounded_below

      proof

         g1(z2) in Y by A3;

        hence Y <> {} ;

        take 0 ;

        let r be ExtReal;

        assume r in Y;

        then ex z1 st r = g1(z1) & z1 in B;

        hence thesis by Th94;

      end;

      

       A5: g1(z) = g(z);

      

       A6: { g1(z) : Y[z] } = { g(z1) : Y[z1] } from FRAENKEL:sch 5( A5);

      { g1(z) : X[z] } = { g(z1) : X[z1] } from FRAENKEL:sch 5( A5);

      then

       A7: ( lower_bound X) = ( dist (x,A)) & ( lower_bound Y) = ( dist (x,B)) by Def17, A6;

      

       A8: g1(z2) in Y by A3;

      reconsider Z = { f(z1,z) where z1, z : P[z1, z] } as Subset of REAL from DOMAIN_1:sch 9;

      consider z1 such that

       A9: z1 in A by A1, SUBSET_1: 4;

      (X ++ Y) c= REAL by MEMBERED: 3;

      then

      reconsider XY = (X ++ Y) as Subset of REAL ;

      

       A10: for r st r in XY holds ex r1 st r1 in Z & r1 <= r

      proof

        let r;

        assume r in XY;

        then r in { (r2 + r1) where r2,r1 be Complex : r2 in X & r1 in Y } by MEMBER_1:def 6;

        then

        consider r2,r1 be Complex such that

         A11: r = (r2 + r1) and

         A12: r2 in X and

         A13: r1 in Y;

        consider z2 such that

         A14: r1 = g1(z2) & z2 in B by A13;

        consider z1 such that

         A15: r2 = g1(z1) and

         A16: z1 in A by A12;

        take r3 = f(z1,z2);

        r2 = |.(z1 - x).| by A15, Th103;

        hence r3 in Z & r3 <= r by A11, A16, A14, Th104;

      end;

      

       A17: Z is bounded_below

      proof

        take 0 ;

        let r be ExtReal;

        assume r in Z;

        then ex z1, z st r = f(z1,z) & P[z1, z];

        hence thesis by Th94;

      end;

      

       A18: X <> {} & X is bounded_below

      proof

         g1(z1) in X by A9;

        hence X <> {} ;

        take 0 ;

        let r be ExtReal;

        assume r in X;

        then ex z st r = g1(z) & z in A;

        hence thesis by Th94;

      end;

      

       A19: for z3, z holds f(z3,z) = f1(z3,z);

      { f(z3,z) where z3,z be Element of ( COMPLEX n) : P[z3, z] } = { f1(z3,z) where z3,z be Element of ( COMPLEX n) : P[z3, z] } from FRAENKEL:sch 7( A19);

      then

       A20: ( lower_bound Z) = ( dist (A,B)) by Def19;

       g1(z1) in X by A9;

      then ( |.(x - z1).| + |.(x - z2).|) in (X ++ Y) by A8, MEMBER_1: 46;

      then XY <> {} ;

      then ( lower_bound XY) >= ( lower_bound Z) by A17, A10, Th125;

      hence thesis by A18, A4, A7, A20, Th124;

    end;

    theorem :: SEQ_4:130

    A meets B implies ( dist (A,B)) = 0

    proof

      assume A meets B;

      then

      consider z be object such that

       A1: z in A and

       A2: z in B by XBOOLE_0: 3;

      reconsider z as Element of ( COMPLEX n) by A1;

      ( dist (z,A)) = 0 & ( dist (z,B)) = 0 by A1, A2, Th115;

      then ( 0 qua Nat + 0 qua Nat) >= ( dist (A,B)) by A1, A2, Th128;

      hence thesis by A1, A2, Th126;

    end;

    definition

      let n;

      :: SEQ_4:def20

      func ComplexOpenSets (n) -> Subset-Family of ( COMPLEX n) equals { A where A be Subset of ( COMPLEX n) : A is open };

      coherence

      proof

        set S = { A where A be Subset of ( COMPLEX n) : A is open };

        S c= ( bool ( COMPLEX n))

        proof

          let x be object;

          assume x in S;

          then ex A be Subset of ( COMPLEX n) st x = A & A is open;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: SEQ_4:131

    for A be Subset of ( COMPLEX n) holds A in ( ComplexOpenSets n) iff A is open

    proof

      let B be Subset of ( COMPLEX n);

      B in { A where A be Subset of ( COMPLEX n) : A is open } iff ex C be Subset of ( COMPLEX n) st B = C & C is open;

      hence thesis;

    end;

    theorem :: SEQ_4:132

    for A be Subset of ( COMPLEX n) holds A is closed iff (A ` ) is open

    proof

      let A be Subset of ( COMPLEX n);

      thus A is closed implies (A ` ) is open

      proof

        assume

         A1: for x st for r st r > 0 holds ex z st |.z.| < r & (x + z) in A holds x in A;

        let x;

        assume x in (A ` );

        then not x in A by XBOOLE_0:def 5;

        then

        consider r such that

         A2: r > 0 and

         A3: for z st |.z.| < r holds not (x + z) in A by A1;

        take r;

        thus 0 < r by A2;

        let z;

        assume |.z.| < r;

        hence thesis by A3, SUBSET_1: 29;

      end;

      assume

       A4: for x st x in (A ` ) holds ex r st 0 < r & for z st |.z.| < r holds (x + z) in (A ` );

      let x such that

       A5: for r st r > 0 holds ex z st |.z.| < r & (x + z) in A;

      now

        let r;

        assume r > 0 ;

        then

        consider z such that

         A6: |.z.| < r & (x + z) in A by A5;

        take z;

        thus |.z.| < r & not (x + z) in (A ` ) by A6, XBOOLE_0:def 5;

      end;

      then not x in (A ` ) by A4;

      hence thesis by SUBSET_1: 29;

    end;

    begin

    reserve v,v1,v2 for FinSequence of REAL ,

n,m,k for Nat,

x for set;

    defpred P[ Nat] means for R be finite Subset of REAL st R <> {} & ( card R) = $1 holds R is bounded_above & ( upper_bound R) in R & R is bounded_below & ( lower_bound R) in R;

    

     Lm7: P[ 0 ];

    

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

    proof

      let n such that

       A1: P[n];

      let R be finite Subset of REAL such that

       A2: R <> {} and

       A3: ( card R) = (n + 1);

      now

        per cases ;

          suppose

           A4: n = 0 ;

          thus R is bounded_above;

          consider x be object such that

           A5: R = {x} by A3, A4, CARD_2: 42;

          x in R by A5, TARSKI:def 1;

          then

          reconsider r = x as Real;

          ( upper_bound R) = r by A5, Th9;

          hence ( upper_bound R) in R by A5, TARSKI:def 1;

          thus R is bounded_below;

          ( lower_bound R) = r by A5, Th9;

          hence ( lower_bound R) in R by A5, TARSKI:def 1;

        end;

          suppose

           A6: n <> 0 ;

          set x = the Element of R;

          reconsider x as Real;

          reconsider X = (R \ {x}) as finite Subset of REAL ;

          set u = ( upper_bound X), m = ( max (x,u)), l = ( lower_bound X), mi = ( min (x,l));

           {x} c= R by A2, ZFMISC_1: 31;

          then ( card (R \ {x})) = (( card R) - ( card {x})) by CARD_2: 44;

          

          then

           A7: ( card X) = ((n + 1) - 1) by A3, CARD_1: 30

          .= n;

          then

           A8: ( upper_bound X) in X by A1, A6, CARD_1: 27;

           A9:

          now

            reconsider s = m as Real;

            let r be Real such that

             A10: 0 < r;

            take s;

            now

              per cases by XXREAL_0: 16;

                suppose m = x;

                hence s in R by A2;

                thus (m - r) < s by A10, XREAL_1: 44;

              end;

                suppose m = u;

                hence s in R by A8, XBOOLE_0:def 5;

                thus (m - r) < s by A10, XREAL_1: 44;

              end;

            end;

            hence s in R & (m - r) < s;

          end;

          

           A11: ( lower_bound X) in X by A1, A6, A7, CARD_1: 27;

           A12:

          now

            reconsider s = mi as Real;

            let r be Real such that

             A13: 0 < r;

            take s;

            now

              per cases by XXREAL_0: 15;

                suppose mi = x;

                hence s in R by A2;

                thus s < (mi + r) by A13, XREAL_1: 29;

              end;

                suppose mi = l;

                hence s in R by A11, XBOOLE_0:def 5;

                thus s < (mi + r) by A13, XREAL_1: 29;

              end;

            end;

            hence s in R & s < (mi + r);

          end;

          thus R is bounded_above;

          

           A14: u <= m by XXREAL_0: 25;

           A15:

          now

            let s be Real such that

             A16: s in R;

            now

              per cases ;

                suppose s = x;

                hence s <= m by XXREAL_0: 25;

              end;

                suppose s <> x;

                then not s in {x} by TARSKI:def 1;

                then s in X by A16, XBOOLE_0:def 5;

                then s <= u by Def1;

                hence s <= m by A14, XXREAL_0: 2;

              end;

            end;

            hence s <= m;

          end;

          now

            per cases by XXREAL_0: 16;

              suppose m = x;

              hence m in R by A2;

            end;

              suppose m = u;

              hence m in R by A8, XBOOLE_0:def 5;

            end;

          end;

          hence ( upper_bound R) in R by A15, A9, Def1;

          thus R is bounded_below;

          

           A17: mi <= l by XXREAL_0: 17;

           A18:

          now

            let s be Real such that

             A19: s in R;

            now

              per cases ;

                suppose s = x;

                hence mi <= s by XXREAL_0: 17;

              end;

                suppose s <> x;

                then not s in {x} by TARSKI:def 1;

                then s in X by A19, XBOOLE_0:def 5;

                then l <= s by Def2;

                hence mi <= s by A17, XXREAL_0: 2;

              end;

            end;

            hence mi <= s;

          end;

          now

            per cases by XXREAL_0: 15;

              suppose mi = x;

              hence mi in R by A2;

            end;

              suppose mi = l;

              hence mi in R by A11, XBOOLE_0:def 5;

            end;

          end;

          hence ( lower_bound R) in R by A18, A12, Def2;

        end;

      end;

      hence thesis;

    end;

    

     Lm9: for n holds P[n] from NAT_1:sch 2( Lm7, Lm8);

    theorem :: SEQ_4:133

    

     Th132: for R be finite Subset of REAL holds R <> {} implies R is bounded_above & ( upper_bound R) in R & R is bounded_below & ( lower_bound R) in R

    proof

      let R be finite Subset of REAL ;

      assume

       A1: R <> {} ;

       P[( card R)] by Lm9;

      hence thesis by A1;

    end;

    theorem :: SEQ_4:134

    for n be Nat holds for f be FinSequence holds 1 <= n & (n + 1) <= ( len f) iff n in ( dom f) & (n + 1) in ( dom f)

    proof

      let n be Nat;

      let f be FinSequence;

      thus 1 <= n & (n + 1) <= ( len f) implies n in ( dom f) & (n + 1) in ( dom f)

      proof

        assume that

         A1: 1 <= n and

         A2: (n + 1) <= ( len f);

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

        then 1 <= (n + 1) & n <= ( len f) by A2, NAT_1: 11, XXREAL_0: 2;

        hence thesis by A1, A2, FINSEQ_3: 25;

      end;

      thus thesis by FINSEQ_3: 25;

    end;

    theorem :: SEQ_4:135

    for n be Nat holds for f be FinSequence holds 1 <= n & (n + 2) <= ( len f) iff n in ( dom f) & (n + 1) in ( dom f) & (n + 2) in ( dom f)

    proof

      let n be Nat;

      let f be FinSequence;

      thus 1 <= n & (n + 2) <= ( len f) implies n in ( dom f) & (n + 1) in ( dom f) & (n + 2) in ( dom f)

      proof

        assume that

         A1: 1 <= n and

         A2: (n + 2) <= ( len f);

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

        then

         A3: 1 <= (n + 1) & (n + 1) <= ( len f) by A2, NAT_1: 11, XXREAL_0: 2;

        n <= (n + 2) by NAT_1: 11;

        then 1 <= (n + 2) & n <= ( len f) by A1, A2, XXREAL_0: 2;

        hence thesis by A1, A2, A3, FINSEQ_3: 25;

      end;

      assume that

       A4: n in ( dom f) and (n + 1) in ( dom f) and

       A5: (n + 2) in ( dom f);

      thus thesis by A4, A5, FINSEQ_3: 25;

    end;

    theorem :: SEQ_4:136

    for D be non empty set, f1,f2 be FinSequence of D, n st 1 <= n & n <= ( len f2) holds ((f1 ^ f2) /. (n + ( len f1))) = (f2 /. n)

    proof

      let D be non empty set, f1,f2 be FinSequence of D, n such that

       A1: 1 <= n and

       A2: n <= ( len f2);

      

       A3: ( len f1) < (n + ( len f1)) by A1, NAT_1: 19;

      ( len (f1 ^ f2)) = (( len f1) + ( len f2)) by FINSEQ_1: 22;

      then

       A4: (n + ( len f1)) <= ( len (f1 ^ f2)) by A2, XREAL_1: 6;

      (n + ( len f1)) >= n by NAT_1: 11;

      then (n + ( len f1)) >= 1 by A1, XXREAL_0: 2;

      

      hence ((f1 ^ f2) /. (n + ( len f1))) = ((f1 ^ f2) . (n + ( len f1))) by A4, FINSEQ_4: 15

      .= (f2 . ((n + ( len f1)) - ( len f1))) by A3, A4, FINSEQ_1: 24

      .= (f2 /. n) by A1, A2, FINSEQ_4: 15;

    end;

    theorem :: SEQ_4:137

    v is increasing implies for n, m st n in ( dom v) & m in ( dom v) & n <= m holds (v . n) <= (v . m)

    proof

      assume

       A1: v is increasing;

      let n, m such that

       A2: n in ( dom v) & m in ( dom v) and

       A3: n <= m;

      now

        per cases ;

          suppose n = m;

          hence thesis;

        end;

          suppose n <> m;

          then n < m by A3, XXREAL_0: 1;

          hence thesis by A1, A2, SEQM_3:def 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: SEQ_4:138

    

     Th137: v is increasing implies for n, m st n in ( dom v) & m in ( dom v) & n <> m holds (v . n) <> (v . m)

    proof

      assume

       A1: v is increasing;

      let n, m;

      assume that

       A2: n in ( dom v) & m in ( dom v) and

       A3: n <> m;

      now

        per cases by A3, XXREAL_0: 1;

          suppose n < m;

          hence thesis by A1, A2, SEQM_3:def 1;

        end;

          suppose n > m;

          hence thesis by A1, A2, SEQM_3:def 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: SEQ_4:139

    

     Th138: v is increasing & v1 = (v | ( Seg n)) implies v1 is increasing

    proof

      assume that

       A1: v is increasing and

       A2: v1 = (v | ( Seg n));

      now

        per cases ;

          suppose n <= ( len v);

          then ( Seg n) c= ( Seg ( len v)) by FINSEQ_1: 5;

          then

           A3: ( Seg n) c= ( dom v) by FINSEQ_1:def 3;

          then ( Seg n) = (( dom v) /\ ( Seg n)) by XBOOLE_1: 28;

          then

           A4: ( dom v1) = ( Seg n) by A2, RELAT_1: 61;

          now

            let m, k such that

             A5: m in ( dom v1) & k in ( dom v1) and

             A6: m < k;

            set r = (v1 . m), s = (v1 . k);

            r = (v . m) & s = (v . k) by A2, A5, FUNCT_1: 47;

            hence r < s by A1, A3, A4, A5, A6, SEQM_3:def 1;

          end;

          hence thesis by SEQM_3:def 1;

        end;

          suppose ( len v) <= n;

          hence thesis by A1, A2, FINSEQ_2: 20;

        end;

      end;

      hence thesis;

    end;

    defpred P1[ Nat] means for v st ( card ( rng v)) = $1 holds ex v1 st ( rng v1) = ( rng v) & ( len v1) = ( card ( rng v)) & v1 is increasing;

    

     Lm10: P1[ 0 ]

    proof

      let v;

      assume ( card ( rng v)) = 0 ;

      then

       A1: ( rng v) = {} ;

      take v1 = v;

      thus ( rng v1) = ( rng v);

      thus ( len v1) = ( card ( rng v)) by A1, RELAT_1: 41;

      for n, m holds n in ( dom v1) & m in ( dom v1) & n < m implies (v1 . n) < (v1 . m) by A1, RELAT_1: 38, RELAT_1: 41;

      hence thesis by SEQM_3:def 1;

    end;

    

     Lm11: for n st P1[n] holds P1[(n + 1)]

    proof

      let n such that

       A1: P1[n];

      let v such that

       A2: ( card ( rng v)) = (n + 1);

      now

        reconsider R = ( rng v) as finite Subset of REAL ;

        set u = ( upper_bound R), X = (R \ {u});

        set f = (X |` v);

        ( Seq f) = (f * ( Sgm ( dom f))) & ( rng ( Sgm ( dom f))) = ( dom f) by FINSEQ_1: 50;

        

        then

         A3: ( rng ( Seq f)) = ( rng f) by RELAT_1: 28

        .= X by RELAT_1: 89, XBOOLE_1: 36;

        then

        reconsider f1 = ( Seq f) as FinSequence of REAL by FINSEQ_1:def 4;

        reconsider X as finite set;

        ( upper_bound R) in R by A2, Th132, CARD_1: 27;

        then

         A4: {u} c= R by ZFMISC_1: 31;

        then

         A5: ( card X) = (( card R) - ( card {u})) by CARD_2: 44;

        

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

        then

        consider v2 such that

         A7: ( rng v2) = ( rng f1) and

         A8: ( len v2) = ( card ( rng f1)) and

         A9: v2 is increasing by A1, A2, A3, A5;

        reconsider uu = u as Element of REAL by XREAL_0:def 1;

        take v1 = (v2 ^ <*uu*>);

        

        thus ( rng v1) = (X \/ ( rng <*u*>)) by A3, A7, FINSEQ_1: 31

        .= ((( rng v) \ {u}) \/ {u}) by FINSEQ_1: 39

        .= (( rng v) \/ {u}) by XBOOLE_1: 39

        .= ( rng v) by A4, XBOOLE_1: 12;

        

        thus

         A10: ( len v1) = (n + ( len <*u*>)) by A2, A3, A5, A6, A8, FINSEQ_1: 22

        .= ( card ( rng v)) by A2, FINSEQ_1: 39;

        now

          let k, m;

          assume that

           A11: k in ( dom v1) and

           A12: m in ( dom v1) and

           A13: k < m;

          

           A14: 1 <= m by A12, FINSEQ_3: 25;

          

           A15: m <= ( len v1) by A12, FINSEQ_3: 25;

          set r = (v1 . k), s = (v1 . m);

          

           A16: 1 <= k by A11, FINSEQ_3: 25;

          

           A17: k <= ( len v1) by A11, FINSEQ_3: 25;

          now

            per cases ;

              suppose

               A18: m = ( len v1);

              k < ( len v1) by A13, A15, XXREAL_0: 2;

              then k <= ( len v2) by A2, A3, A5, A6, A8, A10, NAT_1: 13;

              then

               A19: k in ( dom v2) by A16, FINSEQ_3: 25;

              then r = (v2 . k) by FINSEQ_1:def 7;

              then

               A20: r in ( rng v2) by A19, FUNCT_1:def 3;

              then r in R by A3, A7, XBOOLE_0:def 5;

              then

               A21: r <= u by Def1;

               not r in {u} by A3, A7, A20, XBOOLE_0:def 5;

              then

               A22: r <> u by TARSKI:def 1;

              s = u by A2, A3, A5, A6, A8, A10, A18, FINSEQ_1: 42;

              hence r < s by A21, A22, XXREAL_0: 1;

            end;

              suppose m <> ( len v1);

              then m < ( len v1) by A15, XXREAL_0: 1;

              then m <= ( len v2) by A2, A3, A5, A6, A8, A10, NAT_1: 13;

              then

               A23: m in ( dom v2) by A14, FINSEQ_3: 25;

              then

               A24: s = (v2 . m) by FINSEQ_1:def 7;

              k < ( len v1) by A13, A17, A15, XXREAL_0: 1;

              then k <= ( len v2) by A2, A3, A5, A6, A8, A10, NAT_1: 13;

              then

               A25: k in ( dom v2) by A16, FINSEQ_3: 25;

              then r = (v2 . k) by FINSEQ_1:def 7;

              hence r < s by A9, A13, A25, A23, A24, SEQM_3:def 1;

            end;

          end;

          hence r < s;

        end;

        hence v1 is increasing by SEQM_3:def 1;

      end;

      hence thesis;

    end;

    

     Lm12: for n holds P1[n] from NAT_1:sch 2( Lm10, Lm11);

    theorem :: SEQ_4:140

    for v holds ex v1 st ( rng v1) = ( rng v) & ( len v1) = ( card ( rng v)) & v1 is increasing by Lm12;

    defpred P3[ Nat] means for v1, v2 st ( len v1) = $1 & ( len v2) = $1 & ( rng v1) = ( rng v2) & v1 is increasing & v2 is increasing holds v1 = v2;

    

     Lm13: P3[ 0 ]

    proof

      let v1, v2;

      assume that

       A1: ( len v1) = 0 and

       A2: ( len v2) = 0 and ( rng v1) = ( rng v2) and v1 is increasing and v2 is increasing;

      v1 = {} by A1;

      hence thesis by A2;

    end;

    

     Lm14: for n st P3[n] holds P3[(n + 1)]

    proof

      let n such that

       A1: P3[n];

      let v1, v2 such that

       A2: ( len v1) = (n + 1) and

       A3: ( len v2) = (n + 1) and

       A4: ( rng v1) = ( rng v2) and

       A5: v1 is increasing and

       A6: v2 is increasing;

      reconsider X = ( rng v1) as Subset of REAL ;

      set u = ( upper_bound X);

      X <> {} by A2, CARD_1: 27, RELAT_1: 41;

      then

       A7: ( upper_bound X) in X by Th132;

      then

      consider m be Nat such that

       A8: m in ( dom v2) and

       A9: (v2 . m) = u by A4, FINSEQ_2: 10;

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

      

       A10: m <= ( len v2) by A8, FINSEQ_3: 25;

      

       A11: n <= (n + 1) by NAT_1: 11;

      then ( Seg n) c= ( Seg (n + 1)) by FINSEQ_1: 5;

      then

       A12: ( Seg n) = (( Seg (n + 1)) /\ ( Seg n)) by XBOOLE_1: 28;

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

      then

       A13: ( dom (v2 | ( Seg n))) = ( Seg n) by A3, A12, RELAT_1: 61;

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

      then

       A14: ( dom (v1 | ( Seg n))) = ( Seg n) by A2, A12, RELAT_1: 61;

      then

      reconsider f1 = (v1 | ( Seg n)), f2 = (v2 | ( Seg n)) as FinSequence by A13, FINSEQ_1:def 2;

      ( rng f2) c= ( rng v2) by RELAT_1: 70;

      then

       A15: ( rng f2) c= REAL by XBOOLE_1: 1;

      ( rng f1) c= ( rng v1) by RELAT_1: 70;

      then ( rng f1) c= REAL by XBOOLE_1: 1;

      then

      reconsider f1, f2 as FinSequence of REAL by A15, FINSEQ_1:def 4;

      consider k be Nat such that

       A16: k in ( dom v1) and

       A17: (v1 . k) = u by A7, FINSEQ_2: 10;

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

      

       A18: k <= ( len v1) by A16, FINSEQ_3: 25;

      

       A19: 1 <= k by A16, FINSEQ_3: 25;

       A20:

      now

        assume k <> ( len v1);

        then k < ( len v1) by A18, XXREAL_0: 1;

        then

         A21: (k + 1) <= ( len v1) by NAT_1: 13;

        reconsider s = (v1 . (k + 1)) as Real;

        

         A22: k < (k + 1) by NAT_1: 13;

        1 <= (k + 1) by A19, NAT_1: 13;

        then

         A23: (k + 1) in ( dom v1) by A21, FINSEQ_3: 25;

        then (v1 . (k + 1)) in ( rng v1) by FUNCT_1:def 3;

        then s <= u by Def1;

        hence contradiction by A5, A16, A17, A23, A22, SEQM_3:def 1;

      end;

      

       A24: 1 <= m by A8, FINSEQ_3: 25;

       A25:

      now

        assume m <> ( len v2);

        then m < ( len v2) by A10, XXREAL_0: 1;

        then

         A26: (m + 1) <= ( len v2) by NAT_1: 13;

        reconsider s = (v2 . (m + 1)) as Real;

        

         A27: m < (m + 1) by NAT_1: 13;

        1 <= (m + 1) by A24, NAT_1: 13;

        then

         A28: (m + 1) in ( dom v2) by A26, FINSEQ_3: 25;

        then (v2 . (m + 1)) in ( rng v2) by FUNCT_1:def 3;

        then s <= u by A4, Def1;

        hence contradiction by A6, A8, A9, A28, A27, SEQM_3:def 1;

      end;

      n in NAT by ORDINAL1:def 12;

      then

       A29: ( len f1) = n by A14, FINSEQ_1:def 3;

      then

       A30: ( dom f1) c= ( dom v1) by A2, A11, FINSEQ_3: 30;

      

       A31: ( rng f1) = (( rng v1) \ {u})

      proof

        thus ( rng f1) c= (( rng v1) \ {u})

        proof

          let x be object;

          assume x in ( rng f1);

          then

          consider i be Nat such that

           A32: i in ( dom f1) and

           A33: (f1 . i) = x by FINSEQ_2: 10;

          

           A34: x = (v1 . i) by A32, A33, FUNCT_1: 47;

          

           A35: (v1 . i) in ( rng v1) by A30, A32, FUNCT_1:def 3;

          i <= n by A14, A32, FINSEQ_1: 1;

          then i <> (n + 1) by NAT_1: 13;

          then x <> u by A2, A5, A16, A17, A20, A30, A32, A34, Th137;

          then not x in {u} by TARSKI:def 1;

          hence thesis by A34, A35, XBOOLE_0:def 5;

        end;

        let x be object;

        assume

         A36: x in (( rng v1) \ {u});

        then x in ( rng v1) by XBOOLE_0:def 5;

        then

        consider i be Nat such that

         A37: i in ( dom v1) and

         A38: (v1 . i) = x by FINSEQ_2: 10;

        

         A39: i <= ( len v1) by A37, FINSEQ_3: 25;

         not x in {u} by A36, XBOOLE_0:def 5;

        then i <> ( len v1) by A17, A20, A38, TARSKI:def 1;

        then i < ( len v1) by A39, XXREAL_0: 1;

        then

         A40: i <= ( len f1) by A2, A29, NAT_1: 13;

        1 <= i by A37, FINSEQ_3: 25;

        then

         A41: i in ( dom f1) by A40, FINSEQ_3: 25;

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

        hence thesis by A38, A41, FUNCT_1: 47;

      end;

      

       A42: ( dom v1) = ( Seg ( len v1)) by FINSEQ_1:def 3;

       A43:

      now

        let i be Nat;

        assume

         A44: i in ( dom v1);

        then

         A45: 1 <= i by A42, FINSEQ_1: 1;

        

         A46: i <= (( len f1) + 1) by A2, A29, A42, A44, FINSEQ_1: 1;

        now

          per cases ;

            suppose i = (( len f1) + 1);

            hence ((f1 ^ <*u*>) . i) = (v1 . i) by A2, A17, A20, A29, FINSEQ_1: 42;

          end;

            suppose i <> (( len f1) + 1);

            then i < (( len f1) + 1) by A46, XXREAL_0: 1;

            then i <= ( len f1) by NAT_1: 13;

            then

             A47: i in ( dom f1) by A14, A29, A45;

            

            hence ((f1 ^ <*u*>) . i) = (f1 . i) by FINSEQ_1:def 7

            .= (v1 . i) by A47, FUNCT_1: 47;

          end;

        end;

        hence ((f1 ^ <*u*>) . i) = (v1 . i);

      end;

      ( len (f1 ^ <*u*>)) = (n + ( len <*u*>)) by A29, FINSEQ_1: 22

      .= ( len v1) by A2, FINSEQ_1: 39;

      then

       A48: v1 = (f1 ^ <*u*>) by A43, FINSEQ_2: 9;

      n in NAT by ORDINAL1:def 12;

      then

       A49: ( len f2) = n by A13, FINSEQ_1:def 3;

      

      then

       A50: ( len (f2 ^ <*u*>)) = (n + ( len <*u*>)) by FINSEQ_1: 22

      .= ( len v2) by A3, FINSEQ_1: 39;

      

       A51: ( dom f2) c= ( dom v2) by A3, A11, A49, FINSEQ_3: 30;

      

       A52: ( rng f2) = (( rng v2) \ {u})

      proof

        thus ( rng f2) c= (( rng v2) \ {u})

        proof

          let x be object;

          assume x in ( rng f2);

          then

          consider i be Nat such that

           A53: i in ( dom f2) and

           A54: (f2 . i) = x by FINSEQ_2: 10;

          

           A55: x = (v2 . i) by A53, A54, FUNCT_1: 47;

          

           A56: (v2 . i) in ( rng v2) by A51, A53, FUNCT_1:def 3;

          i <= n by A13, A53, FINSEQ_1: 1;

          then i <> (n + 1) by NAT_1: 13;

          then x <> u by A3, A6, A8, A9, A25, A51, A53, A55, Th137;

          then not x in {u} by TARSKI:def 1;

          hence thesis by A55, A56, XBOOLE_0:def 5;

        end;

        let x be object;

        assume

         A57: x in (( rng v2) \ {u});

        then x in ( rng v2) by XBOOLE_0:def 5;

        then

        consider i be Nat such that

         A58: i in ( dom v2) and

         A59: (v2 . i) = x by FINSEQ_2: 10;

        

         A60: i <= ( len v2) by A58, FINSEQ_3: 25;

         not x in {u} by A57, XBOOLE_0:def 5;

        then i <> ( len v2) by A9, A25, A59, TARSKI:def 1;

        then i < ( len v2) by A60, XXREAL_0: 1;

        then

         A61: i <= ( len f2) by A3, A49, NAT_1: 13;

        1 <= i by A58, FINSEQ_3: 25;

        then

         A62: i in ( dom f2) by A61, FINSEQ_3: 25;

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

        hence thesis by A59, A62, FUNCT_1: 47;

      end;

      

       A63: ( dom v2) = ( Seg ( len v2)) by FINSEQ_1:def 3;

       A64:

      now

        let i be Nat;

        assume

         A65: i in ( dom v2);

        then

         A66: 1 <= i by A63, FINSEQ_1: 1;

        

         A67: i <= (( len f2) + 1) by A3, A49, A63, A65, FINSEQ_1: 1;

        now

          per cases ;

            suppose i = (( len f2) + 1);

            hence ((f2 ^ <*u*>) . i) = (v2 . i) by A3, A9, A25, A49, FINSEQ_1: 42;

          end;

            suppose i <> (( len f2) + 1);

            then i < (( len f2) + 1) by A67, XXREAL_0: 1;

            then i <= ( len f2) by NAT_1: 13;

            then

             A68: i in ( dom f2) by A13, A49, A66;

            

            hence ((f2 ^ <*u*>) . i) = (f2 . i) by FINSEQ_1:def 7

            .= (v2 . i) by A68, FUNCT_1: 47;

          end;

        end;

        hence ((f2 ^ <*u*>) . i) = (v2 . i);

      end;

      f1 is increasing & f2 is increasing by A5, A6, Th138;

      then f1 = f2 by A1, A4, A29, A49, A31, A52;

      hence thesis by A48, A50, A64, FINSEQ_2: 9;

    end;

    

     Lm15: for n holds P3[n] from NAT_1:sch 2( Lm13, Lm14);

    theorem :: SEQ_4:141

    for v1, v2 st ( len v1) = ( len v2) & ( rng v1) = ( rng v2) & v1 is increasing & v2 is increasing holds v1 = v2 by Lm15;

    definition

      let v;

      :: SEQ_4:def21

      func Incr (v) -> increasing FinSequence of REAL means

      : Def21: ( rng it ) = ( rng v) & ( len it ) = ( card ( rng v));

      existence

      proof

        consider v1 such that

         A1: ( rng v1) = ( rng v) & ( len v1) = ( card ( rng v)) and

         A2: v1 is increasing by Lm12;

        reconsider v1 as increasing FinSequence of REAL by A2;

        take v1;

        thus thesis by A1;

      end;

      uniqueness by Lm15;

    end

    registration

      let v be non empty FinSequence of REAL ;

      cluster ( Incr v) -> non empty;

      coherence

      proof

        

         A1: ( len ( Incr v)) = ( card ( rng v)) by Def21;

        assume ( Incr v) is empty;

        then ( rng v) = {} by A1;

        hence contradiction;

      end;

    end

    registration

      cluster non empty bounded_above bounded_below for Subset of REAL ;

      existence

      proof

        reconsider A = { 0 } as Subset of REAL ;

        take A;

        thus A is non empty;

        thus A is bounded_above;

        take 0 ;

        let t be ExtReal;

        assume t in A;

        hence thesis;

      end;

    end

    theorem :: SEQ_4:142

    for A,B be non empty bounded_below Subset of REAL holds ( lower_bound (A \/ B)) = ( min (( lower_bound A),( lower_bound B)))

    proof

      let A,B be non empty bounded_below Subset of REAL ;

      set r = ( min (( lower_bound A),( lower_bound B)));

      

       A1: r <= ( lower_bound B) by XXREAL_0: 17;

      

       A2: for r1 be Real st for t be Real st t in (A \/ B) holds t >= r1 holds r >= r1

      proof

        let r1 be Real;

        assume

         A3: for t be Real st t in (A \/ B) holds t >= r1;

        now

          let t be Real;

          assume t in B;

          then t in (A \/ B) by XBOOLE_0:def 3;

          hence t >= r1 by A3;

        end;

        then

         A4: ( lower_bound B) >= r1 by Th43;

        now

          let t be Real;

          assume t in A;

          then t in (A \/ B) by XBOOLE_0:def 3;

          hence t >= r1 by A3;

        end;

        then ( lower_bound A) >= r1 by Th43;

        hence thesis by A4, XXREAL_0: 20;

      end;

      

       A5: r <= ( lower_bound A) by XXREAL_0: 17;

      for t be Real st t in (A \/ B) holds t >= r

      proof

        let t be Real;

        assume t in (A \/ B);

        then t in A or t in B by XBOOLE_0:def 3;

        then ( lower_bound A) <= t or ( lower_bound B) <= t by Def2;

        hence thesis by A5, A1, XXREAL_0: 2;

      end;

      hence thesis by A2, Th44;

    end;

    theorem :: SEQ_4:143

    for A,B be non empty bounded_above Subset of REAL holds ( upper_bound (A \/ B)) = ( max (( upper_bound A),( upper_bound B)))

    proof

      let A,B be non empty bounded_above Subset of REAL ;

      set r = ( max (( upper_bound A),( upper_bound B)));

      

       A1: r >= ( upper_bound B) by XXREAL_0: 25;

      

       A2: for r1 be Real st for t be Real st t in (A \/ B) holds t <= r1 holds r <= r1

      proof

        let r1 be Real;

        assume

         A3: for t be Real st t in (A \/ B) holds t <= r1;

        now

          let t be Real;

          assume t in B;

          then t in (A \/ B) by XBOOLE_0:def 3;

          hence t <= r1 by A3;

        end;

        then

         A4: ( upper_bound B) <= r1 by Th45;

        now

          let t be Real;

          assume t in A;

          then t in (A \/ B) by XBOOLE_0:def 3;

          hence t <= r1 by A3;

        end;

        then ( upper_bound A) <= r1 by Th45;

        hence thesis by A4, XXREAL_0: 28;

      end;

      

       A5: r >= ( upper_bound A) by XXREAL_0: 25;

      for t be Real st t in (A \/ B) holds t <= r

      proof

        let t be Real;

        assume t in (A \/ B);

        then t in A or t in B by XBOOLE_0:def 3;

        then ( upper_bound A) >= t or ( upper_bound B) >= t by Def1;

        hence thesis by A5, A1, XXREAL_0: 2;

      end;

      hence thesis by A2, Th46;

    end;

    theorem :: SEQ_4:144

    for R be non empty Subset of REAL , r0 be Real st for r be Real st r in R holds r <= r0 holds ( upper_bound R) <= r0

    proof

      let R be non empty Subset of REAL , r0 be Real;

      assume

       A1: for r be Real st r in R holds r <= r0;

      then for r be ExtReal st r in R holds r <= r0;

      then r0 is UpperBound of R by XXREAL_2:def 1;

      then

       A2: R is bounded_above;

      now

        set r1 = (( upper_bound R) - r0);

        assume ( upper_bound R) > r0;

        then r1 > 0 by XREAL_1: 50;

        then ex r be Real st r in R & (( upper_bound R) - r1) < r by A2, Def1;

        hence contradiction by A1;

      end;

      hence thesis;

    end;