frechet2.miz



    begin

    

     Lm1: for T be non empty TopSpace st for p be Point of T holds ( Cl {p}) = {p} holds T is T_1

    proof

      let T be non empty TopSpace;

      assume

       A1: for p be Point of T holds ( Cl {p}) = {p};

      for p be 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 be non empty TopSpace holds not T is T_1 implies ex x1,x2 be 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 be Point of T such that

       A1: ( Cl {x1}) <> {x1} by Lm1;

       not {x1} c= ( Cl {x1}) or not ( Cl {x1}) c= {x1} by A1;

      then

      consider x2 be object such that

       A2: x2 in ( Cl {x1}) and

       A3: not x2 in {x1} by PRE_TOPC: 18;

      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 be non empty TopSpace holds not T is T_1 implies ex x1,x2 be Point of T, S be 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 be 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 ;

        let n be Nat;

        

         A4: n in NAT by ORDINAL1:def 12;

        assume 0 <= n;

         {x1} meets U1 by A2, A3, PRE_TOPC:def 7;

        then x1 in U1 by ZFMISC_1: 50;

        hence thesis by FUNCOP_1: 7, A4;

      end;

    end;

    

     Lm4: for T be 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 be Point of T holds {p} is closed by PCOMPS_1: 7;

      hence thesis by URYSOHN1: 19;

    end;

    theorem :: FRECHET2:1

    for T be non empty 1-sorted, S be sequence of T, NS be increasing sequence of NAT holds (S * NS) is sequence of T;

    theorem :: FRECHET2:2

    for RS be Real_Sequence st RS = ( id NAT ) holds RS is increasing sequence of NAT ;

    theorem :: FRECHET2:3

    

     Th3: for T be non empty 1-sorted, S be sequence of T, A be Subset of T holds (for S1 be subsequence of S holds not ( rng S1) c= A) implies ex n be Element of NAT st for m be 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 be subsequence of S holds not ( rng S1) c= A;

      defpred Q[ set] means $1 in A;

      assume for n be Element of NAT holds ex m be Element of NAT st n <= m & (S . m) in A;

      then

       A2: for n be Element of NAT holds ex m be Element of NAT st n <= m & Q[(S . m)];

      consider S1 be subsequence of S such that

       A3: for n be Element of NAT holds Q[(S1 . n)] from VALUED_1:sch 1( A2);

      ( rng S1) c= A

      proof

        let y be object;

        assume y in ( rng S1);

        then

        consider x1 be object 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 :: FRECHET2:4

    

     Th4: for T be non empty 1-sorted, S be sequence of T, A,B be Subset of T st ( rng S) c= (A \/ B) holds ex S1 be 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 be subsequence of S holds not ( rng S1) c= A & not ( rng S1) c= B;

      then

      consider n1 be Element of NAT such that

       A3: for m be Element of NAT st n1 <= m holds not (S . m) in A by Th3;

      consider n2 be Element of NAT such that

       A4: for m be 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 be non empty TopSpace st T is first-countable holds for x be Point of T holds ex B be Basis of x st ex S be Function st ( dom S) = NAT & ( rng S) = B & for n,m be 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 be Basis of x such that

       A2: B1 is countable by A1;

      consider f be sequence of B1 such that

       A3: ( rng f) = B1 by A2, CARD_3: 96;

      defpred P[ object, object] means ex D1 be set st D1 = $1 & $2 = ( meet (f .: ( succ D1)));

      

       A4: for n be object st n in NAT holds ex A be object st P[n, A]

      proof

        let n be object;

        reconsider D1 = n as set by TARSKI: 1;

        assume n in NAT ;

        take A = ( meet (f .: ( succ D1)));

        thus P[n, A];

      end;

      consider S be Function such that

       A5: ( dom S) = NAT and

       A6: for n be object 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 object;

        assume A in ( rng S);

        then

        consider n be object such that

         A8: n in ( dom S) & A = (S . n) by FUNCT_1:def 3;

        reconsider n as set by TARSKI: 1;

        reconsider fsuccn = (f .: ( succ n)) as Subset-Family of T by XBOOLE_1: 1;

         P[n, (S . n)] by A5, A6, A8;

        then

        consider D1 be set such that

         A9: D1 = n & (S . n) = ( meet fsuccn);

        thus thesis by A8, A9;

      end;

      then

      reconsider B = ( rng S) as Subset-Family of T;

      reconsider B as Subset-Family of T;

      

       A10: ex A be set st A in B

      proof

        take A = ( meet (f .: ( succ 0 )));

         P[ 0 , (S . 0 )] by A6;

        then A = (S . 0 );

        hence thesis by A5, FUNCT_1:def 3;

      end;

      then

       A11: ( Intersect B) = ( meet B) by SETFAM_1:def 9;

      for A be set st A in B holds x in A

      proof

        let A be set;

        assume A in B;

        then

        consider n be object such that

         A12: n in ( dom S) and

         A13: A = (S . n) by FUNCT_1:def 3;

        reconsider n as set by TARSKI: 1;

        ( dom f) = NAT & n in ( succ n) by FUNCT_2:def 1, ORDINAL1: 6;

        then

         A14: (f . n) in (f .: ( succ n)) by A5, A12, FUNCT_1:def 6;

        

         A15: for A1 be 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 be object such that

           A16: m in ( dom f) and m in ( succ n) and

           A17: A1 = (f . m) by FUNCT_1:def 6;

          (f . m) in ( rng f) by A16, FUNCT_1:def 3;

          then

          reconsider A2 = A1 as Subset of T by A3, A17;

          reconsider A2 as Subset of T;

          A2 in B1 by A3, A16, A17, FUNCT_1:def 3;

          hence thesis by YELLOW_8: 12;

        end;

         P[n, (S . n)] by A5, A6, A12;

        then A = ( meet (f .: ( succ n))) by A13;

        hence thesis by A15, A14, SETFAM_1:def 1;

      end;

      then

       A18: x in ( meet B) by A10, SETFAM_1:def 1;

      

       A19: B c= the topology of T

      proof

        let A be object;

        assume A in B;

        then

        consider n be object such that

         A20: n in ( dom S) and

         A21: A = (S . n) by FUNCT_1:def 3;

        reconsider n9 = n as Element of NAT by A5, A20;

        reconsider n as set by TARSKI: 1;

        reconsider C = (f .: ( succ n)) as Subset-Family of T by XBOOLE_1: 1;

        

         A22: C is open by YELLOW_8: 12;

        ( succ n9) is finite;

        then (f .: ( succ n)) is finite;

        then

         A23: ( meet C) is open by A22, TOPS_2: 20;

         P[n, (S . n)] by A5, A6, A20;

        then A = ( meet (f .: ( succ n))) by A21;

        hence thesis by A23;

      end;

      for O be Subset of T st O is open & x in O holds ex A be 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 be Subset of T such that

         A24: A1 in B1 and

         A25: A1 c= O by YELLOW_8:def 1;

        consider n be object such that

         A26: n in ( dom f) and

         A27: A1 = (f . n) by A3, A24, FUNCT_1:def 3;

        reconsider n as set by TARSKI: 1;

        (S . n) in ( rng S) by A5, A26, 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, A26, FUNCT_1:def 3;

        n in ( succ n) by ORDINAL1: 6;

        then (f . n) in (f .: ( succ n)) by A26, FUNCT_1:def 6;

        then

         A28: ( meet (f .: ( succ n))) c= A1 by A27, SETFAM_1: 3;

         P[n, (S . n)] by A26, A6;

        then (S . n) c= A1 by A28;

        hence thesis by A25;

      end;

      then

      reconsider B as Basis of x by A19, A11, A18, TOPS_2: 64, YELLOW_8:def 1;

      take B, S;

      thus ( dom S) = NAT by A5;

      thus ( rng S) = B;

      for n,m be 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 ( Segm (n + 1)) c= ( Segm (m + 1)) by NAT_1: 39;

        then ( succ ( Segm n)) c= ( Segm (m + 1)) by NAT_1: 38;

        then ( succ ( Segm n)) c= ( succ ( Segm m)) by NAT_1: 38;

        then

         A29: (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

         A30: ( meet (f .: ( succ m))) c= ( meet (f .: ( succ n))) by A29, SETFAM_1: 6;

        

         A31: P[m, (S . m)] by A6;

         P[n, (S . n)] by A6;

        hence thesis by A30, A31;

      end;

      hence thesis;

    end;

    theorem :: FRECHET2:5

    for T be non empty TopSpace holds (for S be sequence of T holds for x1,x2 be 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 be sequence of T holds for x1,x2 be 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 be Point of T, S be 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 :: FRECHET2:6

    

     Th6: for T be non empty TopSpace st T is T_2 holds for S be sequence of T, x1,x2 be 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 be sequence of T, x1,x2 be Point of T holds (x1 in ( Lim S) & x2 in ( Lim S) implies x1 = x2));

      then

      consider S be sequence of T such that

       A2: ex x1,x2 be Point of T st x1 in ( Lim S) & x2 in ( Lim S) & x1 <> x2;

      consider x1,x2 be 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 be 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;

      S is_convergent_to x1 by A3, FRECHET:def 5;

      then

      consider n1 be Nat such that

       A11: for m be Nat st n1 <= m holds (S . m) in U1 by A6, A8;

      S is_convergent_to x2 by A4, FRECHET:def 5;

      then

      consider n2 be Nat such that

       A12: for m be Nat st n2 <= m holds (S . m) in U2 by A7, A9;

      reconsider n = ( max (n1,n2)) as Element of NAT by ORDINAL1:def 12;

      

       A13: (S . n) in U1 by A11, XXREAL_0: 25;

      

       A14: (S . n) in U2 by A12, XXREAL_0: 25;

      (U1 /\ U2) = {} by A10;

      hence contradiction by A13, A14, XBOOLE_0:def 4;

    end;

    theorem :: FRECHET2:7

    for T be non empty TopSpace st T is first-countable holds T is T_2 iff for S be sequence of T holds for x1,x2 be 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 be sequence of T holds for x1,x2 be Point of T holds (x1 in ( Lim S) & x2 in ( Lim S) implies x1 = x2) by Th6;

      assume

       A2: for S be sequence of T holds for x1,x2 be 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 be Point of T such that

       A3: x1 <> x2 and

       A4: for U1,U2 be Subset of T st U1 is open & U2 is open & x1 in U1 & x2 in U2 holds U1 meets U2;

      consider B1 be Basis of x1 such that

       A5: ex S be Function st ( dom S) = NAT & ( rng S) = B1 & for n,m be Element of NAT st m >= n holds (S . m) c= (S . n) by A1, Lm5;

      consider B2 be Basis of x2 such that

       A6: ex S be Function st ( dom S) = NAT & ( rng S) = B2 & for n,m be Element of NAT st m >= n holds (S . m) c= (S . n) by A1, Lm5;

      consider S1 be Function such that

       A7: ( dom S1) = NAT and

       A8: ( rng S1) = B1 and

       A9: for n,m be Element of NAT st m >= n holds (S1 . m) c= (S1 . n) by A5;

      consider S2 be Function such that

       A10: ( dom S2) = NAT and

       A11: ( rng S2) = B2 and

       A12: for n,m be Element of NAT st m >= n holds (S2 . m) c= (S2 . n) by A6;

      defpred P[ object, object] means $2 in ((S1 . $1) /\ (S2 . $1));

      

       A13: for n be object st n in NAT holds ex x be object st x in the carrier of T & P[n, x]

      proof

        let n be object;

        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) <> {} ;

        then x in (U1 /\ U2);

        hence x in the carrier of T;

        thus thesis by A18;

      end;

      consider S be Function such that

       A19: ( dom S) = NAT & ( rng S) c= the carrier of T and

       A20: for n be object st n in NAT holds P[n, (S . n)] from FUNCT_1:sch 6( A13);

      reconsider S as sequence of 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 be Subset of T such that

         A21: V2 in B2 and

         A22: V2 c= U2 by YELLOW_8: 13;

        consider n be object 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 Nat;

        reconsider mm = m as Element of NAT by ORDINAL1:def 12;

        (S . mm) in ((S1 . mm) /\ (S2 . mm)) & ((S1 . mm) /\ (S2 . mm)) c= (S2 . mm) by A20, XBOOLE_1: 17;

        then

         A25: (S . m) in (S2 . m);

        assume n <= m;

        then (S2 . mm) 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 be Subset of T such that

         A27: V1 in B1 and

         A28: V1 c= U1 by YELLOW_8: 13;

        consider n be object 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 Nat;

        

         A31: m in NAT by ORDINAL1:def 12;

        then (S . m) in ((S1 . m) /\ (S2 . m)) & ((S1 . m) /\ (S2 . m)) c= (S1 . m) by A20, XBOOLE_1: 17;

        then

         A32: (S . m) in (S1 . m);

        assume n <= m;

        then (S1 . m) c= (S1 . n) by A9, A31;

        then (S . m) in (S1 . n) by A32;

        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 :: FRECHET2:8

    for T be non empty TopStruct, S be sequence of T st not S is convergent holds ( Lim S) = {}

    proof

      let T be non empty TopStruct, S be sequence of T;

      assume

       A1: not S is 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;

    end;

    theorem :: FRECHET2:9

    

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

    theorem :: FRECHET2:10

    for T be non empty TopStruct, S be sequence of T, x be Point of T st not S is_convergent_to x holds ex S1 be subsequence of S st for S2 be 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 be Subset of T such that

       A1: A is open & x in A and

       A2: for n be Nat holds ex m be Nat st n <= m & not (S . m) in A;

      defpred P[ set] means not $1 in A;

      

       A3: for n be Element of NAT holds ex m be Element of NAT st n <= m & P[(S . m)]

      proof

        let n be Element of NAT ;

        consider m be Nat such that

         A4: n <= m & not (S . m) in A by A2;

        reconsider m as Element of NAT by ORDINAL1:def 12;

        take m;

        thus thesis by A4;

      end;

      consider S1 be subsequence of S such that

       A5: for n be Element of NAT holds P[(S1 . n)] from VALUED_1:sch 1( A3);

      take S1;

      let S2 be subsequence of S1;

      ex U1 be Subset of T st U1 is open & x in U1 & for n be Nat holds ex m be Nat st n <= m & not (S2 . m) in U1

      proof

        take A;

        consider NS be increasing sequence of NAT such that

         A6: S2 = (S1 * NS) by VALUED_0:def 17;

        thus A is open & x in A by A1;

        let n be Nat;

        take n;

        thus n <= n;

        n in NAT by ORDINAL1:def 12;

        then n in ( dom S2) by NORMSP_1: 12;

        then (S2 . n) = (S1 . (NS . n)) by A6, FUNCT_1: 12;

        hence thesis by A5;

      end;

      hence thesis;

    end;

    begin

    theorem :: FRECHET2:11

    

     Th11: for T1,T2 be non empty TopSpace, f be Function of T1, T2 holds f is continuous implies for S1 be sequence of T1, S2 be 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 object;

      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 be object 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 be Nat such that

         A11: for m be Nat st n <= m holds (S1 . m) in (f " U2) by A10, A9;

        take n;

        let m be Nat;

        

         A12: m in NAT by ORDINAL1:def 12;

        assume n <= m;

        then (S1 . m) in (f " U2) by A11;

        then

         A13: (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, A13, FUNCT_1: 13, A12;

      end;

      hence thesis by FRECHET:def 5;

    end;

    theorem :: FRECHET2:12

    for T1,T2 be non empty TopSpace, f be Function of T1, T2 st T1 is sequential holds f is continuous iff for S1 be sequence of T1, S2 be 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 be sequence of T1, S2 be sequence of T2 st S2 = (f * S1) holds (f .: ( Lim S1)) c= ( Lim S2) by Th11;

      assume

       A2: for S1 be sequence of T1, S2 be 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 be 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 object;

          assume z in ( rng S2);

          then

          consider n be object 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 object;

        

         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;

    end;

    begin

    definition

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

      :: FRECHET2:def1

      func Cl_Seq A -> Subset of T means

      : Def1: for x be Point of T holds x in it iff ex S be sequence of T st ( rng S) c= A & x in ( Lim S);

      existence

      proof

        defpred P[ Point of T] means ex S be sequence of T st ( rng S) c= A & $1 in ( Lim S);

        reconsider X = { x where x be 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 be sequence of T st ( rng S) c= A & x in ( Lim S)

        proof

          assume x in X;

          then ex x9 be Point of T st x = x9 & ex S be sequence of T st ( rng S) c= A & x9 in ( Lim S);

          hence thesis;

        end;

        assume ex S be 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 be Point of T holds x in A1 iff ex S be sequence of T st ( rng S) c= A & x in ( Lim S) and

         A2: for x be Point of T holds x in A2 iff ex S be sequence of T st ( rng S) c= A & x in ( Lim S);

        for x be Point of T holds x in A1 iff x in A2

        proof

          let x be Point of T;

          x in A1 iff ex S be 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 :: FRECHET2:13

    

     Th13: for T be non empty TopStruct, A be Subset of T, S be sequence of T, x be 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 be 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 be Nat such that

         A5: for m be Nat st n <= m holds (S . m) in O by A3, A4;

        n in NAT by ORDINAL1:def 12;

        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;

      end;

      hence thesis by PRE_TOPC:def 7;

    end;

    theorem :: FRECHET2:14

    

     Th14: for T be non empty TopStruct, A be 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 object;

      assume

       A1: x in ( Cl_Seq A);

      then

      reconsider x9 = x as Point of T;

      ex S be sequence of T st ( rng S) c= A & x9 in ( Lim S) by A1, Def1;

      hence thesis by Th13;

    end;

    theorem :: FRECHET2:15

    

     Th15: for T be non empty TopStruct, S be sequence of T, S1 be subsequence of S, x be 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 be Nat such that

       A2: for m be Nat st n <= m holds (S . m) in U1 by A1;

      take n;

      let m be Nat;

      assume

       A3: n <= m;

      m in NAT by ORDINAL1:def 12;

      then

       A4: m in ( dom S1) by NORMSP_1: 12;

      consider NS be 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 :: FRECHET2:16

    

     Th16: for T be non empty TopStruct, S be sequence of T, S1 be 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 object;

      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 :: FRECHET2:17

    

     Th17: for T be 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 be 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 :: FRECHET2:18

    

     Th18: for T be non empty TopStruct, A be Subset of T holds A c= ( Cl_Seq A)

    proof

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

      let x be object;

      assume

       A1: x in A;

      then

      reconsider x9 = x as Point of T;

      ex S be sequence of T st ( rng S) c= A & x9 in ( Lim S)

      proof

        set S = ( NAT --> x9);

        take S;

         {x9} c= A by A1, TARSKI:def 1;

        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 :: FRECHET2:19

    

     Th19: for T be non empty TopStruct, A,B be 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 object;

        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 be 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;

          hence thesis by A4, Def1;

        end;

          suppose

           A5: x in ( Cl_Seq B);

          then

          reconsider x9 = x as Point of T;

          consider S be 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;

          hence thesis by A7, Def1;

        end;

      end;

      thus ( Cl_Seq (A \/ B)) c= (( Cl_Seq A) \/ ( Cl_Seq B))

      proof

        let x be object;

        assume

         A8: x in ( Cl_Seq (A \/ B));

        then

        reconsider x9 = x as Point of T;

        consider S be sequence of T such that

         A9: ( rng S) c= (A \/ B) and

         A10: x9 in ( Lim S) by A8, Def1;

        consider S1 be 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 :: FRECHET2:20

    

     Th20: for T be non empty TopStruct holds T is Frechet iff for A be Subset of T holds ( Cl A) = ( Cl_Seq A)

    proof

      let T be non empty TopStruct;

      thus T is Frechet implies for A be 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 object;

          assume

           A2: x in ( Cl A);

          then

          reconsider x9 = x as Point of T;

          ex S be sequence of T st ( rng S) c= A9 & x9 in ( Lim S) by A1, A2;

          hence thesis by Def1;

        end;

        thus thesis by Th14;

      end;

      assume

       A3: for A be 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 :: FRECHET2:21

    

     Th21: for T be non empty TopSpace st T is Frechet holds for A,B be 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 :: FRECHET2:22

    

     Th22: for T be non empty TopSpace st T is sequential holds (for A be 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 be Subset of T holds ( Cl_Seq ( Cl_Seq A)) = ( Cl_Seq A);

      assume not T is Frechet;

      then

      consider A be Subset of T such that

       A3: ex x be Point of T st x in ( Cl A) & for S be sequence of T holds (( rng S) c= A implies not x in ( Lim S));

      for Sq be 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 object;

        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;

      consider x be Point of T such that

       A7: x in ( Cl A) and

       A8: for S be 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 :: FRECHET2:23

    for T be non empty TopSpace st T is sequential holds T is Frechet iff for A,B be 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

    definition

      let T be non empty TopSpace, S be sequence of T;

      assume

       A1: ex x be Point of T st ( Lim S) = {x};

      :: FRECHET2:def2

      func lim S -> Point of T means

      : Def2: S is_convergent_to it ;

      existence

      proof

        consider x be 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 be 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 :: FRECHET2:24

    

     Th24: for T be non empty TopSpace st T is T_2 holds for S be sequence of T st S is convergent holds ex x be 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 be Point of T such that

       A2: S is_convergent_to x;

      take x;

      

       A3: x in ( Lim S) by A2, FRECHET:def 5;

      thus ( Lim S) c= {x}

      proof

        let y be object;

        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 object;

      assume y in {x};

      hence thesis by A3, TARSKI:def 1;

    end;

    theorem :: FRECHET2:25

    

     Th25: for T be non empty TopSpace st T is T_2 holds for S be sequence of T, x be 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;

        then ex y be 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 be Point of T st ( Lim S) = {x} by A1, A3, Th24;

      hence thesis by A4, Def2;

    end;

    theorem :: FRECHET2:26

    for M be MetrStruct, S be 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 :: FRECHET2:27

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

    theorem :: FRECHET2:28

    

     Th28: for 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) 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 be Real such that

         A4: r > 0 and

         A5: ( Ball (x,r)) c= U1 by A2, TOPMETR: 15;

        reconsider r as Real;

        ( Ball (x,r)) contains_almost_all_sequence S by A3, A4, METRIC_6: 15;

        then

        consider n be Nat such that

         A6: for m be Nat st n <= m holds (S . m) in ( Ball (x,r));

        reconsider n as Element of NAT by ORDINAL1:def 12;

        take n;

        let m be 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 be 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;

        then

        consider n be Nat such that

         A10: for m be Nat st n <= m holds (S9 . m) in V9 by A2, A7, A8;

        take n;

        let m be Nat;

        assume n <= m;

        hence thesis by A1, A10;

      end;

      hence thesis by METRIC_6: 17;

    end;

    theorem :: FRECHET2:29

    for M be non empty MetrSpace, Sm be sequence of M, St be 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 be 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;

      end;

      assume St is convergent;

      then

      consider x9 be Point of ( TopSpaceMetr M) such that

       A3: St is_convergent_to x9;

      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 :: FRECHET2:30

    for M be non empty MetrSpace, Sm be sequence of M, St be 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

    definition

      let T be TopStruct, S be sequence of T, x be Point of T;

      :: FRECHET2:def3

      pred x is_a_cluster_point_of S means for O be Subset of T, n be Nat st O is open & x in O holds ex m be Element of NAT st n <= m & (S . m) in O;

    end

    theorem :: FRECHET2:31

    

     Th31: for T be non empty TopStruct, S be sequence of T, x be Point of T st ex S1 be 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 be subsequence of S such that

       A1: S1 is_convergent_to x;

      let O be Subset of T, n be Nat;

      assume O is open & x in O;

      then

      consider n1 be Nat such that

       A2: for m be Nat st n1 <= m holds (S1 . m) in O by A1;

      reconsider n2 = ( max (n1,n)) as Element of NAT by ORDINAL1:def 12;

      

       A3: (S1 . n2) in O by A2, XXREAL_0: 25;

      consider NS be 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 :: FRECHET2:32

    for T be non empty TopStruct, S be sequence of T, x be 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 be 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 :: FRECHET2:33

    

     Th33: for T be non empty TopStruct, S be sequence of T, x be Point of T, Y be Subset of T st Y = { y where y be 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 be 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 Nat;

      m in NAT by ORDINAL1:def 12;

      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 be 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 :: FRECHET2:34

    

     Th34: for T be non empty TopStruct, S be sequence of T, x,y be Point of T st for n be 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 be Element of NAT holds (S . n) = y & S is_convergent_to x;

      for G be 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 be Nat such that

         A3: for m be Nat st n <= m holds (S . m) in G by A1, A2, FRECHET:def 3;

        

         A4: n in NAT by ORDINAL1:def 12;

        (S . n) in G by A3;

        then

         A5: y in G by A1, A4;

        y in {y} by TARSKI:def 1;

        then y in ( {y} /\ G) by A5, XBOOLE_0:def 4;

        hence thesis;

      end;

      hence thesis by PRE_TOPC:def 7;

    end;

    theorem :: FRECHET2:35

    

     Th35: for T be non empty TopStruct, x be Point of T, Y be Subset of T, S be sequence of T st Y = { y where y be Point of T : x in ( Cl {y}) } & ( rng S) misses Y & S is_convergent_to x holds ex S1 be 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 be Point of T : x in ( Cl {y}) } and

       A2: (( rng S) /\ Y) = {} and

       A3: S is_convergent_to x;

      defpred P[ Nat, set, set] means $3 in NAT & for n1,n2,m be Element of NAT st n1 = $2 & n2 = $3 & n2 <= m holds (S . m) <> (S . n1);

      

       A4: for z be set st z in ( rng S) holds ex n0 be Element of NAT st for m be 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 be Element of NAT holds ex m be Element of NAT st n0 <= m & z = (S . m);

        then

         A6: for n be Element of NAT holds ex m be Element of NAT st n <= m & P[(S . m)];

        ex S1 be subsequence of S st for n be 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 be Nat holds for z1 be set holds ex z2 be set st P[n, z1, z2]

      proof

        let n be 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 be Element of NAT such that

           A10: for m be 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 be Function such that

       A11: ( dom f) = NAT and

       A12: (f . 0 ) = 0 and

       A13: for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 1( A7);

      

       A14: for n be Nat holds (f . n) is Element of NAT

      proof

        let n be Nat;

        

         A15: n in NAT by ORDINAL1:def 12;

        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, A15;

          (n1 + 1) = n;

          hence thesis by A13;

        end;

      end;

      then for n be Nat holds (f . n) is real;

      then

      reconsider f as Real_Sequence by A11, SEQ_1: 2;

      f is increasing

      proof

        let n be Nat;

        reconsider nn = n, nn1 = (n + 1) as Element of NAT by ORDINAL1:def 12;

        reconsider n2 = (f . nn1) as Element of NAT by A14;

        reconsider n1 = (f . nn) 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);

      

       A16: for n1,n2 be 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

         A17: (S . (f . n2)) = (S1 . n2) by FUNCT_1: 12;

        assume n1 < n2;

        then

         A18: (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 A18, XXREAL_0: 1;

            hence thesis by SEQM_3: 1;

          end;

        end;

        then

         A19: (S . (f . n2)) <> (S . n19) by A13;

        n1 in NAT ;

        then n1 in ( dom S1) by NORMSP_1: 12;

        hence thesis by A19, A17, FUNCT_1: 12;

      end;

      let x1,x2 be object;

      assume that

       A20: x1 in ( dom S1) and

       A21: x2 in ( dom S1) and

       A22: (S1 . x1) = (S1 . x2);

      reconsider n2 = x2 as Element of NAT by A21;

      reconsider n1 = x1 as Element of NAT by A20;

      assume

       A23: x1 <> x2;

      per cases by A23, XXREAL_0: 1;

        suppose n1 < n2;

        hence contradiction by A22, A16;

      end;

        suppose n2 < n1;

        hence contradiction by A22, A16;

      end;

    end;

    theorem :: FRECHET2:36

    

     Th36: for T be non empty TopStruct, S1,S2 be sequence of T st ( rng S2) c= ( rng S1) & S2 is one-to-one holds ex P be 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[ object, object] means (S2 . $1) = (S1 . $2);

      

       A3: for n be object st n in NAT holds ex u be object st u in NAT & P[n, u]

      proof

        let n be object;

        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 be object 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 be Function such that

       A6: ( dom f) = NAT and

       A7: ( rng f) c= NAT and

       A8: for n be object st n in NAT holds P[n, (f . n)] from FUNCT_1:sch 6( A3);

      reconsider A = ( rng f) as non empty Subset of NAT by A6, A7, RELAT_1: 42;

      defpred P[ Nat, set, set] means for B be non empty Subset of NAT , m be Element of NAT st m = $2 & B = { k where k be Element of NAT : k in ( rng f) & k > m } holds $3 = ( min B);

      

       A9: f is one-to-one

      proof

        let x1,x2 be object;

        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;

      end;

      

       A14: for m be Element of NAT holds { k where k be Element of NAT : k in ( rng f) & k > m } <> {}

      proof

        let m be Element of NAT ;

        assume

         A15: { k where k be Element of NAT : k in ( rng f) & k > m } = {} ;

        ( rng f) c= (m + 1)

        proof

          let x be object;

          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 be Element of NAT : k in ( rng f) & k > m } by A16;

            hence contradiction by A15;

          end;

          then x9 in { x99 where x99 be 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 be Element of NAT holds { k where k be Element of NAT : k in ( rng f) & k > m } c= NAT

      proof

        let m be Element of NAT ;

        let z be object;

        assume z in { k where k be Element of NAT : k in ( rng f) & k > m };

        then ex k be Element of NAT st k = z & k in ( rng f) & k > m;

        hence thesis;

      end;

      

       A18: for n be Nat holds for x be set holds ex y be set st P[n, x, y]

      proof

        let n be Nat, x be set;

        per cases ;

          suppose x in NAT ;

          then

          reconsider x9 = x as Element of NAT ;

          set B = { k where k be 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 be 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 be Element of NAT : k in ( rng f) & k > m };

          thus thesis by A19, A20;

        end;

      end;

      consider g be Function such that

       A21: ( dom g) = NAT and

       A22: (g . 0 ) = ( min A) and

       A23: for n be Nat holds P[n, (g . n), (g . (n + 1))] from RECDEF_1:sch 1( A18);

      defpred P[ Nat] means (g . $1) in NAT ;

      

       A24: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume (g . k) in NAT ;

        then

        reconsider m = (g . k) as Element of NAT ;

        set B = { l where l be 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 be Nat holds P[k] from NAT_1:sch 2( A25, A24);

      for n be Nat holds (g . n) is real

      proof

        let n be Nat;

        (g . n) in NAT by A26;

        then

        reconsider w = (g . n) as Element of REAL by XREAL_0:def 1;

        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 Nat;

        reconsider m = (g . n) as Element of NAT by A26;

        reconsider B = { k where k be 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 be 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 object;

        assume y in ( rng g);

        then

        consider x be object 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 object;

        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 be object holds y in ( rng f) implies y in ( rng g)

        proof

          let y be object;

          assume

           A38: y in ( rng f);

          then

          reconsider y9 = y as Element of NAT by A7;

          defpred P[ Nat] means (g1 . $1) < y9;

          assume

           A39: not y in ( rng g);

          

           A40: for n be Nat st P[n] holds P[(n + 1)]

          proof

            let n be Nat;

            reconsider m = (g . n) as Element of NAT by A26;

            reconsider B = { k where k be 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 be 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 be Nat holds P[n] from NAT_1:sch 2( A43, A40);

          ( rng g) c= y9

          proof

            let y be object;

            assume y in ( rng g);

            then

            consider x be object 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 be 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 object;

        assume y in ( rng g);

        then

        consider x be object 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 be 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 be 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, RELAT_1: 28;

      then

      reconsider P = ((g " ) * f) as sequence of 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 be object 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 object;

        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);

      hence thesis;

    end;

    scheme :: FRECHET2:sch1

    PermSeq { T() -> non empty 1-sorted , S() -> sequence of T() , p() -> Permutation of NAT , P[ set] } :

ex n be Element of NAT st for m be Element of NAT st n <= m holds P[((S() * p()) . m)]

      provided

       A1: ex n be Element of NAT st for m be Element of NAT , x be Point of T() st n <= m & x = (S() . m) holds P[x];

      consider n be Element of NAT such that

       A2: for m be Element of NAT , x be 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 be 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 :: FRECHET2:sch2

    PermSeq2 { T() -> non empty TopStruct , S() -> sequence of T() , p() -> Permutation of NAT , P[ set] } :

ex n be Element of NAT st for m be Element of NAT st n <= m holds P[((S() * p()) . m)]

      provided

       A1: ex n be Element of NAT st for m be Element of NAT , x be Point of T() st n <= m & x = (S() . m) holds P[x];

      reconsider T1 = T() as non empty 1-sorted;

      reconsider S1 = S() as sequence of T1;

      

       A2: ex n be Element of NAT st for m be Element of NAT , x be Point of T1 st n <= m & x = (S1 . m) holds P[x] by A1;

      ex n be Element of NAT st for m be Element of NAT st n <= m holds P[((S1 * p()) . m)] from PermSeq( A2);

      hence thesis;

    end;

    theorem :: FRECHET2:37

    

     Th37: for T be non empty TopStruct, S be sequence of T, P be Permutation of NAT , x be 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 be Subset of T st U1 is open & x in U1 holds ex n be Nat st for m be 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 be Element of NAT st for m be Element of NAT , x be Point of T st n <= m & x = (S . m) holds P[x]

        proof

          consider n be Nat such that

           A4: for m be Nat st n <= m holds (S . m) in U1 by A1, A2;

          reconsider n as Element of NAT by ORDINAL1:def 12;

          take n;

          let m be Element of NAT , x be Point of T;

          assume n <= m & x = (S . m);

          hence thesis by A4;

        end;

        consider n be Element of NAT such that

         A5: for m be Element of NAT st n <= m holds P[((S * P) . m)] from PermSeq2( A3);

        take n;

        let m be Nat;

        m in NAT by ORDINAL1:def 12;

        hence thesis by A5;

      end;

      hence thesis;

    end;

    theorem :: FRECHET2:38

    for n0 be Element of NAT holds ex NS be increasing sequence of NAT st for n be Element of NAT holds (NS . n) = (n + n0)

    proof

      let n0 be Element of NAT ;

      deffunc F( Nat) = ($1 + n0);

      consider NS be Real_Sequence such that

       A1: for n be Nat holds (NS . n) = F(n) from SEQ_1:sch 1;

      

       A2: NS is increasing

      proof

        let n be 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 be Nat holds (NS . n) is Element of NAT

      proof

        let n be 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 :: FRECHET2:39

    

     Th39: for T be non empty TopStruct, S be sequence of T, x be Point of T, n0 be 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 Nat;

      assume O is open & x in O;

      then

      consider m0 be Element of NAT such that

       A2: (n + n0) <= m0 and

       A3: (S . m0) in O by A1;

      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 :: FRECHET2:40

    

     Th40: for T be non empty TopStruct, S be sequence of T, x be 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 be 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 be Element of NAT such that 0 <= m and

         A3: (S . m) in G by A1, A2;

        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;

      end;

      hence thesis by PRE_TOPC:def 7;

    end;

    theorem :: FRECHET2:41

    for T be non empty TopStruct st T is Frechet holds for S be sequence of T, x be Point of T st x is_a_cluster_point_of S holds ex S1 be 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 be Point of T : P[y] } as Subset of T from DOMAIN_1:sch 7;

      per cases ;

        suppose

         A3: for n be Element of NAT holds ex m be Element of NAT st m >= n & (S . m) in Y;

        defpred P[ set] means $1 in Y;

        

         A4: for n be Element of NAT holds ex m be Element of NAT st n <= m & P[(S . m)] by A3;

        consider S1 be subsequence of S such that

         A5: for n be Element of NAT holds P[(S1 . n)] from VALUED_1:sch 1( A4);

        take S1;

        ( rng S1) c= Y

        proof

          let y be object;

          assume y in ( rng S1);

          then

          consider n be object 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 be Element of NAT st for m be Element of NAT st m >= n holds not (S . m) in Y;

        then

        consider n0 be Element of NAT such that

         A8: for m be 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 be sequence of T such that

         A9: ( rng S2) c= ( rng S9) and

         A10: x in ( Lim S2) by A1;

        

         A11: S2 is_convergent_to x by A10, FRECHET:def 5;

        

         A12: for n be 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 be object 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;

        then

        consider S29 be 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 be 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

    theorem :: FRECHET2:42

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

    theorem :: FRECHET2:43

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

    theorem :: FRECHET2:44

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

    theorem :: FRECHET2:45

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