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
defpred S₁[ 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

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 )
defpred S₂[ set ] means $1 = z;
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
then reconsider z9 = z as Point of T ;
assume for n0 being Element of NAT ex m being Element of NAT st
( n0 <= m & z = S . m ) ; :: thesis: contradiction
then A6: for n being Element of NAT ex m being Element of NAT st
( n <= m & S₂[S . m] ) ;
ex S1 being subsequence of S st
for n being Element of NAT holds S₂[S1 . n] from VALUED_1:sch 1(A6);
then x in Cl {z9} by A3, Th15, Th34;
then z9 in Y by A1;
hence contradiction by A2, A5, XBOOLE_0:def 4; :: thesis: verum

end;

A7: for n being Nat
for z1 being set ex z2 being set st S₁[n,z1,z2]

proof

let n be 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 A8: 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
A9: n1 = z1 and
n2 = 0 and
n2 <= m ; :: thesis: S . m <> S . n1
thus S . m <> S . n1 by A8, A9; :: 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:12;
then S . z1 in rng S by FUNCT_1:def 3;
then consider n0 being Element of NAT such that
A10: 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 ( n1 = z1 & n2 = n0 & n2 <= m ) ; :: thesis: S . m <> S . n1
hence S . m <> S . n1 by A10; :: thesis: verum

end;

end;

end;

consider f being Function such that
A11: dom f = NAT and
A12: f . 0 = 0 and
A13: for n being Nat holds S₁[n,f . n,f . (n + 1)] from RECDEF_1:sch 1(A7);
A14: for n being Nat holds f . n is Element of NAT

proof

let n be Nat; :: thesis: f . n is Element of NAT
A15: n in NAT by ORDINAL1:def 12;

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 A12; :: 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:6;
then 1 <= n by NAT_1:13;
then reconsider n1 = n - 1 as Element of NAT by INT_1:5, A15;
n1 + 1 = n ;
hence f . n is Element of NAT by A13; :: thesis: verum

end;

end;

end;

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

proof

let n be Nat; :: according to SEQM_3:def 6 :: thesis: not f . (n + 1) <= f . n
reconsider nn = n, nn1 = n + 1 as Element of NAT by ORDINAL1:def 12;
reconsider n2 = f . nn1 as Element of NAT by A14;
reconsider n1 = f . nn as Element of NAT by A14;
assume f . n >= f . (n + 1) ; :: thesis: contradiction
then n2 <= n1 ;
then S . n1 <> S . n1 by A13;
hence contradiction ; :: thesis: verum

end;

then reconsider f = f as increasing sequence of NAT by A14, SEQM_3:13;
take S1 = S * f; :: thesis: S1 is one-to-one
A16: 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 )
reconsider n19 = f . n1 as Element of NAT ;
n2 in NAT ;
then n2 in dom S1 by NORMSP_1:12;
then A17: S . (f . n2) = S1 . n2 by FUNCT_1:12;
assume n1 < n2 ; :: thesis: S1 . n1 <> S1 . n2
then A18: n1 + 1 <= n2 by 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 A18, XXREAL_0:1;
hence f . (n1 + 1) <= f . n2 by SEQM_3:1; :: thesis: verum

end;

end;

end;

then A19: S . (f . n2) <> S . n19 by A13;
n1 in NAT ;
then n1 in dom S1 by NORMSP_1:12;
hence S1 . n1 <> S1 . n2 by A19, A17, FUNCT_1:12; :: thesis: verum

end;

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( 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 ; :: thesis: x1 = x2
reconsider n2 = x2 as Element of NAT by A21;
reconsider n1 = x1 as Element of NAT by A20;
assume A23: x1 <> x2 ; :: thesis: contradiction

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

suppose n1 < n2 ; :: thesis: contradiction

hence contradiction by A22, A16; :: thesis: verum

end;

suppose n2 < n1 ; :: thesis: contradiction

hence contradiction by A22, A16; :: thesis: verum

end;

end;