let X be LinearTopSpace; :: thesis: for s being sequence of the carrier of X

for x being Point of X

for V being local_base of X holds

( x in lim_f s iff for v being Subset of X st v in V /\ (NeighborhoodSystem (0. X)) holds

ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v )

let s be sequence of the carrier of X; :: thesis: for x being Point of X

for V being local_base of X holds

( x in lim_f s iff for v being Subset of X st v in V /\ (NeighborhoodSystem (0. X)) holds

ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v )

let x be Point of X; :: thesis: for V being local_base of X holds

( x in lim_f s iff for v being Subset of X st v in V /\ (NeighborhoodSystem (0. X)) holds

ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v )

let V be local_base of X; :: thesis: ( x in lim_f s iff for v being Subset of X st v in V /\ (NeighborhoodSystem (0. X)) holds

ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v )

set B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } ;

reconsider B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } as Subset-Family of X by Lm2;

A1: B is basis of (BOOL2F (NeighborhoodSystem x)) by Th10;

ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v ; :: thesis: x in lim_f s

for b being Element of B ex i being Nat st

for j being Nat st i <= j holds

s . j in b

for x being Point of X

for V being local_base of X holds

( x in lim_f s iff for v being Subset of X st v in V /\ (NeighborhoodSystem (0. X)) holds

ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v )

let s be sequence of the carrier of X; :: thesis: for x being Point of X

for V being local_base of X holds

( x in lim_f s iff for v being Subset of X st v in V /\ (NeighborhoodSystem (0. X)) holds

ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v )

let x be Point of X; :: thesis: for V being local_base of X holds

( x in lim_f s iff for v being Subset of X st v in V /\ (NeighborhoodSystem (0. X)) holds

ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v )

let V be local_base of X; :: thesis: ( x in lim_f s iff for v being Subset of X st v in V /\ (NeighborhoodSystem (0. X)) holds

ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v )

set B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } ;

reconsider B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } as Subset-Family of X by Lm2;

A1: B is basis of (BOOL2F (NeighborhoodSystem x)) by Th10;

hereby :: thesis: ( ( for v being Subset of X st v in V /\ (NeighborhoodSystem (0. X)) holds

ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v ) implies x in lim_f s )

assume A4:
for v being Subset of X st v in V /\ (NeighborhoodSystem (0. X)) holds ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v ) implies x in lim_f s )

assume A2:
x in lim_f s
; :: thesis: for v being Subset of X st v in V /\ (NeighborhoodSystem (0. X)) holds

ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v

let v be Subset of X; :: thesis: ( v in V /\ (NeighborhoodSystem (0. X)) implies ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v )

assume v in V /\ (NeighborhoodSystem (0. X)) ; :: thesis: ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v

then ( v in V & v in NeighborhoodSystem (0. X) ) by XBOOLE_0:def 4;

then ( v in V & v is a_neighborhood of 0. X ) by YELLOW19:2;

then x + v in B ;

then reconsider b = x + v as Element of B ;

consider i0 being Nat such that

A3: for j being Nat st i0 <= j holds

s . j in b by A2, A1, CARDFIL2:97;

thus ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v by A3; :: thesis: verum

end;ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v

let v be Subset of X; :: thesis: ( v in V /\ (NeighborhoodSystem (0. X)) implies ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v )

assume v in V /\ (NeighborhoodSystem (0. X)) ; :: thesis: ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v

then ( v in V & v in NeighborhoodSystem (0. X) ) by XBOOLE_0:def 4;

then ( v in V & v is a_neighborhood of 0. X ) by YELLOW19:2;

then x + v in B ;

then reconsider b = x + v as Element of B ;

consider i0 being Nat such that

A3: for j being Nat st i0 <= j holds

s . j in b by A2, A1, CARDFIL2:97;

thus ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v by A3; :: thesis: verum

ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v ; :: thesis: x in lim_f s

for b being Element of B 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 A1, CARDFIL2:97; :: thesis: verum
let b be Element of B; :: thesis: ex i being Nat st

for j being Nat st i <= j holds

s . j in b

not B is empty by Lm2;

then b in B ;

then consider U1 being Subset of X such that

A5: b = x + U1 and

A6: U1 in V and

A7: U1 is a_neighborhood of 0. X ;

U1 in NeighborhoodSystem (0. X) by A7, YELLOW19:2;

then U1 in V /\ (NeighborhoodSystem (0. X)) by A6, XBOOLE_0:def 4;

then consider i0 being Nat such that

A8: for j being Nat st i0 <= j holds

s . j in x + U1 by A4;

take i0 ; :: thesis: for j being Nat st i0 <= j holds

s . j in b

thus for j being Nat st i0 <= j holds

s . j in b by A5, A8; :: thesis: verum

end;for j being Nat st i <= j holds

s . j in b

not B is empty by Lm2;

then b in B ;

then consider U1 being Subset of X such that

A5: b = x + U1 and

A6: U1 in V and

A7: U1 is a_neighborhood of 0. X ;

U1 in NeighborhoodSystem (0. X) by A7, YELLOW19:2;

then U1 in V /\ (NeighborhoodSystem (0. X)) by A6, XBOOLE_0:def 4;

then consider i0 being Nat such that

A8: for j being Nat st i0 <= j holds

s . j in x + U1 by A4;

take i0 ; :: thesis: for j being Nat st i0 <= j holds

s . j in b

thus for j being Nat st i0 <= j holds

s . j in b by A5, A8; :: thesis: verum