:: by Roland Coghetto

::

:: Received August 14, 2015

:: Copyright (c) 2015-2016 Association of Mizar Users

theorem Th1: :: CARDFIL3:2

for I, J being set st J in Fin I holds

ex p being FinSequence of I st

( J = rng p & p is one-to-one )

ex p being FinSequence of I st

( J = rng p & p is one-to-one )

proof end;

theorem Th2: :: CARDFIL3:3

for I being set

for Y being non empty set

for x being b_{2} -valued ManySortedSet of I

for p being FinSequence of I holds p * x is FinSequence of Y

for Y being non empty set

for x being b

for p being FinSequence of I holds p * x is FinSequence of Y

proof end;

theorem Th3: :: CARDFIL3:4

for I, X being non empty set

for x being b_{2} -valued ManySortedSet of I

for p, q being FinSequence of I holds (p ^ q) * x = (p * x) ^ (q * x)

for x being b

for p, q being FinSequence of I holds (p ^ q) * x = (p * x) ^ (q * x)

proof end;

definition

let I be set ;

let Y be non empty set ;

let x be Y -valued ManySortedSet of I;

let p be FinSequence of I;

coherence

p * x is FinSequence of Y by Th2;

end;
let Y be non empty set ;

let x be Y -valued ManySortedSet of I;

let p be FinSequence of I;

coherence

p * x is FinSequence of Y by Th2;

:: deftheorem defines # CARDFIL3:def 1 :

for I being set

for Y being non empty set

for x being b_{2} -valued ManySortedSet of I

for p being FinSequence of I holds # (p,x) = p * x;

for I being set

for Y being non empty set

for x being b

for p being FinSequence of I holds # (p,x) = p * x;

definition

let I be set ;

InclPoset (Fin I) is non empty reflexive transitive RelStr ;

end;
func OrderedFIN I -> non empty reflexive transitive RelStr equals :: CARDFIL3:def 2

InclPoset (Fin I);

coherence InclPoset (Fin I);

InclPoset (Fin I) is non empty reflexive transitive RelStr ;

:: deftheorem defines OrderedFIN CARDFIL3:def 2 :

for I being set holds OrderedFIN I = InclPoset (Fin I);

for I being set holds OrderedFIN I = InclPoset (Fin I);

theorem Th5: :: CARDFIL3:6

for M being non empty MetrSpace

for x being Point of (TopSpaceMetr M) holds Balls x is basis of (BOOL2F (NeighborhoodSystem x))

for x being Point of (TopSpaceMetr M) holds Balls x is basis of (BOOL2F (NeighborhoodSystem x))

proof end;

theorem :: CARDFIL3:7

for M being non empty MetrSpace

for L being non empty reflexive transitive RelStr

