:: by El\.zbieta Kraszewska and Jan Popio{\l}ek

::

:: Received April 1, 1992

:: Copyright (c) 1992-2018 Association of Mizar Users

deffunc H

definition

let X be non empty addLoopStr ;

let seq be sequence of X;

ex b_{1} being sequence of X st

( b_{1} . 0 = seq . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) + (seq . (n + 1)) ) )

for b_{1}, b_{2} being sequence of X st b_{1} . 0 = seq . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) + (seq . (n + 1)) ) & b_{2} . 0 = seq . 0 & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) + (seq . (n + 1)) ) holds

b_{1} = b_{2}

end;
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 Nat holds it . (n + 1) = (it . n) + (seq . (n + 1)) ) );

existence ( it . 0 = seq . 0 & ( for n being Nat holds it . (n + 1) = (it . n) + (seq . (n + 1)) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines Partial_Sums BHSP_4:def 1 :

for X being non empty addLoopStr

for seq, b_{3} being sequence of X holds

( b_{3} = Partial_Sums seq iff ( b_{3} . 0 = seq . 0 & ( for n being Nat holds b_{3} . (n + 1) = (b_{3} . n) + (seq . (n + 1)) ) ) );

for X being non empty addLoopStr

for seq, b

( b

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)

for seq1, seq2 being sequence of X holds (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2)

proof 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)

for seq1, seq2 being sequence of X holds (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2)

proof 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)

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 end;

theorem :: BHSP_4:4

for X being RealUnitarySpace

for seq being sequence of X holds Partial_Sums (- seq) = - (Partial_Sums seq)

for seq being sequence of X holds Partial_Sums (- seq) = - (Partial_Sums seq)

proof 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))

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 end;

definition

let X be RealUnitarySpace;

let seq be sequence of X;

coherence

lim (Partial_Sums seq) is Point of X ;

end;
let seq be sequence of X;

coherence

lim (Partial_Sums seq) is Point of X ;

:: 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 );

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);

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) )

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 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) )

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 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) )

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 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 )

for seq being sequence of X st seq is summable holds

( seq is convergent & lim seq = 0. X )

proof 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 Nat st

for n, m being Nat st n >= k & m >= k holds

||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) by BHSP_3:2, BHSP_3:def 4;

for seq being sequence of X holds

( seq is summable iff for r being Real st r > 0 holds

ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) by BHSP_3:2, BHSP_3:def 4;

theorem :: BHSP_4:11

for X being RealUnitarySpace

for seq being sequence of X st seq is summable holds

Partial_Sums seq is bounded ;

for seq being sequence of X st seq is summable holds

Partial_Sums seq is bounded ;

theorem Th12: :: BHSP_4:12

for X being RealUnitarySpace

for seq, seq1 being sequence of X st ( for n being Nat holds seq1 . n = seq . 0 ) holds

Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1

for seq, seq1 being sequence of X st ( for n being Nat holds seq1 . n = seq . 0 ) holds

Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1

proof end;

theorem Th13: :: BHSP_4:13

for X being RealUnitarySpace

for seq being sequence of X st seq is summable holds

for k being Nat holds seq ^\ k is summable

for seq being sequence of X st seq is summable holds

for k being Nat holds seq ^\ k is summable

proof end;

theorem :: BHSP_4:14

for X being RealUnitarySpace

for seq being sequence of X st ex k being Nat st seq ^\ k is summable holds

seq is summable

for seq being sequence of X st ex k being Nat st seq ^\ k is summable holds

seq is summable

proof end;

definition

let X be RealUnitarySpace;

let seq be sequence of X;

let n be Nat;

coherence

(Partial_Sums seq) . n is Point of X ;

end;
let seq be sequence of X;

let n be Nat;

coherence

(Partial_Sums seq) . n is Point of X ;

:: deftheorem defines Sum BHSP_4:def 4 :

for X being RealUnitarySpace

for seq being sequence of X

for n being Nat holds Sum (seq,n) = (Partial_Sums seq) . n;

for X being RealUnitarySpace

for seq being sequence of X

for n being Nat holds Sum (seq,n) = (Partial_Sums seq) . n;

theorem :: BHSP_4:15

theorem Th16: :: BHSP_4:16

for X being RealUnitarySpace

for seq being sequence of X holds Sum (seq,1) = (Sum (seq,0)) + (seq . 1)

for seq being sequence of X holds Sum (seq,1) = (Sum (seq,0)) + (seq . 1)

proof end;

theorem :: BHSP_4:18

theorem Th19: :: BHSP_4:19

for n being Nat

for X being RealUnitarySpace

for seq being sequence of X holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))

for X being RealUnitarySpace

for seq being sequence of X holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))

proof end;

theorem :: BHSP_4:20

for X being RealUnitarySpace

for seq being sequence of X holds seq . 1 = (Sum (seq,1)) - (Sum (seq,0))

for seq being sequence of X holds seq . 1 = (Sum (seq,1)) - (Sum (seq,0))

proof end;

definition

let X be RealUnitarySpace;

let seq be sequence of X;

let n, m be Nat;

coherence

(Sum (seq,n)) - (Sum (seq,m)) is Point of X ;

