let N be RealNormSpace; :: thesis: for s being sequence of the carrier of (TopSpaceMetr (MetricSpaceNorm N))
for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) holds
( x in lim_f s iff for n being positive Nat ex i being Nat st
for j being Nat st i <= j holds
||.((# x) - (# (s . j))).|| < 1 / n )
let s be sequence of the carrier of (TopSpaceMetr (MetricSpaceNorm N)); :: thesis: for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) holds
( x in lim_f s iff for n being positive Nat ex i being Nat st
for j being Nat st i <= j holds
||.((# x) - (# (s . j))).|| < 1 / n )
let x be Point of (TopSpaceMetr (MetricSpaceNorm N)); :: thesis: ( x in lim_f s iff for n being positive Nat ex i being Nat st
for j being Nat st i <= j holds
||.((# x) - (# (s . j))).|| < 1 / n )
reconsider x1 = x as Point of (TopSpaceMetr (MetricSpaceNorm N)) ;
consider y0 being Point of (MetricSpaceNorm N) such that
A1: y0 = x1 and
A2: Balls x1 = { (Ball (y0,(1 / n))) where n is Nat : n <> 0 } by FRECHET:def 1;
A3: ( x in lim_f s implies for n being positive Nat ex i being Nat st
for j being Nat st i <= j holds
||.((# x) - (# (s . j))).|| < 1 / n )

proof

assume A4: x in lim_f s ; :: thesis: for n being positive Nat ex i being Nat st
for j being Nat st i <= j holds
||.((# x) - (# (s . j))).|| < 1 / n

now :: thesis: for n being positive Nat ex i0 being Nat st
for j being Nat st i0 <= j holds
||.((# x) - (# (s . j))).|| < 1 / n

let n be positive Nat; :: thesis: ex i0 being Nat st
for j being Nat st i0 <= j holds
||.((# x) - (# (s . j))).|| < 1 / n
Ball (y0,(1 / n)) in Balls x1 by A2;
then consider i0 being Nat such that
A5: for j being Nat st i0 <= j holds
s . j in Ball (y0,(1 / n)) by A4, Th6;

A6: now :: thesis: for j being Nat st i0 <= j holds
||.((# x) - (# (s . j))).|| < 1 / n

let j be Nat; :: thesis: ( i0 <= j implies ||.((# x) - (# (s . j))).|| < 1 / n )
assume A7: i0 <= j ; :: thesis: ||.((# x) - (# (s . j))).|| < 1 / n
consider y1 being Point of N such that
A8: y0 = y1 and
A9: Ball (y0,(1 / n)) = { q where q is Point of N : ||.(y1 - q).|| < 1 / n } by NORMSP_2:2;
s . j in { q where q is Point of N : ||.(y1 - q).|| < 1 / n } by A7, A5, A9;
then consider q0 being Point of N such that
A10: s . j = q0 and
A11: ||.(y1 - q0).|| < 1 / n ;
thus ||.((# x) - (# (s . j))).|| < 1 / n by A1, A8, A10, A11; :: thesis: verum

end;

take i0 = i0; :: thesis: for j being Nat st i0 <= j holds
||.((# x) - (# (s . j))).|| < 1 / n
thus for j being Nat st i0 <= j holds
||.((# x) - (# (s . j))).|| < 1 / n by A6; :: thesis: verum

end;

hence for n being positive Nat ex i being Nat st
for j being Nat st i <= j holds
||.((# x) - (# (s . j))).|| < 1 / n ; :: thesis: verum

end;

( ( for n being positive Nat ex i being Nat st
for j being Nat st i <= j holds
||.((# x) - (# (s . j))).|| < 1 / n ) implies x in lim_f s )

proof

assume A12: for n being positive Nat ex i being Nat st
for j being Nat st i <= j holds
||.((# x) - (# (s . j))).|| < 1 / n ; :: thesis: x in lim_f s
for b being Element of Balls x ex i being Nat st
for j being Nat st i <= j holds
s . j in b

proof

let b be Element of Balls x; :: thesis: ex i being Nat st
for j being Nat st i <= j holds
s . j in b
b in { (Ball (y0,(1 / n))) where n is Nat : n <> 0 } by A2;
then consider n0 being Nat such that
A13: b = Ball (y0,(1 / n0)) and
A14: n0 <> 0 ;
consider i0 being Nat such that
A15: for j being Nat st i0 <= j holds
||.((# x) - (# (s . j))).|| < 1 / n0 by A12, A14;
take i0 ; :: thesis: for j being Nat st i0 <= j holds
s . j in b
for j being Nat st i0 <= j holds
s . j in b

proof

let j be Nat; :: thesis: ( i0 <= j implies s . j in b )
assume i0 <= j ; :: thesis: s . j in b
then A16: ||.((# x1) - (# (s . j))).|| < 1 / n0 by A15;
consider y1 being Point of N such that
A17: y0 = y1 and
A18: Ball (y0,(1 / n0)) = { q where q is Point of N : ||.(y1 - q).|| < 1 / n0 } by NORMSP_2:2;
thus s . j in b by A1, A13, A16, A17, A18; :: thesis: verum

end;

hence for j being Nat st i0 <= j holds
s . j in b ; :: thesis: verum

end;

hence x in lim_f s by Th6; :: thesis: verum

end;

hence ( x in lim_f s iff for n being positive Nat ex i being Nat st
for j being Nat st i <= j holds
||.((# x) - (# (s . j))).|| < 1 / n ) by A3; :: thesis: verum