let X be Complex_Banach_Algebra; :: thesis: 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; :: thesis: 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 H_{1}( Nat) -> Element of REAL = (Partial_Sums ||.(Conj ($1,z,w)).||) . $1;

ex rseq being Real_Sequence st

for k being Nat holds rseq . k = H_{1}(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; :: thesis: ( ( 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 ; :: thesis: ( seq is convergent & lim seq = 0. X )

then lim rseq = 0 by A5, SEQ_2:def 7;

hence ( seq is convergent & lim seq = 0. X ) by A4, A8, Th12; :: thesis: verum

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; :: thesis: 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 H

ex rseq being Real_Sequence st

for k being Nat holds rseq . k = H

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; :: thesis: ( ( 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 ; :: thesis: ( seq is convergent & lim seq = 0. X )

A3: now :: thesis: for k being Nat holds ||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k

let k be Nat; :: thesis: ||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k

||.(seq . k).|| = ||.((Partial_Sums (Conj (k,z,w))) . k).|| by A2;

hence ||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k by Th10; :: thesis: verum

end;||.(seq . k).|| = ||.((Partial_Sums (Conj (k,z,w))) . k).|| by A2;

hence ||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k by Th10; :: thesis: verum

A4: now :: thesis: for k being Nat holds ||.(seq . k).|| <= rseq . k

let k be Nat; :: thesis: ||.(seq . k).|| <= rseq . k

||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k by A3;

hence ||.(seq . k).|| <= rseq . k by A1; :: thesis: verum

end;||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k by A3;

hence ||.(seq . k).|| <= rseq . k by A1; :: thesis: verum

A5: now :: thesis: for p being Real st p > 0 holds

ex n being Nat st

for k being Nat st n <= k holds

|.((rseq . k) - 0).| < p

then A8:
rseq is convergent
by SEQ_2:def 6;ex n being Nat st

for k being Nat st n <= k holds

|.((rseq . k) - 0).| < p

let p be Real; :: thesis: ( p > 0 implies ex n being Nat st

for k being Nat st n <= k holds

|.((rseq . k) - 0).| < p )

assume p > 0 ; :: thesis: ex n being Nat st

for k being Nat st n <= k holds

|.((rseq . k) - 0).| < p

then consider n being Nat such that

A6: for k being Nat st n <= k holds

|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p by Th31;

take n = n; :: thesis: for k being Nat st n <= k holds

|.((rseq . k) - 0).| < p

|.((rseq . k) - 0).| < p ; :: thesis: verum

end;for k being Nat st n <= k holds

|.((rseq . k) - 0).| < p )

assume p > 0 ; :: thesis: ex n being Nat st

for k being Nat st n <= k holds

|.((rseq . k) - 0).| < p

then consider n being Nat such that

A6: for k being Nat st n <= k holds

|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p by Th31;

take n = n; :: thesis: for k being Nat st n <= k holds

|.((rseq . k) - 0).| < p

now :: thesis: for k being Nat st n <= k holds

|.((rseq . k) - 0).| < p

hence
for k being Nat st n <= k holds |.((rseq . k) - 0).| < p

let k be Nat; :: thesis: ( n <= k implies |.((rseq . k) - 0).| < p )

assume A7: n <= k ; :: thesis: |.((rseq . k) - 0).| < p

|.((rseq . k) - 0).| = |.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| by A1;

hence |.((rseq . k) - 0).| < p by A6, A7; :: thesis: verum

end;assume A7: n <= k ; :: thesis: |.((rseq . k) - 0).| < p

|.((rseq . k) - 0).| = |.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| by A1;

hence |.((rseq . k) - 0).| < p by A6, A7; :: thesis: verum

|.((rseq . k) - 0).| < p ; :: thesis: verum

then lim rseq = 0 by A5, SEQ_2:def 7;

hence ( seq is convergent & lim seq = 0. X ) by A4, A8, Th12; :: thesis: verum