:: CLVECT_3 semantic presentation

begin

                deffunc H1( ComplexUnitarySpace) ->  Element of the U1 of $1 = 0. $1;

theorem Th1: :: CLVECT_3:1
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X holds (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2)
let seq1, seq2 be sequence of X; ::_thesis: (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2)
set PSseq1 = Partial_Sums seq1;
set PSseq2 = Partial_Sums seq2;
A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_seq1)_+_(Partial_Sums_seq2))_._(n_+_1)_=_(((Partial_Sums_seq1)_+_(Partial_Sums_seq2))_._n)_+_((seq1_+_seq2)_._(n_+_1))
let n be Element of NAT ; ::_thesis: ((Partial_Sums seq1) + (Partial_Sums seq2)) . (n + 1) = (((Partial_Sums seq1) + (Partial_Sums seq2)) . n) + ((seq1 + seq2) . (n + 1))
thus ((Partial_Sums seq1) + (Partial_Sums seq2)) . (n + 1) = ((Partial_Sums seq1) . (n + 1)) + ((Partial_Sums seq2) . (n + 1)) by NORMSP_1:def_2
.= (((Partial_Sums seq1) . n) + (seq1 . (n + 1))) + ((Partial_Sums seq2) . (n + 1)) by BHSP_4:def_1
.= (((Partial_Sums seq1) . n) + (seq1 . (n + 1))) + ((seq2 . (n + 1)) + ((Partial_Sums seq2) . n)) by BHSP_4:def_1
.= ((((Partial_Sums seq1) . n) + (seq1 . (n + 1))) + (seq2 . (n + 1))) + ((Partial_Sums seq2) . n) by RLVECT_1:def_3
.= (((Partial_Sums seq1) . n) + ((seq1 . (n + 1)) + (seq2 . (n + 1)))) + ((Partial_Sums seq2) . n) by RLVECT_1:def_3
.= (((Partial_Sums seq1) . n) + ((seq1 + seq2) . (n + 1))) + ((Partial_Sums seq2) . n) by NORMSP_1:def_2
.= (((Partial_Sums seq1) . n) + ((Partial_Sums seq2) . n)) + ((seq1 + seq2) . (n + 1)) by RLVECT_1:def_3
.= (((Partial_Sums seq1) + (Partial_Sums seq2)) . n) + ((seq1 + seq2) . (n + 1)) by NORMSP_1:def_2 ; ::_thesis: verum
end;
((Partial_Sums seq1) + (Partial_Sums seq2)) . 0 = ((Partial_Sums seq1) . 0) + ((Partial_Sums seq2) . 0) by NORMSP_1:def_2
.= (seq1 . 0) + ((Partial_Sums seq2) . 0) by BHSP_4:def_1
.= (seq1 . 0) + (seq2 . 0) by BHSP_4:def_1
.= (seq1 + seq2) . 0 by NORMSP_1:def_2 ;
hence  (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) by A1, BHSP_4:def_1; ::_thesis: verum
end;

theorem Th2: :: CLVECT_3:2
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X holds (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2)
let seq1, seq2 be sequence of X; ::_thesis: (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2)
set PSseq1 = Partial_Sums seq1;
set PSseq2 = Partial_Sums seq2;
A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_seq1)_-_(Partial_Sums_seq2))_._(n_+_1)_=_(((Partial_Sums_seq1)_-_(Partial_Sums_seq2))_._n)_+_((seq1_-_seq2)_._(n_+_1))
let n be Element of NAT ; ::_thesis: ((Partial_Sums seq1) - (Partial_Sums seq2)) . (n + 1) = (((Partial_Sums seq1) - (Partial_Sums seq2)) . n) + ((seq1 - seq2) . (n + 1))
thus ((Partial_Sums seq1) - (Partial_Sums seq2)) . (n + 1) = ((Partial_Sums seq1) . (n + 1)) - ((Partial_Sums seq2) . (n + 1)) by NORMSP_1:def_3
.= (((Partial_Sums seq1) . n) + (seq1 . (n + 1))) - ((Partial_Sums seq2) . (n + 1)) by BHSP_4:def_1
.= (((Partial_Sums seq1) . n) + (seq1 . (n + 1))) - ((seq2 . (n + 1)) + ((Partial_Sums seq2) . n)) by BHSP_4:def_1
.= ((((Partial_Sums seq1) . n) + (seq1 . (n + 1))) - (seq2 . (n + 1))) - ((Partial_Sums seq2) . n) by RLVECT_1:27
.= (((Partial_Sums seq1) . n) + ((seq1 . (n + 1)) - (seq2 . (n + 1)))) - ((Partial_Sums seq2) . n) by RLVECT_1:def_3
.= (((Partial_Sums seq1) . n) - ((Partial_Sums seq2) . n)) + ((seq1 . (n + 1)) - (seq2 . (n + 1))) by RLVECT_1:def_3
.= (((Partial_Sums seq1) - (Partial_Sums seq2)) . n) + ((seq1 . (n + 1)) - (seq2 . (n + 1))) by NORMSP_1:def_3
.= (((Partial_Sums seq1) - (Partial_Sums seq2)) . n) + ((seq1 - seq2) . (n + 1)) by NORMSP_1:def_3 ; ::_thesis: verum
end;
((Partial_Sums seq1) - (Partial_Sums seq2)) . 0 = ((Partial_Sums seq1) . 0) - ((Partial_Sums seq2) . 0) by NORMSP_1:def_3
.= (seq1 . 0) - ((Partial_Sums seq2) . 0) by BHSP_4:def_1
.= (seq1 . 0) - (seq2 . 0) by BHSP_4:def_1
.= (seq1 - seq2) . 0 by NORMSP_1:def_3 ;
hence  (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2) by A1, BHSP_4:def_1; ::_thesis: verum
end;

theorem Th3: :: CLVECT_3:3
for X being ComplexUnitarySpace
for seq being sequence of X
for z being Complex holds Partial_Sums (z * seq) = z * (Partial_Sums seq)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for z being Complex holds Partial_Sums (z * seq) = z * (Partial_Sums seq)
let seq be sequence of X; ::_thesis: for z being Complex holds Partial_Sums (z * seq) = z * (Partial_Sums seq)
let z be Complex; ::_thesis: Partial_Sums (z * seq) = z * (Partial_Sums seq)
set PSseq = Partial_Sums seq;
A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_(z_*_(Partial_Sums_seq))_._(n_+_1)_=_((z_*_(Partial_Sums_seq))_._n)_+_((z_*_seq)_._(n_+_1))
let n be Element of NAT ; ::_thesis: (z * (Partial_Sums seq)) . (n + 1) = ((z * (Partial_Sums seq)) . n) + ((z * seq) . (n + 1))
thus (z * (Partial_Sums seq)) . (n + 1) = z * ((Partial_Sums seq) . (n + 1)) by CLVECT_1:def_14
.= z * (((Partial_Sums seq) . n) + (seq . (n + 1))) by BHSP_4:def_1
.= (z * ((Partial_Sums seq) . n)) + (z * (seq . (n + 1))) by CLVECT_1:def_2
.= ((z * (Partial_Sums seq)) . n) + (z * (seq . (n + 1))) by CLVECT_1:def_14
.= ((z * (Partial_Sums seq)) . n) + ((z * seq) . (n + 1)) by CLVECT_1:def_14 ; ::_thesis: verum
end;
(z * (Partial_Sums seq)) . 0 = z * ((Partial_Sums seq) . 0) by CLVECT_1:def_14
.= z * (seq . 0) by BHSP_4:def_1
.= (z * seq) . 0 by CLVECT_1:def_14 ;
hence  Partial_Sums (z * seq) = z * (Partial_Sums seq) by A1, BHSP_4:def_1; ::_thesis: verum
end;

theorem :: CLVECT_3:4
for X being ComplexUnitarySpace
for seq being sequence of X holds Partial_Sums (- seq) = - (Partial_Sums seq)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds Partial_Sums (- seq) = - (Partial_Sums seq)
let seq be sequence of X; ::_thesis: Partial_Sums (- seq) = - (Partial_Sums seq)
 Partial_Sums ((- 1r) * seq) = (- 1r) * (Partial_Sums seq) by Th3;
then  Partial_Sums (- seq) = (- 1r) * (Partial_Sums seq) by CSSPACE:70;
hence  Partial_Sums (- seq) = - (Partial_Sums seq) by CSSPACE:70; ::_thesis: verum
end;

theorem :: CLVECT_3:5
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X
for z1, z2 being Complex holds (z1 * (Partial_Sums seq1)) + (z2 * (Partial_Sums seq2)) = Partial_Sums ((z1 * seq1) + (z2 * seq2))
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X
for z1, z2 being Complex holds (z1 * (Partial_Sums seq1)) + (z2 * (Partial_Sums seq2)) = Partial_Sums ((z1 * seq1) + (z2 * seq2))
let seq1, seq2 be sequence of X; ::_thesis: for z1, z2 being Complex holds (z1 * (Partial_Sums seq1)) + (z2 * (Partial_Sums seq2)) = Partial_Sums ((z1 * seq1) + (z2 * seq2))
let z1, z2 be Complex; ::_thesis: (z1 * (Partial_Sums seq1)) + (z2 * (Partial_Sums seq2)) = Partial_Sums ((z1 * seq1) + (z2 * seq2))
thus (z1 * (Partial_Sums seq1)) + (z2 * (Partial_Sums seq2)) = (Partial_Sums (z1 * seq1)) + (z2 * (Partial_Sums seq2)) by Th3
.= (Partial_Sums (z1 * seq1)) + (Partial_Sums (z2 * seq2)) by Th3
.= Partial_Sums ((z1 * seq1) + (z2 * seq2)) by Th1 ; ::_thesis: verum
end;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
attrseq is summable  means :Def1: :: CLVECT_3:def 1
 Partial_Sums seq is convergent ;
func Sum seq ->  Point of X equals :: CLVECT_3:def 2
 lim (Partial_Sums seq);
correctness
coherence
lim (Partial_Sums seq) is Point of X;
;
end;

:: deftheorem Def1 defines summable CLVECT_3:def_1_:_
 for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is summable iff Partial_Sums seq is convergent );

:: deftheorem  defines Sum CLVECT_3:def_2_:_
 for X being ComplexUnitarySpace
for seq being sequence of X holds Sum seq = lim (Partial_Sums seq);

theorem :: CLVECT_3:6
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is summable & seq2 is summable implies ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) )
assume  ( seq1 is summable & seq2 is summable ) ; ::_thesis: ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )
then A1: ( Partial_Sums seq1 is convergent & Partial_Sums seq2 is convergent ) by Def1;
then  (Partial_Sums seq1) + (Partial_Sums seq2) is convergent by CLVECT_2:3;
then  Partial_Sums (seq1 + seq2) is convergent by Th1;
hence  seq1 + seq2 is summable by Def1; ::_thesis: Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2)
thus  Sum (seq1 + seq2) = lim ((Partial_Sums seq1) + (Partial_Sums seq2)) by Th1
.= (Sum seq1) + (Sum seq2) by A1, CLVECT_2:13 ; ::_thesis: verum
end;

theorem :: CLVECT_3:7
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is summable & seq2 is summable implies ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) ) )
assume  ( seq1 is summable & seq2 is summable ) ; ::_thesis: ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )
then A1: ( Partial_Sums seq1 is convergent & Partial_Sums seq2 is convergent ) by Def1;
then  (Partial_Sums seq1) - (Partial_Sums seq2) is convergent by CLVECT_2:4;
then  Partial_Sums (seq1 - seq2) is convergent by Th2;
hence  seq1 - seq2 is summable by Def1; ::_thesis: Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2)
thus  Sum (seq1 - seq2) = lim ((Partial_Sums seq1) - (Partial_Sums seq2)) by Th2
.= (Sum seq1) - (Sum seq2) by A1, CLVECT_2:14 ; ::_thesis: verum
end;

