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;
let O be Subset of T; :: according to FRECHET2:def 3 :: thesis: for n being 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 Nat; :: thesis: ( O is open & x in O implies ex m being Element of NAT st
( n <= m & (S ^\ n0) . m in O ) )
assume ( O is open & x in O ) ; :: thesis: ex m being Element of NAT st
( n <= m & (S ^\ n0) . m in O )
then consider m0 being Element of NAT such that
A2: n + n0 <= m0 and
A3: S . m0 in O by A1;
( n0 in NAT & n0 <= n + n0 ) by NAT_1:11, ORDINAL1:def 12;
then reconsider m = m0 - n0 as Element of NAT by A2, INT_1:5, XXREAL_0:2;
take m ; :: thesis: ( n <= m & (S ^\ n0) . m in O )
thus n <= m by A2, XREAL_1:19; :: thesis: (S ^\ n0) . m in O
(S ^\ n0) . m = S . ((m0 - n0) + n0) by NAT_1:def 3
.= S . m0 ;
hence (S ^\ n0) . m in O by A3; :: thesis: verum