let T be non empty TopStruct ; :: thesis: for S being sequence of T
for x being Point of T
for Y being Subset of T st Y = { y where y is Point of T : x in Cl {y} } & rng S c= Y holds
S is_convergent_to x
let S be sequence of T; :: thesis: for x being Point of T
for Y being Subset of T st Y = { y where y is Point of T : x in Cl {y} } & rng S c= Y holds
S is_convergent_to x
let x be Point of T; :: thesis: for Y being Subset of T st Y = { y where y is Point of T : x in Cl {y} } & rng S c= Y holds
S is_convergent_to x
let Y be Subset of T; :: thesis: ( Y = { y where y is Point of T : x in Cl {y} } & rng S c= Y implies S is_convergent_to x )
assume that
A1: Y = { y where y is Point of T : x in Cl {y} } and
A2: rng S c= Y ; :: thesis: S is_convergent_to x
let U1 be Subset of T; :: according to FRECHET:def 3 :: thesis: ( not U1 is open or not x in U1 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or S . b₂ in U1 ) )
assume A3: ( U1 is open & x in U1 ) ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or S . b₂ in U1 )
take 0 ; :: thesis: for b₁ being set holds
( not 0 <= b₁ or S . b₁ in U1 )
let m be Nat; :: thesis: ( not 0 <= m or S . m in U1 )
m in NAT by ORDINAL1:def 12;
then m in dom S by NORMSP_1:12;
then S . m in rng S by FUNCT_1:def 3;
then S . m in Y by A2;
then consider y being Point of T such that
A4: y = S . m and
A5: x in Cl {y} by A1;
assume 0 <= m ; :: thesis: S . m in U1
{y} meets U1 by A3, A5, PRE_TOPC:def 7;
hence S . m in U1 by A4, ZFMISC_1:50; :: thesis: verum