let X be LinearTopSpace; :: thesis:
let s be sequence of the carrier of X; :: thesis:
let x be Point of X; :: thesis:
let V be local_base of X; :: thesis:
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;

assume A2: x in lim_f s ; :: thesis:
let v be Subset of X; :: thesis:
assume v in V /\ (NeighborhoodSystem (0. X)) ; :: thesis:
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:

end;

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

let b be Element of B; :: thesis:
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:
thus for j being Nat st i0 <= j holds
s . j in b by A5, A8; :: thesis:

end;