let T be non empty TopStruct ; :: thesis: for S being sequence of T
for S1 being subsequence of S
for x being Point of T st S is_convergent_to x holds
S1 is_convergent_to x
let S be sequence of T; :: thesis: for S1 being subsequence of S
for x being Point of T st S is_convergent_to x holds
S1 is_convergent_to x
let S1 be subsequence of S; :: thesis: for x being Point of T st S is_convergent_to x holds
S1 is_convergent_to x
let x be Point of T; :: thesis: ( S is_convergent_to x implies S1 is_convergent_to x )
assume A1: S is_convergent_to x ; :: thesis: S1 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 S1 . b₂ in U1 ) )
assume ( U1 is open & x in U1 ) ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or S1 . b₂ in U1 )
then consider n being Nat such that
A2: for m being Nat st n <= m holds
S . m in U1 by A1;
take n ; :: thesis: for b₁ being set holds
( not n <= b₁ or S1 . b₁ in U1 )
let m be Nat; :: thesis: ( not n <= m or S1 . m in U1 )
assume A3: n <= m ; :: thesis: S1 . m in U1
m in NAT by ORDINAL1:def 12;
then A4: m in dom S1 by NORMSP_1:12;
consider NS being increasing sequence of NAT such that
A5: S1 = S * NS by VALUED_0:def 17;
m <= NS . m by SEQM_3:14;
then S . (NS . m) in U1 by A2, A3, XXREAL_0:2;
hence S1 . m in U1 by A5, A4, FUNCT_1:12; :: thesis: verum