:: The Sequential Closure Operator In Sequential and Frechet Spaces
::  by Bart{\l}omiej Skorulski
::
:: Received February 13, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, PRE_TOPC, RCOMP_1, TARSKI, NAT_1, NUMBERS, FUNCOP_1,
      FRECHET, SUBSET_1, CARD_1, STRUCT_0, ORDINAL2, RELAT_1, SEQ_1, VALUED_0,
      XXREAL_0, FUNCT_1, RLVECT_3, CARD_3, SETFAM_1, ORDINAL1, ZFMISC_1,
      FINSET_1, ARYTM_3, SEQ_2, METRIC_1, PCOMPS_1, METRIC_6, XREAL_0, REAL_1,
      WAYBEL_7, ARYTM_1, FUNCT_2, FRECHET2;
 notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
      ORDINAL1, SETFAM_1, FINSET_1, CARD_3, TOPS_2, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, SEQ_1, FUNCT_2, REAL_1, NAT_1, XXREAL_2, VALUED_0, METRIC_1,
      PCOMPS_1, TBSP_1, DOMAIN_1, STRUCT_0, PRE_TOPC, FUNCOP_1, METRIC_6,
      YELLOW_8, FRECHET, SEQ_4;
 constructors SETFAM_1, SEQ_1, REALSET1, CARD_3, TOPS_2, TBSP_1, METRIC_6,
      YELLOW_8, FRECHET, SEQ_4, RELSET_1, FUNCOP_1;
 registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0,
      MEMBERED, STRUCT_0, METRIC_1, PCOMPS_1, FRECHET, VALUED_0, CARD_1,
      XXREAL_2, ORDINAL1, FINSET_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, SEQM_3, PRE_TOPC, TOPS_2, METRIC_6, FUNCT_1, FRECHET,
      XBOOLE_0;
 theorems FRECHET, URYSOHN1, YELLOW_8, PRE_TOPC, TARSKI, FUNCOP_1, NORMSP_1,
      ZFMISC_1, PCOMPS_1, FUNCT_1, AXIOMS, CARD_1, RELAT_1, SETFAM_1, ORDINAL1,
      FUNCT_2, TOPS_2, SUBSET_1, SEQM_3, NAT_1, INT_1, SEQ_1, TOPMETR,
      METRIC_6, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_0, XREAL_1, XXREAL_0,
      VALUED_0, XXREAL_2, CARD_3;
 schemes CLASSES1, DOMAIN_1, NAT_1, RECDEF_1, SEQ_1, FUNCT_1, VALUED_1;

begin

Lm1: for T being non empty TopSpace st for p being Point of T holds Cl({p}) =
{p} holds T is T_1
proof
  let T be non empty TopSpace;
  assume
A1: for p being Point of T holds Cl({p}) = {p};
  for p being Point of T holds {p} is closed
  proof
    let p be Point of T;
    Cl({p}) = {p} by A1;
    hence thesis by PRE_TOPC:22;
  end;
  hence thesis by URYSOHN1:19;
end;

Lm2: for T being non empty TopSpace holds not T is T_1 implies ex x1,x2 being
Point of T st x1 <> x2 & x2 in Cl({x1})
proof
  let T be non empty TopSpace;
  assume not T is T_1;
  then consider x1 being Point of T such that
A1: Cl{x1} <> {x1} by Lm1;
  not {x1} c= Cl{x1} or not Cl{x1} c= {x1} by A1,XBOOLE_0:def 10;
  then consider x2 being set such that
A2: x2 in Cl{x1} and
A3: not x2 in {x1} by PRE_TOPC:18,TARSKI:def 3;
  reconsider x2 as Point of T by A2;
  take x1,x2;
  thus x1 <> x2 by A3,TARSKI:def 1;
  thus thesis by A2;
end;

Lm3: for T being non empty TopSpace holds not T is T_1 implies ex x1,x2 being
Point of T, S being sequence of T st S = (NAT --> x1) & x1 <> x2 & S
is_convergent_to x2
proof
  let T be non empty TopSpace;
  assume not T is T_1;
  then consider x1,x2 being Point of T such that
A1: x1 <> x2 and
A2: x2 in Cl({x1}) by Lm2;
  set S = NAT --> x1;
  take x1,x2,S;
  thus S = (NAT --> x1);
  thus x1 <> x2 by A1;
  thus S is_convergent_to x2
  proof
    let U1 be Subset of T;
    assume
A3: U1 is open & x2 in U1;
    take 0;
    {x1} meets U1 by A2,A3,PRE_TOPC:def 7;
    then x1 in U1 by ZFMISC_1:50;
    hence thesis by FUNCOP_1:7;
  end;
end;

Lm4: for T being non empty TopSpace holds T is T_2 implies T is T_1
proof
  let T be non empty TopSpace;
  assume T is T_2;
  then for p being Point of T holds {p} is closed by PCOMPS_1:7;
  hence thesis by URYSOHN1:19;
end;

theorem
  for T being non empty 1-sorted, S being sequence of T, NS being
  increasing sequence of NAT holds S*NS is sequence of T;

theorem
  for RS being Real_Sequence st RS=id NAT holds RS is increasing
  sequence of NAT;

theorem Th3:
  for T being non empty 1-sorted, S being sequence of T, A being
Subset of T holds (for S1 being subsequence of S holds not rng S1 c= A) implies
ex n being Element of NAT st for m being Element of NAT st n <= m holds not S.m
  in A
proof
  let T be non empty 1-sorted, S be sequence of T, A be Subset of T;
  assume
A1: for S1 being subsequence of S holds not rng S1 c= A;
  defpred Q[set] means $1 in A;
  assume
  for n being Element of NAT ex m being Element of NAT st n <= m & S.m in A;
  then
A2: for n being Element of NAT ex m being Element of NAT st n <= m & Q[S.m];
  consider S1 being subsequence of S such that
A3: for n being Element of NAT holds Q[S1.n] from VALUED_1:sch 1(A2);
  rng S1 c= A
  proof
    let y be set;
    assume y in rng S1;
    then consider x1 being set such that
A4: x1 in dom S1 and
A5: S1.x1 = y by FUNCT_1:def 3;
    reconsider n=x1 as Element of NAT by A4;
    S1.n in A by A3;
    hence thesis by A5;
  end;
  hence contradiction by A1;
end;

theorem Th4:
  for T being non empty 1-sorted,S being sequence of T, A,B being
Subset of T st rng S c= A \/ B holds ex S1 being subsequence of S st rng S1 c=
  A or rng S1 c= B
proof
  let T be non empty 1-sorted,S be sequence of T, A,B be Subset of T;
  assume
A1: rng S c= A \/ B;
  assume
A2: for S1 being subsequence of S holds not rng S1 c= A & not rng S1 c= B;
  then consider n1 being Element of NAT such that
A3: for m being Element of NAT st n1 <= m holds not S.m in A by Th3;
  consider n2 being Element of NAT such that
A4: for m being Element of NAT st n2 <= m holds not S.m in B by A2,Th3;
  reconsider n=max(n1,n2) as Element of NAT;
A5: not S.n in B by A4,XXREAL_0:25;
  n in NAT;
  then n in dom S by NORMSP_1:12;
  then
A6: S.n in rng S by FUNCT_1:def 3;
  not S.n in A by A3,XXREAL_0:25;
  hence contradiction by A1,A5,A6,XBOOLE_0:def 3;
end;

Lm5: for T being non empty TopSpace st T is first-countable holds for x being
Point of T holds ex B being Basis of x st ex S being Function st dom S = NAT &
rng S = B & for n,m being Element of NAT st m >= n holds S.m c= S.n
proof
  let T be non empty TopSpace;
  assume
A1: T is first-countable;
  let x be Point of T;
  consider B1 being Basis of x such that
A2: B1 is countable by A1,FRECHET:def 2;
  consider f being Function of NAT,B1 such that
A3: rng f = B1 by A2,CARD_3:96;
  defpred P[set,set] means $2 = meet (f.:succ $1);
A4: for n being set st n in NAT ex A being set st P[n,A];
  consider S being Function such that
A5: dom S = NAT and
A6: for n being set st n in NAT holds P[n,S.n] from CLASSES1:sch 1(A4);
A7: rng S c= bool the carrier of T
  proof
    let A be set;
    assume A in rng S;
    then consider n being set such that
A8: n in dom S & A = S.n by FUNCT_1:def 3;
    reconsider fsuccn = f.:succ n as Subset-Family of T by XBOOLE_1:1;
    meet fsuccn = meet (f.:succ n);
    then meet (f.:succ n) in bool the carrier of T;
    hence thesis by A5,A6,A8;
  end;
  then reconsider B = rng S as Subset-Family of T;
  reconsider B as Subset-Family of T;
A9: ex A being set st A in B
  proof
    take A = meet(f.:(succ 0));
    A = S.0 by A6;
    hence thesis by A5,FUNCT_1:def 3;
  end;
  then
A10: Intersect B = meet B by SETFAM_1:def 9;
  for A being set st A in B holds x in A
  proof
    let A be set;
    assume A in B;
    then consider n being set such that
A11: n in dom S and
A12: A = S.n by FUNCT_1:def 3;
    dom f = NAT & n in succ n by FUNCT_2:def 1,ORDINAL1:6;
    then
A13: f.n in f.:succ n by A5,A11,FUNCT_1:def 6;
A14: for A1 being set st A1 in f.:(succ n) holds x in A1
    proof
      let A1 be set;
      assume A1 in f.:(succ n);
      then consider m being set such that
