thus ( seq is convergent implies ex g being real number st
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 . m) - g) < p ) :: thesis: ( ex g being real number st
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 . m) - g) < p implies seq is convergent )

proof

assume seq is convergent ; :: thesis: ex g being real number st
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 . m) - g) < p
then 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
|.((seq . m) - g).| < p by COMSEQ_2:def 5;
A2: (Re g) + ((Im g) * <i>) = g by COMPLEX1:13;

now :: thesis: g is real

assume A3: not g is real ; :: thesis: contradiction
A4: Im g <> 0 by A2, A3;
set p = abs (Im g);
A5: abs (Im g) > 0 by A4, COMPLEX1:47;
for n being Element of NAT ex m being Element of NAT st
( n <= m & not |.((seq . m) - g).| < abs (Im g) )

proof

let n be Element of NAT ; :: thesis: ex m being Element of NAT st
( n <= m & not |.((seq . m) - g).| < abs (Im g) )
take n ; :: thesis: ( n <= n & not |.((seq . n) - g).| < abs (Im g) )
thus n <= n ; :: thesis: not |.((seq . n) - g).| < abs (Im g)
A6: Im (seq . n) = 0 by COMPLEX1:def 2;
A7: Im ((seq . n) - g) = (Im (seq . n)) - (Im g) by COMPLEX1:19;
A8: |.((seq . n) - g).| = sqrt (((Re ((seq . n) - g)) ^2) + ((Im g) ^2)) by A7, A6;
(Re ((seq . n) - g)) ^2 >= 0 by XREAL_1:63;
then sqrt (((Re ((seq . n) - g)) ^2) + (|.(Im g).| ^2)) >= |.(Im g).| by SQUARE_1:58;
hence |.((seq . n) - g).| >= |.(Im g).| by A8, COMPLEX1:75; :: thesis: verum

end;

hence contradiction by A1, A5; :: thesis: verum

end;

then reconsider g = g as real number ;
take g ; :: 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 . 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 . m) - g) < p )
reconsider p = p as Real by XREAL_0:def 1;
( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p ) by A1;
hence ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p ) ; :: thesis: verum

end;

given g being real number such that A9: 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 . m) - g) < p ; :: thesis: seq is convergent
g in REAL by XREAL_0:def 1;
then reconsider g = g as Element of COMPLEX by NUMBERS:11;
take g ; :: according to COMSEQ_2:def 5 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= |.((seq . b₃) - g).| ) )
thus for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= |.((seq . b₃) - g).| ) ) by A9; :: thesis: verum