let N be RealNormSpace; :: thesis:
let s be sequence of the carrier of (TopSpaceMetr (MetricSpaceNorm N)); :: thesis:
let x be Point of (TopSpaceMetr (MetricSpaceNorm N)); :: thesis:
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 )

let n be positive Nat; :: thesis:
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;

let j be Nat; :: thesis:
assume A7: i0 <= j ; :: thesis:
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:

end;

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

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:

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 )

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:
for b being Element of Balls x ex i being Nat st
for j being Nat st i <= j holds
s . j in b

let b be Element of Balls x; :: thesis:
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

let j be Nat; :: thesis:
assume i0 <= j ; :: thesis:
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:

end;

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

end;

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: