COMSEQ_1

:: Complex Sequences
::  by Agnieszka Banachowicz and Anna Winnicka
::
:: Received November 5, 1993
:: Copyright (c) 1993-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FUNCT_1, SUBSET_1, NUMBERS, NAT_1, RELAT_1, TARSKI, XCMPLX_0,
      VALUED_0, FUNCOP_1, COMPLEX1, CARD_1, XBOOLE_0, ARYTM_3, VALUED_1,
      ARYTM_1, COMSEQ_1, ZFMISC_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, ORDINAL1, NUMBERS, COMPLEX1,
      RELAT_1, ZFMISC_1, FUNCT_1, NAT_1, RELSET_1, FUNCOP_1, VALUED_1;
 constructors PARTFUN1, FUNCOP_1, REAL_1, COMPLEX1, VALUED_1, RELSET_1,
      VALUED_0;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, MEMBERED,
      VALUED_0, VALUED_1, XCMPLX_0, XREAL_0;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions ORDINAL1;
 equalities VALUED_1, COMPLEX1;
 theorems COMPLEX1, FUNCT_1, FUNCT_2, TARSKI, RELSET_1, XCMPLX_1, XCMPLX_0,
      FUNCOP_1, VALUED_1, ZFMISC_1, RELAT_1, ORDINAL1;
 schemes CLASSES1;

begin

reserve f for Function;
reserve n,k,n1 for Element of NAT;
reserve r,p for Complex;
reserve x,y for set;

definition
  mode Complex_Sequence is sequence of COMPLEX;
end;

reserve seq,seq1,seq2,seq3,seq9,seq19 for Complex_Sequence;

theorem Th1:
  f is Complex_Sequence iff (dom f=NAT & for x st x in NAT holds f.
  x is Element of COMPLEX)
proof
  thus f is Complex_Sequence implies (dom f=NAT & for x st x in NAT holds f.x
  is Element of COMPLEX)
  proof
    assume
A1: f is Complex_Sequence;
    hence
A2: dom f=NAT by FUNCT_2:def 1;
    let x;
    assume x in NAT;
    then
A3: f.x in rng f by A2,FUNCT_1:def 3;
    rng f c=COMPLEX by A1,RELAT_1:def 19;
    hence thesis by A3;
  end;
  assume that
A4: dom f= NAT and
A5: for x st x in NAT holds f.x is Element of COMPLEX;
  now
    let y be object;
    assume y in rng f;
    then consider x being object such that
A6: x in dom f and
A7: y=f.x by FUNCT_1:def 3;
    f.x is Element of COMPLEX by A4,A5,A6;
    hence y in COMPLEX by A7;
  end;
  then rng f c=COMPLEX by TARSKI:def 3;
  hence thesis by A4,FUNCT_2:def 1,RELSET_1:4;
end;

theorem Th2:
  f is Complex_Sequence iff (dom f=NAT & for n holds f.n is Element of COMPLEX)
proof
  thus f is Complex_Sequence implies (dom f=NAT & for n holds f.n is Element
  of COMPLEX) by Th1;
  assume that
A1: dom f=NAT and
A2: for n holds f.n is Element of COMPLEX;
  for x holds x in NAT implies f.x is Element of COMPLEX by A2;
  hence thesis by A1,Th1;
end;

scheme
  ExComplexSeq{F(set) -> Complex}:
 ex seq st for n being Nat holds seq.n=F(n)
proof
  defpred P[object,object] means ex n st n=$1 & $2=F(n);
A1: now
    let x be object;
    assume x in NAT;
    then consider n such that
A2: n=x;
    reconsider r2=F(n) as object;
    take y=r2;
    thus P[x,y] by A2;
  end;
  consider f such that
A3: dom f=NAT and
A4: for x being object st x in NAT holds P[x,f.x] from CLASSES1:sch 1(A1);
  now
    let x;
    assume x in NAT;
    then ex n st n=x & f.x=F(n) by A4;
    hence f.x is Element of COMPLEX by XCMPLX_0:def 2;
  end;
  then reconsider f as Complex_Sequence by A3,Th1;
  take seq=f;
  let n be Nat;
   n in NAT by ORDINAL1:def 12;
   then ex k st k=n & seq.n=F(k) by A4;
  hence thesis;
