let T be non empty TopStruct ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: according to XBOOLE_0:def 7 :: thesis: ex S1 being subsequence of S st S1 is one-to-one
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

proof

let z be set ; :: thesis: ( z in rng S implies ex n0 being Element of NAT st
for m being Element of NAT st n0 <= m holds
z <> S . m )
assume A5: z in rng S ; :: thesis: ex n0 being Element of NAT st
for m being Element of NAT st n0 <= m holds
z <> S . m
assume A6: for n0 being Element of NAT ex m being Element of NAT st
( n0 <= m & z = S . m ) ; :: thesis: contradiction
reconsider z' = z as Point of T by A5;
defpred S₁[ set ] means $1 = z;
A7: for n being Element of NAT ex m being Element of NAT st
( n <= m & S₁[S . m] ) by A6;
consider S1 being subsequence of S such that
A10: for n being Element of NAT holds S₁[S1 . n] from VALUED_1:sch 1(A7);
S1 is_convergent_to x by A3, Th18;
then x in Cl {z'} by A10, Th37;
then z' in Y by A1;
hence contradiction by A2, A5, XBOOLE_0:def 4; :: thesis: verum

end;

defpred S₁[ Element of 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 ) );
A11: for n being Element of NAT
for z1 being set ex z2 being set st S₁[n,z1,z2]

proof

let n be Element of NAT ; :: thesis: for z1 being set ex z2 being set st S₁[n,z1,z2]
let z1 be set ; :: thesis: ex z2 being set st S₁[n,z1,z2]

per cases ( not z1 in NAT or z1 in NAT ) ;

suppose A12: not z1 in NAT ; :: thesis: ex z2 being set st S₁[n,z1,z2]

take 0 ; :: thesis: S₁[n,z1, 0 ]
thus 0 in NAT ; :: thesis: for n1, n2, m being Element of NAT st n1 = z1 & n2 = 0 & n2 <= m holds
S . m <> S . n1
let n1, n2, m be Element of NAT ; :: thesis: ( n1 = z1 & n2 = 0 & n2 <= m implies S . m <> S . n1 )
assume that
A13: n1 = z1 and
( n2 = 0 & n2 <= m ) ; :: thesis: S . m <> S . n1
thus S . m <> S . n1 by A12, A13; :: thesis: verum

end;

suppose z1 in NAT ; :: thesis: ex z2 being set st S₁[n,z1,z2]

then z1 in dom S by NORMSP_1:17;
then S . z1 in rng S by FUNCT_1:def 5;
then consider n0 being Element of NAT such that
A14: for m being Element of NAT st n0 <= m holds
S . z1 <> S . m by A4;
take n0 ; :: thesis: S₁[n,z1,n0]
thus n0 in NAT ; :: thesis: for n1, n2, m being Element of NAT st n1 = z1 & n2 = n0 & n2 <= m holds
S . m <> S . n1
let n1, n2, m be Element of NAT ; :: thesis: ( n1 = z1 & n2 = n0 & n2 <= m implies S . m <> S . n1 )
assume that
A15: n1 = z1 and
A16: n2 = n0 and
A17: n2 <= m ; :: thesis: S . m <> S . n1
thus S . m <> S . n1 by A14, A15, A16, A17; :: thesis: verum

end;

end;

end;

consider f being Function such that
A18: dom f = NAT and
A19: f . 0 = 0 and
A20: for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] from RECDEF_1:sch 1(A11);
A21: for n being Element of NAT holds f . n is Element of NAT

proof

let n be Element of NAT ; :: thesis: f . n is Element of NAT

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: f . n is Element of NAT

hence f . n is Element of NAT by A19; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: f . n is Element of NAT

then 0 < n by NAT_1:3;
then 0 + 1 < n + 1 by XREAL_1:8;
then 1 <= n by NAT_1:13;
then reconsider n1 = n - 1 as Element of NAT by INT_1:18;
n1 + 1 = n ;
hence f . n is Element of NAT by A20; :: thesis: verum

end;

end;

end;

then for n being Element of NAT holds f . n is real ;
then reconsider f = f as Real_Sequence by A18, SEQ_1:4;
f is increasing

proof

let n be Element of NAT ; :: according to SEQM_3:def 11 :: thesis: not f . (n + 1) <= f . n
assume A22: f . n >= f . (n + 1) ; :: thesis: contradiction
reconsider n1 = f . n as Element of NAT by A21;
reconsider n2 = f . (n + 1) as Element of NAT by A21;
n2 <= n1 by A22;
then S . n1 <> S . n1 by A20;
hence contradiction ; :: thesis: verum

end;

then reconsider f = f as increasing sequence of NAT by A21, SEQM_3:29;
take S1 = S * f; :: thesis: S1 is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom S1 or not x2 in dom S1 or not S1 . x1 = S1 . x2 or x1 = x2 )
assume that
A23: x1 in dom S1 and
A24: x2 in dom S1 and
A25: S1 . x1 = S1 . x2 ; :: thesis: x1 = x2
assume A26: x1 <> x2 ; :: thesis: contradiction
A27: for n1, n2 being Element of NAT st n1 < n2 holds
S1 . n1 <> S1 . n2

proof

let n1, n2 be Element of NAT ; :: thesis: ( n1 < n2 implies S1 . n1 <> S1 . n2 )
assume A28: n1 < n2 ; :: thesis: S1 . n1 <> S1 . n2
reconsider n1' = f . n1 as Element of NAT ;
reconsider n3' = f . (n1 + 1) as Element of NAT ;
n3' <= f . n2

proof

A29: n1 + 1 <= n2 by A28, NAT_1:13;
f . (n1 + 1) <= f . n2

proof

per cases ( n1 + 1 = n2 or n1 + 1 <> n2 ) ;

suppose n1 + 1 = n2 ; :: thesis: f . (n1 + 1) <= f . n2

hence f . (n1 + 1) <= f . n2 ; :: thesis: verum

end;

suppose n1 + 1 <> n2 ; :: thesis: f . (n1 + 1) <= f . n2

then n1 + 1 < n2 by A29, XXREAL_0:1;
hence f . (n1 + 1) <= f . n2 by SEQM_3:7; :: thesis: verum

end;

end;

end;

hence n3' <= f . n2 ; :: thesis: verum

end;

then A30: S . (f . n2) <> S . n1' by A20;
n2 in NAT ;
then n2 in dom S1 by NORMSP_1:17;
then A31: S . (f . n2) = S1 . n2 by FUNCT_1:22;
n1 in NAT ;
then n1 in dom S1 by NORMSP_1:17;
hence S1 . n1 <> S1 . n2 by A30, A31, FUNCT_1:22; :: thesis: verum

end;

reconsider n1 = x1 as Element of NAT by A23;
reconsider n2 = x2 as Element of NAT by A24;

per cases ( n1 < n2 or n2 < n1 ) by A26, XXREAL_0:1;

suppose n1 < n2 ; :: thesis: contradiction

hence contradiction by A25, A27; :: thesis: verum

end;

suppose n2 < n1 ; :: thesis: contradiction

hence contradiction by A25, A27; :: thesis: verum

end;

end;