let X be Banach_Algebra; for w, z being Element of X
for seq being sequence of X st ( for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) holds
( seq is convergent & lim seq = 0. X )
let w, z be Element of X; for seq being sequence of X st ( for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) holds
( seq is convergent & lim seq = 0. X )
deffunc H1( Nat) -> Element of REAL = (Partial_Sums ||.(Conj ($1,z,w)).||) . $1;
ex rseq being Real_Sequence st
for k being Nat holds rseq . k = H1(k)
from SEQ_1:sch 1();
then consider rseq being Real_Sequence such that
A1:
for k being Nat holds rseq . k = (Partial_Sums ||.(Conj (k,z,w)).||) . k
;
let seq be sequence of X; ( ( for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) implies ( seq is convergent & lim seq = 0. X ) )
assume A2:
for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k
; ( seq is convergent & lim seq = 0. X )
then A8:
rseq is convergent
by SEQ_2:def 6;
then
lim rseq = 0
by A5, SEQ_2:def 7;
hence
( seq is convergent & lim seq = 0. X )
by A4, A8, Th12; verum