The Mizar article:

Real Normed Space

by
Jan Popiolek

Received September 20, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: NORMSP_1
[ MML identifier index ]


environ

 vocabulary RLVECT_1, BINOP_1, FUNCT_1, PRE_TOPC, RLSUB_1, ABSVALUE, ARYTM_1,
      ARYTM_3, RELAT_1, SEQM_3, SEQ_2, SEQ_1, ORDINAL2, NORMSP_1, ARYTM;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0,
      REAL_1, NAT_1, FUNCT_1, FUNCT_2, BINOP_1, RELAT_1, SEQ_1, SEQ_2, SEQM_3,
      ABSVALUE, STRUCT_0, PRE_TOPC, RLVECT_1, RLSUB_1;
 constructors REAL_1, NAT_1, DOMAIN_1, SEQ_2, SEQM_3, ABSVALUE, RLSUB_1,
      MEMBERED, XBOOLE_0;
 clusters STRUCT_0, XREAL_0, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0,
      NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions RLVECT_1, SEQM_3, STRUCT_0;
 theorems TARSKI, AXIOMS, REAL_1, NAT_1, FUNCT_1, SQUARE_1, SEQ_2, ABSVALUE,
      RLVECT_1, RLSUB_1, FUNCT_2, SEQM_3, STRUCT_0, RELSET_1, XREAL_0,
      XBOOLE_0, XCMPLX_0, XCMPLX_1;
 schemes FUNCT_1, FUNCT_2, SEQ_1, NAT_1;

begin

