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 )

for j being Nat st i <= j holds

||.((# x) - (# (s . j))).|| < 1 / n ) implies x in lim_f s )

for j being Nat st i <= j holds

||.((# x) - (# (s . j))).|| < 1 / n ) by A3; :: thesis: verum

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

( ( for n being positive Nat ex i being Nat st
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

for j being Nat st i <= j holds

||.((# x) - (# (s . j))).|| < 1 / n ; :: thesis: verum

end;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

hence
for n being positive Nat ex i 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;

||.((# x) - (# (s . j))).|| < 1 / n

thus for j being Nat st i0 <= j holds

||.((# x) - (# (s . j))).|| < 1 / n by A6; :: thesis: verum

end;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

take i0 = i0; :: 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;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

||.((# x) - (# (s . j))).|| < 1 / n

thus for j being Nat st i0 <= j holds

||.((# x) - (# (s . j))).|| < 1 / n by A6; :: thesis: verum

for j being Nat st i <= j holds

||.((# x) - (# (s . j))).|| < 1 / n ; :: thesis: verum

for j being Nat st i <= j holds

||.((# x) - (# (s . j))).|| < 1 / n ) implies x in lim_f s )

proof

hence
( x in lim_f s iff for n being positive Nat ex i being Nat st
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

end;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

hence
x in lim_f s
by Th6; :: thesis: verum
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

s . j in b ; :: thesis: verum

end;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

hence
for j being Nat st i0 <= j holds
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;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

s . j in b ; :: thesis: verum

for j being Nat st i <= j holds

||.((# x) - (# (s . j))).|| < 1 / n ) by A3; :: thesis: verum