:: by Roland Coghetto

::

:: Received April 19, 2015

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

Thm01: for X1, X2, X3, X4 being set holds

( ((X1 /\ X4) \ (X2 \/ X3)) /\ (X1 \ ((X2 \/ X3) \/ X4)) is empty & ((X1 /\ X4) \ (X2 \/ X3)) /\ (((X1 /\ X3) /\ X4) \ X2) is empty & (X1 \ ((X2 \/ X3) \/ X4)) /\ (((X1 /\ X3) /\ X4) \ X2) is empty )

proof end;

theorem :: SRINGS_4:1

Lm1: for X1, X2, X3, X4 being set holds X1 \ (X2 \/ X3) c= (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)

proof end;

Lm2: for X1, X2, X3, X4 being set holds (X1 /\ X4) \ X2 c= (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)

proof end;

Lm3: for X1, X2, X3, X4 being set holds ((X1 /\ X3) /\ X4) \ X2 c= (X1 /\ X4) \ X2

proof end;

theorem Thm03: :: SRINGS_4:3

for X1, X2, X3, X4 being set holds (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) = (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)

proof end;

theorem Thm04: :: SRINGS_4:4

for X1, X2, X3, X4 being set holds (X1 \ X2) \ (X3 \ X4) = (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)

proof end;

theorem Thm07: :: SRINGS_4:6

for T, S being set

for f being Function of T,S

for G being Subset-Family of T holds f .: G = { (f .: A) where A is Subset of T : A in G }

for f being Function of T,S

for G being Subset-Family of T holds f .: G = { (f .: A) where A is Subset of T : A in G }

proof end;

registration

let T, S be set ;

let f be Function of T,S;

let G be finite Subset-Family of T;

coherence

f .: G is finite

end;
let f be Function of T,S;

let G be finite Subset-Family of T;

coherence

f .: G is finite

proof end;

registration
end;

registration

let T, S be set ;

let f be Function of T,S;

let G be countable Subset-Family of T;

coherence

f .: G is countable

end;
let f be Function of T,S;

let G be countable Subset-Family of T;

coherence

f .: G is countable

proof end;

Thm08: for X, Y being set

for S being with_empty_element Subset-Family of X

for f being Function of X,Y holds f .: S is with_empty_element Subset-Family of Y

proof end;

registration

let X, Y be set ;

let S be with_empty_element Subset-Family of X;

let f be Function of X,Y;

coherence

not f .: S is with_non-empty_elements by Thm08;

end;
let S be with_empty_element Subset-Family of X;

let f be Function of X,Y;

coherence

not f .: S is with_non-empty_elements by Thm08;

theorem :: SRINGS_4:7

for X, Y being set

for f being Function of X,Y

for SF1, SF2 being Subset-Family of X st SF1 c= SF2 holds

f .: SF1 c= f .: SF2

for f being Function of X,Y

for SF1, SF2 being Subset-Family of X st SF1 c= SF2 holds

f .: SF1 c= f .: SF2

proof end;

theorem Thm10: :: SRINGS_4:8

for X, Y being set

for S being cap-closed Subset-Family of X

for f being Function of X,Y st f is one-to-one holds

f .: S is cap-closed Subset-Family of Y

for S being cap-closed Subset-Family of X

for f being Function of X,Y st f is one-to-one holds

f .: S is cap-closed Subset-Family of Y

proof end;

theorem Thm11: :: SRINGS_4:9

for X, Y being non empty set

for S being cap-finite-partition-closed Subset-Family of X

for f being Function of X,Y st f is one-to-one holds

f .: S is cap-finite-partition-closed Subset-Family of Y

for S being cap-finite-partition-closed Subset-Family of X

for f being Function of X,Y st f is one-to-one holds

f .: S is cap-finite-partition-closed Subset-Family of Y

proof end;

theorem Thm12: :: SRINGS_4:10

for X, Y being non empty set

for S being diff-c=-finite-partition-closed Subset-Family of X

for f being Function of X,Y st f is one-to-one & not f .: S is empty holds

f .: S is diff-c=-finite-partition-closed Subset-Family of Y

for S being diff-c=-finite-partition-closed Subset-Family of X

for f being Function of X,Y st f is one-to-one & not f .: S is empty holds

f .: S is diff-c=-finite-partition-closed Subset-Family of Y

proof end;

theorem :: SRINGS_4:11

