normsp_1.miz



    begin

    definition

      struct ( RLSStruct, N-ZeroStr) NORMSTR (# the carrier -> set,

the ZeroF -> Element of the carrier,

the addF -> BinOp of the carrier,

the Mult -> Function of [: REAL , the carrier:], the carrier,

the normF -> Function of the carrier, REAL #)

       attr strict strict;

    end

    registration

      cluster non empty strict for NORMSTR;

      existence

      proof

        set A = the non empty set, Z = the Element of A, a = the BinOp of A, M = the Function of [: REAL , A:], A, n = the Function of A, REAL ;

        take NORMSTR (# A, Z, a, M, n #);

        thus the carrier of NORMSTR (# A, Z, a, M, n #) is non empty;

        thus thesis;

      end;

    end

    reserve a,b for Real;

    deffunc 09( NORMSTR) = ( 0. $1);

    set V = the RealLinearSpace;

    

     Lm1: the carrier of ( (0). V) = {( 0. V)} by RLSUB_1:def 3;

    reconsider niltonil = (the carrier of ( (0). V) --> ( In ( 0 , REAL ))) as Function of the carrier of ( (0). V), REAL ;

    ( 0. V) is VECTOR of ( (0). V) by Lm1, TARSKI:def 1;

    then

     Lm2: (niltonil . ( 0. V)) = 0 by FUNCOP_1: 7;

    

     Lm3: for u be VECTOR of ( (0). V), a holds (niltonil . (a * u)) = ( |.a.| * (niltonil . u))

    proof

      let u be VECTOR of ( (0). V);

      let a;

      (niltonil . u) = 0 by FUNCOP_1: 7;

      hence thesis by FUNCOP_1: 7;

    end;

    

     Lm4: for u,v be VECTOR of ( (0). V) holds (niltonil . (u + v)) <= ((niltonil . u) + (niltonil . v))

    proof

      let u,v be VECTOR of ( (0). V);

      u = ( 0. V) & v = ( 0. V) by Lm1, TARSKI:def 1;

      hence thesis by Lm1, Lm2, TARSKI:def 1;

    end;

    reconsider X = NORMSTR (# the carrier of ( (0). V), ( 0. ( (0). V)), the addF of ( (0). V), the Mult of ( (0). V), niltonil #) as non empty NORMSTR;

     Lm5:

    now

      let x,y be Point of X;

      let a;

      reconsider u = x, w = y as VECTOR of ( (0). V);

       09(X) = ( 0. V) by RLSUB_1: 11;

      hence ||.x.|| = 0 iff x = 09(X) by Lm1, FUNCOP_1: 7, TARSKI:def 1;

      (a * x) = (a * u);

      hence ||.(a * x).|| = ( |.a.| * ||.x.||) by Lm3;

      (x + y) = (u + w);

      hence ||.(x + y).|| <= ( ||.x.|| + ||.y.||) by Lm4;

    end;

    definition

      let IT be non empty NORMSTR;

      :: NORMSP_1:def1

      attr IT is RealNormSpace-like means

      : Def1: for x,y be Point of IT, a holds ||.(a * x).|| = ( |.a.| * ||.x.||) & ||.(x + y).|| <= ( ||.x.|| + ||.y.||);

    end

    registration

      cluster reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable strict for non empty NORMSTR;

      existence

      proof

        take X;

        thus X is reflexive by Lm5;

        thus X is discerning by Lm5;

        thus X is RealNormSpace-like by Lm5;

        thus X is vector-distributive scalar-distributive scalar-associative scalar-unital

        proof

          thus for a be Real holds for v,w be VECTOR of X holds (a * (v + w)) = ((a * v) + (a * w))

          proof

            let a be Real;

            let v,w be VECTOR of X;

            reconsider v9 = v, w9 = w as VECTOR of ( (0). V);

            

            thus (a * (v + w)) = (a * (v9 + w9))

            .= ((a * v9) + (a * w9)) by RLVECT_1:def 5

            .= ((a * v) + (a * w));

          end;

          thus for a,b be Real holds for v be VECTOR of X holds ((a + b) * v) = ((a * v) + (b * v))

          proof

            let a,b be Real;

            let v be VECTOR of X;

            reconsider v9 = v as VECTOR of ( (0). V);

            

            thus ((a + b) * v) = ((a + b) * v9)

            .= ((a * v9) + (b * v9)) by RLVECT_1:def 6

            .= ((a * v) + (b * v));

          end;

          thus for a,b be Real holds for v be VECTOR of X holds ((a * b) * v) = (a * (b * v))

          proof

            let a,b be Real;

            let v be VECTOR of X;

            reconsider v9 = v as VECTOR of ( (0). V);

            

            thus ((a * b) * v) = ((a * b) * v9)

            .= (a * (b * v9)) by RLVECT_1:def 7

            .= (a * (b * v));

          end;

          let v be VECTOR of X;

          reconsider v9 = v as VECTOR of ( (0). V);

          

          thus (1 * v) = (1 * v9)

          .= v by RLVECT_1:def 8;

        end;

        

         A1: for x,y be VECTOR of X holds for x9,y9 be VECTOR of ( (0). V) st x = x9 & y = y9 holds (x + y) = (x9 + y9) & for a holds (a * x) = (a * x9);

        thus for v,w be VECTOR of X holds (v + w) = (w + v)

        proof

          let v,w be VECTOR of X;

          reconsider v9 = v, w9 = w as VECTOR of ( (0). V);

          

          thus (v + w) = (w9 + v9) by A1

          .= (w + v);

        end;

        thus for u,v,w be VECTOR of X holds ((u + v) + w) = (u + (v + w))

        proof

          let u,v,w be VECTOR of X;

          reconsider u9 = u, v9 = v, w9 = w as VECTOR of ( (0). V);

          

          thus ((u + v) + w) = ((u9 + v9) + w9)

          .= (u9 + (v9 + w9)) by RLVECT_1:def 3

          .= (u + (v + w));

        end;

        thus for v be VECTOR of X holds (v + ( 0. X)) = v

        proof

          let v be VECTOR of X;

          reconsider v9 = v as VECTOR of ( (0). V);

          

          thus (v + ( 0. X)) = (v9 + ( 0. ( (0). V)))

          .= v;

        end;

        thus X is right_complementable

        proof

          let v be VECTOR of X;

          reconsider v9 = v as VECTOR of ( (0). V);

          consider w9 be VECTOR of ( (0). V) such that

           A2: (v9 + w9) = ( 0. ( (0). V)) by ALGSTR_0:def 11;

          reconsider w = w9 as VECTOR of X;

          take w;

          thus thesis by A2;

        end;

        thus thesis;

      end;

    end

    definition

      mode RealNormSpace is reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty NORMSTR;

    end

    reserve RNS for RealNormSpace;

    reserve x,y,z,g,g1,g2 for Point of RNS;

    theorem :: NORMSP_1:1

     ||.( 0. RNS).|| = 0 ;

    theorem :: NORMSP_1:2

    

     Th2: ||.( - x).|| = ||.x.||

    proof

      

       A1: |.( - 1).| = ( - ( - 1)) by ABSVALUE:def 1

      .= 1;

       ||.( - x).|| = ||.(( - 1) * x).|| by RLVECT_1: 16

      .= ( |.( - 1).| * ||.x.||) by Def1;

      hence thesis by A1;

    end;

    theorem :: NORMSP_1:3

    

     Th3: ||.(x - y).|| <= ( ||.x.|| + ||.y.||)

    proof

       ||.(x - y).|| <= ( ||.x.|| + ||.( - y).||) by Def1;

      hence thesis by Th2;

    end;

    theorem :: NORMSP_1:4

    

     Th4: 0 <= ||.x.||

    proof

       ||.(x - x).|| = ||. 09(RNS).|| by RLVECT_1: 15

      .= 0 ;

      then 0 <= (( ||.x.|| + ||.x.||) / 2) by Th3;

      hence thesis;

    end;

    registration

      let RNS, x;

      cluster ||.x.|| -> non negative;

      coherence by Th4;

    end

    theorem :: NORMSP_1:5

     ||.((a * x) + (b * y)).|| <= (( |.a.| * ||.x.||) + ( |.b.| * ||.y.||))

    proof

       ||.((a * x) + (b * y)).|| <= ( ||.(a * x).|| + ||.(b * y).||) by Def1;

      then ||.((a * x) + (b * y)).|| <= (( |.a.| * ||.x.||) + ||.(b * y).||) by Def1;

      hence thesis by Def1;

    end;

    theorem :: NORMSP_1:6

    

     Th6: ||.(x - y).|| = 0 iff x = y

    proof

       ||.(x - y).|| = 0 iff (x - y) = 09(RNS) by NORMSP_0:def 5;

      hence thesis by RLVECT_1: 15, RLVECT_1: 21;

    end;

    theorem :: NORMSP_1:7

    

     Th7: ||.(x - y).|| = ||.(y - x).||

    proof

      (x - y) = ( - (y - x)) by RLVECT_1: 33;

      hence thesis by Th2;

    end;

    theorem :: NORMSP_1:8

    

     Th8: ( ||.x.|| - ||.y.||) <= ||.(x - y).||

    proof

      ((x - y) + y) = (x - (y - y)) by RLVECT_1: 29

      .= (x - 09(RNS)) by RLVECT_1: 15

      .= x;

      then ||.x.|| <= ( ||.(x - y).|| + ||.y.||) by Def1;

      hence thesis by XREAL_1: 20;

    end;

    theorem :: NORMSP_1:9

    

     Th9: |.( ||.x.|| - ||.y.||).| <= ||.(x - y).||

    proof

      ((y - x) + x) = (y - (x - x)) by RLVECT_1: 29

      .= (y - 09(RNS)) by RLVECT_1: 15

      .= y;

      then ||.y.|| <= ( ||.(y - x).|| + ||.x.||) by Def1;

      then ( ||.y.|| - ||.x.||) <= ||.(y - x).|| by XREAL_1: 20;

      then ( ||.y.|| - ||.x.||) <= ||.(x - y).|| by Th7;

      then

       A1: ( - ( ||.y.|| - ||.x.||)) >= ( - ||.(x - y).||) by XREAL_1: 24;

      ( ||.x.|| - ||.y.||) <= ||.(x - y).|| by Th8;

      hence thesis by A1, ABSVALUE: 5;

    end;

    theorem :: NORMSP_1:10

    

     Th10: ||.(x - z).|| <= ( ||.(x - y).|| + ||.(y - z).||)

    proof

      (x - z) = (x + ( 09(RNS) + ( - z)))

      .= (x + ((( - y) + y) + ( - z))) by RLVECT_1: 5

      .= (x + (( - y) + (y + ( - z)))) by RLVECT_1:def 3

      .= ((x - y) + (y - z)) by RLVECT_1:def 3;

      hence thesis by Def1;

    end;

    theorem :: NORMSP_1:11

    x <> y implies ||.(x - y).|| <> 0 by Th6;

    reserve S,S1,S2 for sequence of RNS;

    reserve k,n,m,m1,m2 for Nat;

    reserve r for Real;

    reserve f for Function;

    reserve d,s,t for set;

    theorem :: NORMSP_1:12

    for RNS be non empty 1-sorted, x be Element of RNS holds f is sequence of RNS iff (( dom f) = NAT & for d st d in NAT holds (f . d) is Element of RNS)

    proof

      let RNS be non empty 1-sorted;

      let x be Element of RNS;

      thus f is sequence of RNS implies (( dom f) = NAT & for d st d in NAT holds (f . d) is Element of RNS)

      proof

        assume

         A1: f is sequence of RNS;

        then

         A2: ( rng f) c= the carrier of RNS by RELAT_1:def 19;

        

         A3: ( dom f) = NAT by A1, FUNCT_2:def 1;

        for d st d in NAT holds (f . d) is Element of RNS

        proof

          let d;

          assume d in NAT ;

          then (f . d) in ( rng f) by A3, FUNCT_1:def 3;

          hence thesis by A2;

        end;

        hence thesis by A1, FUNCT_2:def 1;

      end;

      thus (( dom f) = NAT & for d st d in NAT holds (f . d) is Element of RNS) implies f is sequence of RNS

      proof

        assume that

         A4: ( dom f) = NAT and

         A5: for d st d in NAT holds (f . d) is Element of RNS;

        for s be object st s in ( rng f) holds s in the carrier of RNS

        proof

          let s be object;

          assume s in ( rng f);

          then

          consider d be object such that

           A6: d in ( dom f) and

           A7: s = (f . d) by FUNCT_1:def 3;

          (f . d) is Element of RNS by A4, A5, A6;

          hence thesis by A7;

        end;

        then ( rng f) c= the carrier of RNS by TARSKI:def 3;

        hence thesis by A4, FUNCT_2:def 1, RELSET_1: 4;

      end;

    end;

    theorem :: NORMSP_1:13

    for RNS be non empty 1-sorted, x be Element of RNS holds ex S be sequence of RNS st ( rng S) = {x}

    proof

      let RNS be non empty 1-sorted;

      let x be Element of RNS;

      consider f such that

       A1: ( dom f) = NAT and

       A2: ( rng f) = {x} by FUNCT_1: 5;

      reconsider f as sequence of RNS by A1, A2, FUNCT_2:def 1, RELSET_1: 4;

      take f;

      thus thesis by A2;

    end;

    theorem :: NORMSP_1:14

    for RNS be non empty 1-sorted, S be sequence of RNS st (ex x be Element of RNS st for n be Nat holds (S . n) = x) holds ex x be Element of RNS st ( rng S) = {x}

    proof

      let RNS be non empty 1-sorted;

      let S be sequence of RNS;

      given z be Element of RNS such that

       A1: for n be Nat holds (S . n) = z;

      take x = z;

      now

        let s be object;

        assume s in {x};

        then

         A2: s = x by TARSKI:def 1;

        now

          assume

           A3: not s in ( rng S);

          now

            let n;

            n in NAT by ORDINAL1:def 12;

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

            then (S . n) <> x by A2, A3, FUNCT_1:def 3;

            hence contradiction by A1;

          end;

          hence contradiction;

        end;

        hence s in ( rng S);

      end;

      then

       A4: {x} c= ( rng S) by TARSKI:def 3;

      now

        let t be object;

        assume t in ( rng S);

        then

        consider d be object such that

         A5: d in ( dom S) and

         A6: (S . d) = t by FUNCT_1:def 3;

        d in NAT by A5, FUNCT_2:def 1;

        then t = z by A1, A6;

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

      end;

      then ( rng S) c= {x} by TARSKI:def 3;

      hence thesis by A4, XBOOLE_0:def 10;

    end;

    theorem :: NORMSP_1:15

    for RNS be non empty 1-sorted, S be sequence of RNS st ex x be Element of RNS st ( rng S) = {x} holds for n holds (S . n) = (S . (n + 1))

    proof

      let RNS be non empty 1-sorted;

      let S be sequence of RNS;

      given z be Element of RNS such that

       A1: ( rng S) = {z};

      let n;

      n in NAT by ORDINAL1:def 12;

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

      then (S . n) in {z} by A1, FUNCT_1:def 3;

      then

       A2: (S . n) = z by TARSKI:def 1;

      (n + 1) in NAT ;

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

      then (S . (n + 1)) in {z} by A1, FUNCT_1:def 3;

      hence thesis by A2, TARSKI:def 1;

    end;

    theorem :: NORMSP_1:16

    for RNS be non empty 1-sorted, S be sequence of RNS st for n holds (S . n) = (S . (n + 1)) holds for n, k holds (S . n) = (S . (n + k))

    proof

      let RNS be non empty 1-sorted;

      let S be sequence of RNS;

      assume

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

      let n;

      defpred P[ Nat] means (S . n) = (S . (n + $1));

       A2:

      now

        let k such that

         A3: P[k];

        (S . (n + k)) = (S . ((n + k) + 1)) by A1;

        hence P[(k + 1)] by A3;

      end;

      

       A4: P[ 0 ];

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

    end;

    theorem :: NORMSP_1:17

    for RNS be non empty 1-sorted, S be sequence of RNS st for n, k holds (S . n) = (S . (n + k)) holds for n, m holds (S . n) = (S . m)

    proof

      let RNS be non empty 1-sorted;

      let S be sequence of RNS;

      assume

       A1: for n, k holds (S . n) = (S . (n + k));

      let n, m;

       A2:

      now

        assume m <= n;

        then

        consider k be Nat such that

         A3: n = (m + k) by NAT_1: 10;

        reconsider k as Nat;

        n = (m + k) by A3;

        hence thesis by A1;

      end;

      now

        assume n <= m;

        then

        consider k be Nat such that

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

        reconsider k as Nat;

        m = (n + k) by A4;

        hence thesis by A1;

      end;

      hence thesis by A2;

    end;

    theorem :: NORMSP_1:18

    for RNS be non empty 1-sorted, S be sequence of RNS st for n, m holds (S . n) = (S . m) holds ex x be Element of RNS st for n be Nat holds (S . n) = x

    proof

      let RNS be non empty 1-sorted;

      let S be sequence of RNS;

      assume that

       A1: for n, m holds (S . n) = (S . m) and

       A2: for x be Element of RNS holds ex n be Nat st (S . n) <> x;

      now

        let n;

        set z = (S . n);

        consider k be Nat such that

         A3: (S . k) <> z by A2;

        thus contradiction by A1, A3;

      end;

      hence thesis;

    end;

    definition

      let RNS be non empty addLoopStr;

      let S1,S2 be sequence of RNS;

      :: NORMSP_1:def2

      func S1 + S2 -> sequence of RNS means

      : Def2: for n holds (it . n) = ((S1 . n) + (S2 . n));

      existence

      proof

        deffunc F( Nat) = ((S1 . $1) + (S2 . $1));

        consider S be sequence of RNS such that

         A1: for n be Element of NAT holds (S . n) = F(n) from FUNCT_2:sch 4;

        take S;

        let n;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let S,T be sequence of RNS;

        assume that

         A2: for n holds (S . n) = ((S1 . n) + (S2 . n)) and

         A3: for n holds (T . n) = ((S1 . n) + (S2 . n));

        for n be Element of NAT holds (S . n) = (T . n)

        proof

          let n be Element of NAT ;

          (S . n) = ((S1 . n) + (S2 . n)) by A2;

          hence thesis by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let RNS be non empty addLoopStr;

      let S1,S2 be sequence of RNS;

      :: NORMSP_1:def3

      func S1 - S2 -> sequence of RNS means

      : Def3: for n holds (it . n) = ((S1 . n) - (S2 . n));

      existence

      proof

        deffunc F( Nat) = ((S1 . $1) - (S2 . $1));

        consider S be sequence of RNS such that

         A1: for n be Element of NAT holds (S . n) = F(n) from FUNCT_2:sch 4;

        take S;

        let n;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let S,T be sequence of RNS;

        assume that

         A2: for n holds (S . n) = ((S1 . n) - (S2 . n)) and

         A3: for n holds (T . n) = ((S1 . n) - (S2 . n));

        for n be Element of NAT holds (S . n) = (T . n)

        proof

          let n be Element of NAT ;

          (S . n) = ((S1 . n) - (S2 . n)) by A2;

          hence thesis by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let RNS be non empty addLoopStr;

      let S be sequence of RNS;

      let x be Element of RNS;

      :: NORMSP_1:def4

      func S - x -> sequence of RNS means

      : Def4: for n holds (it . n) = ((S . n) - x);

      existence

      proof

        deffunc F( Nat) = ((S . $1) - x);

        consider S be sequence of RNS such that

         A1: for n be Element of NAT holds (S . n) = F(n) from FUNCT_2:sch 4;

        take S;

        let n;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let S1,S2 be sequence of RNS;

        assume that

         A2: for n holds (S1 . n) = ((S . n) - x) and

         A3: for n holds (S2 . n) = ((S . n) - x);

        for n be Element of NAT holds (S1 . n) = (S2 . n)

        proof

          let n be Element of NAT ;

          (S1 . n) = ((S . n) - x) by A2;

          hence thesis by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let RNS be non empty RLSStruct;

      let S be sequence of RNS;

      let a be Real;

      :: NORMSP_1:def5

      func a * S -> sequence of RNS means

      : Def5: for n holds (it . n) = (a * (S . n));

      existence

      proof

        deffunc F( Nat) = (a * (S . $1));

        consider S be sequence of RNS such that

         A1: for n be Element of NAT holds (S . n) = F(n) from FUNCT_2:sch 4;

        take S;

        let n;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let S1,S2 be sequence of RNS;

        assume that

         A2: for n holds (S1 . n) = (a * (S . n)) and

         A3: for n holds (S2 . n) = (a * (S . n));

        for n be Element of NAT holds (S1 . n) = (S2 . n)

        proof

          let n be Element of NAT ;

          (S1 . n) = (a * (S . n)) by A2;

          hence thesis by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let RNS, S;

      :: NORMSP_1:def6

      attr S is convergent means ex g st for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - g).|| < r;

    end

    theorem :: NORMSP_1:19

    

     Th19: S1 is convergent & S2 is convergent implies (S1 + S2) is convergent

    proof

      assume that

       A1: S1 is convergent and

       A2: S2 is convergent;

      consider g1 such that

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

      consider g2 such that

       A4: for r st 0 < r holds ex m st for n st m <= n holds ||.((S2 . n) - g2).|| < r by A2;

      take g = (g1 + g2);

      let r;

      assume

       A5: 0 < r;

      then

      consider m1 such that

       A6: for n st m1 <= n holds ||.((S1 . n) - g1).|| < (r / 2) by A3;

      consider m2 such that

       A7: for n st m2 <= n holds ||.((S2 . n) - g2).|| < (r / 2) by A4, A5;

      take k = (m1 + m2);

      let n such that

       A8: k <= n;

      m2 <= k by NAT_1: 12;

      then m2 <= n by A8, XXREAL_0: 2;

      then

       A9: ||.((S2 . n) - g2).|| < (r / 2) by A7;

      

       A10: ||.(((S1 + S2) . n) - g).|| = ||.(( - (g1 + g2)) + ((S1 . n) + (S2 . n))).|| by Def2

      .= ||.((( - g1) + ( - g2)) + ((S1 . n) + (S2 . n))).|| by RLVECT_1: 31

      .= ||.(((S1 . n) + (( - g1) + ( - g2))) + (S2 . n)).|| by RLVECT_1:def 3

      .= ||.((((S1 . n) - g1) + ( - g2)) + (S2 . n)).|| by RLVECT_1:def 3

      .= ||.(((S1 . n) - g1) + ((S2 . n) - g2)).|| by RLVECT_1:def 3;

      

       A11: ||.(((S1 . n) - g1) + ((S2 . n) - g2)).|| <= ( ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).||) by Def1;

      m1 <= (m1 + m2) by NAT_1: 12;

      then m1 <= n by A8, XXREAL_0: 2;

      then ||.((S1 . n) - g1).|| < (r / 2) by A6;

      then ( ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).||) < ((r / 2) + (r / 2)) by A9, XREAL_1: 8;

      hence thesis by A10, A11, XXREAL_0: 2;

    end;

    theorem :: NORMSP_1:20

    

     Th20: S1 is convergent & S2 is convergent implies (S1 - S2) is convergent

    proof

      assume that

       A1: S1 is convergent and

       A2: S2 is convergent;

      consider g1 such that

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

      consider g2 such that

       A4: for r st 0 < r holds ex m st for n st m <= n holds ||.((S2 . n) - g2).|| < r by A2;

      take g = (g1 - g2);

      let r;

      assume

       A5: 0 < r;

      then

      consider m1 such that

       A6: for n st m1 <= n holds ||.((S1 . n) - g1).|| < (r / 2) by A3;

      consider m2 such that

       A7: for n st m2 <= n holds ||.((S2 . n) - g2).|| < (r / 2) by A4, A5;

      take k = (m1 + m2);

      let n such that

       A8: k <= n;

      m2 <= k by NAT_1: 12;

      then m2 <= n by A8, XXREAL_0: 2;

      then

       A9: ||.((S2 . n) - g2).|| < (r / 2) by A7;

      

       A10: ||.(((S1 - S2) . n) - g).|| = ||.(((S1 . n) - (S2 . n)) - (g1 - g2)).|| by Def3

      .= ||.((((S1 . n) - (S2 . n)) - g1) + g2).|| by RLVECT_1: 29

      .= ||.(((S1 . n) - (g1 + (S2 . n))) + g2).|| by RLVECT_1: 27

      .= ||.((((S1 . n) - g1) - (S2 . n)) + g2).|| by RLVECT_1: 27

      .= ||.(((S1 . n) - g1) - ((S2 . n) - g2)).|| by RLVECT_1: 29;

      

       A11: ||.(((S1 . n) - g1) - ((S2 . n) - g2)).|| <= ( ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).||) by Th3;

      m1 <= (m1 + m2) by NAT_1: 12;

      then m1 <= n by A8, XXREAL_0: 2;

      then ||.((S1 . n) - g1).|| < (r / 2) by A6;

      then ( ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).||) < ((r / 2) + (r / 2)) by A9, XREAL_1: 8;

      hence thesis by A10, A11, XXREAL_0: 2;

    end;

    theorem :: NORMSP_1:21

    

     Th21: S is convergent implies (S - x) is convergent

    proof

      assume S is convergent;

      then

      consider g such that

       A1: for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - g).|| < r;

      take h = (g - x);

      let r;

      assume 0 < r;

      then

      consider m1 such that

       A2: for n st m1 <= n holds ||.((S . n) - g).|| < r by A1;

      take k = m1;

      let n;

      assume k <= n;

      then

       A3: ||.((S . n) - g).|| < r by A2;

       ||.((S . n) - g).|| = ||.(((S . n) - 09(RNS)) - g).||

      .= ||.(((S . n) - (x - x)) - g).|| by RLVECT_1: 15

      .= ||.((((S . n) - x) + x) - g).|| by RLVECT_1: 29

      .= ||.(((S . n) - x) + (( - g) + x)).|| by RLVECT_1:def 3

      .= ||.(((S . n) - x) - h).|| by RLVECT_1: 33;

      hence thesis by A3, Def4;

    end;

    theorem :: NORMSP_1:22

    

     Th22: S is convergent implies (a * S) is convergent

    proof

      assume S is convergent;

      then

      consider g such that

       A1: for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - g).|| < r;

      take h = (a * g);

       A2:

      now

        assume

         A3: a <> 0 ;

        then

         A4: 0 < |.a.| by COMPLEX1: 47;

        let r;

        assume 0 < r;

        then

        consider m1 such that

         A5: for n st m1 <= n holds ||.((S . n) - g).|| < (r / |.a.|) by A1, A4;

        take k = m1;

        let n;

        assume k <= n;

        then

         A6: ||.((S . n) - g).|| < (r / |.a.|) by A5;

        

         A7: 0 <> |.a.| by A3, COMPLEX1: 47;

        

         A8: ( |.a.| * (r / |.a.|)) = ( |.a.| * (( |.a.| " ) * r)) by XCMPLX_0:def 9

        .= (( |.a.| * ( |.a.| " )) * r)

        .= (1 * r) by A7, XCMPLX_0:def 7

        .= r;

         ||.((a * (S . n)) - (a * g)).|| = ||.(a * ((S . n) - g)).|| by RLVECT_1: 34

        .= ( |.a.| * ||.((S . n) - g).||) by Def1;

        then ||.((a * (S . n)) - h).|| < r by A4, A6, A8, XREAL_1: 68;

        hence ||.(((a * S) . n) - h).|| < r by Def5;

      end;

      now

        assume

         A9: a = 0 ;

        let r;

        assume 0 < r;

        then

        consider m1 such that

         A10: for n st m1 <= n holds ||.((S . n) - g).|| < r by A1;

        take k = m1;

        let n;

        assume k <= n;

        then

         A11: ||.((S . n) - g).|| < r by A10;

         ||.((a * (S . n)) - (a * g)).|| = ||.(( 0 * (S . n)) - 09(RNS)).|| by A9, RLVECT_1: 10

        .= ||.( 09(RNS) - 09(RNS)).|| by RLVECT_1: 10

        .= ||. 09(RNS).||

        .= 0 ;

        then ||.((a * (S . n)) - h).|| < r by A11;

        hence ||.(((a * S) . n) - h).|| < r by Def5;

      end;

      hence thesis by A2;

    end;

    theorem :: NORMSP_1:23

    

     Th23: S is convergent implies ||.S.|| is convergent

    proof

      assume S is convergent;

      then

      consider g such that

       A1: for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - g).|| < r;

      now

        let r be Real;

        assume

         A2: 0 < r;

        consider m1 such that

         A3: for n st m1 <= n holds ||.((S . n) - g).|| < r by A1, A2;

        reconsider k = m1 as Nat;

        take k;

        now

          let n be Nat;

          assume

           A4: k <= n;

          reconsider nn = n as Nat;

          

           A5: ||.((S . nn) - g).|| < r by A3, A4;

           |.( ||.(S . nn).|| - ||.g.||).| <= ||.((S . nn) - g).|| by Th9;

          then |.( ||.(S . nn).|| - ||.g.||).| < r by A5, XXREAL_0: 2;

          hence |.(( ||.S.|| . n) qua Real - ||.g.||).| < r by NORMSP_0:def 4;

        end;

        hence for n be Nat st k <= n holds |.(( ||.S.|| . n) - ||.g.||).| < r;

      end;

      hence thesis by SEQ_2:def 6;

    end;

    definition

      let RNS, S;

      assume

       A1: S is convergent;

      :: NORMSP_1:def7

      func lim S -> Point of RNS means

      : Def7: for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - it ).|| < r;

      existence by A1;

      uniqueness

      proof

        for x, y st (for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - x).|| < r) & (for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - y).|| < r) holds x = y

        proof

          given x, y such that

           A2: for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - x).|| < r and

           A3: for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - y).|| < r and

           A4: x <> y;

          

           A5: ||.(x - y).|| <> 0 by A4, Th6;

          then

           A6: ( 0 / 4) < ( ||.(x - y).|| / 4);

          then

          consider m1 such that

           A7: for n st m1 <= n holds ||.((S . n) - x).|| < ( ||.(x - y).|| / 4) by A2;

          consider m2 such that

           A8: for n st m2 <= n holds ||.((S . n) - y).|| < ( ||.(x - y).|| / 4) by A3, A6;

           A9:

          now

             ||.(x - y).|| <= ( ||.(x - (S . m1)).|| + ||.((S . m1) - y).||) by Th10;

            then

             A10: ||.(x - y).|| <= ( ||.((S . m1) - x).|| + ||.((S . m1) - y).||) by Th7;

            assume m2 <= m1;

            then

             A11: ||.((S . m1) - y).|| < ( ||.(x - y).|| / 4) by A8;

             ||.((S . m1) - x).|| < ( ||.(x - y).|| / 4) by A7;

            then ( ||.((S . m1) - x).|| + ||.((S . m1) - y).||) < (( ||.(x - y).|| / 4) + ( ||.(x - y).|| / 4)) by A11, XREAL_1: 8;

            then not ( ||.(x - y).|| / 2) < ||.(x - y).|| by A10, XXREAL_0: 2;

            hence contradiction by A5, XREAL_1: 216;

          end;

          now

             ||.(x - y).|| <= ( ||.(x - (S . m2)).|| + ||.((S . m2) - y).||) by Th10;

            then

             A12: ||.(x - y).|| <= ( ||.((S . m2) - x).|| + ||.((S . m2) - y).||) by Th7;

            assume m1 <= m2;

            then

             A13: ||.((S . m2) - x).|| < ( ||.(x - y).|| / 4) by A7;

             ||.((S . m2) - y).|| < ( ||.(x - y).|| / 4) by A8;

            then ( ||.((S . m2) - x).|| + ||.((S . m2) - y).||) < (( ||.(x - y).|| / 4) + ( ||.(x - y).|| / 4)) by A13, XREAL_1: 8;

            then not ( ||.(x - y).|| / 2) < ||.(x - y).|| by A12, XXREAL_0: 2;

            hence contradiction by A5, XREAL_1: 216;

          end;

          hence contradiction by A9;

        end;

        hence thesis;

      end;

    end

    theorem :: NORMSP_1:24

    S is convergent & ( lim S) = g implies ||.(S - g).|| is convergent & ( lim ||.(S - g).||) = 0

    proof

      assume that

       A1: S is convergent and

       A2: ( lim S) = g;

       A3:

      now

        let r be Real;

        assume

         A4: 0 < r;

        consider m1 such that

         A5: for n st m1 <= n holds ||.((S . n) - g).|| < r by A1, A2, A4, Def7;

        reconsider k = m1 as Nat;

        take k;

        let n be Nat;

        assume

         A6: k <= n;

        reconsider nn = n as Nat;

         ||.((S . nn) - g).|| < r by A5, A6;

        then

         A7: ||.(((S . nn) - g) - 09(RNS)).|| < r;

         |.( ||.((S . nn) - g).|| - ||. 09(RNS).||).| <= ||.(((S . nn) - g) - 09(RNS)).|| by Th9;

        then |.( ||.((S . nn) - g).|| - ||. 09(RNS).||).| < r by A7, XXREAL_0: 2;

        then |.( ||.((S - g) . nn).|| - 0 ).| < r by Def4;

        hence |.(( ||.(S - g).|| . n) - 0 ).| < r by NORMSP_0:def 4;

      end;

       ||.(S - g).|| is convergent by A1, Th21, Th23;

      hence thesis by A3, SEQ_2:def 7;

    end;

    theorem :: NORMSP_1:25

    S1 is convergent & S2 is convergent implies ( lim (S1 + S2)) = (( lim S1) + ( lim S2))

    proof

      assume that

       A1: S1 is convergent and

       A2: S2 is convergent;

      set g2 = ( lim S2);

      set g1 = ( lim S1);

      set g = (g1 + g2);

       A3:

      now

        let r;

        assume 0 < r;

        then

         A4: 0 < (r / 2);

        then

        consider m1 such that

         A5: for n st m1 <= n holds ||.((S1 . n) - g1).|| < (r / 2) by A1, Def7;

        consider m2 such that

         A6: for n st m2 <= n holds ||.((S2 . n) - g2).|| < (r / 2) by A2, A4, Def7;

        take k = (m1 + m2);

        let n such that

         A7: k <= n;

        m2 <= k by NAT_1: 12;

        then m2 <= n by A7, XXREAL_0: 2;

        then

         A8: ||.((S2 . n) - g2).|| < (r / 2) by A6;

        

         A9: ||.(((S1 + S2) . n) - g).|| = ||.(( - (g1 + g2)) + ((S1 . n) + (S2 . n))).|| by Def2

        .= ||.((( - g1) + ( - g2)) + ((S1 . n) + (S2 . n))).|| by RLVECT_1: 31

        .= ||.(((S1 . n) + (( - g1) + ( - g2))) + (S2 . n)).|| by RLVECT_1:def 3

        .= ||.((((S1 . n) - g1) + ( - g2)) + (S2 . n)).|| by RLVECT_1:def 3

        .= ||.(((S1 . n) - g1) + ((S2 . n) - g2)).|| by RLVECT_1:def 3;

        

         A10: ||.(((S1 . n) - g1) + ((S2 . n) - g2)).|| <= ( ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).||) by Def1;

        m1 <= (m1 + m2) by NAT_1: 12;

        then m1 <= n by A7, XXREAL_0: 2;

        then ||.((S1 . n) - g1).|| < (r / 2) by A5;

        then ( ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).||) < ((r / 2) + (r / 2)) by A8, XREAL_1: 8;

        hence ||.(((S1 + S2) . n) - g).|| < r by A9, A10, XXREAL_0: 2;

      end;

      (S1 + S2) is convergent by A1, A2, Th19;

      hence thesis by A3, Def7;

    end;

    theorem :: NORMSP_1:26

    S1 is convergent & S2 is convergent implies ( lim (S1 - S2)) = (( lim S1) - ( lim S2))

    proof

      assume that

       A1: S1 is convergent and

       A2: S2 is convergent;

      set g2 = ( lim S2);

      set g1 = ( lim S1);

      set g = (g1 - g2);

       A3:

      now

        let r;

        assume 0 < r;

        then

         A4: 0 < (r / 2);

        then

        consider m1 such that

         A5: for n st m1 <= n holds ||.((S1 . n) - g1).|| < (r / 2) by A1, Def7;

        consider m2 such that

         A6: for n st m2 <= n holds ||.((S2 . n) - g2).|| < (r / 2) by A2, A4, Def7;

        take k = (m1 + m2);

        let n such that

         A7: k <= n;

        m2 <= k by NAT_1: 12;

        then m2 <= n by A7, XXREAL_0: 2;

        then

         A8: ||.((S2 . n) - g2).|| < (r / 2) by A6;

        

         A9: ||.(((S1 - S2) . n) - g).|| = ||.(((S1 . n) - (S2 . n)) - (g1 - g2)).|| by Def3

        .= ||.((((S1 . n) - (S2 . n)) - g1) + g2).|| by RLVECT_1: 29

        .= ||.(((S1 . n) - (g1 + (S2 . n))) + g2).|| by RLVECT_1: 27

        .= ||.((((S1 . n) - g1) - (S2 . n)) + g2).|| by RLVECT_1: 27

        .= ||.(((S1 . n) - g1) - ((S2 . n) - g2)).|| by RLVECT_1: 29;

        

         A10: ||.(((S1 . n) - g1) - ((S2 . n) - g2)).|| <= ( ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).||) by Th3;

        m1 <= (m1 + m2) by NAT_1: 12;

        then m1 <= n by A7, XXREAL_0: 2;

        then ||.((S1 . n) - g1).|| < (r / 2) by A5;

        then ( ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).||) < ((r / 2) + (r / 2)) by A8, XREAL_1: 8;

        hence ||.(((S1 - S2) . n) - g).|| < r by A9, A10, XXREAL_0: 2;

      end;

      (S1 - S2) is convergent by A1, A2, Th20;

      hence thesis by A3, Def7;

    end;

    theorem :: NORMSP_1:27

    S is convergent implies ( lim (S - x)) = (( lim S) - x)

    proof

      set g = ( lim S);

      set h = (g - x);

      assume

       A1: S is convergent;

       A2:

      now

        let r;

        assume 0 < r;

        then

        consider m1 such that

         A3: for n st m1 <= n holds ||.((S . n) - g).|| < r by A1, Def7;

        take k = m1;

        let n;

        assume k <= n;

        then

         A4: ||.((S . n) - g).|| < r by A3;

         ||.((S . n) - g).|| = ||.(((S . n) - 09(RNS)) - g).||

        .= ||.(((S . n) - (x - x)) - g).|| by RLVECT_1: 15

        .= ||.((((S . n) - x) + x) - g).|| by RLVECT_1: 29

        .= ||.(((S . n) - x) + (( - g) + x)).|| by RLVECT_1:def 3

        .= ||.(((S . n) - x) - h).|| by RLVECT_1: 33;

        hence ||.(((S - x) . n) - h).|| < r by A4, Def4;

      end;

      (S - x) is convergent by A1, Th21;

      hence thesis by A2, Def7;

    end;

    theorem :: NORMSP_1:28

    S is convergent implies ( lim (a * S)) = (a * ( lim S))

    proof

      set g = ( lim S);

      set h = (a * g);

      assume

       A1: S is convergent;

       A2:

      now

        assume

         A3: a = 0 ;

        let r;

        assume 0 < r;

        then

        consider m1 such that

         A4: for n st m1 <= n holds ||.((S . n) - g).|| < r by A1, Def7;

        take k = m1;

        let n;

        assume k <= n;

        then

         A5: ||.((S . n) - g).|| < r by A4;

         ||.((a * (S . n)) - (a * g)).|| = ||.(( 0 * (S . n)) - 09(RNS)).|| by A3, RLVECT_1: 10

        .= ||.( 09(RNS) - 09(RNS)).|| by RLVECT_1: 10

        .= ||. 09(RNS).||

        .= 0 ;

        then ||.((a * (S . n)) - h).|| < r by A5;

        hence ||.(((a * S) . n) - h).|| < r by Def5;

      end;

       A6:

      now

        assume

         A7: a <> 0 ;

        then

         A8: 0 < |.a.| by COMPLEX1: 47;

        let r;

        assume 0 < r;

        then 0 < (r / |.a.|) by A8;

        then

        consider m1 such that

         A9: for n st m1 <= n holds ||.((S . n) - g).|| < (r / |.a.|) by A1, Def7;

        take k = m1;

        let n;

        assume k <= n;

        then

         A10: ||.((S . n) - g).|| < (r / |.a.|) by A9;

        

         A11: 0 <> |.a.| by A7, COMPLEX1: 47;

        

         A12: ( |.a.| * (r / |.a.|)) = ( |.a.| * (( |.a.| " ) * r)) by XCMPLX_0:def 9

        .= (( |.a.| * ( |.a.| " )) * r)

        .= (1 * r) by A11, XCMPLX_0:def 7

        .= r;

         ||.((a * (S . n)) - (a * g)).|| = ||.(a * ((S . n) - g)).|| by RLVECT_1: 34

        .= ( |.a.| * ||.((S . n) - g).||) by Def1;

        then ||.((a * (S . n)) - h).|| < r by A8, A10, A12, XREAL_1: 68;

        hence ||.(((a * S) . n) - h).|| < r by Def5;

      end;

      (a * S) is convergent by A1, Th22;

      hence thesis by A2, A6, Def7;

    end;