end;

registration
  cluster non-zero for Complex_Sequence;
  existence
  proof
    take s = NAT --> 1r;
    rng s = {1} by FUNCOP_1:8;
   hence not 0 in rng s by TARSKI:def 1;
  end;
end;

theorem Th3:
  seq is non-zero iff for x st x in NAT holds seq.x<>0c
proof
  thus seq is non-zero implies for x st x in NAT holds seq.x<>0c
  proof
    assume
A1: seq is non-zero;
    let x;
    assume x in NAT;
    then x in dom seq by Th2;
    then seq.x in rng seq by FUNCT_1:def 3;
    hence thesis by A1;
  end;
  assume
A2: for x st x in NAT holds seq.x<>0c;
  assume 0 in rng seq;
   then 0 in rng seq;
  then ex x being object st x in dom seq & seq.x=0 by FUNCT_1:def 3;
  hence contradiction by A2;
end;

theorem Th4:
  seq is non-zero iff for n holds seq.n<>0c
proof
  thus seq is non-zero implies for n holds seq.n<>0c by Th3;
  assume for n holds seq.n<>0c;
  then for x holds x in NAT implies seq.x<>0c;
  hence thesis by Th3;
end;

theorem
  for IT being non-zero Complex_Sequence holds rng IT c= COMPLEX \ {0c}
    by ORDINAL1:def 15,ZFMISC_1:34;

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:5;
  for x being object st x in {r} holds x in COMPLEX
      by XCMPLX_0:def 2;
  then rng f c= COMPLEX by A2,TARSKI:def 3;
  then reconsider f as Complex_Sequence by A1,FUNCT_2:def 1,RELSET_1:4;
  take f;
  thus thesis by A2;
end;

theorem Th7:
  (seq1+seq2)+seq3=seq1+(seq2+seq3)
proof
  now
    let n;
    thus ((seq1+seq2)+seq3).n=(seq1+seq2 qua Complex_Sequence).n+ seq3.n by
