let X be RealUnitarySpace; :: thesis: for x being Point of X

for seq being sequence of X st seq is constant & x in rng seq holds

lim seq = x

let x be Point of X; :: thesis: for seq being sequence of X st seq is constant & x in rng seq holds

lim seq = x

let seq be sequence of X; :: thesis: ( seq is constant & x in rng seq implies lim seq = x )

assume that

A1: seq is constant and

A2: x in rng seq ; :: thesis: lim seq = x

consider y being Point of X such that

A3: rng seq = {y} by A1, FUNCT_2:111;

consider z being Point of X such that

A4: for n being Nat holds seq . n = z by A1, VALUED_0:def 18;

A5: x = y by A2, A3, TARSKI:def 1;

hence lim seq = x by A6, Def2; :: thesis: verum

for seq being sequence of X st seq is constant & x in rng seq holds

lim seq = x

let x be Point of X; :: thesis: for seq being sequence of X st seq is constant & x in rng seq holds

lim seq = x

let seq be sequence of X; :: thesis: ( seq is constant & x in rng seq implies lim seq = x )

assume that

A1: seq is constant and

A2: x in rng seq ; :: thesis: lim seq = x

consider y being Point of X such that

A3: rng seq = {y} by A1, FUNCT_2:111;

consider z being Point of X such that

A4: for n being Nat holds seq . n = z by A1, VALUED_0:def 18;

A5: x = y by A2, A3, TARSKI:def 1;

A6: now :: thesis: for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),x) < r

seq is convergent
by A1;ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),x) < r

let r be Real; :: thesis: ( r > 0 implies ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),x) < r )

assume A7: r > 0 ; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),x) < r

reconsider m = 0 as Nat ;

take m = m; :: thesis: for n being Nat st n >= m holds

dist ((seq . n),x) < r

let n be Nat; :: thesis: ( n >= m implies dist ((seq . n),x) < r )

assume n >= m ; :: thesis: dist ((seq . n),x) < r

n in NAT by ORDINAL1:def 12;

then n in dom seq by NORMSP_1:12;

then seq . n in rng seq by FUNCT_1:def 3;

then z in rng seq by A4;

then z = x by A3, A5, TARSKI:def 1;

then seq . n = x by A4;

hence dist ((seq . n),x) < r by A7, BHSP_1:34; :: thesis: verum

end;for n being Nat st n >= m holds

dist ((seq . n),x) < r )

assume A7: r > 0 ; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),x) < r

reconsider m = 0 as Nat ;

take m = m; :: thesis: for n being Nat st n >= m holds

dist ((seq . n),x) < r

let n be Nat; :: thesis: ( n >= m implies dist ((seq . n),x) < r )

assume n >= m ; :: thesis: dist ((seq . n),x) < r

n in NAT by ORDINAL1:def 12;

then n in dom seq by NORMSP_1:12;

then seq . n in rng seq by FUNCT_1:def 3;

then z in rng seq by A4;

then z = x by A3, A5, TARSKI:def 1;

then seq . n = x by A4;

hence dist ((seq . n),x) < r by A7, BHSP_1:34; :: thesis: verum

hence lim seq = x by A6, Def2; :: thesis: verum