let X be RealNormSpace; :: thesis: for S being sequence of ()
for St being sequence of
for x being Point of ()
for xt being Point of st S = St & x = xt holds
( St is_convergent_to xt iff S is_convergent_to x )

let S be sequence of (); :: thesis: for St being sequence of
for x being Point of ()
for xt being Point of st S = St & x = xt holds
( St is_convergent_to xt iff S is_convergent_to x )

let St be sequence of ; :: thesis: for x being Point of ()
for xt being Point of st S = St & x = xt holds
( St is_convergent_to xt iff S is_convergent_to x )

let x be Point of (); :: thesis: for xt being Point of st S = St & x = xt holds
( St is_convergent_to xt iff S is_convergent_to x )

let xt be Point of ; :: thesis: ( S = St & x = xt implies ( St is_convergent_to xt iff S is_convergent_to x ) )
assume that
A1: S = St and
A2: x = xt ; :: thesis: ( St is_convergent_to xt iff S is_convergent_to x )
A3: now :: thesis: ( S is_convergent_to x implies St is_convergent_to xt )
assume A4: S is_convergent_to x ; :: thesis: St is_convergent_to xt
now :: thesis: for U1t being Subset of st U1t is open & xt in U1t holds
ex n being Nat st
for m being Nat st n <= m holds
St . m in U1t
let U1t be Subset of ; :: thesis: ( U1t is open & xt in U1t implies ex n being Nat st
for m being Nat st n <= m holds
St . m in U1t )

assume that
A5: U1t is open and
A6: xt in U1t ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
St . m in U1t

reconsider U1 = U1t as open Subset of () by ;
consider n being Nat such that
A7: for m being Nat st n <= m holds
S . m in U1 by ;
take n = n; :: thesis: for m being Nat st n <= m holds
St . m in U1t

let m be Nat; :: thesis: ( n <= m implies St . m in U1t )
assume n <= m ; :: thesis: St . m in U1t
hence St . m in U1t by A1, A7; :: thesis: verum
end;
hence St is_convergent_to xt by FRECHET:def 3; :: thesis: verum
end;
now :: thesis: ( St is_convergent_to xt implies S is_convergent_to x )
assume A8: St is_convergent_to xt ; :: thesis:
now :: thesis: for U1 being Subset of () st U1 is open & x in U1 holds
ex n being Nat st
for m being Nat st n <= m holds
S . m in U1
let U1 be Subset of (); :: thesis: ( U1 is open & x in U1 implies ex n being Nat st
for m being Nat st n <= m holds
S . m in U1 )

assume that
A9: U1 is open and
A10: x in U1 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
S . m in U1

reconsider U1t = U1 as open Subset of by ;
consider n being Nat such that
A11: for m being Nat st n <= m holds
St . m in U1t by ;
take n = n; :: thesis: for m being Nat st n <= m holds
S . m in U1

let m be Nat; :: thesis: ( n <= m implies S . m in U1 )
assume n <= m ; :: thesis: S . m in U1
hence S . m in U1 by ; :: thesis: verum
end;
hence S is_convergent_to x by FRECHET:def 3; :: thesis: verum
end;
hence ( St is_convergent_to xt iff S is_convergent_to x ) by A3; :: thesis: verum