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

for seq being sequence of X st ( for n being Nat holds seq . n = x ) holds

( seq is convergent & lim seq = x )

let x be Point of X; :: thesis: for seq being sequence of X st ( for n being Nat holds seq . n = x ) holds

( seq is convergent & lim seq = x )

let seq be sequence of X; :: thesis: ( ( for n being Nat holds seq . n = x ) implies ( seq is convergent & lim seq = x ) )

assume A1: for n being Nat holds seq . n = x ; :: thesis: ( seq is convergent & lim seq = x )

hence seq is convergent by NDIFF_1:18; :: thesis: lim seq = x

thus lim seq = seq . 0 by A2, NDIFF_1:18

.= x by A1 ; :: thesis: verum

for seq being sequence of X st ( for n being Nat holds seq . n = x ) holds

( seq is convergent & lim seq = x )

let x be Point of X; :: thesis: for seq being sequence of X st ( for n being Nat holds seq . n = x ) holds

( seq is convergent & lim seq = x )

let seq be sequence of X; :: thesis: ( ( for n being Nat holds seq . n = x ) implies ( seq is convergent & lim seq = x ) )

assume A1: for n being Nat holds seq . n = x ; :: thesis: ( seq is convergent & lim seq = x )

now :: thesis: for z, w being object st z in dom seq & w in dom seq holds

seq . z = seq . w

then A2:
seq is constant
by FUNCT_1:def 10;seq . z = seq . w

let z, w be object ; :: thesis: ( z in dom seq & w in dom seq implies seq . z = seq . w )

assume ( z in dom seq & w in dom seq ) ; :: thesis: seq . z = seq . w

then reconsider n1 = z, n2 = w as Nat ;

thus seq . z = seq . n1

.= x by A1

.= seq . n2 by A1

.= seq . w ; :: thesis: verum

end;assume ( z in dom seq & w in dom seq ) ; :: thesis: seq . z = seq . w

then reconsider n1 = z, n2 = w as Nat ;

thus seq . z = seq . n1

.= x by A1

.= seq . n2 by A1

.= seq . w ; :: thesis: verum

hence seq is convergent by NDIFF_1:18; :: thesis: lim seq = x

thus lim seq = seq . 0 by A2, NDIFF_1:18

.= x by A1 ; :: thesis: verum