cardfil4.miz



    begin

    reserve x for object,

X,Y,Z for set,

i,j,k,l,m,n for Nat,

r,s for Real,

no for Element of OrderedNAT ,

A for Subset of [: NAT , NAT :];

    theorem :: CARDFIL4:1

    

     Th1: for W be finite Subset of X st (X \ W) c= Z holds (X \ Z) is finite

    proof

      let W be finite Subset of X;

      assume (X \ W) c= Z;

      then (X \ Z) c= (X \ (X \ W)) by XBOOLE_1: 34;

      then (X \ Z) c= (X /\ W) by XBOOLE_1: 48;

      hence thesis;

    end;

    theorem :: CARDFIL4:2

    

     Th2: Z c= X & (X \ Z) is finite implies ex W be finite Subset of X st (X \ W) = Z

    proof

      assume that

       A1: Z c= X and

       A2: (X \ Z) is finite;

      (X \ (X \ Z)) = (X /\ Z) by XBOOLE_1: 48

      .= Z by A1, XBOOLE_1: 17, XBOOLE_1: 19;

      hence thesis by A2;

    end;

    theorem :: CARDFIL4:3

    

     Th3: for X1,X2 be set, S1 be Subset-Family of X1, S2 be Subset-Family of X2 holds { s where s be Subset of [:X1, X2:] : ex s1,s2 be set st s1 in S1 & s2 in S2 & s = [:s1, s2:] } is Subset-Family of [:X1, X2:]

    proof

      let X1,X2 be set, S1 be Subset-Family of X1, S2 be Subset-Family of X2;

      set S = { s where s be Subset of [:X1, X2:] : ex s1,s2 be set st s1 in S1 & s2 in S2 & s = [:s1, s2:] };

      S c= ( bool [:X1, X2:])

      proof

        let x be object;

        assume x in S;

        then

        consider s0 be Subset of [:X1, X2:] such that

         A1: x = s0 & ex s1,s2 be set st s1 in S1 & s2 in S2 & s0 = [:s1, s2:];

        thus thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL4:4

    

     Th4: x in [:X, Y:] implies x is pair

    proof

      assume x in [:X, Y:];

      then ex a,b be object st a in X & b in Y & x = [a, b] by ZFMISC_1:def 2;

      hence thesis;

    end;

    theorem :: CARDFIL4:5

    

     Th5: 0 < r implies ex m st m is non zero & (1 / m) < r

    proof

      assume

       A1: 0 < r;

      consider m be Nat such that

       A2: (1 / r) < m by SEQ_4: 3;

      

       A3: 0 < m by A1, A2;

      take m;

      thus m is non zero by A1, A2;

      ((1 / r) * r) < (m * r) by A2, A1, XREAL_1: 68;

      then 1 < (m * r) by A1, XCMPLX_1: 106;

      then (1 / m) < ((m * r) / m) by A3, XREAL_1: 74;

      then (1 / m) < (r * (m / m)) by XCMPLX_1: 74;

      hence thesis by A3, XCMPLX_1: 88;

    end;

    theorem :: CARDFIL4:6

    

     Th6: for x,y be Point of RealSpace holds ex xr,yr be Real st x = xr & y = yr & ( dist (x,y)) = ( real_dist . (x,y)) & ( dist (x,y)) = (( Pitag_dist 1) . ( <*x*>, <*y*>)) & ( dist (x,y)) = |.(xr - yr).|

    proof

      let x,y be Point of RealSpace ;

      reconsider xr = x, yr = y as Real;

      

       A1: ( real_dist . (x,y)) = |.(xr - yr).| by METRIC_1:def 12;

      reconsider x2 = <*xr*>, y2 = <*yr*> as Element of ( REAL 1);

      (x2 . 1) = xr & (y2 . 1) = yr by FINSEQ_1:def 8;

      then (( Pitag_dist 1) . ( <*x*>, <*y*>)) = |.(xr - yr).| by SRINGS_5: 99;

      hence thesis by A1;

    end;

    theorem :: CARDFIL4:7

    

     Th7: for x,y be Point of ( TopSpaceMetr ( Euclid 1)) holds ex x1,y1 be Point of RealSpace , xr,yr be Real st x1 = xr & y1 = yr & x = <*xr*> & y = <*yr*> & ( dist (x1,y1)) = ( real_dist . (xr,yr)) & ( dist (x1,y1)) = (( Pitag_dist 1) . ( <*xr*>, <*yr*>)) & ( dist (x1,y1)) = |.(xr - yr).|

    proof

      let x,y be Point of ( TopSpaceMetr ( Euclid 1));

      reconsider xr1 = x as Point of ( Euclid 1);

      xr1 in (1 -tuples_on REAL );

      then xr1 in the set of all <*r*> where r be Element of REAL by FINSEQ_2: 96;

      then

      consider r1 be Element of REAL such that

       A1: xr1 = <*r1*>;

      reconsider yr1 = y as Point of ( Euclid 1);

      yr1 in (1 -tuples_on REAL );

      then yr1 in the set of all <*r*> where r be Element of REAL by FINSEQ_2: 96;

      then

      consider r2 be Element of REAL such that

       A2: yr1 = <*r2*>;

      reconsider xr2 = r1, yr2 = r2 as Element of RealSpace ;

      reconsider x2 = <*r1*>, y2 = <*r2*> as Element of ( REAL 1);

      

       A3: (x2 . 1) = r1 by FINSEQ_1:def 8;

      

       A4: (( Pitag_dist 1) . ( <*r1*>, <*r2*>)) = |.((x2 . 1) - (y2 . 1)).| by SRINGS_5: 99

      .= |.(r1 - r2).| by A3, FINSEQ_1:def 8;

      take xr2, yr2;

      take r1, r2;

      thus thesis by A4, A1, A2, METRIC_1:def 12;

    end;

    theorem :: CARDFIL4:8

    

     Th8: for x,y be Point of ( Euclid 1), r,s be Real st x = <*r*> & y = <*s*> holds ( dist (x,y)) = |.(r - s).|

    proof

      let x,y be Point of ( Euclid 1), r,s be Real;

      assume that

       A1: x = <*r*> and

       A2: y = <*s*>;

      consider x1,y1 be Point of RealSpace , xr,yr be Real such that x1 = xr and y1 = yr and

       A3: x = <*xr*> and

       A4: y = <*yr*> and ( dist (x1,y1)) = ( real_dist . (xr,yr)) and

       A5: ( dist (x1,y1)) = (( Pitag_dist 1) . ( <*xr*>, <*yr*>)) and

       A6: ( dist (x1,y1)) = |.(xr - yr).| by Th7;

      xr = r & yr = s by A3, A1, A2, A4, FINSEQ_1: 76;

      hence thesis by A5, A6, A3, A4;

    end;

    registration

      cluster [: NAT , NAT :] -> countable;

      coherence by CARD_4: 7;

    end

    registration

      cluster [: NAT , NAT :] -> denumerable;

      coherence ;

    end

    theorem :: CARDFIL4:9

    

     Th9: the set of all [ 0 , n] where n be Nat is infinite

    proof

      deffunc F( object) = [ 0 , $1];

      consider f be Function such that

       A1: ( dom f) = NAT and

       A2: for x be object st x in NAT holds (f . x) = F(x) from FUNCT_1:sch 3;

      

       A3: f is one-to-one

      proof

        now

          let x,y be object;

          assume that

           A4: x in ( dom f) and

           A5: y in ( dom f) and

           A6: (f . x) = (f . y);

          (f . y) = [ 0 , y] by A5, A1, A2;

          then [ 0 , x] = [ 0 , y] by A6, A4, A1, A2;

          hence x = y by XTUPLE_0: 1;

        end;

        hence thesis by FUNCT_1:def 4;

      end;

      ( rng f) = the set of all [ 0 , n] where n be Nat

      proof

        

         A7: ( rng f) c= the set of all [ 0 , n] where n be Nat

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A8: y in ( dom f) and

           A9: x = (f . y) by FUNCT_1:def 3;

          reconsider z = y as Nat by A8, A1;

          x = [ 0 , z] by A9, A2, A1, A8;

          hence thesis;

        end;

         the set of all [ 0 , n] where n be Nat c= ( rng f)

        proof

          let x be object;

          assume x in the set of all [ 0 , n] where n be Nat;

          then

          consider n such that

           A10: x = [ 0 , n];

          n in ( dom f) & (f . n) = [ 0 , n] by A1, A2, ORDINAL1:def 12;

          hence thesis by A10, FUNCT_1: 3;

        end;

        hence thesis by A7;

      end;

      hence thesis by A1, A3, CARD_1: 59;

    end;

    theorem :: CARDFIL4:10

    i <= k & j <= l implies [:( Segm i), ( Segm j):] c= [:( Segm k), ( Segm l):]

    proof

      assume that

       A1: i <= k and

       A2: j <= l;

      now

        let x be object;

        assume x in [:( Segm i), ( Segm j):];

        then

        consider xi,xj be object such that

         A3: xi in ( Segm i) and

         A4: xj in ( Segm j) and

         A5: x = [xi, xj] by ZFMISC_1:def 2;

        reconsider xi, xj as Nat by A3, A4;

        xi < k & xj < l by A1, A2, A3, A4, NAT_1: 44, XXREAL_0: 2;

        then xi in ( Segm k) & xj in ( Segm l) by NAT_1: 44;

        hence x in [:( Segm k), ( Segm l):] by A5, ZFMISC_1:def 2;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL4:11

    

     Th10: [:( NAT \ ( Segm m)), ( NAT \ ( Segm n)):] c= ( [: NAT , NAT :] \ [:( Segm m), ( Segm n):])

    proof

      

       A1: ( [: NAT , NAT :] \ [:( Segm m), ( Segm n):]) = ( [:( NAT \ ( Segm m)), NAT :] \/ [: NAT , ( NAT \ ( Segm n)):]) by ZFMISC_1: 103;

       [:( NAT \ ( Segm m)), ( NAT \ ( Segm n)):] = ( [:( NAT \ ( Segm m)), NAT :] \ [:( NAT \ ( Segm m)), ( Segm n):]) by ZFMISC_1: 102;

      hence thesis by A1, XBOOLE_1: 10;

    end;

    theorem :: CARDFIL4:12

    

     Th11: n = no & n <= m implies m in ( uparrow no)

    proof

      assume that

       A1: no = n and

       A2: n <= m;

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

      reconsider p0 = no as Element of NAT ;

      m in { x where x be Element of NAT : ex p0 be Element of NAT st no = p0 & p0 <= x } by A1, A2;

      hence thesis by CARDFIL2: 50;

    end;

    theorem :: CARDFIL4:13

    

     Th12: n = no & m in ( uparrow no) implies n <= m

    proof

      assume that

       A1: n = no and

       A2: m in ( uparrow no);

      m in { x where x be Element of NAT : ex p0 be Element of NAT st no = p0 & p0 <= x } by A2, CARDFIL2: 50;

      then ex x be Element of NAT st m = x & ex p0 be Element of NAT st no = p0 & p0 <= x;

      hence thesis by A1;

    end;

    theorem :: CARDFIL4:14

    

     Th13: n = no implies ( uparrow no) = ( NAT \ ( Segm n))

    proof

      assume

       A1: n = no;

      

       A2: ( uparrow no) c= ( NAT \ ( Segm n))

      proof

        let x be object;

        assume

         A3: x in ( uparrow no);

        then x in { x where x be Element of NAT : ex p0 be Element of NAT st no = p0 & p0 <= x } by CARDFIL2: 50;

        then ex y be Element of NAT st y = x & ex p0 be Element of NAT st no = p0 & p0 <= y;

        then

        reconsider y = x as Element of NAT ;

         not y in ( Segm n) by A1, A3, Th12, NAT_1: 44;

        hence thesis by XBOOLE_0:def 5;

      end;

      ( NAT \ ( Segm n)) c= ( uparrow no)

      proof

        let x be object;

        assume

         A4: x in ( NAT \ ( Segm n));

        then

         A5: x in NAT & not x in ( Segm n) by XBOOLE_0:def 5;

        reconsider y = x as Element of NAT by A4;

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

        n1 <= y & n1 = no by A1, A5, NAT_1: 44;

        then y in { x where x be Element of NAT : ex p0 be Element of NAT st no = p0 & p0 <= x };

        hence thesis by CARDFIL2: 50;

      end;

      hence thesis by A2;

    end;

    theorem :: CARDFIL4:15

    

     Th14: ( proj1 A) = { x where x be Element of NAT : ex y be Element of NAT st [x, y] in A }

    proof

      set A1 = { x where x be Element of NAT : ex y be Element of NAT st [x, y] in A };

      

       A1: ( proj1 A) c= A1

      proof

        let x be object;

        assume x in ( proj1 A);

        then

        consider y be object such that

         A2: [x, y] in A by XTUPLE_0:def 12;

        ex x1,y1 be object st x1 in NAT & y1 in NAT & [x, y] = [x1, y1] by A2, ZFMISC_1:def 2;

        then

        reconsider x, y as Element of NAT by XTUPLE_0: 1;

         [x, y] in A & y is Element of NAT by A2;

        hence thesis;

      end;

      A1 c= ( proj1 A)

      proof

        let x be object;

        assume x in A1;

        then ex x1 be Element of NAT st x = x1 & ex y be Element of NAT st [x1, y] in A;

        hence thesis by XTUPLE_0:def 12;

      end;

      hence thesis by A1;

    end;

    theorem :: CARDFIL4:16

    

     Th15: ( proj2 A) = { y where y be Element of NAT : ex x be Element of NAT st [x, y] in A }

    proof

      set A2 = { y where y be Element of NAT : ex x be Element of NAT st [x, y] in A };

      

       A1: ( proj2 A) c= A2

      proof

        let y be object;

        assume y in ( proj2 A);

        then

        consider x be object such that

         A2: [x, y] in A by XTUPLE_0:def 13;

        ex x1,y1 be object st x1 in NAT & y1 in NAT & [x, y] = [x1, y1] by A2, ZFMISC_1:def 2;

        then

        reconsider x, y as Element of NAT by XTUPLE_0: 1;

         [x, y] in A & y is Element of NAT by A2;

        hence thesis;

      end;

      A2 c= ( proj2 A)

      proof

        let y be object;

        assume y in A2;

        then ex y1 be Element of NAT st y = y1 & ex x be Element of NAT st [x, y1] in A;

        hence thesis by XTUPLE_0:def 13;

      end;

      hence thesis by A1;

    end;

    theorem :: CARDFIL4:17

    

     Th16: for A be finite Subset of [: NAT , NAT :] holds ex m, n st A c= [:( Segm m), ( Segm n):]

    proof

      let A be finite Subset of [: NAT , NAT :];

      per cases ;

        suppose A is empty;

        then A c= [:( Segm 0 ), ( Segm 0 ):];

        hence thesis;

      end;

        suppose

         A1: A is non empty;

        set A1 = { x where x be Element of NAT : ex y be Element of NAT st [x, y] in A };

        

         A2: A1 is non empty

        proof

          set n = the Element of A;

          n in A by A1;

          then

          consider x,y be object such that

           A3: x in NAT and

           A4: y in NAT and

           A5: n = [x, y] by ZFMISC_1:def 2;

          reconsider x, y as Element of NAT by A3, A4;

          x in A1 by A4, A5, A1;

          hence thesis;

        end;

        A1 c= NAT

        proof

          let t be object;

          assume t in A1;

          then ex x be Element of NAT st t = x & ex y be Element of NAT st [x, y] in A;

          hence thesis;

        end;

        then

        reconsider B1 = A1 as non empty ext-real-membered set by A2;

        reconsider A as Relation;

        ( proj1 A) is finite;

        then B1 is finite by Th14;

        then ( sup B1) in A1 by XXREAL_2:def 6;

        then

        consider x1 be Element of NAT such that

         A6: ( sup B1) = x1 and ex y be Element of NAT st [x1, y] in A;

        set A2 = { y where y be Element of NAT : ex x be Element of NAT st [x, y] in A };

        

         A7: A2 is non empty

        proof

          set n = the Element of A;

          n in A by A1;

          then

          consider x,y be object such that

           A8: x in NAT and

           A9: y in NAT and

           A10: n = [x, y] by ZFMISC_1:def 2;

          reconsider x, y as Element of NAT by A8, A9;

          y in A2 by A8, A10, A1;

          hence thesis;

        end;

        A2 c= NAT

        proof

          let t be object;

          assume t in A2;

          then ex y be Element of NAT st t = y & ex x be Element of NAT st [x, y] in A;

          hence thesis;

        end;

        then

        reconsider B2 = A2 as non empty ext-real-membered set by A7;

        reconsider A as Relation;

        ( proj2 A) is finite;

        then B2 is finite by Th15;

        then ( sup B2) in A2 by XXREAL_2:def 6;

        then

        consider y1 be Element of NAT such that

         A11: ( sup B2) = y1 and ex x be Element of NAT st [x, y1] in A;

        A c= [:( Segm (x1 + 1)), ( Segm (y1 + 1)):]

        proof

          let t be object;

          assume

           A12: t in A;

          then

          reconsider u = t as Element of [: NAT , NAT :];

          consider x,y be object such that

           A13: x in NAT and

           A14: y in NAT and

           A15: u = [x, y] by ZFMISC_1:def 2;

          reconsider x2 = x, y2 = y as Element of NAT by A13, A14;

          x2 in A1 by A12, A14, A15;

          then x2 <= ( sup B1) by XXREAL_2: 4;

          then x2 < (x1 + 1) by A6, NAT_1: 13;

          then

           A16: x2 in ( Segm (x1 + 1)) by NAT_1: 44;

          y2 in A2 by A12, A13, A15;

          then y2 <= ( sup B2) by XXREAL_2: 4;

          then y2 < (y1 + 1) by A11, NAT_1: 13;

          then y2 in ( Segm (y1 + 1)) by NAT_1: 44;

          hence thesis by A16, A15, ZFMISC_1:def 2;

        end;

        hence thesis;

      end;

    end;

    theorem :: CARDFIL4:18

    

     Th17: for X be non empty set, cF be Filter of X holds cF is proper Filter of ( BoolePoset X)

    proof

      let X be non empty set, cF be Filter of X;

      reconsider cF as non empty Subset of ( BooleLatt X) by LATTICE3:def 1;

      reconsider cF as Filter of ( BoolePoset X) by CARDFIL2: 73, CARDFIL2: 75;

       not {} in cF by CARD_FIL:def 1;

      then not ( Bottom ( BoolePoset X)) in cF by YELLOW_1: 18;

      hence thesis by WAYBEL_7: 4;

    end;

    theorem :: CARDFIL4:19

    

     Th18: for X be non empty set, cF be Filter of X holds ex cB be filter_base of X st cB = cF & <.cB.) = cF

    proof

      let X be non empty set, cF be Filter of X;

      cF is basis of cF by CARDFIL2: 13;

      then

      reconsider cB = cF as filter_base of X by CARDFIL2: 29;

      take cB;

      now

        hereby

          let x be object;

          assume

           A1: x in <.cB.);

          then

          reconsider y = x as Subset of X;

          ex b be Element of cB st b c= y by A1, CARDFIL2:def 8;

          hence x in cF by CARD_FIL:def 1;

        end;

        let x be object;

        assume x in cF;

        hence x in <.cB.) by CARDFIL2:def 8;

      end;

      then <.cB.) c= cF & cF c= <.cB.);

      hence thesis;

    end;

    theorem :: CARDFIL4:20

    

     Th19: for T be non empty TopSpace, cF be Filter of the carrier of T st x in ( lim_filter cF) holds x is_a_cluster_point_of (cF,T)

    proof

      let T be non empty TopSpace, cF be Filter of the carrier of T;

      assume

       A1: x in ( lim_filter cF);

      now

        let A be Subset of T;

        assume that

         A2: A is open and

         A3: x in A;

        

         A4: A in cF by A1, A3, A2, CARDFIL2: 80, WAYBEL_7:def 5;

         not {} in cF by CARD_FIL:def 1;

        hence for B be set st B in cF holds A meets B by A4, CARD_FIL:def 1;

      end;

      hence thesis by WAYBEL_7:def 4;

    end;

    theorem :: CARDFIL4:21

    

     Th20: for B be Element of base_of_frechet_filter holds ex n st B = ( NAT \ ( Segm n))

    proof

      let B be Element of base_of_frechet_filter ;

      B in ( # ( Tails OrderedNAT ));

      then

      consider no such that

       A1: B = ( uparrow no);

      reconsider n = no as Nat;

      take n;

      thus thesis by A1, Th13;

    end;

    theorem :: CARDFIL4:22

    

     Th21: for B be Subset of NAT st B = ( NAT \ ( Segm n)) holds B is Element of base_of_frechet_filter

    proof

      let B be Subset of NAT ;

      assume

       A1: B = ( NAT \ ( Segm n));

      reconsider no = n as Element of OrderedNAT by ORDINAL1:def 12;

      B = ( uparrow no) by A1, Th13;

      then B in ( # ( Tails OrderedNAT ));

      hence thesis;

    end;

    begin

    reserve X,Y,X1,X2 for non empty set,

cA1,cB1 for filter_base of X1,

cA2,cB2 for filter_base of X2,

cF1 for Filter of X1,

cF2 for Filter of X2,

cBa1 for basis of cF1,

cBa2 for basis of cF2;

    definition

      let X1,X2 be non empty set, cB1 be filter_base of X1, cB2 be filter_base of X2;

      :: CARDFIL4:def1

      func [:cB1,cB2:] -> filter_base of [:X1, X2:] equals the set of all [:B1, B2:] where B1 be Element of cB1, B2 be Element of cB2;

      coherence

      proof

        set cB12 = the set of all [:B1, B2:] where B1 be Element of cB1, B2 be Element of cB2;

        reconsider cB1a = cB1 as non empty Subset-Family of X1;

        reconsider cB2a = cB2 as non empty Subset-Family of X2;

        set cB12a = the set of all [:B1, B2:] where B1 be Element of cB1a, B2 be Element of cB2a;

         the set of all [:B1, B2:] where B1 be Element of cB1a, B2 be Element of cB2a = { s where s be Subset of [:X1, X2:] : ex x1,x2 be set st x1 in cB1a & x2 in cB2a & s = [:x1, x2:] } by SRINGS_2: 2;

        then

        reconsider cB12 as Subset-Family of [:X1, X2:] by Th3;

        now

          thus

           A1: cB12 is non empty

          proof

            set B1 = the Element of cB1a, B2 = the Element of cB2a;

             [:B1, B2:] in cB12;

            hence thesis;

          end;

          thus cB12 is with_non-empty_elements

          proof

            assume not cB12 is with_non-empty_elements;

            then {} in cB12 by SETFAM_1:def 8;

            then ex B1 be Element of cB1a, B2 be Element of cB2a st {} = [:B1, B2:];

            hence contradiction;

          end;

          thus cB12 is quasi_basis

          proof

            hereby

              let b1,b2 be Element of cB12;

              b1 in cB12 by A1;

              then

              consider b11 be Element of cB1, b12 be Element of cB2 such that

               A2: b1 = [:b11, b12:];

              b2 in cB12 by A1;

              then

              consider b21 be Element of cB1, b22 be Element of cB2 such that

               A3: b2 = [:b21, b22:];

              cB1 is quasi_basis;

              then

              consider a1 be Element of cB1 such that

               A4: a1 c= (b11 /\ b21);

              cB2 is quasi_basis;

              then

              consider a2 be Element of cB2 such that

               A5: a2 c= (b12 /\ b22);

               [:a1, a2:] in cB12;

              then

              reconsider b = [:a1, a2:] as Element of cB12;

               [:a1, a2:] c= [:(b11 /\ b21), a2:] & [:(b11 /\ b21), a2:] c= [:(b11 /\ b21), (b12 /\ b22):] by A4, A5, ZFMISC_1: 95;

              then [:a1, a2:] c= [:(b11 /\ b21), (b12 /\ b22):];

              then b c= (b1 /\ b2) by A2, A3, ZFMISC_1: 100;

              hence ex b be Element of cB12 st b c= (b1 /\ b2);

            end;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: CARDFIL4:23

    

     Th22: cF1 = <.cB1.) & cF1 = <.cA1.) & cF2 = <.cB2.) & cF2 = <.cA2.) implies <. [:cB1, cB2:].) = <. [:cA1, cA2:].)

    proof

      assume that

       A1: cF1 = <.cB1.) and

       A2: cF1 = <.cA1.) and

       A3: cF2 = <.cB2.) and

       A4: cF2 = <.cA2.);

      

       A5: (cB1,cA1) are_equivalent_generators by A1, A2, CARDFIL2: 26;

      

       A6: (cB2,cA2) are_equivalent_generators by A3, A4, CARDFIL2: 26;

      now

        hereby

          let B be Element of [:cB1, cB2:];

          B in [:cB1, cB2:];

          then

          consider B1 be Element of cB1, B2 be Element of cB2 such that

           A7: B = [:B1, B2:];

          consider B1A1 be Element of cA1 such that

           A8: B1A1 c= B1 by A5;

          consider B2A2 be Element of cA2 such that

           A9: B2A2 c= B2 by A6;

           [:B1A1, B2A2:] in [:cA1, cA2:];

          then

          reconsider A = [:B1A1, B2A2:] as Element of [:cA1, cA2:];

           [:B1A1, B2A2:] c= [:B1, B2A2:] & [:B1, B2A2:] c= [:B1, B2:] by A8, A9, ZFMISC_1: 95;

          then A c= B by A7;

          hence ex A be Element of [:cA1, cA2:] st A c= B;

        end;

        hereby

          let A be Element of [:cA1, cA2:];

          A in [:cA1, cA2:];

          then

          consider A1 be Element of cA1, A2 be Element of cA2 such that

           A10: A = [:A1, A2:];

          consider A1B1 be Element of cB1 such that

           A11: A1B1 c= A1 by A5;

          consider A2B2 be Element of cB2 such that

           A12: A2B2 c= A2 by A6;

           [:A1B1, A2B2:] in [:cB1, cB2:];

          then

          reconsider B = [:A1B1, A2B2:] as Element of [:cB1, cB2:];

           [:A1B1, A2B2:] c= [:A1, A2B2:] & [:A1, A2B2:] c= [:A1, A2:] by A11, A12, ZFMISC_1: 95;

          then B c= A by A10;

          hence ex B be Element of [:cB1, cB2:] st B c= A;

        end;

      end;

      then ( [:cB1, cB2:], [:cA1, cA2:]) are_equivalent_generators ;

      hence thesis by CARDFIL2: 20;

    end;

    theorem :: CARDFIL4:24

    

     Th23: cBa1 = cB1 implies <.cB1.] = cF1

    proof

      assume

       A1: cBa1 = cB1;

      cF1 = <.( # cBa1).] by CARDFIL2: 21;

      hence thesis by A1;

    end;

    theorem :: CARDFIL4:25

    

     Th24: ex cB1 st <.cB1.) = cF1

    proof

      

       A1: cF1 is basis of cF1 by CARDFIL2: 13;

      then

      reconsider cB1 = cF1 as filter_base of X1 by CARDFIL2: 29;

       <.cB1.) = <.cB1.];

      hence thesis by A1, Th23;

    end;

    definition

      let X1,X2 be non empty set, cF1 be Filter of X1, cF2 be Filter of X2;

      :: CARDFIL4:def2

      func <.cF1,cF2.) -> Filter of [:X1, X2:] means

      : Def1: ex cB1 be filter_base of X1, cB2 be filter_base of X2 st <.cB1.) = cF1 & <.cB2.) = cF2 & it = <. [:cB1, cB2:].);

      existence

      proof

        consider cB1 be filter_base of X1 such that

         A1: <.cB1.) = cF1 by Th24;

        consider cB2 be filter_base of X2 such that

         A2: <.cB2.) = cF2 by Th24;

         <. [:cB1, cB2:].) is Filter of [:X1, X2:];

        hence thesis by A1, A2;

      end;

      uniqueness by Th22;

    end

    definition

      let X1,X2 be non empty set, cF1 be Filter of X1, cF2 be Filter of X2, cB1 be basis of cF1, cB2 be basis of cF2;

      :: CARDFIL4:def3

      func [:cB1,cB2:] -> basis of <.cF1, cF2.) means

      : Def2: ex cB3 be filter_base of X1, cB4 be filter_base of X2 st cB1 = cB3 & cB2 = cB4 & it = [:cB3, cB4:];

      existence

      proof

        reconsider cB3 = cB1 as filter_base of X1 by CARDFIL2: 29;

        reconsider cB4 = cB2 as filter_base of X2 by CARDFIL2: 29;

        reconsider cF1F2 = <.cF1, cF2.) as Filter of [:X1, X2:];

        consider cB5 be filter_base of X1, cB6 be filter_base of X2 such that

         A1: <.cB5.) = cF1 and

         A2: <.cB6.) = cF2 and

         A3: cF1F2 = <. [:cB5, cB6:].) by Def1;

        

         A4: <.cB3.) = cF1 & <.cB4.) = cF2 by Th23;

         [:cB3, cB4:] c= <. [:cB3, cB4:].) by CARDFIL2: 18;

        then

        reconsider cB3B4 = [:cB3, cB4:] as non empty Subset of cF1F2 by A4, A1, A2, A3, Th22;

        cB3B4 is filter_basis

        proof

          let f be Element of cF1F2;

          f is Element of <. [:cB3, cB4:].) by A4, A1, A2, A3, Th22;

          hence thesis by CARDFIL2:def 8;

        end;

        hence thesis;

      end;

      uniqueness ;

    end

    definition

      let n be Nat;

      :: CARDFIL4:def4

      func square-uparrow n -> Subset of [: NAT , NAT :] means

      : Def3: for x be Element of [: NAT , NAT :] holds x in it iff ex n1,n2 be Nat st n1 = (x `1 ) & n2 = (x `2 ) & n <= n1 & n <= n2;

      existence

      proof

        defpred P[ Element of [: NAT , NAT :]] means ex n1,n2 be Nat st n1 = ($1 `1 ) & n2 = ($1 `2 ) & n <= n1 & n <= n2;

        ex B be Subset of [: NAT , NAT :] st for x be Element of [: NAT , NAT :] holds x in B iff P[x] from SUBSET_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let x1,x2 be Subset of [: NAT , NAT :] such that

         A1: for x be Element of [: NAT , NAT :] holds x in x1 iff ex n1,n2 be Nat st n1 = (x `1 ) & n2 = (x `2 ) & n <= n1 & n <= n2 and

         A2: for x be Element of [: NAT , NAT :] holds x in x2 iff ex n1,n2 be Nat st n1 = (x `1 ) & n2 = (x `2 ) & n <= n1 & n <= n2;

        x1 = x2

        proof

          thus x1 c= x2

          proof

            let t be object;

            assume

             A3: t in x1;

            then

            reconsider u = t as Element of [: NAT , NAT :];

            ex n1,n2 be Nat st n1 = (u `1 ) & n2 = (u `2 ) & n <= n1 & n <= n2 by A3, A1;

            hence t in x2 by A2;

          end;

          let t be object;

          assume

           A4: t in x2;

          then

          reconsider u = t as Element of [: NAT , NAT :];

          ex n1,n2 be Nat st n1 = (u `1 ) & n2 = (u `2 ) & n <= n1 & n <= n2 by A4, A2;

          hence t in x1 by A1;

        end;

        hence thesis;

      end;

    end

    theorem :: CARDFIL4:26

    

     Th25: [n, n] in ( square-uparrow n)

    proof

      n in NAT by ORDINAL1:def 12;

      then

      reconsider x = [n, n] as Element of [: NAT , NAT :] by ZFMISC_1:def 2;

      (x `1 ) = n & (x `2 ) = n;

      hence thesis by Def3;

    end;

    registration

      let n;

      cluster ( square-uparrow n) -> non empty;

      coherence by Th25;

    end

    theorem :: CARDFIL4:27

     [i, j] in ( square-uparrow n) implies [(i + k), j] in ( square-uparrow n) & [i, (j + l)] in ( square-uparrow n)

    proof

      assume [i, j] in ( square-uparrow n);

      then

      consider i1,j1 be Nat such that

       A1: i1 = ( [i, j] `1 ) and

       A2: j1 = ( [i, j] `2 ) and

       A3: n <= i1 and

       A4: n <= j1 by Def3;

      i <= (i + k) & j <= (j + l) by NAT_1: 11;

      then

       A5: n <= (i + k) & n <= (j + l) by A1, A2, A3, A4, XXREAL_0: 2;

      i in NAT & (i + k) in NAT & j in NAT & (j + l) in NAT by ORDINAL1:def 12;

      then

      reconsider x = [(i + k), j], y = [i, (j + l)] as Element of [: NAT , NAT :] by ZFMISC_1:def 2;

      now

        ex i2,j1 be Nat st i2 = (x `1 ) & j1 = (x `2 ) & n <= (i + k) & n <= j by A2, A4, A5;

        hence x in ( square-uparrow n) by Def3;

        ex i1,j2 be Nat st i1 = (y `1 ) & j2 = (y `2 ) & n <= i & n <= (j + l) by A1, A3, A5;

        hence y in ( square-uparrow n) by Def3;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL4:28

    ( square-uparrow n) is infinite Subset of [: NAT , NAT :]

    proof

      assume not ( square-uparrow n) is infinite Subset of [: NAT , NAT :];

      then

      reconsider A = ( square-uparrow n) as finite Subset of [: NAT , NAT :];

      consider i,j be Nat such that

       A1: A c= [:( Segm i), ( Segm j):] by Th16;

      consider k,l be Nat such that k = ( [n, n] `1 ) and l = ( [n, n] `2 ) and

       A2: n <= k and

       A3: n <= l;

      k <= (k + i) & l <= (l + j) by NAT_1: 11;

      then

       A4: n <= (k + i) & n <= (l + j) by XXREAL_0: 2, A2, A3;

      (k + i) in NAT & (l + j) in NAT by ORDINAL1:def 12;

      then

      reconsider y = [(k + i), (l + j)] as Element of [: NAT , NAT :] by ZFMISC_1:def 2;

      (y `1 ) = (k + i) & (y `2 ) = (l + j);

      then y in ( square-uparrow n) by Def3, A4;

      then ex a,b be object st a in ( Segm i) & b in ( Segm j) & y = [a, b] by A1, ZFMISC_1:def 2;

      then (k + i) in ( Segm i) & (l + j) in ( Segm j) by XTUPLE_0: 1;

      then ((k + i) - i) < (i - i) & ((l + j) - j) < (j - j) by NAT_1: 44, XREAL_1: 14;

      then k < 0 & l < 0 ;

      hence thesis;

    end;

    theorem :: CARDFIL4:29

    

     Th26: no = n implies ( square-uparrow n) = [:( uparrow no), ( uparrow no):]

    proof

      assume

       A1: no = n;

      thus ( square-uparrow n) c= [:( uparrow no), ( uparrow no):]

      proof

        let x be object;

        assume

         A3: x in ( square-uparrow n);

        then

        reconsider y = x as Element of [: NAT , NAT :];

        consider n1,n2 be Nat such that

         A4: n1 = (y `1 ) and

         A5: n2 = (y `2 ) and

         A6: n <= n1 and

         A7: n <= n2 by A3, Def3;

        

         A8: n1 in ( uparrow no) & n2 in ( uparrow no) by A1, A6, A7, Th11;

        ex x1,x2 be object st x1 in NAT & x2 in NAT & x = [x1, x2] by A3, ZFMISC_1:def 2;

        then

        reconsider z = x as pair object;

        z = [n1, n2] by A4, A5;

        hence thesis by A8, ZFMISC_1:def 2;

      end;

      let x be object;

      assume x in [:( uparrow no), ( uparrow no):];

      then

      consider y1,y2 be object such that

       A9: y1 in ( uparrow no) and

       A10: y2 in ( uparrow no) and

       A11: x = [y1, y2] by ZFMISC_1:def 2;

      reconsider x as Element of [: NAT , NAT :] by A9, A10, A11, ZFMISC_1:def 2;

      reconsider y1, y2 as Nat by A9, A10;

      

       A12: n <= y1 & n <= y2 by A1, A9, A10, Th12;

      (x `1 ) = y1 & (x `2 ) = y2 by A11;

      hence thesis by A12, Def3;

    end;

    theorem :: CARDFIL4:30

    m = (n - 1) implies ( square-uparrow n) c= ( [: NAT , NAT :] \ [:( Seg m), ( Seg m):])

    proof

      assume

       A1: m = (n - 1);

      let x be object;

      assume

       A2: x in ( square-uparrow n);

      then

      reconsider y = x as Element of [: NAT , NAT :];

      consider n1,n2 be Nat such that

       A3: n1 = (y `1 ) and

       A4: n2 = (y `2 ) and

       A5: n <= n1 and n <= n2 by A2, Def3;

       not x in [:( Seg m), ( Seg m):]

      proof

        assume x in [:( Seg m), ( Seg m):];

        then ex x1,x2 be object st x1 in ( Seg m) & x2 in ( Seg m) & x = [x1, x2] by ZFMISC_1:def 2;

        then n1 <= m & n2 <= m by A3, A4, FINSEQ_1: 1;

        then n <= m by A5, XXREAL_0: 2;

        then (n - n) <= ((n - 1) - n) by A1, XREAL_1: 9;

        then 0 <= ( - 1);

        hence thesis;

      end;

      hence thesis by A2, XBOOLE_0:def 5;

    end;

    theorem :: CARDFIL4:31

    ( square-uparrow n) c= ( [: NAT , NAT :] \ [:( Segm n), ( Segm n):])

    proof

      let x be object;

      assume

       A1: x in ( square-uparrow n);

      then

      reconsider y = x as Element of [: NAT , NAT :];

      consider n1,n2 be Nat such that

       A2: n1 = (y `1 ) and

       A3: n2 = (y `2 ) and

       A4: n <= n1 and n <= n2 by A1, Def3;

       not x in [:( Segm n), ( Segm n):]

      proof

        assume x in [:( Segm n), ( Segm n):];

        then ex x1,x2 be object st x1 in ( Segm n) & x2 in ( Segm n) & x = [x1, x2] by ZFMISC_1:def 2;

        then n1 <= (n - 1) & n2 <= (n - 1) by A2, A3, STIRL2_1: 10;

        then n <= (n - 1) by A4, XXREAL_0: 2;

        then (n - n) <= ((n - 1) - n) by XREAL_1: 9;

        then 0 <= ( - 1);

        hence thesis;

      end;

      hence thesis by A1, XBOOLE_0:def 5;

    end;

    theorem :: CARDFIL4:32

    

     Th27: ( square-uparrow n) = [:( NAT \ ( Segm n)), ( NAT \ ( Segm n)):]

    proof

      reconsider no = n as Element of OrderedNAT by ORDINAL1:def 12;

      ( uparrow no) = ( NAT \ ( Segm n)) by Th13;

      hence thesis by Th26;

    end;

    theorem :: CARDFIL4:33

    

     Th28: ex n st ( square-uparrow n) c= [:( NAT \ ( Segm i)), ( NAT \ ( Segm j)):]

    proof

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

      take n;

      let x be object;

      assume

       A1: x in ( square-uparrow n);

      then

      reconsider y = x as Element of [: NAT , NAT :];

      consider n1,n2 be Nat such that

       A2: (y `1 ) = n1 and

       A3: (y `2 ) = n2 and

       A4: n <= n1 and

       A5: n <= n2 by A1, Def3;

      

       A6: y is pair by Th4;

      i <= n by XXREAL_0: 25;

      then

       A7: not n1 in ( Segm i) by A4, XXREAL_0: 2, NAT_1: 44;

      n1 in NAT by ORDINAL1:def 12;

      then

       A8: n1 in ( NAT \ ( Segm i)) by A7, XBOOLE_0:def 5;

      j <= n by XXREAL_0: 25;

      then

       A9: not n2 in ( Segm j) by A5, XXREAL_0: 2, NAT_1: 44;

      n2 in NAT by ORDINAL1:def 12;

      then n2 in ( NAT \ ( Segm j)) by A9, XBOOLE_0:def 5;

      hence thesis by A2, A3, A6, A8, ZFMISC_1:def 2;

    end;

    theorem :: CARDFIL4:34

    

     Th29: n = ( max (i,j)) implies ( square-uparrow n) c= (( square-uparrow i) /\ ( square-uparrow j))

    proof

      assume

       A1: n = ( max (i,j));

      let x be object;

      assume

       A2: x in ( square-uparrow n);

      then

      reconsider y = x as Element of [: NAT , NAT :];

      consider n1,n2 be Nat such that

       A3: n1 = (y `1 ) and

       A4: n2 = (y `2 ) and

       A5: n <= n1 and

       A6: n <= n2 by A2, Def3;

      i <= n & j <= n by A1, XXREAL_0: 25;

      then i <= n1 & j <= n1 & i <= n2 & j <= n2 by A5, A6, XXREAL_0: 2;

      then y in ( square-uparrow i) & y in ( square-uparrow j) by A3, A4, Def3;

      hence thesis by XBOOLE_0:def 4;

    end;

    definition

      let n be Nat;

      :: CARDFIL4:def5

      func square-downarrow n -> Subset of [: NAT , NAT :] means

      : Def4: for x be Element of [: NAT , NAT :] holds x in it iff ex n1,n2 be Nat st n1 = (x `1 ) & n2 = (x `2 ) & n1 < n & n2 < n;

      existence

      proof

        defpred P[ Element of [: NAT , NAT :]] means ex n1,n2 be Nat st n1 = ($1 `1 ) & n2 = ($1 `2 ) & n1 < n & n2 < n;

        ex B be Subset of [: NAT , NAT :] st for x be Element of [: NAT , NAT :] holds x in B iff P[x] from SUBSET_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let x1,x2 be Subset of [: NAT , NAT :] such that

         A1: for x be Element of [: NAT , NAT :] holds x in x1 iff ex n1,n2 be Nat st n1 = (x `1 ) & n2 = (x `2 ) & n1 < n & n2 < n and

         A2: for x be Element of [: NAT , NAT :] holds x in x2 iff ex n1,n2 be Nat st n1 = (x `1 ) & n2 = (x `2 ) & n1 < n & n2 < n;

        thus x1 c= x2

        proof

          let t be object;

          assume

           A3: t in x1;

          then

          reconsider u = t as Element of [: NAT , NAT :];

          ex n1,n2 be Nat st n1 = (u `1 ) & n2 = (u `2 ) & n1 < n & n2 < n by A3, A1;

          hence t in x2 by A2;

        end;

        let t be object;

        assume

         A4: t in x2;

        then

        reconsider u = t as Element of [: NAT , NAT :];

        ex n1,n2 be Nat st n1 = (u `1 ) & n2 = (u `2 ) & n1 < n & n2 < n by A4, A2;

        hence t in x1 by A1;

      end;

    end

    theorem :: CARDFIL4:35

    

     Th30: ( square-downarrow n) = [:( Segm n), ( Segm n):]

    proof

      thus ( square-downarrow n) c= [:( Segm n), ( Segm n):]

      proof

        let x be object;

        assume

         A2: x in ( square-downarrow n);

        then

        consider n1,n2 be Nat such that

         A3: n1 = (x `1 ) and

         A4: n2 = (x `2 ) and

         A5: n1 < n and

         A6: n2 < n by Def4;

        

         A7: n1 in ( Segm n) by A5, NAT_1: 44;

        

         A8: n2 in ( Segm n) by A6, NAT_1: 44;

        ex x1,x2 be object st x1 in NAT & x2 in NAT & x = [x1, x2] by A2, ZFMISC_1:def 2;

        then

        reconsider x as pair object;

        x = [n1, n2] by A3, A4;

        hence thesis by A7, A8, ZFMISC_1:def 2;

      end;

      let x be object;

      assume x in [:( Segm n), ( Segm n):];

      then

      consider y1,y2 be object such that

       A9: y1 in ( Segm n) and

       A10: y2 in ( Segm n) and

       A11: x = [y1, y2] by ZFMISC_1:def 2;

      reconsider y1, y2 as Nat by A9, A10;

      

       A12: y1 = (x `1 ) & y2 = (x `2 ) & y1 < n & y2 < n by A11, A9, A10, NAT_1: 44;

      x is Element of [: NAT , NAT :] by A9, A10, A11, ZFMISC_1:def 2;

      hence thesis by A12, Def4;

    end;

    theorem :: CARDFIL4:36

    for A be finite Subset of [: NAT , NAT :] holds ex n st A c= ( square-downarrow n)

    proof

      let A be finite Subset of [: NAT , NAT :];

      consider m, n such that

       A1: A c= [:( Segm m), ( Segm n):] by Th16;

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

      reconsider mn = ( max (m,n)) as Nat;

      A c= ( square-downarrow mn)

      proof

        ( Segm m) c= ( Segm mn) & ( Segm n) c= ( Segm mn) by XXREAL_0: 25, NAT_1: 39;

        then [:( Segm m), ( Segm n):] c= [:( Segm mn), ( Segm mn):] by ZFMISC_1: 96;

        then [:( Segm m), ( Segm n):] c= ( square-downarrow mn) by Th30;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL4:37

    ( square-downarrow n) is finite Subset of [: NAT , NAT :]

    proof

       [:( Segm n), ( Segm n):] is finite;

      hence thesis by Th30;

    end;

    begin

    theorem :: CARDFIL4:38

    

     Th31: for x be Element of [: base_of_frechet_filter , base_of_frechet_filter :] holds ex i, j st x = [:( NAT \ ( Segm i)), ( NAT \ ( Segm j)):]

    proof

      let x be Element of [: base_of_frechet_filter , base_of_frechet_filter :];

      x in the set of all [:B1, B2:] where B1 be Element of base_of_frechet_filter , B2 be Element of base_of_frechet_filter ;

      then

      consider B1 be Element of base_of_frechet_filter , B2 be Element of base_of_frechet_filter such that

       A1: x = [:B1, B2:];

      consider i such that

       A2: B1 = ( NAT \ ( Segm i)) by Th20;

      consider j such that

       A3: B2 = ( NAT \ ( Segm j)) by Th20;

      take i, j;

      thus thesis by A1, A2, A3;

    end;

    theorem :: CARDFIL4:39

    

     Th32: for x be Element of [: base_of_frechet_filter , base_of_frechet_filter :] holds ex n st ( square-uparrow n) c= x

    proof

      let x be Element of [: base_of_frechet_filter , base_of_frechet_filter :];

      ex i, j st x = [:( NAT \ ( Segm i)), ( NAT \ ( Segm j)):] by Th31;

      hence thesis by Th28;

    end;

    theorem :: CARDFIL4:40

     [: base_of_frechet_filter , base_of_frechet_filter :] is filter_base of [: NAT , NAT :];

    theorem :: CARDFIL4:41

    

     Th33: ex cB be basis of ( Frechet_Filter NAT ) st cB = base_of_frechet_filter & [:cB, cB:] is basis of <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).)

    proof

      reconsider bff = base_of_frechet_filter as basis of ( Frechet_Filter NAT ) by CARDFIL2: 56;

       [:bff, bff:] is basis of <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).);

      hence thesis;

    end;

    definition

      :: CARDFIL4:def6

      func all-square-uparrow -> filter_base of [: NAT , NAT :] equals the set of all ( square-uparrow n) where n be Nat;

      coherence

      proof

        set S = the set of all ( square-uparrow n) where n be Nat;

        S c= ( bool [: NAT , NAT :])

        proof

          let x be object;

          assume x in S;

          then ex n be Nat st x = ( square-uparrow n);

          hence thesis;

        end;

        then

        reconsider S as Subset-Family of [: NAT , NAT :];

        now

          thus S is with_non-empty_elements

          proof

            assume not S is with_non-empty_elements;

            then {} in S by SETFAM_1:def 8;

            then ex n be Nat st {} = ( square-uparrow n);

            hence thesis;

          end;

          

           A1: ( square-uparrow 1) in S;

          hence S is non empty;

          thus S is quasi_basis

          proof

            let b1,b2 be Element of S;

            b1 in S by A1;

            then

            consider i such that

             A2: b1 = ( square-uparrow i);

            b2 in S by A1;

            then

            consider j such that

             A3: b2 = ( square-uparrow j);

            reconsider i, j as Element of NAT by ORDINAL1:def 12;

            reconsider n = ( max (i,j)) as Element of NAT ;

            ( square-uparrow n) in S;

            hence thesis by A2, A3, Th29;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: CARDFIL4:42

    

     Th34: ( all-square-uparrow , [: base_of_frechet_filter , base_of_frechet_filter :]) are_equivalent_generators

    proof

      set cB1 = all-square-uparrow , cB2 = [: base_of_frechet_filter , base_of_frechet_filter :];

       A1:

      now

        let b1 be Element of cB1;

        b1 in cB1;

        then

        consider n such that

         A2: b1 = ( square-uparrow n);

        ( NAT \ ( Segm n)) is Element of base_of_frechet_filter by Th21;

        then [:( NAT \ ( Segm n)), ( NAT \ ( Segm n)):] in [: base_of_frechet_filter , base_of_frechet_filter :];

        then

        reconsider b2 = [:( NAT \ ( Segm n)), ( NAT \ ( Segm n)):] as Element of cB2;

        b2 c= b1 by A2, Th27;

        hence ex b2 be Element of cB2 st b2 c= b1;

      end;

      now

        let b2 be Element of cB2;

        consider n such that

         A1: ( square-uparrow n) c= b2 by Th32;

        ( square-uparrow n) in all-square-uparrow ;

        hence ex b1 be Element of cB1 st b1 c= b2 by A1;

      end;

      hence thesis by A1;

    end;

    theorem :: CARDFIL4:43

    

     Th35: <. [: base_of_frechet_filter , base_of_frechet_filter :].) = <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).)

    proof

      consider cB be basis of ( Frechet_Filter NAT ) such that

       A1: cB = base_of_frechet_filter and [:cB, cB:] is basis of <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).) by Th33;

       <.( # [:cB, cB:]).] = <. [: base_of_frechet_filter , base_of_frechet_filter :].)

      proof

        set cF1 = <.( # [:cB, cB:]).], cF2 = <. [: base_of_frechet_filter , base_of_frechet_filter :].);

        now

          let x be object;

          assume

           A2: x in cF1;

          then

          reconsider y = x as Subset of [: NAT , NAT :];

          consider b be Element of ( # [:cB, cB:]) such that

           A3: b c= y by A2, CARDFIL2:def 8;

          consider cB3 be filter_base of NAT , cB4 be filter_base of NAT such that

           A4: cB = cB3 and

           A5: cB = cB4 and

           A6: [:cB, cB:] = [:cB3, cB4:] by Def2;

          b in the set of all [:B1, B2:] where B1 be Element of cB3, B2 be Element of cB4 by A6;

          then

          consider B1 be Element of cB3, B2 be Element of cB4 such that

           A7: b = [:B1, B2:];

          b in [: base_of_frechet_filter , base_of_frechet_filter :] by A1, A4, A5, A7;

          hence x in cF2 by A3, CARDFIL2:def 8;

        end;

        then

         A8: cF1 c= cF2;

        now

          let x be object;

          assume

           A9: x in cF2;

          then

          reconsider y = x as Subset of [: NAT , NAT :];

          consider b be Element of [: base_of_frechet_filter , base_of_frechet_filter :] such that

           A10: b c= y by A9, CARDFIL2:def 8;

          ex cB3 be filter_base of NAT , cB4 be filter_base of NAT st cB = cB3 & cB = cB4 & [:cB, cB:] = [:cB3, cB4:] by Def2;

          hence x in cF1 by A1, A10, CARDFIL2:def 8;

        end;

        then cF2 c= cF1;

        hence thesis by A8;

      end;

      hence thesis by CARDFIL2: 21;

    end;

    theorem :: CARDFIL4:44

    

     Th36: <. all-square-uparrow .) = <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).) by Th34, CARDFIL2: 19, Th35;

    theorem :: CARDFIL4:45

    

     Th37: <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).) is_filter-finer_than ( Frechet_Filter [: NAT , NAT :])

    proof

      now

        let x be object;

        assume

         A1: x in ( Frechet_Filter [: NAT , NAT :]);

        x in the set of all ( [: NAT , NAT :] \ A) where A be finite Subset of [: NAT , NAT :] by A1, CARDFIL2: 51;

        then

        consider A be finite Subset of [: NAT , NAT :] such that

         A2: x = ( [: NAT , NAT :] \ A);

        reconsider y = x as Subset of [: NAT , NAT :] by A2;

        consider m, n such that

         A3: A c= [:( Segm m), ( Segm n):] by Th16;

        

         A4: ( [: NAT , NAT :] \ [:( Segm m), ( Segm n):]) c= y by A2, A3, XBOOLE_1: 34;

         [:( NAT \ ( Segm m)), ( NAT \ ( Segm n)):] c= ( [: NAT , NAT :] \ [:( Segm m), ( Segm n):]) by Th10;

        then

         A5: [:( NAT \ ( Segm m)), ( NAT \ ( Segm n)):] c= y by A4;

        ( NAT \ ( Segm m)) is Element of base_of_frechet_filter & ( NAT \ ( Segm n)) is Element of base_of_frechet_filter by Th21;

        then [:( NAT \ ( Segm m)), ( NAT \ ( Segm n)):] in [: base_of_frechet_filter , base_of_frechet_filter :];

        hence x in <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).) by Th35, A5, CARDFIL2:def 8;

      end;

      then ( Frechet_Filter [: NAT , NAT :]) c= <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).);

      hence thesis;

    end;

    theorem :: CARDFIL4:46

    

     Th38: ( [: NAT , NAT :] \ the set of all [ 0 , n] where n be Nat) in <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).) & not ( [: NAT , NAT :] \ the set of all [ 0 , n] where n be Nat) in ( Frechet_Filter [: NAT , NAT :])

    proof

      set X = ( [: NAT , NAT :] \ the set of all [ 0 , n] where n be Nat);

      

       A1: ( square-uparrow 1) c= X

      proof

        let x be object;

        assume x in ( square-uparrow 1);

        then x in [:( NAT \ ( Segm 1)), ( NAT \ ( Segm 1)):] by Th27;

        then

        consider n,m be object such that

         A2: n in ( NAT \ ( Segm 1)) and

         A3: m in ( NAT \ ( Segm 1)) and

         A4: x = [n, m] by ZFMISC_1:def 2;

        reconsider n, m as Nat by A2, A3;

        

         A5: x in [: NAT , NAT :] by A4, A2, A3, ZFMISC_1:def 2;

         not n in ( Segm 1) by A2, XBOOLE_0:def 5;

        then

         A6: not n = 0 by NAT_1: 44;

         not x in the set of all [ 0 , n] where n be Nat

        proof

          assume not thesis;

          then ex k be Nat st x = [ 0 , k];

          hence thesis by A6, A4, XTUPLE_0: 1;

        end;

        hence thesis by A5, XBOOLE_0:def 5;

      end;

      ( square-uparrow 1) in the set of all ( square-uparrow n) where n be Nat;

      hence X in <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).) by A1, CARDFIL2:def 8, Th36;

      thus not X in ( Frechet_Filter [: NAT , NAT :])

      proof

        assume not thesis;

        then X in the set of all ( [: NAT , NAT :] \ A) where A be finite Subset of [: NAT , NAT :] by CARDFIL2: 51;

        then

        consider A be finite Subset of [: NAT , NAT :] such that

         A7: X = ( [: NAT , NAT :] \ A);

         the set of all [ 0 , n] where n be Nat c= [: NAT , NAT :]

        proof

          let x be object;

          assume x in the set of all [ 0 , n] where n be Nat;

          then

          consider n be Nat such that

           A8: x = [ 0 , n];

          n in NAT & 0 in NAT by ORDINAL1:def 12;

          hence thesis by A8, ZFMISC_1:def 2;

        end;

        hence contradiction by A7, COMBGRAS: 5, Th9;

      end;

    end;

    theorem :: CARDFIL4:47

    ( Frechet_Filter [: NAT , NAT :]) <> <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).) by Th38;

    begin

    reserve T for non empty TopSpace,

