for T being non empty TopStruct
for S being sequence of T
for P being Permutation of NAT
for x being Point of T st S is_convergent_to x holds
S * P is_convergent_to x