A15:  m in dom f and
      m in succ n and
A16:  A1 = f.m by FUNCT_1:def 6;
      f.m in rng f by A15,FUNCT_1:def 3;
      then reconsider A2=A1 as Subset of T by A3,A16;
      reconsider A2 as Subset of T;
      A2 in B1 by A3,A15,A16,FUNCT_1:def 3;
      hence thesis by YELLOW_8:12;
    end;
    A = meet (f.:(succ n)) by A5,A6,A11,A12;
    hence thesis by A14,A13,SETFAM_1:def 1;
  end;
  then
A17: x in meet B by A9,SETFAM_1:def 1;
A18: B c= the topology of T
  proof
    let A be set;
    assume A in B;
    then consider n being set such that
A19: n in dom S and
A20: A = S.n by FUNCT_1:def 3;
    reconsider n9=n as Element of NAT by A5,A19;
    reconsider C=f.:succ n as Subset-Family of T by XBOOLE_1:1;
A21: C is open
    proof
      let P be Subset of T;
      assume P in C;
      hence thesis by YELLOW_8:12;
    end;
    succ(n9) is finite;
    then f.:(succ n) is finite;
    then
A22: meet C is open by A21,TOPS_2:20;
    A = meet (f.:succ n) by A5,A6,A19,A20;
    hence thesis by A22,PRE_TOPC:def 2;
  end;
  for O being Subset of T st O is open & x in O ex A being Subset of T st
  A in B & A c= O
  proof
    let O be Subset of T;
    assume O is open & x in O;
    then consider A1 being Subset of T such that
A23: A1 in B1 and
A24: A1 c= O by YELLOW_8:def 1;
    consider n being set such that
A25: n in dom f and
A26: A1 = f.n by A3,A23,FUNCT_1:def 3;
    S.n in rng S by A5,A25,FUNCT_1:def 3;
    then reconsider A = S.n as Subset of T by A7;
    reconsider A as Subset of T;
    take A;
    thus A in B by A5,A25,FUNCT_1:def 3;
    n in succ n by ORDINAL1:6;
    then f.n in f.:(succ n) by A25,FUNCT_1:def 6;
    then meet(f.:(succ n)) c= A1 by A26,SETFAM_1:3;
    then S.n c= A1 by A6,A25;
    hence thesis by A24,XBOOLE_1:1;
  end;
  then reconsider B as Basis of x by A18,A10,A17,TOPS_2:64,YELLOW_8:def 1;
  take B,S;
  thus dom S = NAT by A5;
  thus rng S = B;
  for n,m being Element of NAT st m >= n holds S.m c= S.n
  proof
    let n,m be Element of NAT;
    assume m >= n;
    then n + 1 <= m + 1 by XREAL_1:6;
    then n + 1 c= m + 1 by NAT_1:39;
    then succ n c= m +1 by NAT_1:38;
    then succ n c= succ m by NAT_1:38;
    then
A27: f.:(succ n) c= f.:(succ m) by RELAT_1:123;
    n in succ n & dom f = NAT by FUNCT_2:def 1,ORDINAL1:6;
    then f.n in f.:succ n by FUNCT_1:def 6;
    then meet (f.:succ m) c= meet (f.:succ n) by A27,SETFAM_1:6;
    then S.m c= meet (f.:succ n) by A6;
    hence thesis by A6;
  end;
  hence thesis;
end;

theorem
  for T being non empty TopSpace holds (for S being sequence of T holds
  for x1,x2 being Point of T holds (x1 in Lim S & x2 in Lim S implies x1=x2))
  implies T is T_1
proof
  let T be non empty TopSpace;
  assume
A1: for S being sequence of T holds for x1,x2 being Point of T holds (x1
  in Lim S & x2 in Lim S implies x1=x2);
  assume not T is T_1;
  then consider x1,x2 being Point of T,S being sequence of T such that
A2: S = (NAT --> x1) and
A3: x1 <> x2 and
A4: S is_convergent_to x2 by Lm3;
  S is_convergent_to x1 by A2,FRECHET:22;
  then
A5: x1 in Lim S by FRECHET:def 5;
  x2 in Lim S by A4,FRECHET:def 5;
  hence contradiction by A1,A3,A5;
end;

theorem Th6:
  for T being non empty TopSpace st T is T_2 holds for S being
sequence of T, x1,x2 being Point of T holds (x1 in Lim S & x2 in Lim S implies
  x1=x2)
proof
  let T be non empty TopSpace;
  assume
A1: T is T_2;
  assume not(for S being sequence of T, x1,x2 being Point of T holds (x1 in
  Lim S & x2 in Lim S implies x1=x2));
  then consider S being sequence of T such that
A2: ex x1,x2 being Point of T st x1 in Lim S & x2 in Lim S & x1<>x2;
  consider x1,x2 being Point of T such that
A3: x1 in Lim S and
A4: x2 in Lim S and
A5: x1<>x2 by A2;
  consider U1,U2 being Subset of T such that
A6: U1 is open and
A7: U2 is open and
A8: x1 in U1 and
A9: x2 in U2 and
A10: U1 misses U2 by A1,A5,PRE_TOPC:def 10;
  S is_convergent_to x1 by A3,FRECHET:def 5;
  then consider n1 being Element of NAT such that
A11: for m being Element of NAT st n1 <= m holds S.m in U1 by A6,A8,
FRECHET:def 3;
  S is_convergent_to x2 by A4,FRECHET:def 5;
  then consider n2 being Element of NAT such that
A12: for m being Element of NAT st n2 <= m holds S.m in U2 by A7,A9,
FRECHET:def 3;
  reconsider n = max(n1,n2) as Element of NAT;
A13: S.n in U1 by A11,XXREAL_0:25;
A14: S.n in U2 by A12,XXREAL_0:25;
  U1 /\ U2 = {} by A10,XBOOLE_0:def 7;
  hence contradiction by A13,A14,XBOOLE_0:def 4;
end;

theorem
  for T being non empty TopSpace st T is first-countable holds T is T_2
iff for S being sequence of T holds for x1,x2 being Point of T holds (x1 in Lim
  S & x2 in Lim S implies x1=x2)
proof
  let T be non empty TopSpace;
  assume
A1: T is first-countable;
  thus T is T_2 implies for S being sequence of T holds for x1,x2 being Point
  of T holds (x1 in Lim S & x2 in Lim S implies x1=x2) by Th6;
  assume
A2: for S being sequence of T holds for x1,x2 being Point of T holds (x1
  in Lim S & x2 in Lim S implies x1=x2);
  assume not T is T_2;
  then consider x1,x2 being Point of T such that
A3: x1 <> x2 and
A4: for U1,U2 being Subset of T st U1 is open & U2 is open & x1 in U1 &
  x2 in U2 holds U1 meets U2 by PRE_TOPC:def 10;
  consider B1 being Basis of x1 such that
A5: ex S being Function st dom S = NAT & rng S = B1 & for n,m being
  Element of NAT st m >= n holds S.m c= S.n by A1,Lm5;
  consider B2 being Basis of x2 such that
A6: ex S being Function st dom S = NAT & rng S = B2 & for n,m being
  Element of NAT st m >= n holds S.m c= S.n by A1,Lm5;
  consider S1 being Function such that
A7: dom S1 = NAT and
A8: rng S1 = B1 and
A9: for n,m being Element of NAT st m >= n holds S1.m c= S1.n by A5;
  consider S2 being Function such that
A10: dom S2 = NAT and
A11: rng S2 = B2 and
A12: for n,m being Element of NAT st m >= n holds S2.m c= S2.n by A6;
  defpred P[set,set] means $2 in S1.$1 /\ S2.$1;
A13: for n being set st n in NAT ex x being set st x in the carrier of T & P
  [n,x]
  proof
    let n be set;
    set x = the Element of S1.n /\ S2.n;
    assume
A14: n in NAT;
    then
A15: S1.n in B1 by A7,A8,FUNCT_1:def 3;
    then reconsider U1=S1.n as Subset of T;
A16: S2.n in B2 by A10,A11,A14,FUNCT_1:def 3;
    then reconsider U2=S2.n as Subset of T;
    take x;
    reconsider U1 as Subset of T;
    reconsider U2 as Subset of T;
A17: U2 is open & x2 in U2 by A16,YELLOW_8:12;
    U1 is open & x1 in U1 by A15,YELLOW_8:12;
    then U1 meets U2 by A4,A17;
    then
A18: U1 /\ U2 <> {} by XBOOLE_0:def 7;
    then x in U1 /\ U2;
    hence x in the carrier of T;
    thus thesis by A18;
  end;
  consider S being Function such that
A19: dom S = NAT & rng S c= the carrier of T and
A20: for n being set st n in NAT holds P[n,S.n] from FUNCT_1:sch 5(A13);
  reconsider S as Function of NAT,the carrier of T by A19,FUNCT_2:def 1
,RELSET_1:4;
  S is_convergent_to x2
  proof
    let U2 be Subset of T;
    assume U2 is open & x2 in U2;
    then consider V2 being Subset of T such that
A21: V2 in B2 and
A22: V2 c= U2 by YELLOW_8:13;
    consider n being set such that
A23: n in dom S2 and
A24: V2 = S2.n by A11,A21,FUNCT_1:def 3;
    reconsider n as Element of NAT by A10,A23;
    take n;
    let m be Element of NAT;
    S.m in S1.m /\ S2.m & S1.m /\ S2.m c= S2.m by A20,XBOOLE_1:17;
    then
