cardfil3.miz



    begin

    theorem :: CARDFIL3:1

    for I be set holds {} is Element of ( Fin I)

    proof

      let I be set;

      

       A1: ( Fin {} ) c= ( Fin I) by XBOOLE_1: 2, FINSUB_1: 10;

       {} in { {} } by TARSKI:def 1;

      hence thesis by A1, FINSUB_1: 15;

    end;

    theorem :: CARDFIL3:2

    

     Th1: for I,J be set st J in ( Fin I) holds ex p be FinSequence of I st J = ( rng p) & p is one-to-one

    proof

      let I,J be set such that

       A1: J in ( Fin I);

      consider p be FinSequence such that

       A2: J = ( rng p) & p is one-to-one by A1, FINSEQ_4: 58;

      ( rng p) c= I by A1, A2, FINSUB_1:def 5;

      then

      reconsider p as FinSequence of I by FINSEQ_1:def 4;

      take p;

      thus thesis by A2;

    end;

    theorem :: CARDFIL3:3

    

     Th2: for I be set, Y be non empty set, x be Y -valued ManySortedSet of I, p be FinSequence of I holds (p * x) is FinSequence of Y

    proof

      let I be set, Y be non empty set, x be Y -valued ManySortedSet of I, p be FinSequence of I;

      

       A1: ( dom x) = I by PARTFUN1:def 2;

      

       A2: ( rng x) c= Y by RELAT_1:def 19;

      then

       A3: x is Function of I, Y by A1, FUNCT_2: 2;

      reconsider x1 = x as Function of I, Y by A1, A2, FUNCT_2: 2;

      reconsider xp = (p * x1) as FinSequence;

      thus thesis by A3, FINSEQ_2: 32;

    end;

    theorem :: CARDFIL3:4

    

     Th3: for I,X be non empty set, x be X -valued ManySortedSet of I, p,q be FinSequence of I holds ((p ^ q) * x) = ((p * x) ^ (q * x))

    proof

      let I,X be non empty set, x be X -valued ManySortedSet of I, p,q be FinSequence of I;

      

       A1: ( dom x) = I by PARTFUN1:def 2;

      ( rng x) c= X by RELAT_1:def 19;

      then

       A2: x is Function of I, X by A1, FUNCT_2: 2;

      then

       A3: ( dom (p * x)) = ( dom p) & ( dom (q * x)) = ( dom q) & ( dom ((p ^ q) * x)) = ( dom (p ^ q)) by FINSEQ_3: 120;

      

       A4: ( dom (p ^ q)) = ( Seg (( len p) + ( len q))) by FINSEQ_1:def 7;

      

       A5: ( Seg ( len (p * x))) = ( dom p) & ( Seg ( len (q * x))) = ( dom q) by A3, FINSEQ_1:def 3;

      

       A6: ( len (p * x)) = ( len p) & ( len (q * x)) = ( len q) by A5, FINSEQ_1:def 3;

      then

       A7: ( dom ((p * x) ^ (q * x))) = ( Seg (( len p) + ( len q))) by FINSEQ_1:def 7;

      for t be object st t in ( dom ((p ^ q) * x)) holds (((p ^ q) * x) . t) = (((p * x) ^ (q * x)) . t)

      proof

        let t be object;

        assume

         A8: t in ( dom ((p ^ q) * x));

        

         A9: t in ( dom (p ^ q)) by A2, FINSEQ_3: 120, A8;

        

         A10: (((p ^ q) * x) . t) = (x . ((p ^ q) . t)) by A2, FINSEQ_3: 120, A8;

        now

          hereby

            assume

             A11: t in ( dom p);

            then

             A12: (x . ((p ^ q) . t)) = (x . (p . t)) & (x . (p . t)) = ((p * x) . t) by FINSEQ_1:def 7, FUNCT_1: 13;

            t in ( dom (p * x)) by A11, A2, FINSEQ_3: 120;

            hence (((p ^ q) * x) . t) = (((p * x) ^ (q * x)) . t) by A12, A10, FINSEQ_1:def 7;

          end;

          assume ex n be Nat st n in ( dom q) & t = (( len p) + n);

          then

          consider n be Nat such that

           A13: n in ( dom q) and

           A14: t = (( len p) + n);

          

           A15: (x . ((p ^ q) . (( len p) + n))) = (x . (q . n)) by A13, FINSEQ_1:def 7;

          n in ( dom (q * x)) by A13, A2, FINSEQ_3: 120;

          then (((p * x) ^ (q * x)) . (( len p) + n)) = ((q * x) . n) by A6, FINSEQ_1:def 7;

          hence (((p ^ q) * x) . t) = (((p * x) ^ (q * x)) . t) by A13, A14, A15, A10, FUNCT_1: 13;

        end;

        hence thesis by A9, FINSEQ_1: 25;

      end;

      hence thesis by A7, A2, FINSEQ_3: 120, A4;

    end;

    definition

      let I be set, Y be non empty set, x be Y -valued ManySortedSet of I, p be FinSequence of I;

      :: CARDFIL3:def1

      func # (p,x) -> FinSequence of Y equals (p * x);

      coherence by Th2;

    end

    definition

      let I be set;

      :: CARDFIL3:def2

      func OrderedFIN I -> non empty transitive reflexive RelStr equals ( InclPoset ( Fin I));

      coherence ;

    end

    theorem :: CARDFIL3:5

    

     Th4: for I be set holds ( [#] ( OrderedFIN I)) is directed

    proof

      let I be set;

      

       A1: the carrier of ( OrderedFIN I) = ( Fin I) by YELLOW_1: 1;

      then

       A2: ( [#] ( OrderedFIN I)) = ( Fin I) by STRUCT_0:def 3;

      now

        let a,b be Element of ( OrderedFIN I);

        assume that a in ( [#] ( OrderedFIN I)) and b in ( [#] ( OrderedFIN I));

        reconsider z = (a \/ b) as Element of ( OrderedFIN I) by A1, FINSUB_1:def 1;

        take z;

        thus z in ( [#] ( OrderedFIN I)) & a <= z & b <= z by A1, A2, YELLOW_1: 3, XBOOLE_1: 7;

      end;

      hence thesis by WAYBEL_0:def 1;

    end;

    begin

    theorem :: CARDFIL3:6

    

     Th5: for M be non empty MetrSpace, x be Point of ( TopSpaceMetr M) holds ( Balls x) is basis of ( BOOL2F ( NeighborhoodSystem x))

    proof

      let M be non empty MetrSpace, x be Point of ( TopSpaceMetr M);

      set F = ( BOOL2F ( NeighborhoodSystem x));

      now

        let t be object;

        assume

         A1: t in ( Balls x);

        then

        reconsider t1 = t as Subset of ( TopSpaceMetr M);

        consider y be Point of M such that

         A2: y = x and

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

        consider n0 be Nat such that

         A4: t = ( Ball (y,(1 / n0))) and

         A5: n0 <> 0 by A1, A3;

        reconsider r0 = (1 / n0) as Real;

        

         A6: 0 < r0 by A5;

        ( dist (y,y)) < r0 by A6, METRIC_1: 1;

        then

         A7: y in { q where q be Element of M : ( dist (y,q)) < r0 };

        t1 is open & x in t1 by A7, A4, TOPMETR: 14, A2, METRIC_1:def 14;

        then t1 is a_neighborhood of x by CONNSP_2: 3;

        then t in ( NeighborhoodSystem x) by YELLOW19: 2;

        hence t in F by CARDFIL2:def 20;

      end;

      then ( Balls x) c= F;

      then

      reconsider BAX = ( Balls x) as non empty Subset of F;

      now

        let f be Element of F;

        f in ( BOOL2F ( NeighborhoodSystem x));

        then f in ( NeighborhoodSystem x) by CARDFIL2:def 20;

        then f is a_neighborhood of x by YELLOW19: 2;

        then

        consider V be Subset of ( TopSpaceMetr M) such that

         A8: V is open & V c= f & x in V by CONNSP_2: 6;

        consider b be Subset of ( TopSpaceMetr M) such that

         A9: b in ( Balls x) & b c= V by A8, YELLOW_8:def 1;

        reconsider b as Element of BAX by A9;

        take b;

        thus b c= f by A8, A9;

      end;

      then BAX is filter_basis;

      hence thesis;

    end;

    theorem :: CARDFIL3:7

    for M be non empty MetrSpace, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), the carrier of ( TopSpaceMetr M), x be Point of ( TopSpaceMetr M), B be basis of ( BOOL2F ( NeighborhoodSystem x)) st ( [#] L) is directed holds x in ( lim_f f) iff for b be Element of B holds ex i be Element of L st for j be Element of L st i <= j holds (f . j) in b by CARDFIL2: 84;

    theorem :: CARDFIL3:8

    for M be non empty MetrSpace, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), the carrier of ( TopSpaceMetr M), x be Point of ( TopSpaceMetr M) st ( [#] L) is directed holds x in ( lim_f f) iff for b be Element of ( Balls x) holds ex n be Element of L st for m be Element of L st n <= m holds (f . m) in b

    proof

      let M be non empty MetrSpace, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), the carrier of ( TopSpaceMetr M), x be Point of ( TopSpaceMetr M);

      assume

       A1: ( [#] L) is directed;

      ( Balls x) is basis of ( BOOL2F ( NeighborhoodSystem x)) by Th5;

      hence thesis by A1, CARDFIL2: 84;

    end;

    theorem :: CARDFIL3:9

    

     Th6: for M be non empty MetrSpace, s be sequence of the carrier of ( TopSpaceMetr M), x be Point of ( TopSpaceMetr M) holds x in ( lim_f s) iff for b be Element of ( Balls x) holds ex i be Nat st for j be Nat st i <= j holds (s . j) in b

    proof

      let M be non empty MetrSpace, s be sequence of the carrier of ( TopSpaceMetr M), x be Point of ( TopSpaceMetr M);

      ( Balls x) is basis of ( BOOL2F ( NeighborhoodSystem x)) by Th5;

      hence thesis by CARDFIL2: 97;

    end;

    theorem :: CARDFIL3:10

    

     Th7: for T be non empty TopStruct, s be sequence of T, x be Point of T holds x in ( Lim s) iff for U1 be Subset of T st U1 is open & x in U1 holds ex n be Nat st for m be Nat st n <= m holds (s . m) in U1

    proof

      let T be non empty TopStruct, s be sequence of T, x be Point of T;

      x in ( Lim s) iff s is_convergent_to x by FRECHET:def 5;

      hence thesis;

    end;

    theorem :: CARDFIL3:11

    

     Th8: for M be non empty MetrSpace, s be sequence of the carrier of ( TopSpaceMetr M), x be Point of ( TopSpaceMetr M) holds x in ( Lim s) iff for b be Element of ( Balls x) holds ex n be Nat st for m be Nat st n <= m holds (s . m) in b

    proof

      let M be non empty MetrSpace, s be sequence of the carrier of ( TopSpaceMetr M), x be Point of ( TopSpaceMetr M);

      now

        hereby

          assume

           A1: x in ( Lim s);

          now

            let b be Element of ( Balls x);

            ( Balls x) is basis of ( BOOL2F ( NeighborhoodSystem x)) by Th5;

            then ( Balls x) c= ( BOOL2F ( NeighborhoodSystem x));

            then b in ( BOOL2F ( NeighborhoodSystem x));

            then b in ( NeighborhoodSystem x) by CARDFIL2:def 20;

            then b is a_neighborhood of x by YELLOW19: 2;

            then

            consider V be Subset of ( TopSpaceMetr M) such that

             A2: V is open and

             A3: V c= b and

             A4: x in V by CONNSP_2: 6;

            consider n0 be Nat such that

             A5: for m be Nat st n0 <= m holds (s . m) in V by A2, A4, A1, Th7;

            take n0;

            thus for m be Nat st n0 <= m holds (s . m) in b by A3, A5;

          end;

          hence x in ( Lim s) implies for b be Element of ( Balls x) holds ex n be Nat st for m be Nat st n <= m holds (s . m) in b;

        end;

        assume

         A6: for b be Element of ( Balls x) holds ex n be Nat st for m be Nat st n <= m holds (s . m) in b;

        now

          let U1 be Subset of ( TopSpaceMetr M);

          assume U1 is open & x in U1;

          then U1 is a_neighborhood of x by CONNSP_2: 6;

          then U1 in ( NeighborhoodSystem x) by YELLOW19: 2;

          then

           A7: U1 is Element of ( BOOL2F ( NeighborhoodSystem x)) by CARDFIL2:def 20;

          reconsider BAX = ( Balls x) as non empty Subset of ( BOOL2F ( NeighborhoodSystem x)) by Th5;

          BAX is filter_basis by Th5;

          then

          consider b be Element of ( Balls x) such that

           A8: b c= U1 by A7;

          consider n0 be Nat such that

           A9: for m be Nat st n0 <= m holds (s . m) in b by A6;

          take n0;

          thus for m be Nat st n0 <= m holds (s . m) in U1 by A9, A8;

        end;

        hence x in ( Lim s) by Th7;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL3:12

    for M be non empty MetrSpace, s be sequence of the carrier of ( TopSpaceMetr M), x be Point of ( TopSpaceMetr M) holds x in ( lim_f s) iff x in ( Lim s)

    proof

      let M be non empty MetrSpace, s be sequence of the carrier of ( TopSpaceMetr M), x be Point of ( TopSpaceMetr M);

      hereby

        assume x in ( lim_f s);

        then for b be Element of ( Balls x) holds ex i be Nat st for j be Nat st i <= j holds (s . j) in b by Th6;

        hence x in ( Lim s) by Th8;

      end;

      assume x in ( Lim s);

      then for b be Element of ( Balls x) holds ex i be Nat st for j be Nat st i <= j holds (s . j) in b by Th8;

      hence x in ( lim_f s) by Th6;

    end;

    begin

    theorem :: CARDFIL3:13

    for N be RealNormSpace, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), the carrier of ( TopSpaceMetr ( MetricSpaceNorm N)), x be Point of ( TopSpaceMetr ( MetricSpaceNorm N)), B be basis of ( BOOL2F ( NeighborhoodSystem x)) st ( [#] L) is directed holds x in ( lim_f f) iff for b be Element of B holds ex i be Element of L st for j be Element of L st i <= j holds (f . j) in b by CARDFIL2: 84;

    theorem :: CARDFIL3:14

    for N be RealNormSpace, x be Point of ( TopSpaceMetr ( MetricSpaceNorm N)) holds ( Balls x) is basis of ( BOOL2F ( NeighborhoodSystem x)) by Th5;

    theorem :: CARDFIL3:15

    for N be RealNormSpace, s be sequence of the carrier of ( TopSpaceMetr ( MetricSpaceNorm N)), x be Point of ( TopSpaceMetr ( MetricSpaceNorm N)) holds x in ( lim_f s) iff for b be Element of ( Balls x) holds ex i be Nat st for j be Nat st i <= j holds (s . j) in b by Th6;

    theorem :: CARDFIL3:16

    for N be RealNormSpace, x be Point of ( TopSpaceMetr ( MetricSpaceNorm N)) holds ex y be Point of ( MetricSpaceNorm N) st y = x & ( Balls x) = { ( Ball (y,(1 / n))) where n be Nat : n <> 0 } by FRECHET:def 1;

    theorem :: CARDFIL3:17

    for N be RealNormSpace, x be Point of ( TopSpaceMetr ( MetricSpaceNorm N)), y be Point of ( MetricSpaceNorm N), n be positive Nat st x = y holds ( Ball (y,(1 / n))) in ( Balls x)

    proof

      let N be RealNormSpace, x be Point of ( TopSpaceMetr ( MetricSpaceNorm N)), y be Point of ( MetricSpaceNorm N), n be positive Nat such that

       A1: x = y;

      set M = ( MetricSpaceNorm N);

      consider y1 be Point of M such that

       A2: y1 = x and

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

      thus thesis by A1, A2, A3;

    end;

    theorem :: CARDFIL3:18

    for N be RealNormSpace, x be Point of ( MetricSpaceNorm N), n be Nat st n <> 0 holds ( Ball (x,(1 / n))) = { q where q be Element of ( MetricSpaceNorm N) : ( dist (x,q)) < (1 / n) } by METRIC_1:def 14;

    theorem :: CARDFIL3:19

    for N be RealNormSpace, x be Element of ( MetricSpaceNorm N), n be Nat st n <> 0 holds ex y be Point of N st x = y & ( Ball (x,(1 / n))) = { q where q be Point of N : ||.(y - q).|| < (1 / n) } by NORMSP_2: 2;

    theorem :: CARDFIL3:20

    for PM be MetrStruct holds ( TopSpaceMetr PM) = TopStruct (# the carrier of PM, ( Family_open_set PM) #) by PCOMPS_1:def 5;

    theorem :: CARDFIL3:21

    for PM be MetrStruct holds the carrier of TopStruct (# the carrier of PM, ( Family_open_set PM) #) = the carrier of PM;

    theorem :: CARDFIL3:22

    for PM be MetrStruct holds the carrier of ( TopSpaceMetr PM) = the carrier of TopStruct (# the carrier of PM, ( Family_open_set PM) #) by PCOMPS_1:def 5;

    theorem :: CARDFIL3:23

    

     Th9: for PM be MetrStruct holds the carrier of ( TopSpaceMetr PM) = the carrier of PM

    proof

      let PM be MetrStruct;

      the carrier of ( TopSpaceMetr PM) = the carrier of TopStruct (# the carrier of PM, ( Family_open_set PM) #) by PCOMPS_1:def 5;

      hence thesis;

    end;

    theorem :: CARDFIL3:24

    for N be RealNormSpace, s be sequence of the carrier of ( TopSpaceMetr ( MetricSpaceNorm N)), j be Nat holds (s . j) is Element of the carrier of ( TopSpaceMetr ( MetricSpaceNorm N));

    definition

      let N be RealNormSpace, x be Point of ( TopSpaceMetr ( MetricSpaceNorm N));

      :: CARDFIL3:def3

      func # x -> Point of N equals x;

      coherence

      proof

        ( MetricSpaceNorm N) = MetrStruct (# the carrier of N, ( distance_by_norm_of N) #) by NORMSP_2:def 2;

        hence x is Element of N by Th9;

      end;

    end

    theorem :: CARDFIL3:25

    for N be RealNormSpace, s be sequence of the carrier of ( TopSpaceMetr ( MetricSpaceNorm N)), x be Point of ( TopSpaceMetr ( MetricSpaceNorm N)) holds x in ( lim_f s) iff (for n be positive Nat holds ex i be Nat st for j be Nat st i <= j holds ||.(( # x) - ( # (s . j))).|| < (1 / n))

    proof

      let N be RealNormSpace, s be sequence of the carrier of ( TopSpaceMetr ( MetricSpaceNorm N)), x be Point of ( TopSpaceMetr ( MetricSpaceNorm N));

      reconsider x1 = x as Point of ( TopSpaceMetr ( MetricSpaceNorm N));

      consider y0 be Point of ( MetricSpaceNorm N) such that

       A1: y0 = x1 and

       A2: ( Balls x1) = { ( Ball (y0,(1 / n))) where n be Nat : n <> 0 } by FRECHET:def 1;

      

       A3: x in ( lim_f s) implies (for n be positive Nat holds ex i be Nat st for j be Nat st i <= j holds ||.(( # x) - ( # (s . j))).|| < (1 / n))

      proof

        assume

         A4: x in ( lim_f s);

        now

          let n be positive Nat;

          ( Ball (y0,(1 / n))) in ( Balls x1) by A2;

          then

          consider i0 be Nat such that

           A5: for j be Nat st i0 <= j holds (s . j) in ( Ball (y0,(1 / n))) by A4, Th6;

           A6:

          now

            let j be Nat;

            assume

             A7: i0 <= j;

            consider y1 be Point of N such that

             A8: y0 = y1 and

             A9: ( Ball (y0,(1 / n))) = { q where q be Point of N : ||.(y1 - q).|| < (1 / n) } by NORMSP_2: 2;

            (s . j) in { q where q be Point of N : ||.(y1 - q).|| < (1 / n) } by A7, A5, A9;

            then

            consider q0 be Point of N such that

             A10: (s . j) = q0 and

             A11: ||.(y1 - q0).|| < (1 / n);

            thus ||.(( # x) - ( # (s . j))).|| < (1 / n) by A1, A8, A10, A11;

          end;

          take i0;

          thus for j be Nat st i0 <= j holds ||.(( # x) - ( # (s . j))).|| < (1 / n) by A6;

        end;

        hence thesis;

      end;

      (for n be positive Nat holds ex i be Nat st for j be Nat st i <= j holds ||.(( # x) - ( # (s . j))).|| < (1 / n)) implies x in ( lim_f s)

      proof

        assume

         A12: for n be positive Nat holds ex i be Nat st for j be Nat st i <= j holds ||.(( # x) - ( # (s . j))).|| < (1 / n);

        for b be Element of ( Balls x) holds ex i be Nat st for j be Nat st i <= j holds (s . j) in b

        proof

          let b be Element of ( Balls x);

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

          then

          consider n0 be Nat such that

           A13: b = ( Ball (y0,(1 / n0))) and

           A14: n0 <> 0 ;

          consider i0 be Nat such that

           A15: for j be Nat st i0 <= j holds ||.(( # x) - ( # (s . j))).|| < (1 / n0) by A12, A14;

          take i0;

          for j be Nat st i0 <= j holds (s . j) in b

          proof

            let j be Nat;

            assume i0 <= j;

            then

             A16: ||.(( # x1) - ( # (s . j))).|| < (1 / n0) by A15;

            consider y1 be Point of N such that

             A17: y0 = y1 and

             A18: ( Ball (y0,(1 / n0))) = { q where q be Point of N : ||.(y1 - q).|| < (1 / n0) } by NORMSP_2: 2;

            thus (s . j) in b by A1, A13, A16, A17, A18;

          end;

          hence thesis;

        end;

        hence thesis by Th6;

      end;

      hence thesis by A3;

    end;

    begin

    theorem :: CARDFIL3:26

    for X be non empty LinearTopSpace holds ( NeighborhoodSystem ( 0. X)) is local_base of X

    proof

      let X be non empty LinearTopSpace;

      reconsider p = ( 0. X) as Point of X;

      ( BOOL2F ( NeighborhoodSystem ( 0. X))) is Subset-Family of X;

      then

      reconsider NS0 = ( NeighborhoodSystem ( 0. X)) as Subset-Family of X by CARDFIL2:def 20;

      for A be a_neighborhood of p holds ex P be a_neighborhood of p st (P in ( NeighborhoodSystem p) & P c= A) by YELLOW19: 2;

      then NS0 is basis of p by YELLOW13:def 2;

      hence thesis;

    end;

    

     Lm1: for X be non empty addLoopStr, M be Subset of X holds for x,y be Point of X st y in M holds (x + y) in (x + M)

    proof

      let X be non empty addLoopStr, M be Subset of X;

      let x,y be Point of X;

      (x + M) = { (x + u) where u be Point of X : u in M } by RUSUB_4:def 8;

      hence thesis;

    end;

    

     Lm2: for X be non empty LinearTopSpace, x be Point of X, O be local_base of X holds { (x + U) where U be Subset of X : U in O & U is a_neighborhood of ( 0. X) } is non empty Subset-Family of X

    proof

      let X be non empty LinearTopSpace, x be Point of X, O be local_base of X;

      set B = { (x + U) where U be Subset of X : U in O & U is a_neighborhood of ( 0. X) };

      now

        let t be object;

        assume t in B;

        then

        consider U1 be Subset of X such that

         A1: t = (x + U1) and U1 in O and U1 is a_neighborhood of ( 0. X);

        thus t in ( bool the carrier of X) by A1;

      end;

      then B c= ( bool the carrier of X);

      then

      reconsider B1 = B as Subset-Family of X;

      

       A2: ( [#] X) is a_neighborhood of ( 0. X) by TOPGRP_1: 21;

      consider V be a_neighborhood of ( 0. X) such that

       A3: V in O and V c= ( [#] X) by A2, YELLOW13:def 2;

      (x + V) in B1 by A3;

      hence thesis;

    end;

    theorem :: CARDFIL3:27

    for X be LinearTopSpace, O be local_base of X, a be Point of X, P be Subset-Family of X st P = { (a + U) where U be Subset of X : U in O } holds P is basis of a

    proof

      let X be LinearTopSpace, O be basis of ( 0. X), a be Point of X, P be Subset-Family of X such that

       A1: P = { (a + U) where U be Subset of X : U in O };

      let A be a_neighborhood of a;

      a in ( Int A) by CONNSP_2:def 1;

      then (( - a) + ( Int A)) is a_neighborhood of ( 0. X) by RLTOPSP1: 9, CONNSP_2: 3;

      then

      consider V be a_neighborhood of ( 0. X) such that

       A2: V in O and

       A3: V c= (( - a) + ( Int A)) by YELLOW13:def 2;

      take U = (a + V);

      

       A4: (a + ( 0. X)) in (a + ( Int V)) by Lm1, CONNSP_2:def 1;

      (a + ( Int V)) c= ( Int U) by RLTOPSP1: 37;

      hence U is a_neighborhood of a by A4, CONNSP_2:def 1;

      thus U in P by A1, A2;

      U c= (a + (( - a) + ( Int A))) by A3, RLTOPSP1: 8;

      then U c= ((a + ( - a)) + ( Int A)) by RLTOPSP1: 6;

      then U c= (( 0. X) + ( Int A)) by RLVECT_1: 5;

      then ( Int A) c= A & U c= ( Int A) by RLTOPSP1: 5, TOPS_1: 16;

      hence thesis;

    end;

    theorem :: CARDFIL3:28

    for X be non empty LinearTopSpace, x be Point of X, O be local_base of X holds { (x + U) where U be Subset of X : U in O & U is a_neighborhood of ( 0. X) } = { (x + U) where U be Subset of X : U in O & U in ( NeighborhoodSystem ( 0. X)) }

    proof

      let X be non empty LinearTopSpace, x be Point of X, O be local_base of X;

      now

        let t be object;

        assume t in { (x + U) where U be Subset of X : U in O & U is a_neighborhood of ( 0. X) };

        then

        consider U1 be Subset of X such that

         A1: t = (x + U1) and

         A2: U1 in O and

         A3: U1 is a_neighborhood of ( 0. X);

        U1 in ( NeighborhoodSystem ( 0. X)) by A3, YELLOW19: 2;

        hence t in { (x + U) where U be Subset of X : U in O & U in ( NeighborhoodSystem ( 0. X)) } by A1, A2;

      end;

      then

       A4: { (x + U) where U be Subset of X : U in O & U is a_neighborhood of ( 0. X) } c= { (x + U) where U be Subset of X : U in O & U in ( NeighborhoodSystem ( 0. X)) };

      now

        let t be object;

        assume t in { (x + U) where U be Subset of X : U in O & U in ( NeighborhoodSystem ( 0. X)) };

        then

        consider U1 be Subset of X such that

         A5: t = (x + U1) and

         A6: U1 in O and

         A7: U1 in ( NeighborhoodSystem ( 0. X));

        U1 is a_neighborhood of ( 0. X) by A7, YELLOW19: 2;

        hence t in { (x + U) where U be Subset of X : U in O & U is a_neighborhood of ( 0. X) } by A5, A6;

      end;

      then { (x + U) where U be Subset of X : U in O & U in ( NeighborhoodSystem ( 0. X)) } c= { (x + U) where U be Subset of X : U in O & U is a_neighborhood of ( 0. X) };

      hence thesis by A4;

    end;

    theorem :: CARDFIL3:29

    

     Th10: for X be non empty LinearTopSpace, x be Point of X, O be local_base of X, B be Subset-Family of X st B = { (x + U) where U be Subset of X : U in O & U is a_neighborhood of ( 0. X) } holds B is basis of ( BOOL2F ( NeighborhoodSystem x))

    proof

      let X be non empty LinearTopSpace, x be Point of X, O be local_base of X, B be Subset-Family of X;

      assume

       A1: B = { (x + U) where U be Subset of X : U in O & U is a_neighborhood of ( 0. X) };

      set F = ( BOOL2F ( NeighborhoodSystem x));

      

       A2: F c= <.B.]

      proof

        now

          let t be object;

          assume t in F;

          then t in ( NeighborhoodSystem x) by CARDFIL2:def 20;

          then t 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

           A3: t = A;

          x in ( Int A) by CONNSP_2:def 1;

          then (( - x) + ( Int A)) is a_neighborhood of ( 0. X) by RLTOPSP1: 9, CONNSP_2: 3;

          then

          consider V be a_neighborhood of ( 0. X) such that

           A4: V in O and

           A5: V c= (( - x) + ( Int A)) by YELLOW13:def 2;

          set U = (x + V);

          

           A6: U in B by A1, A4;

          U c= (x + (( - x) + ( Int A))) by A5, RLTOPSP1: 8;

          then U c= ((x + ( - x)) + ( Int A)) by RLTOPSP1: 6;

          then U c= (( 0. X) + ( Int A)) by RLVECT_1: 5;

          then ( Int A) c= A & U c= ( Int A) by RLTOPSP1: 5, TOPS_1: 16;

          then U c= A;

          hence t in <.B.] by A3, A6, CARDFIL2:def 8;

        end;

        hence thesis;

      end;

       <.B.] c= F

      proof

        now

          let t be object;

          assume

           A7: t in <.B.];

          then

          reconsider t1 = t as Subset of X;

          consider b be Element of B such that

           A8: b c= t1 by A7, CARDFIL2:def 8;

          set v0 = the Element of O;

          B is non empty by A1, Lm2;

          then b in B;

          then

          consider U1 be Subset of X such that

           A9: b = (x + U1) and U1 in O and

           A10: U1 is a_neighborhood of ( 0. X) by A1;

          reconsider t2 = b as Element of B;

          

           A11: (x + ( 0. X)) in (x + ( Int U1)) by Lm1, A10, CONNSP_2:def 1;

          (x + ( Int U1)) c= ( Int (x + U1)) by RLTOPSP1: 37;

          then t2 is a_neighborhood of x by A9, A11, CONNSP_2:def 1;

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

          then t2 in ( NeighborhoodSystem x) by YELLOW19:def 1;

          then t2 in F by CARDFIL2:def 20;

          hence t in F by A8, CARD_FIL:def 1;

        end;

        hence thesis;

      end;

      hence thesis by CARDFIL2: 22, A2, XBOOLE_0:def 10;

    end;

    theorem :: CARDFIL3:30

    for X be non empty LinearTopSpace, s be sequence of the carrier of X, x be Point of X, V be local_base of X, B be Subset-Family of X st B = { (x + U) where U be Subset of X : U in V & U is a_neighborhood of ( 0. X) } holds x in ( lim_f s) iff for v be Element of B holds ex i be Nat st for j be Nat st i <= j holds (s . j) in v

    proof

      let X be non empty LinearTopSpace, s be sequence of the carrier of X, x be Point of X, V be local_base of X, B be Subset-Family of X;

      assume B = { (x + U) where U be Subset of X : U in V & U is a_neighborhood of ( 0. X) };

      then B is basis of ( BOOL2F ( NeighborhoodSystem x)) by Th10;

      hence x in ( lim_f s) iff for b be Element of B holds ex i be Nat st for j be Nat st i <= j holds (s . j) in b by CARDFIL2: 97;

    end;

    theorem :: CARDFIL3:31

    for X be non empty LinearTopSpace, s be sequence of the carrier of X, x be Point of X, V be local_base of X holds x in ( lim_f s) iff for v be Subset of X st v in (V /\ ( NeighborhoodSystem ( 0. X))) holds ex i be Nat st for j be Nat st i <= j holds (s . j) in (x + v)

    proof

      let X be non empty LinearTopSpace, s be sequence of the carrier of X, x be Point of X, V be local_base of X;

      set B = { (x + U) where U be Subset of X : U in V & U is a_neighborhood of ( 0. X) };

      reconsider B as Subset-Family of X by Lm2;

      

       A1: B is basis of ( BOOL2F ( NeighborhoodSystem x)) by Th10;

      hereby

        assume

         A2: x in ( lim_f s);

        let v be Subset of X;

        assume v in (V /\ ( NeighborhoodSystem ( 0. X)));

        then v in V & v in ( NeighborhoodSystem ( 0. X)) by XBOOLE_0:def 4;

        then v in V & v is a_neighborhood of ( 0. X) by YELLOW19: 2;

        then (x + v) in B;

        then

        reconsider b = (x + v) as Element of B;

        consider i0 be Nat such that

         A3: for j be Nat st i0 <= j holds (s . j) in b by A2, A1, CARDFIL2: 97;

        thus ex i be Nat st for j be Nat st i <= j holds (s . j) in (x + v) by A3;

      end;

      assume

       A4: for v be Subset of X st v in (V /\ ( NeighborhoodSystem ( 0. X))) holds ex i be Nat st for j be Nat st i <= j holds (s . j) in (x + v);

      for b be Element of B holds ex i be Nat st for j be Nat st i <= j holds (s . j) in b

      proof

        let b be Element of B;

        B is non empty by Lm2;

        then b in B;

        then

        consider U1 be Subset of X such that

         A5: b = (x + U1) and

         A6: U1 in V and

         A7: U1 is a_neighborhood of ( 0. X);

        U1 in ( NeighborhoodSystem ( 0. X)) by A7, YELLOW19: 2;

        then U1 in (V /\ ( NeighborhoodSystem ( 0. X))) by A6, XBOOLE_0:def 4;

        then

        consider i0 be Nat such that

         A8: for j be Nat st i0 <= j holds (s . j) in (x + U1) by A4;

        take i0;

        thus thesis by A5, A8;

      end;

      hence x in ( lim_f s) by A1, CARDFIL2: 97;

    end;

    theorem :: CARDFIL3:32

    for T be non empty LinearTopSpace, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), the carrier of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x)) st ( [#] L) is directed holds x in ( lim_f f) iff for b be Element of B holds ex i be Element of L st for j be Element of L st i <= j holds (f . j) in b by CARDFIL2: 84;

    

     Lm3: for T be non empty LinearTopSpace, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), the carrier of T, x be Point of T, V be local_base of T, B be Subset-Family of T st ( [#] L) is directed & B = { (x + U) where U be Subset of T : U in V & U is a_neighborhood of ( 0. T) } holds x in ( lim_f f) iff for b be Element of B holds ex i be Element of L st for j be Element of L st i <= j holds (f . j) in b

    proof

      let T be non empty LinearTopSpace, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), the carrier of T, x be Point of T, V be local_base of T, B be Subset-Family of T;

      assume that

       A1: ( [#] L) is directed and

       A2: B = { (x + U) where U be Subset of T : U in V & U is a_neighborhood of ( 0. T) };

      reconsider B1 = B as basis of ( BOOL2F ( NeighborhoodSystem x)) by A2, Th10;

      x in ( lim_f f) iff for b be Element of B1 holds ex i be Element of L st for j be Element of L st i <= j holds (f . j) in b by A1, CARDFIL2: 84;

      hence thesis;

    end;

    theorem :: CARDFIL3:33

    for T be non empty LinearTopSpace, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), the carrier of T, x be Point of T, V be local_base of T st ( [#] L) is directed holds x in ( lim_f f) iff (for v be Subset of T st v in (V /\ ( NeighborhoodSystem ( 0. T))) holds ex i be Element of L st for j be Element of L st i <= j holds (f . j) in (x + v))

    proof

      let T be non empty LinearTopSpace, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), the carrier of T, x be Point of T, V be local_base of T;

      assume

       A1: ( [#] L) is directed;

      set B = { (x + U) where U be Subset of T : U in V & U is a_neighborhood of ( 0. T) };

      reconsider B as Subset-Family of T by Lm2;

      now

        hereby

          assume

           A2: x in ( lim_f f);

          let v be Subset of T;

          assume v in (V /\ ( NeighborhoodSystem ( 0. T)));

          then v in V & v in ( NeighborhoodSystem ( 0. T)) by XBOOLE_0:def 4;

          then v in V & v is a_neighborhood of ( 0. T) by YELLOW19: 2;

          then (x + v) in B;

          then

          reconsider b = (x + v) as Element of B;

          consider i0 be Element of L such that

           A3: for j be Element of L st i0 <= j holds (f . j) in b by A1, A2, Lm3;

          take i0;

          thus for j be Element of L st i0 <= j holds (f . j) in (x + v) by A3;

        end;

        assume

         A4: for v be Subset of T st v in (V /\ ( NeighborhoodSystem ( 0. T))) holds ex i be Element of L st for j be Element of L st i <= j holds (f . j) in (x + v);

        for b be Element of B holds ex i be Element of L st for j be Element of L st i <= j holds (f . j) in b

        proof

          let b be Element of B;

          B is non empty by Lm2;

          then b in B;

          then

          consider U1 be Subset of T such that

           A5: b = (x + U1) and

           A6: U1 in V and

           A7: U1 is a_neighborhood of ( 0. T);

          U1 in ( NeighborhoodSystem ( 0. T)) by A7, YELLOW19: 2;

          then U1 in (V /\ ( NeighborhoodSystem ( 0. T))) by A6, XBOOLE_0:def 4;

          then

          consider i0 be Element of L such that

           A8: for j be Element of L st i0 <= j holds (f . j) in (x + U1) by A4;

          take i0;

          thus thesis by A5, A8;

        end;

        hence x in ( lim_f f) by A1, Lm3;

      end;

      hence thesis;

    end;

    begin

    definition

      let I be non empty set, L be AbGroup, x be the carrier of L -valued ManySortedSet of I, J be Element of ( Fin I);

      :: CARDFIL3:def4

      func Sum (x,J) -> Element of L means

      : Def1: ex p be one-to-one FinSequence of I st ( rng p) = J & it = (the addF of L "**" ( # (p,x)));

      existence

      proof

        consider p be FinSequence of I such that

         A1: ( rng p) = J & p is one-to-one by Th1;

        (the addF of L "**" ( # (p,x))) is Element of L;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Element of L such that

         A2: ex p1 be one-to-one FinSequence of I st ( rng p1) = J & X1 = (the addF of L "**" ( # (p1,x))) and

         A3: ex p2 be one-to-one FinSequence of I st ( rng p2) = J & X2 = (the addF of L "**" ( # (p2,x)));

        consider p1 be one-to-one FinSequence of I such that

         A4: ( rng p1) = J and

         A5: X1 = (the addF of L "**" ( # (p1,x))) by A2;

        consider p2 be one-to-one FinSequence of I such that

         A6: ( rng p2) = J and

         A7: X2 = (the addF of L "**" ( # (p2,x))) by A3;

        consider P be Permutation of ( dom p1) such that

         A8: p2 = (P * p1) & ( dom P) = ( dom p1) & ( rng P) = ( dom p1) by A4, A6, BHSP_5: 1;

        P is Permutation of ( dom ( # (p1,x)))

        proof

          ( dom x) = I by PARTFUN1:def 2;

          then ( rng p1) c= ( dom x) by FINSEQ_1:def 4;

          then ( dom (p1 * x)) = ( dom p1) by RELAT_1: 27;

          hence thesis;

        end;

        then

        reconsider P as Permutation of ( dom ( # (p1,x)));

        ( # (p2,x)) = (P * ( # (p1,x)))

        proof

          now

            hereby

              let t be object;

              assume

               A9: t in ( # (p2,x));

              consider a,b be object such that

               A10: t = [a, b] by A9, RELAT_1:def 1;

              consider z be object such that

               A11: [a, z] in p2 and

               A12: [z, b] in x by A9, A10, RELAT_1:def 8;

              consider y be object such that

               A13: [a, y] in P and

               A14: [y, z] in p1 by A11, A8, RELAT_1:def 8;

               [a, y] in P & [y, b] in (p1 * x) by A13, A12, A14, RELAT_1:def 8;

              hence t in (P * ( # (p1,x))) by A10, RELAT_1:def 8;

            end;

            let t be object;

            assume

             A15: t in (P * ( # (p1,x)));

            consider a,b be object such that

             A16: t = [a, b] by A15, RELAT_1:def 1;

            consider c be object such that

             A17: [a, c] in P and

             A18: [c, b] in (p1 * x) by A15, A16, RELAT_1:def 8;

            consider d be object such that

             A19: [c, d] in p1 and

             A20: [d, b] in x by A18, RELAT_1:def 8;

             [a, d] in p2 by A8, RELAT_1:def 8, A17, A19;

            hence t in ( # (p2,x)) by A16, A20, RELAT_1:def 8;

          end;

          hence thesis;

        end;

        hence thesis by A5, A7, FVSUM_1: 8, FINSOP_1: 7;

      end;

    end

    theorem :: CARDFIL3:34

    for I be non empty set, L be AbGroup, x be the carrier of L -valued ManySortedSet of I, J be Element of ( Fin I) holds for e be Element of ( Fin I) st e = {} holds ( Sum (x,e)) = ( 0. L) & for e,f be Element of ( Fin I) st e misses f holds ( Sum (x,(e \/ f))) = (( Sum (x,e)) + ( Sum (x,f)))

    proof

      let I be non empty set, L be AbGroup, x be the carrier of L -valued ManySortedSet of I, J be Element of ( Fin I);

       A1:

      now

        let e be Element of ( Fin I);

        assume

         A2: e = {} ;

        consider p be one-to-one FinSequence of I such that

         A3: ( rng p) = e and

         A4: ( Sum (x,e)) = (the addF of L "**" ( # (p,x))) by Def1;

        p = {} by A3, A2;

        then ( # (p,x)) = {} & the addF of L is having_a_unity & ( len ( # (p,x))) = 0 by FVSUM_1: 8;

        then ( Sum (x,e)) = ( the_unity_wrt the addF of L) by A4, FINSOP_1:def 1;

        hence ( Sum (x,e)) = ( 0. L) by FVSUM_1: 7;

      end;

      now

        let e,f be Element of ( Fin I);

        assume

         A5: e misses f;

        consider pe be one-to-one FinSequence of I such that

         A6: ( rng pe) = e and

         A7: ( Sum (x,e)) = (the addF of L "**" ( # (pe,x))) by Def1;

        consider pf be one-to-one FinSequence of I such that

         A8: ( rng pf) = f and

         A9: ( Sum (x,f)) = (the addF of L "**" ( # (pf,x))) by Def1;

        reconsider pepf = (pe ^ pf) as one-to-one FinSequence of I by A5, A6, A8, FINSEQ_3: 91;

        

         A10: ( # (pepf,x)) = (( # (pe,x)) ^ ( # (pf,x))) by Th3;

        ( rng pepf) = (e \/ f) by A6, A8, FINSEQ_1: 31;

        then ( Sum (x,(e \/ f))) = (the addF of L "**" ( # (pepf,x))) by Def1;

        hence ( Sum (x,(e \/ f))) = (( Sum (x,e)) + ( Sum (x,f))) by A7, A9, A10, FINSOP_1: 5, FVSUM_1: 8;

      end;

      hence thesis by A1;

    end;

    definition

      let I be non empty set, L be AbGroup, x be the carrier of L -valued ManySortedSet of I;

      :: CARDFIL3:def5

      func Partial_Sums (x) -> Function of ( [#] ( OrderedFIN I)), the carrier of L means for j be Element of ( Fin I) holds (it . j) = ( Sum (x,j));

      existence

      proof

        deffunc F( Element of ( Fin I)) = ( Sum (x,$1));

        consider f be Function of ( Fin I), the carrier of L such that

         A1: for t be Element of ( Fin I) holds (f . t) = F(t) from FUNCT_2:sch 4;

        the carrier of ( OrderedFIN I) = ( Fin I) by YELLOW_1: 1;

        then

         A2: ( [#] ( OrderedFIN I)) = ( Fin I) by STRUCT_0:def 3;

        reconsider f as Function of ( [#] ( OrderedFIN I)), the carrier of L by A2;

        for j be Element of ( Fin I) holds (f . j) = ( Sum (x,j)) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( Element of ( Fin I)) = ( Sum (x,$1));

        

         A3: for a,b be Function of ( Fin I), the carrier of L st (for q be Element of ( Fin I) holds (a . q) = F(q)) & (for q be Element of ( Fin I) holds (b . q) = F(q)) holds a = b from BINOP_2:sch 1;

        let f,g be Function of ( [#] ( OrderedFIN I)), the carrier of L;

        assume that

         A4: for j be Element of ( Fin I) holds (f . j) = ( Sum (x,j)) and

         A5: for j be Element of ( Fin I) holds (g . j) = ( Sum (x,j));

        the carrier of ( OrderedFIN I) = ( Fin I) by YELLOW_1: 1;

        then ( [#] ( OrderedFIN I)) = ( Fin I) by STRUCT_0:def 3;

        then

        reconsider f, g as Function of ( Fin I), the carrier of L;

        f = g by A3, A4, A5;

        hence thesis;

      end;

    end

    begin

    definition

      let I be non empty set, L be commutative TopGroup, x be the carrier of L -valued ManySortedSet of I, J be Element of ( Fin I);

      :: CARDFIL3:def6

      func Product (x,J) -> Element of L means

      : Def2: ex p be one-to-one FinSequence of I st ( rng p) = J & it = (the multF of L "**" ( # (p,x)));

      existence

      proof

        consider p be FinSequence of I such that

         A1: ( rng p) = J & p is one-to-one by Th1;

        (the multF of L "**" ( # (p,x))) is Element of L;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Element of L such that

         A2: ex p1 be one-to-one FinSequence of I st ( rng p1) = J & X1 = (the multF of L "**" ( # (p1,x))) and

         A3: ex p2 be one-to-one FinSequence of I st ( rng p2) = J & X2 = (the multF of L "**" ( # (p2,x)));

        consider p1 be one-to-one FinSequence of I such that

         A4: ( rng p1) = J and

         A5: X1 = (the multF of L "**" ( # (p1,x))) by A2;

        consider p2 be one-to-one FinSequence of I such that

         A6: ( rng p2) = J and

         A7: X2 = (the multF of L "**" ( # (p2,x))) by A3;

        consider P be Permutation of ( dom p1) such that

         A8: p2 = (P * p1) & ( dom P) = ( dom p1) & ( rng P) = ( dom p1) by A4, A6, BHSP_5: 1;

        P is Permutation of ( dom ( # (p1,x)))

        proof

          ( dom x) = I by PARTFUN1:def 2;

          then ( rng p1) c= ( dom x) by FINSEQ_1:def 4;

          then ( dom (p1 * x)) = ( dom p1) by RELAT_1: 27;

          hence thesis;

        end;

        then

        reconsider P as Permutation of ( dom ( # (p1,x)));

        ( # (p2,x)) = (P * ( # (p1,x)))

        proof

          now

            hereby

              let t be object;

              assume

               A9: t in ( # (p2,x));

              consider a,b be object such that

               A10: t = [a, b] by A9, RELAT_1:def 1;

              consider z be object such that

               A11: [a, z] in p2 and

               A12: [z, b] in x by A9, A10, RELAT_1:def 8;

              consider y be object such that

               A13: [a, y] in P and

               A14: [y, z] in p1 by A11, A8, RELAT_1:def 8;

               [a, y] in P & [y, b] in (p1 * x) by A13, A12, A14, RELAT_1:def 8;

              hence t in (P * ( # (p1,x))) by A10, RELAT_1:def 8;

            end;

            let t be object;

            assume

             A15: t in (P * ( # (p1,x)));

            consider a,b be object such that

             A16: t = [a, b] by A15, RELAT_1:def 1;

            consider c be object such that

             A17: [a, c] in P and

             A18: [c, b] in (p1 * x) by A15, A16, RELAT_1:def 8;

            consider d be object such that

             A19: [c, d] in p1 and

             A20: [d, b] in x by A18, RELAT_1:def 8;

             [a, d] in p2 by A8, RELAT_1:def 8, A17, A19;

            hence t in ( # (p2,x)) by A16, A20, RELAT_1:def 8;

          end;

          hence thesis;

        end;

        hence thesis by A5, A7, FINSOP_1: 7;

      end;

    end

    theorem :: CARDFIL3:35

    

     Th11: for I be set, G be TopGroup, f be Function of ( [#] ( OrderedFIN I)), the carrier of G, x be Point of G, B be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_f f) iff for b be Element of B holds ex i be Element of ( OrderedFIN I) st for j be Element of ( OrderedFIN I) st i <= j holds (f . j) in b

    proof

      let I be set, G be TopGroup, f be Function of ( [#] ( OrderedFIN I)), the carrier of G, x be Point of G, B be basis of ( BOOL2F ( NeighborhoodSystem x));

      ( [#] ( OrderedFIN I)) is directed by Th4;

      hence thesis by CARDFIL2: 84;

    end;

    theorem :: CARDFIL3:36

    for I be non empty set, L be commutative TopGroup, x be the carrier of L -valued ManySortedSet of I, J be Element of ( Fin I) holds for e be Element of ( Fin I) st e = {} holds ( Product (x,e)) = ( 1_ L) & for e,f be Element of ( Fin I) st e misses f holds ( Product (x,(e \/ f))) = (( Product (x,e)) * ( Product (x,f)))

    proof

      let I be non empty set, L be commutative TopGroup, x be the carrier of L -valued ManySortedSet of I, J be Element of ( Fin I);

       A1:

      now

        let e be Element of ( Fin I);

        assume

         A2: e = {} ;

        consider p be one-to-one FinSequence of I such that

         A3: ( rng p) = e and

         A4: ( Product (x,e)) = (the multF of L "**" ( # (p,x))) by Def2;

        p = {} by A3, A2;

        then ( # (p,x)) = {} & the multF of L is having_a_unity & ( len ( # (p,x))) = 0 ;

        then ( Product (x,e)) = ( the_unity_wrt the multF of L) by A4, FINSOP_1:def 1;

        hence ( Product (x,e)) = ( 1_ L) by GROUP_1: 22;

      end;

      now

        let e,f be Element of ( Fin I);

        assume

         A5: e misses f;

        consider pe be one-to-one FinSequence of I such that

         A6: ( rng pe) = e and

         A7: ( Product (x,e)) = (the multF of L "**" ( # (pe,x))) by Def2;

        consider pf be one-to-one FinSequence of I such that

         A8: ( rng pf) = f and

         A9: ( Product (x,f)) = (the multF of L "**" ( # (pf,x))) by Def2;

        reconsider pepf = (pe ^ pf) as one-to-one FinSequence of I by A5, A6, A8, FINSEQ_3: 91;

        

         A10: ( # (pepf,x)) = (( # (pe,x)) ^ ( # (pf,x))) by Th3;

        ( rng pepf) = (e \/ f) by A6, A8, FINSEQ_1: 31;

        then ( Product (x,(e \/ f))) = (the multF of L "**" ( # (pepf,x))) by Def2;

        hence ( Product (x,(e \/ f))) = (( Product (x,e)) * ( Product (x,f))) by A7, A9, A10, FINSOP_1: 5;

      end;

      hence thesis by A1;

    end;

    definition

      let I be non empty set, L be commutative TopGroup, x be the carrier of L -valued ManySortedSet of I;

      :: CARDFIL3:def7

      func Partial_Product (x) -> Function of ( [#] ( OrderedFIN I)), the carrier of L means for j be Element of ( Fin I) holds (it . j) = ( Product (x,j));

      existence

      proof

        deffunc F( Element of ( Fin I)) = ( Product (x,$1));

        consider f be Function of ( Fin I), the carrier of L such that

         A1: for t be Element of ( Fin I) holds (f . t) = F(t) from FUNCT_2:sch 4;

        the carrier of ( OrderedFIN I) = ( Fin I) by YELLOW_1: 1;

        then ( [#] ( OrderedFIN I)) = ( Fin I) by STRUCT_0:def 3;

        then

        reconsider f as Function of ( [#] ( OrderedFIN I)), the carrier of L;

        for j be Element of ( Fin I) holds (f . j) = ( Product (x,j)) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( Element of ( Fin I)) = ( Product (x,$1));

        

         A2: for a,b be Function of ( Fin I), the carrier of L st (for q be Element of ( Fin I) holds (a . q) = F(q)) & (for q be Element of ( Fin I) holds (b . q) = F(q)) holds a = b from BINOP_2:sch 1;

        let f,g be Function of ( [#] ( OrderedFIN I)), the carrier of L;

        assume that

         A3: for j be Element of ( Fin I) holds (f . j) = ( Product (x,j)) and

         A4: for j be Element of ( Fin I) holds (g . j) = ( Product (x,j));

        the carrier of ( OrderedFIN I) = ( Fin I) by YELLOW_1: 1;

        then ( [#] ( OrderedFIN I)) = ( Fin I) by STRUCT_0:def 3;

        then

        reconsider f, g as Function of ( Fin I), the carrier of L;

        f = g by A2, A3, A4;

        hence thesis;

      end;

    end

    theorem :: CARDFIL3:37

    for I be non empty set, G be commutative TopGroup, s be the carrier of G -valued ManySortedSet of I, x be Point of G, B be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_f ( Partial_Product s)) iff for b be Element of B holds ex i be Element of ( OrderedFIN I) st for j be Element of ( OrderedFIN I) st i <= j holds (( Partial_Product s) . j) in b by Th11;

    begin

    definition

      let I be non empty set, L be Abelian TopaddGroup, x be the carrier of L -valued ManySortedSet of I, J be Element of ( Fin I);

      :: CARDFIL3:def8

      func Sum (x,J) -> Element of L means

      : Def3: ex p be one-to-one FinSequence of I st ( rng p) = J & it = (the addF of L "**" ( # (p,x)));

      existence

      proof

        consider p be FinSequence of I such that

         A1: ( rng p) = J & p is one-to-one by Th1;

        (the addF of L "**" ( # (p,x))) is Element of L;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Element of L such that

         A2: ex p1 be one-to-one FinSequence of I st ( rng p1) = J & X1 = (the addF of L "**" ( # (p1,x))) and

         A3: ex p2 be one-to-one FinSequence of I st ( rng p2) = J & X2 = (the addF of L "**" ( # (p2,x)));

        consider p1 be one-to-one FinSequence of I such that

         A4: ( rng p1) = J and

         A5: X1 = (the addF of L "**" ( # (p1,x))) by A2;

        consider p2 be one-to-one FinSequence of I such that

         A6: ( rng p2) = J and

         A7: X2 = (the addF of L "**" ( # (p2,x))) by A3;

        consider P be Permutation of ( dom p1) such that

         A8: p2 = (P * p1) & ( dom P) = ( dom p1) & ( rng P) = ( dom p1) by A4, A6, BHSP_5: 1;

        P is Permutation of ( dom ( # (p1,x)))

        proof

          ( dom x) = I by PARTFUN1:def 2;

          then ( rng p1) c= ( dom x) by FINSEQ_1:def 4;

          then ( dom (p1 * x)) = ( dom p1) by RELAT_1: 27;

          hence thesis;

        end;

        then

        reconsider P as Permutation of ( dom ( # (p1,x)));

        

         A9: ( # (p2,x)) = (P * ( # (p1,x)))

        proof

          now

            hereby

              let t be object;

              assume

               A10: t in ( # (p2,x));

              consider a,b be object such that

               A11: t = [a, b] by A10, RELAT_1:def 1;

              consider z be object such that

               A12: [a, z] in p2 and

               A13: [z, b] in x by A10, A11, RELAT_1:def 8;

              consider y be object such that

               A14: [a, y] in P and

               A15: [y, z] in p1 by A12, A8, RELAT_1:def 8;

               [a, y] in P & [y, b] in (p1 * x) by A14, A13, A15, RELAT_1:def 8;

              hence t in (P * ( # (p1,x))) by A11, RELAT_1:def 8;

            end;

            let t be object;

            assume

             A16: t in (P * ( # (p1,x)));

            then

            consider a,b be object such that

             A17: t = [a, b] by RELAT_1:def 1;

            consider c be object such that

             A18: [a, c] in P and

             A19: [c, b] in (p1 * x) by A16, A17, RELAT_1:def 8;

            consider d be object such that

             A20: [c, d] in p1 and

             A21: [d, b] in x by A19, RELAT_1:def 8;

             [a, d] in p2 by A8, RELAT_1:def 8, A18, A20;

            hence t in ( # (p2,x)) by A17, A21, RELAT_1:def 8;

          end;

          hence thesis;

        end;

        the addF of L is commutative by GROUP_1A: 203;

        hence thesis by A9, A5, A7, FINSOP_1: 7;

      end;

    end

    theorem :: CARDFIL3:38

    

     Th12: for I be set, G be TopaddGroup, f be Function of ( [#] ( OrderedFIN I)), the carrier of G, x be Point of G, B be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_f f) iff for b be Element of B holds ex i be Element of ( OrderedFIN I) st for j be Element of ( OrderedFIN I) st i <= j holds (f . j) in b

    proof

      let I be set, G be TopaddGroup, f be Function of ( [#] ( OrderedFIN I)), the carrier of G, x be Point of G, B be basis of ( BOOL2F ( NeighborhoodSystem x));

      ( [#] ( OrderedFIN I)) is directed by Th4;

      hence thesis by CARDFIL2: 84;

    end;

    theorem :: CARDFIL3:39

    for I be non empty set, L be Abelian TopaddGroup, x be the carrier of L -valued ManySortedSet of I, J be Element of ( Fin I) holds for e be Element of ( Fin I) st e = {} holds ( Sum (x,e)) = ( 0_ L) & for e,f be Element of ( Fin I) st e misses f holds ( Sum (x,(e \/ f))) = (( Sum (x,e)) + ( Sum (x,f)))

    proof

      let I be non empty set, L be Abelian TopaddGroup, x be the carrier of L -valued ManySortedSet of I, J be Element of ( Fin I);

       A1:

      now

        let e be Element of ( Fin I);

        assume

         A2: e = {} ;

        consider p be one-to-one FinSequence of I such that

         A3: ( rng p) = e and

         A4: ( Sum (x,e)) = (the addF of L "**" ( # (p,x))) by Def3;

        p = {} by A3, A2;

        then ( # (p,x)) = {} & the addF of L is having_a_unity & ( len ( # (p,x))) = 0 ;

        then ( Sum (x,e)) = ( the_unity_wrt the addF of L) by A4, FINSOP_1:def 1;

        hence ( Sum (x,e)) = ( 0_ L) by GROUP_1A: 21;

      end;

      now

        let e,f be Element of ( Fin I);

        assume

         A5: e misses f;

        consider pe be one-to-one FinSequence of I such that

         A6: ( rng pe) = e and

         A7: ( Sum (x,e)) = (the addF of L "**" ( # (pe,x))) by Def3;

        consider pf be one-to-one FinSequence of I such that

         A8: ( rng pf) = f and

         A9: ( Sum (x,f)) = (the addF of L "**" ( # (pf,x))) by Def3;

        reconsider pepf = (pe ^ pf) as one-to-one FinSequence of I by A5, A6, A8, FINSEQ_3: 91;

        

         A10: ( # (pepf,x)) = (( # (pe,x)) ^ ( # (pf,x))) by Th3;

        ( rng pepf) = (e \/ f) by A6, A8, FINSEQ_1: 31;

        then ( Sum (x,(e \/ f))) = (the addF of L "**" ( # (pepf,x))) by Def3;

        hence ( Sum (x,(e \/ f))) = (( Sum (x,e)) + ( Sum (x,f))) by A7, A9, A10, FINSOP_1: 5;

      end;

      hence thesis by A1;

    end;

    definition

      let I be non empty set, L be Abelian TopaddGroup, x be the carrier of L -valued ManySortedSet of I;

      :: CARDFIL3:def9

      func Partial_Sums (x) -> Function of ( [#] ( OrderedFIN I)), the carrier of L means for j be Element of ( Fin I) holds (it . j) = ( Sum (x,j));

      existence

      proof

        deffunc F( Element of ( Fin I)) = ( Sum (x,$1));

        consider f be Function of ( Fin I), the carrier of L such that

         A1: for t be Element of ( Fin I) holds (f . t) = F(t) from FUNCT_2:sch 4;

        the carrier of ( OrderedFIN I) = ( Fin I) by YELLOW_1: 1;

        then ( [#] ( OrderedFIN I)) = ( Fin I) by STRUCT_0:def 3;

        then

        reconsider f as Function of ( [#] ( OrderedFIN I)), the carrier of L;

        for j be Element of ( Fin I) holds (f . j) = ( Sum (x,j)) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( Element of ( Fin I)) = ( Sum (x,$1));

        

         A2: for a,b be Function of ( Fin I), the carrier of L st (for q be Element of ( Fin I) holds (a . q) = F(q)) & (for q be Element of ( Fin I) holds (b . q) = F(q)) holds a = b from BINOP_2:sch 1;

        let f,g be Function of ( [#] ( OrderedFIN I)), the carrier of L;

        assume that

         A3: for j be Element of ( Fin I) holds (f . j) = ( Sum (x,j)) and

         A4: for j be Element of ( Fin I) holds (g . j) = ( Sum (x,j));

        the carrier of ( OrderedFIN I) = ( Fin I) by YELLOW_1: 1;

        then ( [#] ( OrderedFIN I)) = ( Fin I) by STRUCT_0:def 3;

        then

        reconsider f, g as Function of ( Fin I), the carrier of L;

        f = g by A2, A3, A4;

        hence thesis;

      end;

    end

    theorem :: CARDFIL3:40

    for I be non empty set, G be Abelian TopaddGroup, s be the carrier of G -valued ManySortedSet of I, x be Point of G, B be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_f ( Partial_Sums s)) iff for b be Element of B holds ex i be Element of ( OrderedFIN I) st for j be Element of ( OrderedFIN I) st i <= j holds (( Partial_Sums s) . j) in b by Th12;