The Mizar article:

Real Sequences and Basic Operations on Them

by
Jaroslaw Kotowicz

Received July 4, 1989

Copyright (c) 1989 Association of Mizar Users

MML identifier: SEQ_1
[ MML identifier index ]


environ

 vocabulary FUNCT_1, ARYTM, RELAT_1, PARTFUN1, BOOLE, ARYTM_1, ABSVALUE,
      ARYTM_3, SEQ_1, ZF_REFLE;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      NAT_1, REAL_1, RELAT_1, FUNCT_1, ABSVALUE, RELSET_1, PARTFUN1, FUNCT_2;
 constructors REAL_1, ABSVALUE, FUNCT_2, PARTFUN1, MEMBERED, XBOOLE_0;
 clusters XREAL_0, RELSET_1, FUNCT_2, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions XREAL_0, PARTFUN1, RELAT_1;
 theorems FUNCT_1, TARSKI, ABSVALUE, FUNCT_2, SUBSET_1, PARTFUN1, RELSET_1,
      RELAT_1, CARD_1, XREAL_0, ZFMISC_1, XBOOLE_0, XBOOLE_1, XCMPLX_0,
      XCMPLX_1;
 schemes FUNCT_1, FUNCT_2, XBOOLE_0;

begin

  reserve f for Function;
  reserve n,k,n1 for Nat;
  reserve r,p for real number;
  reserve x,y,z for set;

definition
 mode Real_Sequence is Function of NAT,REAL;
end;

reserve seq,seq1,seq2,seq3,seq',seq1' for Real_Sequence;

canceled 2;

theorem
 Th3:f is Real_Sequence iff (dom f=NAT & for x st x in NAT holds f.x is real)
  proof
thus f is Real_Sequence implies
            (dom f=NAT & for x st x in NAT holds f.x is real)
   proof
    assume
 A1: f is Real_Sequence;
    hence dom f=NAT by FUNCT_2:def 1;
 A2: rng f c=REAL by A1,RELSET_1:12;
    let x;
    assume x in NAT;
    then x in dom f by A1,FUNCT_2:def 1;
    then f.x in rng f by FUNCT_1:def 5;
    hence f.x in REAL by A2;
   end;
   assume that
 A3: dom f= NAT and
 A4: for x st x in NAT holds f.x is real;
      now let y; assume y in rng f;
     then consider x such that
  A5: x in dom f and
  A6: y=f.x by FUNCT_1:def 5;
       f.x is real by A3,A4,A5;
     hence y in REAL by A6,XREAL_0:def 1;
    end;
   then rng f c=REAL by TARSKI:def 3;
   hence thesis by A3,FUNCT_2:def 1,RELSET_1:11;
 end;

theorem
Th4:f is Real_Sequence iff (dom f=NAT & for n holds f.n is real)
 proof
thus f is Real_Sequence implies (dom f=NAT & for n holds f.n is real) by Th3;
  assume that
A1: dom f=NAT and
A2: for n holds f.n is real;
     for x holds x in NAT implies f.x is real by A2;
  hence thesis by A1,Th3;
 end;

definition let f be Relation;
 attr f is real-yielding means
:Def1: rng f c= REAL;
end;

definition let C be set;
 cluster -> real-yielding PartFunc of C, REAL;
 coherence
  proof let f be PartFunc of C, REAL;
   thus rng f c= REAL;
  end;
end;

definition
 cluster real-yielding Function;
 existence
  proof consider A being set;
   consider f being Function of A, REAL;
   take f;
   thus rng f c= REAL;
  end;
end;

definition let f be real-yielding Function, x be set;
 cluster f.x -> real;
  coherence
 proof per cases;
  suppose x in dom f;
    then A1:   f.x in rng f by FUNCT_1:12;
       rng f c= REAL by Def1;
   hence f.x in REAL by A1;
  suppose not x in dom f;
   hence thesis by CARD_1:51,FUNCT_1:def 4;
 end;
end;

definition let f be real-yielding Function, x be set;
 redefine func f.x -> Real;
  coherence by XREAL_0:def 1;
end;

definition let C be set, f be PartFunc of C, REAL, x be set;
 redefine func f.x -> Real;
  coherence by XREAL_0:def 1;
end;

definition
 let f be PartFunc of NAT, REAL;
 redefine attr f is non-empty means :Def2: rng f c= REAL \ {0};
 compatibility
 proof
   thus f is non-empty implies rng f c= REAL \ {0}
   proof
     assume not {} in rng f;
     hence thesis by ZFMISC_1:40;
   end;
   assume rng f c= REAL \ {0};
   then not {} in rng f by ZFMISC_1:64;
   hence thesis by RELAT_1:def 9;
 end;
  synonym f is being_not_0;
  synonym f is_not_0;
end;

canceled;

theorem
 Th6: seq is being_not_0 iff for x st x in NAT holds seq.x<>0
  proof
  thus seq is being_not_0 implies for x st x in NAT holds seq.x<>0
  proof
   assume seq is being_not_0;
    then A1: rng seq c= REAL\{0} by Def2;
   let x;
   assume x in NAT;
   then x in dom seq by Th4;
   then seq.x in rng seq by FUNCT_1:def 5;
   then not seq.x in {0} by A1,XBOOLE_0:def 4;
   hence seq.x<>0 by TARSKI:def 1;
  end;
  assume
A2: for x st x in NAT holds seq.x<>0;
     now let y;
    assume y in rng seq;
    then consider x such that
 A3: x in dom seq and
 A4: seq.x=y by FUNCT_1:def 5;
      y<>0 by A2,A3,A4;
    then not y in {0} by TARSKI:def 1;
    hence y in REAL\{0} by A4,XBOOLE_0:def 4;
   end;
  then rng seq c=REAL\{0} by TARSKI:def 3;
  hence thesis by Def2;
 end;

theorem
 Th7: seq is being_not_0 iff for n holds seq.n<>0
  proof
thus seq is being_not_0 implies for n holds seq.n<>0 by Th6;
  assume for n holds seq.n<>0;
   then for x holds x in NAT implies seq.x<>0;
  hence thesis by Th6;
 end;

theorem
   for seq,seq1 st (for x st x in NAT holds seq.x=seq1.x) holds seq=seq1
   proof
    let seq,seq1 such that
 A1: for x st x in NAT holds seq.x=seq1.x;
      dom seq= NAT & dom seq1=NAT by FUNCT_2:def 1;
    hence thesis by A1,FUNCT_1:9;
   end;

canceled;

