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

let U1 be Subset of T; :: according to FRECHET:def 3 :: thesis: ( U1 is open & x in U1 implies ex n being Nat st

for m being Nat st n <= m holds

S . m in U1 )

assume that

U1 is open and

A2: x in U1 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

S . m in U1

take 0 ; :: thesis: for m being Nat st 0 <= m holds

S . m in U1

let m be Nat; :: thesis: ( 0 <= m implies S . m in U1 )

m in NAT by ORDINAL1:def 12;

hence ( 0 <= m implies S . m in U1 ) by A1, A2, FUNCOP_1:7; :: thesis: verum

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

let U1 be Subset of T; :: according to FRECHET:def 3 :: thesis: ( U1 is open & x in U1 implies ex n being Nat st

for m being Nat st n <= m holds

S . m in U1 )

assume that

U1 is open and

A2: x in U1 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

S . m in U1

take 0 ; :: thesis: for m being Nat st 0 <= m holds

S . m in U1

let m be Nat; :: thesis: ( 0 <= m implies S . m in U1 )

m in NAT by ORDINAL1:def 12;

hence ( 0 <= m implies S . m in U1 ) by A1, A2, FUNCOP_1:7; :: thesis: verum