for X, Y being non empty set

for S being diff-finite-partition-closed Subset-Family of X

for f being Function of X,Y st f is one-to-one holds

f .: S is diff-finite-partition-closed Subset-Family of Y

for S being diff-finite-partition-closed Subset-Family of X

for f being Function of X,Y st f is one-to-one holds

f .: S is diff-finite-partition-closed Subset-Family of Y

proof end;

theorem :: SRINGS_4:12

for X, Y being non empty set

for S being semiring_of_sets of X

for f being Function of X,Y st f is one-to-one holds

f .: S is semiring_of_sets of Y by Thm11, Thm12;

for S being semiring_of_sets of X

for f being Function of X,Y st f is one-to-one holds

f .: S is semiring_of_sets of Y by Thm11, Thm12;

theorem Thm13: :: SRINGS_4:13

for X being 1 -element FinSequence st not X . 1 is empty holds

ex I being Function of (X . 1),(product X) st

( I is one-to-one & I is onto & ( for x being object st x in X . 1 holds

I . x = <*x*> ) )

ex I being Function of (X . 1),(product X) st

( I is one-to-one & I is onto & ( for x being object st x in X . 1 holds

I . x = <*x*> ) )

proof end;

registration
end;

registration

let X be set ;

existence

ex b_{1} being cap-closed Subset-Family of X st b_{1} is with_empty_element

end;
existence

ex b

proof end;

registration

let X be set ;

ex b_{1} being cap-closed with_empty_element Subset-Family of X st b_{1} is cup-closed

end;
cluster non empty cup-closed cap-closed V22() cap-finite-partition-closed with_empty_element for Subset-Family of X;

existence ex b

proof end;

registration
end;

theorem LemY: :: SRINGS_4:14

for X being set

for S being with_empty_element Subset-Family of X holds DIFFERENCE (S,S) = { (A \ B) where A, B is Element of S : verum }

for S being with_empty_element Subset-Family of X holds DIFFERENCE (S,S) = { (A \ B) where A, B is Element of S : verum }

proof end;

definition

let X be set ;

let S be with_empty_element Subset-Family of X;

coherence

DIFFERENCE (S,S) is Subset-Family of X

end;
let S be with_empty_element Subset-Family of X;

coherence

DIFFERENCE (S,S) is Subset-Family of X

proof end;

:: deftheorem defines semidiff SRINGS_4:def 1 :

for X being set

for S being with_empty_element Subset-Family of X holds semidiff S = DIFFERENCE (S,S);

for X being set

for S being with_empty_element Subset-Family of X holds semidiff S = DIFFERENCE (S,S);

theorem LemX1: :: SRINGS_4:15

for X being set

for S being with_empty_element Subset-Family of X

for x being object st x in semidiff S holds

ex A, B being Element of S st x = A \ B

for S being with_empty_element Subset-Family of X

for x being object st x in semidiff S holds

ex A, B being Element of S st x = A \ B

proof end;

registration

let X be set ;

let S be with_empty_element Subset-Family of X;

coherence

not semidiff S is with_non-empty_elements

end;
let S be with_empty_element Subset-Family of X;

coherence

not semidiff S is with_non-empty_elements

proof end;

Thm14: for X being set

for S being cup-closed cap-closed with_empty_element Subset-Family of X holds

( semidiff S is cap-closed & semidiff S is diff-finite-partition-closed )

proof end;

registration

let X be set ;

let S be cup-closed cap-closed with_empty_element Subset-Family of X;

coherence

( semidiff S is cap-closed & semidiff S is diff-finite-partition-closed ) by Thm14;

end;
let S be cup-closed cap-closed with_empty_element Subset-Family of X;

coherence

( semidiff S is cap-closed & semidiff S is diff-finite-partition-closed ) by Thm14;

theorem :: SRINGS_4:16

for X being set

for S being cup-closed cap-closed with_empty_element Subset-Family of X holds semidiff S is semiring_of_sets of X ;

for S being cup-closed cap-closed with_empty_element Subset-Family of X holds semidiff S is semiring_of_sets of X ;

definition

let T be non empty TopSpace;

