:: COMSEQ_1 semantic presentation

begin


definition
mode Complex_Sequence is sequence of COMPLEX;
end;


theorem Th1: :: COMSEQ_1:1
for f being Function holds
( f is Complex_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of COMPLEX ) ) )
proof
let f be Function; ::_thesis: ( f is Complex_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of COMPLEX ) ) )
thus  ( f is Complex_Sequence implies ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of COMPLEX ) ) ) ::_thesis: ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of COMPLEX ) implies f is Complex_Sequence )
proof
assume A1: f is Complex_Sequence ; ::_thesis: ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of COMPLEX ) )
hence A2: dom f = NAT by FUNCT_2:def_1; ::_thesis: for x being set st x in NAT holds
f . x is Element of COMPLEX
let x be set ; ::_thesis: ( x in NAT implies f . x is Element of COMPLEX )
assume  x in NAT ; ::_thesis: f . x is Element of COMPLEX
then A3: f . x in rng f by A2, FUNCT_1:def_3;
 rng f c= COMPLEX by A1, RELAT_1:def_19;
hence  f . x is Element of COMPLEX by A3; ::_thesis: verum
end;
assume that
A4: dom f = NAT and
A5: for x being set st x in NAT holds
f . x is Element of COMPLEX ; ::_thesis: f is Complex_Sequence
now__::_thesis:_for_y_being_set_st_y_in_rng_f_holds_
y_in_COMPLEX
let y be set ; ::_thesis: ( y in rng f implies y in COMPLEX )
assume  y in rng f ; ::_thesis: y in COMPLEX
then consider x being set  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; ::_thesis: verum
end;
then  rng f c= COMPLEX by TARSKI:def_3;
hence  f is Complex_Sequence by A4, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;

theorem Th2: :: COMSEQ_1:2
for f being Function holds
( f is Complex_Sequence iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of COMPLEX ) ) )
proof
let f be Function; ::_thesis: ( f is Complex_Sequence iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of COMPLEX ) ) )
thus  ( f is Complex_Sequence implies ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of COMPLEX ) ) ) by Th1; ::_thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of COMPLEX ) implies f is Complex_Sequence )
assume that
A1: dom f = NAT and
A2: for n being Element of NAT holds f . n is Element of COMPLEX ; ::_thesis: f is Complex_Sequence
 for x being set st x in NAT holds
f . x is Element of COMPLEX by A2;
hence  f is Complex_Sequence by A1, Th1; ::_thesis: verum
end;

scheme :: COMSEQ_1:sch 1
ExComplexSeq{ F1( set ) ->  complex number } :
 ex seq being Complex_Sequence st
for n being Element of NAT holds seq . n = F1(n)
proof
defpred S1[ set , set ] means  ex n being Element of NAT st
( n = $1 & $2 = F1(n) );
A1: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
ex_y_being_set_st_S1[x,y]
let x be set ; ::_thesis: ( x in NAT implies ex y being set st S1[x,y] )
assume  x in NAT ; ::_thesis: ex y being set st S1[x,y]
then consider n being Element of NAT  such that
A2: n = x ;
reconsider r2 = F1(n) as set ;
take y = r2; ::_thesis: S1[x,y]
thus  S1[x,y] by A2; ::_thesis: verum
end;
consider f being Function such that
A3: dom f = NAT and
A4: for x being set st x in NAT holds
S1[x,f . x] from CLASSES1:sch_1(A1);
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
f_._x_is_Element_of_COMPLEX
let x be set ; ::_thesis: ( x in NAT implies f . x is Element of COMPLEX )
assume  x in NAT ; ::_thesis: f . x is Element of COMPLEX
then  ex n being Element of NAT st
( n = x & f . x = F1(n) ) by A4;
hence  f . x is Element of COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
end;
then reconsider f = f as Complex_Sequence by A3, Th1;
take seq = f; ::_thesis: for n being Element of NAT holds seq . n = F1(n)
let n be Element of NAT ; ::_thesis: seq . n = F1(n)
 ex k being Element of NAT st
( k = n & seq . n = F1(k) ) by A4;
hence  seq . n = F1(n) ; ::_thesis: verum
end;

