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 S1[ Point of T] means x in Cl {$1};
reconsider Y = { y where y is Point of T : S1[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 S2[ set ] means $1 in Y;
A4: for n being Element of NAT ex m being Element of NAT st
( n <= m & S2[S . m] ) by A3;
consider S1 being subsequence of S such that
A5: for n being Element of NAT holds S2[S1 . n] from VALUED_1:sch 1(A4);
take S1 ; :: thesis: S1 is_convergent_to x
rng S1 c= Y
proof
let y be object ; :: 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 object such that
A6: n in dom S1 and
A7: y = S1 . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A6;
S1 . n in Y by A5;
hence y in Y by A7; :: thesis: verum
end;
hence S1 is_convergent_to x by Th33; :: 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
A8: for m being Element of NAT st m >= n0 holds
not S . m in Y ;
set S9 = S ^\ n0;
x in Cl (rng (S ^\ n0)) by A2, Th39, Th40;
then consider S2 being sequence of T such that
A9: rng S2 c= rng (S ^\ n0) and
A10: x in Lim S2 by A1;
A11: S2 is_convergent_to x by A10, FRECHET:def 5;
A12: 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 A8, NAT_1:11;
hence not (S ^\ n0) . n in Y by NAT_1:def 3; :: thesis: verum
end;
(rng (S ^\ n0)) /\ Y = {}
proof
set y = the Element of (rng (S ^\ n0)) /\ Y;
assume A13: (rng (S ^\ n0)) /\ Y <> {} ; :: thesis: contradiction
then the Element of (rng (S ^\ n0)) /\ Y in rng (S ^\ n0) by XBOOLE_0:def 4;
then consider n being object such that
A14: n in dom (S ^\ n0) and
A15: the Element of (rng (S ^\ n0)) /\ Y = (S ^\ n0) . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A14;
not (S ^\ n0) . n in Y by A12;
hence contradiction by A13, A15, XBOOLE_0:def 4; :: thesis: verum
end;
then rng (S ^\ n0) misses Y ;
then consider S29 being subsequence of S2 such that
A16: S29 is one-to-one by A9, A11, Th35, XBOOLE_1:63;
rng S29 c= rng S2 by VALUED_0:21;
then consider P being Permutation of NAT such that
A17: S29 * P is subsequence of S ^\ n0 by A9, A16, Th36, XBOOLE_1:1;
reconsider S1 = S29 * P as subsequence of S ^\ n0 by A17;
reconsider S1 = S1 as subsequence of S by VALUED_0:20;
take S1 ; :: thesis: S1 is_convergent_to x
S29 is_convergent_to x by A11, Th15;
hence S1 is_convergent_to x by Th37; :: thesis: verum
end;
end;