{ (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } is Subset-Family of ([#] T)

end;
func capOpCl T -> Subset-Family of ([#] T) equals :: SRINGS_4:def 2

{ (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } ;

coherence { (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } ;

{ (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } is Subset-Family of ([#] T)

proof end;

:: deftheorem defines capOpCl SRINGS_4:def 2 :

for T being non empty TopSpace holds capOpCl T = { (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } ;

for T being non empty TopSpace holds capOpCl T = { (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } ;

Thm15: for T being non empty TopSpace holds

( capOpCl T is with_empty_element & capOpCl T is cap-closed & capOpCl T is diff-finite-partition-closed )

proof end;

registration

let T be non empty TopSpace;

coherence

( not capOpCl T is with_non-empty_elements & capOpCl T is cap-closed & capOpCl T is diff-finite-partition-closed ) by Thm15;

end;
coherence

( not capOpCl T is with_non-empty_elements & capOpCl T is cap-closed & capOpCl T is diff-finite-partition-closed ) by Thm15;

theorem :: SRINGS_4:17

registration

let n be Nat;

ex b_{1} being n -element FinSequence st b_{1} is non-empty

end;
cluster Relation-like non-empty K42() -defined Function-like finite n -element FinSequence-like FinSubsequence-like countable for FinSequence;

existence ex b

proof end;

definition

let n be non zero Nat;

let X be non-empty n -element FinSequence;

ex b_{1} being n -element FinSequence st

for i being Nat st i in Seg n holds

b_{1} . i is semiring_of_sets of (X . i)

end;
let X be non-empty n -element FinSequence;

mode SemiringFamily of X -> n -element FinSequence means :Def2: :: SRINGS_4:def 3

for i being Nat st i in Seg n holds

it . i is semiring_of_sets of (X . i);

existence for i being Nat st i in Seg n holds

it . i is semiring_of_sets of (X . i);

ex b

for i being Nat st i in Seg n holds

b

proof end;

:: deftheorem Def2 defines SemiringFamily SRINGS_4:def 3 :

for n being non zero Nat

for X being non-empty b_{1} -element FinSequence

for b_{3} being b_{1} -element FinSequence holds

( b_{3} is SemiringFamily of X iff for i being Nat st i in Seg n holds

b_{3} . i is semiring_of_sets of (X . i) );

for n being non zero Nat

for X being non-empty b

for b

( b

b

theorem Thm16: :: SRINGS_4:18

for n being non zero Nat

for X being non-empty b_{1} -element FinSequence

for S being SemiringFamily of X holds dom S = dom X

for X being non-empty b

for S being SemiringFamily of X holds dom S = dom X

proof end;

theorem Thm17: :: SRINGS_4:19

for n being non zero Nat

for X being non-empty b_{1} -element FinSequence

for S being SemiringFamily of X

for i being Nat st i in Seg n holds

union (S . i) c= X . i

for X being non-empty b

for S being SemiringFamily of X

for i being Nat st i in Seg n holds

union (S . i) c= X . i

proof end;

theorem Thm18: :: SRINGS_4:20

for n being non zero Nat

for f being Function

for X being b_{1} -element FinSequence st f in product X holds

f is b_{1} -element FinSequence

for f being Function

for X being b

f is b

proof end;

definition

let n be non zero Nat;

let X be n -element FinSequence;

ex b_{1} being set st

for f being object holds

( f in b_{1} iff ex g being Function st

( f = product g & g in product X ) )

for b_{1}, b_{2} being set st ( for f being object holds

( f in b_{1} iff ex g being Function st

( f = product g & g in product X ) ) ) & ( for f being object holds

( f in b_{2} iff ex g being Function st

( f = product g & g in product X ) ) ) holds

b_{1} = b_{2}

end;
let X be n -element FinSequence;

func SemiringProduct X -> set means :Def3: :: SRINGS_4:def 4

for f being object holds

( f in it iff ex g being Function st

( f = product g & g in product X ) );

existence for f being object holds

( f in it iff ex g being Function st

( f = product g & g in product X ) );

ex b

for f being object holds

( f in b

( f = product g & g in product X ) )

proof end;

uniqueness for b

( f in b

( f = product g & g in product X ) ) ) & ( for f being object holds

( f in b

( f = product g & g in product X ) ) ) holds

b

proof end;

:: deftheorem Def3 defines SemiringProduct SRINGS_4:def 4 :

for n being non zero Nat

for X being b_{1} -element FinSequence

for b_{3} being set holds

( b_{3} = SemiringProduct X iff for f being object holds

( f in b_{3} iff ex g being Function st

( f = product g & g in product X ) ) );

for n being non zero Nat

for X being b

for b

( b

( f in b

( f = product g & g in product X ) ) );

theorem Thm19: :: SRINGS_4:21

for n being non zero Nat

for X being b_{1} -element FinSequence holds SemiringProduct X c= bool (Funcs ((dom X),(union (Union X))))

for X being b

proof end;

theorem Thm20: :: SRINGS_4:22

for n being non zero Nat

for X being non-empty b_{1} -element FinSequence

for S being SemiringFamily of X holds SemiringProduct S is Subset-Family of (product X)

for X being non-empty b

for S being SemiringFamily of X holds SemiringProduct S is Subset-Family of (product X)

proof end;

theorem Thm21: :: SRINGS_4:23

for X being non-empty 1 -element FinSequence holds product X = { <*x*> where x is Element of X . 1 : verum }

proof end;

Thm22: product <*{}*> is empty

proof end;

theorem Thm24: :: SRINGS_4:25

for X being non-empty 1 -element FinSequence

for S being SemiringFamily of X holds SemiringProduct S = { (product <*s*>) where s is Element of S . 1 : verum }

for S being SemiringFamily of X holds SemiringProduct S = { (product <*s*>) where s is Element of S . 1 : verum }

proof end;

theorem Thm27: :: SRINGS_4:28

for X being non-empty 1 -element FinSequence

for S being SemiringFamily of X holds { (product <*s*>) where s is Element of S . 1 : verum } is semiring_of_sets of { <*x*> where x is Element of X . 1 : verum }

for S being SemiringFamily of X holds { (product <*s*>) where s is Element of S . 1 : verum } is semiring_of_sets of { <*x*> where x is Element of X . 1 : verum }

proof end;

theorem Thm28: :: SRINGS_4:29

for X being non-empty 1 -element FinSequence

for S being SemiringFamily of X holds SemiringProduct S is semiring_of_sets of (product X)

for S being SemiringFamily of X holds SemiringProduct S is semiring_of_sets of (product X)

proof end;

theorem Thm29: :: SRINGS_4:30

for X1, X2 being set

for S1 being semiring_of_sets of X1

for S2 being semiring_of_sets of X2 holds { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is semiring_of_sets of [:X1,X2:]

for S1 being semiring_of_sets of X1

for S2 being semiring_of_sets of X2 holds { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is semiring_of_sets of [:X1,X2:]

proof end;

theorem Thm30: :: SRINGS_4:31

for n being non zero Nat

for Xn being non-empty b_{1} -element FinSequence

for X1 being non-empty 1 -element FinSequence

for Sn being SemiringFamily of Xn

for S1 being SemiringFamily of X1 st SemiringProduct Sn is semiring_of_sets of (product Xn) & SemiringProduct S1 is semiring_of_sets of (product X1) holds

for S12 being Subset-Family of [:(product Xn),(product X1):] st S12 = { [:s1,s2:] where s1 is Element of SemiringProduct Sn, s2 is Element of SemiringProduct S1 : verum } holds

ex I being Function of [:(product Xn),(product X1):],(product (Xn ^ X1)) st

( I is one-to-one & I is onto & ( for x, y being FinSequence st x in product Xn & y in product X1 holds

I . (x,y) = x ^ y ) & I .: S12 = SemiringProduct (Sn ^ S1) )

for Xn being non-empty b

for X1 being non-empty 1 -element FinSequence

for Sn being SemiringFamily of Xn

for S1 being SemiringFamily of X1 st SemiringProduct Sn is semiring_of_sets of (product Xn) & SemiringProduct S1 is semiring_of_sets of (product X1) holds

for S12 being Subset-Family of [:(product Xn),(product X1):] st S12 = { [:s1,s2:] where s1 is Element of SemiringProduct Sn, s2 is Element of SemiringProduct S1 : verum } holds

ex I being Function of [:(product Xn),(product X1):],(product (Xn ^ X1)) st

( I is one-to-one & I is onto & ( for x, y being FinSequence st x in product Xn & y in product X1 holds

I . (x,y) = x ^ y ) & I .: S12 = SemiringProduct (Sn ^ S1) )

proof end;

theorem Thm31: :: SRINGS_4:32

for n being non zero Nat

for Xn being non-empty b_{1} -element FinSequence

for X1 being non-empty 1 -element FinSequence

for Sn being SemiringFamily of Xn

for S1 being SemiringFamily of X1 st SemiringProduct Sn is semiring_of_sets of (product Xn) & SemiringProduct S1 is semiring_of_sets of (product X1) holds

SemiringProduct (Sn ^ S1) is semiring_of_sets of (product (Xn ^ X1))

for Xn being non-empty b

for X1 being non-empty 1 -element FinSequence

for Sn being SemiringFamily of Xn

for S1 being SemiringFamily of X1 st SemiringProduct Sn is semiring_of_sets of (product Xn) & SemiringProduct S1 is semiring_of_sets of (product X1) holds

SemiringProduct (Sn ^ S1) is semiring_of_sets of (product (Xn ^ X1))

proof end;

:: Product of n semiring of sets is semiring of sets

theorem Thm32: :: SRINGS_4:33

for n being non zero Nat

for X being non-empty b_{1} -element FinSequence

for S being SemiringFamily of X holds SemiringProduct S is semiring_of_sets of (product X)

for X being non-empty b

for S being SemiringFamily of X holds SemiringProduct S is semiring_of_sets of (product X)

proof end;

definition

let n be non zero Nat;

let X be non-empty n -element FinSequence;

let S be SemiringFamily of X;

end;
let X be non-empty n -element FinSequence;

let S be SemiringFamily of X;

attr S is cap-closed-yielding means :Def4: :: SRINGS_4:def 5

for i being Nat st i in Seg n holds

S . i is cap-closed ;

for i being Nat st i in Seg n holds

S . i is cap-closed ;

:: deftheorem Def4 defines cap-closed-yielding SRINGS_4:def 5 :

for n being non zero Nat

for X being non-empty b_{1} -element FinSequence

for S being SemiringFamily of X holds

( S is cap-closed-yielding iff for i being Nat st i in Seg n holds

S . i is cap-closed );

for n being non zero Nat

for X being non-empty b

for S being SemiringFamily of X holds

( S is cap-closed-yielding iff for i being Nat st i in Seg n holds

S . i is cap-closed );

registration

let n be non zero Nat;

let X be non-empty n -element FinSequence;

ex b_{1} being SemiringFamily of X st b_{1} is cap-closed-yielding

end;
let X be non-empty n -element FinSequence;

cluster non empty Relation-like K42() -defined Function-like finite n -element FinSequence-like FinSubsequence-like countable cap-closed-yielding for SemiringFamily of X;

existence ex b

proof end;

registration

let X be set ;

ex b_{1} being semiring_of_sets of X st b_{1} is cap-closed

end;
cluster non empty cap-closed V22() cap-finite-partition-closed diff-finite-partition-closed diff-c=-finite-partition-closed non with_non-empty_elements for semiring_of_sets of ;

existence ex b

proof end;

theorem Thm33: :: SRINGS_4:34

for X being non-empty 1 -element FinSequence

for S being cap-closed-yielding SemiringFamily of X holds { (product <*s*>) where s is Element of S . 1 : verum } is cap-closed semiring_of_sets of { <*x*> where x is Element of X . 1 : verum }

for S being cap-closed-yielding SemiringFamily of X holds { (product <*s*>) where s is Element of S . 1 : verum } is cap-closed semiring_of_sets of { <*x*> where x is Element of X . 1 : verum }

proof end;

theorem Thm34: :: SRINGS_4:35

for X being non-empty 1 -element FinSequence

for S being cap-closed-yielding SemiringFamily of X holds SemiringProduct S is cap-closed semiring_of_sets of (product X)

for S being cap-closed-yielding SemiringFamily of X holds SemiringProduct S is cap-closed semiring_of_sets of (product X)

proof end;

theorem Thm35: :: SRINGS_4:36

for X1, X2 being set

for S1 being cap-closed semiring_of_sets of X1

for S2 being cap-closed semiring_of_sets of X2 holds { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is cap-closed semiring_of_sets of [:X1,X2:]

for S1 being cap-closed semiring_of_sets of X1

for S2 being cap-closed semiring_of_sets of X2 holds { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is cap-closed semiring_of_sets of [:X1,X2:]

proof end;

theorem Thm36: :: SRINGS_4:37

for n being non zero Nat

for Xn being non-empty b_{1} -element FinSequence

for X1 being non-empty 1 -element FinSequence

for Sn being cap-closed-yielding SemiringFamily of Xn

for S1 being cap-closed-yielding SemiringFamily of X1 st SemiringProduct Sn is cap-closed semiring_of_sets of (product Xn) & SemiringProduct S1 is cap-closed semiring_of_sets of (product X1) holds

SemiringProduct (Sn ^ S1) is cap-closed semiring_of_sets of (product (Xn ^ X1))

for Xn being non-empty b

for X1 being non-empty 1 -element FinSequence

for Sn being cap-closed-yielding SemiringFamily of Xn

for S1 being cap-closed-yielding SemiringFamily of X1 st SemiringProduct Sn is cap-closed semiring_of_sets of (product Xn) & SemiringProduct S1 is cap-closed semiring_of_sets of (product X1) holds

SemiringProduct (Sn ^ S1) is cap-closed semiring_of_sets of (product (Xn ^ X1))

proof end;

Thm37: for n being non zero Nat

for X being non-empty b

for S being cap-closed-yielding SemiringFamily of X holds SemiringProduct S is cap-closed

proof end;

registration

let n be non zero Nat;

let X be non-empty n -element FinSequence;

let S be cap-closed-yielding SemiringFamily of X;

coherence

SemiringProduct S is cap-closed by Thm37;

end;
let X be non-empty n -element FinSequence;

let S be cap-closed-yielding SemiringFamily of X;

coherence

SemiringProduct S is cap-closed by Thm37;

:: Product of n classical semirings of sets is classical semiring of sets

theorem :: SRINGS_4:38

for n being non zero Nat

for X being non-empty b_{1} -element FinSequence

for S being cap-closed-yielding SemiringFamily of X holds SemiringProduct S is cap-closed semiring_of_sets of (product X) by Thm32;

for X being non-empty b

for S being cap-closed-yielding SemiringFamily of X holds SemiringProduct S is cap-closed semiring_of_sets of (product X) by Thm32;

:: n-classical semiring of sets

definition

let n be non zero Nat;

let X be non-empty n -element FinSequence;

ex b_{1} being n -element FinSequence st

for i being Nat st i in Seg n holds

b_{1} . i is cap-closed with_empty_element semi-diff-closed Subset-Family of (X . i)

end;
let X be non-empty n -element FinSequence;

mode ClassicalSemiringFamily of X -> n -element FinSequence means :Def5: :: SRINGS_4:def 6

for i being Nat st i in Seg n holds

it . i is cap-closed with_empty_element semi-diff-closed Subset-Family of (X . i);

existence for i being Nat st i in Seg n holds

it . i is cap-closed with_empty_element semi-diff-closed Subset-Family of (X . i);

ex b

for i being Nat st i in Seg n holds

b

proof end;

:: deftheorem Def5 defines ClassicalSemiringFamily SRINGS_4:def 6 :

for n being non zero Nat

for X being non-empty b_{1} -element FinSequence

for b_{3} being b_{1} -element FinSequence holds

( b_{3} is ClassicalSemiringFamily of X iff for i being Nat st i in Seg n holds

b_{3} . i is cap-closed with_empty_element semi-diff-closed Subset-Family of (X . i) );

for n being non zero Nat

for X being non-empty b

for b

( b

b

notation

let n be non zero Nat;

let X be n -element FinSequence;

synonym MeasurableRectangle X for SemiringProduct X;

end;
let X be n -element FinSequence;

synonym MeasurableRectangle X for SemiringProduct X;

theorem Thm38: :: SRINGS_4:39

for n being non zero Nat

for X being non-empty b_{1} -element FinSequence

for S being ClassicalSemiringFamily of X holds S is cap-closed-yielding SemiringFamily of X

for X being non-empty b

for S being ClassicalSemiringFamily of X holds S is cap-closed-yielding SemiringFamily of X

proof end;

:: finite product of classical semiring of sets is classical semiring of sets ::

:: Version SRING_3 ::

:: Version SRING_3 ::

theorem :: SRINGS_4:40

for n being non zero Nat

for X being non-empty b_{1} -element FinSequence

for S being ClassicalSemiringFamily of X holds MeasurableRectangle S is cap-closed with_empty_element semi-diff-closed Subset-Family of (product X)

for X being non-empty b

for S being ClassicalSemiringFamily of X holds MeasurableRectangle S is cap-closed with_empty_element semi-diff-closed Subset-Family of (product X)

proof end;

:: { O1 \ O2 : O1 is open, O2 is open} is semiring of sets