definition
 struct(RLSStruct) NORMSTR (# carrier -> set,
                 Zero -> Element of the carrier,
                  add -> BinOp of the carrier,
                 Mult -> Function of [:REAL, the carrier:], the carrier,
                 norm -> Function of the carrier, REAL #);
end;

definition
 cluster non empty NORMSTR;
 existence
  proof
    consider A being non empty set, Z being Element of A,
             a being BinOp of A, M being Function of [:REAL,A:],A,
             n being Function of A,REAL;
   take NORMSTR(#A,Z,a,M,n#);
   thus the carrier of NORMSTR(#A,Z,a,M,n#) is non empty;
  end;
end;

 reserve X for non empty NORMSTR;
 reserve a, b for Real;
 reserve x for Point of X;

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

definition let X, x;
          func ||.x.|| -> Real equals
:Def1:   ( the norm of X ).x;
coherence;
end;
     consider V being RealLinearSpace;
Lm1:   the carrier of (0).V = {0.V} by RLSUB_1:def 3;
  deffunc F(set) = 0;
     consider nil_to_nil being Function
     of the carrier of (0).V , REAL such that
Lm2: for u being VECTOR of (0).V holds nil_to_nil.u = F(u) from LambdaD;

Lm3:
nil_to_nil.(0.V) = 0
proof
  0.V is VECTOR of (0).V by Lm1,TARSKI:def 1;
hence thesis by Lm2;
end;

Lm4:
for u being VECTOR of (0).V , a holds
nil_to_nil.(a * u) = abs(a) * nil_to_nil.u
proof
let u be VECTOR of (0).V;
let a;
  nil_to_nil.u = 0 by Lm1,Lm3,TARSKI:def 1;
hence thesis by Lm1,Lm3,TARSKI:def 1;
end;

Lm5:
for u , v being VECTOR of (0).V holds
nil_to_nil.(u + v) <= nil_to_nil.u + nil_to_nil.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,Lm3,TARSKI:def 1;
end;
reconsider X =
 NORMSTR (# the carrier of (0).V, the Zero of (0).V, the add of (0).V,
           the Mult of (0).V, nil_to_nil #)
            as non empty NORMSTR by STRUCT_0:def 1;

Lm6:
now
let x, y be Point of X;
let a;
A1:   ||.x.|| = nil_to_nil.x &
||.y.|| = nil_to_nil.y &
||.a * x.|| = nil_to_nil.(a * x) &
||.x + y.|| = nil_to_nil.(x + y) by Def1;

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

thus ||.x.|| = 0 iff x = 0'(X)
proof
  0'(X) = the Zero of X by RLVECT_1:def 2
     .= 0.(0).V by RLVECT_1:def 2
     .= 0.V by RLSUB_1:19;
hence thesis by Def1,Lm1,Lm3,TARSKI:def 1;
end;

   a * x = (the Mult of X).[a,u] by RLVECT_1:def 4
         .= a * u by RLVECT_1:def 4;
hence ||.a * x.|| = abs(a) * ||.x.|| by A1,Lm4;
   x + y = (the add of X).[x,y] by RLVECT_1:def 3
      .= u + w by RLVECT_1:def 3;
hence ||.x + y.|| <= ||.x.|| + ||.y.|| by A1,Lm5;
end;

definition let IT be non empty NORMSTR;
          attr IT is RealNormSpace-like means
:Def2:   for x , y being Point of IT , a holds
          ( ||.x.|| = 0 iff x = 0.IT ) &
          ||.a * x.|| = abs(a) * ||.x.|| &
          ||.x + y.|| <= ||.x.|| + ||.y.||;
end;

definition
 cluster RealNormSpace-like RealLinearSpace-like Abelian
    add-associative right_zeroed right_complementable strict
      (non empty NORMSTR);
  existence
   proof
    take X;
    thus X is RealNormSpace-like by Def2,Lm6;
A1: now
      let x,y be VECTOR of X;
      let x',y' be VECTOR of (0).V;
      assume A2: x = x' & y = y';
      hence x + y= (the add of X).[x',y'] by RLVECT_1:def 3 .=
      x' + y' by RLVECT_1:def 3;
      let a;
      thus a * x = (the Mult of X).[a,x'] by A2,RLVECT_1:def 4 .=
      a * x' by RLVECT_1:def 4;
     end;
A3:  0.X = the Zero of X by RLVECT_1:def 2 .=
     0.(0).V by RLVECT_1:def 2;
    thus X is RealLinearSpace-like
    proof
     thus for a for v,w being VECTOR of X holds a * (v + w) = a * v + a * w
     proof
      let a;
      let v,w be VECTOR of X;
      reconsider v'= v, w' = w as VECTOR of (0).V;
A4:   a * v' = a * v by A1;
A5:  a * w' = a * w by A1;
    v + w = v'+ w' by A1;
      hence a * (v + w) = a *( v' + w') by A1 .=
      a * v' + a * w' by RLVECT_1:def 9 .= a * v + a * w by A1,A4,A5;
     end;
     thus for a,b for v being VECTOR of X holds (a + b) * v = a * v + b * v
     proof
      let a,b;
      let v be VECTOR of X;
      reconsider v'= v as VECTOR of (0).V;
A6:   a * v' = a * v by A1;
A7:  b * v' = b * v by A1;
      thus (a + b) * v = (a + b) * v' by A1 .=
      a * v' + b * v' by RLVECT_1:def 9 .= a * v + b * v by A1,A6,A7;
     end;
     thus for a,b for v being VECTOR of X holds (a * b) * v = a * (b * v)
     proof
      let a,b;
      let v be VECTOR of X;
      reconsider v'= v as VECTOR of (0).V;
A8:   b * v' = b * v by A1;
      thus (a * b) * v = (a * b) * v' by A1
                .= a * (b * v') by RLVECT_1:def 9
                .= a * (b * v) by A1,A8;
     end;
     let v be VECTOR of X;
     reconsider v'= v as VECTOR of (0).V;
     thus 1 * v = 1 * v' by A1 .= v by RLVECT_1:def 9;
    end;
    thus for v,w being VECTOR of X holds v + w = w + v
    proof
     let v,w be VECTOR of X;
     reconsider v'= v , w'= w as VECTOR of (0).V;
     thus v + w = w'+ v' by A1 .= w + v by A1;
    end;
     thus for u,v,w being VECTOR of X holds (u + v) + w = u + (v + w)
     proof
      let u,v,w be VECTOR of X;
      reconsider u'= u, v'= v, w'= w as VECTOR of (0).V;
      A9: u + v = u'+ v' by A1;
      A10: v + w = v' + w' by A1;
      thus (u + v) + w = (u' + v') + w' by A1,A9 .=
      u' + (v' + w') by RLVECT_1:def 6 .= u + (v + w) by A1,A10;
     end;
     thus for v being VECTOR of X holds v + 0.X = v
     proof
      let v be VECTOR of X;
      reconsider v'= v as VECTOR of (0).V;
      thus v + 0.X = v'+ 0.(0).V by A1,A3 .=v by RLVECT_1:10;
     end;
     thus for v being VECTOR of X
       ex w being VECTOR of X st v + w = 0.X
       proof
        let v be VECTOR of X;
        reconsider v'= v as VECTOR of (0).V;
        consider w' be VECTOR of (0).V such that
        A11: v' + w' = 0.(0).V by RLVECT_1:def 8;
        reconsider w = w' as VECTOR of X;
        take w;
        thus v + w = 0.X by A1,A3,A11;
       end;
    thus thesis;
   end;
end;

definition
 mode RealNormSpace is RealNormSpace-like RealLinearSpace-like
      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;

canceled 4;

theorem
     ||.0.RNS.|| = 0 by Def2;

theorem Th6:
    ||.-x.|| = ||.x.||
proof
A1:   ||.-x.|| = ||.(-1) * x.|| by RLVECT_1:29
           .= abs(-1 ) * ||.x.|| by Def2;
       abs(-1 ) = -(-1) by ABSVALUE:def 1
           .= 1;
     hence thesis by A1;
end;

theorem Th7:
    ||.x - y.|| <= ||.x.|| + ||.y.||
proof
       x - y = x + (-y) by RLVECT_1:def 11;
     then ||.x - y.|| <= ||.x.|| + ||.(-y).|| by Def2;
     hence thesis by Th6;
end;

theorem Th8:
    0 <= ||.x.||
proof
       ||.x - x.|| = ||.0'(RNS).|| by RLVECT_1:28
              .= 0 by Def2;
   then 0 <= ||.x.|| + ||.x.|| by Th7;
     then 0 <= (||.x.|| + ||.x.||)/2 by SQUARE_1:27;
     hence thesis by XCMPLX_1:65;
end;

theorem
      ||.a * x + b * y.|| <= abs(a) * ||.x.|| + abs(b) * ||.y.||
proof
       ||.a * x + b * y.|| <= ||.a * x.|| + ||.b * y.|| by Def2;
     then ||.a * x + b * y.|| <= abs(a) * ||.x.|| + ||.b * y.|| by Def2;
     hence thesis by Def2;
end;

theorem Th10:
     ||.x - y.|| = 0 iff x = y
proof
     ||.x - y.|| = 0 iff x - y = 0'(RNS) by Def2;
     hence thesis by RLVECT_1:28,35;
end;

theorem Th11:
     ||.x - y.|| = ||.y - x.||
proof
       x - y = (-y) + x by RLVECT_1:def 11
          .= - (y - x) by RLVECT_1:47;
    hence thesis by Th6;
end;

theorem Th12:
     ||.x.|| - ||.y.|| <= ||.x - y.||
proof
       (x - y) + y = x - (y - y) by RLVECT_1:43
                .= x - 0'(RNS) by RLVECT_1:28
                .= x by RLVECT_1:26;
     then ||.x.|| <= ||.x - y.|| + ||.y.|| by Def2;
     hence thesis by REAL_1:86;
end;

theorem Th13:
     abs(||.x.|| - ||.y.||) <= ||.x - y.||
proof
A1:   ||.x.|| - ||.y.|| <= ||.x - y.|| by Th12;
       (y - x) + x = y - (x - x) by RLVECT_1:43
                .= y - 0'(RNS) by RLVECT_1:28
                .= y by RLVECT_1:26;
     then ||.y.|| <= ||.y - x.|| + ||.x.|| by Def2;
     then ||.y.|| - ||.x.|| <= ||.y - x.|| by REAL_1:86;
     then ||.y.|| - ||.x.|| <= ||.x - y.|| by Th11;
     then -(||.x.|| - ||.y.||) <= ||.x - y.|| by XCMPLX_1:143;
     then -||.x - y.|| <= -(-(||.x.|| - ||.y.||)) by REAL_1:50;
     hence thesis by A1,ABSVALUE:12;
end;

theorem Th14:
     ||.x - z.|| <= ||.x - y.|| + ||.y - z.||
proof
       x - z = x + (-z) by RLVECT_1:def 11
          .= x + (0'(RNS) + (-z)) by RLVECT_1:10
          .= x + (((-y) + y) + (-z)) by RLVECT_1:16
          .= x + ((-y) + (y + (-z))) by RLVECT_1:def 6
          .= (x + (-y)) + (y + (-z)) by RLVECT_1:def 6
          .= (x - y) + (y + (-z)) by RLVECT_1:def 11
          .= (x - y) + (y - z) by RLVECT_1:def 11;
     hence thesis by Def2;
end;

theorem
      x <> y implies ||.x - y.|| <> 0 by Th10;

definition let RNS be 1-sorted;
          mode sequence of RNS means
:Def3:   it is Function of NAT, the carrier of RNS;
existence
         proof consider f being Function of NAT, the carrier of RNS;
          take f;
          thus thesis;
         end;
end;

definition let RNS be 1-sorted;
 cluster -> Function-like Relation-like sequence of RNS;
 coherence by Def3;
end;

definition let RNS be non empty 1-sorted;
 redefine mode sequence of RNS -> Function of NAT, the carrier of RNS;
 coherence by Def3;
end;

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;

canceled;

theorem Th17:
 for RNS being non empty 1-sorted, x being 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: dom f = NAT by FUNCT_2:def 1;
      A3: rng f c= the carrier of RNS by A1,RELSET_1:12;
            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 A2,FUNCT_1:def 5;
               hence thesis by A3;
          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 st s in rng f holds
          s in the carrier of RNS
          proof
               let s; assume
              s in rng f;
               then consider d such that
          A6:  d in dom f and
          A7:  s = f.d by FUNCT_1:def 5;
                 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;
          then f is Function of NAT, the carrier of RNS by A4,FUNCT_2:def 1,
RELSET_1:11;
          hence thesis by Def3;
     end;
end;

canceled;

theorem Th19:
 for RNS being non empty 1-sorted, x being Element of RNS
       ex S being 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:15;
      f is Function of NAT, the carrier of RNS by A1,A2,FUNCT_2:def 1,RELSET_1:
11
;
    then reconsider f as sequence of RNS by Def3;
    take f;
    thus thesis by A2;
end;

theorem Th20:
 for RNS being non empty 1-sorted, S being sequence of RNS st
     (ex x being Element of RNS st for n holds S.n = x)
      ex x being Element of RNS st rng S={x}
  proof
 let RNS be non empty 1-sorted;
 let S be sequence of RNS;
       given z being Element of RNS such that
   A1:  for n holds S.n = z;
       take x = z;
         now let t; assume t in rng S;
       then consider d such that
   A2: d in dom S and
   A3: S.d = t by FUNCT_1:def 5;
         d in NAT by A2,FUNCT_2:def 1;
       then t = z by A1,A3;
       hence t in {x} by TARSKI:def 1;
       end;
   then A4: rng S c= {x} by TARSKI:def 3;
         now let s; assume
      s in {x};
   then A5:  s = x by TARSKI:def 1;
         now assume
   A6: not s in rng S;
         now let n;
         n in NAT;
       then n in dom S by FUNCT_2:def 1;
       then S.n <> x by A5,A6,FUNCT_1:def 5;
       hence contradiction by A1;
       end;
       hence contradiction;
       end;
       hence s in rng S;
       end;
       then {x} c= rng S by TARSKI:def 3;
       hence thesis by A4,XBOOLE_0:def 10;
    end;

theorem Th21:
 for RNS being non empty 1-sorted, S being sequence of RNS st
     ex x being 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 being Element of RNS such that
 A1:  rng S = {z};
     let n;
       n in NAT & (n+1) in NAT;
     then n in dom S & (n+1) in dom S by FUNCT_2:def 1;
     then S.n in {z} & S.(n+1) in {z} by A1,FUNCT_1:def 5;
     then S.n = z & S.(n+1) = z by TARSKI:def 1;
     hence thesis;
    end;

theorem Th22:
 for RNS being non empty 1-sorted, S being 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:  P[0];
       A3:  now let k such that
       A4:  P[k];
             S.(n+k) = S.(n+k+1) by A1;
           hence P[k+1] by A4,XCMPLX_1:1;
      end;
    thus for k holds P[k] from Ind(A2,A3);
end;

theorem Th23:
 for RNS being non empty 1-sorted, S being 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 n <= m;
           then ex k st m = n + k by NAT_1:28;
           hence S.n = S.m by A1;
           end;
             now assume m <= n;
           then ex k st n = m + k by NAT_1:28;
           hence S.n = S.m by A1;
           end;
     hence thesis by A2;
end;

theorem Th24:
 for RNS being non empty 1-sorted, S being sequence of RNS st
     for n , m holds S.n = S.m
   ex x being Element of RNS st for n 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 being Element of RNS ex n st S.n <> x;
        now let n;
      consider z being Element of RNS such that
 A3:   S.n = z;
         ex k st S.k <> z by A2;
      hence contradiction by A1,A3;
      end;
      hence thesis;
end;

theorem
       ex S st rng S = {0.RNS} by Th19;

definition let RNS be non empty 1-sorted;
          let S be sequence of RNS;
 redefine attr S is constant means :Def4:
   ex x being Element of RNS st for n holds S.n = x;
 compatibility
  proof
A1:   dom S = NAT by FUNCT_2:def 1;
   hereby assume
A2:   S is constant;
    consider n0 being Nat;
    take r = S.n0;
    let n be Nat;
    thus S.n = r by A1,A2,SEQM_3:def 5;
   end;
   given r being Element of RNS such that
A3:  for n holds S.n=r;
   let n1,n2 be set;
   assume
A4:  n1 in dom S & n2 in dom S;
   hence S.n1 = r by A1,A3 .= S.n2 by A1,A3,A4;
  end;
end;

canceled;

theorem
   for RNS being non empty 1-sorted, S being sequence of RNS holds
     S is constant iff ex x being Element of RNS st rng S = {x}
proof
 let RNS be non empty 1-sorted;
 let S be sequence of RNS;
     thus S is constant implies
      ex x being Element of RNS st rng S = {x}
     proof
          assume
            S is constant;
          then ex x being Element of RNS st for n holds S.n = x
           by Def4;
          hence thesis by Th20;
     end;
     assume ex x being Element of RNS st rng S = {x};
          then ( for n holds S.n = S.(n+1) ) by Th21;
          then ( for n , k holds S.n = S.(n+k) ) by Th22;
          then ( for n , m holds S.n = S.m ) by Th23;
          then ( ex x being Element of RNS st for n holds S.n =
x )
             by Th24;
          hence thesis by Def4;
end;

Lm7:
     for RNS being non empty 1-sorted
     for S being sequence of RNS
     for n holds S.n is Element of RNS;

definition let RNS be non empty 1-sorted;
          let S be sequence of RNS;
          let n;
redefine func S.n -> Element of RNS;
coherence by Lm7;
end;

scheme ExRNSSeq{RNS()->RealNormSpace, F(Nat) -> ( Point of RNS() ) } :
       ex S be sequence of RNS() st for n holds S.n = F(n)
       proof
       defpred P[set,set] means ex n st n =$1 & $2 = F(n);
    A1: for d st d in NAT ex s st P[d,s]
       proof
            let d; assume d in NAT;
            then consider n such that
        A2: n = d;
            reconsider z = F(n) as set;
            take z;
            thus thesis by A2;
       end;
    A3: for d , s , t st d in NAT & P[d,s] & P[d,t] holds s = t;
       consider f such that
    A4: dom f = NAT and
    A5: for d st d in NAT holds P[d,f.d] from FuncEx(A3,A1);
         for d st d in NAT holds f.d is Point of RNS()
       proof
            let d; assume d in NAT;
            then ex n st n = d & f.d = F(n) by A5;
            hence thesis;
       end;
       then reconsider f as sequence of RNS() by A4,Th17;
       take S = f;
         now let n;
         P[n,S.n] by A5;
       hence S.n = F(n);
       end;
   hence for n holds S.n = F(n);
end;

scheme ExRLSSeq{RNS()->RealLinearSpace,
                F(Nat) -> Element of RNS() } :
       ex S be sequence of RNS() st for n holds S.n = F(n)
       proof
       defpred P[set,set] means ex n st ( n =$1 & $2 = F(n));
    A1: for d st d in NAT ex s st P[d,s]
       proof
            let d; assume d in NAT;
            then consider n such that
        A2: n = d;
            reconsider z = F(n) as set;
            take z;
            thus thesis by A2;
       end;
    A3: for d , s , t st d in NAT & P[d,s] & P[d,t] holds s = t;
       consider f such that
    A4: dom f = NAT and
    A5: for d st d in NAT holds P[d,f.d] from FuncEx(A3,A1);
         for d st d in NAT holds f.d is Element of RNS()
       proof
            let d; assume d in NAT;
            then ex n st n = d & f.d = F(n) by A5;
            hence thesis;
       end;
       then reconsider f as sequence of RNS() by A4,Th17;
       take S = f;
         now let n;
         P[n,S.n] by A5;
       hence S.n = F(n);
       end;
   hence for n holds S.n = F(n);
end;

definition let RNS be RealLinearSpace;
           let S1, S2 be sequence of RNS;
           func S1 + S2 -> sequence of RNS means
:Def5:     for n holds it.n = S1.n + S2.n;
existence proof
  deffunc F(Nat) = S1.$1 + S2.$1;
  thus ex S being sequence of RNS st for n holds S.n = F(n) from ExRLSSeq;
end;
uniqueness
          proof
               let S, T be sequence of RNS;
               assume that
          A1:  ( for n holds S.n = S1.n + S2.n ) and
          A2:  ( for n holds T.n = S1.n + S2.n );
                 for n holds S.n = T.n
               proof
                    let n;
                   S.n = S1.n + S2.n by A1;
                    hence thesis by A2;
               end;
              hence thesis by FUNCT_2:113;
          end;
end;

definition let RNS be RealLinearSpace;
          let S1 , S2 be sequence of RNS;
          func S1 - S2 -> sequence of RNS means
:Def6:    for n holds it.n = S1.n - S2.n;
existence proof
  deffunc F(Nat) = S1.$1 - S2.$1;
  thus ex S being sequence of RNS st for n holds S.n = F(n) from ExRLSSeq;
end;
uniqueness
          proof
               let S , T be sequence of RNS;
               assume that
          A1:  ( for n holds S.n = S1.n - S2.n ) and
          A2:  ( for n holds T.n = S1.n - S2.n );
                 for n holds S.n = T.n
               proof
                    let n;
                   S.n = S1.n - S2.n by A1;
                    hence thesis by A2;
               end;
              hence thesis by FUNCT_2:113;
          end;
end;

definition let RNS be RealLinearSpace;
          let S be sequence of RNS;
          let x be Element of RNS;
          func S - x -> sequence of RNS means
:Def7:     for n holds it.n = S.n - x;
existence proof
  deffunc F(Nat) = S.$1 - x;
  thus ex S being sequence of RNS st for n holds S.n = F(n) from ExRLSSeq;
end;
uniqueness
          proof
               let S1 , S2 be sequence of RNS;
               assume that
          A1:  ( for n holds S1.n = S.n - x ) and
          A2:  ( for n holds S2.n = S.n - x );
                 for n holds S1.n = S2.n
               proof
                    let n;
                   S1.n = S.n - x by A1;
                    hence thesis by A2;
               end;
              hence thesis by FUNCT_2:113;
          end;
end;

definition let RNS be RealLinearSpace;
          let S be sequence of RNS;
          let a;
          func a * S -> sequence of RNS means
:Def8:     for n holds it.n = a * S.n;
existence proof
  deffunc F(Nat) = a * S.$1;
  thus ex S being sequence of RNS st for n holds S.n = F(n) from ExRLSSeq;
end;
uniqueness
          proof
               let S1 , S2 be sequence of RNS;
               assume that
          A1:  ( for n holds S1.n = a * S.n ) and
          A2:  ( for n holds S2.n = a * S.n );
                 for n holds S1.n = S2.n
               proof
                    let n;
                   S1.n = a * S.n by A1;
                    hence thesis by A2;
               end;
              hence thesis by FUNCT_2:113;
          end;
end;

definition let RNS;
          let S;
          attr S is convergent means
:Def9:    ex g st for r st 0 < r ex m st for n st m <= n holds
          ||.(S.n) - g.|| < r;
end;

canceled 6;

theorem Th34:
     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 ex m st for n st m <= n holds
      ||.(S1.n) - g1.|| < r by A1,Def9;
      consider g2 such that
 A4:  for r st 0 < r ex m st for n st m <= n holds
      ||.(S2.n) - g2.|| < r by A2,Def9;
      take g = g1 + g2;
      let r; assume 0 < r;
 then A5:  0< r/2 by SEQ_2:3;
      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;
        m1 <= m1 + m2 by NAT_1:37;
      then m1 <= n by A8,AXIOMS:22;
  then A9:  ||.(S1.n) - g1.|| < r/2 by A6;
        m2 <= k by NAT_1:37;
      then m2 <= n by A8,AXIOMS:22;
      then ||.(S2.n) - g2.|| < r/2 by A7;
      then ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r/2 + r/2
      by A9,REAL_1:67;
  then A10:  ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r by XCMPLX_1:66;
  A11:  ||.(S1 + S2).n - g.|| = ||.(S1.n) + (S2.n) - (g1+g2).|| by Def5
      .= ||.(S1.n) + ((S2.n) - (g1+g2)).|| by RLVECT_1:42
      .= ||.(S1.n) + (-(g1+g2) + (S2.n)).|| by RLVECT_1:def 11
      .= ||.-(g1+g2) + ((S1.n) + (S2.n)).|| by RLVECT_1:def 6
      .= ||.((-g1)+(-g2)) + ((S1.n) + (S2.n)).|| by RLVECT_1:45
      .= ||.(S1.n) + ((-g1)+(-g2)) + (S2.n).|| by RLVECT_1:def 6
      .= ||.((S1.n) + (-g1)) + (-g2) + (S2.n).|| by RLVECT_1:def 6
      .= ||.(S1.n) - g1 + (-g2) + (S2.n).|| by RLVECT_1:def 11
      .= ||.(S1.n)- g1 + ((S2.n) + -g2).|| by RLVECT_1:def 6
      .= ||.(S1.n) - g1 + ((S2.n) - g2).|| by RLVECT_1:def 11;
        ||.(S1.n) - g1 + ((S2.n) - g2).|| <=
      ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| by Def2;
      hence ||.(S1 + S2).n - g.|| < r by A10,A11,AXIOMS:22;
  end;

theorem Th35:
     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 ex m st for n st m <= n holds
      ||.(S1.n) - g1.|| < r by A1,Def9;
      consider g2 such that
 A4:  for r st 0 < r ex m st for n st m <= n holds
      ||.(S2.n) - g2.|| < r by A2,Def9;
      take g = g1 - g2;
      let r; assume 0 < r;
 then A5:  0< r/2 by SEQ_2:3;
      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;
        m1 <= m1 + m2 by NAT_1:37;
      then m1 <= n by A8,AXIOMS:22;
  then A9:  ||.(S1.n) - g1.|| < r/2 by A6;
        m2 <= k by NAT_1:37;
      then m2 <= n by A8,AXIOMS:22;
      then ||.(S2.n) - g2.|| < r/2 by A7;
      then ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r/2 + r/2
      by A9,REAL_1:67;
  then A10:  ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r by XCMPLX_1:66;
  A11:  ||.(S1 - S2).n - g.|| = ||.((S1.n) - (S2.n)) - (g1 - g2).|| by Def6
      .= ||.(((S1.n) - (S2.n)) - g1) + g2.|| by RLVECT_1:43
      .= ||. ((S1.n) - (g1 + (S2.n))) + g2.|| by RLVECT_1:41
      .= ||. (((S1.n) - g1 ) - (S2.n)) + g2.|| by RLVECT_1:41
      .= ||. ((S1.n) - g1 ) - ((S2.n) - g2).|| by RLVECT_1:43;
        ||.((S1.n) - g1) - ((S2.n) - g2).|| <=
      ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| by Th7;
      hence ||.(S1 - S2).n - g.|| < r by A10,A11,AXIOMS:22;
  end;

theorem Th36:
     S is convergent implies
     S - x is convergent
proof
     assume S is convergent;
           then consider g such that
     A1:    for r st 0 < r ex m st for n
           st m <= n holds ||.(S.n) - g.|| < r by Def9;
           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) - 0'(RNS)) - g.|| by RLVECT_1:26
                        .= ||.((S.n) - (x - x)) - g.|| by RLVECT_1:28
                        .= ||.(((S.n) - x) + x) - g.|| by RLVECT_1:43
                        .= ||.((S.n) - x) + (x - g).|| by RLVECT_1:42
                        .= ||.((S.n) - x) + ((-g) + x).|| by RLVECT_1:def 11
                        .= ||.((S.n) - x) + -h.|| by RLVECT_1:47
                        .= ||.((S.n) - x) - h.|| by RLVECT_1:def 11;
           hence ||.(S - x).n - h.|| < r by A3,Def7;
end;

theorem Th37:
     S is convergent implies
     a * S is convergent
proof
     assume S is convergent;
           then consider g such that
     A1:    for r st 0 < r ex m st for n
           st m <= n holds ||.(S.n) - g.|| < r by Def9;
           take h = a * g;
     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;
           take k = m1;
           let n; assume k <= n;
     then A5:   ||.(S.n) - g.|| < r by A4;
          ||.a * (S.n) - a * g.|| = ||.0 * (S.n) - 0'(RNS).|| by A3,RLVECT_1:23
                        .= ||.0'(RNS) - 0'(RNS).|| by RLVECT_1:23
                        .= ||.0'(RNS).|| by RLVECT_1:26
                        .= 0 by Def2;
           then ||.a * (S.n) - h.|| < r by A5,Th8;
           hence ||.(a * S).n - h.|| < r by Def8;
           end;
             now assume
A6:        a <> 0;
     then A7:   0 < abs(a) by ABSVALUE:6;
           let r such that
     A8:   0 < r;
     A9:   0 <> abs(a) by A6,ABSVALUE:6;
             0/abs(a) =0;
           then 0 < r/abs(a) by A7,A8,REAL_1:73;
           then consider m1 such that
     A10:   for n st m1 <= n holds ||.(S.n) - g.|| < r/abs(a) by A1;
           take k = m1;
           let n; assume k <= n;
     then A11:   ||.(S.n) - g.|| < r/abs(a) by A10;
     A12:   ||.(a * (S.n)) - (a * g).|| = ||.a * ((S.n) - g).|| by RLVECT_1:48
                                    .= abs(a) * ||.(S.n) - g.|| by Def2;
             abs(a) * (r/abs(a)) = abs(a) * (abs(a)" * r) by XCMPLX_0:def 9
                            .= abs(a) *abs(a)" * r by XCMPLX_1:4
                            .= 1 * r by A9,XCMPLX_0:def 7
                            .= r;
           then ||.(a *(S.n)) - h.|| < r by A7,A11,A12,REAL_1:70;
           hence ||.(a * S).n - h.|| < r by Def8;
           end;
     hence thesis by A2;
end;

definition let RNS;
          let S;
          func ||.S.|| -> Real_Sequence means
:Def10:      for n holds it.n =||.(S.n).||;
existence
         proof
           deffunc F(Nat) = ||.(S.$1).||;
              consider s being Real_Sequence such that A1:
              for n holds s.n = F(n) from ExRealSeq;
              take s;
              thus thesis by A1;
         end;
uniqueness
          proof
               let s,t be Real_Sequence;
                    assume
               A2:  ( for n holds s.n = ||.(S.n).|| ) &
                    ( for n holds t.n = ||.(S.n).|| );
                      now let n;
                       s.n = ||.(S.n).|| by A2; hence
                       s.n = t.n by A2;
                    end;
                    hence thesis by FUNCT_2:113;
         end;
end;

canceled;

theorem Th39:
     S is convergent implies ||.S.|| is convergent
proof
     assume S is convergent;
           then consider g such that
     A1:    for r st 0 < r ex m st for n
           st m <= n holds ||.(S.n) - g.|| < r by Def9;
             now let r be real number;
A2:        r is Real by XREAL_0:def 1;
           assume 0 < r;
           then consider m1 such that
     A3:    for n st m1 <= n holds ||.(S.n) - g.|| < r by A1,A2;
           take k = m1;
           now let n; assume
           k <= n;
     then A4:    ||.(S.n) - g.|| < r by A3;
             abs(||.(S.n).|| - ||.g.||) <= ||.(S.n) - g.|| by Th13;
           then abs(||.(S.n).|| - ||.g.||) < r by A4,AXIOMS:22;
           hence abs(||.S.||.n - ||.g.||) < r by Def10;
           end;
           hence for n st k <= n holds abs(||.S.||.n - ||.g.||) < r;
           end;
     hence thesis by SEQ_2:def 6;
end;

definition let RNS;
          let S;
          assume
       A1: S is convergent;
          func lim S -> Point of RNS means
:Def11:   for r st 0 < r ex m st for n st m <= n
          holds ||.(S.n) - it.|| < r;
existence by A1,Def9;
uniqueness
          proof
                 for x , y st
( for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - x.|| < r ) &
( for r st 0 < r 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 ex m st for n st m <= n holds ||.(S.n) - x.|| < r and
A3: for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - y.|| < r and
A4: x <> y;
A5: ||.x - y.|| <> 0 by A4,Th10;
    A6: 0 <= ||.x - y.|| by Th8;
   then A7: 0/4 < ||.x - y.||/4 by A5,REAL_1:73;
   then consider m1 such that
A8: for n st m1 <= n holds ||.(S.n) - x.|| < ||.x - y.||/4 by A2;
   consider m2 such that
A9: for n st m2 <= n holds ||.(S.n) - y.|| < ||.x - y.||/4 by A3,A7;
A10: now assume
   m1 <= m2;
then A11: ||.(S.m2) - x.|| < ||.x - y.||/4 by A8;
      ||.(S.m2) - y.|| < ||.x - y.||/4 by A9;
    then ||.(S.m2) - x.|| + ||.(S.m2) - y.|| < ||.x - y.||/4 + ||.x - y.||/4
    by A11,REAL_1:67;
then A12: ||.(S.m2) - x.|| + ||.(S.m2) - y.|| <= ||.x - y.||/2 by XCMPLX_1:72;
      ||.x - y.|| <= ||.x - (S.m2).|| + ||.(S.m2) - y.|| by Th14;
    then ||.x - y.|| <= ||.(S.m2) - x.|| + ||.(S.m2) - y.|| by Th11;
    then not ||.x - y.||/2 < ||.x - y.|| by A12,AXIOMS:22;
    hence contradiction by A5,A6,SEQ_2:4;
    end;
     now assume m2 <= m1;
then A13: ||.(S.m1) - y.|| < ||.x - y.||/4 by A9;
      ||.(S.m1) - x.|| < ||.x - y.||/4 by A8;
    then ||.(S.m1) - x.|| + ||.(S.m1) - y.|| < ||.x - y.||/4 + ||.x - y.||/4
    by A13,REAL_1:67;
then A14: ||.(S.m1) - x.|| + ||.(S.m1) - y.|| <= ||.x - y.||/2 by XCMPLX_1:72;
      ||.x - y.|| <= ||.x - (S.m1).|| + ||.(S.m1) - y.|| by Th14;
    then ||.x - y.|| <= ||.(S.m1) - x.|| + ||.(S.m1) - y.|| by Th11;
    then not ||.x - y.||/2 < ||.x - y.|| by A14,AXIOMS:22;
    hence contradiction by A5,A6,SEQ_2:4;
    end;
    hence contradiction by A10;
    end;
hence thesis;
end;
end;

canceled;

theorem
       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;
             S - g is convergent by A1,Th36;
     then A3:    ||.S - g.|| is convergent by Th39;
           now let r be real number;
A4:        r is Real by XREAL_0:def 1;
         assume 0 < r;
           then consider m1 such that
     A5:    for n st m1 <= n holds ||.(S.n) - g.|| < r by A1,A2,A4,Def11;
           take k = m1;
           let n; assume
           k <= n;
     then ||.(S.n) - g.|| < r by A5;
     then A6:    ||.((S.n) - g ) - 0'(RNS).|| < r by RLVECT_1:26;
             abs(||.(S.n) - g.|| - ||.0'(RNS).||) <= ||.((S.n) - g ) - 0'(RNS)
.||
           by Th13;
           then abs(||.(S.n) - g.|| - ||.0'(RNS).||) < r by A6,AXIOMS:22;
           then abs((||.(S.n) - g.|| - 0)) < r by Def2;
           then abs((||.(S - g).n.|| - 0)) < r by Def7;
           hence abs((||.S - g.||.n - 0)) < r by Def10;
           end;
    hence thesis by A3,SEQ_2:def 7;
end;

theorem
       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;
 A3:   S1 + S2 is convergent by A1,A2,Th34;
      set g1 = lim S1;
      set g2 = lim S2;
      set g = g1 + g2;
        now let r; assume 0 < r;
 then A4:  0< r/2 by SEQ_2:3;
      then consider m1 such that
 A5:  for n st m1 <= n holds ||.(S1.n) - g1.|| < r/2 by A1,Def11;
      consider m2 such that
 A6:  for n st m2 <= n holds ||.(S2.n) - g2.|| < r/2 by A2,A4,Def11;
      take k = m1 + m2;
      let n such that
  A7:  k <= n;
        m1 <= m1 + m2 by NAT_1:37;
      then m1 <= n by A7,AXIOMS:22;
  then A8:  ||.(S1.n) - g1.|| < r/2 by A5;
        m2 <= k by NAT_1:37;
      then m2 <= n by A7,AXIOMS:22;
      then ||.(S2.n) - g2.|| < r/2 by A6;
      then ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r/2 + r/2
      by A8,REAL_1:67;
  then A9:  ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r by XCMPLX_1:66;
  A10:  ||.(S1 + S2).n - g.|| = ||.(S1.n) + (S2.n) - (g1+g2).|| by Def5
      .= ||.(S1.n) + ((S2.n) - (g1+g2)).|| by RLVECT_1:42
      .= ||.(S1.n) + (-(g1+g2) + (S2.n)).|| by RLVECT_1:def 11
      .= ||.-(g1+g2) + ((S1.n) + (S2.n)).|| by RLVECT_1:def 6
      .= ||.((-g1)+(-g2)) + ((S1.n) + (S2.n)).|| by RLVECT_1:45
      .= ||.(S1.n) + ((-g1)+(-g2)) + (S2.n).|| by RLVECT_1:def 6
      .= ||.((S1.n) + (-g1)) + (-g2) + (S2.n).|| by RLVECT_1:def 6
      .= ||.(S1.n) - g1 + (-g2) + (S2.n).|| by RLVECT_1:def 11
      .= ||.(S1.n)- g1 + ((S2.n) + -g2).|| by RLVECT_1:def 6
      .= ||.(S1.n) - g1 + ((S2.n) - g2).|| by RLVECT_1:def 11;
        ||.(S1.n) - g1 + ((S2.n) - g2).|| <=
      ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| by Def2;
      hence ||.(S1 + S2).n - g.|| < r by A9,A10,AXIOMS:22;
      end;
      hence thesis by A3,Def11;
end;

theorem
       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;
 A3:   S1 - S2 is convergent by A1,A2,Th35;
      set g1 = lim S1;
      set g2 = lim S2;
      set g = g1 - g2;
        now let r; assume 0 < r;
 then A4:  0< r/2 by SEQ_2:3;
      then consider m1 such that
 A5:  for n st m1 <= n holds ||.(S1.n) - g1.|| < r/2 by A1,Def11;
      consider m2 such that
 A6:  for n st m2 <= n holds ||.(S2.n) - g2.|| < r/2 by A2,A4,Def11;
      take k = m1 + m2;
      let n such that
  A7:  k <= n;
        m1 <= m1 + m2 by NAT_1:37;
      then m1 <= n by A7,AXIOMS:22;
  then A8:  ||.(S1.n) - g1.|| < r/2 by A5;
        m2 <= k by NAT_1:37;
      then m2 <= n by A7,AXIOMS:22;
      then ||.(S2.n) - g2.|| < r/2 by A6;
      then ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r/2 + r/2
      by A8,REAL_1:67;
  then A9:  ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r by XCMPLX_1:66;
  A10:  ||.(S1 - S2).n - g.|| = ||.((S1.n) - (S2.n)) - (g1 - g2).|| by Def6
      .= ||.(((S1.n) - (S2.n)) - g1) + g2.|| by RLVECT_1:43
      .= ||. ((S1.n) - (g1 + (S2.n))) + g2.|| by RLVECT_1:41
      .= ||. (((S1.n) - g1 ) - (S2.n)) + g2.|| by RLVECT_1:41
      .= ||. ((S1.n) - g1 ) - ((S2.n) - g2).|| by RLVECT_1:43;
        ||.((S1.n) - g1) - ((S2.n) - g2).|| <=
      ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| by Th7;
      hence ||.(S1 - S2).n - g.|| < r by A9,A10,AXIOMS:22;
      end;
      hence thesis by A3,Def11;
end;

theorem
       S is convergent implies
     lim (S - x) = (lim S) - x
proof
     assume
 A1:   S is convergent;
 then A2:   S - x is convergent by Th36;
      set g = lim S;
      set h = g - x;
        now let r; assume 0 < r;
      then consider m1 such that
 A3:   for n st m1 <= n holds ||.(S.n) - g.|| < r by A1,Def11;
      take k = m1;
      let n; assume k <= n;
 then A4:   ||.(S.n) - g.|| < r by A3;
        ||.(S.n) - g.|| = ||.((S.n) - 0'(RNS)) - g.|| by RLVECT_1:26
                   .= ||.((S.n) - (x - x)) - g.|| by RLVECT_1:28
                   .= ||.(((S.n) - x) + x) - g.|| by RLVECT_1:43
                   .= ||.((S.n) - x) + (x - g).|| by RLVECT_1:42
                   .= ||.((S.n) - x) + ((-g) + x).|| by RLVECT_1:def 11
                   .= ||.((S.n) - x) + -h.|| by RLVECT_1:47
                   .= ||.((S.n) - x) - h.|| by RLVECT_1:def 11;
      hence ||.(S - x).n - h.|| < r by A4,Def7;
      end;
      hence thesis by A2,Def11;
end;

theorem
       S is convergent implies
     lim (a * S) = a * (lim S)
proof
     assume
 A1:   S is convergent;
 then A2:   a * S is convergent by Th37;
      set g = lim S;
      set h = a * g;
     A3:    now assume
     A4:   a = 0;
           let r; assume 0 < r;
           then consider m1 such that
     A5:   for n st m1 <= n holds ||.(S.n) - g.|| < r by A1,Def11;
           take k = m1;
           let n; assume k <= n;
     then A6:   ||.(S.n) - g.|| < r by A5;
          ||.a * (S.n) - a * g.|| = ||.0 * (S.n) - 0'(RNS).|| by A4,RLVECT_1:23
                        .= ||.0'(RNS) - 0'(RNS).|| by RLVECT_1:23
                        .= ||.0'(RNS).|| by RLVECT_1:26
                        .= 0 by Def2;
           then ||.a * (S.n) - h.|| < r by A6,Th8;
           hence ||.(a * S).n - h.|| < r by Def8;
           end;
             now assume
A7:        a <> 0;
     then A8:   0 < abs(a) by ABSVALUE:6;
           let r such that
      A9:   0 < r;
     A10:   0 <> abs(a) by A7,ABSVALUE:6;
             0/abs(a) =0;
           then 0 < r/abs(a) by A8,A9,REAL_1:73;
           then consider m1 such that
     A11:   for n st m1 <= n holds ||.(S.n) - g.|| < r/abs(a) by A1,Def11;
           take k = m1;
           let n; assume k <= n;
     then A12:   ||.(S.n) - g.|| < r/abs(a) by A11;
     A13:   ||.(a * (S.n)) - (a * g).|| = ||.a * ((S.n) - g).|| by RLVECT_1:48
                                    .= abs(a) * ||.(S.n) - g.|| by Def2;
             abs(a) * (r/abs(a)) = abs(a) * (abs(a)" * r) by XCMPLX_0:def 9
                            .= abs(a) *abs(a)" * r by XCMPLX_1:4
                            .= 1 * r by A10,XCMPLX_0:def 7
                            .= r;
           then ||.(a *(S.n)) - h.|| < r by A8,A12,A13,REAL_1:70;
           hence ||.(a * S).n - h.|| < r by Def8;
           end;
     hence thesis by A2,A3,Def11;
end;

Back to top