theorem :: CLVECT_3:8
for X being ComplexUnitarySpace
for seq being sequence of X
for z being Complex st seq is summable holds
( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for z being Complex st seq is summable holds
( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
let seq be sequence of X; ::_thesis: for z being Complex st seq is summable holds
( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
let z be Complex; ::_thesis: ( seq is summable implies ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) )
assume  seq is summable ; ::_thesis: ( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
then A1: Partial_Sums seq is convergent by Def1;
then  z * (Partial_Sums seq) is convergent by CLVECT_2:5;
then  Partial_Sums (z * seq) is convergent by Th3;
hence  z * seq is summable by Def1; ::_thesis: Sum (z * seq) = z * (Sum seq)
thus  Sum (z * seq) = lim (z * (Partial_Sums seq)) by Th3
.= z * (Sum seq) by A1, CLVECT_2:15 ; ::_thesis: verum
end;

theorem Th9: :: CLVECT_3:9
for X being ComplexUnitarySpace
for seq being sequence of X st seq is summable holds
( seq is convergent & lim seq = 0. X )
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st seq is summable holds
( seq is convergent & lim seq = 0. X )
let seq be sequence of X; ::_thesis: ( seq is summable implies ( seq is convergent & lim seq = 0. X ) )
set PSseq = Partial_Sums seq;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_seq)_^\_1)_._n_=_((Partial_Sums_seq)_._n)_+_((seq_^\_1)_._n)
let n be Element of NAT ; ::_thesis: ((Partial_Sums seq) ^\ 1) . n = ((Partial_Sums seq) . n) + ((seq ^\ 1) . n)
(Partial_Sums seq) . (n + 1) = ((Partial_Sums seq) . n) + (seq . (n + 1)) by BHSP_4:def_1
.= ((Partial_Sums seq) . n) + ((seq ^\ 1) . n) by NAT_1:def_3 ;
hence  ((Partial_Sums seq) ^\ 1) . n = ((Partial_Sums seq) . n) + ((seq ^\ 1) . n) by NAT_1:def_3; ::_thesis: verum
end;
then A1: (Partial_Sums seq) ^\ 1 = (Partial_Sums seq) + (seq ^\ 1) by NORMSP_1:def_2;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_^\_1)_+_((Partial_Sums_seq)_-_(Partial_Sums_seq)))_._n_=_(seq_^\_1)_._n
let n be Element of NAT ; ::_thesis: ((seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq))) . n = (seq ^\ 1) . n
thus ((seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq))) . n = ((seq ^\ 1) . n) + (((Partial_Sums seq) - (Partial_Sums seq)) . n) by NORMSP_1:def_2
.= ((seq ^\ 1) . n) + (((Partial_Sums seq) . n) - ((Partial_Sums seq) . n)) by NORMSP_1:def_3
.= ((seq ^\ 1) . n) + H1(X) by RLVECT_1:15
.= (seq ^\ 1) . n by RLVECT_1:4 ; ::_thesis: verum
end;
then  (seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq)) = seq ^\ 1 by FUNCT_2:63;
then A2: seq ^\ 1 = ((Partial_Sums seq) ^\ 1) - (Partial_Sums seq) by A1, CSSPACE:76;
assume  seq is summable ; ::_thesis: ( seq is convergent & lim seq = 0. X )
then A3: Partial_Sums seq is convergent by Def1;
then A4: (Partial_Sums seq) ^\ 1 is convergent by CLVECT_2:90;
then A5: seq ^\ 1 is convergent by A3, A2, CLVECT_2:4;
hence  seq is convergent by CLVECT_2:91; ::_thesis: lim seq = 0. X
 lim ((Partial_Sums seq) ^\ 1) = lim (Partial_Sums seq) by A3, CLVECT_2:90;
then  lim (((Partial_Sums seq) ^\ 1) - (Partial_Sums seq)) = (lim (Partial_Sums seq)) - (lim (Partial_Sums seq)) by A3, A4, CLVECT_2:14
.= H1(X) by RLVECT_1:15 ;
hence  lim seq = 0. X by A2, A5, CLVECT_2:84, CLVECT_2:91; ::_thesis: verum
end;

theorem Th10: :: CLVECT_3:10
for X being ComplexHilbertSpace
for seq being sequence of X holds
( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r )
proof
let X be ComplexHilbertSpace; ::_thesis: for seq being sequence of X holds
( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r )
let seq be sequence of X; ::_thesis: ( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r )
set PSseq = Partial_Sums seq;
thus  ( seq is summable implies for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) ::_thesis: ( ( for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) implies seq is summable )
proof
assume  seq is summable ; ::_thesis: for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r
then  Partial_Sums seq is convergent by Def1;
then  Partial_Sums seq is Cauchy by CLVECT_2:65;
hence  for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r by CLVECT_2:58; ::_thesis: verum
end;
thus  ( ( for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) implies seq is summable ) ::_thesis: verum
proof
assume  for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ; ::_thesis: seq is summable
then  Partial_Sums seq is Cauchy by CLVECT_2:58;
then  Partial_Sums seq is convergent by CLVECT_2:def_11;
hence  seq is summable by Def1; ::_thesis: verum
end;
end;

theorem :: CLVECT_3:11
for X being ComplexUnitarySpace
for seq being sequence of X st seq is summable holds
Partial_Sums seq is bounded
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st seq is summable holds
Partial_Sums seq is bounded
let seq be sequence of X; ::_thesis: ( seq is summable implies Partial_Sums seq is bounded )
assume  seq is summable ; ::_thesis: Partial_Sums seq is bounded
then  Partial_Sums seq is convergent by Def1;
hence  Partial_Sums seq is bounded by CLVECT_2:80; ::_thesis: verum
end;

theorem Th12: :: CLVECT_3:12
for X being ComplexUnitarySpace
for seq1, seq being sequence of X st ( for n being Element of NAT holds seq1 . n = seq . 0 ) holds
Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq being sequence of X st ( for n being Element of NAT holds seq1 . n = seq . 0 ) holds
Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1
let seq1, seq be sequence of X; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = seq . 0 ) implies Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 )
assume A1: for n being Element of NAT holds seq1 . n = seq . 0 ; ::_thesis: Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1
A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_(((Partial_Sums_seq)_^\_1)_-_seq1)_._(n_+_1)_=_((((Partial_Sums_seq)_^\_1)_-_seq1)_._n)_+_((seq_^\_1)_._(n_+_1))
let n be Element of NAT ; ::_thesis: (((Partial_Sums seq) ^\ 1) - seq1) . (n + 1) = ((((Partial_Sums seq) ^\ 1) - seq1) . n) + ((seq ^\ 1) . (n + 1))
thus (((Partial_Sums seq) ^\ 1) - seq1) . (n + 1) = (((Partial_Sums seq) ^\ 1) . (n + 1)) - (seq1 . (n + 1)) by NORMSP_1:def_3
.= (((Partial_Sums seq) ^\ 1) . (n + 1)) - (seq . 0) by A1
.= ((Partial_Sums seq) . ((n + 1) + 1)) - (seq . 0) by NAT_1:def_3
.= ((seq . ((n + 1) + 1)) + ((Partial_Sums seq) . (n + 1))) - (seq . 0) by BHSP_4:def_1
.= ((seq . ((n + 1) + 1)) + ((Partial_Sums seq) . (n + 1))) - (seq1 . n) by A1
.= (seq . ((n + 1) + 1)) + (((Partial_Sums seq) . (n + 1)) - (seq1 . n)) by RLVECT_1:def_3
.= (seq . ((n + 1) + 1)) + ((((Partial_Sums seq) ^\ 1) . n) - (seq1 . n)) by NAT_1:def_3
.= (seq . ((n + 1) + 1)) + ((((Partial_Sums seq) ^\ 1) - seq1) . n) by NORMSP_1:def_3
.= ((((Partial_Sums seq) ^\ 1) - seq1) . n) + ((seq ^\ 1) . (n + 1)) by NAT_1:def_3 ; ::_thesis: verum
end;
(((Partial_Sums seq) ^\ 1) - seq1) . 0 = (((Partial_Sums seq) ^\ 1) . 0) - (seq1 . 0) by NORMSP_1:def_3
.= (((Partial_Sums seq) ^\ 1) . 0) - (seq . 0) by A1
.= ((Partial_Sums seq) . (0 + 1)) - (seq . 0) by NAT_1:def_3
.= (((Partial_Sums seq) . 0) + (seq . (0 + 1))) - (seq . 0) by BHSP_4:def_1
.= ((seq . (0 + 1)) + (seq . 0)) - (seq . 0) by BHSP_4:def_1
.= (seq . (0 + 1)) + ((seq . 0) - (seq . 0)) by RLVECT_1:def_3
.= (seq . (0 + 1)) + H1(X) by RLVECT_1:15
.= seq . (0 + 1) by RLVECT_1:4
.= (seq ^\ 1) . 0 by NAT_1:def_3 ;
hence  Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 by A2, BHSP_4:def_1; ::_thesis: verum
end;

theorem Th13: :: CLVECT_3:13
for X being ComplexUnitarySpace
for seq being sequence of X st seq is summable holds
for k being Element of NAT holds seq ^\ k is summable
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st seq is summable holds
for k being Element of NAT holds seq ^\ k is summable
let seq be sequence of X; ::_thesis: ( seq is summable implies for k being Element of NAT holds seq ^\ k is summable )
defpred S1[ Element of NAT ] means seq ^\ $1 is summable ;
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
reconsider seq1 = NAT --> ((seq ^\ k) . 0) as sequence of X ;
assume  seq ^\ k is summable ; ::_thesis: S1[k + 1]
then  Partial_Sums (seq ^\ k) is convergent by Def1;
then A2: (Partial_Sums (seq ^\ k)) ^\ 1 is convergent by CLVECT_2:90;
 for m being Element of NAT holds seq1 . m = (seq ^\ k) . 0 by FUNCOP_1:7;
then  ( seq1 is convergent & Partial_Sums ((seq ^\ k) ^\ 1) = ((Partial_Sums (seq ^\ k)) ^\ 1) - seq1 ) by Th12, CLVECT_2:1;
then  ( seq ^\ (k + 1) = (seq ^\ k) ^\ 1 & Partial_Sums ((seq ^\ k) ^\ 1) is convergent ) by A2, CLVECT_2:4, NAT_1:48;
hence  S1[k + 1] by Def1; ::_thesis: verum
end;
assume  seq is summable ; ::_thesis: for k being Element of NAT holds seq ^\ k is summable
then A3: S1[ 0 ] by NAT_1:47;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1); ::_thesis: verum
end;

theorem :: CLVECT_3:14
for X being ComplexUnitarySpace
for seq being sequence of X st ex k being Element of NAT st seq ^\ k is summable holds
seq is summable
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st ex k being Element of NAT st seq ^\ k is summable holds
seq is summable
let seq be sequence of X; ::_thesis: ( ex k being Element of NAT st seq ^\ k is summable implies seq is summable )
given k being Element of NAT  such that A1: seq ^\ k is summable ; ::_thesis: seq is summable
 (seq ^\ k) ^\ 1 is summable by A1, Th13;
then A2: Partial_Sums ((seq ^\ k) ^\ 1) is convergent by Def1;
reconsider seq1 = NAT --> ((Partial_Sums seq) . k) as sequence of X ;
defpred S1[ Element of NAT ] means ((Partial_Sums seq) ^\ (k + 1)) . $1 = ((Partial_Sums (seq ^\ (k + 1))) . $1) + (seq1 . $1);
A3: (Partial_Sums (seq ^\ (k + 1))) . 0 = (seq ^\ (k + 1)) . 0 by BHSP_4:def_1
.= seq . (0 + (k + 1)) by NAT_1:def_3
.= seq . (k + 1) ;
A4: now__::_thesis:_for_m_being_Element_of_NAT_st_S1[m]_holds_
S1[m_+_1]
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A5: S1[m] ; ::_thesis: S1[m + 1]
((Partial_Sums (seq ^\ (k + 1))) . (m + 1)) + (seq1 . (m + 1)) = (seq1 . (m + 1)) + (((Partial_Sums (seq ^\ (k + 1))) . m) + ((seq ^\ (k + 1)) . (m + 1))) by BHSP_4:def_1
.= ((seq1 . (m + 1)) + ((Partial_Sums (seq ^\ (k + 1))) . m)) + ((seq ^\ (k + 1)) . (m + 1)) by RLVECT_1:def_3
.= (((Partial_Sums seq) . k) + ((Partial_Sums (seq ^\ (k + 1))) . m)) + ((seq ^\ (k + 1)) . (m + 1)) by FUNCOP_1:7
.= (((Partial_Sums seq) ^\ (k + 1)) . m) + ((seq ^\ (k + 1)) . (m + 1)) by A5, FUNCOP_1:7
.= ((Partial_Sums seq) . (m + (k + 1))) + ((seq ^\ (k + 1)) . (m + 1)) by NAT_1:def_3
.= ((Partial_Sums seq) . (m + (k + 1))) + (seq . ((m + 1) + (k + 1))) by NAT_1:def_3
.= (Partial_Sums seq) . ((m + (k + 1)) + 1) by BHSP_4:def_1
.= (Partial_Sums seq) . ((m + 1) + (k + 1))
.= ((Partial_Sums seq) ^\ (k + 1)) . (m + 1) by NAT_1:def_3 ;
hence  S1[m + 1] ; ::_thesis: verum
end;
((Partial_Sums seq) ^\ (k + 1)) . 0 = (Partial_Sums seq) . (0 + (k + 1)) by NAT_1:def_3
.= ((Partial_Sums seq) . k) + (seq . (k + 1)) by BHSP_4:def_1
.= ((Partial_Sums (seq ^\ (k + 1))) . 0) + (seq1 . 0) by A3, FUNCOP_1:7 ;
then A6: S1[ 0 ] ;
 for m being Element of NAT holds S1[m] from NAT_1:sch_1(A6, A4);
then A7: (Partial_Sums seq) ^\ (k + 1) = (Partial_Sums (seq ^\ (k + 1))) + seq1 by NORMSP_1:def_2
.= (Partial_Sums ((seq ^\ k) ^\ 1)) + seq1 by NAT_1:48 ;
 seq1 is convergent by CLVECT_2:1;
