consider R being Real such that
A5: 0 < R and
A6: for m being Nat holds |.(s1 . m).| < R by A2, Th8;
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((s (#) s1) . m) - 0c).| < p )
assume A7: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((s (#) s1) . m) - 0c).| < p
A8: 0 < p / R by A7, A5;
then consider n1 being Nat such that
A9: for m being Nat st n1 <= m holds
|.((s . m) - 0c).| < p / R by A1, A3, Def6;
take n = n1; :: thesis: for m being Nat st n <= m holds
|.(((s (#) s1) . m) - 0c).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((s (#) s1) . m) - 0c).| < p )
(p / R) * R = (p * (R ")) * R by XCMPLX_0:def 9
.= p * ((R ") * R)
.= p * 1 by A5, XCMPLX_0:def 7 ;
then A10: (p / R) * |.(s1 . m).| < p by A6, A8, XREAL_1:68;
assume n <= m ; :: thesis: |.(((s (#) s1) . m) - 0c).| < p
then A11: |.((s . m) - 0c).| < p / R by A9;
A12: |.(((s (#) s1) . m) - 0c).| = |.((s . m) * (s1 . m)).| by VALUED_1:5
.= |.(s . m).| * |.(s1 . m).| by COMPLEX1:65 ;
A13: 0 <= |.(s1 . m).| by COMPLEX1:46;
hence |.(((s (#) s1) . m) - 0c).| < p by A7, A12; :: thesis: verum