let T be non empty TopStruct ; for x being Point of T
for Y being Subset of T
for S being sequence of T st Y = { y where y is Point of T : x in Cl {y} } & rng S misses Y & S is_convergent_to x holds
ex S1 being subsequence of S st S1 is one-to-one
let x be Point of T; for Y being Subset of T
for S being sequence of T st Y = { y where y is Point of T : x in Cl {y} } & rng S misses Y & S is_convergent_to x holds
ex S1 being subsequence of S st S1 is one-to-one
let Y be Subset of T; for S being sequence of T st Y = { y where y is Point of T : x in Cl {y} } & rng S misses Y & S is_convergent_to x holds
ex S1 being subsequence of S st S1 is one-to-one
let S be sequence of T; ( Y = { y where y is Point of T : x in Cl {y} } & rng S misses Y & S is_convergent_to x implies ex S1 being subsequence of S st S1 is one-to-one )
assume that
A1:
Y = { y where y is Point of T : x in Cl {y} }
and
A2:
(rng S) /\ Y = {}
and
A3:
S is_convergent_to x
; XBOOLE_0:def 7 ex S1 being subsequence of S st S1 is one-to-one
defpred S1[ Nat, set , set ] means ( $3 in NAT & ( for n1, n2, m being Element of NAT st n1 = $2 & n2 = $3 & n2 <= m holds
S . m <> S . n1 ) );
A4:
for z being set st z in rng S holds
ex n0 being Element of NAT st
for m being Element of NAT st n0 <= m holds
z <> S . m
A7:
for n being Nat
for z1 being set ex z2 being set st S1[n,z1,z2]
proof
let n be
Nat;
for z1 being set ex z2 being set st S1[n,z1,z2]let z1 be
set ;
ex z2 being set st S1[n,z1,z2]
end;
consider f being Function such that
A11:
dom f = NAT
and
A12:
f . 0 = 0
and
A13:
for n being Nat holds S1[n,f . n,f . (n + 1)]
from RECDEF_1:sch 1(A7);
A14:
for n being Nat holds f . n is Element of NAT
then
for n being Nat holds f . n is real
;
then reconsider f = f as Real_Sequence by A11, SEQ_1:2;
f is increasing
then reconsider f = f as increasing sequence of NAT by A14, SEQM_3:13;
take S1 = S * f; S1 is one-to-one
A16:
for n1, n2 being Element of NAT st n1 < n2 holds
S1 . n1 <> S1 . n2
let x1, x2 be object ; FUNCT_1:def 4 ( not x1 in dom S1 or not x2 in dom S1 or not S1 . x1 = S1 . x2 or x1 = x2 )
assume that
A20:
x1 in dom S1
and
A21:
x2 in dom S1
and
A22:
S1 . x1 = S1 . x2
; x1 = x2
reconsider n2 = x2 as Element of NAT by A21;
reconsider n1 = x1 as Element of NAT by A20;
assume A23:
x1 <> x2
; contradiction