let T be non empty TopStruct ; :: thesis: ( T is Frechet implies for S being sequence of T
for x being Point of T st x is_a_cluster_point_of S holds
ex S1 being subsequence of S st S1 is_convergent_to x )
assume A1: T is Frechet ; :: thesis: for S being sequence of T
for x being Point of T st x is_a_cluster_point_of S holds
ex S1 being subsequence of S st S1 is_convergent_to x
let S be sequence of T; :: thesis: for x being Point of T st x is_a_cluster_point_of S holds
ex S1 being subsequence of S st S1 is_convergent_to x
let x be Point of T; :: thesis: ( x is_a_cluster_point_of S implies ex S1 being subsequence of S st S1 is_convergent_to x )
assume A2: x is_a_cluster_point_of S ; :: thesis: ex S1 being subsequence of S st S1 is_convergent_to x
defpred S₁[ Point of T] means x in Cl {$1};
reconsider Y = { y where y is Point of T : S₁[y] } as Subset of T from DOMAIN_1:sch 7();

per cases ( for n being Element of NAT ex m being Element of NAT st
( m >= n & S . m in Y ) or ex n being Element of NAT st
for m being Element of NAT st m >= n holds
not S . m in Y ) ;

suppose A3: for n being Element of NAT ex m being Element of NAT st
( m >= n & S . m in Y ) ; :: thesis: ex S1 being subsequence of S st S1 is_convergent_to x

defpred S₂[ set ] means $1 in Y;
A4: for n being Element of NAT ex m being Element of NAT st
( n <= m & S₂[S . m] ) by A3;
consider S1 being subsequence of S such that
A7: for n being Element of NAT holds S₂[S1 . n] from VALUED_1:sch 1(A4);
A8: rng S1 c= Y

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng S1 or y in Y )
assume y in rng S1 ; :: thesis: y in Y
then consider n being set such that
A9: n in dom S1 and
A10: y = S1 . n by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A9;
S1 . n in Y by A7;
hence y in Y by A10; :: thesis: verum

end;

take S1 ; :: thesis: S1 is_convergent_to x
thus S1 is_convergent_to x by A8, Th36; :: thesis: verum

end;

suppose ex n being Element of NAT st
for m being Element of NAT st m >= n holds
not S . m in Y ; :: thesis: ex S1 being subsequence of S st S1 is_convergent_to x

then consider n0 being Element of NAT such that
A11: for m being Element of NAT st m >= n0 holds
not S . m in Y ;
set S' = S ^\ n0;
A12: for n being Element of NAT holds (S ^\ n0) . n = S . (n + n0) by NAT_1:def 3;
A13: for n being Element of NAT holds not (S ^\ n0) . n in Y

proof

let n be Element of NAT ; :: thesis: not (S ^\ n0) . n in Y
not S . (n + n0) in Y by A11, NAT_1:11;
hence not (S ^\ n0) . n in Y by A12; :: thesis: verum

end;

(rng (S ^\ n0)) /\ Y = {}

proof

assume A14: (rng (S ^\ n0)) /\ Y <> {} ; :: thesis: contradiction
consider y being Element of (rng (S ^\ n0)) /\ Y;
( y in rng (S ^\ n0) & y in Y ) by A14, XBOOLE_0:def 4;
then consider n being set such that
A15: n in dom (S ^\ n0) and
A16: y = (S ^\ n0) . n by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A15;
not (S ^\ n0) . n in Y by A13;
hence contradiction by A14, A16, XBOOLE_0:def 4; :: thesis: verum

end;

then A17: rng (S ^\ n0) misses Y by XBOOLE_0:def 7;
x is_a_cluster_point_of S ^\ n0 by A2, Th43;
then x in Cl (rng (S ^\ n0)) by Th44;
then consider S2 being sequence of T such that
A18: rng S2 c= rng (S ^\ n0) and
A19: x in Lim S2 by A1, FRECHET:def 5;
A20: S2 is_convergent_to x by A19, FRECHET:def 4;
rng S2 misses Y by A17, A18, XBOOLE_1:63;
then consider S2' being subsequence of S2 such that
A21: S2' is one-to-one by A20, Th38;
rng S2' c= rng S2 by VALUED_0:21;
then rng S2' c= rng (S ^\ n0) by A18, XBOOLE_1:1;
then consider P being Permutation of NAT such that
A22: S2' * P is subsequence of S ^\ n0 by A21, Th39;
reconsider S1 = S2' * P as subsequence of S ^\ n0 by A22;
reconsider S1 = S1 as subsequence of S by VALUED_0:20;
take S1 ; :: thesis: S1 is_convergent_to x
S2' is_convergent_to x by A20, Th18;
hence S1 is_convergent_to x by Th40; :: thesis: verum

end;

end;