then  (Partial_Sums seq) ^\ (k + 1) is convergent by A2, A7, CLVECT_2:3;
then  Partial_Sums seq is convergent by CLVECT_2:91;
hence  seq is summable by Def1; ::_thesis: verum
end;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
let n be Element of NAT ;
func Sum (seq,n) ->  Point of X equals :: CLVECT_3:def 3
(Partial_Sums seq) . n;
correctness
coherence
(Partial_Sums seq) . n is Point of X;
;
end;

:: deftheorem  defines Sum CLVECT_3:def_3_:_
 for X being ComplexUnitarySpace
for seq being sequence of X
for n being Element of NAT holds Sum (seq,n) = (Partial_Sums seq) . n;

theorem :: CLVECT_3:15
for X being ComplexUnitarySpace
for seq being sequence of X holds Sum (seq,0) = seq . 0 by BHSP_4:def_1;

theorem Th16: :: CLVECT_3:16
for X being ComplexUnitarySpace
for seq being sequence of X holds Sum (seq,1) = (Sum (seq,0)) + (seq . 1)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds Sum (seq,1) = (Sum (seq,0)) + (seq . 1)
let seq be sequence of X; ::_thesis: Sum (seq,1) = (Sum (seq,0)) + (seq . 1)
(Partial_Sums seq) . 1 = ((Partial_Sums seq) . 0) + (seq . (0 + 1)) by BHSP_4:def_1
.= ((Partial_Sums seq) . 0) + (seq . 1) ;
hence  Sum (seq,1) = (Sum (seq,0)) + (seq . 1) ; ::_thesis: verum
end;

theorem Th17: :: CLVECT_3:17
for X being ComplexUnitarySpace
for seq being sequence of X holds Sum (seq,1) = (seq . 0) + (seq . 1)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds Sum (seq,1) = (seq . 0) + (seq . 1)
let seq be sequence of X; ::_thesis: Sum (seq,1) = (seq . 0) + (seq . 1)
thus  Sum (seq,1) = (Sum (seq,0)) + (seq . 1) by Th16
.= (seq . 0) + (seq . 1) by BHSP_4:def_1 ; ::_thesis: verum
end;

theorem :: CLVECT_3:18
for X being ComplexUnitarySpace
for seq being sequence of X
for n being Element of NAT holds Sum (seq,(n + 1)) = (Sum (seq,n)) + (seq . (n + 1)) by BHSP_4:def_1;

theorem Th19: :: CLVECT_3:19
for X being ComplexUnitarySpace
for seq being sequence of X
for n being Element of NAT holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for n being Element of NAT holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))
let seq be sequence of X; ::_thesis: for n being Element of NAT holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))
let n be Element of NAT ; ::_thesis: seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))
thus (Sum (seq,(n + 1))) - (Sum (seq,n)) = ((seq . (n + 1)) + (Sum (seq,n))) - (Sum (seq,n)) by BHSP_4:def_1
.= (seq . (n + 1)) + ((Sum (seq,n)) - (Sum (seq,n))) by RLVECT_1:def_3
.= (seq . (n + 1)) + (0. X) by RLVECT_1:15
.= seq . (n + 1) by RLVECT_1:4 ; ::_thesis: verum
end;

theorem :: CLVECT_3:20
for X being ComplexUnitarySpace
for seq being sequence of X holds seq . 1 = (Sum (seq,1)) - (Sum (seq,0))
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds seq . 1 = (Sum (seq,1)) - (Sum (seq,0))
let seq be sequence of X; ::_thesis: seq . 1 = (Sum (seq,1)) - (Sum (seq,0))
 seq . (0 + 1) = (Sum (seq,(0 + 1))) - (Sum (seq,0)) by Th19;
hence  seq . 1 = (Sum (seq,1)) - (Sum (seq,0)) ; ::_thesis: verum
end;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
let n, m be Element of NAT ;
func Sum (seq,n,m) ->  Point of X equals :: CLVECT_3:def 4
(Sum (seq,n)) - (Sum (seq,m));
correctness
coherence
(Sum (seq,n)) - (Sum (seq,m)) is Point of X;
;
end;

:: deftheorem  defines Sum CLVECT_3:def_4_:_
 for X being ComplexUnitarySpace
for seq being sequence of X
for n, m being Element of NAT holds Sum (seq,n,m) = (Sum (seq,n)) - (Sum (seq,m));

theorem :: CLVECT_3:21
for X being ComplexUnitarySpace
for seq being sequence of X holds Sum (seq,1,0) = seq . 1
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds Sum (seq,1,0) = seq . 1
let seq be sequence of X; ::_thesis: Sum (seq,1,0) = seq . 1
Sum (seq,1,0) = ((seq . 0) + (seq . 1)) - (Sum (seq,0)) by Th17
.= ((seq . 1) + (seq . 0)) - (seq . 0) by BHSP_4:def_1
.= (seq . 1) + ((seq . 0) - (seq . 0)) by RLVECT_1:def_3
.= (seq . 1) + H1(X) by RLVECT_1:15 ;
hence  Sum (seq,1,0) = seq . 1 by RLVECT_1:4; ::_thesis: verum
end;

theorem :: CLVECT_3:22
for X being ComplexUnitarySpace
for seq being sequence of X
for n being Element of NAT holds Sum (seq,(n + 1),n) = seq . (n + 1) by Th19;

theorem Th23: :: CLVECT_3:23
for X being ComplexHilbertSpace
for seq being sequence of X holds
( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )
proof
let X be ComplexHilbertSpace; ::_thesis: for seq being sequence of X holds
( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )
let seq be sequence of X; ::_thesis: ( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )
thus  ( seq is summable implies for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ) ::_thesis: ( ( for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ) implies seq is summable )
proof
assume A1: seq is summable ; ::_thesis: for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r
now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((Sum_(seq,n))_-_(Sum_(seq,m))).||_<_r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r
then consider k being Element of NAT  such that
A2: for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r by A1, Th10;
take k = k; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )
assume  ( n >= k & m >= k ) ; ::_thesis: ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r
hence  ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r by A2; ::_thesis: verum
end;
hence  for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ; ::_thesis: verum
end;
thus  ( ( for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ) implies seq is summable ) ::_thesis: verum
proof
assume A3: for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ; ::_thesis: seq is summable
now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.(((Partial_Sums_seq)_._n)_-_((Partial_Sums_seq)_._m)).||_<_r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r
then consider k being Element of NAT  such that
A4: for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r by A3;
take k = k; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r )
assume  ( n >= k & m >= k ) ; ::_thesis: ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r
then  ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r by A4;
hence  ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ; ::_thesis: verum
end;
hence  seq is summable by Th10; ::_thesis: verum
end;
end;

theorem :: CLVECT_3:24
for X being ComplexHilbertSpace
for seq being sequence of X holds
( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r )
proof
let X be ComplexHilbertSpace; ::_thesis: for seq being sequence of X holds
( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r )
let seq be sequence of X; ::_thesis: ( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r )
thus  ( seq is summable implies for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r ) ::_thesis: ( ( for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r ) implies seq is summable )
proof
assume A1: seq is summable ; ::_thesis: for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r
now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.(Sum_(seq,n,m)).||_<_r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r
then consider k being Element of NAT  such that
A2: for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r by A1, Th23;
take k = k; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.(Sum (seq,n,m)).|| < r )
assume  ( n >= k & m >= k ) ; ::_thesis: ||.(Sum (seq,n,m)).|| < r
hence  ||.(Sum (seq,n,m)).|| < r by A2; ::_thesis: verum
end;
hence  for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r ; ::_thesis: verum
end;
thus  ( ( for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r ) implies seq is summable ) ::_thesis: verum
proof
assume A3: for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r ; ::_thesis: seq is summable
now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((Sum_(seq,n))_-_(Sum_(seq,m))).||_<_r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r
then consider k being Element of NAT  such that
A4: for n, m being Element of NAT st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r by A3;
take k = k; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )
assume  ( n >= k & m >= k ) ; ::_thesis: ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r
then  ||.(Sum (seq,n,m)).|| < r by A4;
hence  ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ; ::_thesis: verum
end;
hence  seq is summable by Th23; ::_thesis: verum
end;
end;

definition
let Cseq be Complex_Sequence;
let n be Element of NAT ;
func Sum (Cseq,n) ->  Complex equals :: CLVECT_3:def 5
(Partial_Sums Cseq) . n;
correctness
coherence
(Partial_Sums Cseq) . n is Complex;
;
end;

:: deftheorem  defines Sum CLVECT_3:def_5_:_
 for Cseq being Complex_Sequence
for n being Element of NAT holds Sum (Cseq,n) = (Partial_Sums Cseq) . n;

definition
let Cseq be Complex_Sequence;
let n, m be Element of NAT ;
func Sum (Cseq,n,m) ->  Complex equals :: CLVECT_3:def 6
(Sum (Cseq,n)) - (Sum (Cseq,m));
correctness
coherence
(Sum (Cseq,n)) - (Sum (Cseq,m)) is Complex;
;
end;

:: deftheorem  defines Sum CLVECT_3:def_6_:_
 for Cseq being Complex_Sequence
for n, m being Element of NAT holds Sum (Cseq,n,m) = (Sum (Cseq,n)) - (Sum (Cseq,m));

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
attrseq is absolutely_summable  means :Def7: :: CLVECT_3:def 7
||.seq.|| is summable ;
end;

:: deftheorem Def7 defines absolutely_summable CLVECT_3:def_7_:_
 for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is absolutely_summable iff ||.seq.|| is summable );

theorem :: CLVECT_3:25
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is absolutely_summable & seq2 is absolutely_summable holds
seq1 + seq2 is absolutely_summable
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is absolutely_summable & seq2 is absolutely_summable holds
seq1 + seq2 is absolutely_summable
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is absolutely_summable & seq2 is absolutely_summable implies seq1 + seq2 is absolutely_summable )
A1: for n being Element of NAT holds
( ||.(seq1 + seq2).|| . n >= 0 & ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n )
proof
let n be Element of NAT ; ::_thesis: ( ||.(seq1 + seq2).|| . n >= 0 & ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n )
 ||.(seq1 + seq2).|| . n = ||.((seq1 + seq2) . n).|| by CLVECT_2:def_3;
hence  ||.(seq1 + seq2).|| . n >= 0 by CSSPACE:44; ::_thesis: ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n
||.(seq1 + seq2).|| . n = ||.((seq1 + seq2) . n).|| by CLVECT_2:def_3
.= ||.((seq1 . n) + (seq2 . n)).|| by NORMSP_1:def_2 ;
then  ||.(seq1 + seq2).|| . n <= ||.(seq1 . n).|| + ||.(seq2 . n).|| by CSSPACE:46;
then  ||.(seq1 + seq2).|| . n <= (||.seq1.|| . n) + ||.(seq2 . n).|| by CLVECT_2:def_3;
then  ||.(seq1 + seq2).|| . n <= (||.seq1.|| . n) + (||.seq2.|| . n) by CLVECT_2:def_3;
hence  ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n by SEQ_1:7; ::_thesis: verum
end;
assume  ( seq1 is absolutely_summable & seq2 is absolutely_summable ) ; ::_thesis: seq1 + seq2 is absolutely_summable
then  ( ||.seq1.|| is summable & ||.seq2.|| is summable ) by Def7;
then  ||.seq1.|| + ||.seq2.|| is summable by SERIES_1:7;
then  ||.(seq1 + seq2).|| is summable by A1, SERIES_1:20;
hence  seq1 + seq2 is absolutely_summable by Def7; ::_thesis: verum
end;

theorem :: CLVECT_3:26
for X being ComplexUnitarySpace
for seq being sequence of X
for z being Complex st seq is absolutely_summable holds
z * seq is absolutely_summable
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for z being Complex st seq is absolutely_summable holds
z * seq is absolutely_summable
let seq be sequence of X; ::_thesis: for z being Complex st seq is absolutely_summable holds
z * seq is absolutely_summable
let z be Complex; ::_thesis: ( seq is absolutely_summable implies z * seq is absolutely_summable )
A1: for n being Element of NAT holds
( ||.(z * seq).|| . n >= 0 & ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n )
proof
let n be Element of NAT ; ::_thesis: ( ||.(z * seq).|| . n >= 0 & ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n )
 ||.(z * seq).|| . n = ||.((z * seq) . n).|| by CLVECT_2:def_3;
