let X be RealUnitarySpace; :: thesis: for x being Point of X
for seq being sequence of X st seq is V11() & x in rng seq holds
lim seq = x
let x be Point of X; :: thesis: for seq being sequence of X st seq is V11() & x in rng seq holds
lim seq = x
let seq be sequence of X; :: thesis: ( seq is V11() & x in rng seq implies lim seq = x )
assume that
A1: seq is V11() 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:188;
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

let r be Real; :: thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq . n),x < r )
assume A7: r > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq . n),x < r
take m = 0 ; :: thesis: for n being Element of NAT st n >= m holds
dist (seq . n),x < r
let n be Element of NAT ; :: thesis: ( n >= m implies dist (seq . n),x < r )
assume n >= m ; :: thesis: dist (seq . n),x < r
n in NAT ;
then n in dom seq by NORMSP_1:17;
then seq . n in rng seq by FUNCT_1:def 5;
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:41; :: thesis: verum

end;

seq is convergent by A1, Th1;
hence lim seq = x by A6, Def2; :: thesis: verum