let seq, seq1 be Real_Sequence; :: thesis: ( seq is convergent & seq1 is bounded & lim seq = 0 implies seq (#) seq1 is convergent )
assume that
A1: seq is convergent and
A2: seq1 is bounded and
A3: lim seq = 0 ; :: thesis: seq (#) seq1 is convergent
reconsider g1 = 0 as Real ;
take g = g1; :: according to SEQ_2:def 6 :: thesis: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq1) . m) - g) < p
let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq1) . m) - g) < p )
assume A4: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq1) . m) - g) < p
consider r being real number such that
A5: 0 < r and
A6: for m being Element of NAT holds abs (seq1 . m) < r by A2, Th15;
A7: 0 < p / r by A4, A5, XREAL_1:141;
then consider n1 being Element of NAT such that
A8: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - 0 ) < p / r by A1, A3, Def7;
take n = n1; :: thesis: for m being Element of NAT st n <= m holds
abs (((seq (#) seq1) . m) - g) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((seq (#) seq1) . m) - g) < p )
assume A9: n <= m ; :: thesis: abs (((seq (#) seq1) . m) - g) < p
abs (seq . m) = abs ((seq . m) - 0 ) ;
then A10: abs (seq . m) < p / r by A8, A9;
A11: abs (((seq (#) seq1) . m) - g) = abs (((seq . m) * (seq1 . m)) - 0 ) by SEQ_1:12
.= (abs (seq . m)) * (abs (seq1 . m)) by COMPLEX1:151 ;

now

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

end;

hence abs (((seq (#) seq1) . m) - g) < p by A4, A11; :: thesis: verum