for f being Function of ([#] L), the carrier of (TopSpaceMetr M)

for x being Point of (TopSpaceMetr M)

for B being basis of (BOOL2F (NeighborhoodSystem x)) st [#] L is directed holds

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b ) by CARDFIL2:84;

for L being non empty reflexive transitive RelStr

for f being Function of ([#] L), the carrier of (TopSpaceMetr M)

for x being Point of (TopSpaceMetr M)

for B being basis of (BOOL2F (NeighborhoodSystem x)) st [#] L is directed holds

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b ) by CARDFIL2:84;

theorem :: CARDFIL3:8

for M being non empty MetrSpace

for L being non empty reflexive transitive RelStr

for f being Function of ([#] L), the carrier of (TopSpaceMetr M)

for x being Point of (TopSpaceMetr M) st [#] L is directed holds

( x in lim_f f iff for b being Element of Balls x ex n being Element of L st

for m being Element of L st n <= m holds

f . m in b )

for L being non empty reflexive transitive RelStr

for f being Function of ([#] L), the carrier of (TopSpaceMetr M)

for x being Point of (TopSpaceMetr M) st [#] L is directed holds

( x in lim_f f iff for b being Element of Balls x ex n being Element of L st

for m being Element of L st n <= m holds

f . m in b )

proof end;

theorem Th6: :: CARDFIL3:9

for M being non empty MetrSpace

for s being sequence of the carrier of (TopSpaceMetr M)

for x being Point of (TopSpaceMetr M) holds

( x in lim_f s iff for b being Element of Balls x ex i being Nat st

for j being Nat st i <= j holds

s . j in b )

for s being sequence of the carrier of (TopSpaceMetr M)

for x being Point of (TopSpaceMetr M) holds

( x in lim_f s iff for b being Element of Balls x ex i being Nat st

for j being Nat st i <= j holds

s . j in b )

proof end;

theorem Th7: :: CARDFIL3:10

for T being non empty TopStruct

for s being sequence of T

for x being Point of T holds

( x in Lim s iff for U1 being Subset of T st U1 is open & x in U1 holds

ex n being Nat st

for m being Nat st n <= m holds

s . m in U1 )

for s being sequence of T

for x being Point of T holds

( x in Lim s iff for U1 being Subset of T st U1 is open & x in U1 holds

ex n being Nat st

for m being Nat st n <= m holds

s . m in U1 )

proof end;

theorem Th8: :: CARDFIL3:11

for M being non empty MetrSpace

for s being sequence of the carrier of (TopSpaceMetr M)

for x being Point of (TopSpaceMetr M) holds

( x in Lim s iff for b being Element of Balls x ex n being Nat st

for m being Nat st n <= m holds

s . m in b )

for s being sequence of the carrier of (TopSpaceMetr M)

for x being Point of (TopSpaceMetr M) holds

( x in Lim s iff for b being Element of Balls x ex n being Nat st

for m being Nat st n <= m holds

s . m in b )

proof end;

theorem :: CARDFIL3:12

for M being non empty MetrSpace

for s being sequence of the carrier of (TopSpaceMetr M)

for x being Point of (TopSpaceMetr M) holds

( x in lim_f s iff x in Lim s )

for s being sequence of the carrier of (TopSpaceMetr M)

for x being Point of (TopSpaceMetr M) holds

( x in lim_f s iff x in Lim s )

proof end;

theorem :: CARDFIL3:13

for N being RealNormSpace

for L being non empty reflexive transitive RelStr

for f being Function of ([#] L), the carrier of (TopSpaceMetr (MetricSpaceNorm N))

for x being Point of (TopSpaceMetr (MetricSpaceNorm N))

for B being basis of (BOOL2F (NeighborhoodSystem x)) st [#] L is directed holds

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b ) by CARDFIL2:84;

for L being non empty reflexive transitive RelStr

for f being Function of ([#] L), the carrier of (TopSpaceMetr (MetricSpaceNorm N))

for x being Point of (TopSpaceMetr (MetricSpaceNorm N))

for B being basis of (BOOL2F (NeighborhoodSystem x)) st [#] L is directed holds

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b ) by CARDFIL2:84;

theorem :: CARDFIL3:14

for N being RealNormSpace

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

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

theorem :: CARDFIL3:15

for N being RealNormSpace

for s being sequence of the carrier of (TopSpaceMetr (MetricSpaceNorm N))

for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) holds

( x in lim_f s iff for b being Element of Balls x ex i being Nat st

for j being Nat st i <= j holds

s . j in b ) by Th6;

for s being sequence of the carrier of (TopSpaceMetr (MetricSpaceNorm N))

for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) holds

( x in lim_f s iff for b being Element of Balls x ex i being Nat st

for j being Nat st i <= j holds

s . j in b ) by Th6;

theorem :: CARDFIL3:16

for N being RealNormSpace

for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) ex y being Point of (MetricSpaceNorm N) st

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

for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) ex y being Point of (MetricSpaceNorm N) st

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

theorem :: CARDFIL3:17

for N being RealNormSpace

for x being Point of (TopSpaceMetr (MetricSpaceNorm N))

for y being Point of (MetricSpaceNorm N)

for n being positive Nat st x = y holds

Ball (y,(1 / n)) in Balls x

for x being Point of (TopSpaceMetr (MetricSpaceNorm N))

for y being Point of (MetricSpaceNorm N)

for n being positive Nat st x = y holds

Ball (y,(1 / n)) in Balls x

proof end;

theorem :: CARDFIL3:18

for N being RealNormSpace

for x being Point of (MetricSpaceNorm N)

for n being Nat st n <> 0 holds

Ball (x,(1 / n)) = { q where q is Element of (MetricSpaceNorm N) : dist (x,q) < 1 / n } by METRIC_1:def 14;

for x being Point of (MetricSpaceNorm N)

for n being Nat st n <> 0 holds

Ball (x,(1 / n)) = { q where q is Element of (MetricSpaceNorm N) : dist (x,q) < 1 / n } by METRIC_1:def 14;

theorem :: CARDFIL3:19

theorem :: CARDFIL3:20

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

theorem :: CARDFIL3:21

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

theorem :: CARDFIL3:22

for PM being 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:24

for N being RealNormSpace

for s being sequence of the carrier of (TopSpaceMetr (MetricSpaceNorm N))

for j being Nat holds s . j is Element of the carrier of (TopSpaceMetr (MetricSpaceNorm N)) ;

for s being sequence of the carrier of (TopSpaceMetr (MetricSpaceNorm N))

for j being Nat holds s . j is Element of the carrier of (TopSpaceMetr (MetricSpaceNorm N)) ;

definition

let N be RealNormSpace;

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

coherence

x is Point of N

end;
let x be Point of (TopSpaceMetr (MetricSpaceNorm N));

coherence

x is Point of N

proof end;

:: deftheorem defines # CARDFIL3:def 3 :

for N being RealNormSpace

for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) holds # x = x;

for N being RealNormSpace

for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) holds # x = x;

theorem :: CARDFIL3:25

for N being RealNormSpace

for s being sequence of the carrier of (TopSpaceMetr (MetricSpaceNorm N))

for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) holds

( x in lim_f s iff for n being positive Nat ex i being Nat st

for j being Nat st i <= j holds

||.((# x) - (# (s . j))).|| < 1 / n )

for s being sequence of the carrier of (TopSpaceMetr (MetricSpaceNorm N))

for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) holds

( x in lim_f s iff for n being positive Nat ex i being Nat st

for j being Nat st i <= j holds

||.((# x) - (# (s . j))).|| < 1 / n )

proof end;

Lm1: for X being non empty addLoopStr

for M being Subset of X

for x, y being Point of X st y in M holds

x + y in x + M

proof end;

Lm2: for X being LinearTopSpace

for x being Point of X

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

proof end;

theorem :: CARDFIL3:27

for X being LinearTopSpace

for O being local_base of X

for a being Point of X

for P being Subset-Family of X st P = { (a + U) where U is Subset of X : U in O } holds

P is basis of a

for O being local_base of X

for a being Point of X

for P being Subset-Family of X st P = { (a + U) where U is Subset of X : U in O } holds

P is basis of a

proof end;

theorem :: CARDFIL3:28

for X being LinearTopSpace

for x being Point of X

for O being local_base of X holds { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } = { (x + U) where U is Subset of X : ( U in O & U in NeighborhoodSystem (0. X) ) }

for x being Point of X

for O being local_base of X holds { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } = { (x + U) where U is Subset of X : ( U in O & U in NeighborhoodSystem (0. X) ) }

proof end;

theorem Th10: :: CARDFIL3:29

for X being LinearTopSpace

for x being Point of X

for O being local_base of X

for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } holds

B is basis of (BOOL2F (NeighborhoodSystem x))

for x being Point of X

for O being local_base of X

for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } holds

B is basis of (BOOL2F (NeighborhoodSystem x))

proof end;

theorem :: CARDFIL3:30

for X being LinearTopSpace

for s being sequence of the carrier of X

for x being Point of X

for V being local_base of X

for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } holds

( x in lim_f s iff for v being Element of B ex i being Nat st

for j being Nat st i <= j holds

s . j in v )

for s being sequence of the carrier of X

for x being Point of X

for V being local_base of X

for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } holds

( x in lim_f s iff for v being Element of B ex i being Nat st

for j being Nat st i <= j holds

s . j in v )

proof end;

theorem :: CARDFIL3:31

for X being LinearTopSpace

for s being sequence of the carrier of X

for x being Point of X

for V being local_base of X holds

( x in lim_f s iff for v being Subset of X st v in V /\ (NeighborhoodSystem (0. X)) holds

ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v )

for s being sequence of the carrier of X

for x being Point of X

for V being local_base of X holds

( x in lim_f s iff for v being Subset of X st v in V /\ (NeighborhoodSystem (0. X)) holds

ex i being Nat st

for j being Nat st i <= j holds

s . j in x + v )

proof end;

theorem :: CARDFIL3:32

for T being LinearTopSpace

for L being non empty reflexive transitive RelStr

for f being Function of ([#] L), the carrier of T

for x being Point of T

for B being basis of (BOOL2F (NeighborhoodSystem x)) st [#] L is directed holds

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b ) by CARDFIL2:84;

for L being non empty reflexive transitive RelStr

for f being Function of ([#] L), the carrier of T

for x being Point of T

for B being basis of (BOOL2F (NeighborhoodSystem x)) st [#] L is directed holds

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b ) by CARDFIL2:84;

Lm3: for T being LinearTopSpace

for L being non empty reflexive transitive RelStr

for f being Function of ([#] L), the carrier of T

for x being Point of T

for V being local_base of T

for B being Subset-Family of T st [#] L is directed & B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } holds

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b )

proof end;

theorem :: CARDFIL3:33

for T being LinearTopSpace

for L being non empty reflexive transitive RelStr

for f being Function of ([#] L), the carrier of T

for x being Point of T

for V being local_base of T st [#] L is directed holds

( x in lim_f f iff for v being Subset of T st v in V /\ (NeighborhoodSystem (0. T)) holds

ex i being Element of L st

for j being Element of L st i <= j holds

f . j in x + v )

for L being non empty reflexive transitive RelStr

for f being Function of ([#] L), the carrier of T

for x being Point of T

for V being local_base of T st [#] L is directed holds

( x in lim_f f iff for v being Subset of T st v in V /\ (NeighborhoodSystem (0. T)) holds

ex i being Element of L st

for j being Element of L st i <= j holds

f . j in x + v )

proof end;

definition

let I be non empty set ;

let L be AbGroup;

let x be the carrier of L -valued ManySortedSet of I;

let J be Element of Fin I;

ex b_{1} being Element of L ex p being one-to-one FinSequence of I st

( rng p = J & b_{1} = the addF of L "**" (# (p,x)) )

for b_{1}, b_{2} being Element of L st ex p being one-to-one FinSequence of I st

( rng p = J & b_{1} = the addF of L "**" (# (p,x)) ) & ex p being one-to-one FinSequence of I st

( rng p = J & b_{2} = the addF of L "**" (# (p,x)) ) holds

b_{1} = b_{2}

end;
let L be AbGroup;

let x be the carrier of L -valued ManySortedSet of I;

let J be Element of Fin I;

func Sum (x,J) -> Element of L means :Def1: :: CARDFIL3:def 4

ex p being one-to-one FinSequence of I st

( rng p = J & it = the addF of L "**" (# (p,x)) );

existence ex p being one-to-one FinSequence of I st

( rng p = J & it = the addF of L "**" (# (p,x)) );

ex b

( rng p = J & b

proof end;

uniqueness for b

( rng p = J & b

( rng p = J & b

b

proof end;

:: deftheorem Def1 defines Sum CARDFIL3:def 4 :

for I being non empty set

for L being AbGroup

for x being the carrier of b_{2} -valued ManySortedSet of I

for J being Element of Fin I

for b_{5} being Element of L holds

( b_{5} = Sum (x,J) iff ex p being one-to-one FinSequence of I st

( rng p = J & b_{5} = the addF of L "**" (# (p,x)) ) );

for I being non empty set

for L being AbGroup

for x being the carrier of b

for J being Element of Fin I

for b

( b

( rng p = J & b

theorem :: CARDFIL3:34

for I being non empty set

for L being AbGroup

for x being the carrier of b_{2} -valued ManySortedSet of I

for J, e being Element of Fin I st e = {} holds

( Sum (x,e) = 0. L & ( for e, f being Element of Fin I st e misses f holds

Sum (x,(e \/ f)) = (Sum (x,e)) + (Sum (x,f)) ) )

for L being AbGroup

for x being the carrier of b

for J, e being Element of Fin I st e = {} holds

( Sum (x,e) = 0. L & ( for e, f being Element of Fin I st e misses f holds

Sum (x,(e \/ f)) = (Sum (x,e)) + (Sum (x,f)) ) )

proof end;

definition

let I be non empty set ;

let L be AbGroup;

let x be the carrier of L -valued ManySortedSet of I;

ex b_{1} being Function of ([#] (OrderedFIN I)), the carrier of L st

for j being Element of Fin I holds b_{1} . j = Sum (x,j)

for b_{1}, b_{2} being Function of ([#] (OrderedFIN I)), the carrier of L st ( for j being Element of Fin I holds b_{1} . j = Sum (x,j) ) & ( for j being Element of Fin I holds b_{2} . j = Sum (x,j) ) holds

b_{1} = b_{2}

end;
let L be AbGroup;

let x be the carrier of L -valued ManySortedSet of I;

func Partial_Sums x -> Function of ([#] (OrderedFIN I)), the carrier of L means :: CARDFIL3:def 5

for j being Element of Fin I holds it . j = Sum (x,j);

existence for j being Element of Fin I holds it . j = Sum (x,j);

ex b

for j being Element of Fin I holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines Partial_Sums CARDFIL3:def 5 :

for I being non empty set

for L being AbGroup

for x being the carrier of b_{2} -valued ManySortedSet of I

for b_{4} being Function of ([#] (OrderedFIN I)), the carrier of L holds

( b_{4} = Partial_Sums x iff for j being Element of Fin I holds b_{4} . j = Sum (x,j) );

for I being non empty set

for L being AbGroup

for x being the carrier of b

for b

( b

definition

let I be non empty set ;

let L be commutative TopGroup;

let x be the carrier of L -valued ManySortedSet of I;

let J be Element of Fin I;

ex b_{1} being Element of L ex p being one-to-one FinSequence of I st

( rng p = J & b_{1} = the multF of L "**" (# (p,x)) )

for b_{1}, b_{2} being Element of L st ex p being one-to-one FinSequence of I st

( rng p = J & b_{1} = the multF of L "**" (# (p,x)) ) & ex p being one-to-one FinSequence of I st

( rng p = J & b_{2} = the multF of L "**" (# (p,x)) ) holds

b_{1} = b_{2}

end;
let L be commutative TopGroup;

let x be the carrier of L -valued ManySortedSet of I;

let J be Element of Fin I;

func Product (x,J) -> Element of L means :Def2: :: CARDFIL3:def 6

ex p being one-to-one FinSequence of I st

( rng p = J & it = the multF of L "**" (# (p,x)) );

existence ex p being one-to-one FinSequence of I st

( rng p = J & it = the multF of L "**" (# (p,x)) );

ex b

( rng p = J & b

proof end;

uniqueness for b

( rng p = J & b

( rng p = J & b

b

proof end;

:: deftheorem Def2 defines Product CARDFIL3:def 6 :

for I being non empty set

for L being commutative TopGroup

for x being the carrier of b_{2} -valued ManySortedSet of I

for J being Element of Fin I

for b_{5} being Element of L holds

( b_{5} = Product (x,J) iff ex p being one-to-one FinSequence of I st

( rng p = J & b_{5} = the multF of L "**" (# (p,x)) ) );

for I being non empty set

for L being commutative TopGroup

for x being the carrier of b

for J being Element of Fin I

for b

( b

( rng p = J & b

theorem Th11: :: CARDFIL3:35

for I being set

for G being TopGroup

for f being Function of ([#] (OrderedFIN I)), the carrier of G

for x being Point of G

for B being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_f f iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

f . j in b )

for G being TopGroup

for f being Function of ([#] (OrderedFIN I)), the carrier of G

for x being Point of G

for B being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_f f iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

f . j in b )

proof end;

theorem :: CARDFIL3:36

for I being non empty set

for L being commutative TopGroup

for x being the carrier of b_{2} -valued ManySortedSet of I

for J, e being Element of Fin I st e = {} holds

( Product (x,e) = 1_ L & ( for e, f being Element of Fin I st e misses f holds

Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) ) )

for L being commutative TopGroup

for x being the carrier of b

for J, e being Element of Fin I st e = {} holds

( Product (x,e) = 1_ L & ( for e, f being Element of Fin I st e misses f holds

Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) ) )

proof end;

definition

let I be non empty set ;

let L be commutative TopGroup;

let x be the carrier of L -valued ManySortedSet of I;

ex b_{1} being Function of ([#] (OrderedFIN I)), the carrier of L st

for j being Element of Fin I holds b_{1} . j = Product (x,j)

for b_{1}, b_{2} being Function of ([#] (OrderedFIN I)), the carrier of L st ( for j being Element of Fin I holds b_{1} . j = Product (x,j) ) & ( for j being Element of Fin I holds b_{2} . j = Product (x,j) ) holds

b_{1} = b_{2}

end;
let L be commutative TopGroup;

let x be the carrier of L -valued ManySortedSet of I;

func Partial_Product x -> Function of ([#] (OrderedFIN I)), the carrier of L means :: CARDFIL3:def 7

for j being Element of Fin I holds it . j = Product (x,j);

existence for j being Element of Fin I holds it . j = Product (x,j);

ex b

for j being Element of Fin I holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines Partial_Product CARDFIL3:def 7 :

for I being non empty set

for L being commutative TopGroup

for x being the carrier of b_{2} -valued ManySortedSet of I

for b_{4} being Function of ([#] (OrderedFIN I)), the carrier of L holds

( b_{4} = Partial_Product x iff for j being Element of Fin I holds b_{4} . j = Product (x,j) );

for I being non empty set

for L being commutative TopGroup

for x being the carrier of b

for b

( b

theorem :: CARDFIL3:37

for I being non empty set

for G being commutative TopGroup

for s being the carrier of b_{2} -valued ManySortedSet of I

for x being Point of G

for B being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_f (Partial_Product s) iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

(Partial_Product s) . j in b ) by Th11;

for G being commutative TopGroup

for s being the carrier of b

for x being Point of G

for B being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_f (Partial_Product s) iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

(Partial_Product s) . j in b ) by Th11;

definition

let I be non empty set ;

let L be Abelian TopaddGroup;

let x be the carrier of L -valued ManySortedSet of I;

let J be Element of Fin I;

ex b_{1} being Element of L ex p being one-to-one FinSequence of I st

( rng p = J & b_{1} = the addF of L "**" (# (p,x)) )

for b_{1}, b_{2} being Element of L st ex p being one-to-one FinSequence of I st

( rng p = J & b_{1} = the addF of L "**" (# (p,x)) ) & ex p being one-to-one FinSequence of I st

( rng p = J & b_{2} = the addF of L "**" (# (p,x)) ) holds

b_{1} = b_{2}

end;
let L be Abelian TopaddGroup;

let x be the carrier of L -valued ManySortedSet of I;

let J be Element of Fin I;

func Sum (x,J) -> Element of L means :Def3: :: CARDFIL3:def 8

ex p being one-to-one FinSequence of I st

( rng p = J & it = the addF of L "**" (# (p,x)) );

existence ex p being one-to-one FinSequence of I st

( rng p = J & it = the addF of L "**" (# (p,x)) );

ex b

( rng p = J & b

proof end;

uniqueness for b

( rng p = J & b

( rng p = J & b

b

proof end;

:: deftheorem Def3 defines Sum CARDFIL3:def 8 :

for I being non empty set

for L being Abelian TopaddGroup

for x being the carrier of b_{2} -valued ManySortedSet of I

for J being Element of Fin I

for b_{5} being Element of L holds

( b_{5} = Sum (x,J) iff ex p being one-to-one FinSequence of I st

( rng p = J & b_{5} = the addF of L "**" (# (p,x)) ) );

for I being non empty set

for L being Abelian TopaddGroup

for x being the carrier of b

for J being Element of Fin I

for b

( b

( rng p = J & b

theorem Th12: :: CARDFIL3:38

for I being set

for G being TopaddGroup

for f being Function of ([#] (OrderedFIN I)), the carrier of G

for x being Point of G

for B being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_f f iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

f . j in b )

for G being TopaddGroup

for f being Function of ([#] (OrderedFIN I)), the carrier of G

for x being Point of G

for B being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_f f iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

f . j in b )

proof end;

theorem :: CARDFIL3:39

for I being non empty set

for L being Abelian TopaddGroup

for x being the carrier of b_{2} -valued ManySortedSet of I

for J, e being Element of Fin I st e = {} holds

( Sum (x,e) = 0_ L & ( for e, f being Element of Fin I st e misses f holds

Sum (x,(e \/ f)) = (Sum (x,e)) + (Sum (x,f)) ) )

for L being Abelian TopaddGroup

for x being the carrier of b

for J, e being Element of Fin I st e = {} holds

( Sum (x,e) = 0_ L & ( for e, f being Element of Fin I st e misses f holds

Sum (x,(e \/ f)) = (Sum (x,e)) + (Sum (x,f)) ) )

proof end;

definition

let I be non empty set ;

let L be Abelian TopaddGroup;

let x be the carrier of L -valued ManySortedSet of I;

ex b_{1} being Function of ([#] (OrderedFIN I)), the carrier of L st

for j being Element of Fin I holds b_{1} . j = Sum (x,j)

for b_{1}, b_{2} being Function of ([#] (OrderedFIN I)), the carrier of L st ( for j being Element of Fin I holds b_{1} . j = Sum (x,j) ) & ( for j being Element of Fin I holds b_{2} . j = Sum (x,j) ) holds

b_{1} = b_{2}

end;
let L be Abelian TopaddGroup;

let x be the carrier of L -valued ManySortedSet of I;

func Partial_Sums x -> Function of ([#] (OrderedFIN I)), the carrier of L means :: CARDFIL3:def 9

for j being Element of Fin I holds it . j = Sum (x,j);

existence for j being Element of Fin I holds it . j = Sum (x,j);

ex b

for j being Element of Fin I holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines Partial_Sums CARDFIL3:def 9 :

for I being non empty set

for L being Abelian TopaddGroup

for x being the carrier of b_{2} -valued ManySortedSet of I

for b_{4} being Function of ([#] (OrderedFIN I)), the carrier of L holds

( b_{4} = Partial_Sums x iff for j being Element of Fin I holds b_{4} . j = Sum (x,j) );

for I being non empty set

for L being Abelian TopaddGroup

for x being the carrier of b

for b

( b

theorem :: CARDFIL3:40

for I being non empty set

for G being Abelian TopaddGroup

for s being the carrier of b_{2} -valued ManySortedSet of I

for x being Point of G

for B being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_f (Partial_Sums s) iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

(Partial_Sums s) . j in b ) by Th12;

for G being Abelian TopaddGroup

for s being the carrier of b

for x being Point of G

for B being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_f (Partial_Sums s) iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

(Partial_Sums s) . j in b ) by Th12;