theorem
   for r ex seq st rng seq={r}
  proof
   let r;
   consider f such that
 A1: dom f=NAT and
 A2: rng f={r} by FUNCT_1:15;
      now let x;
     assume x in {r};
     then x=r by TARSKI:def 1;
     hence x in REAL by XREAL_0:def 1;
    end;
   then rng f c= REAL by A2,TARSKI:def 3;
   then reconsider f as Real_Sequence by A1,FUNCT_2:def 1,RELSET_1:11;
   take f;
   thus rng f = {r} by A2;
 end;

scheme ExRealSeq{F(set)->real number}:
 ex seq st for n holds seq.n=F(n)
  proof
   defpred P[set,set] means ex n st n=$1 & $2=F(n);
 A1: now let x;
     assume x in NAT;
     then consider n such that
  A2: n=x;
     reconsider r2=F(n) as set;
     take y=r2;
     thus P[x,y] by A2;
    end;
 A3: for x,y,z st x in NAT & P[x,y] & P[x,z] holds y=z;
   consider f such that
A4: dom f=NAT and
A5: for x st x in NAT holds P[x,f.x] from FuncEx(A3,A1);
      now let x;
     assume x in NAT;
      then ex n st n=x & f.x=F(n) by A5;
     hence f.x is real;
    end;
   then reconsider f as Real_Sequence by A4,Th3;
   take seq=f;
   let n;
      ex k st k=n & seq.n=F(k) by A5;
   hence seq.n=F(n);
  end;

::
::  BASIC OPERATIONS ON SEQUENCES
::

scheme PartFuncExD'{D,C()->non empty set, P[set,set]}:
 ex f being PartFunc of D(),C() st
  (for d be Element of D() holds
      d in dom f iff (ex c be Element of C() st P[d,c])) &
  (for d be Element of D() st d in dom f holds P[d,f.d])
 proof
  consider x being Element of C();
   defpred X[Element of D(),Element of C()] means
    ((ex c be Element of C() st P[$1,c]) implies P[$1,$2]) &
    ((for c be Element of C() holds not P[$1,c]) implies $2=x);
A1: for d be Element of D() ex z be Element of C() st X[d,z]
:::    ((ex c be Element of C() st P[d,c]) implies P[d,z]) &
:::    ((for c be Element of C() holds not P[d,c]) implies z=x)
   proof let d be Element of D();
      (for c be Element of C() holds not P[d,c]) implies
     ex z st ((ex c be Element of C() st P[d,c]) implies P[d,z]) &
          ((for c be Element of C() holds not P[d,c]) implies z=x);
    hence thesis;
   end;
  consider g being Function of D(),C() such that
A2: for d be Element of D() holds X[d,g.d]
:::     ((ex c be Element of C() st P[d,c]) implies P[d,g.d]) &
:::     ((for c be Element of C() holds not P[d,c]) implies g.d=x)
       from FuncExD(A1);
A3: dom g = D() & rng g c= C() by FUNCT_2:def 1;
   defpred X[set] means ex c be Element of C() st P[$1,c];
  consider X be set such that
A4: for x holds x in X iff x in D() & X[x]
:::& ex c be Element of C() st P[x,c]
       from Separation;
     for x holds x in X implies x in D() by A4;
  then reconsider X as Subset of D() by TARSKI:def 3;
   reconsider f=g|X as PartFunc of D(),C();
   take f;
   thus for d be Element of D() holds
      d in dom f iff (ex c be Element of C() st P[d,c])
    proof let d be Element of D();
       dom f c= X by RELAT_1:87;
hence d in dom f implies ex c be Element of C() st P[d,c] by A4;
     assume ex c be Element of C() st P[d,c];
     then d in X & d in D() by A4;
     then d in dom g /\ X by A3,XBOOLE_0:def 3;
     hence thesis by RELAT_1:90;
    end;
   let d be Element of D();
   assume A5: d in dom f;
     dom f c= X by RELAT_1:87;
   then ex c be Element of C() st P[d,c] by A4,A5;
   then P[d,g.d] by A2;
   hence thesis by A5,FUNCT_1:70;
 end;

scheme LambdaPFD'{D,C()->non empty set, F(set)->Element of C(), P[set]}:
  ex f being PartFunc of D(),C() st
   (for d be Element of D() holds d in dom f iff P[d]) &
   (for d be Element of D() st d in dom f holds f.d = F(d))
  proof defpred X[Element of D(),set] means P[$1] & $2 = F($1);
   consider f being PartFunc of D(),C() such that
A1:  for d be Element of D() holds
      d in dom f iff ex c be Element of C() st X[d,c] :::P[c,d] & c = F(d)
      and
A2:  for d be Element of D() st d in dom f holds X[d,f.d] :::P[d] & f.d = F(d)
      from PartFuncExD';
   take f;
   thus for d be Element of D() holds d in dom f iff P[d]
    proof let d be Element of D();
     thus d in dom f implies P[d]
      proof assume d in dom f;
       then ex c be Element of C() st P[d] & c = F(d) by A1;
       hence thesis;
      end;
     assume P[d];
     then ex c be Element of C() st P[d] & c = F(d);
     hence thesis by A1;
    end;
   thus thesis by A2;
  end;

scheme UnPartFuncD'{C,D,X() -> set, F(set)->set}:
  for f,g being PartFunc of C(),D() st
   (dom f=X() & for c be Element of C() st c in dom f holds f.c = F(c)) &
   (dom g=X() & for c be Element of C() st c in dom g holds g.c = F(c))
  holds f = g
proof let f,g be PartFunc of C(),D(); assume that
A1: (dom f=X() & for c be Element of C() st c in dom f holds f.c = F(c)) and
A2: dom g=X() & for c be Element of C() st c in dom g holds g.c = F(c);
   now let c be Element of C(); assume A3: c in dom f;
  hence f.c = F(c) by A1
            .= g.c by A1,A2,A3;
 end;
 hence thesis by A1,A2,PARTFUN1:34;
end;

definition let C be :::non empty
  set; let f1,f2 be PartFunc of C,REAL;
func f1+f2 -> PartFunc of C,REAL means :Def3:
 dom it = dom f1 /\ dom f2 &
  for c being Element of C st c in dom it holds it.c = f1.c + f2.c;
existence
proof per cases;
 suppose