hence  ||.(z * seq).|| . n >= 0 by CSSPACE:44; ::_thesis: ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n
||.(z * seq).|| . n = ||.((z * seq) . n).|| by CLVECT_2:def_3
.= ||.(z * (seq . n)).|| by CLVECT_1:def_14
.= |.z.| * ||.(seq . n).|| by CSSPACE:43
.= |.z.| * (||.seq.|| . n) by CLVECT_2:def_3
.= (|.z.| (#) ||.seq.||) . n by SEQ_1:9 ;
hence  ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n ; ::_thesis: verum
end;
assume  seq is absolutely_summable ; ::_thesis: z * seq is absolutely_summable
then  ||.seq.|| is summable by Def7;
then  |.z.| (#) ||.seq.|| is summable by SERIES_1:10;
then  ||.(z * seq).|| is summable by A1, SERIES_1:20;
hence  z * seq is absolutely_summable by Def7; ::_thesis: verum
end;

theorem :: CLVECT_3:27
for X being ComplexUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable holds
seq is absolutely_summable
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable holds
seq is absolutely_summable
let seq be sequence of X; ::_thesis: for Rseq being Real_Sequence st ( for n being Element of NAT holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable holds
seq is absolutely_summable
let Rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable implies seq is absolutely_summable )
A1: for n being Element of NAT holds ||.seq.|| . n >= 0
proof
let n be Element of NAT ; ::_thesis: ||.seq.|| . n >= 0
 ||.seq.|| . n = ||.(seq . n).|| by CLVECT_2:def_3;
hence  ||.seq.|| . n >= 0 by CSSPACE:44; ::_thesis: verum
end;
assume  ( ( for n being Element of NAT holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable ) ; ::_thesis: seq is absolutely_summable
then  ||.seq.|| is summable by A1, SERIES_1:20;
hence  seq is absolutely_summable by Def7; ::_thesis: verum
end;

theorem :: CLVECT_3:28
for X being ComplexUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds
( seq . n <> 0. X & Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) ) & Rseq is convergent & lim Rseq < 1 holds
seq is absolutely_summable
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds
( seq . n <> 0. X & Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) ) & Rseq is convergent & lim Rseq < 1 holds
seq is absolutely_summable
let seq be sequence of X; ::_thesis: for Rseq being Real_Sequence st ( for n being Element of NAT holds
( seq . n <> 0. X & Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) ) & Rseq is convergent & lim Rseq < 1 holds
seq is absolutely_summable
let Rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds
( seq . n <> 0. X & Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) ) & Rseq is convergent & lim Rseq < 1 implies seq is absolutely_summable )
assume that
A1: for n being Element of NAT holds
( seq . n <> H1(X) & Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) and
A2: ( Rseq is convergent & lim Rseq < 1 ) ; ::_thesis: seq is absolutely_summable
 for n being Element of NAT holds
( ||.seq.|| . n > 0 & Rseq . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) )
proof
let n be Element of NAT ; ::_thesis: ( ||.seq.|| . n > 0 & Rseq . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) )
 seq . n <> H1(X) by A1;
then A3: ||.(seq . n).|| <> 0 by CSSPACE:42;
 ||.(seq . n).|| >= 0 by CSSPACE:44;
hence  ||.seq.|| . n > 0 by A3, CLVECT_2:def_3; ::_thesis: Rseq . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n)
Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| by A1
.= (||.seq.|| . (n + 1)) / ||.(seq . n).|| by CLVECT_2:def_3 ;
hence  Rseq . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) by CLVECT_2:def_3; ::_thesis: verum
end;
then  ||.seq.|| is summable by A2, SERIES_1:26;
hence  seq is absolutely_summable by Def7; ::_thesis: verum
end;

theorem Th29: :: CLVECT_3:29
for X being ComplexUnitarySpace
for seq being sequence of X
for r being Real st r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(seq . n).|| >= r & seq is convergent holds
lim seq <> 0. X
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for r being Real st r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(seq . n).|| >= r & seq is convergent holds
lim seq <> 0. X
let seq be sequence of X; ::_thesis: for r being Real st r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(seq . n).|| >= r & seq is convergent holds
lim seq <> 0. X
let r be Real; ::_thesis: ( r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(seq . n).|| >= r & seq is convergent implies lim seq <> 0. X )
assume A1: r > 0 ; ::_thesis: ( for m being Element of NAT ex n being Element of NAT st
( n >= m & not ||.(seq . n).|| >= r ) or not seq is convergent or lim seq <> 0. X )
given m being Element of NAT  such that A2: for n being Element of NAT st n >= m holds
||.(seq . n).|| >= r ; ::_thesis: ( not seq is convergent or lim seq <> 0. X )
now__::_thesis:_(_not_seq_is_convergent_or_lim_seq_<>_0._X_)
percases ( not seq is convergent or seq is convergent ) ;
suppose not seq is convergent ; ::_thesis: ( not seq is convergent or lim seq <> 0. X )
hence  ( not seq is convergent or lim seq <> 0. X ) ; ::_thesis: verum
end;
supposeA3: seq is convergent ; ::_thesis: ( not seq is convergent or lim seq <> 0. X )
now__::_thesis:_not_lim_seq_=_H1(X)
assume  lim seq = H1(X) ; ::_thesis: contradiction
then consider k being Element of NAT  such that
A4: for n being Element of NAT st n >= k holds
||.((seq . n) - H1(X)).|| < r by A1, A3, CLVECT_2:19;
now__::_thesis:_for_n_being_Element_of_NAT_holds_not_n_>=_m_+_k
let n be Element of NAT ; ::_thesis: not n >= m + k
assume A5: n >= m + k ; ::_thesis: contradiction
 m + k >= k by NAT_1:11;
then  n >= k by A5, XXREAL_0:2;
then  ||.((seq . n) - H1(X)).|| < r by A4;
then A6: ||.(seq . n).|| < r by RLVECT_1:13;
 m + k >= m by NAT_1:11;
then  n >= m by A5, XXREAL_0:2;
hence  contradiction by A2, A6; ::_thesis: verum
end;
hence  contradiction ; ::_thesis: verum
end;
hence  ( not seq is convergent or lim seq <> 0. X ) ; ::_thesis: verum
end;
end;
end;
hence  ( not seq is convergent or lim seq <> 0. X ) ; ::_thesis: verum
end;

theorem Th30: :: CLVECT_3:30
for X being ComplexUnitarySpace
for seq being sequence of X st ( for n being Element of NAT holds seq . n <> 0. X ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 holds
not seq is summable
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st ( for n being Element of NAT holds seq . n <> 0. X ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 holds
not seq is summable
let seq be sequence of X; ::_thesis: ( ( for n being Element of NAT holds seq . n <> 0. X ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 implies not seq is summable )
assume A1: for n being Element of NAT holds seq . n <> H1(X) ; ::_thesis: ( for m being Element of NAT ex n being Element of NAT st
( n >= m & not ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 ) or not seq is summable )
given m being Element of NAT  such that A2: for n being Element of NAT st n >= m holds
||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 ; ::_thesis: not seq is summable
A3: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_
||.(seq_._n).||_>=_||.(seq_._m).||
defpred S1[ Element of NAT ] means ||.(seq . (m + $1)).|| >= ||.(seq . m).||;
let n be Element of NAT ; ::_thesis: ( n >= m implies ||.(seq . n).|| >= ||.(seq . m).|| )
A4: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A5: ||.(seq . (m + k)).|| >= ||.(seq . m).|| ; ::_thesis: S1[k + 1]
 seq . (m + k) <> H1(X) by A1;
then A6: ||.(seq . (m + k)).|| <> 0 by CSSPACE:42;
 ( ||.(seq . ((m + k) + 1)).|| / ||.(seq . (m + k)).|| >= 1 & ||.(seq . (m + k)).|| >= 0 ) by A2, CSSPACE:44, NAT_1:11;
then  ||.(seq . ((m + k) + 1)).|| >= ||.(seq . (m + k)).|| by A6, XREAL_1:191;
hence  S1[k + 1] by A5, XXREAL_0:2; ::_thesis: verum
end;
A7: S1[ 0 ] ;
A8: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A7, A4);
assume  n >= m ; ::_thesis: ||.(seq . n).|| >= ||.(seq . m).||
then consider k being Nat such that
A9: n = m + k by NAT_1:10;
 k in NAT by ORDINAL1:def_12;
hence  ||.(seq . n).|| >= ||.(seq . m).|| by A8, A9; ::_thesis: verum
end;
 seq . m <> H1(X) by A1;
then  ||.(seq . m).|| <> 0 by CSSPACE:42;
then  ||.(seq . m).|| > 0 by CSSPACE:44;
then  ( not seq is convergent or lim seq <> H1(X) ) by A3, Th29;
hence  not seq is summable by Th9; ::_thesis: verum
end;

theorem :: CLVECT_3:31
for X being ComplexUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds seq . n <> 0. X ) & ( for n being Element of NAT holds Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) & Rseq is convergent & lim Rseq > 1 holds
not seq is summable
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds seq . n <> 0. X ) & ( for n being Element of NAT holds Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) & Rseq is convergent & lim Rseq > 1 holds
not seq is summable
let seq be sequence of X; ::_thesis: for Rseq being Real_Sequence st ( for n being Element of NAT holds seq . n <> 0. X ) & ( for n being Element of NAT holds Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) & Rseq is convergent & lim Rseq > 1 holds
not seq is summable
let Rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n <> 0. X ) & ( for n being Element of NAT holds Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) & Rseq is convergent & lim Rseq > 1 implies not seq is summable )
assume that
A1: for n being Element of NAT holds seq . n <> H1(X) and
A2: for n being Element of NAT holds Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| and
A3: Rseq is convergent and
A4: lim Rseq > 1 ; ::_thesis: not seq is summable
 (lim Rseq) - 1 > 0 by A4, XREAL_1:50;
then consider m being Element of NAT  such that
A5: for n being Element of NAT st n >= m holds
abs ((Rseq . n) - (lim Rseq)) < (lim Rseq) - 1 by A3, SEQ_2:def_7;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_+_1_holds_
||.(seq_._(n_+_1)).||_/_||.(seq_._n).||_>=_1
let n be Element of NAT ; ::_thesis: ( n >= m + 1 implies ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 )
A6: m + 1 >= m by NAT_1:11;
A7: Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| by A2;
assume  n >= m + 1 ; ::_thesis: ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1
then  n >= m by A6, XXREAL_0:2;
then  abs ((||.(seq . (n + 1)).|| / ||.(seq . n).||) - (lim Rseq)) < (lim Rseq) - 1 by A5, A7;
then  - ((lim Rseq) - 1) < (||.(seq . (n + 1)).|| / ||.(seq . n).||) - (lim Rseq) by SEQ_2:1;
then  (1 - (lim Rseq)) + (lim Rseq) < ((||.(seq . (n + 1)).|| / ||.(seq . n).||) - (lim Rseq)) + (lim Rseq) by XREAL_1:6;
hence  ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 ; ::_thesis: verum
end;
hence  not seq is summable by A1, Th30; ::_thesis: verum
end;

theorem :: CLVECT_3:32
for X being ComplexUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root ||.(seq . n).|| ) & Rseq is convergent & lim Rseq < 1 holds
seq is absolutely_summable
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root ||.(seq . n).|| ) & Rseq is convergent & lim Rseq < 1 holds
seq is absolutely_summable
let seq be sequence of X; ::_thesis: for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root ||.(seq . n).|| ) & Rseq is convergent & lim Rseq < 1 holds
seq is absolutely_summable
let Rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds Rseq . n = n -root ||.(seq . n).|| ) & Rseq is convergent & lim Rseq < 1 implies seq is absolutely_summable )
assume that
A1: for n being Element of NAT holds Rseq . n = n -root ||.(seq . n).|| and
A2: ( Rseq is convergent & lim Rseq < 1 ) ; ::_thesis: seq is absolutely_summable
 for n being Element of NAT holds
( ||.seq.|| . n >= 0 & Rseq . n = n -root (||.seq.|| . n) )
proof
let n be Element of NAT ; ::_thesis: ( ||.seq.|| . n >= 0 & Rseq . n = n -root (||.seq.|| . n) )
 ||.seq.|| . n = ||.(seq . n).|| by CLVECT_2:def_3;
hence  ||.seq.|| . n >= 0 by CSSPACE:44; ::_thesis: Rseq . n = n -root (||.seq.|| . n)
 Rseq . n = n -root ||.(seq . n).|| by A1;
hence  Rseq . n = n -root (||.seq.|| . n) by CLVECT_2:def_3; ::_thesis: verum
end;
then  ||.seq.|| is summable by A2, SERIES_1:28;
hence  seq is absolutely_summable by Def7; ::_thesis: verum
end;

theorem :: CLVECT_3:33
for X being ComplexUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
Rseq . n >= 1 holds
not seq is summable
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
Rseq . n >= 1 holds
not seq is summable
let seq be sequence of X; ::_thesis: for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
Rseq . n >= 1 holds
not seq is summable
let Rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
Rseq . n >= 1 implies not seq is summable )
assume A1: for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ; ::_thesis: ( for m being Element of NAT ex n being Element of NAT st
( n >= m & not Rseq . n >= 1 ) or not seq is summable )
given m being Element of NAT  such that A2: for n being Element of NAT st n >= m holds
Rseq . n >= 1 ; ::_thesis: not seq is summable
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_+_1_holds_
||.(seq_._n).||_>=_1
let n be Element of NAT ; ::_thesis: ( n >= m + 1 implies ||.(seq . n).|| >= 1 )
assume A3: n >= m + 1 ; ::_thesis: ||.(seq . n).|| >= 1
 m + 1 >= 1 by NAT_1:11;
