thus ( seq is convergent implies ex g being Real st
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p ) :: thesis: ( ex g being Real st
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p implies seq is convergent )

proof

assume seq is convergent ; :: thesis: ex g being Real st
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p
then consider g being Complex such that
A1: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p ;
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 = |.(Im g).|;
A5: |.(Im g).| > 0 by A4, COMPLEX1:47;
for n being Nat ex m being Nat st
( n <= m & not |.((seq . m) - g).| < |.(Im g).| )

proof

let n be Nat; :: thesis: ex m being Nat st
( n <= m & not |.((seq . m) - g).| < |.(Im g).| )
take n ; :: thesis: ( n <= n & not |.((seq . n) - g).| < |.(Im g).| )
thus n <= n ; :: thesis: not |.((seq . n) - g).| < |.(Im g).|
reconsider sn = seq . n as Element of REAL by XREAL_0:def 1;
A6: Im sn = 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 ;
take g ; :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p )
reconsider p = p as Real ;
( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p ) by A1;
hence ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p ) ; :: thesis: verum

end;

given g being Real such that A9: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((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 object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= |.((seq . b₃) - g).| ) )
thus for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= |.((seq . b₃) - g).| ) ) by A9; :: thesis: verum