let T be non empty TopStruct ; :: thesis:
let S be sequence of T; :: thesis:
let P be Permutation of NAT; :: thesis:
let x be Point of T; :: thesis:
assume A1: S is_convergent_to x ; :: thesis:
for U1 being Subset of T st U1 is open & x in U1 holds
ex n being Nat st
for m being Nat st n <= m holds
(S * P) . m in U1

let U1 be Subset of T; :: thesis:
defpred S₁[ set ] means $1 in U1;
assume A2: ( U1 is open & x in U1 ) ; :: thesis:
A3: ex n being Element of NAT st
for m being Element of NAT
for x being Point of T st n <= m & x = S . m holds
S₁[x]

consider n being Nat such that
A4: for m being Nat st n <= m holds
S . m in U1 by A1, A2;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
take n ; :: thesis:
let m be Element of NAT ; :: thesis:
let x be Point of T; :: thesis:
assume ( n <= m & x = S . m ) ; :: thesis:
hence S₁[x] by A4; :: thesis:

end;

consider n being Element of NAT such that
A5: for m being Element of NAT st n <= m holds
S₁[(S * P) . m] from FRECHET2:sch 2(A3);
take n ; :: thesis:
let m be Nat; :: thesis:
m in NAT by ORDINAL1:def 12;
hence ( n <= m implies (S * P) . m in U1 ) by A5; :: thesis:

end;