let g be Element of COMPLEX ; :: thesis: for seq being Complex_Sequence st ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) holds
lim seq = g
let seq be Complex_Sequence; :: thesis: ( ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) implies lim seq = g )
assume A1: ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) ; :: thesis: lim seq = g

A2: now

assume that
A3: seq is constant and
A4: g in rng seq ; :: thesis: lim seq = g
consider g1 being Element of COMPLEX such that
A5: rng seq = {g1} by A3, FUNCT_2:188;
consider g2 being Element of COMPLEX such that
A6: for n being Nat holds seq . n = g2 by A3, VALUED_0:def 18;
A7: g = g1 by A4, A5, TARSKI:def 1;
A8: seq is convergent by A3, Th48;

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
|.((seq . m) - g).| < p )
assume A9: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g).| < p
take n = 0 ; :: thesis: for m being Element of NAT st n <= m holds
|.((seq . m) - g).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.((seq . m) - g).| < p )
assume n <= m ; :: thesis: |.((seq . m) - g).| < p
m in NAT ;
then m in dom seq by COMSEQ_1:2;
then seq . m in rng seq by FUNCT_1:def 5;
then g2 in rng seq by A6;
then g2 = g by A5, A7, TARSKI:def 1;
then seq . m = g by A6;
hence |.((seq . m) - g).| < p by A9, COMPLEX1:130; :: thesis: verum

end;

hence lim seq = g by A8, COMSEQ_2:def 5; :: thesis: verum

end;

now

assume that
A10: seq is constant and
A11: ex n being Element of NAT st seq . n = g ; :: thesis: lim seq = g
consider n being Element of NAT such that
A12: seq . n = g by A11;
n in NAT ;
then n in dom seq by COMSEQ_1:2;
hence lim seq = g by A2, A10, A12, FUNCT_1:def 5; :: thesis: verum

end;

hence lim seq = g by A1, A2; :: thesis: verum