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 2 :: thesis: ( not U1 is open or not x in U1 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or S1 . b₂ in U1 ) )
assume ( U1 is open & x in U1 ) ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or S1 . b₂ in U1 )
then consider n being Element of NAT such that
A2: for m being Element of NAT st n <= m holds
S . m in U1 by A1, FRECHET:def 2;
take n ; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or S1 . b₁ in U1 )
let m be Element of NAT ; :: thesis: ( not n <= m or S1 . m in U1 )
assume A3: n <= m ; :: thesis: S1 . m in U1
consider NS being increasing sequence of NAT such that
A4: S1 = S * NS by VALUED_0:def 17;
m <= NS . m by SEQM_3:33;
then A5: S . (NS . m) in U1 by A2, A3, XXREAL_0:2;
m in NAT ;
then m in dom S1 by NORMSP_1:17;
hence S1 . m in U1 by A4, A5, FUNCT_1:22; :: thesis: verum