end;
let seq be sequence of X;

let n, m be Nat;

coherence

(Sum (seq,n)) - (Sum (seq,m)) is Point of X ;

:: deftheorem defines Sum BHSP_4:def 5 :

for X being RealUnitarySpace

for seq being sequence of X

for n, m being Nat holds Sum (seq,n,m) = (Sum (seq,n)) - (Sum (seq,m));

for X being RealUnitarySpace

for seq being sequence of X

for n, m being Nat holds Sum (seq,n,m) = (Sum (seq,n)) - (Sum (seq,m));

theorem :: BHSP_4:22

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 Nat st

for n, m being Nat st n >= k & m >= k holds

||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )

for seq being sequence of X holds

( seq is summable iff for r being Real st r > 0 holds

ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )

proof 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 Nat st

for n, m being Nat st n >= k & m >= k holds

||.(Sum (seq,n,m)).|| < r )

for seq being sequence of X holds

( seq is summable iff for r being Real st r > 0 holds

ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.(Sum (seq,n,m)).|| < r )

proof end;

:: deftheorem 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 );

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

for seq1, seq2 being sequence of X st seq1 is absolutely_summable & seq2 is absolutely_summable holds

seq1 + seq2 is absolutely_summable

proof 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

for X being RealUnitarySpace

for seq being sequence of X st seq is absolutely_summable holds

a * seq is absolutely_summable

proof end;

theorem :: BHSP_4:27

for Rseq being Real_Sequence

for X being RealUnitarySpace

for seq being sequence of X st ( for n being Nat holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable holds

seq is absolutely_summable

for X being RealUnitarySpace

for seq being sequence of X st ( for n being Nat holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable holds

seq is absolutely_summable

proof end;

theorem :: BHSP_4:28

for Rseq being Real_Sequence

for X being RealUnitarySpace

for seq being sequence of X st ( for n being Nat holds

( seq . n <> 0. X & Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) ) & Rseq is convergent & lim Rseq < 1 holds

seq is absolutely_summable

for X being RealUnitarySpace

for seq being sequence of X st ( for n being 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 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 Nat st

for n being Nat st n >= m holds

||.(seq . n).|| >= r & seq is convergent holds

lim seq <> 0. X

for X being RealUnitarySpace

for seq being sequence of X st r > 0 & ex m being Nat st

for n being Nat st n >= m holds

||.(seq . n).|| >= r & seq is convergent holds

lim seq <> 0. X

proof end;

theorem Th30: :: BHSP_4:30

for X being RealUnitarySpace

for seq being sequence of X st ( for n being Nat holds seq . n <> 0. X ) & ex m being Nat st

for n being Nat st n >= m holds

||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 holds

not seq is summable

for seq being sequence of X st ( for n being Nat holds seq . n <> 0. X ) & ex m being Nat st

for n being Nat st n >= m holds

||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 holds

not seq is summable

proof end;

theorem :: BHSP_4:31

for Rseq being Real_Sequence

for X being RealUnitarySpace

for seq being sequence of X st ( for n being Nat holds seq . n <> 0. X ) & ( for n being Nat holds Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) & Rseq is convergent & lim Rseq > 1 holds

not seq is summable

for X being RealUnitarySpace

for seq being sequence of X st ( for n being Nat holds seq . n <> 0. X ) & ( for n being Nat holds Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) & Rseq is convergent & lim Rseq > 1 holds

not seq is summable

proof end;

theorem :: BHSP_4:32

for Rseq being Real_Sequence

for X being RealUnitarySpace

for seq being sequence of X st ( for n being Nat holds Rseq . n = n -root ||.(seq . n).|| ) & Rseq is convergent & lim Rseq < 1 holds

seq is absolutely_summable

for X being RealUnitarySpace

for seq being sequence of X st ( for n being Nat holds Rseq . n = n -root ||.(seq . n).|| ) & Rseq is convergent & lim Rseq < 1 holds

seq is absolutely_summable

proof end;

theorem :: BHSP_4:33

for Rseq being Real_Sequence

for X being RealUnitarySpace

for seq being sequence of X st ( for n being Nat holds Rseq . n = n -root (||.seq.|| . n) ) & ex m being Nat st

for n being Nat st n >= m holds

Rseq . n >= 1 holds

not seq is summable

for X being RealUnitarySpace

for seq being sequence of X st ( for n being Nat holds Rseq . n = n -root (||.seq.|| . n) ) & ex m being Nat st

for n being Nat st n >= m holds

Rseq . n >= 1 holds

not seq is summable

proof end;

theorem :: BHSP_4:34

for Rseq being Real_Sequence

for X being RealUnitarySpace

for seq being sequence of X st ( for n being Nat holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 holds

not seq is summable

for X being RealUnitarySpace

for seq being sequence of X st ( for n being Nat holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 holds

not seq is summable

proof end;

theorem Th35: :: BHSP_4:35

for X being RealUnitarySpace

for seq being sequence of X holds Partial_Sums ||.seq.|| is non-decreasing

for seq being sequence of X holds Partial_Sums ||.seq.|| is non-decreasing

proof end;

theorem :: BHSP_4:36

for X being RealUnitarySpace

for seq being sequence of X

for n being Nat holds (Partial_Sums ||.seq.||) . n >= 0

for seq being sequence of X

for n being Nat holds (Partial_Sums ||.seq.||) . n >= 0

proof end;

theorem Th37: :: BHSP_4:37

for X being RealUnitarySpace

for seq being sequence of X

for n being Nat holds ||.((Partial_Sums seq) . n).|| <= (Partial_Sums ||.seq.||) . n

for seq being sequence of X

for n being Nat holds ||.((Partial_Sums seq) . n).|| <= (Partial_Sums ||.seq.||) . n

proof end;

theorem :: BHSP_4:38

theorem Th39: :: BHSP_4:39

for X being RealUnitarySpace

for seq being sequence of X

for n, m being Nat holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)).|

for seq being sequence of X

for n, m being Nat holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)).|

proof end;

theorem :: BHSP_4:40

theorem :: BHSP_4:41

theorem :: BHSP_4:42

for X being RealHilbertSpace

for seq being sequence of X st seq is absolutely_summable holds

seq is summable

for seq being sequence of X st seq is absolutely_summable holds

seq is summable

proof end;

definition

let X be RealUnitarySpace;

let seq be sequence of X;

let Rseq be Real_Sequence;

ex b_{1} being sequence of X st

for n being Nat holds b_{1} . n = (Rseq . n) * (seq . n)

for b_{1}, b_{2} being sequence of X st ( for n being Nat holds b_{1} . n = (Rseq . n) * (seq . n) ) & ( for n being Nat holds b_{2} . n = (Rseq . n) * (seq . n) ) holds

b_{1} = b_{2}

end;
let seq be sequence of X;

let Rseq be Real_Sequence;

func Rseq * seq -> sequence of X means :Def7: :: BHSP_4:def 7

for n being Nat holds it . n = (Rseq . n) * (seq . n);

existence for n being Nat holds it . n = (Rseq . n) * (seq . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines * BHSP_4:def 7 :

for X being RealUnitarySpace

for seq being sequence of X

for Rseq being Real_Sequence

for b_{4} being sequence of X holds

( b_{4} = Rseq * seq iff for n being Nat holds b_{4} . n = (Rseq . n) * (seq . n) );

for X being RealUnitarySpace

for seq being sequence of X

for Rseq being Real_Sequence

for b

( b

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)

for X being RealUnitarySpace

for seq1, seq2 being sequence of X holds Rseq * (seq1 + seq2) = (Rseq * seq1) + (Rseq * seq2)

proof 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)

for X being RealUnitarySpace

for seq being sequence of X holds (Rseq1 + Rseq2) * seq = (Rseq1 * seq) + (Rseq2 * seq)

proof 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)

