let T be non empty TopStruct ; :: thesis: for x being Point of T
for S being sequence of T st S = NAT --> x holds
S is_convergent_to x
let x be Point of T; :: thesis: for S being sequence of T st S = NAT --> x holds
S is_convergent_to x
let S be sequence of T; :: thesis: ( S = NAT --> x implies S is_convergent_to x )
assume A1: S = NAT --> x ; :: thesis: S is_convergent_to x
thus S is_convergent_to x :: thesis: verum

proof

let U1 be Subset of T; :: according to FRECHET:def 3 :: thesis: ( U1 is open & x in U1 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in U1 )
assume that
U1 is open and
A2: x in U1 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in U1
take 0 ; :: thesis: for m being Element of NAT st 0 <= m holds
S . m in U1
thus for m being Element of NAT st 0 <= m holds
S . m in U1 by A1, A2, FUNCOP_1:7; :: thesis: verum

end;