let seq, seq1 be Real_Sequence; :: thesis: ( seq is convergent & seq1 is bounded & lim seq = 0 implies lim (seq (#) seq1) = 0 )
assume that
A1: seq is convergent and
A2: seq1 is bounded and
A3: lim seq = 0 ; :: thesis: lim (seq (#) seq1) = 0
A4: seq (#) seq1 is convergent by A1, A2, A3, Th25;

now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((seq (#) seq1) . m) - 0).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((seq (#) seq1) . m) - 0).| < p )
assume A5: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((seq (#) seq1) . m) - 0).| < p
consider r being Real such that
A6: 0 < r and
A7: for m being Nat holds |.(seq1 . m).| < r by A2, Th3;
A8: 0 < p / r by A5, A6;
then consider n1 being Nat such that
A9: for m being Nat st n1 <= m holds
|.((seq . m) - 0).| < p / r by A1, A3, Def6;
take n = n1; :: thesis: for m being Nat st n <= m holds
|.(((seq (#) seq1) . m) - 0).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((seq (#) seq1) . m) - 0).| < p )
assume n <= m ; :: thesis: |.(((seq (#) seq1) . m) - 0).| < p
then A10: |.((seq . m) - 0).| < p / r by A9;
A11: |.(((seq (#) seq1) . m) - 0).| = |.(((seq . m) * (seq1 . m)) - 0).| by SEQ_1:8
.= |.(seq . m).| * |.(seq1 . m).| by COMPLEX1:65 ;

now :: thesis: ( |.(seq1 . m).| <> 0 implies |.(((seq (#) seq1) . m) - 0).| < p )

assume A12: |.(seq1 . m).| <> 0 ; :: thesis: |.(((seq (#) seq1) . m) - 0).| < p
(p / r) * r = (p * (r ")) * r by XCMPLX_0:def 9
.= p * ((r ") * r)
.= p * 1 by A6, XCMPLX_0:def 7 ;
then A13: (p / r) * |.(seq1 . m).| < p by A7, A8, XREAL_1:68;
0 <= |.(seq1 . m).| by COMPLEX1:46;
then |.(((seq (#) seq1) . m) - 0).| < (p / r) * |.(seq1 . m).| by A10, A11, A12, XREAL_1:68;
hence |.(((seq (#) seq1) . m) - 0).| < p by A13, XXREAL_0:2; :: thesis: verum

end;

hence |.(((seq (#) seq1) . m) - 0).| < p by A5, A11; :: thesis: verum

end;

hence lim (seq (#) seq1) = 0 by A4, Def6; :: thesis: verum