notation
let f be complex-valued Relation;
synonym  non-zero f for  non-empty ;
end;

registration
cluster Relation-like non-zero NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued for Element of K19(K20(NAT,COMPLEX));
existence
 ex b1 being Complex_Sequence st b1 is non-zero
proof
take s = NAT --> 1r; ::_thesis: s is non-zero
 rng s = {1} by FUNCOP_1:8;
hence  not 0 in rng s by TARSKI:def_1; :: according to RELAT_1:def_9 ::_thesis: verum
end;
end;

theorem Th3: :: COMSEQ_1:3
for seq being Complex_Sequence holds
( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0c )
proof
let seq be Complex_Sequence; ::_thesis: ( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0c )
thus  ( seq is non-zero implies for x being set st x in NAT holds
seq . x <> 0c ) ::_thesis: ( ( for x being set st x in NAT holds
seq . x <> 0c ) implies seq is non-zero )
proof
assume A1: seq is non-zero ; ::_thesis: for x being set st x in NAT holds
seq . x <> 0c
let x be set ; ::_thesis: ( x in NAT implies seq . x <> 0c )
assume  x in NAT ; ::_thesis: seq . x <> 0c
then  x in dom seq by Th2;
then  seq . x in rng seq by FUNCT_1:def_3;
hence  seq . x <> 0c by A1, RELAT_1:def_9; ::_thesis: verum
end;
assume A2: for x being set st x in NAT holds
seq . x <> 0c ; ::_thesis: seq is non-zero
assume  0 in rng seq ; :: according to RELAT_1:def_9 ::_thesis: contradiction
then  ex x being set st
( x in dom seq & seq . x = 0 ) by FUNCT_1:def_3;
hence  contradiction by A2; ::_thesis: verum
end;

theorem Th4: :: COMSEQ_1:4
for seq being Complex_Sequence holds
( seq is non-zero iff for n being Element of NAT holds seq . n <> 0c )
proof
let seq be Complex_Sequence; ::_thesis: ( seq is non-zero iff for n being Element of NAT holds seq . n <> 0c )
thus  ( seq is non-zero implies for n being Element of NAT holds seq . n <> 0c ) by Th3; ::_thesis: ( ( for n being Element of NAT holds seq . n <> 0c ) implies seq is non-zero )
assume  for n being Element of NAT holds seq . n <> 0c ; ::_thesis: seq is non-zero
then  for x being set st x in NAT holds
seq . x <> 0c ;
hence  seq is non-zero by Th3; ::_thesis: verum
end;

theorem :: COMSEQ_1:5
for IT being non-zero Complex_Sequence holds rng IT c= COMPLEX \ {0c}
proof
let IT be non-zero Complex_Sequence; ::_thesis: rng IT c= COMPLEX \ {0c}
 not 0c in rng IT by RELAT_1:def_9;
hence  rng IT c= COMPLEX \ {0c} by ZFMISC_1:34; ::_thesis: verum
end;

theorem :: COMSEQ_1:6
for r being Element of COMPLEX ex seq being Complex_Sequence st rng seq = {r}
proof
let r be Element of COMPLEX ; ::_thesis: ex seq being Complex_Sequence st rng seq = {r}
consider f being Function such that
A1: dom f = NAT and
A2: rng f = {r} by FUNCT_1:5;
now__::_thesis:_for_x_being_set_st_x_in_{r}_holds_
x_in_COMPLEX
let x be set ; ::_thesis: ( x in {r} implies x in COMPLEX )
assume  x in {r} ; ::_thesis: x in COMPLEX
then  x = r by TARSKI:def_1;
hence  x in COMPLEX ; ::_thesis: verum
end;
then  rng f c= COMPLEX by A2, TARSKI:def_3;
then reconsider f = f as Complex_Sequence by A1, FUNCT_2:def_1, RELSET_1:4;
take  f ; ::_thesis: rng f = {r}
thus  rng f = {r} by A2; ::_thesis: verum
end;

