consider g being Element of COMPLEX such that
A1: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s . m) - g).| < p by Def4;
take r = g *' ; :: according to COMSEQ_2:def 4 :: thesis: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s *' ) . m) - r).| < p
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 *' ) . m) - r).| < p )
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s *' ) . m) - r).| < p
then consider n being Element of NAT such that
A2: for m being Element of NAT st n <= m holds
|.((s . m) - g).| < p by A1;
take n ; :: thesis: for m being Element of NAT st n <= m holds
|.(((s *' ) . m) - r).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.(((s *' ) . m) - r).| < p )
assume A3: n <= m ; :: thesis: |.(((s *' ) . m) - r).| < p
|.(((s *' ) . m) - r).| = |.(((s . m) *' ) - (g *' )).| by Def2
.= |.(((s . m) - g) *' ).| by COMPLEX1:120
.= |.((s . m) - g).| by COMPLEX1:139 ;
hence |.(((s *' ) . m) - r).| < p by A2, A3; :: thesis: verum