let X be Complex_Banach_Algebra; :: thesis: for seq being sequence of X

for rseq being Real_Sequence st ( for n being Nat holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds

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

let seq be sequence of X; :: thesis: for rseq being Real_Sequence st ( for n being Nat holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds

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

let rseq be Real_Sequence; :: thesis: ( ( for n being Nat holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 implies ( seq is convergent & lim seq = 0. X ) )

assume that

A1: for n being Nat holds ||.(seq . n).|| <= rseq . n and

A2: rseq is convergent and

A3: lim rseq = 0 ; :: thesis: ( seq is convergent & lim seq = 0. X )

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (0. X)).|| < p ;

hence seq is convergent ; :: thesis: lim seq = 0. X

hence lim seq = 0. X by A8, CLVECT_1:def 16; :: thesis: verum

for rseq being Real_Sequence st ( for n being Nat holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds

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

let seq be sequence of X; :: thesis: for rseq being Real_Sequence st ( for n being Nat holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds

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

let rseq be Real_Sequence; :: thesis: ( ( for n being Nat holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 implies ( seq is convergent & lim seq = 0. X ) )

assume that

A1: for n being Nat holds ||.(seq . n).|| <= rseq . n and

A2: rseq is convergent and

A3: lim rseq = 0 ; :: thesis: ( seq is convergent & lim seq = 0. X )

now :: thesis: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (0. X)).|| < p

then A8:
for p being Real st 0 < p holds ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (0. X)).|| < p

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

for m being Nat st n <= m holds

||.((seq . m) - (0. X)).|| < p )

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

for m being Nat st n <= m holds

||.((seq . m) - (0. X)).|| < p

then consider n being Nat such that

A4: for m being Nat st n <= m holds

|.((rseq . m) - 0).| < p by A2, A3, SEQ_2:def 7;

for m being Nat st n <= m holds

||.((seq . m) - (0. X)).|| < p ; :: thesis: verum

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

||.((seq . m) - (0. X)).|| < p )

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

for m being Nat st n <= m holds

||.((seq . m) - (0. X)).|| < p

then consider n being Nat such that

A4: for m being Nat st n <= m holds

|.((rseq . m) - 0).| < p by A2, A3, SEQ_2:def 7;

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

||.((seq . m) - (0. X)).|| < p

hence
ex n being Nat st ||.((seq . m) - (0. X)).|| < p

let m be Nat; :: thesis: ( n <= m implies ||.((seq . m) - (0. X)).|| < p )

assume n <= m ; :: thesis: ||.((seq . m) - (0. X)).|| < p

then A5: |.((rseq . m) - 0).| < p by A4;

A6: ||.((seq . m) - (0. X)).|| = ||.(seq . m).|| by RLVECT_1:13;

A7: rseq . m <= |.(rseq . m).| by ABSVALUE:4;

||.(seq . m).|| <= rseq . m by A1;

then ||.((seq . m) - (0. X)).|| <= |.(rseq . m).| by A6, A7, XXREAL_0:2;

hence ||.((seq . m) - (0. X)).|| < p by A5, XXREAL_0:2; :: thesis: verum

end;assume n <= m ; :: thesis: ||.((seq . m) - (0. X)).|| < p

then A5: |.((rseq . m) - 0).| < p by A4;

A6: ||.((seq . m) - (0. X)).|| = ||.(seq . m).|| by RLVECT_1:13;

A7: rseq . m <= |.(rseq . m).| by ABSVALUE:4;

||.(seq . m).|| <= rseq . m by A1;

then ||.((seq . m) - (0. X)).|| <= |.(rseq . m).| by A6, A7, XXREAL_0:2;

hence ||.((seq . m) - (0. X)).|| < p by A5, XXREAL_0:2; :: thesis: verum

for m being Nat st n <= m holds

||.((seq . m) - (0. X)).|| < p ; :: thesis: verum

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (0. X)).|| < p ;

hence seq is convergent ; :: thesis: lim seq = 0. X

hence lim seq = 0. X by A8, CLVECT_1:def 16; :: thesis: verum