let X be RealUnitarySpace; :: thesis: for x being Point of X
for seq being sequence of X st seq is V11() & ex n being Element of NAT st seq . n = x holds
lim seq = x
let x be Point of X; :: thesis: for seq being sequence of X st seq is V11() & ex n being Element of NAT st seq . n = x holds
lim seq = x
let seq be sequence of X; :: thesis: ( seq is V11() & ex n being Element of NAT st seq . n = x implies lim seq = x )
assume that
A1: seq is V11() and
A2: ex n being Element of NAT st seq . n = x ; :: thesis: lim seq = x
consider n being Element of NAT such that
A3: seq . n = x by A2;
n in NAT ;
then n in dom seq by NORMSP_1:17;
then x in rng seq by A3, FUNCT_1:def 5;
hence lim seq = x by A1, Th10; :: thesis: verum