then A4: n >= 1 by A3, XXREAL_0:2;
 m + 1 >= m by NAT_1:11;
then A5: n >= m by A3, XXREAL_0:2;
Rseq . n = n -root (||.seq.|| . n) by A1
.= n -root ||.(seq . n).|| by CLVECT_2:def_3 ;
then  ( ||.(seq . n).|| >= 0 & (n -root ||.(seq . n).||) |^ n >= 1 ) by A2, A5, CSSPACE:44, PREPOWER:11;
hence  ||.(seq . n).|| >= 1 by A4, POWER:4; ::_thesis: verum
end;
then  ( not seq is convergent or lim seq <> H1(X) ) by Th29;
hence  not seq is summable by Th9; ::_thesis: verum
end;

theorem :: CLVECT_3:34
for X being ComplexUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 holds
not seq is summable
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 holds
not seq is summable
let seq be sequence of X; ::_thesis: for Rseq being Real_Sequence st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 holds
not seq is summable
let Rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 implies not seq is summable )
assume that
A1: for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) and
A2: Rseq is convergent and
A3: lim Rseq > 1 ; ::_thesis: not seq is summable
 (lim Rseq) - 1 > 0 by A3, XREAL_1:50;
then consider m being Element of NAT  such that
A4: for n being Element of NAT st n >= m holds
abs ((Rseq . n) - (lim Rseq)) < (lim Rseq) - 1 by A2, SEQ_2:def_7;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_+_1_holds_
||.(seq_._n).||_>=_1
let n be Element of NAT ; ::_thesis: ( n >= m + 1 implies ||.(seq . n).|| >= 1 )
assume A5: n >= m + 1 ; ::_thesis: ||.(seq . n).|| >= 1
A6: Rseq . n = n -root (||.seq.|| . n) by A1
.= n -root ||.(seq . n).|| by CLVECT_2:def_3 ;
 m + 1 >= m by NAT_1:11;
then  n >= m by A5, XXREAL_0:2;
then  abs ((n -root ||.(seq . n).||) - (lim Rseq)) < (lim Rseq) - 1 by A4, A6;
then  - ((lim Rseq) - 1) < (n -root ||.(seq . n).||) - (lim Rseq) by SEQ_2:1;
then  (1 - (lim Rseq)) + (lim Rseq) < ((n -root ||.(seq . n).||) - (lim Rseq)) + (lim Rseq) by XREAL_1:6;
then A7: ( ||.(seq . n).|| >= 0 & (n -root ||.(seq . n).||) |^ n >= 1 ) by CSSPACE:44, PREPOWER:11;
 m + 1 >= 1 by NAT_1:11;
then  n >= 1 by A5, XXREAL_0:2;
hence  ||.(seq . n).|| >= 1 by A7, POWER:4; ::_thesis: verum
end;
then  ( not seq is convergent or lim seq <> H1(X) ) by Th29;
hence  not seq is summable by Th9; ::_thesis: verum
end;

theorem Th35: :: CLVECT_3:35
for X being ComplexUnitarySpace
for seq being sequence of X holds Partial_Sums ||.seq.|| is non-decreasing
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds Partial_Sums ||.seq.|| is non-decreasing
let seq be sequence of X; ::_thesis: Partial_Sums ||.seq.|| is non-decreasing
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Sums_||.seq.||)_._n_<=_(Partial_Sums_||.seq.||)_._(n_+_1)
let n be Element of NAT ; ::_thesis: (Partial_Sums ||.seq.||) . n <= (Partial_Sums ||.seq.||) . (n + 1)
 ||.(seq . (n + 1)).|| >= 0 by CSSPACE:44;
then  ||.seq.|| . (n + 1) >= 0 by CLVECT_2:def_3;
then  0 + ((Partial_Sums ||.seq.||) . n) <= (||.seq.|| . (n + 1)) + ((Partial_Sums ||.seq.||) . n) by XREAL_1:6;
hence  (Partial_Sums ||.seq.||) . n <= (Partial_Sums ||.seq.||) . (n + 1) by SERIES_1:def_1; ::_thesis: verum
end;
hence  Partial_Sums ||.seq.|| is non-decreasing by SEQM_3:def_8; ::_thesis: verum
end;

theorem :: CLVECT_3:36
for X being ComplexUnitarySpace
for seq being sequence of X
for n being Element of NAT holds (Partial_Sums ||.seq.||) . n >= 0
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for n being Element of NAT holds (Partial_Sums ||.seq.||) . n >= 0
let seq be sequence of X; ::_thesis: for n being Element of NAT holds (Partial_Sums ||.seq.||) . n >= 0
let n be Element of NAT ; ::_thesis: (Partial_Sums ||.seq.||) . n >= 0
 ||.(seq . 0).|| >= 0 by CSSPACE:44;
then  ||.seq.|| . 0 >= 0 by CLVECT_2:def_3;
then  (Partial_Sums ||.seq.||) . 0 >= 0 by SERIES_1:def_1;
hence  (Partial_Sums ||.seq.||) . n >= 0 by Th35, SEQM_3:11; ::_thesis: verum
end;

theorem Th37: :: CLVECT_3:37
for X being ComplexUnitarySpace
for seq being sequence of X
for n being Element of NAT holds ||.((Partial_Sums seq) . n).|| <= (Partial_Sums ||.seq.||) . n
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for n being Element of NAT holds ||.((Partial_Sums seq) . n).|| <= (Partial_Sums ||.seq.||) . n
let seq be sequence of X; ::_thesis: for n being Element of NAT holds ||.((Partial_Sums seq) . n).|| <= (Partial_Sums ||.seq.||) . n
defpred S1[ Element of NAT ] means ||.((Partial_Sums seq) . $1).|| <= (Partial_Sums ||.seq.||) . $1;
A1: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
 (Partial_Sums seq) . (n + 1) = ((Partial_Sums seq) . n) + (seq . (n + 1)) by BHSP_4:def_1;
then A2: ||.((Partial_Sums seq) . (n + 1)).|| <= ||.((Partial_Sums seq) . n).|| + ||.(seq . (n + 1)).|| by CSSPACE:46;
assume  S1[n] ; ::_thesis: S1[n + 1]
then  ||.((Partial_Sums seq) . n).|| + ||.(seq . (n + 1)).|| <= ((Partial_Sums ||.seq.||) . n) + ||.(seq . (n + 1)).|| by XREAL_1:6;
then  ||.((Partial_Sums seq) . (n + 1)).|| <= ((Partial_Sums ||.seq.||) . n) + ||.(seq . (n + 1)).|| by A2, XXREAL_0:2;
then  ||.((Partial_Sums seq) . (n + 1)).|| <= ((Partial_Sums ||.seq.||) . n) + (||.seq.|| . (n + 1)) by CLVECT_2:def_3;
hence  S1[n + 1] by SERIES_1:def_1; ::_thesis: verum
end;
(Partial_Sums ||.seq.||) . 0 = ||.seq.|| . 0 by SERIES_1:def_1
.= ||.(seq . 0).|| by CLVECT_2:def_3 ;
then A3: S1[ 0 ] by BHSP_4:def_1;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); ::_thesis: verum
end;

theorem :: CLVECT_3:38
for X being ComplexUnitarySpace
for seq being sequence of X
for n being Element of NAT holds ||.(Sum (seq,n)).|| <= Sum (||.seq.||,n)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for n being Element of NAT holds ||.(Sum (seq,n)).|| <= Sum (||.seq.||,n)
let seq be sequence of X; ::_thesis: for n being Element of NAT holds ||.(Sum (seq,n)).|| <= Sum (||.seq.||,n)
let n be Element of NAT ; ::_thesis: ||.(Sum (seq,n)).|| <= Sum (||.seq.||,n)
 ||.((Partial_Sums seq) . n).|| <= (Partial_Sums ||.seq.||) . n by Th37;
hence  ||.(Sum (seq,n)).|| <= Sum (||.seq.||,n) by SERIES_1:def_5; ::_thesis: verum
end;

theorem Th39: :: CLVECT_3:39
for X being ComplexUnitarySpace
for seq being sequence of X
for n, m being Element of NAT holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n))
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for n, m being Element of NAT holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n))
let seq be sequence of X; ::_thesis: for n, m being Element of NAT holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n))
let n, m be Element of NAT ; ::_thesis: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n))
A1: now__::_thesis:_(_n_>=_m_implies_||.(((Partial_Sums_seq)_._m)_-_((Partial_Sums_seq)_._n)).||_<=_abs_(((Partial_Sums_||.seq.||)_._m)_-_((Partial_Sums_||.seq.||)_._n))_)
reconsider d = n, t = m as Integer ;
set PSseq9 = Partial_Sums ||.seq.||;
set PSseq = Partial_Sums seq;
defpred S1[ Element of NAT ] means ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + $1))).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . (m + $1)));
A2: Partial_Sums ||.seq.|| is non-decreasing by Th35;
A3: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A4: ||.(seq . ((m + k) + 1)).|| >= 0 by CSSPACE:44;
A5: abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . (m + (k + 1)))) = abs (- (((Partial_Sums ||.seq.||) . (m + (k + 1))) - ((Partial_Sums ||.seq.||) . m)))
.= abs (((Partial_Sums ||.seq.||) . ((m + k) + 1)) - ((Partial_Sums ||.seq.||) . m)) by COMPLEX1:52
.= abs ((((Partial_Sums ||.seq.||) . (m + k)) + (||.seq.|| . ((m + k) + 1))) - ((Partial_Sums ||.seq.||) . m)) by SERIES_1:def_1
.= abs ((||.(seq . ((m + k) + 1)).|| + ((Partial_Sums ||.seq.||) . (m + k))) - ((Partial_Sums ||.seq.||) . m)) by CLVECT_2:def_3
.= abs ((((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m)) + ||.(seq . ((m + k) + 1)).||) ;
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| = ||.(((Partial_Sums seq) . m) - (((Partial_Sums seq) . (m + k)) + (seq . ((m + k) + 1)))).|| by BHSP_4:def_1
.= ||.((((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + k))) - (seq . ((m + k) + 1))).|| by RLVECT_1:27
.= ||.((((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + k))) + (- (seq . ((m + k) + 1)))).|| ;
then  ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + k))).|| + ||.(- (seq . ((m + k) + 1))).|| by CSSPACE:46;
then A6: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + k))).|| + ||.(seq . ((m + k) + 1)).|| by CSSPACE:47;
 (Partial_Sums ||.seq.||) . (m + k) >= (Partial_Sums ||.seq.||) . m by A2, SEQM_3:5;
then A7: ((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m) >= 0 by XREAL_1:48;
assume  S1[k] ; ::_thesis: S1[k + 1]
then  ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + k))).|| + ||.(seq . ((m + k) + 1)).|| <= (abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . (m + k)))) + ||.(seq . ((m + k) + 1)).|| by XREAL_1:6;
then  ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= (abs (- (((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m)))) + ||.(seq . ((m + k) + 1)).|| by A6, XXREAL_0:2;
then  ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= (abs (((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m))) + ||.(seq . ((m + k) + 1)).|| by COMPLEX1:52;
then  ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= (((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m)) + ||.(seq . ((m + k) + 1)).|| by A7, ABSVALUE:def_1;
hence  S1[k + 1] by A7, A4, A5, ABSVALUE:def_1; ::_thesis: verum
end;
assume  n >= m ; ::_thesis: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n))
then reconsider k = d - t as Element of NAT by INT_1:5;
A8: m + k = n ;
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + 0))).|| = ||.H1(X).|| by RLVECT_1:15
.= 0 by CSSPACE:42 ;
then A9: S1[ 0 ] by COMPLEX1:46;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A9, A3);
hence  ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) by A8; ::_thesis: verum
end;
now__::_thesis:_(_n_<=_m_implies_||.(((Partial_Sums_seq)_._m)_-_((Partial_Sums_seq)_._n)).||_<=_abs_(((Partial_Sums_||.seq.||)_._m)_-_((Partial_Sums_||.seq.||)_._n))_)
reconsider d = n, t = m as Integer ;
set PSseq9 = Partial_Sums ||.seq.||;
set PSseq = Partial_Sums seq;
defpred S1[ Element of NAT ] means ||.(((Partial_Sums seq) . (n + $1)) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . (n + $1)) - ((Partial_Sums ||.seq.||) . n));
A10: Partial_Sums ||.seq.|| is non-decreasing by Th35;
A11: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A12: abs (((Partial_Sums ||.seq.||) . (n + (k + 1))) - ((Partial_Sums ||.seq.||) . n)) = abs ((((Partial_Sums ||.seq.||) . (n + k)) + (||.seq.|| . ((n + k) + 1))) - ((Partial_Sums ||.seq.||) . n)) by SERIES_1:def_1
.= abs ((||.(seq . ((n + k) + 1)).|| + ((Partial_Sums ||.seq.||) . (n + k))) - ((Partial_Sums ||.seq.||) . n)) by CLVECT_2:def_3
.= abs (||.(seq . ((n + k) + 1)).|| + (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n))) ;
||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| = ||.(((seq . ((n + k) + 1)) + ((Partial_Sums seq) . (n + k))) - ((Partial_Sums seq) . n)).|| by BHSP_4:def_1
.= ||.((seq . ((n + k) + 1)) + (((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n))).|| by RLVECT_1:def_3 ;
then A13: ||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| <= ||.(seq . ((n + k) + 1)).|| + ||.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).|| by CSSPACE:46;
 (Partial_Sums ||.seq.||) . (n + k) >= (Partial_Sums ||.seq.||) . n by A10, SEQM_3:5;