theorem Th7: :: COMSEQ_1:7
for seq1, seq2, seq3 being Complex_Sequence holds (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)
proof
let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_+_seq2)_+_seq3)_._n_=_(seq1_+_(seq2_+_seq3))_._n
let n be Element of NAT ; ::_thesis: ((seq1 + seq2) + seq3) . n = (seq1 + (seq2 + seq3)) . n
thus ((seq1 + seq2) + seq3) . n = ((seq1 + seq2) . 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 ; ::_thesis: verum
end;
hence  (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th8: :: COMSEQ_1:8
for seq1, seq2, seq3 being Complex_Sequence holds (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3)
proof
let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_(#)_seq2)_(#)_seq3)_._n_=_(seq1_(#)_(seq2_(#)_seq3))_._n
let n be Element of NAT ; ::_thesis: ((seq1 (#) seq2) (#) seq3) . n = (seq1 (#) (seq2 (#) seq3)) . 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 ; ::_thesis: verum
end;
hence  (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th9: :: COMSEQ_1:9
for seq1, seq2, seq3 being Complex_Sequence holds (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3)
proof
let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_+_seq2)_(#)_seq3)_._n_=_((seq1_(#)_seq3)_+_(seq2_(#)_seq3))_._n
let n be Element of NAT ; ::_thesis: ((seq1 + seq2) (#) seq3) . n = ((seq1 (#) seq3) + (seq2 (#) seq3)) . 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 ; ::_thesis: verum
end;
hence  (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_1:10
for seq3, seq1, seq2 being Complex_Sequence holds seq3 (#) (seq1 + seq2) = (seq3 (#) seq1) + (seq3 (#) seq2) by Th9;

theorem :: COMSEQ_1:11
for seq being Complex_Sequence holds - seq = (- 1r) (#) seq ;

theorem Th12: :: COMSEQ_1:12
for r being Element of COMPLEX
for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2
proof
let r be Element of COMPLEX ; ::_thesis: for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2
let seq1, seq2 be Complex_Sequence; ::_thesis: r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2
now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(seq1_(#)_seq2))_._n_=_((r_(#)_seq1)_(#)_seq2)_._n
let n be Element of NAT ; ::_thesis: (r (#) (seq1 (#) seq2)) . n = ((r (#) seq1) (#) seq2) . 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 ; ::_thesis: verum
end;
hence  r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2 by FUNCT_2:63; ::_thesis: verum
end;

theorem Th13: :: COMSEQ_1:13
for r being Element of COMPLEX
for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)
proof
let r be Element of COMPLEX ; ::_thesis: for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)
let seq1, seq2 be Complex_Sequence; ::_thesis: r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(seq1_(#)_seq2))_._n_=_(seq1_(#)_(r_(#)_seq2))_._n
let n be Element of NAT ; ::_thesis: (r (#) (seq1 (#) seq2)) . n = (seq1 (#) (r (#) seq2)) . 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 ; ::_thesis: verum
end;
hence  r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th14: :: COMSEQ_1:14
for seq1, seq2, seq3 being Complex_Sequence holds (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) - (seq2 (#) seq3)
proof
let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) - (seq2 (#) seq3)
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) ; ::_thesis: verum
end;

theorem :: COMSEQ_1:15
for seq3, seq1, seq2 being Complex_Sequence holds (seq3 (#) seq1) - (seq3 (#) seq2) = seq3 (#) (seq1 - seq2) by Th14;

theorem Th16: :: COMSEQ_1:16
for r being Element of COMPLEX
for seq1, seq2 being Complex_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2)
proof
let r be Element of COMPLEX ; ::_thesis: for seq1, seq2 being Complex_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2)
let seq1, seq2 be Complex_Sequence; ::_thesis: r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(seq1_+_seq2))_._n_=_((r_(#)_seq1)_+_(r_(#)_seq2))_._n
let n be Element of NAT ; ::_thesis: (r (#) (seq1 + seq2)) . n = ((r (#) seq1) + (r (#) seq2)) . 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 ; ::_thesis: verum
end;
hence  r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th17: :: COMSEQ_1:17
for r, p being Element of COMPLEX
for seq being Complex_Sequence holds (r * p) (#) seq = r (#) (p (#) seq)
proof
let r, p be Element of COMPLEX ; ::_thesis: for seq being Complex_Sequence holds (r * p) (#) seq = r (#) (p (#) seq)
let seq be Complex_Sequence; ::_thesis: (r * p) (#) seq = r (#) (p (#) seq)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_*_p)_(#)_seq)_._n_=_(r_(#)_(p_(#)_seq))_._n
let n be Element of NAT ; ::_thesis: ((r * p) (#) seq) . n = (r (#) (p (#) seq)) . 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 ; ::_thesis: verum
end;
hence  (r * p) (#) seq = r (#) (p (#) seq) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th18: :: COMSEQ_1:18
for r being Element of COMPLEX
for seq1, seq2 being Complex_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2)
proof
let r be Element of COMPLEX ; ::_thesis: for seq1, seq2 being Complex_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2)
let seq1, seq2 be Complex_Sequence; ::_thesis: r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2)
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) ; ::_thesis: verum
end;

theorem :: COMSEQ_1:19
for r being Element of COMPLEX
for seq1, seq being Complex_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq
proof
let r be Element of COMPLEX ; ::_thesis: for seq1, seq being Complex_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq
let seq1, seq be Complex_Sequence; ::_thesis: r (#) (seq1 /" seq) = (r (#) seq1) /" seq
thus r (#) (seq1 /" seq) = r (#) (seq1 (#) (seq "))
.= (r (#) seq1) /" seq by Th12 ; ::_thesis: verum
end;

theorem :: COMSEQ_1:20
for seq1, seq2, seq3 being Complex_Sequence holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
proof
let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
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 ; ::_thesis: verum
end;

theorem :: COMSEQ_1:21
for seq being Complex_Sequence holds 1r (#) seq = seq
proof
let seq be Complex_Sequence; ::_thesis: 1r (#) seq = seq
now__::_thesis:_for_n_being_Element_of_NAT_holds_(1r_(#)_seq)_._n_=_seq_._n
let n be Element of NAT ; ::_thesis: (1r (#) seq) . n = seq . n
thus (1r (#) seq) . n = 1r * (seq . n) by VALUED_1:6
.= seq . n ; ::_thesis: verum
end;
hence  1r (#) seq = seq by FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_1:22
for seq being Complex_Sequence holds - (- seq) = seq ;

theorem :: COMSEQ_1:23
for seq1, seq2 being Complex_Sequence holds seq1 - (- seq2) = seq1 + seq2 ;

theorem :: COMSEQ_1:24
for seq1, seq2, seq3 being Complex_Sequence holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
proof
let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
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 ; ::_thesis: verum
end;

theorem :: COMSEQ_1:25
for seq1, seq2, seq3 being Complex_Sequence holds seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3
proof
let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3
thus seq1 + (seq2 - seq3) = seq1 + (seq2 + (- seq3))
.= (seq1 + seq2) - seq3 by Th7 ; ::_thesis: verum
end;

theorem :: COMSEQ_1:26
for seq1, seq2 being Complex_Sequence holds
( (- seq1) (#) seq2 = - (seq1 (#) seq2) & seq1 (#) (- seq2) = - (seq1 (#) seq2) )
proof
let seq1, seq2 be Complex_Sequence; ::_thesis: ( (- seq1) (#) seq2 = - (seq1 (#) seq2) & seq1 (#) (- seq2) = - (seq1 (#) seq2) )
thus (- seq1) (#) seq2 = ((- 1r) (#) seq1) (#) seq2
.= (- 1r) (#) (seq1 (#) seq2) by Th12
.= - (seq1 (#) seq2) ; ::_thesis: seq1 (#) (- seq2) = - (seq1 (#) seq2)
thus seq1 (#) (- seq2) = seq1 (#) ((- 1r) (#) seq2)
.= (- 1r) (#) (seq1 (#) seq2) by Th13
.= - (seq1 (#) seq2) ; ::_thesis: verum
end;

theorem Th27: :: COMSEQ_1:27
for seq being Complex_Sequence st seq is non-zero holds
seq " is non-zero
proof
let seq be Complex_Sequence; ::_thesis: ( seq is non-zero implies seq " is non-zero )
assume that
A1: seq is non-zero and
A2: not seq " is non-zero ; ::_thesis: contradiction
consider n1 being Element of NAT  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; ::_thesis: verum
end;

theorem :: COMSEQ_1:28
canceled;

theorem Th29: :: COMSEQ_1:29
for seq, seq1 being Complex_Sequence holds
( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero )
proof
let seq, seq1 be Complex_Sequence; ::_thesis: ( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero )
thus  ( seq is non-zero & seq1 is non-zero implies seq (#) seq1 is non-zero ) ::_thesis: ( seq (#) seq1 is non-zero implies ( seq is non-zero & seq1 is non-zero ) )
proof
assume A1: ( seq is non-zero & seq1 is non-zero ) ; ::_thesis: seq (#) seq1 is non-zero
now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_(#)_seq1)_._n_<>_0c
let n be Element of NAT ; ::_thesis: (seq (#) seq1) . n <> 0c
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; ::_thesis: verum
end;
hence  seq (#) seq1 is non-zero by Th4; ::_thesis: verum
end;
assume A3: seq (#) seq1 is non-zero ; ::_thesis: ( seq is non-zero & seq1 is non-zero )
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._n_<>_0c
let n be Element of NAT ; ::_thesis: seq . n <> 0c
 (seq (#) seq1) . n = (seq . n) * (seq1 . n) by VALUED_1:5;
hence  seq . n <> 0c by A3, Th4; ::_thesis: verum
end;
hence  seq is non-zero by Th4; ::_thesis: seq1 is non-zero
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_<>_0c
let n be Element of NAT ; ::_thesis: seq1 . n <> 0c
 (seq (#) seq1) . n = (seq . n) * (seq1 . n) by VALUED_1:5;
hence  seq1 . n <> 0c by A3, Th4; ::_thesis: verum
end;
hence  seq1 is non-zero by Th4; ::_thesis: verum
end;

theorem Th30: :: COMSEQ_1:30
for seq, seq1 being Complex_Sequence holds (seq ") (#) (seq1 ") = (seq (#) seq1) "
proof
let seq, seq1 be Complex_Sequence; ::_thesis: (seq ") (#) (seq1 ") = (seq (#) seq1) "
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_")_(#)_(seq1_"))_._n_=_((seq_(#)_seq1)_")_._n
let n be Element of NAT ; ::_thesis: ((seq ") (#) (seq1 ")) . n = ((seq (#) seq1) ") . 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 ; ::_thesis: verum
end;
hence  (seq ") (#) (seq1 ") = (seq (#) seq1) " by FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_1:31
for seq, seq1 being Complex_Sequence st seq is non-zero holds
(seq1 /" seq) (#) seq = seq1
proof
let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is non-zero implies (seq1 /" seq) (#) seq = seq1 )
assume A1: seq is non-zero ; ::_thesis: (seq1 /" seq) (#) seq = seq1
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_/"_seq)_(#)_seq)_._n_=_seq1_._n
let n be Element of NAT ; ::_thesis: ((seq1 /" seq) (#) seq) . n = seq1 . 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 ; ::_thesis: verum
end;
hence  (seq1 /" seq) (#) seq = seq1 by FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_1:32
for seq9, seq, seq19, seq1 being Complex_Sequence holds (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1)
proof
let seq9, seq, seq19, seq1 be Complex_Sequence; ::_thesis: (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq9_/"_seq)_(#)_(seq19_/"_seq1))_._n_=_((seq9_(#)_seq19)_/"_(seq_(#)_seq1))_._n
let n be Element of NAT ; ::_thesis: ((seq9 /" seq) (#) (seq19 /" seq1)) . n = ((seq9 (#) seq19) /" (seq (#) seq1)) . 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 Th30
.= ((seq9 (#) seq19) . n) * (((seq (#) seq1) ") . n) by VALUED_1:5
.= ((seq9 (#) seq19) /" (seq (#) seq1)) . n by VALUED_1:5 ; ::_thesis: verum
end;
hence  (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_1:33
for seq, seq1 being Complex_Sequence st seq is non-zero & seq1 is non-zero holds
seq /" seq1 is non-zero
proof
let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is non-zero & seq1 is non-zero implies seq /" seq1 is non-zero )
assume that
A1: seq is non-zero and
A2: seq1 is non-zero ; ::_thesis: seq /" seq1 is non-zero
 seq1 " is non-zero by A2, Th27;
hence  seq /" seq1 is non-zero by A1, Th29; ::_thesis: verum
end;

theorem Th34: :: COMSEQ_1:34
for seq, seq1 being Complex_Sequence holds (seq /" seq1) " = seq1 /" seq
proof
let seq, seq1 be Complex_Sequence; ::_thesis: (seq /" seq1) " = seq1 /" seq
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_/"_seq1)_")_._n_=_(seq1_/"_seq)_._n
let n be Element of NAT ; ::_thesis: ((seq /" seq1) ") . n = (seq1 /" seq) . n
thus ((seq /" seq1) ") . n = ((seq ") (#) ((seq1 ") ")) . n by Th30
.= (seq1 /" seq) . n ; ::_thesis: verum
end;
hence  (seq /" seq1) " = seq1 /" seq by FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_1:35
for seq2, seq1, seq being Complex_Sequence holds seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq
proof
let seq2, seq1, seq be Complex_Sequence; ::_thesis: seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq
thus seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) (#) (seq ") by Th8
.= (seq2 (#) seq1) /" seq ; ::_thesis: verum
end;

theorem :: COMSEQ_1:36
for seq2, seq, seq1 being Complex_Sequence holds seq2 /" (seq /" seq1) = (seq2 (#) seq1) /" seq
proof
let seq2, seq, seq1 be Complex_Sequence; ::_thesis: seq2 /" (seq /" seq1) = (seq2 (#) seq1) /" seq
now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq2_/"_(seq_/"_seq1))_._n_=_((seq2_(#)_seq1)_/"_seq)_._n
let n be Element of NAT ; ::_thesis: (seq2 /" (seq /" seq1)) . n = ((seq2 (#) seq1) /" seq) . n
thus (seq2 /" (seq /" seq1)) . n = (seq2 (#) (seq1 /" seq)) . n by Th34
.= ((seq2 (#) seq1) (#) (seq ")) . n by Th8
.= ((seq2 (#) seq1) /" seq) . n ; ::_thesis: verum
end;
hence  seq2 /" (seq /" seq1) = (seq2 (#) seq1) /" seq by FUNCT_2:63; ::_thesis: verum
end;

theorem Th37: :: COMSEQ_1:37
for seq1, seq2, seq being Complex_Sequence st seq1 is non-zero holds
seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1)
proof
let seq1, seq2, seq be Complex_Sequence; ::_thesis: ( seq1 is non-zero implies seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1) )
assume A1: seq1 is non-zero ; ::_thesis: seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq2_/"_seq)_._n_=_((seq2_(#)_seq1)_/"_(seq_(#)_seq1))_._n
let n be Element of NAT ; ::_thesis: (seq2 /" seq) . n = ((seq2 (#) seq1) /" (seq (#) seq1)) . 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 Th30
.= ((seq2 (#) seq1) /" (seq (#) seq1)) . n by VALUED_1:5 ; ::_thesis: verum
end;
hence  seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th38: :: COMSEQ_1:38
for r being Element of COMPLEX
for seq being Complex_Sequence st r <> 0c & seq is non-zero holds
r (#) seq is non-zero
proof
let r be Element of COMPLEX ; ::_thesis: for seq being Complex_Sequence st r <> 0c & seq is non-zero holds
r (#) seq is non-zero
let seq be Complex_Sequence; ::_thesis: ( r <> 0c & seq is non-zero implies r (#) seq is non-zero )
assume that
A1: r <> 0c and
A2: seq is non-zero and
A3: not r (#) seq is non-zero ; ::_thesis: contradiction
consider n1 being Element of NAT  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; ::_thesis: verum
end;

theorem :: COMSEQ_1:39
for seq being Complex_Sequence st seq is non-zero holds
- seq is non-zero
proof
let seq be Complex_Sequence; ::_thesis: ( seq is non-zero implies - seq is non-zero )
A1: - (- 1r) = 1r ;
assume  seq is non-zero ; ::_thesis: - seq is non-zero
hence  - seq is non-zero by A1, Th38; ::_thesis: verum
end;

theorem Th40: :: COMSEQ_1:40
for r being Element of COMPLEX
for seq being Complex_Sequence holds (r (#) seq) " = (r ") (#) (seq ")
proof
let r be Element of COMPLEX ; ::_thesis: for seq being Complex_Sequence holds (r (#) seq) " = (r ") (#) (seq ")
let seq be Complex_Sequence; ::_thesis: (r (#) seq) " = (r ") (#) (seq ")
now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_(#)_seq)_")_._n_=_((r_")_(#)_(seq_"))_._n
let n be Element of NAT ; ::_thesis: ((r (#) seq) ") . n = ((r ") (#) (seq ")) . 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 ; ::_thesis: verum
end;
hence  (r (#) seq) " = (r ") (#) (seq ") by FUNCT_2:63; ::_thesis: verum
end;

theorem Th41: :: COMSEQ_1:41
for seq being Complex_Sequence st seq is non-zero holds
(- seq) " = (- 1r) (#) (seq ")
proof
let seq be Complex_Sequence; ::_thesis: ( seq is non-zero implies (- seq) " = (- 1r) (#) (seq ") )
 (- 1) " = - 1 ;
hence  ( seq is non-zero implies (- seq) " = (- 1r) (#) (seq ") ) by Th40; ::_thesis: verum
end;

theorem :: COMSEQ_1:42
for seq, seq1 being Complex_Sequence st seq is non-zero holds
( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) )
proof
let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is non-zero implies ( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) ) )
assume A1: seq is non-zero ; ::_thesis: ( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) )
thus  - (seq1 /" seq) = (- 1r) (#) (seq1 /" seq)
.= ((- 1r) (#) seq1) (#) (seq ") by Th12
.= (- seq1) /" seq ; ::_thesis: seq1 /" (- seq) = - (seq1 /" seq)
thus seq1 /" (- seq) = seq1 (#) ((- 1r) (#) (seq ")) by A1, Th41
.= (- 1r) (#) (seq1 (#) (seq ")) by Th13
.= - (seq1 /" seq) ; ::_thesis: verum
end;

theorem :: COMSEQ_1:43
for seq1, seq, seq19 being Complex_Sequence holds
( (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) /" seq & (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq )
proof
let seq1, seq, seq19 be Complex_Sequence; ::_thesis: ( (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) /" seq & (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq )
thus (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) (#) (seq ") by Th9
.= (seq1 + seq19) /" seq ; ::_thesis: (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq
thus (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) (#) (seq ") by Th14
.= (seq1 - seq19) /" seq ; ::_thesis: verum
end;

theorem :: COMSEQ_1:44
for seq, seq9, seq1, seq19 being Complex_Sequence st seq is non-zero & seq9 is non-zero holds
( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) )
proof
let seq, seq9, seq1, seq19 be Complex_Sequence; ::_thesis: ( 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) ) )
assume that
A1: seq is non-zero and
A2: seq9 is non-zero ; ::_thesis: ( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) )
thus (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) /" (seq (#) seq9)) + (seq19 /" seq9) by A2, Th37
.= ((seq1 (#) seq9) /" (seq (#) seq9)) + ((seq19 (#) seq) /" (seq (#) seq9)) by A1, Th37
.= ((seq1 (#) seq9) + (seq19 (#) seq)) (#) ((seq (#) seq9) ") by Th9
.= ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) ; ::_thesis: (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9)
thus (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) /" (seq (#) seq9)) - (seq19 /" seq9) by A2, Th37
.= ((seq1 (#) seq9) /" (seq (#) seq9)) - ((seq19 (#) seq) /" (seq (#) seq9)) by A1, Th37
.= ((seq1 (#) seq9) - (seq19 (#) seq)) (#) ((seq (#) seq9) ") by Th14
.= ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) ; ::_thesis: verum
end;

theorem :: COMSEQ_1:45
for seq19, seq, seq9, seq1 being Complex_Sequence holds (seq19 /" seq) /" (seq9 /" seq1) = (seq19 (#) seq1) /" (seq (#) seq9)
proof
let seq19, seq, seq9, seq1 be Complex_Sequence; ::_thesis: (seq19 /" seq) /" (seq9 /" seq1) = (seq19 (#) seq1) /" (seq (#) seq9)
thus (seq19 /" seq) /" (seq9 /" seq1) = (seq19 /" seq) (#) ((seq9 ") (#) ((seq1 ") ")) by Th30
.= ((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 Th30 ; ::_thesis: verum
end;

theorem Th46: :: COMSEQ_1:46
for seq, seq9 being Complex_Sequence holds |.(seq (#) seq9).| = |.seq.| (#) |.seq9.|
proof
let seq, seq9 be Complex_Sequence; ::_thesis: |.(seq (#) seq9).| = |.seq.| (#) |.seq9.|
now__::_thesis:_for_n_being_Element_of_NAT_holds_|.(seq_(#)_seq9).|_._n_=_(|.seq.|_(#)_|.seq9.|)_._n
let n be Element of NAT ; ::_thesis: |.(seq (#) seq9).| . n = (|.seq.| (#) |.seq9.|) . 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 ; ::_thesis: verum
end;
hence  |.(seq (#) seq9).| = |.seq.| (#) |.seq9.| by FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_1:47
for seq being Complex_Sequence st seq is non-zero holds
|.seq.| is non-zero
proof
let seq be Complex_Sequence; ::_thesis: ( seq is non-zero implies |.seq.| is non-zero )
assume A1: seq is non-zero ; ::_thesis: |.seq.| is non-zero
now__::_thesis:_for_n_being_Element_of_NAT_holds_|.seq.|_._n_<>_0
let n be Element of NAT ; ::_thesis: |.seq.| . n <> 0
 seq . n <> 0c by A1, Th4;
then  |.(seq . n).| <> 0 by COMPLEX1:45;
hence  |.seq.| . n <> 0 by VALUED_1:18; ::_thesis: verum
end;
hence  |.seq.| is non-zero by SEQ_1:5; ::_thesis: verum
end;

theorem Th48: :: COMSEQ_1:48
for seq being Complex_Sequence holds |.seq.| " = |.(seq ").|
proof
let seq be Complex_Sequence; ::_thesis: |.seq.| " = |.(seq ").|
now__::_thesis:_for_n_being_Element_of_NAT_holds_|.(seq_").|_._n_=_(|.seq.|_")_._n
let n be Element of NAT ; ::_thesis: |.(seq ").| . n = (|.seq.| ") . 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, COMPLEX1:67
.= |.(seq . n).| " by XCMPLX_1:215
.= (|.seq.| . n) " by VALUED_1:18
.= (|.seq.| ") . n by VALUED_1:10 ; ::_thesis: verum
end;
hence  |.seq.| " = |.(seq ").| by FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_1:49
for seq9, seq being Complex_Sequence holds |.(seq9 /" seq).| = |.seq9.| /" |.seq.|
proof
let seq9, seq be Complex_Sequence; ::_thesis: |.(seq9 /" seq).| = |.seq9.| /" |.seq.|
thus |.(seq9 /" seq).| = |.seq9.| (#) |.(seq ").| by Th46
.= |.seq9.| /" |.seq.| by Th48 ; ::_thesis: verum
end;

theorem :: COMSEQ_1:50
for r being Element of COMPLEX
for seq being Complex_Sequence holds |.(r (#) seq).| = |.r.| (#) |.seq.|
proof
let r be Element of COMPLEX ; ::_thesis: for seq being Complex_Sequence holds |.(r (#) seq).| = |.r.| (#) |.seq.|
let seq be Complex_Sequence; ::_thesis: |.(r (#) seq).| = |.r.| (#) |.seq.|
now__::_thesis:_for_n_being_Element_of_NAT_holds_|.(r_(#)_seq).|_._n_=_(|.r.|_(#)_|.seq.|)_._n
let n be Element of NAT ; ::_thesis: |.(r (#) seq).| . n = (|.r.| (#) |.seq.|) . 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 ; ::_thesis: verum
end;
hence  |.(r (#) seq).| = |.r.| (#) |.seq.| by FUNCT_2:63; ::_thesis: verum
end;