:: BHSP_4 semantic presentation

begin

            deffunc H1( RealUnitarySpace) ->  Element of the carrier of $1 = 0. $1;

definition
let X be non empty addLoopStr ;
let seq be sequence of X;
func Partial_Sums seq ->  sequence of X means :Def1: :: BHSP_4:def 1
( it . 0 = seq . 0 & ( for n being Element of NAT holds it . (n + 1) = (it . n) + (seq . (n + 1)) ) );
existence
 ex b1 being sequence of X st
( b1 . 0 = seq . 0 & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) + (seq . (n + 1)) ) )
proof
deffunc H2( Nat, Point of X) ->  Element of the carrier of X = $2 + (seq . ($1 + 1));
consider f being Function of NAT, the carrier of X such that
A1: ( f . 0 = seq . 0 & ( for n being Nat holds f . (n + 1) = H2(n,f . n) ) ) from NAT_1:sch_12();
take  f ; ::_thesis: ( f . 0 = seq . 0 & ( for n being Element of NAT holds f . (n + 1) = (f . n) + (seq . (n + 1)) ) )
thus  ( f . 0 = seq . 0 & ( for n being Element of NAT holds f . (n + 1) = (f . n) + (seq . (n + 1)) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being sequence of X st b1 . 0 = seq . 0 & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) + (seq . (n + 1)) ) & b2 . 0 = seq . 0 & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) + (seq . (n + 1)) ) holds
b1 = b2
proof
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 . 0 = seq . 0 & ( for n being Element of NAT holds seq1 . (n + 1) = (seq1 . n) + (seq . (n + 1)) ) & seq2 . 0 = seq . 0 & ( for n being Element of NAT holds seq2 . (n + 1) = (seq2 . n) + (seq . (n + 1)) ) implies seq1 = seq2 )
assume that
A2: seq1 . 0 = seq . 0 and
A3: for n being Element of NAT holds seq1 . (n + 1) = (seq1 . n) + (seq . (n + 1)) and
A4: seq2 . 0 = seq . 0 and
A5: for n being Element of NAT holds seq2 . (n + 1) = (seq2 . n) + (seq . (n + 1)) ; ::_thesis: seq1 = seq2
defpred S1[ Element of NAT ] means seq1 . $1 = seq2 . $1;
A6: 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  seq1 . k = seq2 . k ; ::_thesis: S1[k + 1]
hence seq1 . (k + 1) = (seq2 . k) + (seq . (k + 1)) by A3
.= seq2 . (k + 1) by A5 ;
::_thesis: verum
end;
A7: S1[ 0 ] by A2, A4;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A6);
hence  seq1 = seq2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Partial_Sums BHSP_4:def_1_:_
 for X being non empty addLoopStr
for seq, b3 being sequence of X holds
( b3 = Partial_Sums seq iff ( b3 . 0 = seq . 0 & ( for n being Element of NAT holds b3 . (n + 1) = (b3 . n) + (seq . (n + 1)) ) ) );