then A14: ((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n) >= 0 by XREAL_1:48;
assume  S1[k] ; ::_thesis: S1[k + 1]
then  ||.(seq . ((n + k) + 1)).|| + ||.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).|| <= ||.(seq . ((n + k) + 1)).|| + (abs (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n))) by XREAL_1:7;
then  ||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| <= ||.(seq . ((n + k) + 1)).|| + (abs (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n))) by A13, XXREAL_0:2;
then A15: ||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| <= ||.(seq . ((n + k) + 1)).|| + (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n)) by A14, ABSVALUE:def_1;
 ||.(seq . ((n + k) + 1)).|| >= 0 by CSSPACE:44;
hence  S1[k + 1] by A14, A15, A12, ABSVALUE:def_1; ::_thesis: verum
end;
assume  n <= m ; ::_thesis: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n))
then reconsider k = t - d as Element of NAT by INT_1:5;
A16: n + k = m ;
||.(((Partial_Sums seq) . (n + 0)) - ((Partial_Sums seq) . n)).|| = ||.H1(X).|| by RLVECT_1:15
.= 0 by CSSPACE:42 ;
then A17: S1[ 0 ] by COMPLEX1:46;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A17, A11);
hence  ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) by A16; ::_thesis: verum
end;
hence  ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) by A1; ::_thesis: verum
end;

theorem Th40: :: CLVECT_3:40
for X being ComplexUnitarySpace
for seq being sequence of X
for n, m being Element of NAT holds ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= abs ((Sum (||.seq.||,m)) - (Sum (||.seq.||,n)))
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for n, m being Element of NAT holds ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= abs ((Sum (||.seq.||,m)) - (Sum (||.seq.||,n)))
let seq be sequence of X; ::_thesis: for n, m being Element of NAT holds ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= abs ((Sum (||.seq.||,m)) - (Sum (||.seq.||,n)))
let n, m be Element of NAT ; ::_thesis: ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= abs ((Sum (||.seq.||,m)) - (Sum (||.seq.||,n)))
 ||.((Sum (seq,m)) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) by Th39;
then  ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= abs ((Sum (||.seq.||,m)) - ((Partial_Sums ||.seq.||) . n)) by SERIES_1:def_5;
hence  ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= abs ((Sum (||.seq.||,m)) - (Sum (||.seq.||,n))) by SERIES_1:def_5; ::_thesis: verum
end;

theorem :: CLVECT_3:41
for X being ComplexUnitarySpace
for seq being sequence of X
for n, m being Element of NAT holds ||.(Sum (seq,m,n)).|| <= abs (Sum (||.seq.||,m,n))
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for n, m being Element of NAT holds ||.(Sum (seq,m,n)).|| <= abs (Sum (||.seq.||,m,n))
let seq be sequence of X; ::_thesis: for n, m being Element of NAT holds ||.(Sum (seq,m,n)).|| <= abs (Sum (||.seq.||,m,n))
let n, m be Element of NAT ; ::_thesis: ||.(Sum (seq,m,n)).|| <= abs (Sum (||.seq.||,m,n))
 ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= abs ((Sum (||.seq.||,m)) - (Sum (||.seq.||,n))) by Th40;
hence  ||.(Sum (seq,m,n)).|| <= abs (Sum (||.seq.||,m,n)) by SERIES_1:def_6; ::_thesis: verum
end;

theorem :: CLVECT_3:42
for X being ComplexHilbertSpace
for seq being sequence of X st seq is absolutely_summable holds
seq is summable
proof
let X be ComplexHilbertSpace; ::_thesis: for seq being sequence of X st seq is absolutely_summable holds
seq is summable
let seq be sequence of X; ::_thesis: ( seq is absolutely_summable implies seq is summable )
assume A1: seq is absolutely_summable ; ::_thesis: seq is summable
A2: ||.seq.|| is summable by A1, Def7;
now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.(((Partial_Sums_seq)_._n)_-_((Partial_Sums_seq)_._m)).||_<_r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r
then  r / 2 > 0 ;
then consider k being Element of NAT  such that
A3: for m being Element of NAT st m >= k holds
abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k)) < r / 2 by A2, SERIES_1:21;
take k = k; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r
now__::_thesis:_for_m,_n_being_Element_of_NAT_st_m_>=_k_&_n_>=_k_holds_
||.(((Partial_Sums_seq)_._n)_-_((Partial_Sums_seq)_._m)).||_<_r
let m, n be Element of NAT ; ::_thesis: ( m >= k & n >= k implies ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r )
A4: ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| <= abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . m)) by Th39;
assume  ( m >= k & n >= k ) ; ::_thesis: ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r
then  ( abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k)) < r / 2 & abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . k)) < r / 2 ) by A3;
then A5: (abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . k))) + (abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k))) < (r / 2) + (r / 2) by XREAL_1:8;
 abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . m)) = abs ((((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . k)) - (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k))) ;
then  abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . m)) <= (abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . k))) + (abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k))) by COMPLEX1:57;
then  abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . m)) < r by A5, XXREAL_0:2;
hence  ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r by A4, XXREAL_0:2; ::_thesis: verum
end;
hence  for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ; ::_thesis: verum
end;
hence  seq is summable by Th10; ::_thesis: verum
end;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
let Cseq be Complex_Sequence;
funcCseq * seq ->  sequence of X means :Def8: :: CLVECT_3:def 8
 for n being Element of NAT holds it . n = (Cseq . n) * (seq . n);
existence
 ex b1 being sequence of X st
for n being Element of NAT holds b1 . n = (Cseq . n) * (seq . n)
proof
deffunc H2( Element of NAT ) ->  Element of the U1 of X = (Cseq . $1) * (seq . $1);
thus  ex M being sequence of X st
for n being Element of NAT holds M . n = H2(n) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = (Cseq . n) * (seq . n) ) & ( for n being Element of NAT holds b2 . n = (Cseq . n) * (seq . n) ) holds
b1 = b2
proof
let seq1, seq2 be sequence of X; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = (Cseq . n) * (seq . n) ) & ( for n being Element of NAT holds seq2 . n = (Cseq . n) * (seq . n) ) implies seq1 = seq2 )
assume that
A1: for n being Element of NAT holds seq1 . n = (Cseq . n) * (seq . n) and
A2: for n being Element of NAT holds seq2 . n = (Cseq . n) * (seq . n) ; ::_thesis: seq1 = seq2
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_seq2_._n
let n be Element of NAT ; ::_thesis: seq1 . n = seq2 . n
 seq1 . n = (Cseq . n) * (seq . n) by A1;
hence  seq1 . n = seq2 . n by A2; ::_thesis: verum
end;
hence  seq1 = seq2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines * CLVECT_3:def_8_:_
 for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence
for b4 being sequence of X holds
( b4 = Cseq * seq iff for n being Element of NAT holds b4 . n = (Cseq . n) * (seq . n) );