A25: S.m in S2.m;
    assume n <= m;
    then S2.m c= S2.n by A12;
    then S.m in S2.n by A25;
    hence S.m in U2 by A22,A24;
  end;
  then
A26: x2 in Lim S by FRECHET:def 5;
  S is_convergent_to x1
  proof
    let U1 be Subset of T;
    assume U1 is open & x1 in U1;
    then consider V1 being Subset of T such that
A27: V1 in B1 and
A28: V1 c= U1 by YELLOW_8:13;
    consider n being set such that
A29: n in dom S1 and
A30: V1 = S1.n by A8,A27,FUNCT_1:def 3;
    reconsider n as Element of NAT by A7,A29;
    take n;
    let m be Element of NAT;
    S.m in S1.m /\ S2.m & S1.m /\ S2.m c= S1.m by A20,XBOOLE_1:17;
    then
A31: S.m in S1.m;
    assume n <= m;
    then S1.m c= S1.n by A9;
    then S.m in S1.n by A31;
    hence S.m in U1 by A28,A30;
  end;
  then x1 in Lim S by FRECHET:def 5;
  hence contradiction by A2,A3,A26;
end;

theorem
  for T being non empty TopStruct, S being sequence of T st S is
  not convergent holds Lim S = {}
proof
  let T be non empty TopStruct, S be sequence of T;
  assume
A1: S is not convergent;
  set x = the Element of Lim S;
  assume
A2: Lim S <> {};
  then x in Lim S;
  then reconsider x as Point of T;
  S is_convergent_to x by A2,FRECHET:def 5;
  hence contradiction by A1,FRECHET:def 4;
end;

theorem Th9:
  for T being non empty TopSpace,A being Subset of T holds A is
  closed implies for S being sequence of T st rng S c= A holds Lim S c= A
     by FRECHET:24;

theorem
  for T being non empty TopStruct,S being sequence of T, x being Point
  of T st not S is_convergent_to x holds ex S1 being subsequence of S st for S2
  being subsequence of S1 holds not S2 is_convergent_to x
proof
  let T be non empty TopStruct,S be sequence of T, x be Point of T;
  assume not S is_convergent_to x;
  then consider A being Subset of T such that
A1: A is open & x in A and
A2: for n being Element of NAT ex m being Element of NAT st n <= m & not
  S.m in A by FRECHET:def 3;
  defpred P[set] means not $1 in A;
A3: for n being Element of NAT ex m being Element of NAT st n <= m & P[S.m]
  by A2;
  consider S1 being subsequence of S such that
A4: for n being Element of NAT holds P[S1.n] from VALUED_1:sch 1(A3);
  take S1;
  let S2 be subsequence of S1;
  ex U1 being Subset of T st U1 is open & x in U1 & for n being Element of
  NAT ex m being Element of NAT st n <= m & not S2.m in U1
  proof
    take A;
    consider NS being increasing sequence of NAT such that
A5: S2=S1*NS by VALUED_0:def 17;
    thus A is open & x in A by A1;
    let n be Element of NAT;
    take n;
    thus n <= n;
    n in NAT;
    then n in dom S2 by NORMSP_1:12;
    then S2.n=S1.(NS.n) by A5,FUNCT_1:12;
    hence thesis by A4;
  end;
  hence thesis by FRECHET:def 3;
end;

begin ::The Continuous Maps

theorem Th11:
  for T1,T2 being non empty TopSpace, f being Function of T1,T2
holds f is continuous implies for S1 being sequence of T1, S2 being sequence of
  T2 st S2=f*S1 holds f.:(Lim S1) c= Lim S2
proof
  let T1,T2 be non empty TopSpace, f be Function of T1,T2;
  assume
A1: f is continuous;
  let S1 be sequence of T1, S2 be sequence of T2;
  assume
A2: S2=f*S1;
  let y be set;
  assume
A3: y in f.:(Lim S1);
  then reconsider y9=y as Point of T2;
  S2 is_convergent_to y9
  proof
    let U2 be Subset of T2;
    assume that
A4: U2 is open and
A5: y9 in U2;
    consider x being set such that