A1: C is empty;
  reconsider F = {} as PartFunc of C,REAL by PARTFUN1:56;
  take F;
  thus dom F = dom f1 /\ dom f2 by A1,RELAT_1:60,XBOOLE_1:3;
  thus thesis by RELAT_1:60;
 suppose C is non empty;
  then reconsider C' = C as non empty set;
  defpred X[set] means $1 in dom f1 /\ dom f2;
  deffunc U(Element of C') = f1.$1 + f2.$1;
  consider F be PartFunc of C',REAL such that
A2: for c being Element of C' holds c in dom F iff X[c] and
A3: for c being Element of C' st c in dom F holds F.c = U(c)
                  from LambdaPFD';
  reconsider F as PartFunc of C,REAL;
 take F;
 thus dom F = dom f1 /\ (dom f2 qua Subset of C) by A2,SUBSET_1:8;
 thus thesis by A3;
end;
  uniqueness
   proof deffunc U(Element of C) = f1.$1 + f2.$1;
    thus for f,g being PartFunc of C,REAL st
   (dom f=dom f1 /\ dom f2 &
      for c be Element of C st c in dom f holds f.c = U(c)) &
   (dom g=dom f1 /\ dom f2 &
      for c be Element of C st c in dom g holds g.c = U(c))
  holds f = g from UnPartFuncD';
   end;
  commutativity;
func f1-f2 -> PartFunc of C,REAL means :Def4:
dom it = dom f1 /\ dom f2 &
 for c being Element of C st c in dom it holds it.c = f1.c - f2.c;
existence
proof per cases;
 suppose
A4: C is empty;
  reconsider F = {} as PartFunc of C,REAL by PARTFUN1:56;
  take F;
  thus dom F = dom f1 /\ dom f2 by A4,RELAT_1:60,XBOOLE_1:3;
  thus thesis by RELAT_1:60;
 suppose C is non empty;
  then reconsider C' = C as non empty set;
  defpred X[set] means $1 in dom f1 /\ dom f2;
  deffunc U(Element of C') = f1.$1 - f2.$1;
  consider F be PartFunc of C',REAL such that
A5: for c being Element of C' holds c in dom F iff X[c] and
A6: for c being Element of C' st c in dom F holds F.c = U(c)
                  from LambdaPFD';
  reconsider F as PartFunc of C,REAL;
 take F;
 thus dom F = dom f1 /\ (dom f2 qua Subset of C) by A5,SUBSET_1:8;
 thus thesis by A6;
end;
uniqueness
   proof deffunc U(Element of C) = f1.$1 - f2.$1;
    thus for f,g being PartFunc of C,REAL st
   (dom f=dom f1 /\ dom f2 &
      for c be Element of C st c in dom f holds f.c = U(c)) &
   (dom g=dom f1 /\ dom f2 &
      for c be Element of C st c in dom g holds g.c = U(c))
  holds f = g from UnPartFuncD';
   end;
func f1(#)f2 -> PartFunc of C,REAL means :Def5:
dom it = dom f1 /\ dom f2 &
   for c being Element of C st c in dom it holds it.c = f1.c * f2.c;
existence
proof per cases;
 suppose
A7: C is empty;
  reconsider F = {} as PartFunc of C,REAL by PARTFUN1:56;
  take F;
  thus dom F = dom f1 /\ dom f2 by A7,RELAT_1:60,XBOOLE_1:3;
  thus thesis by RELAT_1:60;
 suppose C is non empty;
  then reconsider C' = C as non empty set;
  defpred X[set] means $1 in dom f1 /\ dom f2;
  deffunc U(Element of C') = f1.$1 * f2.$1;
  consider F be PartFunc of C',REAL such that
A8: for c being Element of C' holds c in dom F iff X[c] and
A9: for c being Element of C' st c in dom F holds F.c = U(c)
                  from LambdaPFD';
  reconsider F as PartFunc of C,REAL;
 take F;
 thus dom F = dom f1 /\ (dom f2 qua Subset of C) by A8,SUBSET_1:8;
 thus thesis by A9;
end;
uniqueness
   proof deffunc U(Element of C) = f1.$1 * f2.$1;
    thus for f,g being PartFunc of C,REAL st
   (dom f=dom f1 /\ dom f2 &
      for c be Element of C st c in dom f holds f.c = U(c)) &
   (dom g=dom f1 /\ dom f2 &
      for c be Element of C st c in dom g holds g.c = U(c))
  holds f = g from UnPartFuncD';
   end;
  commutativity;
end;

theorem Th11:
 seq = seq1 + seq2 iff for n holds seq.n =seq1.n + seq2.n
  proof
   thus seq = seq1 + seq2 implies for n holds seq.n =seq1.n + seq2.n
    proof assume
A1:   seq = seq1 + seq2;
     let n;
        dom seq = NAT by FUNCT_2:def 1;
     hence seq.n =seq1.n + seq2.n by A1,Def3;
    end;
   assume
A2:  for n holds seq.n =seq1.n + seq2.n;
A3:  dom seq = NAT /\ NAT by FUNCT_2:def 1
        .= NAT /\ dom seq2 by FUNCT_2:def 1
        .= dom seq1 /\ dom seq2 by FUNCT_2:def 1;
      for n st n in dom seq holds seq.n = seq1.n + seq2.n by A2;
   hence thesis by A3,Def3;
  end;

theorem Th12:
 seq = seq1 (#) seq2 iff for n holds seq.n =seq1.n * seq2.n
  proof
   thus seq = seq1 (#) seq2 implies for n holds seq.n =seq1.n * seq2.n
    proof assume
A1:   seq = seq1 (#) seq2;
     let n;
        dom seq = NAT by FUNCT_2:def 1;
     hence seq.n =seq1.n * seq2.n by A1,Def5;
    end;
   assume
A2:  for n holds seq.n =seq1.n * seq2.n;
A3:  dom seq = NAT /\ NAT by FUNCT_2:def 1
        .= NAT /\ dom seq2 by FUNCT_2:def 1
        .= dom seq1 /\ dom seq2 by FUNCT_2:def 1;
      for n st n in dom seq holds seq.n = seq1.n * seq2.n by A2;
   hence thesis by A3,Def5;
  end;

definition
  let seq1,seq2;
  cluster seq1+seq2 -> total;
  coherence
   proof
       dom seq1 = NAT & dom seq2 = NAT by FUNCT_2:def 1;
    hence dom(seq1 + seq2) = NAT /\ NAT by Def3 .= NAT;
   end;
  cluster seq1(#)seq2 -> total;
  coherence
   proof
       dom seq1 = NAT & dom seq2 = NAT by FUNCT_2:def 1;
    hence dom(seq1 (#) seq2) = NAT /\ NAT by Def5 .= NAT;
   end;
end;

definition let C be set; let f be PartFunc of C,REAL;
   let r be real number;
 reconsider r1 = r as Element of REAL by XREAL_0:def 1;
func r(#)f -> PartFunc of C,REAL means :Def6:
 dom it = dom f & for c being Element of C st c in dom it holds it.c = r * f.c;
existence
proof per cases;
 suppose
A1: C is empty;
  reconsider F = {} as PartFunc of C,REAL by PARTFUN1:56;
  take F;
  thus dom F = dom f by A1,RELAT_1:60,XBOOLE_1:3;
  thus thesis by RELAT_1:60;
 suppose C is non empty;
  then reconsider C' = C as non empty set;
  defpred X[set] means $1 in dom f;
  deffunc U(Element of C') = r1 * f.$1;
  consider F be PartFunc of C',REAL such that
A2: for c being Element of C' holds c in dom F iff X[c] and
A3: for c being Element of C' st c in dom F holds F.c = U(c)
                  from LambdaPFD';
  reconsider F as PartFunc of C,REAL;
 take F;
 thus dom F = dom f by A2,SUBSET_1:8;
 thus thesis by A3;
end;
uniqueness
 proof deffunc U(Element of C) = r1 * f.$1;
    for f1, f2 be PartFunc of C,REAL st
   (dom f1 = dom f & for c being Element of C st c in dom f1 holds
      f1.c = U(c)) &
   (dom f2 = dom f & for c being Element of C st c in dom f2 holds
      f2.c = U(c)) holds f1 = f2 from UnPartFuncD';
  hence thesis;
 end;
end;

definition
 let r,seq;
 cluster r(#)seq -> total;
 coherence
  proof
   thus dom(r(#)seq) = dom seq by Def6 .= NAT by FUNCT_2:def 1;
  end;
end;

theorem Th13:
  seq1 = r(#)seq2 iff for n holds seq1.n=r*seq2.n
 proof
  thus seq1 = r(#)seq2 implies for n holds seq1.n=r*seq2.n
   proof assume
A1:   seq1 = r(#)seq2;
    let n;
       dom(r(#)seq2) = NAT by FUNCT_2:def 1;
    hence thesis by A1,Def6;
   end;
  assume
A2: for n holds seq1.n=r*seq2.n;
A3: dom seq1 = NAT by FUNCT_2:def 1 .= dom seq2 by FUNCT_2:def 1;
     for n st n in dom seq1 holds seq1.n = r * seq2.n by A2;
  hence thesis by A3,Def6;
 end;

definition let C be set; let f be PartFunc of C,REAL;
func -f ->PartFunc of C,REAL means :Def7:
 dom it = dom f & for c being Element of C st c in dom it holds it.c = -(f.c);
existence
proof per cases;
 suppose
A1: C is empty;
  reconsider F = {} as PartFunc of C,REAL by PARTFUN1:56;
  take F;
  thus dom F = dom f by A1,RELAT_1:60,XBOOLE_1:3;
  thus thesis by RELAT_1:60;
 suppose C is non empty;
  then reconsider C' = C as non empty set;
  defpred X[set] means $1 in dom f;
  deffunc U(Element of C') = -(f.$1);
  consider F be PartFunc of C',REAL such that
A2: for c being Element of C' holds c in dom F iff X[c] and
A3: for c being Element of C' st c in dom F holds F.c = U(c)
                  from LambdaPFD';
  reconsider F as PartFunc of C,REAL;
 take F;
 thus dom F = dom f by A2,SUBSET_1:8;
 thus thesis by A3;
end;
uniqueness
 proof deffunc U(Element of C) = -(f.$1);
    for f1, f2 be PartFunc of C,REAL st
   (dom f1 = dom f & for c being Element of C st c in dom f1 holds
      f1.c = U(c)) &
   (dom f2 = dom f & for c being Element of C st c in dom f2 holds
      f2.c = U(c)) holds f1 = f2 from UnPartFuncD';
  hence thesis;
 end;
end;

definition
 let seq;
 cluster - seq -> total;
 coherence
  proof
   thus dom -seq = dom seq by Def7 .= NAT by FUNCT_2:def 1;
  end;
end;

theorem Th14:
  seq1 = -seq2 iff for n holds seq1.n= -seq2.n
 proof
  thus seq1 = -seq2 implies for n holds seq1.n=-seq2.n
   proof assume
A1:   seq1 = -seq2;
    let n;
       dom(-seq2) = NAT by FUNCT_2:def 1;
    hence thesis by A1,Def7;
   end;
  assume
A2: for n holds seq1.n= -seq2.n;
A3: dom seq1 = NAT by FUNCT_2:def 1 .= dom seq2 by FUNCT_2:def 1;
     for n st n in dom seq1 holds seq1.n = - seq2.n by A2;
  hence thesis by A3,Def7;
 end;

definition
 let seq1,seq2;
 cluster seq1-seq2 -> total;
 coherence
  proof
      dom seq1 = NAT & dom seq2 = NAT by FUNCT_2:def 1;
   hence dom(seq1 - seq2) = NAT /\ NAT by Def4 .= NAT;
  end;
end;

theorem Th15:
 seq1 - seq2 = seq1 +- seq2
 proof
A1: dom(seq1 +- seq2) = NAT /\ NAT by FUNCT_2:def 1
      .= NAT /\ dom seq2 by FUNCT_2:def 1
      .= dom seq1 /\ dom seq2 by FUNCT_2:def 1;
    for c being Element of NAT st c in dom(seq1 +- seq2)
     holds (seq1 +- seq2).c = seq1.c - seq2.c
  proof let c be Element of NAT;
   assume c in dom(seq1 +- seq2);
   thus (seq1 +- seq2).c = seq1.c + (-seq2).c by Th11
         .= seq1.c + -seq2.c by Th14
         .= seq1.c - seq2.c by XCMPLX_0:def 8;
  end;
  hence thesis by A1,Def4;
 end;

definition
 let seq;
func seq" -> Real_Sequence means :Def8: for n holds it.n=(seq.n)";
 existence
  proof deffunc U(Nat) = (seq.$1)";
   thus ex f being Real_Sequence st
    for n holds f.n=U(n) from ExRealSeq;
  end;
 uniqueness
  proof
   let seq1,seq2 such that
A1: for n holds seq1.n=(seq.n)" and
A2: for n holds seq2.n=(seq.n)";
      now let n;
       seq1.n=(seq.n)" & seq2.n=(seq.n)" by A1,A2;
     hence seq1.n=seq2.n;
    end;
   hence seq1=seq2 by FUNCT_2:113;
  end;
end;

definition
 let seq1,seq;
func seq1 /" seq ->Real_Sequence equals :Def9: seq1(#)(seq");
 correctness;
end;

definition let C be set; let f be PartFunc of C,REAL;
func abs f -> PartFunc of C,REAL means :Def10:
 dom it = dom f & for c being Element of C st c in dom it holds
   it.c = abs(f.c);
existence
proof per cases;
 suppose
A1: C is empty;
  reconsider F = {} as PartFunc of C,REAL by PARTFUN1:56;
  take F;
  thus dom F = dom f by A1,RELAT_1:60,XBOOLE_1:3;
  thus thesis by RELAT_1:60;
 suppose C is non empty;
  then reconsider C' = C as non empty set;
  defpred X[set] means $1 in dom f;
  deffunc U(Element of C') = abs(f.$1);
  consider F be PartFunc of C',REAL such that
A2: for c being Element of C' holds c in dom F iff X[c] and
A3: for c being Element of C' st c in dom F holds F.c = U(c)
                  from LambdaPFD';
  reconsider F as PartFunc of C,REAL;
 take F;
 thus dom F = dom f by A2,SUBSET_1:8;
 thus thesis by A3;
end;
uniqueness
 proof deffunc U(Element of C) = abs(f.$1);
    for f1, f2 be PartFunc of C,REAL st
   (dom f1 = dom f & for c being Element of C st c in dom f1 holds
      f1.c = U(c)) &
   (dom f2 = dom f & for c being Element of C st c in dom f2 holds
      f2.c = U(c)) holds f1 = f2 from UnPartFuncD';
  hence thesis;
 end;
end;

definition let seq;
  cluster abs seq -> total;
 coherence
  proof
   thus dom abs seq = dom seq by Def10 .= NAT by FUNCT_2:def 1;
  end;
end;

theorem Th16:
  seq1 = abs seq iff for n holds seq1.n= abs(seq.n)
 proof
  thus seq1 = abs seq implies for n holds seq1.n=abs(seq.n)
   proof assume
A1:   seq1 = abs(seq);
    let n;
       dom(abs(seq)) = NAT by FUNCT_2:def 1;
    hence thesis by A1,Def10;
   end;
  assume
A2: for n holds seq1.n= abs(seq.n);
A3: dom seq1 = NAT by FUNCT_2:def 1 .= dom seq by FUNCT_2:def 1;
     for n st n in dom seq1 holds seq1.n = abs(seq.n) by A2;
  hence thesis by A3,Def10;
 end;

canceled 3;

theorem
 Th20: (seq1+seq2)+seq3=seq1+(seq2+seq3)
  proof
     now let n;
    thus ((seq1+seq2)+seq3).n=(seq1+seq2).n+ seq3.n by Th11
     .=seq1.n+seq2.n+seq3.n by Th11
     .=seq1.n+(seq2.n+seq3.n) by XCMPLX_1:1
     .=seq1.n+(seq2+seq3).n by Th11
     .=(seq1+(seq2+seq3)).n by Th11;
   end;
  hence thesis by FUNCT_2:113;
 end;

canceled;

theorem
 Th22: (seq1(#)seq2)(#)seq3=seq1(#)(seq2(#)seq3)
  proof
     now let n;
    thus ((seq1(#)seq2)(#)seq3).n=(seq1(#)seq2).n*seq3.n by Th12
     .=seq1.n*seq2.n*seq3.n by Th12
     .=seq1.n*(seq2.n*seq3.n) by XCMPLX_1:4
     .=seq1.n*(seq2(#)seq3).n by Th12
     .=(seq1(#)(seq2(#)seq3)).n by Th12;
   end;
  hence thesis by FUNCT_2:113;
 end;

theorem
 Th23: (seq1+seq2)(#)seq3=seq1(#)seq3+seq2(#)seq3
  proof
     now let n;
    thus ((seq1+seq2)(#)seq3).n=(seq1+seq2).n*seq3.n by Th12
     .=(seq1.n+seq2.n)*seq3.n by Th11
     .=seq1.n*seq3.n+seq2.n*seq3.n by XCMPLX_1:8
     .=(seq1(#)seq3).n+seq2.n*seq3.n by Th12
     .=(seq1(#)seq3).n+(seq2(#)seq3).n by Th12
     .=((seq1(#)seq3)+(seq2(#)seq3)).n by Th11;
   end;
  hence thesis by FUNCT_2:113;
 end;

theorem
    seq3(#)(seq1+seq2)=seq3(#)seq1+seq3(#)seq2 by Th23;

theorem
 Th25: -seq=(-1)(#)seq
  proof
     now let n;
    thus ((-1)(#)seq).n=(-1)*seq.n by Th13
     .=-(1*seq.n) by XCMPLX_1:175
     .=(-seq).n by Th14;
   end;
  hence thesis by FUNCT_2:113;
 end;

theorem
 Th26: r(#)(seq1(#)seq2)=r(#)seq1(#)seq2
  proof
     now let n;
    thus (r(#)(seq1(#)seq2)).n=r*(seq1(#)seq2).n by Th13
     .=r*(seq1.n*seq2.n) by Th12
     .=(r*seq1.n)*seq2.n by XCMPLX_1:4
     .=(r(#)seq1).n*seq2.n by Th13
     .=(r(#)seq1 (#) seq2).n by Th12;
   end;
  hence thesis by FUNCT_2:113;
 end;

theorem
 Th27: r(#)(seq1(#)seq2)=seq1(#)(r(#)seq2)
  proof
     now let n;
    thus (r(#)(seq1(#)seq2)).n=r*(seq1(#)seq2).n by Th13
     .=r*(seq1.n*seq2.n) by Th12
     .=seq1.n*(r*seq2.n) by XCMPLX_1:4
     .=seq1.n*(r(#)seq2).n by Th13
     .=(seq1(#)(r(#)seq2)).n by Th12;
   end;
  hence thesis by FUNCT_2:113;
 end;

theorem
 Th28: (seq1-seq2)(#)seq3=seq1(#)seq3-seq2(#)seq3
 proof
  thus (seq1-seq2)(#)seq3=(seq1+-seq2)(#)seq3 by Th15
   .=seq1(#)seq3+(-seq2)(#)seq3 by Th23
   .=seq1(#)seq3+((-1)(#)seq2)(#)seq3 by Th25
   .=seq1(#)seq3+(-1)(#)(seq2(#)seq3) by Th26
   .=seq1(#)seq3+-(seq2(#)seq3) by Th25
   .=seq1(#)seq3-seq2(#)seq3 by Th15;
 end;

theorem
    seq3(#)seq1-seq3(#)seq2=seq3(#)(seq1-seq2) by Th28;

theorem
 Th30: r(#)(seq1+seq2)=r(#)seq1+r(#)seq2
  proof
     now let n;
    thus (r(#)(seq1 + seq2)).n=r*(seq1+seq2).n by Th13
     .=r*(seq1.n+seq2.n) by Th11
     .=r*seq1.n+r*seq2.n by XCMPLX_1:8
     .=(r(#)seq1).n+r*seq2.n by Th13
     .=(r(#)seq1).n+(r(#)seq2).n by Th13
     .=((r(#)seq1)+(r(#)seq2)).n by Th11;
   end;
  hence thesis by FUNCT_2:113;
 end;

theorem
 Th31: (r*p)(#)seq=r(#)(p(#)seq)
  proof
     now let n;
    thus ((r*p)(#)seq).n=(r*p)*seq.n by Th13
     .=r*(p*seq.n) by XCMPLX_1:4
     .=r*(p(#)seq).n by Th13
     .=(r(#)(p(#)seq)).n by Th13;
   end;
  hence thesis by FUNCT_2:113;
 end;

theorem
 Th32: r(#)(seq1-seq2)=r(#)seq1-r(#)seq2
  proof
   thus r(#)(seq1-seq2)=r(#)(seq1+-seq2) by Th15
    .=r(#)seq1+r(#)(-seq2) by Th30
    .=r(#)seq1+r(#)((-1)(#)seq2) by Th25
    .=r(#)seq1+((-1)*r)(#)seq2 by Th31
    .=r(#)seq1+(-1)(#)(r(#)seq2) by Th31
    .=r(#)seq1+-(r(#)seq2) by Th25
    .=r(#)seq1-(r(#)seq2) by Th15;
  end;

theorem
 Th33: r(#)(seq1/"seq)=(r(#)seq1)/"seq
  proof
   thus r(#)(seq1/"seq)=r(#)(seq1(#)seq") by Def9
    .=(r(#)seq1)(#)(seq") by Th26
    .=(r(#)seq1)/"seq by Def9;
 end;

theorem
    seq1-(seq2+seq3)=seq1-seq2-seq3
  proof
   thus seq1-(seq2+seq3)=seq1+-(seq2+seq3) by Th15
    .=seq1+(-1)(#)(seq2+seq3) by Th25
    .=seq1+((-1)(#)seq2+(-1)(#)seq3) by Th30
    .=seq1+(-seq2+(-1)(#)seq3) by Th25
    .=seq1+(-seq2+-seq3) by Th25
    .=seq1+-seq2+-seq3 by Th20
    .=seq1-seq2+-seq3 by Th15
    .=seq1-seq2-seq3 by Th15;
 end;

theorem
 Th35:  1(#)seq=seq
  proof
     now let n;
    thus (1(#)seq).n=1*seq.n by Th13
     .=seq.n;
   end;
   hence thesis by FUNCT_2:113;
  end;

theorem
 Th36:  -(-seq)=seq
  proof
   thus -(-seq)=(-1)(#)(-seq) by Th25
    .=(-1)(#)((-1)(#)seq) by Th25
    .=((-1)*(-1))(#)seq by Th31
    .=seq by Th35;
   end;

theorem
 Th37: seq1-(-seq2)=seq1+seq2
  proof
   thus seq1-(-seq2)=seq1+(-(-seq2)) by Th15
    .=seq1+seq2 by Th36;
  end;

theorem
    seq1-(seq2-seq3)=seq1-seq2+seq3
  proof
   thus seq1-(seq2-seq3)=seq1+-(seq2-seq3) by Th15
    .=seq1+(-1)(#)(seq2-seq3) by Th25
    .=seq1+((-1)(#)seq2-((-1)(#)seq3)) by Th32
    .=seq1+(-seq2-((-1)(#)seq3)) by Th25
    .=seq1+(-seq2-(-seq3)) by Th25
    .=seq1+(-seq2+seq3) by Th37
    .=seq1+-seq2+seq3 by Th20
    .=seq1-seq2+seq3 by Th15;
  end;

theorem
    seq1+(seq2-seq3)=seq1+seq2-seq3
  proof
   thus seq1+(seq2-seq3)=seq1+(seq2+-seq3) by Th15
    .=seq1+seq2+-seq3 by Th20
    .=seq1+seq2-seq3 by Th15;
  end;

theorem
    (-seq1)(#)seq2=-(seq1(#)seq2) & seq1(#)(-seq2)=-(seq1(#)seq2)
  proof
   thus (-seq1)(#)seq2=(-1)(#)seq1(#)seq2 by Th25
    .=(-1)(#)(seq1(#)seq2) by Th26
    .=-(seq1(#)seq2) by Th25;
   thus seq1(#)(-seq2)=seq1(#)((-1)(#)seq2) by Th25
    .=(-1)(#)(seq1(#)seq2) by Th27
    .=-(seq1(#)seq2) by Th25;
  end;

theorem
 Th41:seq is being_not_0 implies seq" is being_not_0
  proof
   assume that
 A1: seq is being_not_0 and
 A2: not seq" is being_not_0;
   consider n1 such that
 A3: (seq").n1=0 by A2,Th7;
 A4: seq.n1<>0 by A1,Th7;
     (seq.n1)"=(seq").n1 by Def8;
   hence contradiction by A3,A4,XCMPLX_1:203;
  end;

theorem
 Th42:seq""=seq
  proof
      now let n;
     thus (seq"").n=((seq").n)" by Def8
      .=(seq.n)"" by Def8
      .=seq.n;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
 Th43:seq is being_not_0 & seq1 is being_not_0 iff seq(#)seq1 is being_not_0
  proof
thus seq is being_not_0 & seq1 is being_not_0 implies seq(#)seq1 is
being_not_0
  proof
   assume that
A1: seq is being_not_0 and
A2: seq1 is being_not_0;
      now let n;
 A3: seq.n<>0 by A1,Th7;
 A4: seq1.n<>0 by A2,Th7;
       (seq(#)seq1).n=(seq.n)*(seq1.n) by Th12;
     hence (seq(#)seq1).n<>0 by A3,A4,XCMPLX_1:6;
    end;
   hence thesis by Th7;
  end;
  assume
A5: seq(#)seq1 is being_not_0;
     now let n;
      (seq(#)seq1).n=(seq.n)*(seq1.n) by Th12;
    hence seq.n<>0 by A5,Th7;
   end;
  hence seq is being_not_0 by Th7;
     now let n;
      (seq(#)seq1).n=(seq.n)*(seq1.n) by Th12;
    hence seq1.n<>0 by A5,Th7;
   end;
  hence seq1 is being_not_0 by Th7;
 end;

theorem
 Th44:seq"(#)seq1"=(seq(#)seq1)"
  proof
      now let n;
     thus ((seq")(#)(seq1")).n=((seq").n)*((seq1").n) by Th12
      .=((seq").n)*(seq1.n)" by Def8
      .=(seq.n)"*(seq1.n)" by Def8
      .=((seq.n)*(seq1.n))" by XCMPLX_1:205
      .=((seq(#)seq1).n)" by Th12
      .=((seq(#)seq1)").n by Def8;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
   seq is being_not_0 implies (seq1/"seq)(#)seq=seq1
  proof
   assume
A1: seq is being_not_0;
      now let n;
 A2: seq.n<>0 by A1,Th7;
     thus ((seq1/"seq)(#)seq).n=((seq1/"seq).n)*seq.n by Th12
      .=((seq1(#)seq").n)*seq.n by Def9
      .=(seq1.n)*(seq".n)*seq.n by Th12
      .=(seq1.n)*(seq.n)"*seq.n by Def8
      .=(seq1.n)*((seq.n)"*seq.n) by XCMPLX_1:4
      .=(seq1.n)*1 by A2,XCMPLX_0:def 7
      .=seq1.n;
     end;
    hence thesis by FUNCT_2:113;
   end;

theorem
   (seq'/"seq)(#)(seq1'/"seq1)=(seq'(#)seq1')/"(seq(#)seq1)
  proof
      now let n;
  thus ((seq'/"seq)(#)(seq1'/"seq1)).n=((seq'/"seq).n)*(seq1'/"seq1).n by Th12
       .=((seq'(#)seq").n)*(seq1'/"seq1).n by Def9
       .=((seq'(#)seq").n)*(seq1'(#)seq1").n by Def9
        .=(seq'.n)*(seq".n)*(seq1'(#)seq1").n by Th12
        .=(seq'.n)*(seq".n)*((seq1'.n)*seq1".n) by Th12
        .=(seq'.n)*(seq".n)*(seq1'.n)*seq1".n by XCMPLX_1:4
        .=(seq'.n)*((seq1'.n)*(seq".n))*seq1".n by XCMPLX_1:4
        .=(seq'.n)*(((seq1'.n)*(seq".n))*seq1".n) by XCMPLX_1:4
        .=(seq'.n)*((seq1'.n)*((seq".n)*seq1".n)) by XCMPLX_1:4
        .=(seq'.n)*((seq1'.n)*((seq"(#)seq1").n)) by Th12
        .=(seq'.n)*(seq1'.n)*((seq"(#)seq1").n) by XCMPLX_1:4
        .=(seq'.n)*(seq1'.n)*((seq(#)seq1)".n) by Th44
        .=((seq'(#)seq1').n)*(seq(#)seq1)".n by Th12
        .=((seq'(#)seq1')(#)(seq(#)seq1)").n by Th12
        .=((seq'(#)seq1')/"(seq(#)seq1)).n by Def9;
      end;
     hence thesis by FUNCT_2:113;
   end;

theorem
   seq is being_not_0 & seq1 is being_not_0 implies seq/"seq1 is being_not_0
  proof
   assume that
A1: seq is being_not_0 and
A2: seq1 is being_not_0;
   seq1" is being_not_0 by A2,Th41;
   then seq(#)seq1" is being_not_0 by A1,Th43;
   hence thesis by Def9;
  end;

theorem
 Th48:(seq/"seq1)"=seq1/"seq
  proof
      now let n;
     thus (seq/"seq1)".n=(seq(#)seq1")".n by Def9
      .=(seq"(#)seq1"").n by Th44
      .=(seq1(#)seq").n by Th42
      .=(seq1/"seq).n by Def9;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
 Th49: seq2(#)(seq1/"seq)=(seq2(#)seq1)/"seq
  proof
      now let n;
     thus (seq2(#)(seq1/"seq)).n=(seq2(#)(seq1(#)seq")).n by Def9
      .=(seq2(#)seq1(#)seq").n by Th22
      .=((seq2(#)seq1)/"seq).n by Def9;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
    seq2/"(seq/"seq1)=(seq2(#)seq1)/"seq
  proof
      now let n;
     thus (seq2/"(seq/"seq1)).n=((seq2(#)(seq/"seq1)")).n by Def9
      .=((seq2(#)(seq1/"seq))).n by Th48
      .=((seq2(#)seq1)/"seq).n by Th49;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
 Th51:seq1 is being_not_0 implies
                  seq2/"seq=(seq2(#)seq1)/"(seq(#)seq1)
  proof
   assume that
A1: seq1 is being_not_0;
      now let n;
  A2: seq1.n<>0 by A1,Th7;
     thus (seq2/"seq).n=(seq2(#)seq").n by Def9
      .=(seq2.n)*1*seq".n by Th12
      .=(seq2.n)*((seq1.n)*(seq1.n)")*seq".n by A2,XCMPLX_0:def 7
      .=(seq2.n)*(((seq1.n)*(seq1.n)")*seq".n) by XCMPLX_1:4
      .=(seq2.n)*((seq1.n)*((seq1.n)"*seq".n)) by XCMPLX_1:4
      .=(seq2.n)*(seq1.n)*((seq1.n)"*seq".n) by XCMPLX_1:4
      .=((seq2(#)seq1).n)*((seq1.n)"*seq".n) by Th12
      .=((seq2(#)seq1).n)*((seq1".n)*seq".n) by Def8
      .=((seq2(#)seq1).n)*(seq"(#)seq1").n by Th12
      .=((seq2(#)seq1).n)*(seq(#)seq1)".n by Th44
      .=((seq2(#)seq1)(#)(seq(#)seq1)").n by Th12
      .=((seq2(#)seq1)/"(seq(#)seq1)).n by Def9;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
 Th52:r<>0 & seq is being_not_0 implies r(#)seq is being_not_0
  proof
   assume that
A1: r<>0 and
A2: seq is being_not_0 and
A3: not r(#)seq is being_not_0;
   consider n1 such that
A4: (r(#)seq).n1=0 by A3,Th7;
A5: r*seq.n1=0 by A4,Th13;
     seq.n1 <> 0 by A2,Th7;
   hence contradiction by A1,A5,XCMPLX_1:6;
  end;

theorem
   seq is being_not_0 implies -seq is being_not_0
  proof
   assume
  seq is being_not_0;
   then (-1)(#)seq is being_not_0 by Th52;
   hence thesis by Th25;
  end;

theorem
 Th54:(r(#)seq)"=r"(#)seq"
  proof
      now let n;
     thus (r(#)seq)".n=((r(#)seq).n)" by Def8
      .=(r*(seq.n))" by Th13
      .=r"*(seq.n)" by XCMPLX_1:205
      .=r"*seq".n by Def8
      .=(r"(#)seq").n by Th13;
    end;
   hence thesis by FUNCT_2:113;
  end;

 Lm1:(-1)"=-1;

theorem
 Th55:(-seq)"=(-1)(#)seq"
  proof
   thus (-seq)"=((-1)(#)seq)" by Th25
    .=(-1)(#)seq" by Lm1,Th54;
  end;

theorem
   -seq1/"seq=(-seq1)/"seq & seq1/"(-seq)=-seq1/"seq
  proof
   thus -seq1/"seq=(-1)(#)(seq1/"seq) by Th25
    .=((-1)(#)seq1)/"seq by Th33
    .=(-seq1)/"seq by Th25;
   thus seq1/"(-seq)=seq1(#)(-seq)" by Def9
    .=seq1(#)((-1)(#)seq") by Th55
    .=(-1)(#)(seq1(#)(seq")) by Th27
    .=-(seq1(#)seq") by Th25
    .=-(seq1/"seq) by Def9;
  end;

theorem
 Th57: seq1/"seq + seq1'/"seq=(seq1+seq1')/"seq &
                           seq1/"seq - seq1'/"seq=(seq1-seq1')/"seq
  proof
   thus seq1/"seq+seq1'/"seq=seq1(#)seq" +seq1'/"seq by Def9
    .=seq1(#)seq" +seq1'(#)seq" by Def9
    .=(seq1+seq1')(#)seq" by Th23
    .=(seq1+seq1')/"seq by Def9;
   thus seq1/"seq-seq1'/"seq=seq1(#)seq" -seq1'/"seq by Def9
    .=seq1(#)seq" -seq1'(#)seq" by Def9
    .=(seq1-seq1')(#)seq" by Th28
    .=(seq1-seq1')/"seq by Def9;
  end;

theorem
   seq is being_not_0 & seq' is being_not_0 implies
       (seq1/"seq + seq1'/"seq'=(seq1(#)seq'+seq1'(#)seq)/"(seq(#)seq')) &
       (seq1/"seq - seq1'/"seq'=(seq1(#)seq'-seq1'(#)seq)/"(seq(#)seq'))
  proof
   assume that
A1: seq is being_not_0 and
A2: seq' is being_not_0;
   thus seq1/"seq + seq1'/"seq'=(seq1(#)seq')/"(seq(#)seq')+seq1'/"seq'
      by A2,Th51
    .=(seq1(#)seq')/"(seq(#)seq')+(seq1'(#)seq)/"(seq(#)seq') by A1,Th51
    .=(seq1(#)seq'+seq1'(#)seq)/"(seq(#)seq') by Th57;
   thus seq1/"seq - seq1'/"seq'=(seq1(#)seq')/"(seq(#)seq')-seq1'/"seq'
      by A2,Th51
    .=(seq1(#)seq')/"(seq(#)seq')-(seq1'(#)seq)/"(seq(#)seq') by A1,Th51
    .=(seq1(#)seq'-seq1'(#)seq)/"(seq(#)seq') by Th57;
  end;

theorem
   (seq1'/"seq)/"(seq'/"seq1)=(seq1'(#)seq1)/"(seq(#)seq')
  proof
   thus (seq1'/"seq)/"(seq'/"seq1)=(seq1'/"seq)(#)(seq'/"seq1)" by Def9
    .=(seq1'/"seq)(#)(seq'(#)seq1")" by Def9
    .=(seq1'/"seq)(#)(seq'"(#)seq1"") by Th44
    .=(seq1'/"seq)(#)(seq1(#)seq'") by Th42
    .=(seq1'(#)seq")(#)(seq1(#)seq'") by Def9
    .=seq1'(#)seq"(#)seq1(#)seq'" by Th22
    .=seq1'(#)(seq1(#)seq")(#)seq'" by Th22
    .=seq1'(#)((seq1(#)seq")(#)seq'") by Th22
    .=seq1'(#)(seq1(#)(seq"(#)seq'")) by Th22
    .=seq1'(#)seq1(#)(seq"(#)seq'") by Th22
    .=seq1'(#)seq1(#)(seq(#)seq')" by Th44
    .=(seq1'(#)seq1)/"(seq(#)seq') by Def9;
  end;

theorem
 Th60:abs(seq(#)seq')=abs(seq)(#)abs(seq')
  proof
     now let n;
    thus (abs(seq(#)seq')).n=abs(((seq(#)seq').n)) by Th16
     .=abs((seq.n)*(seq'.n)) by Th12
     .=abs((seq.n))*abs((seq'.n)) by ABSVALUE:10
     .=((abs(seq)).n)*abs((seq'.n)) by Th16
     .=((abs(seq)).n)*(abs(seq')).n by Th16
     .=(abs(seq)(#)abs(seq')).n by Th12;
   end;
  hence thesis by FUNCT_2:113;
 end;

theorem
   seq is being_not_0 implies abs(seq) is being_not_0
  proof
   assume
 A1: seq is being_not_0;
      now let n;
       seq.n<>0 by A1,Th7;
     then abs(seq.n)<>0 by ABSVALUE:6;
     hence (abs(seq)).n<>0 by Th16;
    end;
   hence thesis by Th7;
  end;

theorem
 Th62:abs(seq)"=abs(seq")
  proof
      now let n;
     thus (abs(seq")).n=abs(seq".n) by Th16
      .=abs((seq.n)") by Def8
      .=abs(1/(seq.n)) by XCMPLX_1:217
      .=1/abs(seq.n) by ABSVALUE:15
      .=(abs(seq.n))" by XCMPLX_1:217
      .=(abs(seq).n)" by Th16
      .=(abs(seq))".n by Def8;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
   abs(seq'/"seq)=abs(seq')/"abs(seq)
  proof
   thus abs(seq'/"seq)=abs(seq'(#)seq") by Def9
    .=abs(seq')(#)abs(seq") by Th60
    .=abs(seq')(#)abs(seq)" by Th62
    .=abs(seq')/"abs(seq) by Def9;
  end;

theorem
   abs(r(#)seq)=abs(r)(#)abs(seq)
  proof
     now let n;
    thus abs(r(#)seq).n=abs((r(#)seq).n) by Th16
     .=abs(r*(seq.n)) by Th13
     .=abs(r)*abs(seq.n) by ABSVALUE:10
     .=abs(r)*(abs(seq)).n by Th16
     .=(abs(r)(#)abs(seq)).n by Th13;
   end;
  hence thesis by FUNCT_2:113;
 end;

Back to top