let seq, seq9 be Real_Sequence; :: thesis: ( seq is convergent & seq9 is convergent implies lim (seq (#) seq9) = (lim seq) * (lim seq9) )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; :: thesis: lim (seq (#) seq9) = (lim seq) * (lim seq9)
consider r being real number such that
A3: 0 < r and
A4: for n being Element of NAT holds abs (seq . n) < r by A1, Th15;
A5: 0 <= abs (lim seq9) by COMPLEX1:46;
A6: 0 + 0 < (abs (lim seq9)) + r by A3, COMPLEX1:46, XREAL_1:8;

now

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 (#) seq9) . m) - ((lim seq) * (lim seq9))) < p )
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq9) . m) - ((lim seq) * (lim seq9))) < p
then A7: 0 < p / ((abs (lim seq9)) + r) by A6, XREAL_1:139;
then consider n1 being Element of NAT such that
A8: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (lim seq)) < p / ((abs (lim seq9)) + r) by A1, Def7;
consider n2 being Element of NAT such that
A9: for m being Element of NAT st n2 <= m holds
abs ((seq9 . m) - (lim seq9)) < p / ((abs (lim seq9)) + r) by A2, A7, Def7;
take n = n1 + n2; :: thesis: for m being Element of NAT st n <= m holds
abs (((seq (#) seq9) . m) - ((lim seq) * (lim seq9))) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((seq (#) seq9) . m) - ((lim seq) * (lim seq9))) < p )
assume A10: n <= m ; :: thesis: abs (((seq (#) seq9) . m) - ((lim seq) * (lim seq9))) < p
A11: 0 <= abs (seq . m) by COMPLEX1:46;
A12: 0 <= abs ((seq9 . m) - (lim seq9)) by COMPLEX1:46;
n2 <= n by NAT_1:12;
then n2 <= m by A10, XXREAL_0:2;
then A13: abs ((seq9 . m) - (lim seq9)) < p / ((abs (lim seq9)) + r) by A9;
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A10, XXREAL_0:2;
then A14: abs ((seq . m) - (lim seq)) <= p / ((abs (lim seq9)) + r) by A8;
abs (((seq (#) seq9) . m) - ((lim seq) * (lim seq9))) = abs ((((seq . m) * (seq9 . m)) - (((seq . m) * (lim seq9)) - ((seq . m) * (lim seq9)))) - ((lim seq) * (lim seq9))) by SEQ_1:8
.= abs (((seq . m) * ((seq9 . m) - (lim seq9))) + (((seq . m) - (lim seq)) * (lim seq9))) ;
then A15: abs (((seq (#) seq9) . m) - ((lim seq) * (lim seq9))) <= (abs ((seq . m) * ((seq9 . m) - (lim seq9)))) + (abs (((seq . m) - (lim seq)) * (lim seq9))) by COMPLEX1:56;
abs (seq . m) < r by A4;
then (abs (seq . m)) * (abs ((seq9 . m) - (lim seq9))) < r * (p / ((abs (lim seq9)) + r)) by A11, A12, A13, XREAL_1:96;
then A16: abs ((seq . m) * ((seq9 . m) - (lim seq9))) < r * (p / ((abs (lim seq9)) + r)) by COMPLEX1:65;
abs (((seq . m) - (lim seq)) * (lim seq9)) = (abs (lim seq9)) * (abs ((seq . m) - (lim seq))) by COMPLEX1:65;
then A17: abs (((seq . m) - (lim seq)) * (lim seq9)) <= (abs (lim seq9)) * (p / ((abs (lim seq9)) + r)) by A5, A14, XREAL_1:64;
(r * (p / ((abs (lim seq9)) + r))) + ((abs (lim seq9)) * (p / ((abs (lim seq9)) + r))) = (p / ((abs (lim seq9)) + r)) * ((abs (lim seq9)) + r)
.= p by A6, XCMPLX_1:87 ;
then (abs ((seq . m) * ((seq9 . m) - (lim seq9)))) + (abs (((seq . m) - (lim seq)) * (lim seq9))) < p by A16, A17, XREAL_1:8;
hence abs (((seq (#) seq9) . m) - ((lim seq) * (lim seq9))) < p by A15, XXREAL_0:2; :: thesis: verum

end;

hence lim (seq (#) seq9) = (lim seq) * (lim seq9) by A1, A2, Def7; :: thesis: verum