A6: x in dom f and
A7: x in Lim S1 and
A8: y = f.x by A3,FUNCT_1:def 6;
A9: x in f"U2 by A5,A6,A8,FUNCT_1:def 7;
    reconsider U1=f"U2 as Subset of T1;
    [#]T2 <> {};
    then
A10: U1 is open by A1,A4,TOPS_2:43;
    reconsider x as Point of T1 by A6;
    S1 is_convergent_to x by A7,FRECHET:def 5;
    then consider n being Element of NAT such that
A11: for m being Element of NAT st n <= m holds S1.m in f"U2 by A10,A9,
FRECHET:def 3;
    take n;
    let m be Element of NAT;
    assume n <= m;
    then S1.m in f"U2 by A11;
    then
A12: f.(S1.m) in U2 by FUNCT_1:def 7;
    dom S1 = NAT by FUNCT_2:def 1;
    hence S2.m in U2 by A2,A12,FUNCT_1:13;
  end;
  hence thesis by FRECHET:def 5;
end;

theorem
  for T1,T2 being non empty TopSpace, f being Function of T1,T2 st T1 is
  sequential holds f is continuous iff for S1 being sequence of T1, S2 being
  sequence of T2 st S2=f*S1 holds f.:(Lim S1) c= Lim S2
proof
  let T1,T2 be non empty TopSpace, f be Function of T1,T2;
  assume
A1: T1 is sequential;
  thus f is continuous implies for S1 being sequence of T1, S2 being sequence
  of T2 st S2=f*S1 holds f.:(Lim S1) c= Lim S2 by Th11;
  assume
A2: for S1 being sequence of T1, S2 being sequence of T2 st S2=f*S1
  holds f.:(Lim S1) c= Lim S2;
  let B be Subset of T2;
  reconsider A=f"B as Subset of T1;
  assume
A3: B is closed;
  for S being sequence of T1 st S is convergent & rng S c= A holds Lim S c= A
  proof
    reconsider B9=B as Subset of T2;
    let S be sequence of T1;
    assume that
    S is convergent and
A4: rng S c= A;
    set S2=f*S;
    rng S2 c= B9
    proof
      let z be set;
      assume z in rng S2;
      then consider n being set such that
A5:   n in dom S2 and
A6:   z = S2.n by FUNCT_1:def 3;
      dom S = NAT by NORMSP_1:12;
      then S.n in rng S by A5,FUNCT_1:def 3;
      then f.(S.n) in B by A4,FUNCT_1:def 7;
      hence thesis by A5,A6,FUNCT_1:12;
    end;
    then
A7: Lim S2 c= B9 by A3,Th9;
    let x be set;
A8: dom f = the carrier of T1 by FUNCT_2:def 1;
A9: f.:(Lim S) c= Lim S2 by A2;
    assume
A10: x in Lim S;
    then f.x in f.:(Lim S) by A8,FUNCT_1:def 6;
    then f.x in Lim S2 by A9;
    hence thesis by A10,A8,A7,FUNCT_1:def 7;
  end;
  hence thesis by A1,FRECHET:def 7;
end;

begin ::The Sequential Closure Operator

definition
  let T be non empty TopStruct, A be Subset of T;

  func Cl_Seq A -> Subset of T means
  :Def1:
  for x being Point of T holds x in
  it iff ex S being sequence of T st rng S c= A & x in Lim S;
  existence
  proof
    defpred P[Point of T] means ex S being sequence of T st rng S c=A & $1 in
    Lim S;
    reconsider X= {x where x is Point of T: P[x]} as Subset of T from DOMAIN_1
    :sch 7;
    reconsider X as Subset of T;
    take X;
    let x be Point of T;
    thus x in X implies ex S being sequence of T st rng S c= A & x in Lim S
    proof
      assume x in X;
      then
      ex x9 being Point of T st x=x9 & ex S being sequence of T st rng S c=
      A & x9 in Lim S;
      hence thesis;
    end;
    assume ex S being sequence of T st rng S c= A & x in Lim S;
    hence thesis;
  end;
  uniqueness
  proof
    let A1,A2 be Subset of T;
    assume that
A1: for x being Point of T holds x in A1 iff ex S being sequence of T
    st rng S c= A & x in Lim S and
A2: for x being Point of T holds x in A2 iff ex S being sequence of T
    st rng S c= A & x in Lim S;
    for x being Point of T holds x in A1 iff x in A2
    proof
      let x be Point of T;
      x in A1 iff ex S being sequence of T st rng S c= A & x in Lim S by A1;
      hence thesis by A2;
    end;
    hence thesis by SUBSET_1:3;
  end;
end;

theorem Th13:
  for T being non empty TopStruct, A being Subset of T, S being
  sequence of T, x being Point of T st rng S c= A & x in Lim S holds x in Cl(A)
proof
  let T be non empty TopStruct, A be Subset of T, S be sequence of T, x be
  Point of T;
  assume that
A1: rng S c= A and
A2: x in Lim S;
  for O being Subset of T st O is open holds x in O implies A meets O
  proof
    let O be Subset of T;
    assume
A3: O is open;
A4: S is_convergent_to x by A2,FRECHET:def 5;
    assume x in O;
    then consider n being Element of NAT such that
A5: for m being Element of NAT st n <= m holds S.m in O by A3,A4,FRECHET:def 3;
    n in NAT;
    then n in dom S by NORMSP_1:12;
    then
A6: S.n in rng S by FUNCT_1:def 3;
    S.n in O by A5;
    then S.n in A /\ O by A1,A6,XBOOLE_0:def 4;
    hence thesis by XBOOLE_0:def 7;
  end;
  hence thesis by PRE_TOPC:def 7;
end;

theorem Th14:
  for T being non empty TopStruct, A being Subset of T holds Cl_Seq(A) c= Cl(A)
proof
  let T be non empty TopStruct, A be Subset of T;
  let x be set;
  assume
A1: x in Cl_Seq(A);
  then reconsider x9=x as Point of T;
  ex S being sequence of T st rng S c= A & x9 in Lim S by A1,Def1;
  hence thesis by Th13;
end;

theorem Th15:
  for T being non empty TopStruct, S being sequence of T, S1 being
  subsequence of S, x being Point of T holds S is_convergent_to x implies S1
  is_convergent_to x
proof
  let T be non empty TopStruct, S be sequence of T, S1 be subsequence of S, x
  be Point of T;
  assume
A1: S is_convergent_to x;
  let U1 be Subset of T;
  assume U1 is open & x in U1;
  then consider n being Element of NAT such that
A2: for m being Element of NAT st n <= m holds S.m in U1 by A1,FRECHET:def 3;
  take n;
  let m be Element of NAT;
  assume
A3: n <= m;
  m in NAT;
  then
A4: m in dom S1 by NORMSP_1:12;
  consider NS being increasing sequence of NAT such that
A5: S1 = S * NS by VALUED_0:def 17;
  m <= NS.m by SEQM_3:14;
  then S.(NS.m) in U1 by A2,A3,XXREAL_0:2;
  hence S1.m in U1 by A5,A4,FUNCT_1:12;
end;

theorem Th16:
  for T being non empty TopStruct, S being sequence of T, S1 being
  subsequence of S holds Lim S c= Lim S1
proof
  let T be non empty TopStruct, S be sequence of T, S1 be subsequence of S;
  let x be set;
  assume
A1: x in Lim S;
  then reconsider x9=x as Point of T;
  S is_convergent_to x9 by A1,FRECHET:def 5;
  then S1 is_convergent_to x9 by Th15;
  hence thesis by FRECHET:def 5;
end;

theorem Th17:
  for T being non empty TopStruct holds Cl_Seq({}T) = {}
proof
  let T be non empty TopStruct;
  set x = the Element of Cl_Seq({}T);
  assume
A1: Cl_Seq({}T) <> {};
  then x in Cl_Seq({}T);
  then reconsider x as Point of T;
  consider S being sequence of T such that
A2: rng S c= {}T and
  x in Lim S by A1,Def1;
  rng S = {} by A2;
  then dom S = {} by RELAT_1:42;
  hence contradiction by NORMSP_1:12;
end;

theorem Th18:
  for T being non empty TopStruct, A being Subset of T holds A c= Cl_Seq(A)
proof
  let T be non empty TopStruct, A be Subset of T;
  let x be set;
  assume
A1: x in A;
  then reconsider x9=x as Point of T;
  ex S being sequence of T st rng S c= A & x9 in Lim S
  proof
    set S = NAT --> x9;
    take S;
    {x9} c= A
    proof
      let x99 be set;
      assume x99 in {x9};
      hence thesis by A1,TARSKI:def 1;
    end;
    hence rng S c= A by FUNCOP_1:8;
    S is_convergent_to x9 by FRECHET:22;
    hence thesis by FRECHET:def 5;
  end;
  hence thesis by Def1;
end;

theorem Th19:
  for T being non empty TopStruct, A,B being Subset of T holds
  Cl_Seq(A) \/ Cl_Seq(B) = Cl_Seq(A \/ B)
proof
  let T be non empty TopStruct, A,B be Subset of T;
  thus Cl_Seq(A) \/ Cl_Seq(B) c= Cl_Seq(A \/ B)
  proof
    let x be set;
    assume
A1: x in Cl_Seq(A) \/ Cl_Seq(B);
    per cases by A1,XBOOLE_0:def 3;
    suppose
A2:   x in Cl_Seq(A);
      then reconsider x9=x as Point of T;
      consider S being sequence of T such that
A3:   rng S c= A and
A4:   x9 in Lim S by A2,Def1;
      A c= A \/ B by XBOOLE_1:7;
      then rng S c= A \/ B by A3,XBOOLE_1:1;
      hence thesis by A4,Def1;
    end;
    suppose
A5:   x in Cl_Seq(B);
      then reconsider x9=x as Point of T;
      consider S being sequence of T such that
A6:   rng S c= B and
A7:   x9 in Lim S by A5,Def1;
      B c= A \/ B by XBOOLE_1:7;
      then rng S c= A \/ B by A6,XBOOLE_1:1;
      hence thesis by A7,Def1;
    end;
  end;
  thus Cl_Seq(A \/ B) c= Cl_Seq(A) \/ Cl_Seq(B)
  proof
    let x be set;
    assume
A8: x in Cl_Seq(A \/ B);
    then reconsider x9 = x as Point of T;
    consider S being sequence of T such that
A9: rng S c= A \/ B and
A10: x9 in Lim S by A8,Def1;
    consider S1 being subsequence of S such that
A11: rng S1 c= A or rng S1 c= B by A9,Th4;
A12: Lim S c= Lim S1 by Th16;
    per cases by A11;
    suppose
      rng S1 c= A;
      then x9 in Cl_Seq(A) by A10,A12,Def1;
      hence thesis by XBOOLE_0:def 3;
    end;
    suppose
      rng S1 c= B;
      then x9 in Cl_Seq(B) by A10,A12,Def1;
      hence thesis by XBOOLE_0:def 3;
    end;
  end;
end;

theorem Th20:
  for T being non empty TopStruct holds T is Frechet iff for A
  being Subset of T holds Cl(A)=Cl_Seq(A)
proof
  let T be non empty TopStruct;
  thus T is Frechet implies for A being Subset of T holds Cl(A)=Cl_Seq(A)
  proof
    assume
A1: T is Frechet;
    let A be Subset of T;
    reconsider A9=A as Subset of T;
    thus Cl(A)c=Cl_Seq(A)
    proof
      let x be set;
      assume
A2:   x in Cl(A);
      then reconsider x9=x as Point of T;
      ex S being sequence of T st rng S c= A9 & x9 in Lim S by A1,A2,
FRECHET:def 6;
      hence thesis by Def1;
    end;
    thus thesis by Th14;
  end;
  assume
A3: for A being Subset of T holds Cl(A)=Cl_Seq(A);
  let A be Subset of T,x be Point of T;
  assume x in Cl(A);
  then x in Cl_Seq(A) by A3;
  hence thesis by Def1;
end;

theorem Th21:
  for T being non empty TopSpace st T is Frechet holds for A,B
  being Subset of T holds Cl_Seq({}T) = {} & A c= Cl_Seq(A) & Cl_Seq(A \/ B) =
  Cl_Seq(A) \/ Cl_Seq(B) & Cl_Seq(Cl_Seq(A)) = Cl_Seq(A)
proof
  let T be non empty TopSpace;
  assume
A1: T is Frechet;
  let A,B be Subset of T;
  thus Cl_Seq({}T) = {} & A c= Cl_Seq(A) & Cl_Seq(A \/ B)=Cl_Seq(A) \/ Cl_Seq(
  B) by Th17,Th18,Th19;
  thus Cl_Seq(Cl_Seq(A)) = Cl_Seq(Cl(A)) by A1,Th20
    .= Cl(Cl(A)) by A1,Th20
    .= Cl_Seq(A) by A1,Th20;
end;

theorem Th22:
  for T being non empty TopSpace st T is sequential holds (for A
  being Subset of T holds Cl_Seq(Cl_Seq(A)) = Cl_Seq(A)) implies T is Frechet
proof
  let T be non empty TopSpace;
  assume
A1: T is sequential;
  assume
A2: for A being Subset of T holds Cl_Seq(Cl_Seq(A)) = Cl_Seq(A);
  assume not T is Frechet;
  then consider A being Subset of T such that
A3: ex x being Point of T st x in Cl(A) & for S being sequence of T
  holds (rng S c= A implies not x in Lim S ) by FRECHET:def 6;
  for Sq being sequence of T st Sq is convergent & rng Sq c= Cl_Seq(A)
  holds Lim Sq c= Cl_Seq(A)
  proof
    let Sq be sequence of T;
    assume that
    Sq is convergent and
A4: rng Sq c= Cl_Seq(A);
    let y be set;
    assume
A5: y in Lim Sq;
    then reconsider y9=y as Point of T;
    y9 in Cl_Seq(Cl_Seq(A)) by A4,A5,Def1;
    hence thesis by A2;
  end;
  then
A6: Cl_Seq(A) is closed by A1,FRECHET:def 7;
  consider x being Point of T such that
A7: x in Cl(A) and
A8: for S being sequence of T holds (rng S c= A implies not x in Lim S ) by A3;
  A c= Cl_Seq(A) by Th18;
  then x in Cl_Seq(A) by A7,A6,PRE_TOPC:15;
  hence contradiction by A8,Def1;
end;

theorem
  for T being non empty TopSpace st T is sequential holds T is Frechet
iff for A,B being Subset of T holds Cl_Seq({}T) = {} & A c= Cl_Seq(A) & Cl_Seq(
A \/ B) = Cl_Seq(A) \/ Cl_Seq(B) & Cl_Seq(Cl_Seq(A)) = Cl_Seq(A) by Th21,Th22;

begin ::The Limit

definition
  let T be non empty TopSpace, S be sequence of T;
  assume
A1: ex x being Point of T st Lim S = {x};
  func lim S -> Point of T means
  :Def2:
  S is_convergent_to it;
  existence
  proof
    consider x being Point of T such that
A2: Lim S = {x} by A1;
    take x;
    x in {x} by TARSKI:def 1;
    hence thesis by A2,FRECHET:def 5;
  end;
  uniqueness
  proof
    let x1,x2 be Point of T;
    assume that
A3: S is_convergent_to x1 and
A4: S is_convergent_to x2;
    consider x being Point of T such that
A5: Lim S = {x} by A1;
A6: x2 in {x} by A4,A5,FRECHET:def 5;
    x1 in Lim S by A3,FRECHET:def 5;
    then x1=x by A5,TARSKI:def 1;
    hence thesis by A6,TARSKI:def 1;
  end;
end;

theorem Th24:
  for T being non empty TopSpace st T is T_2 for S being sequence
  of T st S is convergent holds ex x being Point of T st Lim S = {x}
proof
  let T be non empty TopSpace;
  assume
A1: T is T_2;
  let S be sequence of T;
  assume S is convergent;
  then consider x being Point of T such that
A2: S is_convergent_to x by FRECHET:def 4;
  take x;
A3: x in Lim S by A2,FRECHET:def 5;
  thus Lim S c= {x}
  proof
    let y be set;
    assume
A4: y in Lim S;
    then reconsider y9=y as Point of T;
    y9=x by A1,A3,A4,Th6;
    hence thesis by TARSKI:def 1;
  end;
  let y be set;
  assume y in {x};
  hence thesis by A3,TARSKI:def 1;
end;

theorem Th25:
  for T being non empty TopSpace st T is T_2 for S being sequence
  of T,x being Point of T holds S is_convergent_to x iff S is convergent & x =
  lim S
proof
  let T be non empty TopSpace;
  assume
A1: T is T_2;
  let S be sequence of T, x be Point of T;
  thus S is_convergent_to x implies S is convergent & x = lim S
  proof
    assume
A2: S is_convergent_to x;
    hence S is convergent by FRECHET:def 4;
    then ex y being Point of T st Lim S = {y} by A1,Th24;
    hence thesis by A2,Def2;
  end;
  assume that
A3: S is convergent and
A4: x = lim S;
  ex x being Point of T st Lim S = {x} by A1,A3,Th24;
  hence thesis by A4,Def2;
end;

theorem
  for M being MetrStruct,S being sequence of M holds S is sequence of
  TopSpaceMetr(M)
proof
  let M be MetrStruct,S be sequence of M;
  the carrier of M = the carrier of TopSpaceMetr M by TOPMETR:12;
  hence thesis;
end;

theorem
  for M being non empty MetrStruct,S being sequence of TopSpaceMetr(M)
  holds S is sequence of M by TOPMETR:12;

theorem Th28:
  for M being non empty MetrSpace,S being sequence of M, x being
  Point of M, S9 being sequence of TopSpaceMetr(M), x9 being Point of
TopSpaceMetr(M) st S = S9 & x = x9 holds S is_convergent_in_metrspace_to x iff
  S9 is_convergent_to x9
proof
  let M be non empty MetrSpace,S be sequence of M, x be Point of M, S9 be
  sequence of TopSpaceMetr(M), x9 be Point of TopSpaceMetr(M);
  assume that
A1: S = S9 and
A2: x=x9;
  thus S is_convergent_in_metrspace_to x implies S9 is_convergent_to x9
  proof
    assume
A3: S is_convergent_in_metrspace_to x;
    let U1 be Subset of TopSpaceMetr(M);
    assume U1 is open & x9 in U1;
    then consider r being real number such that
A4: r>0 and
A5: Ball(x,r) c= U1 by A2,TOPMETR:15;
    reconsider r as Real by XREAL_0:def 1;
    Ball(x,r) contains_almost_all_sequence S by A3,A4,METRIC_6:15;
    then consider n being Element of NAT such that
A6: for m being Element of NAT st n <= m holds S.m in Ball(x,r) by
METRIC_6:def 5;
    take n;
    let m be Element of NAT;
    assume n <= m;
    then S.m in Ball(x,r) by A6;
    hence S9.m in U1 by A1,A5;
  end;
  assume
A7: S9 is_convergent_to x9;
  for V being Subset of M st x in V & V in Family_open_set M holds V
  contains_almost_all_sequence S
  proof
    let V be Subset of M;
    assume that
A8: x in V and
A9: V in Family_open_set M;
    reconsider V9=V as Subset of TopSpaceMetr(M) by TOPMETR:12;
    reconsider V9 as Subset of TopSpaceMetr(M);
    V9 in the topology of TopSpaceMetr(M) by A9,TOPMETR:12;
    then V9 is open by PRE_TOPC:def 2;
    then consider n being Element of NAT such that
A10: for m being Element of NAT st n <= m holds S9.m in V9 by A2,A7,A8,
FRECHET:def 3;
    take n;
    let m be Element of NAT;
    assume n <= m;
    hence thesis by A1,A10;
  end;
  hence thesis by METRIC_6:17;
end;

theorem
  for M being non empty MetrSpace,Sm being sequence of M, St being
  sequence of TopSpaceMetr(M) st Sm=St holds Sm is convergent iff St is
  convergent
proof
  let M be non empty MetrSpace,Sm be sequence of M, St be sequence of
  TopSpaceMetr(M);
  assume
A1: Sm=St;
  thus Sm is convergent implies St is convergent
  proof
    assume Sm is convergent;
    then consider x being Point of M such that
A2: Sm is_convergent_in_metrspace_to x by METRIC_6:10;
    reconsider x9=x as Point of TopSpaceMetr(M) by TOPMETR:12;
    St is_convergent_to x9 by A1,A2,Th28;
    hence thesis by FRECHET:def 4;
  end;
  assume St is convergent;
  then consider x9 being Point of TopSpaceMetr(M) such that
A3: St is_convergent_to x9 by FRECHET:def 4;
  reconsider x=x9 as Point of M by TOPMETR:12;
  Sm is_convergent_in_metrspace_to x by A1,A3,Th28;
  hence thesis by METRIC_6:9;
end;

theorem
  for M being non empty MetrSpace,Sm being sequence of M, St being
  sequence of TopSpaceMetr(M) st Sm=St & Sm is convergent holds lim Sm = lim St
proof
  let M be non empty MetrSpace,Sm be sequence of M, St be sequence of
  TopSpaceMetr(M);
  assume that
A1: Sm=St and
A2: Sm is convergent;
  set x=lim Sm;
  reconsider x9=x as Point of TopSpaceMetr(M) by TOPMETR:12;
  Sm is_convergent_in_metrspace_to x by A2,METRIC_6:12;
  then TopSpaceMetr(M) is T_2 & St is_convergent_to x9 by A1,Th28,PCOMPS_1:34;
  hence thesis by Th25;
end;

begin ::The Cluster Points

definition
  let T be TopStruct, S be sequence of T, x be Point of T;
  pred x is_a_cluster_point_of S means
  :Def3:
  for O being Subset of T, n being
Element of NAT st O is open & x in O ex m being Element of NAT st n <= m & S.m
  in O;
end;

theorem Th31:
  for T being non empty TopStruct, S being sequence of T, x being
  Point of T st ex S1 being subsequence of S st S1 is_convergent_to x holds x
  is_a_cluster_point_of S
proof
  let T be non empty TopStruct, S be sequence of T, x be Point of T;
  given S1 being subsequence of S such that
A1: S1 is_convergent_to x;
  let O be Subset of T, n be Element of NAT;
  assume O is open & x in O;
  then consider n1 being Element of NAT such that
A2: for m being Element of NAT st n1 <= m holds S1.m in O by A1,FRECHET:def 3;
  set n2=max(n1,n);
A3: S1.n2 in O by A2,XXREAL_0:25;
  consider NS being increasing sequence of NAT such that
A4: S1 = S * NS by VALUED_0:def 17;
  take NS.n2;
  n <= n2 & n2 <= NS.n2 by SEQM_3:14,XXREAL_0:25;
  hence n <= NS.n2 by XXREAL_0:2;
  n2 in NAT;
  then n2 in dom NS by FUNCT_2:def 1;
  hence thesis by A4,A3,FUNCT_1:13;
end;

theorem
  for T being non empty TopStruct, S being sequence of T, x being Point
  of T st S is_convergent_to x holds x is_a_cluster_point_of S
proof
  let T be non empty TopStruct, S be sequence of T, x be Point of T;
  assume
A1: S is_convergent_to x;
  ex S1 being subsequence of S st S1 is_convergent_to x
  proof
    reconsider S1=S as subsequence of S by VALUED_0:19;
    take S1;
    thus thesis by A1;
  end;
  hence thesis by Th31;
end;

theorem Th33:
  for T being non empty TopStruct, S being sequence of T, x being
Point of T, Y being Subset of T st Y = {y where y is Point of T : x in Cl({y})
  } & rng S c= Y holds S is_convergent_to x
proof
  let T be non empty TopStruct, S be sequence of T, x be Point of T, Y be
  Subset of T;
  assume that
A1: Y = {y where y is Point of T : x in Cl({y}) } and
A2: rng S c= Y;
  let U1 be Subset of T;
  assume
A3: U1 is open & x in U1;
  take 0;
  let m be Element of NAT;
  m in NAT;
  then m in dom S by NORMSP_1:12;
  then S.m in rng S by FUNCT_1:def 3;
  then S.m in Y by A2;
  then consider y being Point of T such that
A4: y=S.m and
A5: x in Cl({y}) by A1;
  assume 0 <= m;
  {y} meets U1 by A3,A5,PRE_TOPC:def 7;
  hence S.m in U1 by A4,ZFMISC_1:50;
end;

theorem Th34:
  for T being non empty TopStruct, S being sequence of T, x,y
  being Point of T st for n being Element of NAT holds S.n = y & S
  is_convergent_to x holds x in Cl({y})
proof
  let T be non empty TopStruct, S be sequence of T, x,y be Point of T;
  assume
A1: for n being Element of NAT holds S.n = y & S is_convergent_to x;
  for G being Subset of T st G is open holds x in G implies {y} meets G
  proof
    let G be Subset of T;
    assume
A2: G is open;
    assume x in G;
    then consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds S.m in G by A1,A2,FRECHET:def 3;
    S.n in G by A3;
    then
A4: y in G by A1;
    y in {y} by TARSKI:def 1;
    then y in {y} /\ G by A4,XBOOLE_0:def 4;
    hence thesis by XBOOLE_0:def 7;
  end;
  hence thesis by PRE_TOPC:def 7;
end;

theorem Th35:
  for T being non empty TopStruct, x being Point of T, Y being
Subset of T, S being sequence of T st Y = { y where y is Point of T : x in Cl({
  y}) } & rng S misses Y & S is_convergent_to x ex S1 being subsequence of S st
  S1 is one-to-one
proof
  let T be non empty TopStruct, x be Point of T, Y be Subset of T, S be
  sequence of T;
  assume that
A1: Y = { y where y is Point of T : x in Cl({y}) } and
A2: rng S /\ Y = {} and
A3: S is_convergent_to x;
  defpred P[Element of NAT,set,set] means $3 in NAT & for n1,n2,m being
  Element of NAT st n1=$2 & n2=$3 & n2 <= m holds S.m <> S.n1;
A4: for z being set st z in rng S ex n0 being Element of NAT st for m being
  Element of NAT st n0 <= m holds z <> S.m
  proof
    let z be set;
    defpred P[set] means $1 = z;
    assume
A5: z in rng S;
    then reconsider z9=z as Point of T;
    assume
    for n0 being Element of NAT ex m being Element of NAT st n0 <= m & z = S.m;
    then
A6: for n being Element of NAT ex m being Element of NAT st n <= m & P[S.m ];
    ex S1 being subsequence of S st for n being Element of NAT holds P[S1.n
    ] from VALUED_1:sch 1(A6 );
    then x in Cl({z9}) by A3,Th15,Th34;
    then z9 in Y by A1;
    hence contradiction by A2,A5,XBOOLE_0:def 4;
  end;
A7: for n being Element of NAT for z1 being set ex z2 being set st P[n,z1, z2]
  proof
    let n be Element of NAT, z1 be set;
    per cases;
    suppose
A8:   not z1 in NAT;
      take 0;
      thus 0 in NAT;
      let n1,n2,m be Element of NAT;
      assume that
A9:   n1=z1 and
      n2=0 and
      n2 <= m;
      thus thesis by A8,A9;
    end;
    suppose
      z1 in NAT;
      then z1 in dom S by NORMSP_1:12;
      then S.z1 in rng S by FUNCT_1:def 3;
      then consider n0 being Element of NAT such that
A10:  for m being Element of NAT st n0 <= m holds S.z1 <> S.m by A4;
      take n0;
      thus n0 in NAT;
      let n1,n2,m be Element of NAT;
      assume n1=z1 & n2=n0 & n2 <= m;
      hence thesis by A10;
    end;
  end;
  consider f being Function such that
A11: dom f = NAT and
A12: f.0 = 0 and
A13: for n being Element of NAT holds P[n,f.n,f.(n+1)] from RECDEF_1:sch
  1(A7);
A14: for n being Element of NAT holds f.n is Element of NAT
  proof
    let n be Element of NAT;
    per cases;
    suppose
      n = 0;
      hence thesis by A12;
    end;
    suppose
      n <> 0;
      then 0 < n by NAT_1:3;
      then 0 + 1 < n + 1 by XREAL_1:6;
      then 1 <= n by NAT_1:13;
      then reconsider n1=n-1 as Element of NAT by INT_1:5;
      n1 + 1 = n;
      hence thesis by A13;
    end;
  end;
  then for n be Element of NAT holds f.n is real;
  then reconsider f as Real_Sequence by A11,SEQ_1:2;
  f is increasing
  proof
    let n be Element of NAT;
    reconsider n2=f.(n+1) as Element of NAT by A14;
    reconsider n1=f.n as Element of NAT by A14;
    assume f.n >= f.(n+1);
    then n2 <= n1;
    then S.n1 <> S.n1 by A13;
    hence contradiction;
  end;
  then reconsider f as increasing sequence of NAT by A14,SEQM_3:13;
  take S1=S*f;
A15: for n1,n2 being Element of NAT st n1 < n2 holds S1.n1 <> S1.n2
  proof
    let n1,n2 be Element of NAT;
    reconsider n19=f.n1 as Element of NAT;
    n2 in NAT;
    then n2 in dom S1 by NORMSP_1:12;
    then
A16: S.(f.n2) = S1.n2 by FUNCT_1:12;
    assume n1 < n2;
    then
A17: n1 + 1 <= n2 by NAT_1:13;
    f.(n1+1) <= f.n2
    proof
      per cases;
      suppose
        n1+1 = n2;
        hence thesis;
      end;
      suppose
        n1 + 1 <> n2;
        then n1 + 1 < n2 by A17,XXREAL_0:1;
        hence thesis by SEQM_3:1;
      end;
    end;
    then
A18: S.(f.n2) <> S.n19 by A13;
    n1 in NAT;
    then n1 in dom S1 by NORMSP_1:12;
    hence thesis by A18,A16,FUNCT_1:12;
  end;
  let x1,x2 be set;
  assume that
A19: x1 in dom S1 and
A20: x2 in dom S1 and
A21: S1.x1 = S1.x2;
  reconsider n2=x2 as Element of NAT by A20;
  reconsider n1=x1 as Element of NAT by A19;
  assume
A22: x1 <> x2;
  per cases by A22,XXREAL_0:1;
  suppose
    n1 < n2;
    hence contradiction by A21,A15;
  end;
  suppose
    n2 < n1;
    hence contradiction by A21,A15;
  end;
end;

theorem Th36:
  for T being non empty TopStruct, S1,S2 being sequence of T st
  rng S2 c= rng S1 & S2 is one-to-one ex P being Permutation of NAT st S2*P is
  subsequence of S1
proof
  let T be non empty TopStruct, S1,S2 be sequence of T;
  assume that
A1: rng S2 c= rng S1 and
A2: S2 is one-to-one;
  defpred P[set,set] means S2.$1=S1.$2;
A3: for n being set st n in NAT ex u being set st u in NAT & P[n,u]
  proof
    let n be set;
    assume n in NAT;
    then n in dom S2 by NORMSP_1:12;
    then S2.n in rng S2 by FUNCT_1:def 3;
    then consider m being set such that
A4: m in dom S1 and
A5: S2.n = S1.m by A1,FUNCT_1:def 3;
    take m;
    thus m in NAT by A4;
    thus thesis by A5;
  end;
  consider f being Function such that
A6: dom f = NAT and
A7: rng f c= NAT and
A8: for n being set st n in NAT holds P[n,f.n] from FUNCT_1:sch 5(A3);
  reconsider A=rng f as non empty Subset of NAT by A6,A7,RELAT_1:42;
  defpred P[Element of NAT,set,set] means for B being non empty Subset of NAT,
m being Element of NAT st m=$2 & B={k where k is Element of NAT:k in rng f & k>
  m} holds $3=min B;
A9: f is one-to-one
  proof
    let x1,x2 be set;
    assume that
A10: x1 in dom f and
A11: x2 in dom f and
A12: f.x1 = f.x2;
    S2.x2 = S1.(f.x2) by A6,A8,A11;
    then
A13: S2.x1 = S2.x2 by A6,A8,A10,A12;
    x1 in dom S2 & x2 in dom S2 by A6,A10,A11,NORMSP_1:12;
    hence thesis by A2,A13,FUNCT_1:def 4;
  end;
A14: for m being Element of NAT holds {k where k is Element of NAT : k in
  rng f & k>m} <> {}
  proof
    let m be Element of NAT;
    assume
A15: {k where k is Element of NAT : k in rng f & k>m} = {};
    rng f c= m + 1
    proof
      let x be set;
      assume
A16:  x in rng f;
      then reconsider x9=x as Element of NAT by A7;
      x9 < m + 1
      proof
        assume x9>= m + 1;
        then x9 > m by NAT_1:13;
        then x9 in {k where k is Element of NAT : k in rng f & k>m} by A16;
        hence contradiction by A15;
      end;
      then x9 in {x99 where x99 is Element of NAT:x99< m+1};
      hence thesis by AXIOMS:4;
    end;
    then rng f is finite;
    hence contradiction by A6,A9,CARD_1:59;
  end;
A17: for m being Element of NAT holds {k where k is Element of NAT : k in
  rng f & k>m} c= NAT
  proof
    let m be Element of NAT;
    let z be set;
    assume z in {k where k is Element of NAT : k in rng f & k>m};
    then ex k being Element of NAT st k = z & k in rng f & k>m;
    hence thesis;
  end;
A18: for n being Element of NAT for x being set ex y being set st P[n,x,y]
  proof
    let n be Element of NAT, x be set;
    per cases;
    suppose
      x in NAT;
      then reconsider x9=x as Element of NAT;
      set B={k where k is Element of NAT:k in rng f & k>x9};
      reconsider B as Subset of NAT by A17;
      reconsider B as non empty Subset of NAT by A14;
      take min B;
      let B9 be non empty Subset of NAT, m be Element of NAT;
      assume m=x & B9={k where k is Element of NAT:k in rng f & k>m};
      hence thesis;
    end;
    suppose
A19:  not x in NAT;
      take 0;
      let B be non empty Subset of NAT, m be Element of NAT;
      assume that
A20:  m=x and
      B={k where k is Element of NAT:k in rng f & k>m};
      thus thesis by A19,A20;
    end;
  end;
  consider g being Function such that
A21: dom g = NAT and
A22: g.0 = min A and
A23: for n being Element of NAT holds P[n,g.n,g.(n+1)] from RECDEF_1:sch
  1(A18);
  defpred P[Element of NAT] means g.$1 in NAT;
A24: for k being Element of NAT st P[k] holds P[k+1]
  proof
    let k be Element of NAT;
    assume g.k in NAT;
    then reconsider m=g.k as Element of NAT;
    set B={l where l is Element of NAT:l in rng f & l>m};
    reconsider B as Subset of NAT by A17;
    reconsider B as non empty Subset of NAT by A14;
    g.(k+1)= min B by A23;
    hence thesis;
  end;
A25: P[0] by A22;
A26: for k being Element of NAT holds P[k] from NAT_1:sch 1(A25,A24);
  for n being Element of NAT holds g.n is real
  proof
    let n be Element of NAT;
    g.n in NAT by A26;
    then reconsider w = g.n as Element of REAL;
    w is real;
    hence thesis;
  end;
  then reconsider g1=g as Real_Sequence by A21,SEQ_1:2;
A27: g1 is increasing
  proof
    let n be Element of NAT;
    reconsider m=g.n as Element of NAT by A26;
    reconsider B={k where k is Element of NAT : k in rng f & k>m} as non empty
    Subset of NAT by A14,A17;
    g1.(n+1)=min B by A23;
    then g1.(n+1) in B by XXREAL_2:def 7;
    then ex k being Element of NAT st k = g1.(n+1) & k in rng f & k>m;
    hence thesis;
  end;
A28: rng g c= NAT
  proof
    let y be set;
    assume y in rng g;
    then consider x being set such that
A29: x in dom g and
A30: y = g.x by FUNCT_1:def 3;
    reconsider x as Element of NAT by A21,A29;
    g.x in NAT by A26;
    hence thesis by A30;
  end;
  then reconsider g1 as increasing sequence of NAT by A21,A27,RELSET_1:4;
A31: g1 is one-to-one
  proof
    let x1,x2 be set;
    assume that
A32: x1 in dom g1 and
A33: x2 in dom g1 and
A34: g1.x1 = g1.x2;
    reconsider n2=x2 as Element of NAT by A33;
    reconsider n1=x1 as Element of NAT by A32;
    assume
A35: x1 <> x2;
    per cases by A35,XXREAL_0:1;
    suppose
      n1 < n2;
      hence contradiction by A34,SEQM_3:1;
    end;
    suppose
      n2 < n1;
      hence contradiction by A34,SEQM_3:1;
    end;
  end;
  then
A36: rng(g") = NAT by A21,FUNCT_1:33;
A37: rng f = rng g
  proof
    thus for y being set holds y in rng f implies y in rng g
    proof
      let y be set;
      assume
A38:  y in rng f;
      then reconsider y9=y as Element of NAT by A7;
      defpred P[Element of NAT] means g1.$1 < y9;
      assume
A39:  not y in rng g;
A40:  for n being Element of NAT st P[n] holds P[n+1]
      proof
        let n be Element of NAT;
        reconsider m = g.n as Element of NAT by A26;
        reconsider B={k where k is Element of NAT:k in rng f & k>m} as non
        empty Subset of NAT by A14,A17;
A41:    g.(n+1)=min B & g.(n+1) in rng g by A21,A23,FUNCT_1:def 3;
        assume g1.n < y9;
        then y9 in {k where k is Element of NAT:k in rng f & k>m} by A38;
        then
A42:    min B <= y9 by XXREAL_2:def 7;
        assume not g1.(n+1) < y9;
        hence contradiction by A39,A42,A41,XXREAL_0:1;
      end;
A43:  P[0]
      proof
        assume
A44:    not g1.0 < y9;
        min A <= y9 & g.0 in rng g by A21,A38,FUNCT_1:def 3,XXREAL_2:def 7;
        hence contradiction by A22,A39,A44,XXREAL_0:1;
      end;
A45:  for n being Element of NAT holds P[n] from NAT_1:sch 1(A43,A40);
      rng g c= y9
      proof
        let y be set;
        assume y in rng g;
        then consider x being set such that
A46:    x in dom g and
A47:    y = g.x by FUNCT_1:def 3;
        reconsider x as Element of NAT by A21,A46;
        g1.x < y9 by A45;
        then g1.x in {i where i is Element of NAT:i<y9};
        hence thesis by A47,AXIOMS:4;
      end;
      then rng g is finite;
      hence contradiction by A21,A31,CARD_1:59;
    end;
    let y be set;
    assume y in rng g;
    then consider x being set such that
A48: x in dom g and
A49: y = g.x by FUNCT_1:def 3;
    reconsider n=x as Element of NAT by A21,A48;
    per cases;
    suppose
      n=0;
      hence thesis by A22,A49,XXREAL_2:def 7;
    end;
    suppose
      n<>0;
      then n > 0 by NAT_1:3;
      then n + 1 > 0 + 1 by XREAL_1:6;
      then 1 <= n by NAT_1:13;
      then reconsider m=n-1 as Element of NAT by INT_1:5;
      reconsider l = g.m as Element of NAT by A26;
      reconsider B={k where k is Element of NAT:k in rng f & k>l} as non empty
      Subset of NAT by A14,A17;
      m+1 = n;
      then g.n = min B by A23;
      then y in B by A49,XXREAL_2:def 7;
      then ex k being Element of NAT st k = y & k in rng f & k>l;
      hence thesis;
    end;
  end;
  then
A50: rng f = dom(g") by A31,FUNCT_1:33;
  then dom(g"*f) = dom f & rng(g"*f) = rng(g") by RELAT_1:27,28;
  then reconsider P=g"*f as Function of NAT,NAT by A6,A36,FUNCT_2:def 1
,RELSET_1:4;
  rng(g") = dom g by A31,FUNCT_1:33;
  then rng P = NAT by A21,A50,RELAT_1:28;
  then P is onto by FUNCT_2:def 3;
  then reconsider P as Permutation of NAT by A9,A31;
  take P";
  NAT = dom (S2*P") & NAT = dom (S1*g) & for x being set st x in NAT
  holds (S2*P").x = (S1*g).x
  proof
    thus NAT = dom (S2*(P")) by FUNCT_2:def 1;
    rng g c= dom S1 by A28,NORMSP_1:12;
    hence NAT = dom (S1*g) by A21,RELAT_1:27;
    let x be set;
    assume
A51: x in NAT;
    then
A52: g. x in rng g by A21,FUNCT_1:def 3;
    then
A53: f".(g.x) in dom f by A9,A37,FUNCT_1:32;
    dom (P") = NAT by FUNCT_2:def 1;
    hence (S2*(P")).x = S2.(((g"*f)").x) by A51,FUNCT_1:13
      .= S2.((f"*(g")").x) by A9,A31,FUNCT_1:44
      .= S2.((f"*g).x) by A31,FUNCT_1:43
      .= S2.(f".(g.x)) by A21,A51,FUNCT_1:13
      .= S1.(f.(f".(g.x))) by A6,A8,A53
      .= S1.(g.x) by A9,A37,A52,FUNCT_1:35
      .= (S1*g).x by A21,A51,FUNCT_1:13;
  end;
  then S2*(P")=S1*g1 by FUNCT_1:2;
  hence thesis;
end;

scheme
  PermSeq {T()->non empty 1-sorted,S()->sequence of T(),p()->Permutation of
NAT, P[set]} : ex n being Element of NAT st for m being Element of NAT st n<=m
  holds P[(S()*p()).m]
provided
A1: ex n being Element of NAT st for m being Element of NAT, x being
Point of T() st n<=m & x=S().m holds P[x]
proof
  consider n being Element of NAT such that
A2: for m being Element of NAT, x being Point of T() st n<=m & x=S().m
  holds P[x] by A1;
  n in succ n & dom (p()") = NAT by FUNCT_2:def 1,ORDINAL1:6;
  then (p()").n in (p()").:(succ n) by FUNCT_1:def 6;
  then reconsider X=(p()").:(succ n) as finite non empty Subset of NAT;
  reconsider mX = (max X) + 1 as Element of NAT;
  take mX;
  let m be Element of NAT;
  m in NAT;
  then
A3: m in dom p() by FUNCT_2:52;
  assume
A4: mX<=m;
  n<=p().m
  proof
    assume p().m<n;
    then p().m in {p1 where p1 is Element of NAT : p1 < n};
    then p().m in n by AXIOMS:4;
    then p().m in succ n by ORDINAL1:8;
    then m in p()"(succ n) by A3,FUNCT_1:def 7;
    then m in (p()").:(succ n) by FUNCT_1:85;
    then m <=max X by XXREAL_2:def 8;
    hence contradiction by A4,NAT_1:13;
  end;
  then
A5: P[S().(p().m)] by A2;
  m in NAT;
  then m in dom p() by FUNCT_2:def 1;
  hence thesis by A5,FUNCT_1:13;
end;

scheme
  PermSeq2 {T()->non empty TopStruct,S()->sequence of T(),p()->Permutation of
NAT, P[set]} : ex n being Element of NAT st for m being Element of NAT st n<=m
  holds P[(S()*p()).m]
provided
A1: ex n being Element of NAT st for m being Element of NAT, x being
Point of T() st n<=m & x=S().m holds P[x]
proof
  reconsider T1=T() as non empty 1-sorted;
  reconsider S1=S() as sequence of T1;
A2: ex n being Element of NAT st for m being Element of NAT, x being Point
  of T1 st n<=m & x=S1.m holds P[x] by A1;
  ex n being Element of NAT st for m being Element of NAT st n<=m holds P[
  (S1*p()).m] from PermSeq(A2);
  hence thesis;
end;

theorem Th37:
  for T being non empty TopStruct, S being sequence of T, P being
  Permutation of NAT, x being Point of T st S is_convergent_to x holds S*P
  is_convergent_to x
proof
  let T be non empty TopStruct, S be sequence of T, P be Permutation of NAT, x
  be Point of T;
  assume
A1: S is_convergent_to x;
  for U1 being Subset of T st U1 is open & x in U1 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;
    defpred P[set] means $1 in U1;
    assume
A2: U1 is open & x in U1;
A3: ex n being Element of NAT st for m being Element of NAT, x being Point
    of T st n<=m & x=S.m holds P[x]
    proof
      consider n being Element of NAT such that
A4:   for m being Element of NAT st n<=m holds S.m in U1 by A1,A2,FRECHET:def 3
;
      take n;
      let m be Element of NAT, x be Point of T;
      assume n<=m & x=S.m;
      hence thesis by A4;
    end;
    thus ex n being Element of NAT st for m being Element of NAT st n <= m
    holds P[(S*P).m] from PermSeq2(A3);
  end;
  hence thesis by FRECHET:def 3;
end;

theorem
  for n0 being Element of NAT ex NS being increasing sequence of NAT st
  for n being Element of NAT holds NS.n=n+n0
proof
  let n0 be Element of NAT;
  deffunc F(Element of NAT) = $1 + n0;
  consider NS being Real_Sequence such that
A1: for n being Element of NAT holds NS.n=F(n) from SEQ_1:sch 1;
A2: NS is increasing
  proof
    let n be Element of NAT;
    n < n + 1 by NAT_1:13;
    then n + n0 < (n+1) + n0 by XREAL_1:6;
    then NS.n < (n+1) + n0 by A1;
    hence thesis by A1;
  end;
  for n being Element of NAT holds NS.n is Element of NAT
  proof
    let n be Element of NAT;
    n + n0 in NAT;
    hence thesis by A1;
  end;
  then reconsider NS as increasing sequence of NAT by A2,SEQM_3:13;
  take NS;
  thus thesis by A1;
end;

theorem Th39:
  for T being non empty TopStruct, S being sequence of T, x being
  Point of T, n0 being Nat st x is_a_cluster_point_of S holds x
  is_a_cluster_point_of S^\n0
proof
  let T be non empty TopStruct, S be sequence of T, x be Point of T, n0 be Nat;
  assume
A1: x is_a_cluster_point_of S;
  set S1 = S^\n0;
  let O be Subset of T, n be Element of NAT;
  assume O is open & x in O;
  then consider m0 being Element of NAT such that
A2: n + n0 <= m0 and
A3: S.m0 in O by A1,Def3;
  n0 in NAT & n0 <= n + n0 by NAT_1:11,ORDINAL1:def 12;
  then reconsider m=m0-n0 as Element of NAT by A2,INT_1:5,XXREAL_0:2;
  take m;
  thus n <= m by A2,XREAL_1:19;
  S1.m = S.(m0-n0+n0) by NAT_1:def 3
    .= S.m0;
  hence thesis by A3;
end;

theorem Th40:
  for T being non empty TopStruct, S being sequence of T, x being
  Point of T st x is_a_cluster_point_of S holds x in Cl(rng S)
proof
  let T be non empty TopStruct, S be sequence of T, x be Point of T;
  assume
A1: x is_a_cluster_point_of S;
  for G being Subset of T st G is open holds x in G implies rng S meets G
  proof
    let G be Subset of T;
    assume
A2: G is open;
    assume x in G;
    then consider m being Element of NAT such that
    0 <= m and
A3: S.m in G by A1,A2,Def3;
    m in NAT;
    then m in dom S by NORMSP_1:12;
    then S.m in rng S by FUNCT_1:def 3;
    then S.m in rng S /\ G by A3,XBOOLE_0:def 4;
    hence thesis by XBOOLE_0:def 7;
  end;
  hence thesis by PRE_TOPC:def 7;
end;

theorem
  for T being non empty TopStruct st T is Frechet for S being sequence
  of T, x being Point of T st x is_a_cluster_point_of S holds ex S1 being
  subsequence of S st S1 is_convergent_to x
proof
  let T be non empty TopStruct;
  assume
A1: T is Frechet;
  let S be sequence of T, x be Point of T;
  assume
A2: x is_a_cluster_point_of S;
  defpred P[Point of T] means x in Cl{$1};
  reconsider Y={y where y is Point of T : P[y]} as Subset of T from DOMAIN_1:
  sch 7;
  per cases;
  suppose
A3: for n being Element of NAT ex m being Element of NAT st m >= n & S .m in Y;
    defpred P[set] means $1 in Y;
A4: for n being Element of NAT ex m being Element of NAT st n <= m & P[S.m
    ] by A3;
    consider S1 being subsequence of S such that
A5: for n being Element of NAT holds P[S1.n] from VALUED_1:sch 1(A4);
    take S1;
    rng S1 c= Y
    proof
      let y be set;
      assume y in rng S1;
      then consider n being set such that
A6:   n in dom S1 and
A7:   y = S1.n by FUNCT_1:def 3;
      reconsider n as Element of NAT by A6;
      S1.n in Y by A5;
      hence thesis by A7;
    end;
    hence thesis by Th33;
  end;
  suppose
    ex n being Element of NAT st for m being Element of NAT st m >= n
    holds not S.m in Y;
    then consider n0 being Element of NAT such that
A8: for m being Element of NAT st m >= n0 holds not S.m in Y;
    set S9 = S^\n0;
    x in Cl(rng S9) by A2,Th39,Th40;
    then consider S2 being sequence of T such that
A9: rng S2 c= rng S9 and
A10: x in Lim S2 by A1,FRECHET:def 6;
A11: S2 is_convergent_to x by A10,FRECHET:def 5;
A12: for n being Element of NAT holds not S9.n in Y
    proof
      let n be Element of NAT;
      not S.(n+n0) in Y by A8,NAT_1:11;
      hence thesis by NAT_1:def 3;
    end;
    rng S9 /\ Y = {}
    proof
      set y = the Element of rng S9 /\ Y;
      assume
A13:  rng S9 /\ Y <> {};
      then y in rng S9 by XBOOLE_0:def 4;
      then consider n being set such that
A14:  n in dom S9 and
A15:  y = S9.n by FUNCT_1:def 3;
      reconsider n as Element of NAT by A14;
      not S9.n in Y by A12;
      hence contradiction by A13,A15,XBOOLE_0:def 4;
    end;
    then rng S9 misses Y by XBOOLE_0:def 7;
    then consider S29 being subsequence of S2 such that
A16: S29 is one-to-one by A9,A11,Th35,XBOOLE_1:63;
    rng S29 c= rng S2 by VALUED_0:21;
    then consider P being Permutation of NAT such that
A17: S29*P is subsequence of S9 by A9,A16,Th36,XBOOLE_1:1;
    reconsider S1=S29*P as subsequence of S9 by A17;
    reconsider S1 as subsequence of S by VALUED_0:20;
    take S1;
    S29 is_convergent_to x by A11,Th15;
    hence thesis by Th37;
  end;
end;

begin :: Auxiliary theorems

theorem
  for T being non empty TopSpace st T is first-countable holds for x
being Point of T holds ex B being Basis of x st ex S being Function st dom S =
  NAT & rng S = B & for n,m being Element of NAT st m >= n holds S.m c= S.n by
Lm5;

theorem
  for T being non empty TopSpace st for p being Point of T holds Cl({p})
  = {p} holds T is T_1 by Lm1;

theorem
  for T being non empty TopSpace holds T is T_2 implies T is T_1 by Lm4;

theorem
  for T being non empty TopSpace st not T is T_1 holds ex x1,x2 being
  Point of T, S being sequence of T st S = (NAT --> x1) & x1 <> x2 & S
  is_convergent_to x2 by Lm3;