let g be Complex; :: thesis: for seq being Complex_Sequence st ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being 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 Nat st seq . n = g ) ) implies lim seq = g )
A1: now :: thesis: ( seq is constant & g in rng seq & ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Nat st seq . n = g ) ) implies lim seq = g )
assume that
A2: seq is constant and
A3: g in rng seq ; :: thesis: ( ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Nat st seq . n = g ) ) implies lim seq = g )
consider g1 being Element of COMPLEX such that
A4: rng seq = {g1} by A2, FUNCT_2:111;
consider g2 being Element of COMPLEX such that
A5: for n being Nat holds seq . n = g2 by A2, VALUED_0:def 18;
A6: g = g1 by A3, A4, TARSKI:def 1;
A7: now :: 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 )
assume A8: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p
reconsider n = 0 as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((seq . m) - g).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - g).| < p )
assume n <= m ; :: thesis: |.((seq . m) - g).| < p
m in NAT by ORDINAL1:def 12;
then m in dom seq by COMSEQ_1:2;
then seq . m in rng seq by FUNCT_1:def 3;
then g2 in rng seq by A5;
then g2 = g by A4, A6, TARSKI:def 1;
then seq . m = g by A5;
hence |.((seq . m) - g).| < p by A8, COMPLEX1:44; :: thesis: verum
end;
seq is convergent by A2, Th26;
hence ( ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Nat st seq . n = g ) ) implies lim seq = g ) by A7, COMSEQ_2:def 6; :: thesis: verum
end;
A9: now :: thesis: ( seq is constant & ex n being Nat st seq . n = g & ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Nat st seq . n = g ) ) implies lim seq = g )
assume that
seq is constant and
A10: ex n being Nat st seq . n = g ; :: thesis: ( ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Nat st seq . n = g ) ) implies lim seq = g )
consider n being Nat such that
A11: seq . n = g by A10;
n in NAT by ORDINAL1:def 12;
then n in dom seq by COMSEQ_1:2;
hence ( ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Nat st seq . n = g ) ) implies lim seq = g ) by A1, A11, FUNCT_1:def 3; :: thesis: verum
end;
assume ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Nat st seq . n = g ) ) ; :: thesis: lim seq = g
hence lim seq = g by A1, A9; :: thesis: verum