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