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 Nat st
for m being 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 Nat st
for m being Nat st n <= m holds
(S * P) . m in U1 )
defpred S₁[ set ] means $1 in U1;
assume A2: ( U1 is open & x in U1 ) ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
(S * P) . m in U1
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]

proof

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: 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 ( n <= m & x = S . m ) ; :: thesis: S₁[x]
hence S₁[x] by A4; :: thesis: verum

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: for m being Nat st n <= m holds
(S * P) . m in U1
let m be Nat; :: thesis: ( n <= m implies (S * P) . m in U1 )
m in NAT by ORDINAL1:def 12;
hence ( n <= m implies (S * P) . m in U1 ) by A5; :: thesis: verum

end;

hence S * P is_convergent_to x ; :: thesis: verum