theorem :: CLVECT_3:43
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X
for Cseq being Complex_Sequence holds Cseq * (seq1 + seq2) = (Cseq * seq1) + (Cseq * seq2)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X
for Cseq being Complex_Sequence holds Cseq * (seq1 + seq2) = (Cseq * seq1) + (Cseq * seq2)
let seq1, seq2 be sequence of X; ::_thesis: for Cseq being Complex_Sequence holds Cseq * (seq1 + seq2) = (Cseq * seq1) + (Cseq * seq2)
let Cseq be Complex_Sequence; ::_thesis: Cseq * (seq1 + seq2) = (Cseq * seq1) + (Cseq * seq2)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Cseq_*_(seq1_+_seq2))_._n_=_((Cseq_*_seq1)_+_(Cseq_*_seq2))_._n
let n be Element of NAT ; ::_thesis: (Cseq * (seq1 + seq2)) . n = ((Cseq * seq1) + (Cseq * seq2)) . n
thus (Cseq * (seq1 + seq2)) . n = (Cseq . n) * ((seq1 + seq2) . n) by Def8
.= (Cseq . n) * ((seq1 . n) + (seq2 . n)) by NORMSP_1:def_2
.= ((Cseq . n) * (seq1 . n)) + ((Cseq . n) * (seq2 . n)) by CLVECT_1:def_2
.= ((Cseq * seq1) . n) + ((Cseq . n) * (seq2 . n)) by Def8
.= ((Cseq * seq1) . n) + ((Cseq * seq2) . n) by Def8
.= ((Cseq * seq1) + (Cseq * seq2)) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;
hence  Cseq * (seq1 + seq2) = (Cseq * seq1) + (Cseq * seq2) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: CLVECT_3:44
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 + Cseq2) * seq = (Cseq1 * seq) + (Cseq2 * seq)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 + Cseq2) * seq = (Cseq1 * seq) + (Cseq2 * seq)
let seq be sequence of X; ::_thesis: for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 + Cseq2) * seq = (Cseq1 * seq) + (Cseq2 * seq)
let Cseq1, Cseq2 be Complex_Sequence; ::_thesis: (Cseq1 + Cseq2) * seq = (Cseq1 * seq) + (Cseq2 * seq)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((Cseq1_+_Cseq2)_*_seq)_._n_=_((Cseq1_*_seq)_+_(Cseq2_*_seq))_._n
let n be Element of NAT ; ::_thesis: ((Cseq1 + Cseq2) * seq) . n = ((Cseq1 * seq) + (Cseq2 * seq)) . n
thus ((Cseq1 + Cseq2) * seq) . n = ((Cseq1 + Cseq2) . n) * (seq . n) by Def8
.= ((Cseq1 . n) + (Cseq2 . n)) * (seq . n) by VALUED_1:1
.= ((Cseq1 . n) * (seq . n)) + ((Cseq2 . n) * (seq . n)) by CLVECT_1:def_3
.= ((Cseq1 * seq) . n) + ((Cseq2 . n) * (seq . n)) by Def8
.= ((Cseq1 * seq) . n) + ((Cseq2 * seq) . n) by Def8
.= ((Cseq1 * seq) + (Cseq2 * seq)) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;
hence  (Cseq1 + Cseq2) * seq = (Cseq1 * seq) + (Cseq2 * seq) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: CLVECT_3:45
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq)
let seq be sequence of X; ::_thesis: for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq)
let Cseq1, Cseq2 be Complex_Sequence; ::_thesis: (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((Cseq1_(#)_Cseq2)_*_seq)_._n_=_(Cseq1_*_(Cseq2_*_seq))_._n
let n be Element of NAT ; ::_thesis: ((Cseq1 (#) Cseq2) * seq) . n = (Cseq1 * (Cseq2 * seq)) . n
thus ((Cseq1 (#) Cseq2) * seq) . n = ((Cseq1 (#) Cseq2) . n) * (seq . n) by Def8
.= ((Cseq1 . n) * (Cseq2 . n)) * (seq . n) by VALUED_1:5
.= (Cseq1 . n) * ((Cseq2 . n) * (seq . n)) by CLVECT_1:def_4
.= (Cseq1 . n) * ((Cseq2 * seq) . n) by Def8
.= (Cseq1 * (Cseq2 * seq)) . n by Def8 ; ::_thesis: verum
end;
hence  (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th46: :: CLVECT_3:46
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence
for z being Complex holds (z (#) Cseq) * seq = z * (Cseq * seq)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for Cseq being Complex_Sequence
for z being Complex holds (z (#) Cseq) * seq = z * (Cseq * seq)
let seq be sequence of X; ::_thesis: for Cseq being Complex_Sequence
for z being Complex holds (z (#) Cseq) * seq = z * (Cseq * seq)
let Cseq be Complex_Sequence; ::_thesis: for z being Complex holds (z (#) Cseq) * seq = z * (Cseq * seq)
let z be Complex; ::_thesis: (z (#) Cseq) * seq = z * (Cseq * seq)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((z_(#)_Cseq)_*_seq)_._n_=_(z_*_(Cseq_*_seq))_._n
let n be Element of NAT ; ::_thesis: ((z (#) Cseq) * seq) . n = (z * (Cseq * seq)) . n
thus ((z (#) Cseq) * seq) . n = ((z (#) Cseq) . n) * (seq . n) by Def8
.= (z * (Cseq . n)) * (seq . n) by VALUED_1:6
.= z * ((Cseq . n) * (seq . n)) by CLVECT_1:def_4
.= z * ((Cseq * seq) . n) by Def8
.= (z * (Cseq * seq)) . n by CLVECT_1:def_14 ; ::_thesis: verum
end;
hence  (z (#) Cseq) * seq = z * (Cseq * seq) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: CLVECT_3:47
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence holds Cseq * (- seq) = (- Cseq) * seq
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for Cseq being Complex_Sequence holds Cseq * (- seq) = (- Cseq) * seq
let seq be sequence of X; ::_thesis: for Cseq being Complex_Sequence holds Cseq * (- seq) = (- Cseq) * seq
let Cseq be Complex_Sequence; ::_thesis: Cseq * (- seq) = (- Cseq) * seq
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Cseq_*_(-_seq))_._n_=_((-_Cseq)_*_seq)_._n
let n be Element of NAT ; ::_thesis: (Cseq * (- seq)) . n = ((- Cseq) * seq) . n
thus (Cseq * (- seq)) . n = (Cseq . n) * ((- seq) . n) by Def8
.= (Cseq . n) * (- (seq . n)) by BHSP_1:44
.= (- (Cseq . n)) * (seq . n) by CLVECT_1:6
.= ((- Cseq) . n) * (seq . n) by VALUED_1:8
.= ((- Cseq) * seq) . n by Def8 ; ::_thesis: verum
end;
hence  Cseq * (- seq) = (- Cseq) * seq by FUNCT_2:63; ::_thesis: verum
end;

theorem Th48: :: CLVECT_3:48
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds
Cseq * seq is convergent
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds
Cseq * seq is convergent
let seq be sequence of X; ::_thesis: for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds
Cseq * seq is convergent
let Cseq be Complex_Sequence; ::_thesis: ( Cseq is convergent & seq is convergent implies Cseq * seq is convergent )
assume that
A1: Cseq is convergent and
A2: seq is convergent ; ::_thesis: Cseq * seq is convergent
consider p being Element of COMPLEX  such that
A3: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
|.((Cseq . n) - p).| < r by A1, COMSEQ_2:def_5;
consider g being Point of X such that
A4: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq . n) - g).|| < r by A2, CLVECT_2:9;
now__::_thesis:_ex_h_being_Element_of_the_U1_of_X_st_
for_r_being_Real_st_r_>_0_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_m_holds_
||.(((Cseq_*_seq)_._n)_-_h).||_<_r
take h = p * g; ::_thesis: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(((Cseq * seq) . n) - h).|| < r
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(((Cseq * seq) . n) - h).|| < r )
 Cseq is bounded by A1;
then consider b being Real such that
A5: b > 0 and
A6: for n being Element of NAT holds |.(Cseq . n).| < b by COMSEQ_2:8;
A7: b + ||.g.|| > 0 + 0 by A5, CSSPACE:44, XREAL_1:8;
assume A8: r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(((Cseq * seq) . n) - h).|| < r
then consider m1 being Element of NAT  such that
A9: for n being Element of NAT st n >= m1 holds
|.((Cseq . n) - p).| < r / (b + ||.g.||) by A3, A7;
consider m2 being Element of NAT  such that
A10: for n being Element of NAT st n >= m2 holds
||.((seq . n) - g).|| < r / (b + ||.g.||) by A4, A7, A8;
take m = m1 + m2; ::_thesis: for n being Element of NAT st n >= m holds
||.(((Cseq * seq) . n) - h).|| < r
let n be Element of NAT ; ::_thesis: ( n >= m implies ||.(((Cseq * seq) . n) - h).|| < r )
assume A11: n >= m ; ::_thesis: ||.(((Cseq * seq) . n) - h).|| < r
 m1 + m2 >= m1 by NAT_1:12;
then  n >= m1 by A11, XXREAL_0:2;
then  ( ||.g.|| >= 0 & |.((Cseq . n) - p).| <= r / (b + ||.g.||) ) by A9, CSSPACE:44;
then A12: ||.g.|| * |.((Cseq . n) - p).| <= ||.g.|| * (r / (b + ||.g.||)) by XREAL_1:64;
A13: ( |.(Cseq . n).| >= 0 & ||.((seq . n) - g).|| >= 0 ) by COMPLEX1:46, CSSPACE:44;
 m >= m2 by NAT_1:12;
then  n >= m2 by A11, XXREAL_0:2;
then A14: ||.((seq . n) - g).|| < r / (b + ||.g.||) by A10;
 |.(Cseq . n).| < b by A6;
then  |.(Cseq . n).| * ||.((seq . n) - g).|| < b * (r / (b + ||.g.||)) by A14, A13, XREAL_1:96;
then  (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < (b * (r / (b + ||.g.||))) + (||.g.|| * (r / (b + ||.g.||))) by A12, XREAL_1:8;
then  (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < ((b * r) / (b + ||.g.||)) + (||.g.|| * (r / (b + ||.g.||))) by XCMPLX_1:74;
then  (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < ((b * r) / (b + ||.g.||)) + ((||.g.|| * r) / (b + ||.g.||)) by XCMPLX_1:74;
then  (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < ((b * r) + (||.g.|| * r)) / (b + ||.g.||) by XCMPLX_1:62;
then  (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < ((b + ||.g.||) * r) / (b + ||.g.||) ;
then A15: (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < r by A7, XCMPLX_1:89;
||.(((Cseq * seq) . n) - (p * g)).|| = ||.(((Cseq . n) * (seq . n)) - (p * g)).|| by Def8
.= ||.((((Cseq . n) * (seq . n)) - (p * g)) + H1(X)).|| by RLVECT_1:4
.= ||.((((Cseq . n) * (seq . n)) - (p * g)) + (((Cseq . n) * g) - ((Cseq . n) * g))).|| by RLVECT_1:15
.= ||.(((Cseq . n) * (seq . n)) - ((p * g) - (((Cseq . n) * g) - ((Cseq . n) * g)))).|| by RLVECT_1:29
.= ||.(((Cseq . n) * (seq . n)) - (((Cseq . n) * g) + ((p * g) - ((Cseq . n) * g)))).|| by RLVECT_1:29
.= ||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * g)) - ((p * g) - ((Cseq . n) * g))).|| by RLVECT_1:27
.= ||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * g)) + (((Cseq . n) * g) - (p * g))).|| by RLVECT_1:33 ;
then  ||.(((Cseq * seq) . n) - (p * g)).|| <= ||.(((Cseq . n) * (seq . n)) - ((Cseq . n) * g)).|| + ||.(((Cseq . n) * g) - (p * g)).|| by CSSPACE:46;
then  ||.(((Cseq * seq) . n) - (p * g)).|| <= ||.((Cseq . n) * ((seq . n) - g)).|| + ||.(((Cseq . n) * g) - (p * g)).|| by CLVECT_1:9;
then  ||.(((Cseq * seq) . n) - (p * g)).|| <= ||.((Cseq . n) * ((seq . n) - g)).|| + ||.(((Cseq . n) - p) * g).|| by CLVECT_1:10;
then  ||.(((Cseq * seq) . n) - (p * g)).|| <= (|.(Cseq . n).| * ||.((seq . n) - g).||) + ||.(((Cseq . n) - p) * g).|| by CSSPACE:43;
then  ||.(((Cseq * seq) . n) - (p * g)).|| <= (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) by CSSPACE:43;
hence  ||.(((Cseq * seq) . n) - h).|| < r by A15, XXREAL_0:2; ::_thesis: verum
end;
hence  Cseq * seq is convergent by CLVECT_2:9; ::_thesis: verum
end;

theorem :: CLVECT_3:49
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence st Cseq is bounded & seq is bounded holds
Cseq * seq is bounded
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for Cseq being Complex_Sequence st Cseq is bounded & seq is bounded holds
Cseq * seq is bounded
let seq be sequence of X; ::_thesis: for Cseq being Complex_Sequence st Cseq is bounded & seq is bounded holds
Cseq * seq is bounded
let Cseq be Complex_Sequence; ::_thesis: ( Cseq is bounded & seq is bounded implies Cseq * seq is bounded )
assume that
A1: Cseq is bounded and
A2: seq is bounded ; ::_thesis: Cseq * seq is bounded
consider M1 being Real such that
A3: M1 > 0 and
A4: for n being Element of NAT holds |.(Cseq . n).| < M1 by A1, COMSEQ_2:8;
consider M2 being Real such that
A5: M2 > 0 and
A6: for n being Element of NAT holds ||.(seq . n).|| <= M2 by A2, CLVECT_2:def_10;
now__::_thesis:_ex_M_being_Element_of_REAL_st_
(_M_>_0_&_(_for_n_being_Element_of_NAT_holds_||.((Cseq_*_seq)_._n).||_<=_M_)_)
set M = M1 * M2;
take M = M1 * M2; ::_thesis: ( M > 0 & ( for n being Element of NAT holds ||.((Cseq * seq) . n).|| <= M ) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((Cseq_*_seq)_._n).||_<=_M
let n be Element of NAT ; ::_thesis: ||.((Cseq * seq) . n).|| <= M
 |.(Cseq . n).| >= 0 by COMPLEX1:46;
then A7: |.(Cseq . n).| * ||.(seq . n).|| <= |.(Cseq . n).| * M2 by A6, XREAL_1:64;
 |.(Cseq . n).| <= M1 by A4;
then A8: |.(Cseq . n).| * M2 <= M1 * M2 by A5, XREAL_1:64;
||.((Cseq * seq) . n).|| = ||.((Cseq . n) * (seq . n)).|| by Def8
.= |.(Cseq . n).| * ||.(seq . n).|| by CSSPACE:43 ;
hence  ||.((Cseq * seq) . n).|| <= M by A7, A8, XXREAL_0:2; ::_thesis: verum
end;
hence  ( M > 0 & ( for n being Element of NAT holds ||.((Cseq * seq) . n).|| <= M ) ) by A3, A5; ::_thesis: verum
end;
hence  Cseq * seq is bounded by CLVECT_2:def_10; ::_thesis: verum
end;

theorem :: CLVECT_3:50
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds
( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) )
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds
( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) )
let seq be sequence of X; ::_thesis: for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds
( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) )
let Cseq be Complex_Sequence; ::_thesis: ( Cseq is convergent & seq is convergent implies ( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) ) )
assume that
A1: Cseq is convergent and
A2: seq is convergent ; ::_thesis: ( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) )
 Cseq is bounded by A1;
then consider b being Real such that
A3: b > 0 and
A4: for n being Element of NAT holds |.(Cseq . n).| < b by COMSEQ_2:8;
A5: b + ||.(lim seq).|| > 0 + 0 by A3, CSSPACE:44, XREAL_1:8;
A6: ||.(lim seq).|| >= 0 by CSSPACE:44;
A7: now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_m_holds_
dist_(((Cseq_*_seq)_._n),((lim_Cseq)_*_(lim_seq)))_<_r
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r
then A8: r / (b + ||.(lim seq).||) > 0 by A5;
then consider m1 being Element of NAT  such that
A9: for n being Element of NAT st n >= m1 holds
|.((Cseq . n) - (lim Cseq)).| < r / (b + ||.(lim seq).||) by A1, COMSEQ_2:def_6;
consider m2 being Element of NAT  such that
A10: for n being Element of NAT st n >= m2 holds
dist ((seq . n),(lim seq)) < r / (b + ||.(lim seq).||) by A2, A8, CLVECT_2:def_2;
take m = m1 + m2; ::_thesis: for n being Element of NAT st n >= m holds
dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r )
assume A11: n >= m ; ::_thesis: dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r
 m1 + m2 >= m1 by NAT_1:12;
then  n >= m1 by A11, XXREAL_0:2;
then  |.((Cseq . n) - (lim Cseq)).| <= r / (b + ||.(lim seq).||) by A9;
then A12: ||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).| <= ||.(lim seq).|| * (r / (b + ||.(lim seq).||)) by A6, XREAL_1:64;
A13: ||.((seq . n) - (lim seq)).|| >= 0 by CSSPACE:44;
 m >= m2 by NAT_1:12;
then  n >= m2 by A11, XXREAL_0:2;
then  dist ((seq . n),(lim seq)) < r / (b + ||.(lim seq).||) by A10;
then A14: ||.((seq . n) - (lim seq)).|| < r / (b + ||.(lim seq).||) by CSSPACE:def_16;
 ( |.(Cseq . n).| < b & |.(Cseq . n).| >= 0 ) by A4, COMPLEX1:46;
then  |.(Cseq . n).| * ||.((seq . n) - (lim seq)).|| < b * (r / (b + ||.(lim seq).||)) by A14, A13, XREAL_1:96;
then  (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < (b * (r / (b + ||.(lim seq).||))) + (||.(lim seq).|| * (r / (b + ||.(lim seq).||))) by A12, XREAL_1:8;
then  (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < ((b * r) / (b + ||.(lim seq).||)) + (||.(lim seq).|| * (r / (b + ||.(lim seq).||))) by XCMPLX_1:74;
then  (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < ((b * r) / (b + ||.(lim seq).||)) + ((||.(lim seq).|| * r) / (b + ||.(lim seq).||)) by XCMPLX_1:74;
then  (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < ((b * r) + (||.(lim seq).|| * r)) / (b + ||.(lim seq).||) by XCMPLX_1:62;
then  (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < ((b + ||.(lim seq).||) * r) / (b + ||.(lim seq).||) ;
then A15: (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < r by A5, XCMPLX_1:89;
||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| = ||.(((Cseq . n) * (seq . n)) - ((lim Cseq) * (lim seq))).|| by Def8
.= ||.((((Cseq . n) * (seq . n)) - ((lim Cseq) * (lim seq))) + H1(X)).|| by RLVECT_1:4
.= ||.((((Cseq . n) * (seq . n)) - ((lim Cseq) * (lim seq))) + (((Cseq . n) * (lim seq)) - ((Cseq . n) * (lim seq)))).|| by RLVECT_1:15
.= ||.(((Cseq . n) * (seq . n)) - (((lim Cseq) * (lim seq)) - (((Cseq . n) * (lim seq)) - ((Cseq . n) * (lim seq))))).|| by RLVECT_1:29
.= ||.(((Cseq . n) * (seq . n)) - (((Cseq . n) * (lim seq)) + (((lim Cseq) * (lim seq)) - ((Cseq . n) * (lim seq))))).|| by RLVECT_1:29
.= ||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq))) - (((lim Cseq) * (lim seq)) - ((Cseq . n) * (lim seq)))).|| by RLVECT_1:27
.= ||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq))) + (((Cseq . n) * (lim seq)) - ((lim Cseq) * (lim seq)))).|| by RLVECT_1:33 ;
then  ||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| <= ||.(((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq))).|| + ||.(((Cseq . n) * (lim seq)) - ((lim Cseq) * (lim seq))).|| by CSSPACE:46;
then  ||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| <= ||.((Cseq . n) * ((seq . n) - (lim seq))).|| + ||.(((Cseq . n) * (lim seq)) - ((lim Cseq) * (lim seq))).|| by CLVECT_1:9;
then  ||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| <= ||.((Cseq . n) * ((seq . n) - (lim seq))).|| + ||.(((Cseq . n) - (lim Cseq)) * (lim seq)).|| by CLVECT_1:10;
then  ||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| <= (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + ||.(((Cseq . n) - (lim Cseq)) * (lim seq)).|| by CSSPACE:43;
then  ||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| <= (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) by CSSPACE:43;
then  ||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| < r by A15, XXREAL_0:2;
hence  dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r by CSSPACE:def_16; ::_thesis: verum
end;
 Cseq * seq is convergent by A1, A2, Th48;
hence  ( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) ) by A7, CLVECT_2:def_2; ::_thesis: verum
end;

definition
let Cseq be Complex_Sequence;
attrCseq is Cauchy  means :Def9: :: CLVECT_3:def 9
 for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
|.((Cseq . n) - (Cseq . m)).| < r;
end;

:: deftheorem Def9 defines Cauchy CLVECT_3:def_9_:_
 for Cseq being Complex_Sequence holds
( Cseq is Cauchy iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
|.((Cseq . n) - (Cseq . m)).| < r );

theorem :: CLVECT_3:51
for Cseq being Complex_Sequence
for X being ComplexHilbertSpace
for seq being sequence of X st seq is Cauchy & Cseq is Cauchy holds
Cseq * seq is Cauchy
proof
let Cseq be Complex_Sequence; ::_thesis: for X being ComplexHilbertSpace
for seq being sequence of X st seq is Cauchy & Cseq is Cauchy holds
Cseq * seq is Cauchy
let X be ComplexHilbertSpace; ::_thesis: for seq being sequence of X st seq is Cauchy & Cseq is Cauchy holds
Cseq * seq is Cauchy
let seq be sequence of X; ::_thesis: ( seq is Cauchy & Cseq is Cauchy implies Cseq * seq is Cauchy )
assume that
A1: seq is Cauchy and
A2: Cseq is Cauchy ; ::_thesis: Cseq * seq is Cauchy
now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
|.((Cseq_._n)_-_(Cseq_._k)).|_<_r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
|.((Cseq . n) - (Cseq . k)).| < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
|.((Cseq . n) - (Cseq . k)).| < r
then consider k being Element of NAT  such that
A3: for n, m being Element of NAT st n >= k & m >= k holds
|.((Cseq . n) - (Cseq . m)).| < r by A2, Def9;
take k = k; ::_thesis: for n being Element of NAT st n >= k holds
|.((Cseq . n) - (Cseq . k)).| < r
thus  for n being Element of NAT st n >= k holds
|.((Cseq . n) - (Cseq . k)).| < r by A3; ::_thesis: verum
end;
then A4: Cseq is convergent by COMSEQ_3:46;
 seq is convergent by A1, CLVECT_2:def_11;
hence  Cseq * seq is Cauchy by A4, Th48, CLVECT_2:65; ::_thesis: verum
end;

theorem Th52: :: CLVECT_3:52
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence
for n being Element of NAT holds (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Cseq * seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for Cseq being Complex_Sequence
for n being Element of NAT holds (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Cseq * seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))
let seq be sequence of X; ::_thesis: for Cseq being Complex_Sequence
for n being Element of NAT holds (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Cseq * seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))
let Cseq be Complex_Sequence; ::_thesis: for n being Element of NAT holds (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Cseq * seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))
defpred S1[ Element of NAT ] means (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . $1 = ((Partial_Sums (Cseq * seq)) . ($1 + 1)) - ((Cseq * (Partial_Sums seq)) . ($1 + 1));
A1: (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . 0 = ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq)) . 0 by BHSP_4:def_1
.= ((Cseq - (Cseq ^\ 1)) . 0) * ((Partial_Sums seq) . 0) by Def8
.= ((Cseq + (- (Cseq ^\ 1))) . 0) * (seq . 0) by BHSP_4:def_1
.= ((Cseq . 0) + ((- (Cseq ^\ 1)) . 0)) * (seq . 0) by VALUED_1:1
.= ((Cseq . 0) + (- ((Cseq ^\ 1) . 0))) * (seq . 0) by VALUED_1:8
.= ((Cseq . 0) - ((Cseq ^\ 1) . 0)) * (seq . 0)
.= ((Cseq . 0) - (Cseq . (0 + 1))) * (seq . 0) by NAT_1:def_3
.= ((Cseq . 0) * (seq . 0)) - ((Cseq . 1) * (seq . 0)) by CLVECT_1:10 ;
A2: (Cseq * (Partial_Sums seq)) . (0 + 1) = (Cseq . (0 + 1)) * ((Partial_Sums seq) . (0 + 1)) by Def8
.= (Cseq . (0 + 1)) * (((Partial_Sums seq) . 0) + (seq . (0 + 1))) by BHSP_4:def_1
.= (Cseq . 1) * ((seq . 0) + (seq . 1)) by BHSP_4:def_1
.= ((Cseq . 1) * (seq . 0)) + ((Cseq . 1) * (seq . 1)) by CLVECT_1:def_2 ;
A3: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
then  ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Cseq * seq)) . (n + 1)) - (((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))) by RLVECT_1:29;
then A4: ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Cseq * seq)) . (n + 1)) - H1(X) by RLVECT_1:15;
(Partial_Sums (Cseq * seq)) . ((n + 1) + 1) = ((Partial_Sums (Cseq * seq)) . (n + 1)) + ((Cseq * seq) . ((n + 1) + 1)) by BHSP_4:def_1
.= (((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1))) + ((Cseq * seq) . ((n + 1) + 1)) by A4, RLVECT_1:13
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Cseq * seq) . ((n + 1) + 1))) by RLVECT_1:def_3
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Cseq . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq * seq) . ((n + 1) + 1))) by Def8
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) - (Cseq . ((n + 1) + 1))) + (Cseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by Def8
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) - (Cseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by CLVECT_1:def_3
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) - ((Cseq ^\ 1) . (n + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by NAT_1:def_3
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) + (- ((Cseq ^\ 1) . (n + 1)))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) + ((- (Cseq ^\ 1)) . (n + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by VALUED_1:8
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by VALUED_1:1
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by RLVECT_1:def_3
.= (((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1)))) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by RLVECT_1:def_3
.= (((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq)) . (n + 1))) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by Def8
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by BHSP_4:def_1
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + ((Cseq . ((n + 1) + 1)) * (((Partial_Sums seq) . (n + 1)) + (seq . ((n + 1) + 1)))) by CLVECT_1:def_2
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . ((n + 1) + 1))) by BHSP_4:def_1
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + ((Cseq * (Partial_Sums seq)) . ((n + 1) + 1)) by Def8 ;
then  ((Partial_Sums (Cseq * seq)) . ((n + 1) + 1)) - ((Cseq * (Partial_Sums seq)) . ((n + 1) + 1)) = ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + (((Cseq * (Partial_Sums seq)) . ((n + 1) + 1)) - ((Cseq * (Partial_Sums seq)) . ((n + 1) + 1))) by RLVECT_1:def_3;
then  ((Partial_Sums (Cseq * seq)) . ((n + 1) + 1)) - ((Cseq * (Partial_Sums seq)) . ((n + 1) + 1)) = ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + H1(X) by RLVECT_1:15;
hence  S1[n + 1] by RLVECT_1:4; ::_thesis: verum
end;
(Partial_Sums (Cseq * seq)) . (0 + 1) = ((Partial_Sums (Cseq * seq)) . 0) + ((Cseq * seq) . (0 + 1)) by BHSP_4:def_1
.= ((Cseq * seq) . 0) + ((Cseq * seq) . 1) by BHSP_4:def_1
.= ((Cseq . 0) * (seq . 0)) + ((Cseq * seq) . 1) by Def8
.= ((Cseq . 0) * (seq . 0)) + ((Cseq . 1) * (seq . 1)) by Def8 ;
then (Partial_Sums (Cseq * seq)) . (0 + 1) = (((Cseq . 0) * (seq . 0)) + H1(X)) + ((Cseq . 1) * (seq . 1)) by RLVECT_1:4
.= (((Cseq . 0) * (seq . 0)) + (((Cseq . 1) * (seq . 0)) - ((Cseq . 1) * (seq . 0)))) + ((Cseq . 1) * (seq . 1)) by RLVECT_1:15
.= ((((Cseq . 0) * (seq . 0)) + (- ((Cseq . 1) * (seq . 0)))) + ((Cseq . 1) * (seq . 0))) + ((Cseq . 1) * (seq . 1)) by RLVECT_1:def_3
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . 0) + ((Cseq * (Partial_Sums seq)) . (0 + 1)) by A1, A2, RLVECT_1:def_3 ;
then  ((Partial_Sums (Cseq * seq)) . (0 + 1)) - ((Cseq * (Partial_Sums seq)) . (0 + 1)) = ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . 0) + (((Cseq * (Partial_Sums seq)) . (0 + 1)) - ((Cseq * (Partial_Sums seq)) . (0 + 1))) by RLVECT_1:def_3;
then  ((Partial_Sums (Cseq * seq)) . (0 + 1)) - ((Cseq * (Partial_Sums seq)) . (0 + 1)) = ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . 0) + H1(X) by RLVECT_1:15;
then A5: S1[ 0 ] by RLVECT_1:4;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A3); ::_thesis: verum
end;

