let T be non empty TopStruct ; :: thesis: for S being sequence of T
for x being Point of T
for n0 being Nat st x is_a_cluster_point_of S holds
x is_a_cluster_point_of S ^\ n0
let S be sequence of T; :: thesis: for x being Point of T
for n0 being Nat st x is_a_cluster_point_of S holds
x is_a_cluster_point_of S ^\ n0
let x be Point of T; :: thesis: for n0 being Nat st x is_a_cluster_point_of S holds
x is_a_cluster_point_of S ^\ n0
let n0 be Nat; :: thesis: ( x is_a_cluster_point_of S implies x is_a_cluster_point_of S ^\ n0 )
assume A1: x is_a_cluster_point_of S ; :: thesis: x is_a_cluster_point_of S ^\ n0
set S1 = S ^\ n0;
A2: for n being Element of NAT holds (S ^\ n0) . n = S . (n + n0) by NAT_1:def 3;
let O be Subset of T; :: according to FRECHET2:def 4 :: thesis: for n being Element of NAT st O is open & x in O holds
ex m being Element of NAT st
( n <= m & (S ^\ n0) . m in O )
let n be Element of NAT ; :: thesis: ( O is open & x in O implies ex m being Element of NAT st
( n <= m & (S ^\ n0) . m in O ) )
assume that
A4: O is open and
A5: x in O ; :: thesis: ex m being Element of NAT st
( n <= m & (S ^\ n0) . m in O )
consider m0 being Element of NAT such that
A6: n + n0 <= m0 and
A7: S . m0 in O by A1, A4, A5, Def4;
X: n0 in NAT by ORDINAL1:def 13;
n0 <= n + n0 by NAT_1:11;
then reconsider m = m0 - n0 as Element of NAT by A6, X, INT_1:18, XXREAL_0:2;
take m ; :: thesis: ( n <= m & (S ^\ n0) . m in O )
thus n <= m by A6, XREAL_1:21; :: thesis: (S ^\ n0) . m in O
(S ^\ n0) . m = S . ((m0 - n0) + n0) by A2
.= S . m0 ;
hence (S ^\ n0) . m in O by A7; :: thesis: verum