VALUED_1:1
      .=seq1.n+seq2.n+seq3.n by VALUED_1:1
      .=seq1.n+(seq2.n+seq3.n)
      .=seq1.n+(seq2+seq3).n by VALUED_1:1
      .=(seq1+(seq2+seq3)).n by VALUED_1:1;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th8:
  (seq1(#)seq2)(#)seq3=seq1(#)(seq2(#)seq3)
proof
  now
    let n;
    thus ((seq1(#)seq2)(#)seq3).n=(seq1(#)seq2).n*seq3.n by VALUED_1:5
      .=seq1.n*seq2.n*seq3.n by VALUED_1:5
      .=seq1.n*(seq2.n*seq3.n)
      .=seq1.n*(seq2(#)seq3).n by VALUED_1:5
      .=(seq1(#)(seq2(#)seq3)).n by VALUED_1:5;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th9:
  (seq1+seq2)(#)seq3=seq1(#)seq3+seq2(#)seq3
proof
  now
    let n;
    thus ((seq1+seq2)(#)seq3).n=(seq1+seq2).n*seq3.n by VALUED_1:5
      .=(seq1.n+seq2.n)*seq3.n by VALUED_1:1
      .=seq1.n*seq3.n+seq2.n*seq3.n
      .=(seq1(#)seq3).n+seq2.n*seq3.n by VALUED_1:5
      .=(seq1(#)seq3).n+(seq2(#)seq3).n by VALUED_1:5
      .=((seq1(#)seq3)+(seq2(#)seq3)).n by VALUED_1:1;
  end;
  hence thesis by FUNCT_2:63;
end;

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

theorem
  -seq=(-1r)(#)seq;

theorem Th12:
  r(#)(seq1(#)seq2)=r(#)seq1(#)seq2
proof
  now
    let n;
    thus (r(#)(seq1(#)seq2)).n=r*(seq1(#)seq2).n by VALUED_1:6
      .=r*(seq1.n*seq2.n) by VALUED_1:5
      .=(r*seq1.n)*seq2.n
      .=(r(#)seq1).n*seq2.n by VALUED_1:6
      .=(r(#)seq1 (#) seq2).n by VALUED_1:5;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th13:
  r(#)(seq1(#)seq2)=seq1(#)(r(#)seq2)
proof
  now
    let n;
    thus (r(#)(seq1(#)seq2)).n=r*(seq1(#)seq2).n by VALUED_1:6
      .=r*(seq1.n*seq2.n) by VALUED_1:5
      .=seq1.n*(r*seq2.n)
      .=seq1.n*(r(#)seq2).n by VALUED_1:6
      .=(seq1(#)(r(#)seq2)).n by VALUED_1:5;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th14:
  (seq1-seq2)(#)seq3=seq1(#)seq3-seq2(#)seq3
proof
  thus (seq1-seq2)(#)seq3=seq1(#)seq3+(-seq2)(#)seq3 by Th9
    .=seq1(#)seq3+((-1r)(#)seq2)(#)seq3
    .=seq1(#)seq3+(-1r)(#)(seq2(#)seq3) by Th12
    .=seq1(#)seq3-seq2(#)seq3;
end;

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

theorem Th16:
  r(#)(seq1+seq2)=r(#)seq1+r(#)seq2
proof
  now
    let n;
    thus (r(#)(seq1 + seq2)).n=r*(seq1+seq2).n by VALUED_1:6
      .=r*(seq1.n+seq2.n) by VALUED_1:1
      .=r*seq1.n+r*seq2.n
      .=(r(#)seq1).n+r*seq2.n by VALUED_1:6
      .=(r(#)seq1).n+(r(#)seq2).n by VALUED_1:6
      .=((r(#)seq1)+(r(#)seq2)).n by VALUED_1:1;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th17:
  (r*p)(#)seq=r(#)(p(#)seq)
proof
  now
    let n;
    thus ((r*p)(#)seq).n=(r*p)*seq.n by VALUED_1:6
      .=r*(p*seq.n)
      .=r*(p(#)seq).n by VALUED_1:6
      .=(r(#)(p(#)seq)).n by VALUED_1:6;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th18:
  r(#)(seq1-seq2)=r(#)seq1-r(#)seq2
proof
  thus r(#)(seq1-seq2)=r(#)seq1+r(#)(-seq2) by Th16
    .=r(#)seq1+r(#)((-1r)(#)seq2)
    .=r(#)seq1+((-1r)*r)(#)seq2 by Th17
    .=r(#)seq1+(-1r)(#)(r(#)seq2) by Th17
    .=r(#)seq1-(r(#)seq2);
end;

theorem
  r(#)(seq1/"seq)=(r(#)seq1)/"seq
proof
  thus r(#)(seq1/"seq) = r(#)(seq1(#)(seq)") .= (r(#)seq1)/"seq by Th12;
end;

theorem
  seq1-(seq2+seq3)=seq1-seq2-seq3
proof
  thus seq1-(seq2+seq3)=seq1+(-1r)(#)(seq2+seq3)
    .=seq1+((-1r)(#)seq2+(-1r)(#)seq3) by Th16
    .=seq1+(-seq2+(-1r)(#)seq3)
    .=seq1+(-seq2+-seq3)
    .=seq1-seq2-seq3 by Th7;
end;

theorem
  1r(#)seq=seq
proof
  now
    let n;
    thus (1r(#)seq).n=1r*seq.n by VALUED_1:6
      .=seq.n;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  --seq = seq;

theorem
  seq1 - (-seq2) = seq1 + seq2;

theorem
  seq1 - (seq2 - seq3) = seq1 - seq2 + seq3
proof
  thus seq1-(seq2-seq3)=seq1+(-1r)(#)(seq2-seq3)
    .=seq1+((-1r)(#)seq2-((-1r)(#)seq3)) by Th18
    .=seq1+(-seq2-((-1r)(#)seq3))
    .=seq1+(-seq2-(-seq3))
    .=seq1-seq2+seq3 by Th7;
end;

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

theorem
  (-seq1)(#)seq2=-(seq1(#)seq2) & seq1(#)(-seq2)=-(seq1(#)seq2)
by Th12;

theorem Th27:
  seq is non-zero implies seq" is non-zero
proof
  assume that
A1: seq is non-zero and
A2: not seq" is non-zero;
  consider n1 such that
A3: (seq").n1=0c by A2,Th4;
  (seq.n1)"=(seq").n1 by VALUED_1:10;
  hence contradiction by A1,A3,Th4,XCMPLX_1:202;
end;

::$CT

theorem Th28:
  seq is non-zero & seq1 is non-zero iff seq(#)seq1 is non-zero
proof
  thus seq is non-zero & seq1 is non-zero implies seq(#)seq1 is non-zero
  proof
    assume
A1: seq is non-zero & seq1 is non-zero;
    now
      let n;
A2:   (seq(#)seq1).n=(seq.n)*(seq1.n) by VALUED_1:5;
      seq.n<>0c & seq1.n<>0c by A1,Th4;
      hence (seq(#)seq1).n<>0c by A2;
    end;
    hence thesis by Th4;
  end;
  assume
A3: seq(#)seq1 is non-zero;
  now
    let n;
    (seq(#)seq1).n=(seq.n)*(seq1.n) by VALUED_1:5;
    hence seq.n<>0c by A3,Th4;
  end;
  hence seq is non-zero by Th4;
  now
    let n;
    (seq(#)seq1).n=(seq.n)*(seq1.n) by VALUED_1:5;
    hence seq1.n<>0c by A3,Th4;
  end;
  hence thesis by Th4;
end;

theorem Th29:
  seq"(#)seq1"=(seq(#)seq1)"
proof
  now
    let n;
    thus ((seq")(#)(seq1")).n=((seq").n)*((seq1").n) by VALUED_1:5
      .=((seq").n)*(seq1.n)" by VALUED_1:10
      .=(seq.n)"*(seq1.n)" by VALUED_1:10
      .=((seq.n)*(seq1.n))" by XCMPLX_1:204
      .=((seq(#)seq1).n)" by VALUED_1:5
      .=((seq(#)seq1)").n by VALUED_1:10;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  seq is non-zero implies (seq1/"seq)(#)seq=seq1
proof
  assume
A1: seq is non-zero;
  now
    let n;
A2: seq.n<>0c by A1,Th4;
    thus ((seq1/"seq)(#)seq).n=((seq1(#)seq").n)*seq.n by VALUED_1:5
      .=(seq1.n)*(seq".n)*seq.n by VALUED_1:5
      .=(seq1.n)*(seq.n)"*seq.n by VALUED_1:10
      .=(seq1.n)*((seq.n)"*seq.n)
      .=(seq1.n)*1r by A2,XCMPLX_0:def 7
      .=seq1.n;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  (seq9/"seq)(#)(seq19/"seq1)=(seq9(#)seq19)/"(seq(#)seq1)
proof
  now
    let n;
    thus ((seq9/"seq)(#)(seq19/"seq1)).n=((seq9(#)seq").n)*(seq19/"seq1).n by
VALUED_1:5
      .=(seq9.n)*(seq".n)*(seq19(#)seq1").n by VALUED_1:5
      .=(seq9.n)*(seq".n)*((seq19.n)*seq1".n) by VALUED_1:5
      .=(seq9.n)*((seq19.n)*((seq".n)*seq1".n))
      .=(seq9.n)*((seq19.n)*((seq"(#)seq1").n)) by VALUED_1:5
      .=(seq9.n)*(seq19.n)*((seq"(#)seq1").n)
      .=(seq9.n)*(seq19.n)*((seq(#)seq1)".n) by Th29
      .=((seq9(#)seq19).n)*(seq(#)seq1)".n by VALUED_1:5
      .=((seq9(#)seq19)/"(seq(#)seq1)).n by VALUED_1:5;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  seq is non-zero & seq1 is non-zero implies seq/"seq1 is non-zero
proof
  assume that
A1: seq is non-zero and
A2: seq1 is non-zero;
  seq1" is non-zero by A2,Th27;
  hence thesis by A1,Th28;
end;

theorem Th33:
  (seq/"seq1)"=seq1/"seq
proof
  now
    let n;
    thus (seq/"seq1)".n=(seq"(#)seq1"").n by Th29
      .=(seq1/"seq).n;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq
proof
  thus seq2 (#) (seq1 /" seq) = seq2 (#) seq1 (#) (seq") by Th8
    .= (seq2 (#) seq1) /" seq;
end;

theorem
  seq2/"(seq/"seq1)=(seq2(#)seq1)/"seq
proof
  now
    let n;
    thus (seq2/"(seq/"seq1)).n=((seq2(#)(seq1/"seq))).n by Th33
      .=((seq2(#)seq1)(#)(seq")).n by Th8
      .=((seq2(#)seq1)/"seq).n;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th36:
  seq1 is non-zero implies seq2/"seq=(seq2(#)seq1)/"(seq(#)seq1)
proof
  assume
A1: seq1 is non-zero;
  now
    let n;
A2: seq1.n<>0c by A1,Th4;
    thus (seq2/"seq).n=(seq2.n)*1r*seq".n by VALUED_1:5
      .=(seq2.n)*((seq1.n)*(seq1.n)")*seq".n by A2,XCMPLX_0:def 7
      .=(seq2.n)*(seq1.n)*((seq1.n)"*seq".n)
      .=((seq2(#)seq1).n)*((seq1.n)"*seq".n) by VALUED_1:5
      .=((seq2(#)seq1).n)*((seq1".n)*seq".n) by VALUED_1:10
      .=((seq2(#)seq1).n)*(seq"(#)seq1").n by VALUED_1:5
      .=((seq2(#)seq1).n)*(seq(#)seq1)".n by Th29
      .=((seq2(#)seq1)/"(seq(#)seq1)).n by VALUED_1:5;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th37:
  r<>0c & seq is non-zero implies r(#)seq is non-zero
proof
  assume that
A1: r<>0c and
A2: seq is non-zero and
A3: not r(#)seq is non-zero;
  consider n1 such that
A4: (r(#)seq).n1=0c by A3,Th4;
A5: r*seq.n1=0c by A4,VALUED_1:6;
  seq.n1 <> 0c by A2,Th4;
  hence contradiction by A1,A5;
end;

theorem
  seq is non-zero implies -seq is non-zero
by Th37;

theorem Th39:
  (r(#)seq)"=r"(#)seq"
proof
  now
    let n;
    thus (r(#)seq)".n=((r(#)seq).n)" by VALUED_1:10
      .=(r*(seq.n))" by VALUED_1:6
      .=r"*(seq.n)" by XCMPLX_1:204
      .=r"*seq".n by VALUED_1:10
      .=(r"(#)seq").n by VALUED_1:6;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th40:
  seq is non-zero implies (-seq)"=(-1r)(#)seq"
proof
  (-1)" = -1;
  hence thesis by Th39;
end;

theorem
  seq is non-zero implies -seq1/"seq=(-seq1)/"seq & seq1/"(-seq)=-seq1/" seq
proof
  assume
A1: seq is non-zero;
  thus -seq1/"seq=(-1r)(#)(seq1/"seq) .=((-1r)(#)seq1)(#)(seq") by Th12
    .=(-seq1)/"seq;
  thus seq1/"(-seq)=seq1(#)((-1r)(#)seq") by A1,Th40
    .=(-1r)(#)(seq1(#)(seq")) by Th13
    .=-(seq1/"seq);
end;

theorem
  seq1/"seq + seq19/"seq = (seq1+seq19) /" seq & seq1/"seq - seq19/"seq
  = (seq1-seq19) /" seq
proof
  thus seq1/"seq + seq19/"seq = (seq1+seq19)(#)(seq") by Th9
    .= (seq1+seq19) /" seq;
  thus seq1/"seq - seq19/"seq = (seq1-seq19)(#)(seq") by Th14
    .= (seq1-seq19) /" seq;
end;

theorem
  seq is non-zero & seq9 is non-zero implies seq1/"seq + seq19/"seq9=(
seq1(#)seq9+seq19(#)seq)/"(seq(#)seq9) & seq1/"seq - seq19/"seq9=(seq1(#)seq9-
  seq19(#)seq)/"(seq(#)seq9)
proof
  assume that
A1: seq is non-zero and
A2: seq9 is non-zero;
  thus seq1/"seq + seq19/"seq9=(seq1(#)seq9)/"(seq(#)seq9)+seq19/"seq9 by A2
,Th36
    .=(seq1(#)seq9)/"(seq(#)seq9)+(seq19(#)seq)/"(seq(#)seq9) by A1,Th36
    .=(seq1(#)seq9+seq19(#)seq)(#)((seq(#)seq9)") by Th9
    .=(seq1(#)seq9+seq19(#)seq)/"(seq(#)seq9);
  thus seq1/"seq - seq19/"seq9=(seq1(#)seq9)/"(seq(#)seq9)-seq19/"seq9 by A2
,Th36
    .=(seq1(#)seq9)/"(seq(#)seq9)-(seq19(#)seq)/"(seq(#)seq9) by A1,Th36
    .=(seq1(#)seq9-seq19(#)seq)(#)((seq(#)seq9)") by Th14
    .=(seq1(#)seq9-seq19(#)seq)/"(seq(#)seq9);
end;

theorem
  (seq19/"seq)/"(seq9/"seq1)=(seq19(#)seq1)/"(seq(#)seq9)
proof
  thus (seq19/"seq)/"(seq9/"seq1)= (seq19/"seq)(#)(seq9"(#)seq1"") by Th29
    .=seq19(#)seq"(#)seq1(#)seq9" by Th8
    .=seq19(#)(seq1(#)seq")(#)seq9" by Th8
    .=seq19(#)((seq1(#)seq")(#)seq9") by Th8
    .=seq19(#)(seq1(#)(seq"(#)seq9")) by Th8
    .=seq19(#)seq1(#)(seq"(#)seq9") by Th8
    .=(seq19(#)seq1)/"(seq(#)seq9) by Th29;
end;

theorem Th45:
  |.seq(#)seq9.|=|.seq.|(#)|.seq9.|
proof
  now
    let n;
    thus (|.seq(#)seq9.|).n=|.((seq(#)seq9).n).| by VALUED_1:18
      .=|.(seq.n)*(seq9.n).| by VALUED_1:5
      .=|.(seq.n).|*|.(seq9.n).| by COMPLEX1:65
      .=((|.seq.|).n)*|.(seq9.n).| by VALUED_1:18
      .=((|.seq.|).n)*(|.seq9.|).n by VALUED_1:18
      .=(|.seq.|(#)|.seq9.|).n by VALUED_1:5;
  end;
  hence thesis by FUNCT_2:63;
end;

::$CT

theorem Th46:
  |. seq .| " = |. seq" .|
proof
  now
    let n;
    thus (|.seq".|).n=|.seq".n.| by VALUED_1:18
      .=|.(seq.n)".| by VALUED_1:10
      .=|.1r/(seq.n).| by XCMPLX_1:215
      .=1/|.seq.n.| by COMPLEX1:48,67
      .=|.seq.n.|" by XCMPLX_1:215
      .=(|.seq.|.n)" by VALUED_1:18
      .=(|.seq.|)".n by VALUED_1:10;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  |.seq9/"seq.|=|.seq9.|/"|.seq.|
proof
  thus |.seq9/"seq.|=|.seq9.|(#)|.seq".| by Th45
    .=|.seq9.|/"|.seq.| by Th46;
end;

theorem
  |.r(#)seq.|=|.r.|(#)|.seq.|
proof
  now
    let n;
    thus |.r(#)seq.|.n=|.(r(#)seq).n.| by VALUED_1:18
      .=|.r*(seq.n).| by VALUED_1:6
      .=|.r.|*|.seq.n.| by COMPLEX1:65
      .=|.r.|*(|.seq.|).n by VALUED_1:18
      .=(|.r.|(#)|.seq.|).n by VALUED_1:6;
  end;
  hence thesis by FUNCT_2:63;
end;