for X being RealUnitarySpace

for seq being sequence of X holds (Rseq1 (#) Rseq2) * seq = Rseq1 * (Rseq2 * seq)

proof 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)

for Rseq being Real_Sequence

for X being RealUnitarySpace

for seq being sequence of X holds (a (#) Rseq) * seq = a * (Rseq * seq)

proof 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

for X being RealUnitarySpace

for seq being sequence of X holds Rseq * (- seq) = (- Rseq) * seq

proof 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

for X being RealUnitarySpace

for seq being sequence of X st Rseq is convergent & seq is convergent holds

Rseq * seq is convergent

proof 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

for X being RealUnitarySpace

for seq being sequence of X st Rseq is bounded & seq is bounded holds

Rseq * seq is bounded

proof 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) )

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 end;

:: deftheorem 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 Nat st

for n, m being Nat st n >= k & m >= k holds

|.((Rseq . n) - (Rseq . m)).| < r );

for Rseq being Real_Sequence holds

( Rseq is Cauchy iff for r being Real st r > 0 holds

ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

|.((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

for X being RealHilbertSpace

for seq being sequence of X st seq is Cauchy & Rseq is Cauchy holds

Rseq * seq is Cauchy

proof end;

theorem Th52: :: BHSP_4:52

for Rseq being Real_Sequence

for X being RealUnitarySpace

for seq being sequence of X

for n being Nat holds (Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Rseq * seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))

for X being RealUnitarySpace

for seq being sequence of X

for n being Nat holds (Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Rseq * seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))

proof end;

theorem Th53: :: BHSP_4:53

for Rseq being Real_Sequence

for X being RealUnitarySpace

for seq being sequence of X

for n being Nat holds (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq))) . n)

for X being RealUnitarySpace

for seq being sequence of X

for n being Nat holds (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq))) . n)

proof end;

theorem :: BHSP_4:54

for Rseq being Real_Sequence

for X being RealUnitarySpace

for seq being sequence of X

for n being Nat holds Sum ((Rseq * seq),(n + 1)) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - (Sum ((((Rseq ^\ 1) - Rseq) * (Partial_Sums seq)),n)) by Th53;

for X being RealUnitarySpace

for seq being sequence of X

for n being Nat holds Sum ((Rseq * seq),(n + 1)) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - (Sum ((((Rseq ^\ 1) - Rseq) * (Partial_Sums seq)),n)) by Th53;