theorem Th1: :: BHSP_4:1
for X being non empty Abelian add-associative addLoopStr
for seq1, seq2 being sequence of X holds (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2)
proof
let X be non empty Abelian add-associative addLoopStr ; ::_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 Def1
.= (((Partial_Sums seq1) . n) + (seq1 . (n + 1))) + ((seq2 . (n + 1)) + ((Partial_Sums seq2) . n)) by Def1
.= ((((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 Def1
.= (seq1 . 0) + (seq2 . 0) by Def1
.= (seq1 + seq2) . 0 by NORMSP_1:def_2 ;
hence  (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) by A1, Def1; ::_thesis: verum
end;

theorem Th2: :: BHSP_4:2
for X being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for seq1, seq2 being sequence of X holds (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2)
proof
let X be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_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 Def1
.= (((Partial_Sums seq1) . n) + (seq1 . (n + 1))) - ((seq2 . (n + 1)) + ((Partial_Sums seq2) . n)) by Def1
.= ((((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 Def1
.= (seq1 . 0) - (seq2 . 0) by Def1
.= (seq1 - seq2) . 0 by NORMSP_1:def_3 ;
hence  (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2) by A1, Def1; ::_thesis: verum
end;

theorem Th3: :: BHSP_4:3
for a being Real
for X being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for seq being sequence of X holds Partial_Sums (a * seq) = a * (Partial_Sums seq)
proof
let a be Real; ::_thesis: for X being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for seq being sequence of X holds Partial_Sums (a * seq) = a * (Partial_Sums seq)
let X be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for seq being sequence of X holds Partial_Sums (a * seq) = a * (Partial_Sums seq)
let seq be sequence of X; ::_thesis: Partial_Sums (a * seq) = a * (Partial_Sums seq)
set PSseq = Partial_Sums seq;
A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_(a_*_(Partial_Sums_seq))_._(n_+_1)_=_((a_*_(Partial_Sums_seq))_._n)_+_((a_*_seq)_._(n_+_1))
let n be Element of NAT ; ::_thesis: (a * (Partial_Sums seq)) . (n + 1) = ((a * (Partial_Sums seq)) . n) + ((a * seq) . (n + 1))
thus (a * (Partial_Sums seq)) . (n + 1) = a * ((Partial_Sums seq) . (n + 1)) by NORMSP_1:def_5
.= a * (((Partial_Sums seq) . n) + (seq . (n + 1))) by Def1
.= (a * ((Partial_Sums seq) . n)) + (a * (seq . (n + 1))) by RLVECT_1:def_5
.= ((a * (Partial_Sums seq)) . n) + (a * (seq . (n + 1))) by NORMSP_1:def_5
.= ((a * (Partial_Sums seq)) . n) + ((a * seq) . (n + 1)) by NORMSP_1:def_5 ; ::_thesis: verum
end;
(a * (Partial_Sums seq)) . 0 = a * ((Partial_Sums seq) . 0) by NORMSP_1:def_5
.= a * (seq . 0) by Def1
.= (a * seq) . 0 by NORMSP_1:def_5 ;
hence  Partial_Sums (a * seq) = a * (Partial_Sums seq) by A1, Def1; ::_thesis: verum
end;


theorem :: BHSP_4:4
for X being RealUnitarySpace
for seq being sequence of X holds Partial_Sums (- seq) = - (Partial_Sums seq)
proof
let X be RealUnitarySpace; ::_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 ((- 1) * seq) = (- 1) * (Partial_Sums seq) by Th3;
then  Partial_Sums (- seq) = (- 1) * (Partial_Sums seq) by BHSP_1:55;
hence  Partial_Sums (- seq) = - (Partial_Sums seq) by BHSP_1:55; ::_thesis: verum
end;

theorem :: BHSP_4:5
for a, b being Real
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds (a * (Partial_Sums seq1)) + (b * (Partial_Sums seq2)) = Partial_Sums ((a * seq1) + (b * seq2))
proof
let a, b be Real; ::_thesis: for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds (a * (Partial_Sums seq1)) + (b * (Partial_Sums seq2)) = Partial_Sums ((a * seq1) + (b * seq2))
let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X holds (a * (Partial_Sums seq1)) + (b * (Partial_Sums seq2)) = Partial_Sums ((a * seq1) + (b * seq2))
let seq1, seq2 be sequence of X; ::_thesis: (a * (Partial_Sums seq1)) + (b * (Partial_Sums seq2)) = Partial_Sums ((a * seq1) + (b * seq2))
thus (a * (Partial_Sums seq1)) + (b * (Partial_Sums seq2)) = (Partial_Sums (a * seq1)) + (b * (Partial_Sums seq2)) by Th3
.= (Partial_Sums (a * seq1)) + (Partial_Sums (b * seq2)) by Th3
.= Partial_Sums ((a * seq1) + (b * seq2)) by Th1 ; ::_thesis: verum
end;

definition
let X be RealUnitarySpace;
let seq be sequence of X;
attrseq is summable  means :Def2: :: BHSP_4:def 2
 Partial_Sums seq is convergent ;
func Sum seq ->  Point of X equals :: BHSP_4:def 3
 lim (Partial_Sums seq);
coherence
 lim (Partial_Sums seq) is Point of X ;
end;

:: deftheorem Def2 defines summable BHSP_4:def_2_:_
 for X being RealUnitarySpace
for seq being sequence of X holds
( seq is summable iff Partial_Sums seq is convergent );

:: deftheorem  defines Sum BHSP_4:def_3_:_
 for X being RealUnitarySpace
for seq being sequence of X holds Sum seq = lim (Partial_Sums seq);

theorem :: BHSP_4:6
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 Def2;
then  (Partial_Sums seq1) + (Partial_Sums seq2) is convergent by BHSP_2:3;
then  Partial_Sums (seq1 + seq2) is convergent by Th1;
hence  seq1 + seq2 is summable by Def2; ::_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, BHSP_2:13 ; ::_thesis: verum
end;

theorem :: BHSP_4:7
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 Def2;
then  (Partial_Sums seq1) - (Partial_Sums seq2) is convergent by BHSP_2:4;
then  Partial_Sums (seq1 - seq2) is convergent by Th2;
hence  seq1 - seq2 is summable by Def2; ::_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, BHSP_2:14 ; ::_thesis: verum
end;

theorem :: BHSP_4:8
for a being Real
for X being RealUnitarySpace
for seq being sequence of X st seq is summable holds
( a * seq is summable & Sum (a * seq) = a * (Sum seq) )
proof
let a be Real; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X st seq is summable holds
( a * seq is summable & Sum (a * seq) = a * (Sum seq) )
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X st seq is summable holds
( a * seq is summable & Sum (a * seq) = a * (Sum seq) )
let seq be sequence of X; ::_thesis: ( seq is summable implies ( a * seq is summable & Sum (a * seq) = a * (Sum seq) ) )
assume  seq is summable ; ::_thesis: ( a * seq is summable & Sum (a * seq) = a * (Sum seq) )
then A1: Partial_Sums seq is convergent by Def2;
then  a * (Partial_Sums seq) is convergent by BHSP_2:5;
then  Partial_Sums (a * seq) is convergent by Th3;
hence  a * seq is summable by Def2; ::_thesis: Sum (a * seq) = a * (Sum seq)
thus  Sum (a * seq) = lim (a * (Partial_Sums seq)) by Th3
.= a * (Sum seq) by A1, BHSP_2:15 ; ::_thesis: verum
end;

theorem Th9: :: BHSP_4:9
for X being RealUnitarySpace
for seq being sequence of X st seq is summable holds
( seq is convergent & lim seq = 0. X )
proof
let X be RealUnitarySpace; ::_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 Def1
.= ((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;
 (seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq)) = seq ^\ 1
proof
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: K68(((seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq))),n) = K68((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 A2: seq ^\ 1 = ((Partial_Sums seq) ^\ 1) - (Partial_Sums seq) by A1, BHSP_1:61;
assume  seq is summable ; ::_thesis: ( seq is convergent & lim seq = 0. X )
then A3: Partial_Sums seq is convergent by Def2;
then A4: (Partial_Sums seq) ^\ 1 is convergent by BHSP_3:36;
then A5: seq ^\ 1 is convergent by A3, A2, BHSP_2:4;
hence  seq is convergent by BHSP_3:37; ::_thesis: lim seq = 0. X
 lim ((Partial_Sums seq) ^\ 1) = lim (Partial_Sums seq) by A3, BHSP_3:36;
then  lim (((Partial_Sums seq) ^\ 1) - (Partial_Sums seq)) = (lim (Partial_Sums seq)) - (lim (Partial_Sums seq)) by A3, A4, BHSP_2:14
.= H1(X) by RLVECT_1:15 ;
hence  lim seq = 0. X by A2, A5, BHSP_3:28, BHSP_3:37; ::_thesis: verum
end;

theorem Th10: :: BHSP_4:10
for X being RealHilbertSpace
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 RealHilbertSpace; ::_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 Def2;
then  Partial_Sums seq is Cauchy by BHSP_3:9;
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 BHSP_3:2; ::_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 BHSP_3:2;
then  Partial_Sums seq is convergent by BHSP_3:def_4;
hence  seq is summable by Def2; ::_thesis: verum
end;
end;

theorem :: BHSP_4:11
for X being RealUnitarySpace
for seq being sequence of X st seq is summable holds
Partial_Sums seq is bounded
proof
let X be RealUnitarySpace; ::_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 Def2;
hence  Partial_Sums seq is bounded by BHSP_3:24; ::_thesis: verum
end;

theorem Th12: :: BHSP_4:12
for X being RealUnitarySpace
for seq, seq1 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 RealUnitarySpace; ::_thesis: for seq, seq1 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 seq, seq1 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 Def1
.= ((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 Def1
.= ((seq . (0 + 1)) + (seq . 0)) - (seq . 0) by Def1
.= (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, Def1; ::_thesis: verum
end;

theorem Th13: :: BHSP_4:13
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 Def2;
then A2: (Partial_Sums (seq ^\ k)) ^\ 1 is convergent by BHSP_3:36;
 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, BHSP_2:1;
then  ( seq ^\ (k + 1) = (seq ^\ k) ^\ 1 & Partial_Sums ((seq ^\ k) ^\ 1) is convergent ) by A2, BHSP_2:4, BHSP_3:31;
hence  S1[k + 1] by Def2; ::_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 :: BHSP_4:14
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 Def2;
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 Def1
.= 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 Def1
.= ((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 Def1
.= (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 Def1
.= ((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 BHSP_3:31 ;
 seq1 is convergent by BHSP_2:1;
then  (Partial_Sums seq) ^\ (k + 1) is convergent by A2, A7, BHSP_2:3;
then  Partial_Sums seq is convergent by BHSP_3:37;
hence  seq is summable by Def2; ::_thesis: verum
end;

definition
let X be RealUnitarySpace;
let seq be sequence of X;
let n be Element of NAT ;
func Sum (seq,n) ->  Point of X equals :: BHSP_4:def 4
(Partial_Sums seq) . n;
coherence
 (Partial_Sums seq) . n is Point of X ;
end;

:: deftheorem  defines Sum BHSP_4:def_4_:_
 for X being RealUnitarySpace
for seq being sequence of X
for n being Element of NAT holds Sum (seq,n) = (Partial_Sums seq) . n;

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

theorem Th16: :: BHSP_4:16
for X being RealUnitarySpace
for seq being sequence of X holds Sum (seq,1) = (Sum (seq,0)) + (seq . 1)
proof
let X be RealUnitarySpace; ::_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 Def1
.= ((Partial_Sums seq) . 0) + (seq . 1) ;
hence  Sum (seq,1) = (Sum (seq,0)) + (seq . 1) ; ::_thesis: verum
end;

theorem Th17: :: BHSP_4:17
for X being RealUnitarySpace
for seq being sequence of X holds Sum (seq,1) = (seq . 0) + (seq . 1)
proof
let X be RealUnitarySpace; ::_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 Def1 ; ::_thesis: verum
end;

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

theorem Th19: :: BHSP_4:19
for n being Element of NAT
for X being RealUnitarySpace
for seq being sequence of X holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))
proof
let n be Element of NAT ; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))
let seq be sequence of X; ::_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 Def1
.= (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 :: BHSP_4:20
for X being RealUnitarySpace
for seq being sequence of X holds seq . 1 = (Sum (seq,1)) - (Sum (seq,0))
proof
let X be RealUnitarySpace; ::_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 RealUnitarySpace;
let seq be sequence of X;
let n, m be Element of NAT ;
func Sum (seq,n,m) ->  Point of X equals :: BHSP_4:def 5
(Sum (seq,n)) - (Sum (seq,m));
coherence
 (Sum (seq,n)) - (Sum (seq,m)) is Point of X ;
end;

:: deftheorem  defines Sum BHSP_4:def_5_:_
 for X being RealUnitarySpace
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 :: BHSP_4:21
for X being RealUnitarySpace
for seq being sequence of X holds Sum (seq,1,0) = seq . 1
proof
let X be RealUnitarySpace; ::_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 Def1
.= (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 :: BHSP_4:22
for n being Element of NAT
for X being RealUnitarySpace
for seq being sequence of X holds Sum (seq,(n + 1),n) = seq . (n + 1) by Th19;

theorem Th23: :: BHSP_4:23
for X being RealHilbertSpace
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 RealHilbertSpace; ::_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 :: BHSP_4:24
for X being RealHilbertSpace
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 RealHilbertSpace; ::_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 X be RealUnitarySpace;
let seq be sequence of X;
attrseq is absolutely_summable  means :Def6: :: BHSP_4:def 6
||.seq.|| is summable ;
end;

:: deftheorem Def6 defines absolutely_summable BHSP_4:def_6_:_
 for X being RealUnitarySpace
for seq being sequence of X holds
( seq is absolutely_summable iff ||.seq.|| is summable );

theorem :: BHSP_4:25
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_2:def_3;
hence  ||.(seq1 + seq2).|| . n >= 0 by BHSP_1:28; ::_thesis: ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n
||.(seq1 + seq2).|| . n = ||.((seq1 + seq2) . n).|| by BHSP_2:def_3
.= ||.((seq1 . n) + (seq2 . n)).|| by NORMSP_1:def_2 ;
then  ||.(seq1 + seq2).|| . n <= ||.(seq1 . n).|| + ||.(seq2 . n).|| by BHSP_1:30;
then  ||.(seq1 + seq2).|| . n <= (||.seq1.|| . n) + ||.(seq2 . n).|| by BHSP_2:def_3;
then  ||.(seq1 + seq2).|| . n <= (||.seq1.|| . n) + (||.seq2.|| . n) by BHSP_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 Def6;
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 Def6; ::_thesis: verum
end;

theorem :: BHSP_4:26
for a being Real
for X being RealUnitarySpace
for seq being sequence of X st seq is absolutely_summable holds
a * seq is absolutely_summable
proof
let a be Real; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X st seq is absolutely_summable holds
a * seq is absolutely_summable
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X st seq is absolutely_summable holds
a * seq is absolutely_summable
let seq be sequence of X; ::_thesis: ( seq is absolutely_summable implies a * seq is absolutely_summable )
A1: for n being Element of NAT holds
( ||.(a * seq).|| . n >= 0 & ||.(a * seq).|| . n <= ((abs a) (#) ||.seq.||) . n )
proof
let n be Element of NAT ; ::_thesis: ( ||.(a * seq).|| . n >= 0 & ||.(a * seq).|| . n <= ((abs a) (#) ||.seq.||) . n )
 ||.(a * seq).|| . n = ||.((a * seq) . n).|| by BHSP_2:def_3;
hence  ||.(a * seq).|| . n >= 0 by BHSP_1:28; ::_thesis: ||.(a * seq).|| . n <= ((abs a) (#) ||.seq.||) . n
||.(a * seq).|| . n = ||.((a * seq) . n).|| by BHSP_2:def_3
.= ||.(a * (seq . n)).|| by NORMSP_1:def_5
.= (abs a) * ||.(seq . n).|| by BHSP_1:27
.= (abs a) * (||.seq.|| . n) by BHSP_2:def_3
.= ((abs a) (#) ||.seq.||) . n by SEQ_1:9 ;
hence  ||.(a * seq).|| . n <= ((abs a) (#) ||.seq.||) . n ; ::_thesis: verum
end;
assume  seq is absolutely_summable ; ::_thesis: a * seq is absolutely_summable
then  ||.seq.|| is summable by Def6;
then  (abs a) (#) ||.seq.|| is summable by SERIES_1:10;
then  ||.(a * seq).|| is summable by A1, SERIES_1:20;
hence  a * seq is absolutely_summable by Def6; ::_thesis: verum
end;

theorem :: BHSP_4:27
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X st ( for n being Element of NAT holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable holds
seq is absolutely_summable
proof
let Rseq be Real_Sequence; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X st ( for n being Element of NAT holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable holds
seq is absolutely_summable
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X 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 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 BHSP_2:def_3;
hence  ||.seq.|| . n >= 0 by BHSP_1:28; ::_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 Def6; ::_thesis: verum
end;

theorem :: BHSP_4:28
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X 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 Rseq be Real_Sequence; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X 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 X be RealUnitarySpace; ::_thesis: for seq being sequence of X 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 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 BHSP_1:26;
 ||.(seq . n).|| >= 0 by BHSP_1:28;
hence  ||.seq.|| . n > 0 by A3, BHSP_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 BHSP_2:def_3 ;
hence  Rseq . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) by BHSP_2:def_3; ::_thesis: verum
end;
then  ||.seq.|| is summable by A2, SERIES_1:26;
hence  seq is absolutely_summable by Def6; ::_thesis: verum
end;

theorem Th29: :: BHSP_4:29
for r being Real
for X being RealUnitarySpace
for seq being sequence of X 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 r be Real; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X 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 X be RealUnitarySpace; ::_thesis: for seq being sequence of X 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: ( 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 )
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, BHSP_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;

theorem Th30: :: BHSP_4:30
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_1:26;
 ( ||.(seq . ((m + k) + 1)).|| / ||.(seq . (m + k)).|| >= 1 & ||.(seq . (m + k)).|| >= 0 ) by A2, BHSP_1:28, 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 A10: ||.(seq . m).|| <> 0 by BHSP_1:26;
 ||.(seq . m).|| >= 0 by BHSP_1:28;
then  ( not seq is convergent or lim seq <> H1(X) ) by A10, A3, Th29;
hence  not seq is summable by Th9; ::_thesis: verum
end;

theorem :: BHSP_4:31
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X 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 Rseq be Real_Sequence; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X 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 X be RealUnitarySpace; ::_thesis: for seq being sequence of X 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 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 :: BHSP_4:32
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X 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 Rseq be Real_Sequence; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X 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 X be RealUnitarySpace; ::_thesis: for seq being sequence of X 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 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 BHSP_2:def_3;
hence  ||.seq.|| . n >= 0 by BHSP_1:28; ::_thesis: Rseq . n = n -root (||.seq.|| . n)
 Rseq . n = n -root ||.(seq . n).|| by A1;
hence  Rseq . n = n -root (||.seq.|| . n) by BHSP_2:def_3; ::_thesis: verum
end;
then  ||.seq.|| is summable by A2, SERIES_1:28;
hence  seq is absolutely_summable by Def6; ::_thesis: verum
end;

theorem :: BHSP_4:33
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X 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 Rseq be Real_Sequence; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X 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 X be RealUnitarySpace; ::_thesis: for seq being sequence of X 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 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 BHSP_2:def_3 ;
then  ( ||.(seq . n).|| >= 0 & (n -root ||.(seq . n).||) |^ n >= 1 ) by A2, A5, BHSP_1:28, 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 :: BHSP_4:34
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X 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 Rseq be Real_Sequence; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X 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 X be RealUnitarySpace; ::_thesis: for seq being sequence of X 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 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 BHSP_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 BHSP_1:28, 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: :: BHSP_4:35
for X being RealUnitarySpace
for seq being sequence of X holds Partial_Sums ||.seq.|| is non-decreasing
proof
let X be RealUnitarySpace; ::_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 BHSP_1:28;
then  ||.seq.|| . (n + 1) >= 0 by BHSP_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 :: BHSP_4:36
for X being RealUnitarySpace
for seq being sequence of X
for n being Element of NAT holds (Partial_Sums ||.seq.||) . n >= 0
proof
let X be RealUnitarySpace; ::_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 BHSP_1:28;
then A1: ||.seq.|| . 0 >= 0 by BHSP_2:def_3;
 (Partial_Sums ||.seq.||) . 0 <= (Partial_Sums ||.seq.||) . n by Th35, SEQM_3:11;
hence  (Partial_Sums ||.seq.||) . n >= 0 by A1, SERIES_1:def_1; ::_thesis: verum
end;

theorem Th37: :: BHSP_4:37
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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] )
assume  S1[n] ; ::_thesis: S1[n + 1]
then A2: ||.((Partial_Sums seq) . n).|| + ||.(seq . (n + 1)).|| <= ((Partial_Sums ||.seq.||) . n) + ||.(seq . (n + 1)).|| by XREAL_1:6;
 (Partial_Sums seq) . (n + 1) = ((Partial_Sums seq) . n) + (seq . (n + 1)) by Def1;
then  ||.((Partial_Sums seq) . (n + 1)).|| <= ||.((Partial_Sums seq) . n).|| + ||.(seq . (n + 1)).|| by BHSP_1:30;
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 BHSP_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 BHSP_2:def_3 ;
then A3: S1[ 0 ] by Def1;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); ::_thesis: verum
end;

theorem :: BHSP_4:38
for X being RealUnitarySpace
for seq being sequence of X
for n being Element of NAT holds ||.(Sum (seq,n)).|| <= Sum (||.seq.||,n) by Th37;

theorem Th39: :: BHSP_4:39
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_1:28;
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 BHSP_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 Def1
.= ||.((((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 BHSP_1:30;
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 BHSP_1:31;
 (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 BHSP_1:26 ;
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: ||.(seq . ((n + k) + 1)).|| >= 0 by BHSP_1:28;
A13: 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 BHSP_2:def_3
.= abs (||.(seq . ((n + k) + 1)).|| + (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n))) ;
assume  S1[k] ; ::_thesis: S1[k + 1]
then A14: ||.(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;
 (Partial_Sums ||.seq.||) . (n + k) >= (Partial_Sums ||.seq.||) . n by A10, SEQM_3:5;
then A15: ((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n) >= 0 by XREAL_1:48;
||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| = ||.(((seq . ((n + k) + 1)) + ((Partial_Sums seq) . (n + k))) - ((Partial_Sums seq) . n)).|| by Def1
.= ||.((seq . ((n + k) + 1)) + (((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n))).|| by RLVECT_1:def_3 ;
then  ||.(((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_1:30;
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 A14, XXREAL_0:2;
then  ||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| <= ||.(seq . ((n + k) + 1)).|| + (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n)) by A15, ABSVALUE:def_1;
hence  S1[k + 1] by A15, A12, A13, 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 BHSP_1:26 ;
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 :: BHSP_4:40
for X being RealUnitarySpace
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))) by Th39;

theorem :: BHSP_4:41
for X being RealUnitarySpace
for seq being sequence of X
for n, m being Element of NAT holds ||.(Sum (seq,m,n)).|| <= abs (Sum (||.seq.||,m,n)) by Th39;

theorem :: BHSP_4:42
for X being RealHilbertSpace
for seq being sequence of X st seq is absolutely_summable holds
seq is summable
proof
let X be RealHilbertSpace; ::_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, Def6;
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 by XREAL_1:215;
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 RealUnitarySpace;
let seq be sequence of X;
let Rseq be Real_Sequence;
funcRseq * seq ->  sequence of X means :Def7: :: BHSP_4:def 7
 for n being Element of NAT holds it . n = (Rseq . n) * (seq . n);
existence
 ex b1 being sequence of X st
for n being Element of NAT holds b1 . n = (Rseq . n) * (seq . n)
proof
deffunc H2( Element of NAT ) ->  Element of the carrier of X = (Rseq . $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 = (Rseq . n) * (seq . n) ) & ( for n being Element of NAT holds b2 . n = (Rseq . n) * (seq . n) ) holds
b1 = b2
proof
let seq1, seq2 be sequence of X; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = (Rseq . n) * (seq . n) ) & ( for n being Element of NAT holds seq2 . n = (Rseq . n) * (seq . n) ) implies seq1 = seq2 )
assume that
A1: for n being Element of NAT holds seq1 . n = (Rseq . n) * (seq . n) and
A2: for n being Element of NAT holds seq2 . n = (Rseq . n) * (seq . n) ; ::_thesis: seq1 = seq2
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: K68(seq1,n) = K68(seq2,n)
 seq1 . n = (Rseq . n) * (seq . n) by A1;
hence  seq1 . n = seq2 . n by A2; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines * BHSP_4:def_7_:_
 for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence
for b4 being sequence of X holds
( b4 = Rseq * seq iff for n being Element of NAT holds b4 . n = (Rseq . n) * (seq . n) );

theorem :: BHSP_4:43
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds Rseq * (seq1 + seq2) = (Rseq * seq1) + (Rseq * seq2)
proof
let Rseq be Real_Sequence; ::_thesis: for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds Rseq * (seq1 + seq2) = (Rseq * seq1) + (Rseq * seq2)
let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X holds Rseq * (seq1 + seq2) = (Rseq * seq1) + (Rseq * seq2)
let seq1, seq2 be sequence of X; ::_thesis: Rseq * (seq1 + seq2) = (Rseq * seq1) + (Rseq * seq2)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: K68((Rseq * (seq1 + seq2)),n) = K68(((Rseq * seq1) + (Rseq * seq2)),n)
thus (Rseq * (seq1 + seq2)) . n = (Rseq . n) * ((seq1 + seq2) . n) by Def7
.= (Rseq . n) * ((seq1 . n) + (seq2 . n)) by NORMSP_1:def_2
.= ((Rseq . n) * (seq1 . n)) + ((Rseq . n) * (seq2 . n)) by RLVECT_1:def_5
.= ((Rseq * seq1) . n) + ((Rseq . n) * (seq2 . n)) by Def7
.= ((Rseq * seq1) . n) + ((Rseq * seq2) . n) by Def7
.= ((Rseq * seq1) + (Rseq * seq2)) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;

theorem :: BHSP_4:44
for Rseq1, Rseq2 being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X holds (Rseq1 + Rseq2) * seq = (Rseq1 * seq) + (Rseq2 * seq)
proof
let Rseq1, Rseq2 be Real_Sequence; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X holds (Rseq1 + Rseq2) * seq = (Rseq1 * seq) + (Rseq2 * seq)
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X holds (Rseq1 + Rseq2) * seq = (Rseq1 * seq) + (Rseq2 * seq)
let seq be sequence of X; ::_thesis: (Rseq1 + Rseq2) * seq = (Rseq1 * seq) + (Rseq2 * seq)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: K68(((Rseq1 + Rseq2) * seq),n) = K68(((Rseq1 * seq) + (Rseq2 * seq)),n)
thus ((Rseq1 + Rseq2) * seq) . n = ((Rseq1 + Rseq2) . n) * (seq . n) by Def7
.= ((Rseq1 . n) + (Rseq2 . n)) * (seq . n) by SEQ_1:7
.= ((Rseq1 . n) * (seq . n)) + ((Rseq2 . n) * (seq . n)) by RLVECT_1:def_6
.= ((Rseq1 * seq) . n) + ((Rseq2 . n) * (seq . n)) by Def7
.= ((Rseq1 * seq) . n) + ((Rseq2 * seq) . n) by Def7
.= ((Rseq1 * seq) + (Rseq2 * seq)) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;

theorem :: BHSP_4:45
for Rseq1, Rseq2 being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X holds (Rseq1 (#) Rseq2) * seq = Rseq1 * (Rseq2 * seq)
proof
let Rseq1, Rseq2 be Real_Sequence; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X holds (Rseq1 (#) Rseq2) * seq = Rseq1 * (Rseq2 * seq)
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X holds (Rseq1 (#) Rseq2) * seq = Rseq1 * (Rseq2 * seq)
let seq be sequence of X; ::_thesis: (Rseq1 (#) Rseq2) * seq = Rseq1 * (Rseq2 * seq)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: K68(((Rseq1 (#) Rseq2) * seq),n) = K68((Rseq1 * (Rseq2 * seq)),n)
thus ((Rseq1 (#) Rseq2) * seq) . n = ((Rseq1 (#) Rseq2) . n) * (seq . n) by Def7
.= ((Rseq1 . n) * (Rseq2 . n)) * (seq . n) by SEQ_1:8
.= (Rseq1 . n) * ((Rseq2 . n) * (seq . n)) by RLVECT_1:def_7
.= (Rseq1 . n) * ((Rseq2 * seq) . n) by Def7
.= (Rseq1 * (Rseq2 * seq)) . n by Def7 ; ::_thesis: verum
end;

theorem Th46: :: BHSP_4:46
for a being Real
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X holds (a (#) Rseq) * seq = a * (Rseq * seq)
proof
let a be Real; ::_thesis: for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X holds (a (#) Rseq) * seq = a * (Rseq * seq)
let Rseq be Real_Sequence; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X holds (a (#) Rseq) * seq = a * (Rseq * seq)
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X holds (a (#) Rseq) * seq = a * (Rseq * seq)
let seq be sequence of X; ::_thesis: (a (#) Rseq) * seq = a * (Rseq * seq)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: K68(((a (#) Rseq) * seq),n) = K68((a * (Rseq * seq)),n)
thus ((a (#) Rseq) * seq) . n = ((a (#) Rseq) . n) * (seq . n) by Def7
.= (a * (Rseq . n)) * (seq . n) by SEQ_1:9
.= a * ((Rseq . n) * (seq . n)) by RLVECT_1:def_7
.= a * ((Rseq * seq) . n) by Def7
.= (a * (Rseq * seq)) . n by NORMSP_1:def_5 ; ::_thesis: verum
end;

theorem :: BHSP_4:47
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X holds Rseq * (- seq) = (- Rseq) * seq
proof
let Rseq be Real_Sequence; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X holds Rseq * (- seq) = (- Rseq) * seq
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X holds Rseq * (- seq) = (- Rseq) * seq
let seq be sequence of X; ::_thesis: Rseq * (- seq) = (- Rseq) * seq
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: K68((Rseq * (- seq)),n) = K68(((- Rseq) * seq),n)
thus (Rseq * (- seq)) . n = (Rseq . n) * ((- seq) . n) by Def7
.= (Rseq . n) * (- (seq . n)) by BHSP_1:44
.= (- (Rseq . n)) * (seq . n) by RLVECT_1:24
.= ((- Rseq) . n) * (seq . n) by SEQ_1:10
.= ((- Rseq) * seq) . n by Def7 ; ::_thesis: verum
end;

theorem Th48: :: BHSP_4:48
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X st Rseq is convergent & seq is convergent holds
Rseq * seq is convergent
proof
let Rseq be Real_Sequence; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X st Rseq is convergent & seq is convergent holds
Rseq * seq is convergent
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X st Rseq is convergent & seq is convergent holds
Rseq * seq is convergent
let seq be sequence of X; ::_thesis: ( Rseq is convergent & seq is convergent implies Rseq * seq is convergent )
assume that
A1: Rseq is convergent and
A2: seq is convergent ; ::_thesis: Rseq * seq is convergent
consider p being real number  such that
A3: for r being real number st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
abs ((Rseq . n) - p) < r by A1, SEQ_2:def_6;
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, BHSP_2:9;
reconsider p = p as Real by XREAL_0:def_1;
now__::_thesis:_ex_h_being_Element_of_the_carrier_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_
||.(((Rseq_*_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
||.(((Rseq * 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
||.(((Rseq * seq) . n) - h).|| < r )
 Rseq is bounded by A1, SEQ_2:13;
then consider b being real number  such that
A5: b > 0 and
A6: for n being Element of NAT holds abs (Rseq . n) < b by SEQ_2:3;
reconsider b = b as Real by XREAL_0:def_1;
A7: b + ||.g.|| > 0 + 0 by A5, BHSP_1:28, 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
||.(((Rseq * seq) . n) - h).|| < r
then consider m1 being Element of NAT  such that
A9: for n being Element of NAT st n >= m1 holds
abs ((Rseq . n) - p) < r / (b + ||.g.||) by A3, A7, XREAL_1:139;
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, XREAL_1:139;
take m = m1 + m2; ::_thesis: for n being Element of NAT st n >= m holds
||.(((Rseq * seq) . n) - h).|| < r
let n be Element of NAT ; ::_thesis: ( n >= m implies ||.(((Rseq * seq) . n) - h).|| < r )
assume A11: n >= m ; ::_thesis: ||.(((Rseq * seq) . n) - h).|| < r
 m1 + m2 >= m1 by NAT_1:12;
then  n >= m1 by A11, XXREAL_0:2;
then  ( ||.g.|| >= 0 & abs ((Rseq . n) - p) <= r / (b + ||.g.||) ) by A9, BHSP_1:28;
then A12: ||.g.|| * (abs ((Rseq . n) - p)) <= ||.g.|| * (r / (b + ||.g.||)) by XREAL_1:64;
A13: ( abs (Rseq . n) >= 0 & ||.((seq . n) - g).|| >= 0 ) by BHSP_1:28, COMPLEX1:46;
 m >= m2 by NAT_1:12;
then  n >= m2 by A11, XXREAL_0:2;
then A14: ||.((seq . n) - g).|| < r / (b + ||.g.||) by A10;
 abs (Rseq . n) < b by A6;
then  (abs (Rseq . n)) * ||.((seq . n) - g).|| < b * (r / (b + ||.g.||)) by A14, A13, XREAL_1:96;
then  ((abs (Rseq . n)) * ||.((seq . n) - g).||) + (||.g.|| * (abs ((Rseq . n) - p))) < (b * (r / (b + ||.g.||))) + (||.g.|| * (r / (b + ||.g.||))) by A12, XREAL_1:8;
then  ((abs (Rseq . n)) * ||.((seq . n) - g).||) + (||.g.|| * (abs ((Rseq . n) - p))) < ((b * r) / (b + ||.g.||)) + (||.g.|| * (r / (b + ||.g.||))) by XCMPLX_1:74;
then  ((abs (Rseq . n)) * ||.((seq . n) - g).||) + (||.g.|| * (abs ((Rseq . n) - p))) < ((b * r) / (b + ||.g.||)) + ((||.g.|| * r) / (b + ||.g.||)) by XCMPLX_1:74;
then  ((abs (Rseq . n)) * ||.((seq . n) - g).||) + (||.g.|| * (abs ((Rseq . n) - p))) < ((b * r) + (||.g.|| * r)) / (b + ||.g.||) by XCMPLX_1:62;
then  ((abs (Rseq . n)) * ||.((seq . n) - g).||) + (||.g.|| * (abs ((Rseq . n) - p))) < ((b + ||.g.||) * r) / (b + ||.g.||) ;
then A15: ((abs (Rseq . n)) * ||.((seq . n) - g).||) + (||.g.|| * (abs ((Rseq . n) - p))) < r by A7, XCMPLX_1:89;
||.(((Rseq * seq) . n) - (p * g)).|| = ||.(((Rseq . n) * (seq . n)) - (p * g)).|| by Def7
.= ||.((((Rseq . n) * (seq . n)) - (p * g)) + H1(X)).|| by RLVECT_1:4
.= ||.((((Rseq . n) * (seq . n)) - (p * g)) + (((Rseq . n) * g) - ((Rseq . n) * g))).|| by RLVECT_1:15
.= ||.(((Rseq . n) * (seq . n)) - ((p * g) - (((Rseq . n) * g) - ((Rseq . n) * g)))).|| by RLVECT_1:29
.= ||.(((Rseq . n) * (seq . n)) - (((Rseq . n) * g) + ((p * g) - ((Rseq . n) * g)))).|| by RLVECT_1:29
.= ||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * g)) - ((p * g) - ((Rseq . n) * g))).|| by RLVECT_1:27
.= ||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * g)) + (((Rseq . n) * g) - (p * g))).|| by RLVECT_1:33 ;
then  ||.(((Rseq * seq) . n) - (p * g)).|| <= ||.(((Rseq . n) * (seq . n)) - ((Rseq . n) * g)).|| + ||.(((Rseq . n) * g) - (p * g)).|| by BHSP_1:30;
then  ||.(((Rseq * seq) . n) - (p * g)).|| <= ||.((Rseq . n) * ((seq . n) - g)).|| + ||.(((Rseq . n) * g) - (p * g)).|| by RLVECT_1:34;
then  ||.(((Rseq * seq) . n) - (p * g)).|| <= ||.((Rseq . n) * ((seq . n) - g)).|| + ||.(((Rseq . n) - p) * g).|| by RLVECT_1:35;
then  ||.(((Rseq * seq) . n) - (p * g)).|| <= ((abs (Rseq . n)) * ||.((seq . n) - g).||) + ||.(((Rseq . n) - p) * g).|| by BHSP_1:27;
then  ||.(((Rseq * seq) . n) - (p * g)).|| <= ((abs (Rseq . n)) * ||.((seq . n) - g).||) + (||.g.|| * (abs ((Rseq . n) - p))) by BHSP_1:27;
hence  ||.(((Rseq * seq) . n) - h).|| < r by A15, XXREAL_0:2; ::_thesis: verum
end;
hence  Rseq * seq is convergent by BHSP_2:9; ::_thesis: verum
end;

theorem :: BHSP_4:49
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X st Rseq is bounded & seq is bounded holds
Rseq * seq is bounded
proof
let Rseq be Real_Sequence; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X st Rseq is bounded & seq is bounded holds
Rseq * seq is bounded
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X st Rseq is bounded & seq is bounded holds
Rseq * seq is bounded
let seq be sequence of X; ::_thesis: ( Rseq is bounded & seq is bounded implies Rseq * seq is bounded )
assume that
A1: Rseq is bounded and
A2: seq is bounded ; ::_thesis: Rseq * seq is bounded
consider M1 being real number  such that
A3: M1 > 0 and
A4: for n being Element of NAT holds abs (Rseq . n) < M1 by A1, SEQ_2:3;
consider M2 being Real such that
A5: M2 > 0 and
A6: for n being Element of NAT holds ||.(seq . n).|| <= M2 by A2, BHSP_3:def_3;
now__::_thesis:_ex_M_being_Real_st_
(_M_>_0_&_(_for_n_being_Element_of_NAT_holds_||.((Rseq_*_seq)_._n).||_<=_M_)_)
reconsider M = M1 * M2 as Real ;
take M = M; ::_thesis: ( M > 0 & ( for n being Element of NAT holds ||.((Rseq * seq) . n).|| <= M ) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((Rseq_*_seq)_._n).||_<=_M
let n be Element of NAT ; ::_thesis: ||.((Rseq * seq) . n).|| <= M
 abs (Rseq . n) >= 0 by COMPLEX1:46;
then A7: (abs (Rseq . n)) * ||.(seq . n).|| <= (abs (Rseq . n)) * M2 by A6, XREAL_1:64;
 abs (Rseq . n) <= M1 by A4;
then A8: (abs (Rseq . n)) * M2 <= M1 * M2 by A5, XREAL_1:64;
||.((Rseq * seq) . n).|| = ||.((Rseq . n) * (seq . n)).|| by Def7
.= (abs (Rseq . n)) * ||.(seq . n).|| by BHSP_1:27 ;
hence  ||.((Rseq * seq) . n).|| <= M by A7, A8, XXREAL_0:2; ::_thesis: verum
end;
hence  ( M > 0 & ( for n being Element of NAT holds ||.((Rseq * seq) . n).|| <= M ) ) by A3, A5, XREAL_1:129; ::_thesis: verum
end;
hence  Rseq * seq is bounded by BHSP_3:def_3; ::_thesis: verum
end;

theorem :: BHSP_4:50
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X st Rseq is convergent & seq is convergent holds
( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) )
proof
let Rseq be Real_Sequence; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X st Rseq is convergent & seq is convergent holds
( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) )
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X st Rseq is convergent & seq is convergent holds
( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) )
let seq be sequence of X; ::_thesis: ( Rseq is convergent & seq is convergent implies ( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) ) )
assume that
A1: Rseq is convergent and
A2: seq is convergent ; ::_thesis: ( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) )
 Rseq is bounded by A1, SEQ_2:13;
then consider b being real number  such that
A3: b > 0 and
A4: for n being Element of NAT holds abs (Rseq . n) < b by SEQ_2:3;
reconsider b = b as Real by XREAL_0:def_1;
A5: b + ||.(lim seq).|| > 0 + 0 by A3, BHSP_1:28, XREAL_1:8;
A6: ||.(lim seq).|| >= 0 by BHSP_1:28;
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_(((Rseq_*_seq)_._n),((lim_Rseq)_*_(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 (((Rseq * seq) . n),((lim Rseq) * (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 (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < r
then A8: r / (b + ||.(lim seq).||) > 0 by A5, XREAL_1:139;
then consider m1 being Element of NAT  such that
A9: for n being Element of NAT st n >= m1 holds
abs ((Rseq . n) - (lim Rseq)) < r / (b + ||.(lim seq).||) by A1, SEQ_2:def_7;
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, BHSP_2:def_2;
take m = m1 + m2; ::_thesis: for n being Element of NAT st n >= m holds
dist (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < r )
assume A11: n >= m ; ::_thesis: dist (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < r
 m1 + m2 >= m1 by NAT_1:12;
then  n >= m1 by A11, XXREAL_0:2;
then  abs ((Rseq . n) - (lim Rseq)) <= r / (b + ||.(lim seq).||) by A9;
then A12: ||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq))) <= ||.(lim seq).|| * (r / (b + ||.(lim seq).||)) by A6, XREAL_1:64;
A13: ||.((seq . n) - (lim seq)).|| >= 0 by BHSP_1:28;
 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 BHSP_1:def_5;
 ( abs (Rseq . n) < b & abs (Rseq . n) >= 0 ) by A4, COMPLEX1:46;
then  (abs (Rseq . n)) * ||.((seq . n) - (lim seq)).|| < b * (r / (b + ||.(lim seq).||)) by A14, A13, XREAL_1:96;
then  ((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq)))) < (b * (r / (b + ||.(lim seq).||))) + (||.(lim seq).|| * (r / (b + ||.(lim seq).||))) by A12, XREAL_1:8;
then  ((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq)))) < ((b * r) / (b + ||.(lim seq).||)) + (||.(lim seq).|| * (r / (b + ||.(lim seq).||))) by XCMPLX_1:74;
then  ((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq)))) < ((b * r) / (b + ||.(lim seq).||)) + ((||.(lim seq).|| * r) / (b + ||.(lim seq).||)) by XCMPLX_1:74;
then  ((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq)))) < ((b * r) + (||.(lim seq).|| * r)) / (b + ||.(lim seq).||) by XCMPLX_1:62;
then  ((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq)))) < ((b + ||.(lim seq).||) * r) / (b + ||.(lim seq).||) ;
then A15: ((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq)))) < r by A5, XCMPLX_1:89;
||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| = ||.(((Rseq . n) * (seq . n)) - ((lim Rseq) * (lim seq))).|| by Def7
.= ||.((((Rseq . n) * (seq . n)) - ((lim Rseq) * (lim seq))) + H1(X)).|| by RLVECT_1:4
.= ||.((((Rseq . n) * (seq . n)) - ((lim Rseq) * (lim seq))) + (((Rseq . n) * (lim seq)) - ((Rseq . n) * (lim seq)))).|| by RLVECT_1:15
.= ||.(((Rseq . n) * (seq . n)) - (((lim Rseq) * (lim seq)) - (((Rseq . n) * (lim seq)) - ((Rseq . n) * (lim seq))))).|| by RLVECT_1:29
.= ||.(((Rseq . n) * (seq . n)) - (((Rseq . n) * (lim seq)) + (((lim Rseq) * (lim seq)) - ((Rseq . n) * (lim seq))))).|| by RLVECT_1:29
.= ||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq))) - (((lim Rseq) * (lim seq)) - ((Rseq . n) * (lim seq)))).|| by RLVECT_1:27
.= ||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq))) + (((Rseq . n) * (lim seq)) - ((lim Rseq) * (lim seq)))).|| by RLVECT_1:33 ;
then  ||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| <= ||.(((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq))).|| + ||.(((Rseq . n) * (lim seq)) - ((lim Rseq) * (lim seq))).|| by BHSP_1:30;
then  ||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| <= ||.((Rseq . n) * ((seq . n) - (lim seq))).|| + ||.(((Rseq . n) * (lim seq)) - ((lim Rseq) * (lim seq))).|| by RLVECT_1:34;
then  ||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| <= ||.((Rseq . n) * ((seq . n) - (lim seq))).|| + ||.(((Rseq . n) - (lim Rseq)) * (lim seq)).|| by RLVECT_1:35;
then  ||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| <= ((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + ||.(((Rseq . n) - (lim Rseq)) * (lim seq)).|| by BHSP_1:27;
then  ||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| <= ((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq)))) by BHSP_1:27;
then  ||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| < r by A15, XXREAL_0:2;
hence  dist (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < r by BHSP_1:def_5; ::_thesis: verum
end;
 Rseq * seq is convergent by A1, A2, Th48;
hence  ( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) ) by A7, BHSP_2:def_2; ::_thesis: verum
end;

definition
let Rseq be Real_Sequence;
attrRseq is Cauchy  means :Def8: :: BHSP_4:def 8
 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
abs ((Rseq . n) - (Rseq . m)) < r;
end;

:: deftheorem Def8 defines Cauchy BHSP_4:def_8_:_
 for Rseq being Real_Sequence holds
( Rseq 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
abs ((Rseq . n) - (Rseq . m)) < r );

theorem :: BHSP_4:51
for Rseq being Real_Sequence
for X being RealHilbertSpace
for seq being sequence of X st seq is Cauchy & Rseq is Cauchy holds
Rseq * seq is Cauchy
proof
let Rseq be Real_Sequence; ::_thesis: for X being RealHilbertSpace
for seq being sequence of X st seq is Cauchy & Rseq is Cauchy holds
Rseq * seq is Cauchy
let X be RealHilbertSpace; ::_thesis: for seq being sequence of X st seq is Cauchy & Rseq is Cauchy holds
Rseq * seq is Cauchy
let seq be sequence of X; ::_thesis: ( seq is Cauchy & Rseq is Cauchy implies Rseq * seq is Cauchy )
assume that
A1: seq is Cauchy and
A2: Rseq is Cauchy ; ::_thesis: Rseq * seq is Cauchy
now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
abs_((Rseq_._n)_-_(Rseq_._k))_<_r
let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs ((Rseq . n) - (Rseq . k)) < r )
assume A3: r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs ((Rseq . n) - (Rseq . k)) < r
 r is Real by XREAL_0:def_1;
then consider k being Element of NAT  such that
A4: for n, m being Element of NAT st n >= k & m >= k holds
abs ((Rseq . n) - (Rseq . m)) < r by A2, A3, Def8;
take k = k; ::_thesis: for n being Element of NAT st n >= k holds
abs ((Rseq . n) - (Rseq . k)) < r
thus  for n being Element of NAT st n >= k holds
abs ((Rseq . n) - (Rseq . k)) < r by A4; ::_thesis: verum
end;
then A5: Rseq is convergent by SEQ_4:41;
 seq is convergent by A1, BHSP_3:def_4;
hence  Rseq * seq is Cauchy by A5, Th48, BHSP_3:9; ::_thesis: verum
end;

theorem Th52: :: BHSP_4:52
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X
for n being Element of NAT holds (Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Rseq * seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))
proof
let Rseq be Real_Sequence; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X
for n being Element of NAT holds (Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Rseq * seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X
for n being Element of NAT holds (Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Rseq * seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))
let seq be sequence of X; ::_thesis: for n being Element of NAT holds (Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Rseq * seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))
defpred S1[ Element of NAT ] means (Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . $1 = ((Partial_Sums (Rseq * seq)) . ($1 + 1)) - ((Rseq * (Partial_Sums seq)) . ($1 + 1));
A1: (Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . 0 = ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq)) . 0 by Def1
.= ((Rseq - (Rseq ^\ 1)) . 0) * ((Partial_Sums seq) . 0) by Def7
.= ((Rseq + (- (Rseq ^\ 1))) . 0) * (seq . 0) by Def1
.= ((Rseq . 0) + ((- (Rseq ^\ 1)) . 0)) * (seq . 0) by SEQ_1:7
.= ((Rseq . 0) + (- ((Rseq ^\ 1) . 0))) * (seq . 0) by SEQ_1:10
.= ((Rseq . 0) - ((Rseq ^\ 1) . 0)) * (seq . 0)
.= ((Rseq . 0) - (Rseq . (0 + 1))) * (seq . 0) by NAT_1:def_3
.= ((Rseq . 0) * (seq . 0)) - ((Rseq . 1) * (seq . 0)) by RLVECT_1:35 ;
A2: (Rseq * (Partial_Sums seq)) . (0 + 1) = (Rseq . (0 + 1)) * ((Partial_Sums seq) . (0 + 1)) by Def7
.= (Rseq . (0 + 1)) * (((Partial_Sums seq) . 0) + (seq . (0 + 1))) by Def1
.= (Rseq . 1) * ((seq . 0) + (seq . 1)) by Def1
.= ((Rseq . 1) * (seq . 0)) + ((Rseq . 1) * (seq . 1)) by RLVECT_1:def_5 ;
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 ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Rseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Rseq * seq)) . (n + 1)) - (((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))) by RLVECT_1:29;
then A4: ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Rseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Rseq * seq)) . (n + 1)) - H1(X) by RLVECT_1:15;
(Partial_Sums (Rseq * seq)) . ((n + 1) + 1) = ((Partial_Sums (Rseq * seq)) . (n + 1)) + ((Rseq * seq) . ((n + 1) + 1)) by Def1
.= (((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Rseq * (Partial_Sums seq)) . (n + 1))) + ((Rseq * seq) . ((n + 1) + 1)) by A4, RLVECT_1:13
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Rseq * (Partial_Sums seq)) . (n + 1)) + ((Rseq * seq) . ((n + 1) + 1))) by RLVECT_1:def_3
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Rseq . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Rseq * seq) . ((n + 1) + 1))) by Def7
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Rseq . (n + 1)) - (Rseq . ((n + 1) + 1))) + (Rseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by Def7
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Rseq . (n + 1)) - (Rseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by RLVECT_1:def_6
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Rseq . (n + 1)) - ((Rseq ^\ 1) . (n + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by NAT_1:def_3
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Rseq . (n + 1)) + (- ((Rseq ^\ 1) . (n + 1)))) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Rseq . (n + 1)) + ((- (Rseq ^\ 1)) . (n + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by SEQ_1:10
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Rseq - (Rseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by SEQ_1:7
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + ((((Rseq - (Rseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + (((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by RLVECT_1:def_3
.= (((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Rseq - (Rseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1)))) + (((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by RLVECT_1:def_3
.= (((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq)) . (n + 1))) + (((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by Def7
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + (((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by Def1
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + ((Rseq . ((n + 1) + 1)) * (((Partial_Sums seq) . (n + 1)) + (seq . ((n + 1) + 1)))) by RLVECT_1:def_5
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + ((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . ((n + 1) + 1))) by Def1
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + ((Rseq * (Partial_Sums seq)) . ((n + 1) + 1)) by Def7 ;
then  ((Partial_Sums (Rseq * seq)) . ((n + 1) + 1)) - ((Rseq * (Partial_Sums seq)) . ((n + 1) + 1)) = ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + (((Rseq * (Partial_Sums seq)) . ((n + 1) + 1)) - ((Rseq * (Partial_Sums seq)) . ((n + 1) + 1))) by RLVECT_1:def_3;
then  ((Partial_Sums (Rseq * seq)) . ((n + 1) + 1)) - ((Rseq * (Partial_Sums seq)) . ((n + 1) + 1)) = ((Partial_Sums ((Rseq - (Rseq ^\ 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 (Rseq * seq)) . (0 + 1) = ((Partial_Sums (Rseq * seq)) . 0) + ((Rseq * seq) . (0 + 1)) by Def1
.= ((Rseq * seq) . 0) + ((Rseq * seq) . 1) by Def1
.= ((Rseq . 0) * (seq . 0)) + ((Rseq * seq) . 1) by Def7
.= ((Rseq . 0) * (seq . 0)) + ((Rseq . 1) * (seq . 1)) by Def7 ;
then (Partial_Sums (Rseq * seq)) . (0 + 1) = (((Rseq . 0) * (seq . 0)) + H1(X)) + ((Rseq . 1) * (seq . 1)) by RLVECT_1:4
.= (((Rseq . 0) * (seq . 0)) + (((Rseq . 1) * (seq . 0)) - ((Rseq . 1) * (seq . 0)))) + ((Rseq . 1) * (seq . 1)) by RLVECT_1:15
.= ((((Rseq . 0) * (seq . 0)) + (- ((Rseq . 1) * (seq . 0)))) + ((Rseq . 1) * (seq . 0))) + ((Rseq . 1) * (seq . 1)) by RLVECT_1:def_3
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . 0) + ((Rseq * (Partial_Sums seq)) . (0 + 1)) by A1, A2, RLVECT_1:def_3 ;
then  ((Partial_Sums (Rseq * seq)) . (0 + 1)) - ((Rseq * (Partial_Sums seq)) . (0 + 1)) = ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . 0) + (((Rseq * (Partial_Sums seq)) . (0 + 1)) - ((Rseq * (Partial_Sums seq)) . (0 + 1))) by RLVECT_1:def_3;
then  ((Partial_Sums (Rseq * seq)) . (0 + 1)) - ((Rseq * (Partial_Sums seq)) . (0 + 1)) = ((Partial_Sums ((Rseq - (Rseq ^\ 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: :: BHSP_4:53
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X
for n being Element of NAT holds (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq))) . n)
proof
let Rseq be Real_Sequence; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X
for n being Element of NAT holds (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq))) . n)
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X
for n being Element of NAT holds (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq))) . n)
let seq be sequence of X; ::_thesis: for n being Element of NAT holds (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq))) . n)
let n be Element of NAT ; ::_thesis: (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq))) . n)
 ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Rseq * (Partial_Sums seq)) . (n + 1)) = (((Partial_Sums (Rseq * seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))) + ((Rseq * (Partial_Sums seq)) . (n + 1)) by Th52;
then  ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Rseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Rseq * seq)) . (n + 1)) - (((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))) by RLVECT_1:29;
then  ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Rseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Rseq * seq)) . (n + 1)) - H1(X) by RLVECT_1:15;
then  (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums ((((- 1) (#) (Rseq ^\ 1)) - (- Rseq)) * (Partial_Sums seq))) . n) by RLVECT_1:13;
then  (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums (((- 1) (#) ((Rseq ^\ 1) - Rseq)) * (Partial_Sums seq))) . n) by SEQ_1:24;
then  (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums ((- 1) * (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq)))) . n) by Th46;
then  (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) + (((- 1) * (Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq)))) . n) by Th3;
then  (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) + ((- 1) * ((Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq))) . n)) by NORMSP_1:def_5;
hence  (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq))) . n) by RLVECT_1:16; ::_thesis: verum
end;

theorem :: BHSP_4:54
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X
for n being Element of NAT holds Sum ((Rseq * seq),(n + 1)) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - (Sum ((((Rseq ^\ 1) - Rseq) * (Partial_Sums seq)),n)) by Th53;