s for Function of [: NAT , NAT :], the carrier of T,

M for Subset of the carrier of T;

    reserve cF3,cF4 for Filter of the carrier of T;

    theorem :: CARDFIL4:48

    

     Th39: cF4 is_filter-finer_than cF3 implies ( lim_filter cF3) c= ( lim_filter cF4)

    proof

      assume

       A1: cF4 is_filter-finer_than cF3;

      let x be object;

      assume x in ( lim_filter cF3);

      then

      consider y be Point of T such that

       A2: x = y and

       A3: cF3 is_filter-finer_than ( NeighborhoodSystem y);

      ( NeighborhoodSystem y) c= cF3 & cF3 c= cF4 by A1, A3;

      then ( NeighborhoodSystem y) c= cF4;

      then cF4 is_filter-finer_than ( NeighborhoodSystem y);

      hence thesis by A2;

    end;

    theorem :: CARDFIL4:49

    

     Th40: for f be Function of X, Y, cFXa,cFXb be Filter of X st cFXb is_filter-finer_than cFXa holds ( filter_image (f,cFXb)) is_filter-finer_than ( filter_image (f,cFXa))

    proof

      let f be Function of X, Y, cFXa,cFXb be Filter of X;

      assume

       A1: cFXb is_filter-finer_than cFXa;

      ( filter_image (f,cFXa)) c= ( filter_image (f,cFXb))

      proof

        let x be object;

        assume x in ( filter_image (f,cFXa));

        then ex M be Subset of Y st x = M & (f " M) in cFXa;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL4:50

    

     Th41: (s " M) in ( Frechet_Filter [: NAT , NAT :]) iff ex A be finite Subset of [: NAT , NAT :] st (s " M) = ( [: NAT , NAT :] \ A)

    proof

      hereby

        assume (s " M) in ( Frechet_Filter [: NAT , NAT :]);

        then (s " M) in the set of all ( [: NAT , NAT :] \ A) where A be finite Subset of [: NAT , NAT :] by CARDFIL2: 51;

        hence ex A be finite Subset of [: NAT , NAT :] st (s " M) = ( [: NAT , NAT :] \ A);

      end;

      assume ex A be finite Subset of [: NAT , NAT :] st (s " M) = ( [: NAT , NAT :] \ A);

      then (s " M) in the set of all ( [: NAT , NAT :] \ A) where A be finite Subset of [: NAT , NAT :];

      hence (s " M) in ( Frechet_Filter [: NAT , NAT :]) by CARDFIL2: 51;

    end;

    theorem :: CARDFIL4:51

    

     Th42: (s " M) in <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).) iff ex n st ( square-uparrow n) c= (s " M)

    proof

      hereby

        assume (s " M) in <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).);

        then

        consider b be Element of [: base_of_frechet_filter , base_of_frechet_filter :] such that

         A1: b c= (s " M) by Th35, CARDFIL2:def 8;

        ex n st ( square-uparrow n) c= b by Th32;

        hence ex n st ( square-uparrow n) c= (s " M) by A1, XBOOLE_1: 1;

      end;

      given n such that

       A2: ( square-uparrow n) c= (s " M);

      ( square-uparrow n) in the set of all ( square-uparrow n) where n be Nat;

      then ex b2 be Element of [: base_of_frechet_filter , base_of_frechet_filter :] st b2 c= ( square-uparrow n) by Th34;

      then

       A3: ex b2 be Element of [: base_of_frechet_filter , base_of_frechet_filter :] st b2 c= (s " M) by A2, XBOOLE_1: 1;

      ( dom s) = [: NAT , NAT :] by FUNCT_2:def 1;

      then (s " M) is Subset of [: NAT , NAT :] by RELAT_1: 132;

      hence (s " M) in <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).) by A3, Th35, CARDFIL2:def 8;

    end;

    theorem :: CARDFIL4:52

    

     Th43: ( filter_image (s,( Frechet_Filter [: NAT , NAT :]))) = { M where M be Subset of the carrier of T : ex A be finite Subset of [: NAT , NAT :] st (s " M) = ( [: NAT , NAT :] \ A) }

    proof

      set X = { M where M be Subset of the carrier of T : (s " M) in ( Frechet_Filter [: NAT , NAT :]) }, Y = { M where M be Subset of the carrier of T : ex A be finite Subset of [: NAT , NAT :] st (s " M) = ( [: NAT , NAT :] \ A) };

      X = Y

      proof

        now

          let x be object;

          assume x in X;

          then

          consider M be Subset of the carrier of T such that

           A1: x = M and

           A2: (s " M) in ( Frechet_Filter [: NAT , NAT :]);

          ex A be finite Subset of [: NAT , NAT :] st (s " M) = ( [: NAT , NAT :] \ A) by Th41, A2;

          hence x in Y by A1;

        end;

        then

         A3: X c= Y;

        now

          let x be object;

          assume x in Y;

          then

          consider M be Subset of the carrier of T such that

           A4: x = M and

           A5: ex A be finite Subset of [: NAT , NAT :] st (s " M) = ( [: NAT , NAT :] \ A);

          (s " M) in ( Frechet_Filter [: NAT , NAT :]) by A5, Th41;

          hence x in X by A4;

        end;

        then Y c= X;

        hence thesis by A3;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL4:53

    

     Th44: ( filter_image (s, <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) = { M where M be Subset of the carrier of T : ex n be Nat st ( square-uparrow n) c= (s " M) }

    proof

      set X = { M where M be Subset of the carrier of T : (s " M) in <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).) }, Y = { M where M be Subset of the carrier of T : ex n be Nat st ( square-uparrow n) c= (s " M) };

      X = Y

      proof

        now

          let x be object;

          assume x in X;

          then

          consider M be Subset of the carrier of T such that

           A1: x = M and

           A2: (s " M) in <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).);

          ex n st ( square-uparrow n) c= (s " M) by Th42, A2;

          hence x in Y by A1;

        end;

        then

         A3: X c= Y;

        now

          let x be object;

          assume x in Y;

          then

          consider M be Subset of the carrier of T such that

           A4: x = M and

           A5: ex n st ( square-uparrow n) c= (s " M);

          (s " M) in <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).) by A5, Th42;

          hence x in X by A4;

        end;

        then Y c= X;

        hence thesis by A3;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL4:54

    

     Th45: for x be Point of T holds x in ( lim_filter (s,( Frechet_Filter [: NAT , NAT :]))) iff for A be a_neighborhood of x holds ex B be finite Subset of [: NAT , NAT :] st (s " A) = ( [: NAT , NAT :] \ B)

    proof

      let x be Point of T;

      set F = ( filter_image (s,( Frechet_Filter [: NAT , NAT :])));

      

       A1: F is_filter-finer_than ( NeighborhoodSystem x) iff for A be a_neighborhood of x holds ex B be finite Subset of [: NAT , NAT :] st (s " A) = ( [: NAT , NAT :] \ B)

      proof

        hereby

          assume F is_filter-finer_than ( NeighborhoodSystem x);

          then ( NeighborhoodSystem x) c= { M where M be Subset of the carrier of T : ex A be finite Subset of [: NAT , NAT :] st (s " M) = ( [: NAT , NAT :] \ A) } by Th43;

          then

           A2: the set of all A where A be a_neighborhood of x c= { M where M be Subset of the carrier of T : ex A be finite Subset of [: NAT , NAT :] st (s " M) = ( [: NAT , NAT :] \ A) } by YELLOW19:def 1;

          thus for A be a_neighborhood of x holds ex B be finite Subset of [: NAT , NAT :] st (s " A) = ( [: NAT , NAT :] \ B)

          proof

            let A be a_neighborhood of x;

            A in the set of all A where A be a_neighborhood of x;

            then A in { M where M be Subset of the carrier of T : ex A be finite Subset of [: NAT , NAT :] st (s " M) = ( [: NAT , NAT :] \ A) } by A2;

            then ex M be Subset of the carrier of T st A = M & ex B be finite Subset of [: NAT , NAT :] st (s " M) = ( [: NAT , NAT :] \ B);

            hence thesis;

          end;

        end;

        assume

         A3: for A be a_neighborhood of x holds ex B be finite Subset of [: NAT , NAT :] st (s " A) = ( [: NAT , NAT :] \ B);

        ( NeighborhoodSystem x) c= F

        proof

          let y be object;

          assume y in ( NeighborhoodSystem x);

          then y in the set of all A where A be a_neighborhood of x by YELLOW19:def 1;

          then

          consider A be a_neighborhood of x such that

           A4: y = A;

          ex B be finite Subset of [: NAT , NAT :] st (s " A) = ( [: NAT , NAT :] \ B) by A3;

          then A in { M where M be Subset of the carrier of T : ex A be finite Subset of [: NAT , NAT :] st (s " M) = ( [: NAT , NAT :] \ A) };

          hence thesis by A4, Th43;

        end;

        hence F is_filter-finer_than ( NeighborhoodSystem x);

      end;

      F is_filter-finer_than ( NeighborhoodSystem x) iff x in ( lim_filter F)

      proof

        thus F is_filter-finer_than ( NeighborhoodSystem x) implies x in ( lim_filter F);

        assume x in ( lim_filter F);

        then ex y be Point of T st x = y & F is_filter-finer_than ( NeighborhoodSystem y);

        hence F is_filter-finer_than ( NeighborhoodSystem x);

      end;

      hence thesis by A1;

    end;

    theorem :: CARDFIL4:55

    

     Th46: for x be Point of T holds x in ( lim_filter (s,( Frechet_Filter [: NAT , NAT :]))) iff for A be a_neighborhood of x holds ( [: NAT , NAT :] \ (s " A)) is finite

    proof

      let x be Point of T;

      hereby

        assume

         A1: x in ( lim_filter (s,( Frechet_Filter [: NAT , NAT :])));

        now

          let A be a_neighborhood of x;

          ex B be finite Subset of [: NAT , NAT :] st (s " A) = ( [: NAT , NAT :] \ B) by A1, Th45;

          hence ( [: NAT , NAT :] \ (s " A)) is finite by Th1;

        end;

        hence for A be a_neighborhood of x holds ( [: NAT , NAT :] \ (s " A)) is finite;

      end;

      assume

       A2: for A be a_neighborhood of x holds ( [: NAT , NAT :] \ (s " A)) is finite;

      now

        let A be a_neighborhood of x;

        

         A3: ( dom s) = [: NAT , NAT :] by FUNCT_2:def 1;

        ( [: NAT , NAT :] \ (s " A)) is finite by A2;

        hence ex B be finite Subset of [: NAT , NAT :] st (s " A) = ( [: NAT , NAT :] \ B) by A3, RELAT_1: 132, Th2;

      end;

      hence x in ( lim_filter (s,( Frechet_Filter [: NAT , NAT :]))) by Th45;

    end;

    theorem :: CARDFIL4:56

    

     Th47: for x be Point of T holds x in ( lim_filter (s, <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) iff for A be a_neighborhood of x holds ex n be Nat st ( square-uparrow n) c= (s " A)

    proof

      let x be Point of T;

      set F = ( filter_image (s, <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).)));

      

       A1: F is_filter-finer_than ( NeighborhoodSystem x) iff for A be a_neighborhood of x holds ex n be Nat st ( square-uparrow n) c= (s " A)

      proof

        hereby

          assume F is_filter-finer_than ( NeighborhoodSystem x);

          then ( NeighborhoodSystem x) c= { M where M be Subset of the carrier of T : ex n be Nat st ( square-uparrow n) c= (s " M) } by Th44;

          then

           A2: the set of all A where A be a_neighborhood of x c= { M where M be Subset of the carrier of T : ex n be Nat st ( square-uparrow n) c= (s " M) } by YELLOW19:def 1;

          thus for A be a_neighborhood of x holds ex n be Nat st ( square-uparrow n) c= (s " A)

          proof

            let A be a_neighborhood of x;

            A in the set of all A where A be a_neighborhood of x;

            then A in { M where M be Subset of the carrier of T : ex n be Nat st ( square-uparrow n) c= (s " M) } by A2;

            then ex M be Subset of the carrier of T st A = M & ex n be Nat st ( square-uparrow n) c= (s " M);

            hence thesis;

          end;

        end;

        assume

         A3: for A be a_neighborhood of x holds ex n be Nat st ( square-uparrow n) c= (s " A);

        ( NeighborhoodSystem x) c= F

        proof

          let y be object;

          assume y in ( NeighborhoodSystem x);

          then y in the set of all A where A be a_neighborhood of x by YELLOW19:def 1;

          then

          consider A be a_neighborhood of x such that

           A4: y = A;

          ex n be Nat st ( square-uparrow n) c= (s " A) by A3;

          then A in { M where M be Subset of the carrier of T : ex n be Nat st ( square-uparrow n) c= (s " M) };

          hence thesis by A4, Th44;

        end;

        hence F is_filter-finer_than ( NeighborhoodSystem x);

      end;

      F is_filter-finer_than ( NeighborhoodSystem x) iff x in ( lim_filter F)

      proof

        thus F is_filter-finer_than ( NeighborhoodSystem x) implies x in ( lim_filter F);

        assume x in ( lim_filter F);

        then ex y be Point of T st x = y & F is_filter-finer_than ( NeighborhoodSystem y);

        hence F is_filter-finer_than ( NeighborhoodSystem x);

      end;

      hence thesis by A1;

    end;

    theorem :: CARDFIL4:57

    

     Th48: for x be Point of T, cB be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_filter (s, <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) iff for B be Element of cB holds ex n be Nat st ( square-uparrow n) c= (s " B)

    proof

      let x be Point of T, cB be basis of ( BOOL2F ( NeighborhoodSystem x));

      hereby

        assume

         A1: x in ( lim_filter (s, <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).)));

        hereby

          let B be Element of cB;

          B is a_neighborhood of x by YELLOW19: 2;

          hence ex n be Nat st ( square-uparrow n) c= (s " B) by A1, Th47;

        end;

      end;

      assume

       A2: for B be Element of cB holds ex n be Nat st ( square-uparrow n) c= (s " B);

      now

        let A be a_neighborhood of x;

        

         A3: A is Element of ( BOOL2F ( NeighborhoodSystem x)) by YELLOW19: 2;

        cB is filter_basis;

        then

        consider B be Element of cB such that

         A4: B c= A by A3;

        

         A5: ex n be Nat st ( square-uparrow n) c= (s " B) by A2;

        (s " B) c= (s " A) by A4, RELAT_1: 145;

        hence ex n be Nat st ( square-uparrow n) c= (s " A) by A5, XBOOLE_1: 1;

      end;

      hence x in ( lim_filter (s, <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) by Th47;

    end;

    theorem :: CARDFIL4:58

    

     Th49: for x be Point of T, cB be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_filter (s,( Frechet_Filter [: NAT , NAT :]))) iff for B be Element of cB holds ex A be finite Subset of [: NAT , NAT :] st (s " B) = ( [: NAT , NAT :] \ A)

    proof

      let x be Point of T, cB be basis of ( BOOL2F ( NeighborhoodSystem x));

      hereby

        assume

         A1: x in ( lim_filter (s,( Frechet_Filter [: NAT , NAT :])));

        hereby

          let B be Element of cB;

          B is a_neighborhood of x by YELLOW19: 2;

          hence ex A be finite Subset of [: NAT , NAT :] st (s " B) = ( [: NAT , NAT :] \ A) by A1, Th45;

        end;

      end;

      assume

       A2: for B be Element of cB holds ex A be finite Subset of [: NAT , NAT :] st (s " B) = ( [: NAT , NAT :] \ A);

      now

        let A be a_neighborhood of x;

        

         A3: A is Element of ( BOOL2F ( NeighborhoodSystem x)) by YELLOW19: 2;

        cB is filter_basis;

        then

        consider B be Element of cB such that

         A4: B c= A by A3;

        ex C be finite Subset of [: NAT , NAT :] st (s " B) = ( [: NAT , NAT :] \ C) by A2;

        hence ( [: NAT , NAT :] \ (s " A)) is finite by A4, RELAT_1: 145, Th1;

      end;

      hence x in ( lim_filter (s,( Frechet_Filter [: NAT , NAT :]))) by Th46;

    end;

    theorem :: CARDFIL4:59

    

     Th50: for x be Point of T, cB be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_filter (s, <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) iff for B be Element of cB holds ex n be Nat st (s .: ( square-uparrow n)) c= B

    proof

      let x be Point of T, cB be basis of ( BOOL2F ( NeighborhoodSystem x));

      hereby

        assume

         A1: x in ( lim_filter (s, <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).)));

        hereby

          let B be Element of cB;

          consider n be Nat such that

           A2: ( square-uparrow n) c= (s " B) by A1, Th48;

          take n;

          

           A3: (s .: ( square-uparrow n)) c= (s .: (s " B)) by A2, RELAT_1: 123;

          (s .: (s " B)) c= B by FUNCT_1: 75;

          hence (s .: ( square-uparrow n)) c= B by A3;

        end;

      end;

      assume

       A4: for B be Element of cB holds ex n be Nat st (s .: ( square-uparrow n)) c= B;

      now

        let B be Element of cB;

        consider n be Nat such that

         A5: (s .: ( square-uparrow n)) c= B by A4;

        

         A6: (s " (s .: ( square-uparrow n))) c= (s " B) by A5, RELAT_1: 143;

        ( dom s) = [: NAT , NAT :] by FUNCT_2:def 1;

        then ( square-uparrow n) c= (s " (s .: ( square-uparrow n))) by FUNCT_1: 76;

        then ( square-uparrow n) c= (s " B) by A6;

        hence ex n be Nat st ( square-uparrow n) c= (s " B);

      end;

      hence x in ( lim_filter (s, <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) by Th48;

    end;

    theorem :: CARDFIL4:60

    

     Th51: for x be Point of T, cB be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_filter (s,( Frechet_Filter [: NAT , NAT :]))) iff for B be Element of cB holds ex A be finite Subset of [: NAT , NAT :] st (s .: ( [: NAT , NAT :] \ A)) c= B

    proof

      let x be Point of T, cB be basis of ( BOOL2F ( NeighborhoodSystem x));

      hereby

        assume

         A1: x in ( lim_filter (s,( Frechet_Filter [: NAT , NAT :])));

        hereby

          let B be Element of cB;

          consider A be finite Subset of [: NAT , NAT :] such that

           A2: (s " B) = ( [: NAT , NAT :] \ A) by A1, Th49;

          take A;

          thus (s .: ( [: NAT , NAT :] \ A)) c= B by A2, FUNCT_1: 75;

        end;

      end;

      assume

       A3: for B be Element of cB holds ex A be finite Subset of [: NAT , NAT :] st (s .: ( [: NAT , NAT :] \ A)) c= B;

      for A be a_neighborhood of x holds ( [: NAT , NAT :] \ (s " A)) is finite

      proof

        let A be a_neighborhood of x;

        

         A4: A is Element of ( BOOL2F ( NeighborhoodSystem x)) by YELLOW19: 2;

        cB is filter_basis;

        then

        consider B be Element of cB such that

         A5: B c= A by A4;

        consider C be finite Subset of [: NAT , NAT :] such that

         A6: (s .: ( [: NAT , NAT :] \ C)) c= B by A3;

        (s .: ( [: NAT , NAT :] \ C)) c= A by A6, A5;

        then

         A7: (s " (s .: ( [: NAT , NAT :] \ C))) c= (s " A) by RELAT_1: 143;

        ( dom s) = [: NAT , NAT :] by FUNCT_2:def 1;

        then ( [: NAT , NAT :] \ C) c= (s " (s .: ( [: NAT , NAT :] \ C))) by FUNCT_1: 76;

        then ( [: NAT , NAT :] \ C) c= (s " A) by A7;

        then ( [: NAT , NAT :] \ (s " A)) c= ( [: NAT , NAT :] \ ( [: NAT , NAT :] \ C)) by XBOOLE_1: 34;

        then ( [: NAT , NAT :] \ (s " A)) c= ( [: NAT , NAT :] /\ C) by XBOOLE_1: 48;

        hence thesis;

      end;

      hence x in ( lim_filter (s,( Frechet_Filter [: NAT , NAT :]))) by Th46;

    end;

    theorem :: CARDFIL4:61

    

     Th52: for x be Point of T, cB be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_filter (s,( Frechet_Filter [: NAT , NAT :]))) iff for B be Element of cB holds ex n, m st (s .: ( [: NAT , NAT :] \ [:( Segm n), ( Segm m):])) c= B

    proof

      let x be Point of T, cB be basis of ( BOOL2F ( NeighborhoodSystem x));

      hereby

        assume

         A1: x in ( lim_filter (s,( Frechet_Filter [: NAT , NAT :])));

        now

          let B be Element of cB;

          consider A be finite Subset of [: NAT , NAT :] such that

           A2: (s .: ( [: NAT , NAT :] \ A)) c= B by A1, Th51;

          consider n, m such that

           A3: A c= [:( Segm n), ( Segm m):] by Th16;

          ( [: NAT , NAT :] \ [:( Segm n), ( Segm m):]) c= ( [: NAT , NAT :] \ A) by A3, XBOOLE_1: 34;

          then (s .: ( [: NAT , NAT :] \ [:( Segm n), ( Segm m):])) c= (s .: ( [: NAT , NAT :] \ A)) by RELAT_1: 123;

          then (s .: ( [: NAT , NAT :] \ [:( Segm n), ( Segm m):])) c= B by A2;

          hence ex n, m st (s .: ( [: NAT , NAT :] \ [:( Segm n), ( Segm m):])) c= B;

        end;

        hence for B be Element of cB holds ex n, m st (s .: ( [: NAT , NAT :] \ [:( Segm n), ( Segm m):])) c= B;

      end;

      assume

       A4: for B be Element of cB holds ex n, m st (s .: ( [: NAT , NAT :] \ [:( Segm n), ( Segm m):])) c= B;

      now

        let B be Element of cB;

        consider n, m such that

         A5: (s .: ( [: NAT , NAT :] \ [:( Segm n), ( Segm m):])) c= B by A4;

        reconsider A = [:( Segm n), ( Segm m):] as finite Subset of [: NAT , NAT :];

        thus ex A be finite Subset of [: NAT , NAT :] st (s .: ( [: NAT , NAT :] \ A)) c= B by A5;

      end;

      hence x in ( lim_filter (s,( Frechet_Filter [: NAT , NAT :]))) by Th51;

    end;

    theorem :: CARDFIL4:62

    

     Th53: x in (s .: ( square-uparrow n)) iff ex i, j st n <= i & n <= j & x = (s . (i,j))

    proof

      hereby

        assume x in (s .: ( square-uparrow n));

        then

        consider y be object such that

         A1: y in ( dom s) and

         A2: y in ( square-uparrow n) and

         A3: x = (s . y) by FUNCT_1:def 6;

        reconsider z = y as Element of [: NAT , NAT :] by A1;

        consider i, j such that

         A4: (z `1 ) = i and

         A5: (z `2 ) = j and

         A6: n <= i and

         A7: n <= j by A2, Def3;

        consider m1,m2 be object such that m1 in NAT and m2 in NAT and

         A8: z = [m1, m2] by ZFMISC_1:def 2;

        x = (s . (i,j)) by A4, A5, A8, A3, BINOP_1:def 1;

        hence ex i, j st n <= i & n <= j & x = (s . (i,j)) by A6, A7;

      end;

      assume ex i, j st n <= i & n <= j & x = (s . (i,j));

      then

      consider i, j such that

       A9: n <= i and

       A10: n <= j and

       A11: x = (s . (i,j));

      

       A12: ( dom s) = [: NAT , NAT :] by FUNCT_2:def 1;

      

       A13: i in NAT & j in NAT by ORDINAL1:def 12;

      

       A14: x = (s . [i, j]) by A11, BINOP_1:def 1;

      ( [i, j] `1 ) = i & ( [i, j] `2 ) = j & [i, j] in [: NAT , NAT :] by A13, ZFMISC_1:def 2;

      then [i, j] in ( square-uparrow n) by A9, A10, Def3;

      hence x in (s .: ( square-uparrow n)) by A12, A14, FUNCT_1:def 6;

    end;

    theorem :: CARDFIL4:63

    x in (s .: ( [: NAT , NAT :] \ [:( Segm i), ( Segm j):])) iff ex n,m be Nat st (i <= n or j <= m) & x = (s . (n,m))

    proof

      hereby

        assume x in (s .: ( [: NAT , NAT :] \ [:( Segm i), ( Segm j):]));

        then

        consider y be object such that

         A1: y in ( dom s) and

         A2: y in ( [: NAT , NAT :] \ [:( Segm i), ( Segm j):]) and

         A3: x = (s . y) by FUNCT_1:def 6;

        reconsider z = y as Element of [: NAT , NAT :] by A1;

        

         A4: not (z `1 ) in ( Segm i) or not (z `2 ) in ( Segm j)

        proof

          assume not ( not (z `1 ) in ( Segm i) or not (z `2 ) in ( Segm j));

          then

           A5: [(z `1 ), (z `2 )] in [:( Segm i), ( Segm j):] by ZFMISC_1:def 2;

          z is pair by Th4;

          hence thesis by A2, A5, XBOOLE_0:def 5;

        end;

        reconsider n = (z `1 ), m = (z `2 ) as Nat;

        take n, m;

        thus i <= n or j <= m by A4, NAT_1: 44;

        z is pair by Th4;

        hence x = (s . (n,m)) by A3, BINOP_1:def 1;

      end;

      assume ex n,m be Nat st (i <= n or j <= m) & x = (s . (n,m));

      then

      consider n,m be Nat such that

       A6: (i <= n or j <= m) and

       A7: x = (s . (n,m));

      n in NAT & m in NAT by ORDINAL1:def 12;

      then

       A8: [n, m] in [: NAT , NAT :] by ZFMISC_1:def 2;

       not [n, m] in [:( Segm i), ( Segm j):]

      proof

        assume [n, m] in [:( Segm i), ( Segm j):];

        then ex a,b be object st a in ( Segm i) & b in ( Segm j) & [n, m] = [a, b] by ZFMISC_1:def 2;

        then n in ( Segm i) & m in ( Segm j) by XTUPLE_0: 1;

        hence thesis by A6, NAT_1: 44;

      end;

      then

       A9: [n, m] in ( [: NAT , NAT :] \ [:( Segm i), ( Segm j):]) by A8, XBOOLE_0:def 5;

      

       A10: x = (s . [n, m]) by BINOP_1:def 1, A7;

       [n, m] in ( dom s) by A8, FUNCT_2:def 1;

      hence x in (s .: ( [: NAT , NAT :] \ [:( Segm i), ( Segm j):])) by A9, A10, FUNCT_1:def 6;

    end;

    theorem :: CARDFIL4:64

    

     Th54: for x be Point of T, cB be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_filter (s, <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) iff for B be Element of cB holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds (s . (n1,n2)) in B

    proof

      let x be Point of T, cB be basis of ( BOOL2F ( NeighborhoodSystem x));

      (for B be Element of cB holds ex n be Nat st (s .: ( square-uparrow n)) c= B) iff (for B be Element of cB holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds (s . (n1,n2)) in B)

      proof

        hereby

          assume

           A1: for B be Element of cB holds ex n be Nat st (s .: ( square-uparrow n)) c= B;

          hereby

            let B be Element of cB;

            consider n0 be Nat such that

             A2: (s .: ( square-uparrow n0)) c= B by A1;

            take n0;

            thus for n1,n2 be Nat st n0 <= n1 & n0 <= n2 holds (s . (n1,n2)) in B by A2, Th53;

          end;

        end;

        assume

         A3: for B be Element of cB holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds (s . (n1,n2)) in B;

        hereby

          let B be Element of cB;

          consider n0 be Nat such that

           A4: for n1,n2 be Nat st n0 <= n1 & n0 <= n2 holds (s . (n1,n2)) in B by A3;

          thus ex n be Nat st (s .: ( square-uparrow n)) c= B

          proof

            take n0;

            let x be object;

            assume x in (s .: ( square-uparrow n0));

            then ex n1,n2 be Nat st n0 <= n1 & n0 <= n2 & x = (s . (n1,n2)) by Th53;

            hence thesis by A4;

          end;

        end;

      end;

      hence thesis by Th50;

    end;

    theorem :: CARDFIL4:65

    

     Th55: for x be Point of T, cB be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_filter (s,( Frechet_Filter [: NAT , NAT :]))) iff for B be Element of cB holds ex i, j st for m, n st i <= m or j <= n holds (s . (m,n)) in B

    proof

      let x be Point of T, cB be basis of ( BOOL2F ( NeighborhoodSystem x));

      hereby

        assume

         A1: x in ( lim_filter (s,( Frechet_Filter [: NAT , NAT :])));

        hereby

          let B be Element of cB;

          consider i,j be Nat such that

           A2: (s .: ( [: NAT , NAT :] \ [:( Segm i), ( Segm j):])) c= B by A1, Th52;

          take i, j;

          thus for m, n st i <= m or j <= n holds (s . (m,n)) in B

          proof

            let m, n;

            assume

             A3: i <= m or j <= n;

            m in NAT & n in NAT by ORDINAL1:def 12;

            then

             A4: [m, n] in [: NAT , NAT :] by ZFMISC_1:def 2;

            

             A5: not (m in ( Segm i) & n in ( Segm j)) by A3, NAT_1: 44;

             not [m, n] in [:( Segm i), ( Segm j):]

            proof

              assume [m, n] in [:( Segm i), ( Segm j):];

              then ex a,b be object st a in ( Segm i) & b in ( Segm j) & [m, n] = [a, b] by ZFMISC_1:def 2;

              hence thesis by A5, XTUPLE_0: 1;

            end;

            then

             A6: [m, n] in ( [: NAT , NAT :] \ [:( Segm i), ( Segm j):]) by A4, XBOOLE_0:def 5;

             [m, n] in ( dom s) by A4, FUNCT_2:def 1;

            then (s . [m, n]) in (s .: ( [: NAT , NAT :] \ [:( Segm i), ( Segm j):])) by A6, FUNCT_1:def 6;

            then (s . [m, n]) in B by A2;

            hence (s . (m,n)) in B by BINOP_1:def 1;

          end;

        end;

      end;

      assume

       A7: for B be Element of cB holds ex i, j st for m, n st i <= m or j <= n holds (s . (m,n)) in B;

      now

        let B be Element of cB;

        consider i, j such that

         A8: for m, n st i <= m or j <= n holds (s . (m,n)) in B by A7;

        (s .: ( [: NAT , NAT :] \ [:( Segm i), ( Segm j):])) c= B

        proof

          let t be object;

          assume t in (s .: ( [: NAT , NAT :] \ [:( Segm i), ( Segm j):]));

          then

          consider a be object such that

           A9: a in ( dom s) and

           A10: a in ( [: NAT , NAT :] \ [:( Segm i), ( Segm j):]) and

           A11: t = (s . a) by FUNCT_1:def 6;

          reconsider a as Element of [: NAT , NAT :] by A9;

          consider a1,a2 be object such that

           A12: a1 in NAT and

           A13: a2 in NAT and

           A14: a = [a1, a2] by ZFMISC_1:def 2;

          reconsider a1, a2 as Nat by A12, A13;

           not a1 in ( Segm i) or not a2 in ( Segm j)

          proof

            assume not ( not a1 in ( Segm i) or not a2 in ( Segm j));

            then [a1, a2] in [:( Segm i), ( Segm j):] by ZFMISC_1:def 2;

            hence thesis by A14, A10, XBOOLE_0:def 5;

          end;

          then

           A15: i <= a1 or j <= a2 by NAT_1: 44;

          t = (s . (a1,a2)) by A11, A14, BINOP_1:def 1;

          hence t in B by A8, A15;

        end;

        hence ex n1,n2 be Nat st (s .: ( [: NAT , NAT :] \ [:( Segm n1), ( Segm n2):])) c= B;

      end;

      hence x in ( lim_filter (s,( Frechet_Filter [: NAT , NAT :]))) by Th52;

    end;

    theorem :: CARDFIL4:66

    

     Th56: ( lim_filter (s,( Frechet_Filter [: NAT , NAT :]))) c= ( lim_filter (s, <. all-square-uparrow .)))

    proof

       <. all-square-uparrow .) = <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).) by Th34, CARDFIL2: 19, Th35;

      hence thesis by Th37, Th39, Th40;

    end;

    begin

    theorem :: CARDFIL4:67

    

     Th57: for M be non empty MetrSpace, p be Point of M, x be Point of ( TopSpaceMetr M), s be Function of [: NAT , NAT :], ( TopSpaceMetr M) st x = p holds x in ( lim_filter (s, <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) iff for m be non zero Nat holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds (s . (n1,n2)) in { q where q be Point of M : ( dist (p,q)) < (1 / m) }

    proof

      let M be non empty MetrSpace, p be Point of M, x be Point of ( TopSpaceMetr M), s be Function of [: NAT , NAT :], ( TopSpaceMetr M);

      assume

       A1: x = p;

      x in ( lim_filter (s, <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) iff for m be non zero Nat holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds (s . (n1,n2)) in { q where q be Point of M : ( dist (p,q)) < (1 / m) }

      proof

        hereby

          assume

           A2: x in ( lim_filter (s, <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).)));

          hereby

            let m be non zero Nat;

            set B = { q where q be Point of M : ( dist (p,q)) < (1 / m) };

            

             A3: B = ( Ball (p,(1 / m))) by METRIC_1:def 14;

            ex y be Point of M st y = x & ( Balls x) = { ( Ball (y,(1 / m))) where m be Nat : m <> 0 } by FRECHET:def 1;

            then

             A4: B in ( Balls x) by A3, A1;

            ( Balls x) is basis of ( BOOL2F ( NeighborhoodSystem x)) by CARDFIL3: 6;

            hence ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds (s . (n1,n2)) in { q where q be Point of M : ( dist (p,q)) < (1 / m) } by A2, A4, Th54;

          end;

        end;

        assume

         A5: for m be non zero Nat holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds (s . (n1,n2)) in { q where q be Point of M : ( dist (p,q)) < (1 / m) };

        

         A6: ( Balls x) is basis of ( BOOL2F ( NeighborhoodSystem x)) by CARDFIL3: 6;

        for B be Element of ( Balls x) holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds (s . (n1,n2)) in B

        proof

          let B be Element of ( Balls x);

          consider y be Point of M such that

           A7: y = x and

           A8: ( Balls x) = { ( Ball (y,(1 / m))) where m be Nat : m <> 0 } by FRECHET:def 1;

          B in ( Balls x);

          then

          consider m0 be Nat such that

           A9: B = ( Ball (y,(1 / m0))) and

           A10: m0 <> 0 by A8;

          consider n0 be Nat such that

           A11: for n1,n2 be Nat st n0 <= n1 & n0 <= n2 holds (s . (n1,n2)) in { q where q be Point of M : ( dist (p,q)) < (1 / m0) } by A5, A10;

          for n1,n2 be Nat st n0 <= n1 & n0 <= n2 holds (s . (n1,n2)) in B

          proof

            let n1,n2 be Nat;

            assume n0 <= n1 & n0 <= n2;

            then (s . (n1,n2)) in { q where q be Point of M : ( dist (p,q)) < (1 / m0) } by A11;

            hence thesis by A9, A1, A7, METRIC_1:def 14;

          end;

          hence thesis;

        end;

        hence x in ( lim_filter (s, <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) by A6, Th54;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL4:68

    for M be non empty MetrSpace, p be Point of M, x be Point of ( TopSpaceMetr M), s be Function of [: NAT , NAT :], ( TopSpaceMetr M), s2 be Function of [: NAT , NAT :], M st x = p & s = s2 holds x in ( lim_filter (s, <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) iff for m be non zero Nat holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds (s2 . (n1,n2)) in { q where q be Point of M : ( dist (p,q)) < (1 / m) } by Th57;

    begin

    reserve Rseq for Function of [: NAT , NAT :], REAL ;

    theorem :: CARDFIL4:69

    for x be Point of ( TopSpaceMetr ( Euclid 1)), y be Point of ( Euclid 1), cB be basis of ( BOOL2F ( NeighborhoodSystem x)), b be Element of cB st x = y & cB = ( Balls x) holds ex n be Nat st b = { q where q be Element of ( Euclid 1) : ( dist (y,q)) < (1 / n) }

    proof

      let x be Point of ( TopSpaceMetr ( Euclid 1)), y be Point of ( Euclid 1), cB be basis of ( BOOL2F ( NeighborhoodSystem x)), b be Element of cB;

      assume that

       A1: x = y and

       A2: cB = ( Balls x);

      consider z be Point of ( Euclid 1) such that

       A3: x = z and

       A4: ( Balls x) = { ( Ball (z,(1 / n))) where n be Nat : n <> 0 } by FRECHET:def 1;

      b in { ( Ball (z,(1 / n))) where n be Nat : n <> 0 } by A2, A4;

      then

      consider n be Nat such that

       A5: b = ( Ball (z,(1 / n))) and n <> 0 ;

      ( Ball (y,(1 / n))) = { q where q be Element of ( Euclid 1) : ( dist (y,q)) < (1 / n) } by METRIC_1:def 14;

      hence thesis by A5, A1, A3;

    end;

    definition

      let s be Function of [: NAT , NAT :], REAL ;

      :: CARDFIL4:def7

      func # s -> Function of [: NAT , NAT :], R^1 equals s;

      coherence ;

    end

    theorem :: CARDFIL4:70

    for s be Function of [: NAT , NAT :], ( TopSpaceMetr ( Euclid 1)), y be Point of ( Euclid 1) holds ((s .: ( square-uparrow n)) c= { q where q be Element of ( Euclid 1) : ( dist (y,q)) < (1 / m) }) iff (for x be object st x in (s .: ( square-uparrow n)) holds ex rx,ry be Real st x = <*rx*> & y = <*ry*> & |.(ry - rx).| < (1 / m))

    proof

      let s be Function of [: NAT , NAT :], ( TopSpaceMetr ( Euclid 1)), y be Point of ( Euclid 1);

      hereby

        assume

         A1: ((s .: ( square-uparrow n)) c= { q where q be Element of ( Euclid 1) : ( dist (y,q)) < (1 / m) });

        now

          let x be object;

          assume

           A2: x in (s .: ( square-uparrow n));

          then

          consider yo be object such that

           A3: yo in ( dom s) and yo in ( square-uparrow n) and

           A4: x = (s . yo) by FUNCT_1:def 6;

          reconsider z = x as Element of ( Euclid 1) by A3, A4, FUNCT_2: 5;

          z in { q where q be Element of ( Euclid 1) : ( dist (y,q)) < (1 / m) } by A2, A1;

          then

          consider q be Element of ( Euclid 1) such that

           A5: z = q and

           A6: ( dist (y,q)) < (1 / m);

          reconsider yr1 = y as Point of ( Euclid 1);

          yr1 in (1 -tuples_on REAL );

          then yr1 in the set of all <*r*> where r be Element of REAL by FINSEQ_2: 96;

          then

          consider ry be Element of REAL such that

           A8: yr1 = <*ry*>;

          reconsider zr1 = z as Point of ( Euclid 1);

          zr1 in (1 -tuples_on REAL );

          then zr1 in the set of all <*r*> where r be Element of REAL by FINSEQ_2: 96;

          then

          consider rx be Element of REAL such that

           A9: zr1 = <*rx*>;

           |.(ry - rx).| < (1 / m) by A5, A6, A8, A9, Th8;

          hence ex rx,ry be Real st x = <*rx*> & y = <*ry*> & |.(ry - rx).| < (1 / m) by A8, A9;

        end;

        hence for x be object st x in (s .: ( square-uparrow n)) holds ex rx,ry be Real st x = <*rx*> & y = <*ry*> & |.(ry - rx).| < (1 / m);

      end;

      assume

       A10: for x be object st x in (s .: ( square-uparrow n)) holds ex rx,ry be Real st x = <*rx*> & y = <*ry*> & |.(ry - rx).| < (1 / m);

      now

        let t be object;

        assume

         A11: t in (s .: ( square-uparrow n));

        then

        consider rx,ry be Real such that

         A12: t = <*rx*> and

         A13: y = <*ry*> and

         A14: |.(ry - rx).| < (1 / m) by A10;

        consider yo be object such that

         A15: yo in ( dom s) and yo in ( square-uparrow n) and

         A16: t = (s . yo) by A11, FUNCT_1:def 6;

        reconsider q = t as Element of ( Euclid 1) by A15, A16, FUNCT_2: 5;

        ( dist (y,q)) < (1 / m) by A12, A13, A14, Th8;

        hence t in { q where q be Element of ( Euclid 1) : ( dist (y,q)) < (1 / m) };

      end;

      hence ((s .: ( square-uparrow n)) c= { q where q be Element of ( Euclid 1) : ( dist (y,q)) < (1 / m) });

    end;

    theorem :: CARDFIL4:71

    

     Th58: r in ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) iff (for m be non zero Nat holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds |.((Rseq . (n1,n2)) - r).| < (1 / m))

    proof

      reconsider p = r as Point of RealSpace by XREAL_0:def 1;

      (for m be non zero Nat holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds ((Rseq . (n1,n2)) in { q where q be Point of RealSpace : ( dist (p,q)) < (1 / m) })) iff (for m be non zero Nat holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds |.((Rseq . (n1,n2)) - r).| < (1 / m))

      proof

        hereby

          assume

           A1: for m be non zero Nat holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds ((Rseq . (n1,n2)) in { q where q be Point of RealSpace : ( dist (p,q)) < (1 / m) });

          now

            let m be non zero Nat;

            consider n0 be Nat such that

             A2: for n1,n2 be Nat st n0 <= n1 & n0 <= n2 holds (Rseq . (n1,n2)) in { q where q be Point of RealSpace : ( dist (p,q)) < (1 / m) } by A1;

            take n0;

            for n1,n2 be Nat st n0 <= n1 & n0 <= n2 holds |.((Rseq . (n1,n2)) - r).| < (1 / m)

            proof

              let n1,n2 be Nat;

              assume n0 <= n1 & n0 <= n2;

              then (Rseq . (n1,n2)) in { q where q be Point of RealSpace : ( dist (p,q)) < (1 / m) } by A2;

              then

              consider q be Point of RealSpace such that

               A3: (Rseq . (n1,n2)) = q and

               A4: ( dist (p,q)) < (1 / m);

              reconsider qr = q as Real;

              ex xr,yr be Real st p = xr & q = yr & ( dist (p,q)) = ( real_dist . (p,q)) & ( dist (p,q)) = (( Pitag_dist 1) . ( <*p*>, <*q*>)) & ( dist (p,q)) = |.(xr - yr).| by Th6;

              hence |.((Rseq . (n1,n2)) - r).| < (1 / m) by A3, A4, COMPLEX1: 60;

            end;

            hence for n1,n2 be Nat st n0 <= n1 & n0 <= n2 holds |.((Rseq . (n1,n2)) - r).| < (1 / m);

          end;

          hence for m be non zero Nat holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds |.((Rseq . (n1,n2)) - r).| < (1 / m);

        end;

        assume

         A5: for m be non zero Nat holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds |.((Rseq . (n1,n2)) - r).| < (1 / m);

        now

          let m be non zero Nat;

          consider n0 be Nat such that

           A6: for n1,n2 be Nat st n0 <= n1 & n0 <= n2 holds |.((Rseq . (n1,n2)) - r).| < (1 / m) by A5;

          now

            take n0;

            hereby

              let n1,n2 be Nat;

              assume n0 <= n1 & n0 <= n2;

              then

               A7: |.((Rseq . (n1,n2)) - r).| < (1 / m) by A6;

              reconsider m1 = n1, m2 = n2 as Element of NAT by ORDINAL1:def 12;

              (Rseq . (m1,m2)) in the carrier of RealSpace ;

              then

              reconsider q = (Rseq . (n1,n2)) as Point of RealSpace ;

              consider xr,yr be Real such that

               A8: p = xr and

               A9: q = yr and ( dist (p,q)) = ( real_dist . (p,q)) and ( dist (p,q)) = (( Pitag_dist 1) . ( <*p*>, <*q*>)) and

               A10: ( dist (p,q)) = |.(xr - yr).| by Th6;

               |.(xr - yr).| < (1 / m) by A8, A9, A7, COMPLEX1: 60;

              hence (Rseq . (n1,n2)) in { q where q be Point of RealSpace : ( dist (p,q)) < (1 / m) } by A10;

            end;

          end;

          hence ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds (Rseq . (n1,n2)) in { q where q be Point of RealSpace : ( dist (p,q)) < (1 / m) };

        end;

        hence (for m be non zero Nat holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds ((Rseq . (n1,n2)) in { q where q be Point of RealSpace : ( dist (p,q)) < (1 / m) }));

      end;

      hence thesis by Th57;

    end;

    begin

    theorem :: CARDFIL4:72

    

     Th59: ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) <> {} implies ex x be Real st ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) = {x}

    proof

      assume

       A1: ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) <> {} ;

      reconsider s1 = Rseq as Function of [: NAT , NAT :], the carrier of R^1 ;

      consider x be object such that

       A2: ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) = {x} by A1, ZFMISC_1: 131;

      x in ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) by A2, TARSKI:def 1;

      hence thesis by A2;

    end;

    theorem :: CARDFIL4:73

    

     Th60: Rseq is P-convergent implies ( P-lim Rseq) in ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).)))

    proof

      assume

       A1: Rseq is P-convergent;

      for m be non zero Nat holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds |.((Rseq . (n1,n2)) - ( P-lim Rseq)).| < (1 / m)

      proof

        let m be non zero Nat;

        ( 0 / m) < (1 / m) by XREAL_1: 74;

        hence thesis by A1, DBLSEQ_1:def 2;

      end;

      hence ( P-lim Rseq) in ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) by Th58;

    end;

    theorem :: CARDFIL4:74

    

     Th61: Rseq is P-convergent iff ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) <> {}

    proof

      hereby

        assume Rseq is P-convergent;

        then

        consider x be Real such that

         A1: for e be Real st 0 < e holds ex N be Nat st for n,m be Nat st n >= N & m >= N holds |.((Rseq . (n,m)) - x).| < e;

        for m be non zero Nat holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds |.((Rseq . (n1,n2)) - x).| < (1 / m)

        proof

          let m be non zero Nat;

          ( 0 / m) < (1 / m) by XREAL_1: 74;

          hence thesis by A1;

        end;

        hence ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) <> {} by Th58;

      end;

      assume ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) <> {} ;

      then

      consider p be object such that

       A2: p in ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) by XBOOLE_0:def 1;

      reconsider p as Real by A2;

      ex p0 be Real st for e be Real st 0 < e holds ex N be Nat st for n,m be Nat st n >= N & m >= N holds |.((Rseq . (n,m)) - p0).| < e

      proof

        take p;

        hereby

          let e be Real;

          assume 0 < e;

          then ex m st m is non zero & (1 / m) < e by Th5;

          then

          consider m0 be non zero Nat such that m0 is non zero and

           A3: (1 / m0) < e;

          consider n0 be Nat such that

           A4: for n1,n2 be Nat st n0 <= n1 & n0 <= n2 holds |.((Rseq . (n1,n2)) - p).| < (1 / m0) by Th58, A2;

          now

            take N = n0;

            hereby

              let n,m be Nat;

              assume n >= N & m >= N;

              then |.((Rseq . (n,m)) - p).| < (1 / m0) by A4;

              hence |.((Rseq . (n,m)) - p).| < e by A3, XXREAL_0: 2;

            end;

          end;

          hence ex N be Nat st for n,m be Nat st n >= N & m >= N holds |.((Rseq . (n,m)) - p).| < e;

        end;

      end;

      hence Rseq is P-convergent;

    end;

    theorem :: CARDFIL4:75

    

     Th62: Rseq is P-convergent implies {( P-lim Rseq)} = ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).)))

    proof

      assume Rseq is P-convergent;

      then

       A1: ( P-lim Rseq) in ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) by Th60;

      then ex x be Real st ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) = {x} by Th59;

      hence {( P-lim Rseq)} = ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) by A1, TARSKI:def 1;

    end;

    theorem :: CARDFIL4:76

    ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) is non empty implies Rseq is P-convergent & {( P-lim Rseq)} = ( lim_filter (( # Rseq), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) by Th61, Th62;

    begin

    definition

      :: CARDFIL4:def8

      func dblseq_ex_1 -> Function of [: NAT , NAT :], REAL means

      : Def5: for m,n be Nat holds (it . (m,n)) = (1 / (m + 1));

      existence

      proof

        defpred P[ object, object] means ex r be Real, n1,n2 be Nat st $1 = [n1, n2] & $2 = r & r = (1 / (n1 + 1));

        

         A1: for x be object st x in [: NAT , NAT :] holds ex y be object st y in REAL & P[x, y]

        proof

          let x be object;

          assume x in [: NAT , NAT :];

          then

          consider n1,n2 be object such that

           A2: n1 in NAT and

           A3: n2 in NAT and

           A4: x = [n1, n2] by ZFMISC_1:def 2;

          reconsider n1, n2 as Nat by A2, A3;

          reconsider y = (1 / (n1 + 1)) as Real;

          take y;

          thus y in REAL by XREAL_0:def 1;

          thus P[x, y] by A3, A4;

        end;

        consider f be Function of [: NAT , NAT :], REAL such that

         A5: for x be object st x in [: NAT , NAT :] holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

        now

          let m,n be Nat;

          m in NAT & n in NAT by ORDINAL1:def 12;

          then [m, n] in [: NAT , NAT :] by ZFMISC_1:def 2;

          then

          consider r be Real, n1,n2 be Nat such that

           A6: [m, n] = [n1, n2] and

           A7: (f . [m, n]) = r and

           A8: r = (1 / (n1 + 1)) by A5;

          (f . (m,n)) = r by A7, BINOP_1:def 1

          .= (1 / (m + 1)) by A8, A6, XTUPLE_0: 1;

          hence (f . (m,n)) = (1 / (m + 1));

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be Function of [: NAT , NAT :], REAL such that

         A1: for m,n be Nat holds (F1 . (m,n)) = (1 / (m + 1)) and

         A2: for m,n be Nat holds (F2 . (m,n)) = (1 / (m + 1));

        now

          ( dom F1) = [: NAT , NAT :] & ( dom F2) = [: NAT , NAT :] by FUNCT_2:def 1;

          hence ( dom F1) = ( dom F2);

          hereby

            let x be object;

            assume x in ( dom F1);

            then

            consider n1,n2 be object such that

             A4: n1 in NAT and

             A5: n2 in NAT and

             A6: x = [n1, n2] by ZFMISC_1:def 2;

            reconsider n1, n2 as Nat by A4, A5;

            

            thus (F1 . x) = (F1 . (n1,n2)) by A6, BINOP_1:def 1

            .= (1 / (n1 + 1)) by A1

            .= (F2 . (n1,n2)) by A2

            .= (F2 . x) by A6, BINOP_1:def 1;

          end;

        end;

        hence thesis by FUNCT_1:def 11;

      end;

    end

    theorem :: CARDFIL4:77

    

     Th63: for m be non zero Nat holds ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds |.(( dblseq_ex_1 . (n1,n2)) - 0 ).| < (1 / m)

    proof

      let m be non zero Nat;

      now

        let n1,n2 be Nat;

        assume that

         A1: m <= n1 and m <= n2;

        (m + 0 ) < (n1 + 1) by A1, XREAL_1: 8;

        then (1 / (n1 + 1)) < (1 / m) by XREAL_1: 76;

        then |.((1 / (n1 + 1)) - 0 ).| < (1 / m) by ABSVALUE:def 1;

        hence |.(( dblseq_ex_1 . (n1,n2)) - 0 ).| < (1 / m) by Def5;

      end;

      hence ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds |.(( dblseq_ex_1 . (n1,n2)) - 0 ).| < (1 / m);

    end;

    theorem :: CARDFIL4:78

    

     Th64: 0 in ( lim_filter (( # dblseq_ex_1 ), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) by Th63, Th58;

    theorem :: CARDFIL4:79

    

     Th65: ( lim_filter (( # dblseq_ex_1 ),( Frechet_Filter [: NAT , NAT :]))) = {}

    proof

      assume ( lim_filter (( # dblseq_ex_1 ),( Frechet_Filter [: NAT , NAT :]))) <> {} ;

      then ( lim_filter (( # dblseq_ex_1 ),( Frechet_Filter [: NAT , NAT :]))) is non empty;

      then

      consider x be object such that

       A1: x in ( lim_filter (( # dblseq_ex_1 ),( Frechet_Filter [: NAT , NAT :])));

      

       A2: ( lim_filter (( # dblseq_ex_1 ),( Frechet_Filter [: NAT , NAT :]))) c= ( lim_filter (( # dblseq_ex_1 ), <. all-square-uparrow .))) by Th56;

      

       A3: <. all-square-uparrow .) = <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).) by Th34, CARDFIL2: 19, Th35;

      then

      consider y be Real such that

       A4: ( lim_filter (( # dblseq_ex_1 ), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) = {y} by A1, A2, Th59;

      y = 0 by A4, Th64;

      then

       A5: x = 0 by A1, A2, A3, A4, TARSKI:def 1;

      reconsider xp = 0 as Point of ( TopSpaceMetr RealSpace ) by Th64;

      

       A6: ( Balls xp) is basis of ( BOOL2F ( NeighborhoodSystem xp)) by CARDFIL3: 6;

      consider yr be Point of RealSpace such that

       A7: yr = xp and

       A8: ( Balls xp) = { ( Ball (yr,(1 / n))) where n be Nat : n <> 0 } by FRECHET:def 1;

      ( Ball (yr,(1 / 2))) in ( Balls xp) by A8;

      then

      consider i, j such that

       A9: for m, n st i <= m or j <= n holds ( dblseq_ex_1 . (m,n)) in ( Ball (yr,(1 / 2))) by A6, A5, A1, Th55;

      ( dblseq_ex_1 . ( 0 ,j)) in ( Ball (yr,(1 / 2))) by A9;

      then ( dblseq_ex_1 . ( 0 ,j)) in ].(yr - (1 / 2)), (yr + (1 / 2)).[ by FRECHET: 7;

      then (1 / ( 0 + 1)) in ].(yr - (1 / 2)), (yr + (1 / 2)).[ by Def5;

      hence thesis by A7, XXREAL_1: 4;

    end;

    theorem :: CARDFIL4:80

    ( lim_filter (( # dblseq_ex_1 ), <.( Frechet_Filter NAT ), ( Frechet_Filter NAT ).))) <> ( lim_filter (( # dblseq_ex_1 ),( Frechet_Filter [: NAT , NAT :]))) by Th63, Th58, Th65;

    begin

    definition

      let X1,X2 be non empty set, cF1 be Filter of X1, Y be Hausdorff non empty TopSpace, f be Function of [:X1, X2:], Y;

      assume

       A1: for x be Element of X2 holds ( lim_filter (( ProjMap2 (f,x)),cF1)) <> {} ;

      :: CARDFIL4:def9

      func lim_in_cod1 (f,cF1) -> Function of X2, Y means

      : Def6: (for x be Element of X2 holds {(it . x)} = ( lim_filter (( ProjMap2 (f,x)),cF1)));

      existence

      proof

        defpred P[ object, object] means ex x be Element of X2, y be Element of Y st x = $1 & y = $2 & $2 in ( lim_filter (( ProjMap2 (f,x)),cF1));

        

         A2: for x be object st x in X2 holds ex y be object st y in the carrier of Y & P[x, y]

        proof

          let x be object;

          assume x in X2;

          then

          reconsider x2 = x as Element of X2;

          ( lim_filter (( ProjMap2 (f,x2)),cF1)) is non empty by A1;

          then

          consider y be object such that

           A3: y in ( lim_filter (( ProjMap2 (f,x2)),cF1));

          take y;

          thus y in the carrier of Y by A3;

          thus P[x, y] by A3;

        end;

        consider g1 be Function of X2, the carrier of Y such that

         A4: for x be object st x in X2 holds P[x, (g1 . x)] from FUNCT_2:sch 1( A2);

        reconsider g2 = g1 as Function of X2, Y;

        take g2;

        hereby

          let x be Element of X2;

           P[x, (g2 . x)] by A4;

          then

          consider x2 be Element of X2, y1 be Element of Y such that

           A5: x = x2 and

           A6: (g2 . x) = y1 and

           A7: y1 in ( lim_filter (( ProjMap2 (f,x2)),cF1));

          ( lim_filter (( ProjMap2 (f,x)),cF1)) is non empty trivial by A1;

          then ex z be object st ( lim_filter (( ProjMap2 (f,x)),cF1)) = {z} by ZFMISC_1: 131;

          hence {(g2 . x)} = ( lim_filter (( ProjMap2 (f,x)),cF1)) by A5, A6, A7, TARSKI:def 1;

        end;

      end;

      uniqueness

      proof

        let g1,g2 be Function of X2, Y such that

         A1: for x be Element of X2 holds {(g1 . x)} = ( lim_filter (( ProjMap2 (f,x)),cF1)) and

         A2: for x be Element of X2 holds {(g2 . x)} = ( lim_filter (( ProjMap2 (f,x)),cF1));

        now

          let x be Element of X2;

           {(g1 . x)} = ( lim_filter (( ProjMap2 (f,x)),cF1)) by A1;

          then {(g1 . x)} = {(g2 . x)} by A2;

          hence (g1 . x) = (g2 . x) by ZFMISC_1: 3;

        end;

        hence g1 = g2 by FUNCT_2:def 8;

      end;

    end

    definition

      let X1,X2 be non empty set, cF2 be Filter of X2, Y be Hausdorff non empty TopSpace, f be Function of [:X1, X2:], Y;

      assume

       A1: for x be Element of X1 holds ( lim_filter (( ProjMap1 (f,x)),cF2)) <> {} ;

      :: CARDFIL4:def10

      func lim_in_cod2 (f,cF2) -> Function of X1, Y means

      : Def7: (for x be Element of X1 holds {(it . x)} = ( lim_filter (( ProjMap1 (f,x)),cF2)));

      existence

      proof

        defpred P[ object, object] means ex x be Element of X1, y be Element of Y st x = $1 & y = $2 & $2 in ( lim_filter (( ProjMap1 (f,x)),cF2));

        

         A2: for x be object st x in X1 holds ex y be object st y in the carrier of Y & P[x, y]

        proof

          let x be object;

          assume x in X1;

          then

          reconsider x1 = x as Element of X1;

          ( lim_filter (( ProjMap1 (f,x1)),cF2)) is non empty by A1;

          then

          consider y be object such that

           A3: y in ( lim_filter (( ProjMap1 (f,x1)),cF2));

          take y;

          thus y in the carrier of Y by A3;

          thus P[x, y] by A3;

        end;

        consider g1 be Function of X1, the carrier of Y such that

         A4: for x be object st x in X1 holds P[x, (g1 . x)] from FUNCT_2:sch 1( A2);

        reconsider g2 = g1 as Function of X1, Y;

        take g2;

        hereby

          let x be Element of X1;

           P[x, (g2 . x)] by A4;

          then

          consider x1 be Element of X1, y1 be Element of Y such that

           A5: x = x1 and

           A6: (g2 . x) = y1 and

           A7: y1 in ( lim_filter (( ProjMap1 (f,x1)),cF2));

          ( lim_filter (( ProjMap1 (f,x)),cF2)) is non empty trivial by A1;

          then ex z be object st ( lim_filter (( ProjMap1 (f,x)),cF2)) = {z} by ZFMISC_1: 131;

          hence {(g2 . x)} = ( lim_filter (( ProjMap1 (f,x)),cF2)) by A5, A6, A7, TARSKI:def 1;

        end;

      end;

      uniqueness

      proof

        let g1,g2 be Function of X1, Y such that

         A1: for x be Element of X1 holds {(g1 . x)} = ( lim_filter (( ProjMap1 (f,x)),cF2)) and

         A2: for x be Element of X1 holds {(g2 . x)} = ( lim_filter (( ProjMap1 (f,x)),cF2));

        now

          let x be Element of X1;

           {(g1 . x)} = ( lim_filter (( ProjMap1 (f,x)),cF2)) by A1;

          then {(g1 . x)} = {(g2 . x)} by A2;

          hence (g1 . x) = (g2 . x) by ZFMISC_1: 3;

        end;

        hence g1 = g2 by FUNCT_2:def 8;

      end;

    end

    theorem :: CARDFIL4:81

    for f be Function of X, REAL holds f is Function of X, R^1 ;

    theorem :: CARDFIL4:82

    for s be sequence of REAL holds s is Function of NAT , R^1 ;

    reserve f for Function of ( [#] OrderedNAT ), R^1 ,

seq for Function of NAT , REAL ;

    theorem :: CARDFIL4:83

    

     Th70: f = seq & ( lim_f f) <> {} implies seq is convergent & ex z be Real st z in ( lim_f f) & for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - z).| < p

    proof

      assume that

       A1: f = seq and

       A2: ( lim_f f) <> {} ;

      consider x be object such that

       A3: x in ( lim_f f) by A2, XBOOLE_0:def 1;

      reconsider y = x as Point of ( TopSpaceMetr RealSpace ) by A3;

      reconsider z = y as Real;

      

       A4: ( Balls y) is basis of ( BOOL2F ( NeighborhoodSystem y)) by CARDFIL3: 6;

      consider yr be Point of RealSpace such that

       A5: yr = y and

       A6: ( Balls y) = { ( Ball (yr,(1 / n))) where n be Nat : n <> 0 } by FRECHET:def 1;

      

       A7: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - z).| < p

      proof

        now

          let p be Real;

          assume 0 < p;

          then

          consider M be Nat such that

           A8: M is non zero and

           A9: (1 / M) < p by Th5;

          now

            ( Ball (yr,(1 / M))) in ( Balls y) by A8, A6;

            then

            consider i be Element of OrderedNAT such that

             A10: for j be Element of OrderedNAT st i <= j holds (f . j) in ( Ball (yr,(1 / M))) by A4, A3, CARDFIL2: 84;

            reconsider i0 = i as Nat;

            take i0;

            let m be Nat;

            assume

             A11: i0 <= m;

            reconsider m0 = m as Element of OrderedNAT by ORDINAL1:def 12;

            m0 in { x where x be Element of NAT : ex p0 be Element of NAT st i0 = p0 & p0 <= x } by A11;

            then m0 in ( uparrow i) by CARDFIL2: 50;

            then (f . m0) in ( Ball (yr,(1 / M))) by A10, WAYBEL_0: 18;

            then (f . m0) in ].(yr - (1 / M)), (yr + (1 / M)).[ by FRECHET: 7;

            then

             A12: (yr - (1 / M)) < (seq . m0) < (yr + (1 / M)) by A1, XXREAL_1: 4;

            (yr - p) < (yr - (1 / M)) & (yr + (1 / M)) < (yr + p) by A9, XREAL_1: 8, XREAL_1: 15;

            then (yr - p) < (seq . m0) < (yr + p) by A12, XXREAL_0: 2;

            then (seq . m0) in ].(yr - p), (yr + p).[ by XXREAL_1: 4;

            then (f . m0) in ( Ball (yr,p)) by A1, FRECHET: 7;

            then (f . m0) in { q where q be Element of RealSpace : ( dist (yr,q)) < p } by METRIC_1:def 14;

            then

            consider q0 be Element of RealSpace such that

             A13: (f . m0) = q0 and

             A14: ( dist (yr,q0)) < p;

            reconsider g2 = yr as Point of RealSpace ;

            ex x1r,y1r be Real st q0 = x1r & g2 = y1r & ( dist (q0,g2)) = ( real_dist . (q0,g2)) & ( dist (q0,g2)) = (( Pitag_dist 1) . ( <*q0*>, <*g2*>)) & ( dist (q0,g2)) = |.(x1r - y1r).| by Th6;

            hence |.((seq . m) - z).| < p by A14, A1, A5, A13;

          end;

          hence ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - z).| < p;

        end;

        hence thesis;

      end;

      hence seq is convergent by SEQ_2:def 6;

      thus ex z be Real st z in ( lim_f f) & for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - z).| < p by A3, A7;

    end;

    theorem :: CARDFIL4:84

    

     Th71: f = seq & ( lim_f f) <> {} implies ( lim_f f) = {( lim seq)}

    proof

      assume that

       A1: f = seq and

       A2: ( lim_f f) <> {} ;

      consider x be object such that

       A3: x in ( lim_f f) by A2, XBOOLE_0:def 1;

      reconsider y = x as Point of R^1 by A3;

      consider u be object such that

       A4: ( lim_f f) = {u} by A3, ZFMISC_1: 131;

      ( lim_f f) = {( lim seq)}

      proof

        ( lim_f f) c= {( lim seq)}

        proof

          let t be object;

          assume

           A5: t in ( lim_f f);

          then

          reconsider t1 = t as Real;

          

           A6: seq is convergent & ex z be Real st z in ( lim_f f) & for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - z).| < p by A1, A2, Th70;

          consider z be Real such that

           A7: z in ( lim_f f) and

           A8: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - z).| < p by A1, A2, Th70;

          t = u & z = u by A5, A7, A4, TARSKI:def 1;

          then t1 = ( lim seq) by A8, A6, SEQ_2:def 7;

          hence thesis by TARSKI:def 1;

        end;

        hence thesis by A4, ZFMISC_1: 3;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL4:85

    for f be Function of ( [#] OrderedNAT ), T holds for s be sequence of T st f = s holds ( lim_f f) = ( lim_f s) by CARDFIL2: 54;

    theorem :: CARDFIL4:86

    for f be Function of ( [#] OrderedNAT ), T holds for g be Function of NAT , T st f = g holds ( lim_f f) = ( lim_f g) by CARDFIL2: 54;

    theorem :: CARDFIL4:87

    

     Th72: for f be Function of NAT , R^1 st f = seq & ( lim_f f) <> {} holds ( lim_f f) = {( lim seq)}

    proof

      let f be Function of NAT , R^1 ;

      assume that

       A1: f = seq and

       A2: ( lim_f f) <> {} ;

      ( [#] OrderedNAT ) = NAT & the carrier of R^1 = REAL by STRUCT_0:def 3;

      then

      reconsider f1 = f as Function of ( [#] OrderedNAT ), R^1 ;

      ( lim_f f) = ( lim_f f1) by CARDFIL2: 54;

      hence thesis by A1, A2, Th71;

    end;

    theorem :: CARDFIL4:88

    (for x be Element of NAT holds ( lim_filter (( ProjMap2 (( # Rseq),x)),( Frechet_Filter NAT ))) <> {} ) iff Rseq is convergent_in_cod1

    proof

      hereby

        assume

         A1: for x be Element of NAT holds ( lim_filter (( ProjMap2 (( # Rseq),x)),( Frechet_Filter NAT ))) <> {} ;

        now

          let m be Element of NAT ;

          ( lim_filter (( ProjMap2 (( # Rseq),m)),( Frechet_Filter NAT ))) is non empty by A1;

          then

          consider r be Element of ( TopSpaceMetr RealSpace ) such that

           A2: r in ( lim_filter (( ProjMap2 (( # Rseq),m)),( Frechet_Filter NAT )));

          

           A3: r in ( lim_f ( ProjMap2 (( # Rseq),m))) by A2;

          

           A4: ( Balls r) is basis of ( BOOL2F ( NeighborhoodSystem r)) by CARDFIL3: 6;

          reconsider r1 = r as Real;

          now

            let e be Real;

            assume 0 < e;

            then

            consider m1 be Nat such that

             A5: m1 is non zero and

             A6: (1 / m1) < e by Th5;

            consider y be Point of RealSpace such that

             A7: y = r and

             A8: ( Balls r) = { ( Ball (y,(1 / n))) where n be Nat : n <> 0 } by FRECHET:def 1;

            

             A9: ( Ball (y,(1 / m1))) c= ( Ball (y,e)) by A6, PCOMPS_1: 1;

            ( Ball (y,(1 / m1))) in ( Balls r) by A8, A5;

            then

            consider i be Nat such that

             A10: for j be Nat st i <= j holds (( ProjMap2 (( # Rseq),m)) . j) in ( Ball (y,(1 / m1))) by A4, A3, CARDFIL2: 97;

            thus ex N be Nat st for n be Nat st N <= n holds |.((( ProjMap2 (Rseq,m)) . n) - r1).| < e

            proof

              take i;

              let j be Nat;

              assume i <= j;

              then (( ProjMap2 (( # Rseq),m)) . j) in ( Ball (y,e)) by A9, A10;

              then (( ProjMap2 (( # Rseq),m)) . j) in ].(y - e), (y + e).[ by FRECHET: 7;

              hence thesis by A7, FCONT_3: 1;

            end;

          end;

          hence ( ProjMap2 (Rseq,m)) is convergent by SEQ_2:def 6;

        end;

        hence Rseq is convergent_in_cod1;

      end;

      assume

       A13: Rseq is convergent_in_cod1;

      now

        let x be Element of NAT ;

        consider r be Real such that

         A14: for p be Real st 0 < p holds ex n st for m be Nat st n <= m holds |.((( ProjMap2 (Rseq,x)) . m) - r).| < p by A13, SEQ_2:def 6;

        reconsider r1 = r as Point of ( TopSpaceMetr RealSpace ) by XREAL_0:def 1;

        

         A15: ( Balls r1) is basis of ( BOOL2F ( NeighborhoodSystem r1)) by CARDFIL3: 6;

        for b be Element of ( Balls r1) holds ex i be Nat st for j be Nat st i <= j holds (( ProjMap2 (( # Rseq),x)) . j) in b

        proof

          let b be Element of ( Balls r1);

          consider y be Point of RealSpace such that

           A16: y = r1 and

           A17: ( Balls r1) = { ( Ball (y,(1 / n))) where n be Nat : n <> 0 } by FRECHET:def 1;

          b in { ( Ball (y,(1 / n))) where n be Nat : n <> 0 } by A17;

          then

          consider n0 be Nat such that

           A18: b = ( Ball (y,(1 / n0))) and

           A19: n0 <> 0 ;

           0 < n0 & ( 0 * n0) < 1 by A19;

          then

          consider n1 be Nat such that

           A20: for m be Nat st n1 <= m holds |.((( ProjMap2 (Rseq,x)) . m) - r).| < (1 / n0) by A14, XREAL_1: 81;

          now

            take n1;

            hereby

              let j be Nat;

              assume n1 <= j;

              then

               A21: |.((( ProjMap2 (Rseq,x)) . j) - r).| < (1 / n0) by A20;

              (( ProjMap2 (Rseq,x)) . j) = (r + ((( ProjMap2 (Rseq,x)) . j) - r));

              then (( ProjMap2 (Rseq,x)) . j) in ].(r - (1 / n0)), (r + (1 / n0)).[ by A21, FCONT_3: 3;

              hence (( ProjMap2 (( # Rseq),x)) . j) in b by A16, A18, FRECHET: 7;

            end;

          end;

          hence ex i be Nat st for j be Nat st i <= j holds (( ProjMap2 (( # Rseq),x)) . j) in b;

        end;

        then ( lim_f ( ProjMap2 (( # Rseq),x))) <> {} by A15, CARDFIL2: 97;

        hence ( lim_filter (( ProjMap2 (( # Rseq),x)),( Frechet_Filter NAT ))) <> {} ;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL4:89

    (for x be Element of NAT holds ( lim_filter (( ProjMap1 (( # Rseq),x)),( Frechet_Filter NAT ))) <> {} ) iff Rseq is convergent_in_cod2

    proof

      hereby

        assume

         A1: for x be Element of NAT holds ( lim_filter (( ProjMap1 (( # Rseq),x)),( Frechet_Filter NAT ))) <> {} ;

        now

          let m be Element of NAT ;

          ( lim_filter (( ProjMap1 (( # Rseq),m)),( Frechet_Filter NAT ))) is non empty by A1;

          then

          consider r be Element of ( TopSpaceMetr RealSpace ) such that

           A2: r in ( lim_filter (( ProjMap1 (( # Rseq),m)),( Frechet_Filter NAT )));

          

           A3: r in ( lim_f ( ProjMap1 (( # Rseq),m))) by A2;

          

           A4: ( Balls r) is basis of ( BOOL2F ( NeighborhoodSystem r)) by CARDFIL3: 6;

          reconsider r1 = r as Real;

          now

            let e be Real;

            assume 0 < e;

            then

            consider m1 be Nat such that

             A5: m1 is non zero and

             A6: (1 / m1) < e by Th5;

            consider y be Point of RealSpace such that

             A7: y = r and

             A8: ( Balls r) = { ( Ball (y,(1 / n))) where n be Nat : n <> 0 } by FRECHET:def 1;

            

             A9: ( Ball (y,(1 / m1))) c= ( Ball (y,e)) by A6, PCOMPS_1: 1;

            ( Ball (y,(1 / m1))) in ( Balls r) by A8, A5;

            then

            consider i be Nat such that

             A10: for j be Nat st i <= j holds (( ProjMap1 (( # Rseq),m)) . j) in ( Ball (y,(1 / m1))) by A4, A3, CARDFIL2: 97;

            thus ex N be Nat st for n be Nat st N <= n holds |.((( ProjMap1 (Rseq,m)) . n) - r1).| < e

            proof

              take i;

              let j be Nat;

              assume i <= j;

              then (( ProjMap1 (( # Rseq),m)) . j) in ( Ball (y,e)) by A9, A10;

              then (( ProjMap1 (( # Rseq),m)) . j) in ].(y - e), (y + e).[ by FRECHET: 7;

              hence thesis by A7, FCONT_3: 1;

            end;

          end;

          hence ( ProjMap1 (Rseq,m)) is convergent by SEQ_2:def 6;

        end;

        hence Rseq is convergent_in_cod2;

      end;

      assume

       A11: Rseq is convergent_in_cod2;

      now

        let x be Element of NAT ;

        consider r be Real such that

         A12: for p be Real st 0 < p holds ex n st for m be Nat st n <= m holds |.((( ProjMap1 (Rseq,x)) . m) - r).| < p by A11, SEQ_2:def 6;

        reconsider r1 = r as Point of ( TopSpaceMetr RealSpace ) by XREAL_0:def 1;

        

         A13: ( Balls r1) is basis of ( BOOL2F ( NeighborhoodSystem r1)) by CARDFIL3: 6;

        for b be Element of ( Balls r1) holds ex i be Nat st for j be Nat st i <= j holds (( ProjMap1 (( # Rseq),x)) . j) in b

        proof

          let b be Element of ( Balls r1);

          consider y be Point of RealSpace such that

           A14: y = r1 and

           A15: ( Balls r1) = { ( Ball (y,(1 / n))) where n be Nat : n <> 0 } by FRECHET:def 1;

          b in { ( Ball (y,(1 / n))) where n be Nat : n <> 0 } by A15;

          then

          consider n0 be Nat such that

           A16: b = ( Ball (y,(1 / n0))) and

           A17: n0 <> 0 ;

           0 < n0 & ( 0 * n0) < 1 by A17;

          then

          consider n1 be Nat such that

           A18: for m be Nat st n1 <= m holds |.((( ProjMap1 (Rseq,x)) . m) - r).| < (1 / n0) by A12, XREAL_1: 81;

          now

            take n1;

            hereby

              let j be Nat;

              assume n1 <= j;

              then

               A19: |.((( ProjMap1 (Rseq,x)) . j) - r).| < (1 / n0) by A18;

              (( ProjMap1 (Rseq,x)) . j) = (r + ((( ProjMap1 (Rseq,x)) . j) - r));

              then (( ProjMap1 (Rseq,x)) . j) in ].(r - (1 / n0)), (r + (1 / n0)).[ by A19, FCONT_3: 3;

              hence (( ProjMap1 (( # Rseq),x)) . j) in b by A14, A16, FRECHET: 7;

            end;

          end;

          hence ex i be Nat st for j be Nat st i <= j holds (( ProjMap1 (( # Rseq),x)) . j) in b;

        end;

        then ( lim_f ( ProjMap1 (( # Rseq),x))) is non empty by A13, CARDFIL2: 97;

        hence ( lim_filter (( ProjMap1 (( # Rseq),x)),( Frechet_Filter NAT ))) is non empty;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL4:90

    

     Th73: for t be Element of NAT , f be Function of [: NAT , NAT :], R^1 holds for seq be Function of [: NAT , NAT :], REAL st f = seq & (for x be Element of NAT holds ( lim_filter (( ProjMap1 (f,x)),( Frechet_Filter NAT ))) <> {} ) holds ( lim_filter (( ProjMap1 (f,t)),( Frechet_Filter NAT ))) = {( lim ( ProjMap1 (seq,t)))}

    proof

      let t be Element of NAT , f be Function of [: NAT , NAT :], R^1 ;

      let seq be Function of [: NAT , NAT :], REAL ;

      assume that

       A1: f = seq and

       A2: for x be Element of NAT holds ( lim_filter (( ProjMap1 (f,x)),( Frechet_Filter NAT ))) <> {} ;

      ( lim_filter (( ProjMap1 (f,t)),( Frechet_Filter NAT ))) is non empty trivial by A2;

      then

      consider x be object such that

       A3: ( lim_filter (( ProjMap1 (f,t)),( Frechet_Filter NAT ))) = {x} by ZFMISC_1: 131;

      reconsider f1 = ( ProjMap1 (f,t)) as Function of NAT , R^1 ;

      reconsider seq1 = ( ProjMap1 (seq,t)) as Function of NAT , REAL ;

      ( lim_f f1) = {( lim seq1)} by A1, A3, Th72;

      hence thesis;

    end;

    theorem :: CARDFIL4:91

    

     Th74: for t be Element of NAT , f be Function of [: NAT , NAT :], R^1 holds for seq be Function of [: NAT , NAT :], REAL st f = seq & (for x be Element of NAT holds ( lim_filter (( ProjMap2 (f,x)),( Frechet_Filter NAT ))) <> {} ) holds ( lim_filter (( ProjMap2 (f,t)),( Frechet_Filter NAT ))) = {( lim ( ProjMap2 (seq,t)))}

    proof

      let t be Element of NAT , f be Function of [: NAT , NAT :], R^1 ;

      let seq be Function of [: NAT , NAT :], REAL ;

      assume that

       A1: f = seq and

       A2: for x be Element of NAT holds ( lim_filter (( ProjMap2 (f,x)),( Frechet_Filter NAT ))) <> {} ;

      ( lim_filter (( ProjMap2 (f,t)),( Frechet_Filter NAT ))) is non empty trivial by A2;

      then

      consider x be object such that

       A3: ( lim_filter (( ProjMap2 (f,t)),( Frechet_Filter NAT ))) = {x} by ZFMISC_1: 131;

      reconsider f1 = ( ProjMap2 (f,t)) as Function of NAT , R^1 ;

      reconsider seq1 = ( ProjMap2 (seq,t)) as Function of NAT , REAL ;

      ( lim_f f1) = {( lim seq1)} by A1, A3, Th72;

      hence thesis;

    end;

    theorem :: CARDFIL4:92

    for Y be Hausdorff non empty TopSpace, f be Function of [: NAT , NAT :], Y st (for x be Element of NAT holds ( lim_filter (( ProjMap2 (f,x)),( Frechet_Filter NAT ))) <> {} ) & f = Rseq & Y = R^1 holds ( lim_in_cod1 (f,( Frechet_Filter NAT ))) = ( lim_in_cod1 Rseq)

    proof

      let Y be Hausdorff non empty TopSpace, f be Function of [: NAT , NAT :], Y;

      assume that

       A1: for x be Element of NAT holds ( lim_filter (( ProjMap2 (f,x)),( Frechet_Filter NAT ))) <> {} and

       A2: f = Rseq and

       A3: Y = R^1 ;

      now

        ( dom ( lim_in_cod1 (f,( Frechet_Filter NAT )))) = NAT by FUNCT_2:def 1;

        hence ( dom ( lim_in_cod1 (f,( Frechet_Filter NAT )))) = ( dom ( lim_in_cod1 Rseq)) by FUNCT_2:def 1;

        thus for t be object st t in ( dom ( lim_in_cod1 (f,( Frechet_Filter NAT )))) holds (( lim_in_cod1 (f,( Frechet_Filter NAT ))) . t) = (( lim_in_cod1 Rseq) . t)

        proof

          let t be object;

          assume t in ( dom ( lim_in_cod1 (f,( Frechet_Filter NAT ))));

          then

          reconsider t1 = t as Element of NAT ;

          

           A4: {(( lim_in_cod1 (f,( Frechet_Filter NAT ))) . t1)} = ( lim_filter (( ProjMap2 (f,t1)),( Frechet_Filter NAT ))) by A1, Def6;

          ( lim_filter (( ProjMap2 (f,t1)),( Frechet_Filter NAT ))) = {( lim ( ProjMap2 (Rseq,t1)))} by A1, A3, A2, Th74

          .= {(( lim_in_cod1 Rseq) . t1)} by DBLSEQ_1:def 5;

          hence thesis by A4, ZFMISC_1: 3;

        end;

      end;

      hence thesis by FUNCT_1:def 11;

    end;

    theorem :: CARDFIL4:93

    for Y be non empty Hausdorff TopSpace, f be Function of [: NAT , NAT :], Y st (for x be Element of NAT holds ( lim_filter (( ProjMap1 (f,x)),( Frechet_Filter NAT ))) <> {} ) & f = Rseq & Y = R^1 holds ( lim_in_cod2 (f,( Frechet_Filter NAT ))) = ( lim_in_cod2 Rseq)

    proof

      let Y be non empty Hausdorff TopSpace, f be Function of [: NAT , NAT :], Y;

      assume that

       A1: for x be Element of NAT holds ( lim_filter (( ProjMap1 (f,x)),( Frechet_Filter NAT ))) <> {} and

       A2: f = Rseq and

       A3: Y = R^1 ;

      now

        ( dom ( lim_in_cod2 (f,( Frechet_Filter NAT )))) = NAT by FUNCT_2:def 1;

        hence ( dom ( lim_in_cod2 (f,( Frechet_Filter NAT )))) = ( dom ( lim_in_cod2 Rseq)) by FUNCT_2:def 1;

        thus for t be object st t in ( dom ( lim_in_cod2 (f,( Frechet_Filter NAT )))) holds (( lim_in_cod2 (f,( Frechet_Filter NAT ))) . t) = (( lim_in_cod2 Rseq) . t)

        proof

          let t be object;

          assume t in ( dom ( lim_in_cod2 (f,( Frechet_Filter NAT ))));

          then

          reconsider t1 = t as Element of NAT ;

          

           A4: {(( lim_in_cod2 (f,( Frechet_Filter NAT ))) . t1)} = ( lim_filter (( ProjMap1 (f,t1)),( Frechet_Filter NAT ))) by A1, Def7;

          ( lim_filter (( ProjMap1 (f,t1)),( Frechet_Filter NAT ))) = {( lim ( ProjMap1 (Rseq,t1)))} by A1, A3, A2, Th73

          .= {(( lim_in_cod2 Rseq) . t1)} by DBLSEQ_1:def 6;

          hence thesis by A4, ZFMISC_1: 3;

        end;

      end;

      hence ( lim_in_cod2 (f,( Frechet_Filter NAT ))) = ( lim_in_cod2 Rseq) by FUNCT_1:def 11;

    end;

    begin

    reserve Y for non empty TopSpace,

x for Point of Y,

f for Function of [:X1, X2:], Y;

    theorem :: CARDFIL4:94

    x in ( lim_filter (f, <.cF1, cF2.))) & <.cB1.) = cF1 & <.cB2.) = cF2 implies for V be Subset of Y st V is open & x in V holds ex B1 be Element of cB1, B2 be Element of cB2 st (f .: [:B1, B2:]) c= V

    proof

      assume that

       A1: x in ( lim_filter (f, <.cF1, cF2.))) and

       A2: <.cB1.) = cF1 and

       A3: <.cB2.) = cF2;

      reconsider FF = ( filter_image (f, <.cF1, cF2.))) as Filter of the carrier of Y;

      let V be Subset of Y;

      assume that

       A4: V is open and

       A5: x in V;

      V in { M where M be Subset of Y : (f " M) in <.cF1, cF2.) } by A1, A4, A5, CARDFIL2: 80, WAYBEL_7:def 5;

      then

      consider M be Subset of Y such that

       A6: V = M and

       A7: (f " M) in <.cF1, cF2.);

       <.cF1, cF2.) = <. [:cB1, cB2:].) by A2, A3, Def1;

      then

      consider B be Element of [:cB1, cB2:] such that

       A8: B c= (f " M) by A7, CARDFIL2:def 8;

      B in [:cB1, cB2:];

      then

      consider B1 be Element of cB1, B2 be Element of cB2 such that

       A9: B = [:B1, B2:];

      take B1, B2;

      

       A10: (f .: [:B1, B2:]) c= (f .: (f " M)) by A8, A9, RELAT_1: 123;

      (f .: (f " M)) c= M by FUNCT_1: 75;

      hence thesis by A6, A10;

    end;

    theorem :: CARDFIL4:95

    

     Th75: x in ( lim_filter (f, <.cF1, cF2.))) & <.cB1.) = cF1 & <.cB2.) = cF2 implies for U be a_neighborhood of x st U is closed holds ex B1 be Element of cB1, B2 be Element of cB2 st (f .: [:B1, B2:]) c= ( Int U)

    proof

      assume that

       A1: x in ( lim_filter (f, <.cF1, cF2.))) and

       A2: <.cB1.) = cF1 and

       A3: <.cB2.) = cF2;

      reconsider FF = ( filter_image (f, <.cF1, cF2.))) as Filter of the carrier of Y;

      let U be a_neighborhood of x;

      assume U is closed;

      x in ( Int U) by CONNSP_2:def 1;

      then ( Int U) in { M where M be Subset of Y : (f " M) in <.cF1, cF2.) } by A1, CARDFIL2: 80, WAYBEL_7:def 5;

      then

      consider M be Subset of Y such that

       A4: ( Int U) = M and

       A5: (f " M) in <.cF1, cF2.);

       <.cF1, cF2.) = <. [:cB1, cB2:].) by A2, A3, Def1;

      then

      consider B be Element of [:cB1, cB2:] such that

       A6: B c= (f " M) by A5, CARDFIL2:def 8;

      B in [:cB1, cB2:];

      then

      consider B1 be Element of cB1, B2 be Element of cB2 such that

       A7: B = [:B1, B2:];

      take B1, B2;

      

       A8: (f .: [:B1, B2:]) c= (f .: (f " M)) by A6, A7, RELAT_1: 123;

      (f .: (f " M)) c= M by FUNCT_1: 75;

      hence thesis by A4, A8;

    end;

    theorem :: CARDFIL4:96

    x in ( lim_filter (f, <.cF1, cF2.))) & <.cB1.) = cF1 & <.cB2.) = cF2 implies for U be a_neighborhood of x st U is closed holds ex B1 be Element of cB1, B2 be Element of cB2 st for y be Element of B1 holds (f .: [: {y}, B2:]) c= ( Int U)

    proof

      assume that

       A1: x in ( lim_filter (f, <.cF1, cF2.))) and

       A2: <.cB1.) = cF1 and

       A3: <.cB2.) = cF2;

      now

        let U be a_neighborhood of x;

        assume U is closed;

        then

        consider B1 be Element of cB1, B2 be Element of cB2 such that

         A4: (f .: [:B1, B2:]) c= ( Int U) by A1, A2, A3, Th75;

        take B1, B2;

        let y be Element of B1;

         [: {y}, B2:] c= [:B1, B2:] by ZFMISC_1: 95;

        then (f .: [: {y}, B2:]) c= (f .: [:B1, B2:]) by RELAT_1: 125;

        hence (f .: [: {y}, B2:]) c= ( Int U) by A4;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL4:97

    

     Th76: x in ( lim_filter (f, <.cF1, cF2.))) & <.cB1.) = cF1 & <.cB2.) = cF2 implies for U be a_neighborhood of x st U is closed holds ex B1 be Element of cB1, B2 be Element of cB2 st for z be Element of X1, y be Element of Y st z in B1 & y in ( lim_filter (( ProjMap1 (f,z)),cF2)) holds y in ( Cl ( Int U))

    proof

      assume that

       A1: x in ( lim_filter (f, <.cF1, cF2.))) and

       A2: <.cB1.) = cF1 and

       A3: <.cB2.) = cF2;

      let U be a_neighborhood of x;

      assume U is closed;

      then

      consider B1 be Element of cB1, B2 be Element of cB2 such that

       A4: (f .: [:B1, B2:]) c= ( Int U) by A1, A2, A3, Th75;

      take B1, B2;

      

       A5: for y be Element of B1 holds (f .: [: {y}, B2:]) c= ( Int U)

      proof

        let y be Element of B1;

         [: {y}, B2:] c= [:B1, B2:] by ZFMISC_1: 95;

        then (f .: [: {y}, B2:]) c= (f .: [:B1, B2:]) by RELAT_1: 125;

        hence thesis by A4;

      end;

      

       A6: for z be Element of B1, y be Element of Y st y in ( lim_filter (( ProjMap1 (f,z)),cF2)) holds ( filter_image (( ProjMap1 (f,z)),cF2)) is proper Filter of ( BoolePoset ( [#] Y)) & ( Int U) in ( filter_image (( ProjMap1 (f,z)),cF2)) & y is_a_cluster_point_of (( filter_image (( ProjMap1 (f,z)),cF2)),Y)

      proof

        let z be Element of B1, y be Element of Y;

        assume

         A7: y in ( lim_filter (( ProjMap1 (f,z)),cF2));

        ( filter_image (( ProjMap1 (f,z)),cF2)) is Filter of ( [#] Y) by STRUCT_0:def 3;

        hence ( filter_image (( ProjMap1 (f,z)),cF2)) is proper Filter of ( BoolePoset ( [#] Y)) by Th17;

        

         A8: (( ProjMap1 (f,z)) " ( Int U)) is Subset of X2

        proof

          ( dom ( ProjMap1 (f,z))) = X2 by FUNCT_2:def 1;

          hence thesis by RELAT_1: 132;

        end;

        

         A9: for z be Element of B1 holds (( ProjMap1 (f,z)) .: B2) c= ( Int U)

        proof

          let z be Element of B1;

          let t be object;

          assume t in (( ProjMap1 (f,z)) .: B2);

          then

          consider u be object such that u in ( dom ( ProjMap1 (f,z))) and

           A10: u in B2 and

           A11: t = (( ProjMap1 (f,z)) . u) by FUNCT_1:def 6;

          (( ProjMap1 (f,z)) . u) = (f . (z,u)) by A10, MESFUNC9:def 6;

          then

           A12: t = (f . [z, u]) by A11, BINOP_1:def 1;

          now

             [z, u] in [:X1, X2:] by A10, ZFMISC_1:def 2;

            hence [z, u] in ( dom f) by FUNCT_2:def 1;

            z in {z} & u in B2 by TARSKI:def 1, A10;

            hence [z, u] in [: {z}, B2:] by ZFMISC_1:def 2;

          end;

          then

           A13: t in (f .: [: {z}, B2:]) by A12, FUNCT_1:def 6;

          (f .: [: {z}, B2:]) c= ( Int U) by A5;

          hence thesis by A13;

        end;

        thus ( Int U) in ( filter_image (( ProjMap1 (f,z)),cF2)) & y is_a_cluster_point_of (( filter_image (( ProjMap1 (f,z)),cF2)),Y)

        proof

          (( ProjMap1 (f,z)) .: B2) c= ( Int U) by A9;

          then B2 c= (( ProjMap1 (f,z)) " ( Int U)) by FUNCT_2: 95;

          then (( ProjMap1 (f,z)) " ( Int U)) in cF2 by A3, A8, CARDFIL2:def 8;

          hence ( Int U) in ( filter_image (( ProjMap1 (f,z)),cF2));

          thus thesis by A7, Th19;

        end;

      end;

      for z be Element of B1, y be Element of Y st y in ( lim_filter (( ProjMap1 (f,z)),cF2)) holds y in ( Cl ( Int U))

      proof

        let z be Element of B1, y be Element of Y;

        assume y in ( lim_filter (( ProjMap1 (f,z)),cF2));

        then ( filter_image (( ProjMap1 (f,z)),cF2)) is proper Filter of ( BoolePoset ( [#] Y)) & ( Int U) in ( filter_image (( ProjMap1 (f,z)),cF2)) & y is_a_cluster_point_of (( filter_image (( ProjMap1 (f,z)),cF2)),Y) by A6;

        hence thesis by YELLOW19: 25;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL4:98

    

     Th77: x in ( lim_filter (f, <.cF1, cF2.))) & <.cB1.) = cF1 & <.cB2.) = cF2 implies for U be a_neighborhood of x st U is closed holds ex B1 be Element of cB1, B2 be Element of cB2 st for z be Element of X2, y be Element of Y st z in B2 & y in ( lim_filter (( ProjMap2 (f,z)),cF1)) holds y in ( Cl ( Int U))

    proof

      assume that

       A1: x in ( lim_filter (f, <.cF1, cF2.))) and

       A2: <.cB1.) = cF1 and

       A3: <.cB2.) = cF2;

      let U be a_neighborhood of x;

      assume U is closed;

      then

      consider B1 be Element of cB1, B2 be Element of cB2 such that

       A4: (f .: [:B1, B2:]) c= ( Int U) by A1, A2, A3, Th75;

      take B1, B2;

      

       A5: for y be Element of B2 holds (f .: [:B1, {y}:]) c= ( Int U)

      proof

        let y be Element of B2;

         [:B1, {y}:] c= [:B1, B2:] by ZFMISC_1: 95;

        then (f .: [:B1, {y}:]) c= (f .: [:B1, B2:]) by RELAT_1: 125;

        hence thesis by A4;

      end;

      

       A6: for z be Element of B2, y be Element of Y st y in ( lim_filter (( ProjMap2 (f,z)),cF1)) holds ( filter_image (( ProjMap2 (f,z)),cF1)) is proper Filter of ( BoolePoset ( [#] Y)) & ( Int U) in ( filter_image (( ProjMap2 (f,z)),cF1)) & y is_a_cluster_point_of (( filter_image (( ProjMap2 (f,z)),cF1)),Y)

      proof

        let z be Element of B2, y be Element of Y;

        assume

         A7: y in ( lim_filter (( ProjMap2 (f,z)),cF1));

        ( filter_image (( ProjMap2 (f,z)),cF1)) is Filter of ( [#] Y) by STRUCT_0:def 3;

        hence ( filter_image (( ProjMap2 (f,z)),cF1)) is proper Filter of ( BoolePoset ( [#] Y)) by Th17;

        

         A8: (( ProjMap2 (f,z)) " ( Int U)) is Subset of X1

        proof

          ( dom ( ProjMap2 (f,z))) = X1 by FUNCT_2:def 1;

          hence thesis by RELAT_1: 132;

        end;

        

         A9: for z be Element of B2 holds (( ProjMap2 (f,z)) .: B1) c= ( Int U)

        proof

          let z be Element of B2;

          let t be object;

          assume t in (( ProjMap2 (f,z)) .: B1);

          then

          consider u be object such that u in ( dom ( ProjMap2 (f,z))) and

           A10: u in B1 and

           A11: t = (( ProjMap2 (f,z)) . u) by FUNCT_1:def 6;

          (( ProjMap2 (f,z)) . u) = (f . (u,z)) by A10, MESFUNC9:def 7;

          then

           A12: t = (f . [u, z]) by A11, BINOP_1:def 1;

          now

             [u, z] in [:X1, X2:] by A10, ZFMISC_1:def 2;

            hence [u, z] in ( dom f) by FUNCT_2:def 1;

            z in {z} & u in B1 by TARSKI:def 1, A10;

            hence [u, z] in [:B1, {z}:] by ZFMISC_1:def 2;

          end;

          then

           VALB: t in (f .: [:B1, {z}:]) by A12, FUNCT_1:def 6;

          (f .: [:B1, {z}:]) c= ( Int U) by A5;

          hence thesis by VALB;

        end;

        thus ( Int U) in ( filter_image (( ProjMap2 (f,z)),cF1)) & y is_a_cluster_point_of (( filter_image (( ProjMap2 (f,z)),cF1)),Y)

        proof

          (( ProjMap2 (f,z)) .: B1) c= ( Int U) by A9;

          then B1 c= (( ProjMap2 (f,z)) " ( Int U)) by FUNCT_2: 95;

          then (( ProjMap2 (f,z)) " ( Int U)) in cF1 by A2, A8, CARDFIL2:def 8;

          hence ( Int U) in ( filter_image (( ProjMap2 (f,z)),cF1));

          thus thesis by A7, Th19;

        end;

      end;

      for z be Element of B2, y be Element of Y st y in ( lim_filter (( ProjMap2 (f,z)),cF1)) holds y in ( Cl ( Int U))

      proof

        let z be Element of B2, y be Element of Y;

        assume y in ( lim_filter (( ProjMap2 (f,z)),cF1));

        then ( filter_image (( ProjMap2 (f,z)),cF1)) is proper Filter of ( BoolePoset ( [#] Y)) & ( Int U) in ( filter_image (( ProjMap2 (f,z)),cF1)) & y is_a_cluster_point_of (( filter_image (( ProjMap2 (f,z)),cF1)),Y) by A6;

        hence thesis by YELLOW19: 25;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL4:99

    

     Th78: for Y be Hausdorff regular non empty TopSpace, f be Function of [:X1, X2:], Y st (for x be Element of X2 holds ( lim_filter (( ProjMap2 (f,x)),cF1)) <> {} ) holds ( lim_filter (f, <.cF1, cF2.))) c= ( lim_filter (( lim_in_cod1 (f,cF1)),cF2))

    proof

      let Y be Hausdorff regular non empty TopSpace, f be Function of [:X1, X2:], Y;

      assume

       A1: for x1 be Element of X2 holds ( lim_filter (( ProjMap2 (f,x1)),cF1)) <> {} ;

      now

        let y0 be object;

        assume

         A2: y0 in ( lim_filter (f, <.cF1, cF2.)));

        then

        reconsider y = y0 as Element of Y;

        consider cB1 be filter_base of X1 such that cB1 = cF1 and

         A3: <.cB1.) = cF1 by Th18;

        consider cB2 be filter_base of X2 such that cB2 = cF2 and

         A4: <.cB2.) = cF2 by Th18;

        

         A5: for U be a_neighborhood of y st U is closed holds ex B1 be Element of cB1, B2 be Element of cB2 st for z be Element of B2 holds ( lim_filter (( ProjMap2 (f,z)),cF1)) c= ( Cl ( Int U))

        proof

          let U be a_neighborhood of y;

          assume U is closed;

          then

          consider B1 be Element of cB1, B2 be Element of cB2 such that

           A6: for z be Element of X2, t be Element of Y st z in B2 & t in ( lim_filter (( ProjMap2 (f,z)),cF1)) holds t in ( Cl ( Int U)) by A3, A4, A2, Th77;

          take B1, B2;

          thus thesis by A6;

        end;

        ( NeighborhoodSystem y) c= ( filter_image (( lim_in_cod1 (f,cF1)),cF2))

        proof

          let n be object;

          assume n in ( NeighborhoodSystem y);

          then n in the set of all A where A be a_neighborhood of y by YELLOW19:def 1;

          then

          consider A be a_neighborhood of y such that

           A7: n = A;

          y in ( Int A) by CONNSP_2:def 1;

          then

          consider Q be Subset of Y such that

           A8: Q is closed and

           A9: Q c= A and

           A10: y in ( Int Q) by YELLOW_8: 27;

          Q is a_neighborhood of y by A10, CONNSP_2:def 1;

          then

          consider B1 be Element of cB1, B2 be Element of cB2 such that

           A11: for z be Element of B2 holds ( lim_filter (( ProjMap2 (f,z)),cF1)) c= ( Cl ( Int Q)) by A8, A5;

          

           A12: ( Cl Q) = Q by PRE_TOPC: 18, A8, TOPS_1: 5;

          

           A13: ( Cl ( Int Q)) c= ( Cl Q) by TOPS_1: 16, PRE_TOPC: 19;

          reconsider n1 = n as Subset of Y by A7;

          now

            (( lim_in_cod1 (f,cF1)) .: B2) c= n1

            proof

              let t be object;

              assume t in (( lim_in_cod1 (f,cF1)) .: B2);

              then

              consider u be object such that

               A14: u in ( dom ( lim_in_cod1 (f,cF1))) and

               A15: u in B2 and

               A16: t = (( lim_in_cod1 (f,cF1)) . u) by FUNCT_1:def 6;

              reconsider u1 = u as Element of X2 by A14;

               {t} = ( lim_filter (( ProjMap2 (f,u1)),cF1)) by A16, A1, Def6;

              then

               A17: t in ( lim_filter (( ProjMap2 (f,u1)),cF1)) by TARSKI:def 1;

              ( lim_filter (( ProjMap2 (f,u1)),cF1)) c= ( Cl ( Int Q)) by A11, A15;

              hence thesis by A7, A17, A13, A12, A9;

            end;

            hence B2 c= (( lim_in_cod1 (f,cF1)) " n1) by FUNCT_2: 95;

            ( dom ( lim_in_cod1 (f,cF1))) = X2 by FUNCT_2:def 1;

            hence (( lim_in_cod1 (f,cF1)) " n1) is Subset of X2 by RELAT_1: 132;

          end;

          then (( lim_in_cod1 (f,cF1)) " n1) in cF2 by A4, CARDFIL2:def 8;

          hence thesis;

        end;

        then ( filter_image (( lim_in_cod1 (f,cF1)),cF2)) is_filter-finer_than ( NeighborhoodSystem y);

        hence y0 in ( lim_filter (( lim_in_cod1 (f,cF1)),cF2));

      end;

      hence thesis;

    end;

    theorem :: CARDFIL4:100

    

     Th79: for Y be Hausdorff regular non empty TopSpace, f be Function of [:X1, X2:], Y st (for x be Element of X1 holds ( lim_filter (( ProjMap1 (f,x)),cF2)) <> {} ) holds ( lim_filter (f, <.cF1, cF2.))) c= ( lim_filter (( lim_in_cod2 (f,cF2)),cF1))

    proof

      let Y be Hausdorff regular non empty TopSpace, f be Function of [:X1, X2:], Y;

      assume

       A1: for x1 be Element of X1 holds ( lim_filter (( ProjMap1 (f,x1)),cF2)) <> {} ;

      now

        let y0 be object;

        assume

         A2: y0 in ( lim_filter (f, <.cF1, cF2.)));

        then

        reconsider y = y0 as Element of Y;

        consider cB1 be filter_base of X1 such that cB1 = cF1 and

         A3: <.cB1.) = cF1 by Th18;

        consider cB2 be filter_base of X2 such that cB2 = cF2 and

         A4: <.cB2.) = cF2 by Th18;

        

         A5: for U be a_neighborhood of y st U is closed holds ex B1 be Element of cB1, B2 be Element of cB2 st for z be Element of B1 holds ( lim_filter (( ProjMap1 (f,z)),cF2)) c= ( Cl ( Int U))

        proof

          let U be a_neighborhood of y;

          assume U is closed;

          then

          consider B1 be Element of cB1, B2 be Element of cB2 such that

           A6: for z be Element of X1, t be Element of Y st z in B1 & t in ( lim_filter (( ProjMap1 (f,z)),cF2)) holds t in ( Cl ( Int U)) by A3, A4, A2, Th76;

          take B1, B2;

          thus thesis by A6;

        end;

        ( NeighborhoodSystem y) c= ( filter_image (( lim_in_cod2 (f,cF2)),cF1))

        proof

          let n be object;

          assume n in ( NeighborhoodSystem y);

          then n in the set of all A where A be a_neighborhood of y by YELLOW19:def 1;

          then

          consider A be a_neighborhood of y such that

           A7: n = A;

          y in ( Int A) by CONNSP_2:def 1;

          then

          consider Q be Subset of Y such that

           A8: Q is closed and

           A9: Q c= A and

           A10: y in ( Int Q) by YELLOW_8: 27;

          Q is a_neighborhood of y by A10, CONNSP_2:def 1;

          then

          consider B1 be Element of cB1, B2 be Element of cB2 such that

           A11: for z be Element of B1 holds ( lim_filter (( ProjMap1 (f,z)),cF2)) c= ( Cl ( Int Q)) by A8, A5;

          

           A12: ( Cl Q) = Q by PRE_TOPC: 18, A8, TOPS_1: 5;

          

           A13: ( Cl ( Int Q)) c= ( Cl Q) by TOPS_1: 16, PRE_TOPC: 19;

          reconsider n1 = n as Subset of Y by A7;

          now

            (( lim_in_cod2 (f,cF2)) .: B1) c= n1

            proof

              let t be object;

              assume t in (( lim_in_cod2 (f,cF2)) .: B1);

              then

              consider u be object such that

               A14: u in ( dom ( lim_in_cod2 (f,cF2))) and

               A15: u in B1 and

               A16: t = (( lim_in_cod2 (f,cF2)) . u) by FUNCT_1:def 6;

              reconsider u1 = u as Element of X1 by A14;

               {t} = ( lim_filter (( ProjMap1 (f,u1)),cF2)) by A16, A1, Def7;

              then

               A17: t in ( lim_filter (( ProjMap1 (f,u1)),cF2)) by TARSKI:def 1;

              ( lim_filter (( ProjMap1 (f,u1)),cF2)) c= ( Cl ( Int Q)) by A11, A15;

              hence thesis by A7, A17, A13, A12, A9;

            end;

            hence B1 c= (( lim_in_cod2 (f,cF2)) " n1) by FUNCT_2: 95;

            ( dom ( lim_in_cod2 (f,cF2))) = X1 by FUNCT_2:def 1;

            hence (( lim_in_cod2 (f,cF2)) " n1) is Subset of X1 by RELAT_1: 132;

          end;

          then (( lim_in_cod2 (f,cF2)) " n1) in cF1 by A3, CARDFIL2:def 8;

          hence thesis;

        end;

        then ( filter_image (( lim_in_cod2 (f,cF2)),cF1)) is_filter-finer_than ( NeighborhoodSystem y);

        hence y0 in ( lim_filter (( lim_in_cod2 (f,cF2)),cF1));

      end;

      hence thesis;

    end;

    theorem :: CARDFIL4:101

    

     Th80: for X1,X2 be non empty set, cF1 be Filter of X1, cF2 be Filter of X2, Y be Hausdorff regular non empty TopSpace, f be Function of [:X1, X2:], Y st ( lim_filter (f, <.cF1, cF2.))) <> {} & (for x be Element of X1 holds ( lim_filter (( ProjMap1 (f,x)),cF2)) <> {} ) holds ( lim_filter (f, <.cF1, cF2.))) = ( lim_filter (( lim_in_cod2 (f,cF2)),cF1))

    proof

      let X1,X2 be non empty set, cF1 be Filter of X1, cF2 be Filter of X2, Y be Hausdorff regular non empty TopSpace, f be Function of [:X1, X2:], Y;

      assume that

       A1: ( lim_filter (f, <.cF1, cF2.))) <> {} and

       A2: for x be Element of X1 holds ( lim_filter (( ProjMap1 (f,x)),cF2)) <> {} ;

      consider y be object such that

       A3: ( lim_filter (f, <.cF1, cF2.))) = {y} by A1, ZFMISC_1: 131;

      

       A4: y in ( lim_filter (f, <.cF1, cF2.))) by A3, TARSKI:def 1;

      

       A5: ( lim_filter (f, <.cF1, cF2.))) c= ( lim_filter (( lim_in_cod2 (f,cF2)),cF1)) by A2, Th79;

      ( lim_filter (( lim_in_cod2 (f,cF2)),cF1)) is non empty trivial by A3, A5;

      then ex z be object st ( lim_filter (( lim_in_cod2 (f,cF2)),cF1)) = {z} by ZFMISC_1: 131;

      hence thesis by A3, A5, A4, TARSKI:def 1;

    end;

    theorem :: CARDFIL4:102

    

     Th81: for X1,X2 be non empty set, cF1 be Filter of X1, cF2 be Filter of X2, Y be Hausdorff regular non empty TopSpace, f be Function of [:X1, X2:], Y st ( lim_filter (f, <.cF1, cF2.))) <> {} & (for x be Element of X2 holds ( lim_filter (( ProjMap2 (f,x)),cF1)) <> {} ) holds ( lim_filter (f, <.cF1, cF2.))) = ( lim_filter (( lim_in_cod1 (f,cF1)),cF2))

    proof

      let X1,X2 be non empty set, cF1 be Filter of X1, cF2 be Filter of X2, Y be Hausdorff regular non empty TopSpace, f be Function of [:X1, X2:], Y;

      assume that

       A1: ( lim_filter (f, <.cF1, cF2.))) <> {} and

       A2: for x be Element of X2 holds ( lim_filter (( ProjMap2 (f,x)),cF1)) <> {} ;

      consider y be object such that

       A3: ( lim_filter (f, <.cF1, cF2.))) = {y} by A1, ZFMISC_1: 131;

      

       A4: ( lim_filter (f, <.cF1, cF2.))) c= ( lim_filter (( lim_in_cod1 (f,cF1)),cF2)) by A2, Th78;

      

       A5: y in ( lim_filter (f, <.cF1, cF2.))) by A3, TARSKI:def 1;

      ( lim_filter (( lim_in_cod1 (f,cF1)),cF2)) is non empty trivial by A4, A3;

      then ex z be object st ( lim_filter (( lim_in_cod1 (f,cF1)),cF2)) = {z} by ZFMISC_1: 131;

      hence thesis by A3, A5, A4, TARSKI:def 1;

    end;

    theorem :: CARDFIL4:103

    for X1,X2 be non empty set, cF1 be Filter of X1, cF2 be Filter of X2, Y be Hausdorff regular non empty TopSpace, f be Function of [:X1, X2:], Y st ( lim_filter (f, <.cF1, cF2.))) <> {} & (for x be Element of X1 holds ( lim_filter (( ProjMap1 (f,x)),cF2)) <> {} ) & (for x be Element of X2 holds ( lim_filter (( ProjMap2 (f,x)),cF1)) <> {} ) holds ( lim_filter (( lim_in_cod2 (f,cF2)),cF1)) = ( lim_filter (( lim_in_cod1 (f,cF1)),cF2))

    proof

      let X1,X2 be non empty set, cF1 be Filter of X1, cF2 be Filter of X2, Y be Hausdorff regular non empty TopSpace, f be Function of [:X1, X2:], Y;

      assume that

       A1: ( lim_filter (f, <.cF1, cF2.))) <> {} and

       A2: (for x be Element of X1 holds ( lim_filter (( ProjMap1 (f,x)),cF2)) <> {} ) and

       A3: (for x be Element of X2 holds ( lim_filter (( ProjMap2 (f,x)),cF1)) <> {} );

      ( lim_filter (f, <.cF1, cF2.))) = ( lim_filter (( lim_in_cod1 (f,cF1)),cF2)) by A1, A3, Th81;

      hence thesis by A1, A2, Th80;

    end;