let T be non empty TopStruct ; :: thesis: 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
let S be sequence of T; :: thesis: 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
let P be Permutation of NAT ; :: thesis: for x being Point of T st S is_convergent_to x holds
S * P is_convergent_to x
let x be Point of T; :: thesis: ( S is_convergent_to x implies S * P is_convergent_to x )
assume A1: S is_convergent_to x ; :: thesis: S * P is_convergent_to x
for U1 being Subset of T st U1 is open & x in U1 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(S * P) . m in U1

proof

let U1 be Subset of T; :: thesis: ( U1 is open & x in U1 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(S * P) . m in U1 )
assume that
A2: U1 is open and
A3: x in U1 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(S * P) . m in U1
defpred S₁[ set ] means $1 in U1;
A4: 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]

proof

consider n being Element of NAT such that
A5: for m being Element of NAT st n <= m holds
S . m in U1 by A1, A2, A3, FRECHET:def 2;
take n ; :: thesis: for m being Element of NAT
for x being Point of T st n <= m & x = S . m holds
S₁[x]
let m be Element of NAT ; :: thesis: for x being Point of T st n <= m & x = S . m holds
S₁[x]
let x be Point of T; :: thesis: ( n <= m & x = S . m implies S₁[x] )
assume that
A6: n <= m and
A7: x = S . m ; :: thesis: S₁[x]
thus x in U1 by A5, A6, A7; :: thesis: verum

end;

thus ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S₁[(S * P) . m] from FRECHET2:sch 2(A4); :: thesis: verum

end;

hence S * P is_convergent_to x by FRECHET:def 2; :: thesis: verum