let X be Complex_Banach_Algebra; :: thesis: for s, s' being sequence of X st s is convergent & s' is convergent holds
lim (s * s') = (lim s) * (lim s')
let s, s' be sequence of X; :: thesis: ( s is convergent & s' is convergent implies lim (s * s') = (lim s) * (lim s') )
assume that
A1: s is convergent and
A2: s' is convergent ; :: thesis: lim (s * s') = (lim s) * (lim s')
||.s.|| is bounded by A1, CLVECT_1:119, SEQ_2:27;
then consider R being real number such that
A3: for n being Element of NAT holds ||.s.|| . n < R by SEQ_2:def 3;
set g2 = lim s';
set g1 = lim s;
set g = (lim s) * (lim s');

A4: now

let n be Element of NAT ; :: thesis: ||.(s . n).|| < R
||.(s . n).|| = ||.s.|| . n by CLVECT_1:def 17;
hence ||.(s . n).|| < R by A3; :: thesis: verum

end;

||.(s . 1).|| = ||.s.|| . 1 by CLVECT_1:def 17;
then 0 <= ||.s.|| . 1 by CLVECT_1:106;
then A5: 0 < R by A3;
reconsider R = R as Real by XREAL_0:def 1;
A6: 0 + 0 < ||.(lim s').|| + R by A5, CLVECT_1:106, XREAL_1:10;
A7: 0 <= ||.(lim s').|| by CLVECT_1:106;

A8: now

let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((s * s') . m) - ((lim s) * (lim s'))).|| < p )
assume A9: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((s * s') . m) - ((lim s) * (lim s'))).|| < p
then consider n1 being Element of NAT such that
A10: for m being Element of NAT st n1 <= m holds
||.((s . m) - (lim s)).|| < p / (||.(lim s').|| + R) by A1, A6, CLVECT_1:def 18;
consider n2 being Element of NAT such that
A11: for m being Element of NAT st n2 <= m holds
||.((s' . m) - (lim s')).|| < p / (||.(lim s').|| + R) by A2, A6, A9, CLVECT_1:def 18;
take n = n1 + n2; :: thesis: for m being Element of NAT st n <= m holds
||.(((s * s') . m) - ((lim s) * (lim s'))).|| < p
let m be Element of NAT ; :: thesis: ( n <= m implies ||.(((s * s') . m) - ((lim s) * (lim s'))).|| < p )
assume A12: n <= m ; :: thesis: ||.(((s * s') . m) - ((lim s) * (lim s'))).|| < p
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A12, XXREAL_0:2;
then ||.((s . m) - (lim s)).|| <= p / (||.(lim s').|| + R) by A10;
then A13: ||.(lim s').|| * ||.((s . m) - (lim s)).|| <= ||.(lim s').|| * (p / (||.(lim s').|| + R)) by A7, XREAL_1:66;
||.(((s . m) - (lim s)) * (lim s')).|| <= ||.(lim s').|| * ||.((s . m) - (lim s)).|| by CLOPBAN3:42;
then A14: ||.(((s . m) - (lim s)) * (lim s')).|| <= ||.(lim s').|| * (p / (||.(lim s').|| + R)) by A13, XXREAL_0:2;
A15: 0 <= ||.(s . m).|| by CLVECT_1:106;
||.(((s * s') . m) - ((lim s) * (lim s'))).|| = ||.(((s . m) * (s' . m)) - ((lim s) * (lim s'))).|| by CLOPBAN3:def 10
.= ||.((((s . m) * (s' . m)) - ((s . m) * (lim s'))) + (((s . m) * (lim s')) - ((lim s) * (lim s')))).|| by CLOPBAN3:42
.= ||.(((s . m) * ((s' . m) - (lim s'))) + (((s . m) * (lim s')) - ((lim s) * (lim s')))).|| by CLOPBAN3:42
.= ||.(((s . m) * ((s' . m) - (lim s'))) + (((s . m) - (lim s)) * (lim s'))).|| by CLOPBAN3:42 ;
then A16: ||.(((s * s') . m) - ((lim s) * (lim s'))).|| <= ||.((s . m) * ((s' . m) - (lim s'))).|| + ||.(((s . m) - (lim s)) * (lim s')).|| by CLVECT_1:def 11;
A17: ||.((s . m) * ((s' . m) - (lim s'))).|| <= ||.(s . m).|| * ||.((s' . m) - (lim s')).|| by CLOPBAN3:42;
n2 <= n by NAT_1:12;
then n2 <= m by A12, XXREAL_0:2;
then A18: ||.((s' . m) - (lim s')).|| < p / (||.(lim s').|| + R) by A11;
A19: 0 <= ||.((s' . m) - (lim s')).|| by CLVECT_1:106;
||.(s . m).|| < R by A4;
then ||.(s . m).|| * ||.((s' . m) - (lim s')).|| < R * (p / (||.(lim s').|| + R)) by A15, A19, A18, XREAL_1:98;
then A20: ||.((s . m) * ((s' . m) - (lim s'))).|| < R * (p / (||.(lim s').|| + R)) by A17, XXREAL_0:2;
(R * (p / (||.(lim s').|| + R))) + (||.(lim s').|| * (p / (||.(lim s').|| + R))) = (p / (||.(lim s').|| + R)) * (||.(lim s').|| + R)
.= p by A6, XCMPLX_1:88 ;
then ||.((s . m) * ((s' . m) - (lim s'))).|| + ||.(((s . m) - (lim s)) * (lim s')).|| < p by A20, A14, XREAL_1:10;
hence ||.(((s * s') . m) - ((lim s) * (lim s'))).|| < p by A16, XXREAL_0:2; :: thesis: verum

end;

s * s' is convergent by A1, A2, Th3;
hence lim (s * s') = (lim s) * (lim s') by A8, CLVECT_1:def 18; :: thesis: verum