theorem Th53: :: CLVECT_3:53
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence
for n being Element of NAT holds (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for Cseq being Complex_Sequence
for n being Element of NAT holds (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n)
let seq be sequence of X; ::_thesis: for Cseq being Complex_Sequence
for n being Element of NAT holds (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n)
let Cseq be Complex_Sequence; ::_thesis: for n being Element of NAT holds (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n)
let n be Element of NAT ; ::_thesis: (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n)
 ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1)) = (((Partial_Sums (Cseq * seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))) + ((Cseq * (Partial_Sums seq)) . (n + 1)) by Th52;
then  ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Cseq * seq)) . (n + 1)) - (((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))) by RLVECT_1:29;
then  ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Cseq * seq)) . (n + 1)) - H1(X) by RLVECT_1:15;
then  (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums ((Cseq + (- (Cseq ^\ 1))) * (Partial_Sums seq))) . n) by RLVECT_1:13;
then  (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums ((((- 1r) (#) (Cseq ^\ 1)) - (- Cseq)) * (Partial_Sums seq))) . n) by COMSEQ_1:11;
then  (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums ((((- 1r) (#) (Cseq ^\ 1)) - ((- 1r) (#) Cseq)) * (Partial_Sums seq))) . n) by COMSEQ_1:11;
then  (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums (((- 1r) (#) ((Cseq ^\ 1) - Cseq)) * (Partial_Sums seq))) . n) by COMSEQ_1:18;
then  (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums ((- 1r) * (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq)))) . n) by Th46;
then  (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + (((- 1r) * (Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq)))) . n) by Th3;
then  (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((- 1r) * ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n)) by CLVECT_1:def_14;
hence  (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n) by CLVECT_1:3; ::_thesis: verum
end;

theorem :: CLVECT_3:54
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence
for n being Element of NAT holds Sum ((Cseq * seq),(n + 1)) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - (Sum ((((Cseq ^\ 1) - Cseq) * (Partial_Sums seq)),n)) by Th53;