srings_4.miz
begin
reserve X1,X2,X3,X4 for
set;
Thm01: (((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
thus (((X1
/\ X4)
\ (X2
\/ X3))
/\ (X1
\ ((X2
\/ X3)
\/ X4))) is
empty
proof
let t be
object;
assume t
in (((X1
/\ X4)
\ (X2
\/ X3))
/\ (X1
\ ((X2
\/ X3)
\/ X4)));
then t
in ((X1
/\ X4)
\ (X2
\/ X3)) & t
in (X1
\ ((X2
\/ X3)
\/ X4)) by
XBOOLE_0:def 4;
then t
in (X1
/\ X4) & not t
in (X2
\/ X3) & t
in X1 & not t
in ((X2
\/ X3)
\/ X4) by
XBOOLE_0:def 5;
then (t
in X1 & t
in X4) & not (t
in X2 & t
in X3) & t
in X1 & not ((t
in X2 or t
in X3) or t
in X4) by
XBOOLE_0:def 3,
XBOOLE_0:def 4;
hence contradiction;
end;
thus (((X1
/\ X4)
\ (X2
\/ X3))
/\ (((X1
/\ X3)
/\ X4)
\ X2)) is
empty
proof
let t be
object;
assume t
in (((X1
/\ X4)
\ (X2
\/ X3))
/\ (((X1
/\ X3)
/\ X4)
\ X2));
then t
in ((X1
/\ X4)
\ (X2
\/ X3)) & t
in (((X1
/\ X3)
/\ X4)
\ X2) by
XBOOLE_0:def 4;
then t
in (X1
/\ X4) & not t
in (X2
\/ X3) & t
in ((X1
/\ X3)
/\ X4) & not t
in X2 by
XBOOLE_0:def 5;
then t
in X1 & t
in X4 & not (t
in X2 or t
in X3) & t
in (X1
/\ X3) & t
in X4 & not t
in X2 by
XBOOLE_0:def 3,
XBOOLE_0:def 4;
hence contradiction by
XBOOLE_0:def 4;
end;
let t be
object;
assume t
in ((X1
\ ((X2
\/ X3)
\/ X4))
/\ (((X1
/\ X3)
/\ X4)
\ X2));
then t
in (X1
\ ((X2
\/ X3)
\/ X4)) & t
in (((X1
/\ X3)
/\ X4)
\ X2) by
XBOOLE_0:def 4;
then t
in X1 & not t
in ((X2
\/ X3)
\/ X4) & t
in ((X1
/\ X3)
/\ X4) & not t
in X2 by
XBOOLE_0:def 5;
then t
in X1 & not t
in (X2
\/ X3) & not t
in X4 & t
in (X1
/\ X3) & t
in X4 & not t
in X2 by
XBOOLE_0:def 3,
XBOOLE_0:def 4;
hence contradiction;
end;
theorem ::
SRINGS_4:1
((X1
/\ X4)
\ (X2
\/ X3))
misses (X1
\ ((X2
\/ X3)
\/ X4)) & ((X1
/\ X4)
\ (X2
\/ X3))
misses (((X1
/\ X3)
/\ X4)
\ X2) & (X1
\ ((X2
\/ X3)
\/ X4))
misses (((X1
/\ X3)
/\ X4)
\ X2) by
Thm01;
theorem ::
SRINGS_4:2
Thm02: ((X1
\ X2)
\ (X3
\ X4))
= ((X1
\ (X2
\/ X3))
\/ ((X1
/\ X4)
\ X2))
proof
hereby
let t be
object;
assume t
in ((X1
\ X2)
\ (X3
\ X4));
then t
in (X1
\ X2) & not t
in (X3
\ X4) by
XBOOLE_0:def 5;
then t
in X1 & not t
in X2 & ( not t
in X3 or t
in X4) by
XBOOLE_0:def 5;
then (t
in X1 & not (t
in X2 or t
in X3)) or t
in (X1
/\ X4) & not t
in X2 by
XBOOLE_0:def 4;
then (t
in X1 & not t
in (X2
\/ X3)) or t
in ((X1
/\ X4)
\ X2) by
XBOOLE_0:def 3,
XBOOLE_0:def 5;
then t
in (X1
\ (X2
\/ X3)) or t
in ((X1
/\ X4)
\ X2) by
XBOOLE_0:def 5;
hence t
in ((X1
\ (X2
\/ X3))
\/ ((X1
/\ X4)
\ X2)) by
XBOOLE_0:def 3;
end;
let t be
object;
assume t
in ((X1
\ (X2
\/ X3))
\/ ((X1
/\ X4)
\ X2));
then t
in (X1
\ (X2
\/ X3)) or t
in ((X1
/\ X4)
\ X2) by
XBOOLE_0:def 3;
then (t
in X1 & not t
in (X2
\/ X3)) or (t
in (X1
/\ X4) & not t
in X2) by
XBOOLE_0:def 5;
then (t
in X1 & not t
in X2 & not t
in X3) or (t
in X1 & t
in X4 & not t
in X2) by
XBOOLE_0:def 3,
XBOOLE_0:def 4;
then t
in (X1
\ X2) & not t
in (X3
\ X4) by
XBOOLE_0:def 5;
hence t
in ((X1
\ X2)
\ (X3
\ X4)) by
XBOOLE_0:def 5;
end;
Lm1: (X1
\ (X2
\/ X3))
c= ((((X1
/\ X4)
\ (X2
\/ X3))
\/ (X1
\ ((X2
\/ X3)
\/ X4)))
\/ (((X1
/\ X3)
/\ X4)
\ X2))
proof
let t be
object;
assume t
in (X1
\ (X2
\/ X3));
then t
in X1 & not t
in (X2
\/ X3) by
XBOOLE_0:def 5;
then (t
in X1 & t
in X4 & not (t
in X2 or t
in X3)) or (t
in X1 & not (t
in (X2
\/ X3) or t
in X4)) or (t
in (X1
/\ X3) & t
in X4 & not t
in X2) by
XBOOLE_0:def 3;
then (t
in (X1
/\ X4) & not (t
in (X2
\/ X3))) or (t
in X1 & not (t
in ((X2
\/ X3)
\/ X4))) or (t
in ((X1
/\ X3)
/\ X4) & not t
in X2) by
XBOOLE_0:def 3,
XBOOLE_0:def 4;
then t
in ((X1
/\ X4)
\ (X2
\/ X3)) or t
in (X1
\ ((X2
\/ X3)
\/ X4)) or t
in (((X1
/\ X3)
/\ X4)
\ X2) by
XBOOLE_0:def 5;
then t
in (((X1
/\ X4)
\ (X2
\/ X3))
\/ (X1
\ ((X2
\/ X3)
\/ X4))) or t
in (((X1
/\ X3)
/\ X4)
\ X2) by
XBOOLE_0:def 3;
hence thesis by
XBOOLE_0:def 3;
end;
Lm2: ((X1
/\ X4)
\ X2)
c= ((((X1
/\ X4)
\ (X2
\/ X3))
\/ (X1
\ ((X2
\/ X3)
\/ X4)))
\/ (((X1
/\ X3)
/\ X4)
\ X2))
proof
let t be
object;
assume t
in ((X1
/\ X4)
\ X2);
then (t
in X1 & t
in X4 & not t
in X2 & not t
in X3) or (t
in X1 & ( not t
in X2 & not t
in X3 & not t
in X4)) or (t
in X1 & t
in X3 & t
in X4 & not t
in X2) by
XBOOLE_0:def 4,
XBOOLE_0:def 5;
then (t
in X1 & t
in X4 & not (t
in X2 or t
in X3)) or (t
in X1 & not (t
in (X2
\/ X3) or t
in X4)) or (t
in (X1
/\ X3) & t
in X4 & not t
in X2) by
XBOOLE_0:def 3,
XBOOLE_0:def 4;
then (t
in (X1
/\ X4) & not (t
in (X2
\/ X3))) or (t
in X1 & not (t
in ((X2
\/ X3)
\/ X4))) or (t
in ((X1
/\ X3)
/\ X4) & not t
in X2) by
XBOOLE_0:def 3,
XBOOLE_0:def 4;
then t
in ((X1
/\ X4)
\ (X2
\/ X3)) or t
in (X1
\ ((X2
\/ X3)
\/ X4)) or t
in (((X1
/\ X3)
/\ X4)
\ X2) by
XBOOLE_0:def 5;
then t
in (((X1
/\ X4)
\ (X2
\/ X3))
\/ (X1
\ ((X2
\/ X3)
\/ X4))) or t
in (((X1
/\ X3)
/\ X4)
\ X2) by
XBOOLE_0:def 3;
hence thesis by
XBOOLE_0:def 3;
end;
Lm3: (((X1
/\ X3)
/\ X4)
\ X2)
c= ((X1
/\ X4)
\ X2)
proof
((X1
/\ X3)
/\ X4)
= ((X1
/\ X4)
/\ X3) by
XBOOLE_1: 16;
hence thesis by
XBOOLE_1: 17,
XBOOLE_1: 33;
end;
theorem ::
SRINGS_4:3
Thm03: ((X1
\ (X2
\/ X3))
\/ ((X1
/\ X4)
\ X2))
= ((((X1
/\ X4)
\ (X2
\/ X3))
\/ (X1
\ ((X2
\/ X3)
\/ X4)))
\/ (((X1
/\ X3)
/\ X4)
\ X2))
proof
set M1 = (X1
\ (X2
\/ X3));
set M2 = ((X1
/\ X4)
\ X2);
set M3 = ((X1
/\ X4)
\ (X2
\/ X3));
set M4 = (X1
\ ((X2
\/ X3)
\/ X4));
set M5 = (((X1
/\ X3)
/\ X4)
\ X2);
set Z = ((M3
\/ M4)
\/ M5);
M1
c= Z & M2
c= Z by
Lm1,
Lm2;
then (M1
\/ M2)
c= (Z
\/ Z) by
XBOOLE_1: 13;
hence (M1
\/ M2)
c= Z;
M3
c= M2 & M4
c= M1 & M5
c= M2 by
XBOOLE_1: 7,
XBOOLE_1: 34,
Lm3;
then (M3
\/ M4)
c= ((M1
\/ M2)
\/ (M1
\/ M2)) & M5
c= (M1
\/ M2) by
XBOOLE_1: 10,
XBOOLE_1: 13;
hence ((M3
\/ M4)
\/ M5)
c= (M1
\/ M2) by
XBOOLE_1: 13;
end;
theorem ::
SRINGS_4:4
Thm04: ((X1
\ X2)
\ (X3
\ X4))
= ((((X1
/\ X4)
\ (X2
\/ X3))
\/ (X1
\ ((X2
\/ X3)
\/ X4)))
\/ (((X1
/\ X3)
/\ X4)
\ X2))
proof
((X1
\ X2)
\ (X3
\ X4))
= ((X1
\ (X2
\/ X3))
\/ ((X1
/\ X4)
\ X2)) by
Thm02;
hence thesis by
Thm03;
end;
theorem ::
SRINGS_4:5
Thm05: (
union
{X1, X2, X3})
= ((X1
\/ X2)
\/ X3)
proof
thus (
union
{X1, X2, X3})
= (
union (
{X1, X2}
\/
{X3})) by
ENUMSET1: 3
.= ((
union
{X1, X2})
\/ (
union
{X3})) by
ZFMISC_1: 78
.= ((X1
\/ X2)
\/ (
union
{X3})) by
ZFMISC_1: 75
.= ((X1
\/ X2)
\/ X3);
end;
begin
theorem ::
SRINGS_4:6
Thm07: for T,S be
set, f be
Function of T, S, G be
Subset-Family of T holds (f
.: G)
= { (f
.: A) where A be
Subset of T : A
in G }
proof
let T,S be
set, f be
Function of T, S, G be
Subset-Family of T;
hereby
let t be
object;
assume
A1: t
in (f
.: G);
then
reconsider t1 = t as
Subset of S;
consider B be
Subset of T such that
A2: B
in G and
A3: t1
= (f
.: B) by
A1,
FUNCT_2:def 10;
thus t
in { (f
.: A) where A be
Subset of T : A
in G } by
A2,
A3;
end;
let t be
object;
assume t
in { (f
.: A) where A be
Subset of T : A
in G };
then
consider A be
Subset of T such that
A4: t
= (f
.: A) and
A5: A
in G;
thus t
in (f
.: G) by
A4,
A5,
FUNCT_2:def 10;
end;
registration
let T,S be
set, f be
Function of T, S, G be
finite
Subset-Family of T;
cluster (f
.: G) ->
finite;
coherence
proof
A1: G is
finite;
deffunc
F(
Element of (
bool T)) = (f
.: $1);
{
F(A) where A be
Element of (
bool T) : A
in G } is
finite from
FRAENKEL:sch 21(
A1);
hence thesis by
Thm07;
end;
end
registration
let f be
Function, A be
countable
set;
cluster (f
.: A) ->
countable;
coherence
proof
(
card (f
.: A))
c= (
card A) by
CARD_1: 67;
hence thesis by
WAYBEL12: 1;
end;
end
scheme ::
SRINGS_4:sch1
FraenkelCountable { A() ->
set , X() ->
set , F(
object) ->
set } :
{ F(w) where w be
Element of A() : w
in X() } is
countable
provided
A1: X() is
countable;
set M = { F(w) where w be
Element of A() : w
in X() };
per cases ;
suppose
A2: A() is
empty;
M
c=
{F({})}
proof
let x be
object;
assume x
in M;
then
consider w be
Element of A() such that
A3: x
= F(w) & w
in X();
w
=
{} by
A2,
SUBSET_1:def 1;
hence thesis by
A3,
TARSKI:def 1;
end;
hence thesis;
end;
suppose
A4: A() is non
empty;
consider f be
Function such that
A5: (
dom f)
= (X()
/\ A()) and
A6: for y be
object st y
in (X()
/\ A()) holds (f
. y)
= F(y) from
FUNCT_1:sch 3;
M
= (f
.: X())
proof
thus M
c= (f
.: X())
proof
let x be
object;
assume x
in M;
then
consider u be
Element of A() such that
A7: x
= F(u) and
A8: u
in X();
A9: u
in (
dom f) by
A4,
A5,
A8,
XBOOLE_0:def 4;
then (f
. u)
= F(u) by
A5,
A6;
hence thesis by
A7,
A8,
A9,
FUNCT_1:def 6;
end;
let x be
object;
assume x
in (f
.: X());
then
consider y be
object such that
A10: y
in (
dom f) and
A11: y
in X() and
A12: x
= (f
. y) by
FUNCT_1:def 6;
reconsider y as
Element of A() by
A5,
A10,
XBOOLE_0:def 4;
x
= F(y) by
A5,
A6,
A10,
A12;
hence thesis by
A11;
end;
hence thesis by
A1;
end;
end;
registration
let T,S be
set, f be
Function of T, S, G be
countable
Subset-Family of T;
cluster (f
.: G) ->
countable;
coherence
proof
A1: G is
countable;
deffunc
F(
Element of (
bool T)) = (f
.: $1);
{
F(A) where A be
Element of (
bool T) : A
in G } is
countable from
FraenkelCountable(
A1);
hence thesis by
Thm07;
end;
end
Thm08: for X,Y be
set, S be
with_empty_element
Subset-Family of X, f be
Function of X, Y holds (f
.: S) is
with_empty_element
Subset-Family of Y
proof
let X,Y be
set, S be
with_empty_element
Subset-Family of X, f be
Function of X, Y;
{} is
Subset of Y &
{} is
Subset of X &
{}
in S &
{}
= (f
.:
{} ) by
SETFAM_1:def 8;
then
{}
in (f
.: S) by
FUNCT_2:def 10;
hence thesis;
end;
registration
let X,Y be
set, S be
with_empty_element
Subset-Family of X, f be
Function of X, Y;
cluster (f
.: S) ->
with_empty_element;
coherence by
Thm08;
end
theorem ::
SRINGS_4:7
for X,Y be
set, f be
Function of X, Y, SF1,SF2 be
Subset-Family of X st SF1
c= SF2 holds (f
.: SF1)
c= (f
.: SF2)
proof
let X,Y be
set, f be
Function of X, Y, SF1,SF2 be
Subset-Family of X;
assume
A1: SF1
c= SF2;
A2: (f
.: SF1)
= { (f
.: A) where A be
Subset of X : A
in SF1 } & (f
.: SF2)
= { (f
.: A) where A be
Subset of X : A
in SF2 } by
Thm07;
let x be
object;
assume x
in (f
.: SF1);
then
consider A be
Subset of X such that
A3: x
= (f
.: A) and
A4: A
in SF1 by
A2;
thus x
in (f
.: SF2) by
A1,
A2,
A3,
A4;
end;
theorem ::
SRINGS_4:8
Thm10: for X,Y be
set, S be
cap-closed
Subset-Family of X, f be
Function of X, Y st f is
one-to-one holds (f
.: S) is
cap-closed
Subset-Family of Y
proof
let X,Y be
set, S be
cap-closed
Subset-Family of X, f be
Function of X, Y;
assume
A1: f is
one-to-one;
now
let s1,s2 be
set;
assume
A2: s1
in (f
.: S) & s2
in (f
.: S);
consider c1 be
Subset of X such that
A3: c1
in S and
A4: s1
= (f
.: c1) by
A2,
FUNCT_2:def 10;
consider c2 be
Subset of X such that
A5: c2
in S and
A6: s2
= (f
.: c2) by
A2,
FUNCT_2:def 10;
reconsider f12 = (f
.: (c1
/\ c2)) as
Subset of Y;
(c1
/\ c2)
in S by
A3,
A5,
FINSUB_1:def 2;
then f12
in (f
.: S) by
FUNCT_2:def 10;
hence (s1
/\ s2)
in (f
.: S) by
A1,
A4,
A6,
FUNCT_1: 62;
end;
hence thesis by
FINSUB_1:def 2;
end;
theorem ::
SRINGS_4:9
Thm11: for X,Y be non
empty
set, S be
cap-finite-partition-closed
Subset-Family of X, f be
Function of X, Y st f is
one-to-one holds (f
.: S) is
cap-finite-partition-closed
Subset-Family of Y
proof
let X,Y be non
empty
set, S be
cap-finite-partition-closed
Subset-Family of X, f be
Function of X, Y;
assume
A1: f is
one-to-one;
per cases ;
suppose (f
.: S) is
empty;
hence thesis;
end;
suppose
A2: (f
.: S) is non
empty;
reconsider fS = (f
.: S) as
Subset-Family of Y;
fS is
cap-finite-partition-closed
proof
let s1,s2 be
Element of fS;
assume
A3: (s1
/\ s2) is non
empty;
A4: s1
in fS by
A2;
consider c1 be
Subset of X such that
A5: c1
in S and
A6: s1
= (f
.: c1) by
A4,
FUNCT_2:def 10;
A7: s2
in fS by
A2;
consider c2 be
Subset of X such that
A8: c2
in S and
A9: s2
= (f
.: c2) by
A7,
FUNCT_2:def 10;
A10: (f
.: (c1
/\ c2))
= (s1
/\ s2) by
A1,
A6,
A9,
FUNCT_1: 62;
then
A11: (c1
/\ c2) is non
empty by
A3;
consider x1 be
finite
Subset of S such that
A12: x1 is
a_partition of (c1
/\ c2) by
A5,
A8,
A11,
SRINGS_1:def 1;
x1
c= S & S
c= (
bool X);
then x1
c= (
bool X);
then
reconsider x2 = x1 as
Subset-Family of X;
now
thus (f
.: x2) is
finite
Subset of fS by
FUNCT_2: 103;
thus (f
.: x2) is
a_partition of (s1
/\ s2)
proof
now
(f
.: x2)
c= (
bool (s1
/\ s2))
proof
let t be
object;
assume t
in (f
.: x2);
then
consider y1 be
Subset of X such that
A13: y1
in x2 and
A14: t
= (f
.: y1) by
FUNCT_2:def 10;
reconsider t1 = t as
set by
A14;
(f
.: y1)
c= (f
.: (c1
/\ c2)) by
A12,
A13,
RELAT_1: 123;
then t1
c= (s1
/\ s2) by
A14,
A1,
A6,
A9,
FUNCT_1: 62;
hence t
in (
bool (s1
/\ s2));
end;
hence (f
.: x2) is
Subset-Family of (s1
/\ s2);
now
hereby
let t be
object;
assume t
in (
union (f
.: x2));
then
consider u be
set such that
A15: t
in u and
A16: u
in (f
.: x2) by
TARSKI:def 4;
consider v be
Subset of X such that
A17: v
in x2 and
A18: u
= (f
.: v) by
A16,
FUNCT_2:def 10;
(f
.: v)
c= (f
.: (c1
/\ c2)) by
A12,
A17,
RELAT_1: 123;
hence t
in (s1
/\ s2) by
A15,
A18,
A10;
end;
let t be
object;
assume t
in (s1
/\ s2);
then t
in (f
.: (c1
/\ c2)) by
A1,
A6,
A9,
FUNCT_1: 62;
then
consider v be
object such that
A19: v
in (
dom f) and
A20: v
in (c1
/\ c2) and
A21: t
= (f
. v) by
FUNCT_1:def 6;
v
in (
union x1) by
A12,
A20,
EQREL_1:def 4;
then
consider u be
set such that
A22: v
in u and
A23: u
in x1 by
TARSKI:def 4;
reconsider fu = (f
.: u) as
Subset of Y;
(f
. v)
in (f
.: u) & (f
.: u)
in (f
.: x2) by
A19,
A22,
FUNCT_1:def 6,
A23,
FUNCT_2:def 10;
hence t
in (
union (f
.: x2)) by
A21,
TARSKI:def 4;
end;
hence (
union (f
.: x2))
= (s1
/\ s2) by
TARSKI:def 3;
now
let A be
Subset of (s1
/\ s2);
assume A
in (f
.: x2);
then
consider a0 be
Subset of X such that
A26: a0
in x2 and
A27: A
= (f
.: a0) by
FUNCT_2:def 10;
thus A
<>
{}
proof
assume
A28: A
=
{} ;
(
dom f)
= X by
PARTFUN1:def 2;
hence contradiction by
A26,
A12,
A28,
A27;
end;
let B be
Subset of (s1
/\ s2);
assume B
in (f
.: x2);
then
consider b0 be
Subset of X such that
A29: b0
in x2 and
A30: B
= (f
.: b0) by
FUNCT_2:def 10;
thus A
= B or A
misses B by
A26,
A29,
A12,
EQREL_1:def 4,
A27,
A30,
A1,
FUNCT_1: 66;
end;
hence for A be
Subset of (s1
/\ s2) st A
in (f
.: x2) holds A
<>
{} & for B be
Subset of (s1
/\ s2) st B
in (f
.: x2) holds A
= B or A
misses B;
end;
hence thesis by
EQREL_1:def 4;
end;
end;
hence ex x be
finite
Subset of fS st x is
a_partition of (s1
/\ s2);
end;
hence thesis;
end;
end;
theorem ::
SRINGS_4:10
Thm12: for X,Y be non
empty
set, S be
diff-c=-finite-partition-closed
Subset-Family of X, f be
Function of X, Y st f is
one-to-one & (f
.: S) is non
empty holds (f
.: S) is
diff-c=-finite-partition-closed
Subset-Family of Y
proof
let X,Y be non
empty
set, S be
diff-c=-finite-partition-closed
Subset-Family of X, f be
Function of X, Y;
assume that
A1: f is
one-to-one and
A2: (f
.: S) is non
empty;
reconsider fS = (f
.: S) as
Subset-Family of Y;
fS is
diff-c=-finite-partition-closed
proof
let s1,s2 be
Element of fS;
assume
A3: s2
c= s1;
s1
in fS by
A2;
then
consider c1 be
Subset of X such that
A4: c1
in S and
A5: s1
= (f
.: c1) by
FUNCT_2:def 10;
s2
in fS by
A2;
then
consider c2 be
Subset of X such that
A6: c2
in S and
A7: s2
= (f
.: c2) by
FUNCT_2:def 10;
A8: (f
.: (c1
\ c2))
= (s1
\ s2) by
A1,
A5,
A7,
FUNCT_1: 64;
(
dom f)
= X by
PARTFUN1:def 2;
then
consider y1 be
finite
Subset of S such that
A9: y1 is
a_partition of (c1
\ c2) by
A3,
A5,
A7,
A1,
FUNCT_1: 87,
A4,
A6,
SRINGS_1:def 3;
y1
c= S & S
c= (
bool X);
then y1
c= (
bool X);
then
reconsider y2 = y1 as
Subset-Family of X;
thus ex x be
finite
Subset of fS st x is
a_partition of (s1
\ s2)
proof
reconsider fy = (f
.: y2) as
finite
Subset of fS by
FUNCT_2: 103;
take fy;
now
(f
.: y2)
c= (
bool (s1
\ s2))
proof
let t be
object;
assume t
in (f
.: y2);
then
consider z1 be
Subset of X such that
A10: z1
in y2 and
A11: t
= (f
.: z1) by
FUNCT_2:def 10;
reconsider t1 = t as
set by
A11;
(f
.: z1)
c= (f
.: (c1
\ c2)) by
A9,
A10,
RELAT_1: 123;
hence t
in (
bool (s1
\ s2)) by
A11,
A8;
end;
hence (f
.: y2) is
Subset-Family of (s1
\ s2);
now
hereby
let t be
object;
assume t
in (
union (f
.: y2));
then
consider u be
set such that
A12: t
in u and
A13: u
in (f
.: y2) by
TARSKI:def 4;
consider v be
Subset of X such that
A14: v
in y2 and
A15: u
= (f
.: v) by
A13,
FUNCT_2:def 10;
(f
.: v)
c= (f
.: (c1
\ c2)) by
A14,
A9,
RELAT_1: 123;
hence t
in (s1
\ s2) by
A12,
A15,
A8;
end;
let t be
object;
assume t
in (s1
\ s2);
then t
in (f
.: (c1
\ c2)) by
A1,
A5,
A7,
FUNCT_1: 64;
then
consider v be
object such that
A16: v
in (
dom f) and
A17: v
in (c1
\ c2) and
A18: t
= (f
. v) by
FUNCT_1:def 6;
v
in (
union y1) by
A9,
A17,
EQREL_1:def 4;
then
consider u be
set such that
A19: v
in u and
A20: u
in y1 by
TARSKI:def 4;
reconsider fu = (f
.: u) as
Subset of Y;
(f
. v)
in (f
.: u) & (f
.: u)
in (f
.: y2) by
A16,
A19,
FUNCT_1:def 6,
A20,
FUNCT_2:def 10;
hence t
in (
union (f
.: y2)) by
A18,
TARSKI:def 4;
end;
hence (
union (f
.: y2))
= (s1
\ s2) by
TARSKI:def 3;
thus for A be
Subset of (s1
\ s2) st A
in (f
.: y2) holds A
<>
{} & for B be
Subset of (s1
\ s2) st B
in (f
.: y2) holds A
= B or A
misses B
proof
let A be
Subset of (s1
\ s2);
assume A
in (f
.: y2);
then
consider a0 be
Subset of X such that
A23: a0
in y2 and
A24: A
= (f
.: a0) by
FUNCT_2:def 10;
thus A
<>
{}
proof
assume
A25: A
=
{} ;
(
dom f)
= X by
PARTFUN1:def 2;
hence contradiction by
A23,
A9,
A25,
A24;
end;
let B be
Subset of (s1
\ s2);
assume B
in (f
.: y2);
then
consider b0 be
Subset of X such that
A26: b0
in y2 and
A27: B
= (f
.: b0) by
FUNCT_2:def 10;
thus thesis by
A23,
A24,
A26,
A27,
A1,
A9,
EQREL_1:def 4,
FUNCT_1: 66;
end;
end;
hence thesis by
EQREL_1:def 4;
end;
end;
hence thesis;
end;
theorem ::
SRINGS_4:11
for X,Y be non
empty
set, S be
diff-finite-partition-closed
Subset-Family of X, f be
Function of X, Y st f is
one-to-one holds (f
.: S) is
diff-finite-partition-closed
Subset-Family of Y
proof
let X,Y be non
empty
set, S be
diff-finite-partition-closed
Subset-Family of X, f be
Function of X, Y;
assume
A1: f is
one-to-one;
per cases ;
suppose (f
.: S) is
empty;
then for S1,S2 be
Element of (f
.: S) st (S1
\ S2) is non
empty holds (f
.: S) is
diff-finite-partition-closed by
SUBSET_1:def 1;
then (f
.: S) is
diff-finite-partition-closed;
hence thesis;
end;
suppose
A2: (f
.: S) is non
empty;
reconsider fS = (f
.: S) as
Subset-Family of Y;
now
let s1,s2 be
Element of fS;
assume
A3: (s1
\ s2) is non
empty;
A4: s1
in fS by
A2;
consider c1 be
Subset of X such that
A5: c1
in S and
A6: s1
= (f
.: c1) by
A4,
FUNCT_2:def 10;
A7: s2
in fS by
A2;
consider c2 be
Subset of X such that
A8: c2
in S and
A9: s2
= (f
.: c2) by
A7,
FUNCT_2:def 10;
A10: (f
.: (c1
\ c2))
= (s1
\ s2) by
A1,
A6,
A9,
FUNCT_1: 64;
then
A11: (c1
\ c2) is non
empty by
A3;
consider x1 be
finite
Subset of S such that
A12: x1 is
a_partition of (c1
\ c2) by
A5,
A8,
A11,
SRINGS_1:def 2;
x1
c= S & S
c= (
bool X);
then x1
c= (
bool X);
then
reconsider x2 = x1 as
Subset-Family of X;
now
thus (f
.: x2) is
finite
Subset of fS by
FUNCT_2: 103;
thus (f
.: x2) is
a_partition of (s1
\ s2)
proof
now
(f
.: x2)
c= (
bool (s1
\ s2))
proof
let t be
object;
assume t
in (f
.: x2);
then
consider y1 be
Subset of X such that
A13: y1
in x2 and
A14: t
= (f
.: y1) by
FUNCT_2:def 10;
reconsider t1 = t as
set by
A14;
(f
.: y1)
c= (f
.: (c1
\ c2)) by
A12,
A13,
RELAT_1: 123;
then t1
c= (s1
\ s2) by
A14,
A1,
A6,
A9,
FUNCT_1: 64;
hence t
in (
bool (s1
\ s2));
end;
hence (f
.: x2) is
Subset-Family of (s1
\ s2);
now
hereby
let t be
object;
assume t
in (
union (f
.: x2));
then
consider u be
set such that
A15: t
in u and
A16: u
in (f
.: x2) by
TARSKI:def 4;
consider v be
Subset of X such that
A17: v
in x2 and
A18: u
= (f
.: v) by
A16,
FUNCT_2:def 10;
(f
.: v)
c= (f
.: (c1
\ c2)) by
A12,
A17,
RELAT_1: 123;
hence t
in (s1
\ s2) by
A15,
A18,
A10;
end;
let t be
object;
assume t
in (s1
\ s2);
then t
in (f
.: (c1
\ c2)) by
A1,
A6,
A9,
FUNCT_1: 64;
then
consider v be
object such that
A19: v
in (
dom f) and
A20: v
in (c1
\ c2) and
A21: t
= (f
. v) by
FUNCT_1:def 6;
v
in (
union x1) by
A12,
A20,
EQREL_1:def 4;
then
consider u be
set such that
A22: v
in u and
A23: u
in x1 by
TARSKI:def 4;
reconsider fu = (f
.: u) as
Subset of Y;
(f
. v)
in (f
.: u) & (f
.: u)
in (f
.: x2) by
A19,
A22,
FUNCT_1:def 6,
A23,
FUNCT_2:def 10;
hence t
in (
union (f
.: x2)) by
A21,
TARSKI:def 4;
end;
hence (
union (f
.: x2))
= (s1
\ s2) by
TARSKI:def 3;
now
let A be
Subset of (s1
\ s2);
assume A
in (f
.: x2);
then
consider a0 be
Subset of X such that
A26: a0
in x2 and
A27: A
= (f
.: a0) by
FUNCT_2:def 10;
thus A
<>
{}
proof
assume
A28: A
=
{} ;
(
dom f)
= X by
PARTFUN1:def 2;
hence contradiction by
A26,
A12,
A28,
A27;
end;
hereby
let B be
Subset of (s1
\ s2);
assume B
in (f
.: x2);
then
consider b0 be
Subset of X such that
A29: b0
in x2 and
A30: B
= (f
.: b0) by
FUNCT_2:def 10;
thus A
= B or A
misses B by
A26,
A29,
A12,
EQREL_1:def 4,
A27,
A30,
A1,
FUNCT_1: 66;
end;
end;
hence for A be
Subset of (s1
\ s2) st A
in (f
.: x2) holds A
<>
{} & for B be
Subset of (s1
\ s2) st B
in (f
.: x2) holds A
= B or A
misses B;
end;
hence thesis by
EQREL_1:def 4;
end;
end;
hence ex x be
finite
Subset of fS st x is
a_partition of (s1
\ s2);
end;
then fS is
diff-finite-partition-closed;
hence thesis;
end;
end;
theorem ::
SRINGS_4:12
for X,Y be non
empty
set, S be
semiring_of_sets of X, f be
Function of X, Y st f is
one-to-one holds (f
.: S) is
semiring_of_sets of Y by
Thm11,
Thm12;
begin
::$Canceled
registration
let X be
set;
cluster (
cobool X) ->
cap-closed;
coherence
proof
set D = (
cobool X);
for x,y be
set st x
in D & y
in D holds (x
/\ y)
in D
proof
let x,y be
set;
assume x
in D & y
in D;
per cases by
TARSKI:def 2;
suppose x
=
{} ;
hence thesis by
TARSKI:def 2;
end;
suppose x
= X & y
= X;
hence thesis by
TARSKI:def 2;
end;
suppose x
= X & y
=
{} ;
hence thesis by
TARSKI:def 2;
end;
end;
hence thesis;
end;
end
registration
let X be
set;
cluster
with_empty_element for
cap-closed
Subset-Family of X;
existence
proof
take (
cobool X);
thus thesis;
end;
end
registration
let X be
set;
cluster
cup-closed for
with_empty_element
cap-closed
Subset-Family of X;
existence
proof
(
cobool X) is
cup-closed
proof
let a,b be
set;
assume a
in (
cobool X) & b
in (
cobool X);
then a
=
{} & b
=
{} or a
= X & b
=
{} or a
=
{} & b
= X or a
= X & b
= X by
TARSKI:def 2;
hence (a
\/ b)
in (
cobool X) by
TARSKI:def 2;
end;
hence thesis;
end;
end
registration
let X,Y be non
empty
set;
cluster (
DIFFERENCE (X,Y)) -> non
empty;
correctness
proof
consider x be
object such that
A1: x
in X by
XBOOLE_0:def 1;
reconsider x as
Element of X by
A1;
consider y be
object such that
A2: y
in Y by
XBOOLE_0:def 1;
reconsider y as
Element of Y by
A2;
(x
\ y)
in (
DIFFERENCE (X,Y)) by
SETFAM_1:def 6;
hence (
DIFFERENCE (X,Y)) is non
empty;
end;
end
theorem ::
SRINGS_4:14
LemY: for X be
set, S be
with_empty_element
Subset-Family of X holds (
DIFFERENCE (S,S))
= the set of all (A
\ B) where A,B be
Element of S
proof
let X be
set, S be
with_empty_element
Subset-Family of X;
thus (
DIFFERENCE (S,S))
c= the set of all (A
\ B) where A,B be
Element of S
proof
let x be
object;
assume x
in (
DIFFERENCE (S,S));
then
consider X,Y be
set such that
A1: X
in S & Y
in S & x
= (X
\ Y) by
SETFAM_1:def 6;
thus thesis by
A1;
end;
let x be
object;
assume x
in the set of all (A
\ B) where A,B be
Element of S;
then
consider A1,B1 be
Element of S such that
A2: x
= (A1
\ B1);
thus thesis by
A2,
SETFAM_1:def 6;
end;
definition
let X be
set, S be
with_empty_element
Subset-Family of X;
::
SRINGS_4:def1
func
semidiff S ->
Subset-Family of X equals (
DIFFERENCE (S,S));
coherence
proof
set AB = the set of all (A
\ B) where A,B be
Element of S;
AB
c= (
bool X)
proof
let t be
object;
assume t
in the set of all (A
\ B) where A,B be
Element of S;
then
consider A0,B0 be
Element of S such that
A1: t
= (A0
\ B0);
thus t
in (
bool X) by
A1;
end;
then
reconsider AB as
Subset-Family of X;
{}
in S by
SETFAM_1:def 8;
then (
{}
\
{} )
in AB;
hence thesis by
LemY;
end;
end
theorem ::
SRINGS_4:15
LemX1: for X be
set, S be
with_empty_element
Subset-Family of X, x be
object st x
in (
semidiff S) holds ex A,B be
Element of S st x
= (A
\ B)
proof
let X be
set, S be
with_empty_element
Subset-Family of X, x be
object;
assume x
in (
semidiff S);
then x
in the set of all (A
\ B) where A,B be
Element of S by
LemY;
hence thesis;
end;
registration
let X be
set, S be
with_empty_element
Subset-Family of X;
cluster (
semidiff S) ->
with_empty_element;
coherence
proof
set AB = the set of all (A
\ B) where A,B be
Element of S;
AB
c= (
bool X)
proof
let t be
object;
assume t
in the set of all (A
\ B) where A,B be
Element of S;
then
consider A0,B0 be
Element of S such that
A1: t
= (A0
\ B0);
thus t
in (
bool X) by
A1;
end;
then
reconsider AB as
Subset-Family of X;
{}
in S by
SETFAM_1:def 8;
then (
{}
\
{} )
in AB;
hence thesis by
LemY;
end;
end
Thm14: for X be
set, S be
with_empty_element
cap-closed
cup-closed
Subset-Family of X holds (
semidiff S) is
cap-closed
diff-finite-partition-closed
proof
let X be
set, S be
with_empty_element
cap-closed
cup-closed
Subset-Family of X;
thus (
semidiff S) is
cap-closed
proof
let s1,s2 be
set;
assume
A1: s1
in (
semidiff S) & s2
in (
semidiff S);
then
consider a1,b1 be
Element of S such that
A2: s1
= (a1
\ b1) by
LemX1;
consider a2,b2 be
Element of S such that
A3: s2
= (a2
\ b2) by
A1,
LemX1;
A4: (s1
/\ s2)
= (((a1
\ b1)
/\ a2)
\ b2) by
A2,
A3,
XBOOLE_1: 49
.= (((a1
/\ a2)
\ b1)
\ b2) by
XBOOLE_1: 49
.= ((a1
/\ a2)
\ (b1
\/ b2)) by
XBOOLE_1: 41;
(a1
/\ a2) is
Element of S & (b1
\/ b2) is
Element of S by
FINSUB_1:def 1,
FINSUB_1:def 2;
hence (s1
/\ s2)
in (
semidiff S) by
A4,
SETFAM_1:def 6;
end;
thus (
semidiff S) is
diff-finite-partition-closed
proof
let s1,s2 be
Element of (
semidiff S);
assume
A5: (s1
\ s2) is non
empty;
consider a1,b1 be
Element of S such that
A6: s1
= (a1
\ b1) by
LemX1;
consider a2,b2 be
Element of S such that
A7: s2
= (a2
\ b2) by
LemX1;
A8: (a1
/\ b2)
in S by
FINSUB_1:def 2;
(a1
/\ a2)
in S by
FINSUB_1:def 2;
then
A9: ((a1
/\ a2)
/\ b2)
in S by
FINSUB_1:def 2;
A10: (b1
\/ a2)
in S by
FINSUB_1:def 1;
then
A11: ((b1
\/ a2)
\/ b2)
in S by
FINSUB_1:def 1;
A12: (s1
\ s2)
= ((((a1
/\ b2)
\ (b1
\/ a2))
\/ (a1
\ ((b1
\/ a2)
\/ b2)))
\/ (((a1
/\ a2)
/\ b2)
\ b1)) by
A6,
A7,
Thm04;
A13: ((a1
/\ b2)
\ (b1
\/ a2))
c= (s1
\ s2) & (a1
\ ((b1
\/ a2)
\/ b2))
c= (s1
\ s2) & (((a1
/\ a2)
/\ b2)
\ b1)
c= (s1
\ s2)
proof
A14: (((a1
/\ b2)
\ (b1
\/ a2))
\/ (a1
\ ((b1
\/ a2)
\/ b2)))
c= (s1
\ s2) by
A12,
XBOOLE_1: 7;
((a1
/\ b2)
\ (b1
\/ a2))
c= (((a1
/\ b2)
\ (b1
\/ a2))
\/ (a1
\ ((b1
\/ a2)
\/ b2))) & (a1
\ ((b1
\/ a2)
\/ b2))
c= (((a1
/\ b2)
\ (b1
\/ a2))
\/ (a1
\ ((b1
\/ a2)
\/ b2))) by
XBOOLE_1: 7;
hence thesis by
A12,
A14,
XBOOLE_1: 7;
end;
per cases by
A5,
A12;
suppose
A16: ((a1
/\ b2)
\ (b1
\/ a2))
<>
{} & (a1
\ ((b1
\/ a2)
\/ b2))
<>
{} & (((a1
/\ a2)
/\ b2)
\ b1)
<>
{} ;
set x =
{((a1
/\ b2)
\ (b1
\/ a2)), (a1
\ ((b1
\/ a2)
\/ b2)), (((a1
/\ a2)
/\ b2)
\ b1)};
a17: x
c= (
semidiff S)
proof
let t be
object;
assume t
in x;
then t
= ((a1
/\ b2)
\ (b1
\/ a2)) or t
= (a1
\ ((b1
\/ a2)
\/ b2)) or t
= (((a1
/\ a2)
/\ b2)
\ b1) by
ENUMSET1:def 1;
hence t
in (
semidiff S) by
A8,
A10,
A11,
A9,
SETFAM_1:def 6;
end;
x
c= (
bool (s1
\ s2))
proof
let t be
object;
assume
A18: t
in x;
then
reconsider t1 = t as
set;
t1
c= (s1
\ s2) by
A13,
A18,
ENUMSET1:def 1;
hence t
in (
bool (s1
\ s2));
end;
then
reconsider x as
Subset-Family of (s1
\ s2);
x is
a_partition of (s1
\ s2)
proof
thus (
union x)
= (s1
\ s2) by
A12,
Thm05;
let u be
Subset of (s1
\ s2);
assume
A19: u
in x;
then
A20: u
= ((a1
/\ b2)
\ (b1
\/ a2)) or u
= (a1
\ ((b1
\/ a2)
\/ b2)) or u
= (((a1
/\ a2)
/\ b2)
\ b1) by
ENUMSET1:def 1;
thus u
<>
{} by
A19,
A16;
let v be
Subset of (s1
\ s2);
assume v
in x;
then v
= ((a1
/\ b2)
\ (b1
\/ a2)) or v
= (a1
\ ((b1
\/ a2)
\/ b2)) or v
= (((a1
/\ a2)
/\ b2)
\ b1) by
ENUMSET1:def 1;
hence u
= v or u
misses v by
A20,
Thm01;
end;
hence ex x be
finite
Subset of (
semidiff S) st x is
a_partition of (s1
\ s2) by
a17;
end;
suppose
A20a: ((a1
/\ b2)
\ (b1
\/ a2))
=
{} & (a1
\ ((b1
\/ a2)
\/ b2))
<>
{} & (((a1
/\ a2)
/\ b2)
\ b1)
<>
{} ;
set x =
{(a1
\ ((b1
\/ a2)
\/ b2)), (((a1
/\ a2)
/\ b2)
\ b1)};
a21: x
c= (
semidiff S)
proof
let t be
object;
assume t
in x;
then t
= (a1
\ ((b1
\/ a2)
\/ b2)) or t
= (((a1
/\ a2)
/\ b2)
\ b1) by
TARSKI:def 2;
hence t
in (
semidiff S) by
A11,
A9,
SETFAM_1:def 6;
end;
x
c= (
bool (s1
\ s2))
proof
let t be
object;
assume
A22: t
in x;
then
reconsider t1 = t as
set;
(a1
\ ((b1
\/ a2)
\/ b2))
c= (s1
\ s2) & (((a1
/\ a2)
/\ b2)
\ b1)
c= (s1
\ s2)
proof
A23: (((a1
/\ b2)
\ (b1
\/ a2))
\/ (a1
\ ((b1
\/ a2)
\/ b2)))
c= (s1
\ s2) by
A12,
XBOOLE_1: 7;
((a1
/\ b2)
\ (b1
\/ a2))
c= (((a1
/\ b2)
\ (b1
\/ a2))
\/ (a1
\ ((b1
\/ a2)
\/ b2))) & (a1
\ ((b1
\/ a2)
\/ b2))
c= (((a1
/\ b2)
\ (b1
\/ a2))
\/ (a1
\ ((b1
\/ a2)
\/ b2))) by
XBOOLE_1: 7;
hence thesis by
A12,
A23,
XBOOLE_1: 7;
end;
then t1
c= (s1
\ s2) by
A22,
TARSKI:def 2;
hence t
in (
bool (s1
\ s2));
end;
then
reconsider x as
Subset-Family of (s1
\ s2);
x is
a_partition of (s1
\ s2)
proof
thus (
union x)
= (s1
\ s2) by
A12,
A20a,
ZFMISC_1: 75;
let u be
Subset of (s1
\ s2);
assume
A25: u
in x;
then
A26: u
= (a1
\ ((b1
\/ a2)
\/ b2)) or u
= (((a1
/\ a2)
/\ b2)
\ b1) by
TARSKI:def 2;
thus u
<>
{} by
A25,
A20a;
let v be
Subset of (s1
\ s2);
assume v
in x;
then v
= (a1
\ ((b1
\/ a2)
\/ b2)) or v
= (((a1
/\ a2)
/\ b2)
\ b1) by
TARSKI:def 2;
hence u
= v or u
misses v by
A26,
Thm01;
end;
hence ex x be
finite
Subset of (
semidiff S) st x is
a_partition of (s1
\ s2) by
a21;
end;
suppose
A26a: ((a1
/\ b2)
\ (b1
\/ a2))
<>
{} & (a1
\ ((b1
\/ a2)
\/ b2))
<>
{} & (((a1
/\ a2)
/\ b2)
\ b1)
=
{} ;
set x =
{((a1
/\ b2)
\ (b1
\/ a2)), (a1
\ ((b1
\/ a2)
\/ b2))};
a27: x
c= (
semidiff S)
proof
let t be
object;
assume t
in x;
then t
= ((a1
/\ b2)
\ (b1
\/ a2)) or t
= (a1
\ ((b1
\/ a2)
\/ b2)) by
TARSKI:def 2;
hence t
in (
semidiff S) by
SETFAM_1:def 6,
A8,
A10,
A11;
end;
x
c= (
bool (s1
\ s2))
proof
let t be
object;
assume
A28: t
in x;
then
reconsider t1 = t as
set;
t1
c= (s1
\ s2) by
A13,
A28,
TARSKI:def 2;
hence t
in (
bool (s1
\ s2));
end;
then
reconsider x as
Subset-Family of (s1
\ s2);
x is
a_partition of (s1
\ s2)
proof
thus (
union x)
= (s1
\ s2) by
A12,
A26a,
ZFMISC_1: 75;
let u be
Subset of (s1
\ s2);
assume
A29: u
in x;
then
A30: u
= ((a1
/\ b2)
\ (b1
\/ a2)) or u
= (a1
\ ((b1
\/ a2)
\/ b2)) by
TARSKI:def 2;
thus u
<>
{} by
A29,
A26a;
let v be
Subset of (s1
\ s2);
assume v
in x;
then v
= ((a1
/\ b2)
\ (b1
\/ a2)) or v
= (a1
\ ((b1
\/ a2)
\/ b2)) by
TARSKI:def 2;
hence u
= v or u
misses v by
A30,
Thm01;
end;
hence ex x be
finite
Subset of (
semidiff S) st x is
a_partition of (s1
\ s2) by
a27;
end;
suppose
A31: ((a1
/\ b2)
\ (b1
\/ a2))
<>
{} & (a1
\ ((b1
\/ a2)
\/ b2))
=
{} & (((a1
/\ a2)
/\ b2)
\ b1)
<>
{} ;
set x =
{((a1
/\ b2)
\ (b1
\/ a2)), (((a1
/\ a2)
/\ b2)
\ b1)};
a32: x
c= (
semidiff S)
proof
let t be
object;
assume t
in x;
then t
= ((a1
/\ b2)
\ (b1
\/ a2)) or t
= (((a1
/\ a2)
/\ b2)
\ b1) by
TARSKI:def 2;
hence t
in (
semidiff S) by
A8,
A9,
A10,
SETFAM_1:def 6;
end;
x
c= (
bool (s1
\ s2))
proof
let t be
object;
assume
A33: t
in x;
then
reconsider t1 = t as
set;
t1
c= (s1
\ s2) by
A13,
A33,
TARSKI:def 2;
hence t
in (
bool (s1
\ s2));
end;
then
reconsider x as
Subset-Family of (s1
\ s2);
x is
a_partition of (s1
\ s2)
proof
thus (
union x)
= (s1
\ s2) by
A12,
A31,
ZFMISC_1: 75;
let u be
Subset of (s1
\ s2);
assume
A34: u
in x;
then
A35: u
= ((a1
/\ b2)
\ (b1
\/ a2)) or u
= (((a1
/\ a2)
/\ b2)
\ b1) by
TARSKI:def 2;
thus u
<>
{} by
A31,
A34;
let v be
Subset of (s1
\ s2);
assume v
in x;
then v
= ((a1
/\ b2)
\ (b1
\/ a2)) or v
= (((a1
/\ a2)
/\ b2)
\ b1) by
TARSKI:def 2;
hence u
= v or u
misses v by
A35,
Thm01;
end;
hence ex x be
finite
Subset of (
semidiff S) st x is
a_partition of (s1
\ s2) by
a32;
end;
suppose
A36: ((a1
/\ b2)
\ (b1
\/ a2))
<>
{} & (a1
\ ((b1
\/ a2)
\/ b2))
=
{} & (((a1
/\ a2)
/\ b2)
\ b1)
=
{} ;
set x =
{((a1
/\ b2)
\ (b1
\/ a2))};
a37: x
c= (
semidiff S)
proof
let t be
object;
assume t
in x;
then t
= ((a1
/\ b2)
\ (b1
\/ a2)) by
TARSKI:def 1;
hence t
in (
semidiff S) by
SETFAM_1:def 6,
A8,
A10;
end;
x
c= (
bool (s1
\ s2))
proof
let t be
object;
assume
A38: t
in x;
then
reconsider t1 = t as
set;
t1
c= (s1
\ s2) by
A13,
A38,
TARSKI:def 1;
hence t
in (
bool (s1
\ s2));
end;
then
reconsider x as
Subset-Family of (s1
\ s2);
x is
a_partition of (s1
\ s2)
proof
thus (
union x)
= (s1
\ s2) by
A12,
A36;
let u be
Subset of (s1
\ s2);
assume
A39: u
in x;
then
A40: u
= ((a1
/\ b2)
\ (b1
\/ a2)) by
TARSKI:def 1;
thus u
<>
{} by
A39,
A36;
thus for v be
Subset of (s1
\ s2) st v
in x holds u
= v or u
misses v by
A40,
TARSKI:def 1;
end;
hence ex x be
finite
Subset of (
semidiff S) st x is
a_partition of (s1
\ s2) by
a37;
end;
suppose
A41: ((a1
/\ b2)
\ (b1
\/ a2))
=
{} & (a1
\ ((b1
\/ a2)
\/ b2))
<>
{} & (((a1
/\ a2)
/\ b2)
\ b1)
=
{} ;
set x =
{(a1
\ ((b1
\/ a2)
\/ b2))};
a42: x
c= (
semidiff S)
proof
let t be
object;
assume t
in x;
then t
= (a1
\ ((b1
\/ a2)
\/ b2)) by
TARSKI:def 1;
hence t
in (
semidiff S) by
SETFAM_1:def 6,
A11;
end;
x
c= (
bool (s1
\ s2))
proof
let t be
object;
assume
A43: t
in x;
then
reconsider t1 = t as
set;
t1
c= (s1
\ s2) by
A13,
A43,
TARSKI:def 1;
hence t
in (
bool (s1
\ s2));
end;
then
reconsider x as
Subset-Family of (s1
\ s2);
x is
a_partition of (s1
\ s2)
proof
thus (
union x)
= (s1
\ s2) by
A12,
A41;
let u be
Subset of (s1
\ s2);
assume
A44: u
in x;
then
A45: u
= (a1
\ ((b1
\/ a2)
\/ b2)) by
TARSKI:def 1;
thus u
<>
{} by
A44,
A41;
thus for v be
Subset of (s1
\ s2) st v
in x holds u
= v or u
misses v by
A45,
TARSKI:def 1;
end;
hence ex x be
finite
Subset of (
semidiff S) st x is
a_partition of (s1
\ s2) by
a42;
end;
suppose
A46: ((a1
/\ b2)
\ (b1
\/ a2))
=
{} & (a1
\ ((b1
\/ a2)
\/ b2))
=
{} & (((a1
/\ a2)
/\ b2)
\ b1)
<>
{} ;
set x =
{(((a1
/\ a2)
/\ b2)
\ b1)};
a47: x
c= (
semidiff S)
proof
let t be
object;
assume t
in x;
then t
= (((a1
/\ a2)
/\ b2)
\ b1) by
TARSKI:def 1;
hence t
in (
semidiff S) by
SETFAM_1:def 6,
A9;
end;
x
c= (
bool (s1
\ s2))
proof
let t be
object;
assume
A48: t
in x;
then
reconsider t1 = t as
set;
t1
c= (s1
\ s2) by
A13,
A48,
TARSKI:def 1;
hence t
in (
bool (s1
\ s2));
end;
then
reconsider x as
Subset-Family of (s1
\ s2);
x is
a_partition of (s1
\ s2)
proof
thus (
union x)
= (s1
\ s2) by
A12,
A46;
let u be
Subset of (s1
\ s2);
assume
A49: u
in x;
then
A50: u
= (((a1
/\ a2)
/\ b2)
\ b1) by
TARSKI:def 1;
thus u
<>
{} by
A49,
A46;
thus for v be
Subset of (s1
\ s2) st v
in x holds u
= v or u
misses v by
A50,
TARSKI:def 1;
end;
hence ex x be
finite
Subset of (
semidiff S) st x is
a_partition of (s1
\ s2) by
a47;
end;
end;
end;
registration
let X be
set, S be
with_empty_element
cap-closed
cup-closed
Subset-Family of X;
cluster (
semidiff S) ->
cap-closed
diff-finite-partition-closed;
coherence by
Thm14;
end
theorem ::
SRINGS_4:16
for X be
set, S be
with_empty_element
cap-closed
cup-closed
Subset-Family of X holds (
semidiff S) is
semiring_of_sets of X;
begin
definition
let T be non
empty
TopSpace;
::
SRINGS_4:def2
func
capOpCl T ->
Subset-Family of (
[#] T) equals { (A
/\ B) where A,B be
Subset of T : A is
open & B is
closed };
coherence
proof
{ (A
/\ B) where A,B be
Subset of T : A is
open & B is
closed }
c= (
bool (
[#] T))
proof
let t be
object;
assume t
in { (A
/\ B) where A,B be
Subset of T : A is
open & B is
closed };
then
consider A0,B0 be
Subset of T such that
A1: t
= (A0
/\ B0) and A0 is
open and B0 is
closed;
reconsider t0 = t as
set by
A1;
(
[#] T) is non
empty & A0 is
Subset of (
[#] T) & B0 is
Subset of (
[#] T) by
STRUCT_0:def 3;
then t0
c= ((
[#] T)
/\ (
[#] T)) by
A1,
XBOOLE_1: 27;
hence t
in (
bool (
[#] T));
end;
hence thesis;
end;
end
Thm15: for T be non
empty
TopSpace holds (
capOpCl T) is
with_empty_element
cap-closed
diff-finite-partition-closed
proof
let T be non
empty
TopSpace;
set SR = { (A
/\ B) where A,B be
Subset of T : A is
open & B is
closed };
the
topology of T is
with_empty_element
cap-closed
cup-closed
Subset-Family of (
[#] T)
proof
A1: the
topology of T is
with_empty_element by
PRE_TOPC: 1;
A2: the
topology of T is
cap-closed by
PRE_TOPC:def 1;
the
topology of T is
cup-closed
proof
now
let x,y be
set;
assume
A3: x
in the
topology of T & y
in the
topology of T;
{x, y}
c= (
bool the
carrier of T)
proof
let t be
object;
assume t
in
{x, y};
then t
in the
topology of T by
A3,
TARSKI:def 2;
hence t
in (
bool the
carrier of T);
end;
then
reconsider xy =
{x, y} as
Subset-Family of T;
xy
c= the
topology of T by
A3,
TARSKI:def 2;
then (
union xy)
in the
topology of T by
PRE_TOPC:def 1;
hence (x
\/ y)
in the
topology of T by
ZFMISC_1: 75;
end;
hence thesis;
end;
hence thesis by
A1,
A2,
STRUCT_0:def 3;
end;
then
reconsider XS = the
topology of T as
with_empty_element
cap-closed
cup-closed
Subset-Family of (
[#] T);
SR
= (
semidiff XS)
proof
hereby
let x be
object;
assume x
in SR;
then
consider A,B be
Subset of T such that
A4: x
= (A
/\ B) and
A5: A is
open and
A6: B is
closed;
A is
Element of (
bool (
[#] T)) by
STRUCT_0:def 3;
then
A7: (A
\ (
[#] T)) is
empty by
XBOOLE_1: 37;
A8: (A
\ ((
[#] T)
\ B))
= ((A
\ (
[#] T))
\/ (A
/\ B)) by
XBOOLE_1: 52
.= (A
/\ B) by
A7;
reconsider A1 = A, CB1 = ((
[#] T)
\ B) as
Element of XS by
A5,
A6,
PRE_TOPC:def 2,
PRE_TOPC:def 3;
x
= (A1
\ CB1) by
A4,
A8;
hence x
in (
semidiff XS) by
SETFAM_1:def 6;
end;
let x be
object;
assume x
in (
semidiff XS);
then
consider A,B be
Element of XS such that
A9: x
= (A
\ B) by
LemX1;
A
in the
topology of T & B
in the
topology of T;
then
reconsider A1 = A, B1 = B as
Subset of T;
A10: (A1
\ (
[#] T)) is
empty & ((
[#] T)
/\ B1)
= B1 by
XBOOLE_1: 37,
XBOOLE_1: 28;
A11: A1 is
open & B1 is
open by
PRE_TOPC:def 2;
A12: ((
[#] T)
\ ((
[#] T)
\ B1))
= ((
[#] T)
/\ B1) by
XBOOLE_1: 48
.= B1 by
XBOOLE_1: 28;
then
A13: ((
[#] T)
\ B1) is
closed by
PRE_TOPC:def 2,
PRE_TOPC:def 3;
(A1
\ ((
[#] T)
\ ((
[#] T)
\ B1)))
= ((A1
\ (
[#] T))
\/ (A1
/\ ((
[#] T)
\ B1))) by
XBOOLE_1: 52
.= (A1
/\ ((
[#] T)
\ B1)) by
A10;
hence x
in SR by
A9,
A11,
A12,
A13;
end;
hence thesis;
end;
registration
let T be non
empty
TopSpace;
cluster (
capOpCl T) ->
with_empty_element
cap-closed
diff-finite-partition-closed;
coherence by
Thm15;
end
theorem ::
SRINGS_4:17
for T be non
empty
TopSpace holds (
capOpCl T) is
semiring_of_sets of (
[#] T);
begin
registration
let n be
Nat;
cluster
non-empty for n
-element
FinSequence;
existence
proof
set p = (n
|->
{
{} });
take p;
not
{}
in (
rng p)
proof
assume
{}
in (
rng p);
then
consider a be
object such that
A1: a
in (
dom p) and
A2:
{}
= (p
. a) by
FUNCT_1:def 3;
a
in (
Seg n) by
FINSEQ_1: 89,
A1;
hence contradiction by
A2,
FINSEQ_2: 57;
end;
hence thesis by
RELAT_1:def 9;
end;
end
definition
let n be non
zero
Nat, X be
non-emptyn
-element
FinSequence;
::
SRINGS_4:def3
mode
SemiringFamily of X -> n
-element
FinSequence means
:
Def2: for i be
Nat st i
in (
Seg n) holds (it
. i) is
semiring_of_sets of (X
. i);
existence
proof
deffunc
F(
set) = (
Fin (X
. $1));
consider p be
FinSequence such that
A1: (
len p)
= n and
A2: for i be
Nat st i
in (
dom p) holds (p
. i)
=
F(i) from
FINSEQ_1:sch 2;
reconsider p as n
-element
FinSequence by
A1,
CARD_1:def 7;
take p;
let i be
Nat;
assume
A3: i
in (
Seg n);
reconsider Xi = (X
. i) as
set;
A4: (
Fin Xi) is
semiring_of_sets of Xi by
SRINGS_2: 6;
i
in (
dom p) by
A3,
A1,
FINSEQ_1:def 3;
hence (p
. i) is
semiring_of_sets of (X
. i) by
A2,
A4;
end;
end
reserve n for non
zero
Nat;
reserve X for
non-emptyn
-element
FinSequence;
theorem ::
SRINGS_4:18
Thm16: for S be
SemiringFamily of X holds (
dom S)
= (
dom X)
proof
let S be
SemiringFamily of X;
(
dom S)
= (
Seg n) by
FINSEQ_1: 89;
hence thesis by
FINSEQ_1: 89;
end;
theorem ::
SRINGS_4:19
Thm17: for S be
SemiringFamily of X holds for i be
Nat st i
in (
Seg n) holds (
union (S
. i))
c= (X
. i)
proof
let S be
SemiringFamily of X;
let i be
Nat;
assume i
in (
Seg n);
then (S
. i) is
semiring_of_sets of (X
. i) by
Def2;
then (
union (S
. i))
c= (
union (
bool (X
. i))) by
ZFMISC_1: 77;
hence (
union (S
. i))
c= (X
. i) by
ZFMISC_1: 81;
end;
theorem ::
SRINGS_4:20
Thm18: for f be
Function, X be n
-element
FinSequence st f
in (
product X) holds f is n
-element
FinSequence
proof
let f be
Function, X be n
-element
FinSequence;
assume
A1: f
in (
product X);
A2: (
dom X)
= (
Seg n) by
FINSEQ_1: 89;
then (
dom f)
= (
Seg n) by
A1,
CARD_3: 9;
then
reconsider f as
FinSequence by
FINSEQ_1:def 2;
(
dom f) is n
-element by
A1,
A2,
CARD_3: 9;
then (
card (
dom f))
= n by
CARD_1:def 7;
then (
card f)
= n by
CARD_1: 62;
hence thesis by
CARD_1:def 7;
end;
definition
let n be non
zero
Nat, X be n
-element
FinSequence;
::
SRINGS_4:def4
func
SemiringProduct (X) ->
set means
:
Def3: for f be
object holds f
in it iff ex g be
Function st f
= (
product g) & g
in (
product X);
existence
proof
defpred
P[
object] means ex g be
Function st $1
= (
product g) & g
in (
product X);
consider Y be
set such that
A1: for x be
object holds x
in Y iff x
in (
bool (
Funcs ((
dom X),(
union (
Union X))))) &
P[x] from
XBOOLE_0:sch 1;
take Y;
now
thus for x be
object st x
in Y holds ex g be
Function st x
= (
product g) & g
in (
product X) by
A1;
let x be
object;
assume
A2: ex g be
Function st x
= (
product g) & g
in (
product X);
given g be
Function such that
A3: x
= (
product g) and
A4: g
in (
product X);
A5: (
dom g)
= (
dom X) by
A4,
CARD_3: 9;
(
rng g)
c= (
Union X)
proof
let t be
object;
assume t
in (
rng g);
then
consider u be
object such that
A6: u
in (
dom g) and
A7: t
= (g
. u) by
FUNCT_1:def 3;
consider h be
Function such that
A8: g
= h and
A9: (
dom h)
= (
dom X) and
A10: for v be
object st v
in (
dom X) holds (h
. v)
in (X
. v) by
A4,
CARD_3:def 5;
t
in (X
. u) & (X
. u)
in (
rng X) by
A8,
A9,
A10,
A6,
A7,
FUNCT_1:def 3;
hence thesis by
TARSKI:def 4;
end;
then (
Union g)
c= (
union (
Union X)) by
ZFMISC_1: 77;
then (
Funcs ((
dom g),(
Union g)))
c= (
Funcs ((
dom X),(
union (
Union X)))) by
A5,
FUNCT_5: 56;
then
A11: (
bool (
Funcs ((
dom g),(
Union g))))
c= (
bool (
Funcs ((
dom X),(
union (
Union X))))) by
ZFMISC_1: 67;
(
product g)
c= (
Funcs ((
dom g),(
Union g))) by
FUNCT_6: 1;
hence x
in Y by
A2,
A1,
A3,
A11;
end;
hence thesis;
end;
uniqueness
proof
let S1,S2 be
set such that
A12: for f be
object holds f
in S1 iff ex g be
Function st f
= (
product g) & g
in (
product X) and
A13: for f be
object holds f
in S2 iff ex g be
Function st f
= (
product g) & g
in (
product X);
now
let x be
object;
x
in S1 iff ex g be
Function st x
= (
product g) & g
in (
product X) by
A12;
hence x
in S1 iff x
in S2 by
A13;
end;
hence thesis by
TARSKI: 2;
end;
end
theorem ::
SRINGS_4:21
Thm19: for X be n
-element
FinSequence holds (
SemiringProduct X)
c= (
bool (
Funcs ((
dom X),(
union (
Union X)))))
proof
let X be n
-element
FinSequence;
let x be
object;
assume x
in (
SemiringProduct X);
then
consider g be
Function such that
A1: x
= (
product g) and
A2: g
in (
product X) by
Def3;
A3: (
dom g)
= (
dom X) by
A2,
CARD_3: 9;
(
rng g)
c= (
Union X)
proof
let t be
object;
assume t
in (
rng g);
then
consider u be
object such that
A4: u
in (
dom g) and
A5: t
= (g
. u) by
FUNCT_1:def 3;
consider h be
Function such that
A6: g
= h and
A7: (
dom h)
= (
dom X) and
A8: for v be
object st v
in (
dom X) holds (h
. v)
in (X
. v) by
A2,
CARD_3:def 5;
t
in (X
. u) & (X
. u)
in (
rng X) by
A6,
A7,
A8,
A4,
A5,
FUNCT_1:def 3;
hence thesis by
TARSKI:def 4;
end;
then (
Union g)
c= (
union (
Union X)) by
ZFMISC_1: 77;
then (
Funcs ((
dom g),(
Union g)))
c= (
Funcs ((
dom X),(
union (
Union X)))) by
A3,
FUNCT_5: 56;
then
A9: (
bool (
Funcs ((
dom g),(
Union g))))
c= (
bool (
Funcs ((
dom X),(
union (
Union X))))) by
ZFMISC_1: 67;
(
product g)
c= (
Funcs ((
dom g),(
Union g))) by
FUNCT_6: 1;
hence thesis by
A1,
A9;
end;
theorem ::
SRINGS_4:22
Thm20: for S be
SemiringFamily of X holds (
SemiringProduct S) is
Subset-Family of (
product X)
proof
let S be
SemiringFamily of X;
reconsider SPS = (
SemiringProduct S) as
Subset of (
bool (
Funcs ((
dom S),(
union (
Union S))))) by
Thm19;
SPS
c= (
bool (
product X))
proof
let x be
object;
assume
A1: x
in SPS;
reconsider x1 = x as
set by
TARSKI: 1;
x1
c= (
product X)
proof
let t be
object;
assume
A2: t
in x1;
consider g be
Function such that
A3: x1
= (
product g) and
A4: g
in (
product S) by
A1,
Def3;
A5: (
dom g)
= (
dom S) by
A4,
CARD_3: 9;
consider u be
Function such that
A7: t
= u and
A8: (
dom u)
= (
dom g) and
A9: for v be
object st v
in (
dom g) holds (u
. v)
in (g
. v) by
A2,
A3,
CARD_3:def 5;
consider w be
Function such that
A10: g
= w and (
dom w)
= (
dom S) and
A12: for y be
object st y
in (
dom S) holds (w
. y)
in (S
. y) by
A4,
CARD_3:def 5;
A12a: (
dom S)
= (
dom X) by
Thm16;
now
let a be
object;
assume
A13: a
in (
dom X);
A15: a
in (
Seg n) by
A13,
FINSEQ_1: 89;
reconsider a1 = a as
Nat by
A13;
(u
. a)
in (g
. a) & (g
. a)
in (S
. a) by
A13,
A12a,
A10,
A12,
A9,
A5;
then
A16: (u
. a)
in (
union (S
. a)) & a
in (
Seg n) by
A13,
FINSEQ_1: 89,
TARSKI:def 4;
(
union (S
. a))
c= (X
. a) by
A15,
Thm17;
hence (u
. a)
in (X
. a) by
A16;
end;
hence t
in (
product X) by
A12a,
A5,
A8,
A7,
CARD_3:def 5;
end;
hence x
in (
bool (
product X));
end;
hence thesis;
end;
theorem ::
SRINGS_4:23
Thm21: for X be
non-empty1
-element
FinSequence holds (
product X)
= the set of all
<*x*> where x be
Element of (X
. 1)
proof
let X be
non-empty1
-element
FinSequence;
A1: (
dom X)
=
{1} by
FINSEQ_1: 89,
FINSEQ_1: 2;
A2: (X
. 1) is non
empty
proof
assume
A3: (X
. 1) is
empty;
1
in (
dom X) by
A1,
TARSKI:def 1;
hence contradiction by
A3;
end;
(
len X)
= 1 by
CARD_1:def 7;
then X
=
<*(X
. 1)*> by
FINSEQ_1: 40;
then
consider I be
Function of (X
. 1), (
product X) such that I is
one-to-one and
A4: I is
onto and
A5: for x be
object st x
in (X
. 1) holds (I
. x)
=
<*x*> by
A2,
PRVECT_3: 4;
now
hereby
let t be
object;
assume t
in (
product X);
then t
in (
rng I) by
A4,
FUNCT_2:def 3;
then
consider a be
object such that
A6: a
in (
dom I) and
A7: t
= (I
. a) by
FUNCT_1:def 3;
t
=
<*a*> by
A7,
A6,
A5;
hence t
in the set of all
<*x*> where x be
Element of (X
. 1) by
A6;
end;
let t be
object;
assume t
in the set of all
<*x*> where x be
Element of (X
. 1);
then
consider x be
Element of (X
. 1) such that
A9: t
=
<*x*>;
reconsider t1 = t as
FinSequence by
A9;
(
dom t1)
= (
Seg 1) by
A9,
FINSEQ_1:def 8;
then
A10: (
dom t1)
= (
dom X) by
FINSEQ_1: 89;
for a be
object st a
in (
dom X) holds (t1
. a)
in (X
. a)
proof
let a be
object;
assume a
in (
dom X);
then
A11: a
= 1 by
A1,
TARSKI:def 1;
then (t1
. a) is
Element of (X
. 1) by
A9,
FINSEQ_1: 40;
hence thesis by
A2,
A11;
end;
hence t
in (
product X) by
A10,
CARD_3:def 5;
end;
then the set of all
<*x*> where x be
Element of (X
. 1)
c= (
product X) & (
product X)
c= the set of all
<*x*> where x be
Element of (X
. 1);
hence thesis;
end;
Thm22: (
product
<*
{} *>) is
empty
proof
{}
in
{
{} } by
TARSKI:def 1;
then
{}
in (
rng
<*
{} *>) by
FINSEQ_1: 39;
hence thesis by
CARD_3: 26;
end;
registration
cluster (
product
<*
{} *>) ->
empty;
coherence by
Thm22;
end
theorem ::
SRINGS_4:24
Thm23: for x be non
empty
set holds (
product
<*x*>)
= the set of all
<*y*> where y be
Element of x
proof
let x be non
empty
set;
A1: (
rng
<*x*>)
=
{x} & (
<*x*>
. 1)
= x by
FINSEQ_1: 38,
FINSEQ_1: 40;
then
{}
in (
rng
<*x*>) implies
{}
= x;
then
<*x*> is
non-empty1
-element
FinSequence by
RELAT_1:def 9;
hence thesis by
A1,
Thm21;
end;
theorem ::
SRINGS_4:25
Thm24: for X be
non-empty1
-element
FinSequence, S be
SemiringFamily of X holds (
SemiringProduct S)
= the set of all (
product
<*s*>) where s be
Element of (S
. 1)
proof
let X be
non-empty1
-element
FinSequence, S be
SemiringFamily of X;
A1: (
dom X)
=
{1} by
FINSEQ_1: 2,
FINSEQ_1: 89;
A2: S is
non-empty
proof
assume not S is
non-empty;
then
{}
in (
rng S) by
RELAT_1:def 9;
then
consider a be
object such that
A3: a
in (
dom S) and
A4: (S
. a)
=
{} by
FUNCT_1:def 3;
a
in (
dom X) by
Thm16,
A3;
then
A5: (S
. 1)
=
{} by
A4,
A1,
TARSKI:def 1;
S is
SemiringFamily of X & 1
in (
Seg 1) by
FINSEQ_1: 3;
hence contradiction by
A5,
Def2;
end;
then
A6: (
product S)
= the set of all
<*s*> where s be
Element of (S
. 1) by
Thm21;
now
hereby
let x be
object;
assume x
in (
SemiringProduct S);
then
consider f be
Function such that
A7: x
= (
product f) and
A8: f
in (
product S) by
Def3;
f
in the set of all
<*s*> where s be
Element of (S
. 1) by
A2,
A8,
Thm21;
then
consider s be
Element of (S
. 1) such that
A9: f
=
<*s*>;
thus x
in the set of all (
product
<*s*>) where s be
Element of (S
. 1) by
A7,
A9;
end;
let x be
object;
assume x
in the set of all (
product
<*s*>) where s be
Element of (S
. 1);
then
consider s be
Element of (S
. 1) such that
A10: x
= (
product
<*s*>);
set f =
<*s*>;
x
= (
product f) & f
in (
product S) by
A10,
A6;
hence x
in (
SemiringProduct S) by
Def3;
end;
then the set of all (
product
<*s*>) where s be
Element of (S
. 1)
c= (
SemiringProduct S) & (
SemiringProduct S)
c= the set of all (
product
<*s*>) where s be
Element of (S
. 1);
hence thesis;
end;
theorem ::
SRINGS_4:26
Thm25: for x,y be
set holds ((
product
<*x*>)
/\ (
product
<*y*>))
= (
product
<*(x
/\ y)*>)
proof
let x,y be
set;
per cases ;
suppose
A1: not x is
empty & not y is
empty & not (x
/\ y) is
empty;
then
A2: (
product
<*x*>)
= the set of all
<*t*> where t be
Element of x & (
product
<*y*>)
= the set of all
<*t*> where t be
Element of y & (
product
<*(x
/\ y)*>)
= the set of all
<*t*> where t be
Element of (x
/\ y) by
Thm23;
set Px = the set of all
<*t*> where t be
Element of x;
set Py = the set of all
<*t*> where t be
Element of y;
set Pxy = the set of all
<*t*> where t be
Element of (x
/\ y);
now
hereby
let u be
object;
assume u
in (Px
/\ Py);
then
A3: u
in Px & u
in Py by
XBOOLE_0:def 4;
then
consider ux be
Element of x such that
A4: u
=
<*ux*>;
consider uy be
Element of y such that
A5: u
=
<*uy*> by
A3;
ux
= uy by
A4,
A5,
FINSEQ_1: 76;
then ux
in (x
/\ y) by
A1,
XBOOLE_0:def 4;
hence u
in Pxy by
A4;
end;
let u be
object;
assume u
in Pxy;
then
consider uxy be
Element of (x
/\ y) such that
A6: u
=
<*uxy*>;
uxy is
Element of x & uxy is
Element of y by
A1,
XBOOLE_0:def 4;
then u
in Px & u
in Py by
A6;
hence u
in (Px
/\ Py) by
XBOOLE_0:def 4;
end;
then (Px
/\ Py)
c= Pxy & Pxy
c= (Px
/\ Py);
hence thesis by
A2;
end;
suppose
A7: not x is
empty & not y is
empty & (x
/\ y) is
empty;
then
A8: (
product
<*x*>)
= the set of all
<*t*> where t be
Element of x & (
product
<*y*>)
= the set of all
<*t*> where t be
Element of y by
Thm23;
set Px = the set of all
<*t*> where t be
Element of x;
set Py = the set of all
<*t*> where t be
Element of y;
(Px
/\ Py)
c=
{}
proof
let t be
object;
assume t
in (Px
/\ Py);
then
A9: t
in Px & t
in Py by
XBOOLE_0:def 4;
then
consider t1 be
Element of x such that
A10: t
=
<*t1*>;
consider t2 be
Element of y such that
A11: t
=
<*t2*> by
A9;
t1
= t2 by
A10,
A11,
FINSEQ_1: 76;
hence thesis by
A7,
XBOOLE_0:def 4;
end;
hence thesis by
A8,
A7;
end;
suppose x is
empty or y is
empty;
hence thesis by
Thm22;
end;
end;
theorem ::
SRINGS_4:27
Thm26: for x,y be
set holds ((
product
<*x*>)
\ (
product
<*y*>))
= (
product
<*(x
\ y)*>)
proof
let x,y be
set;
per cases ;
suppose
A1: not x is
empty & not y is
empty & not (x
\ y) is
empty;
then
A2: (
product
<*x*>)
= the set of all
<*t*> where t be
Element of x & (
product
<*y*>)
= the set of all
<*t*> where t be
Element of y & (
product
<*(x
\ y)*>)
= the set of all
<*t*> where t be
Element of (x
\ y) by
Thm23;
set Px = the set of all
<*t*> where t be
Element of x;
set Py = the set of all
<*t*> where t be
Element of y;
set Pxy = the set of all
<*t*> where t be
Element of (x
\ y);
now
hereby
let u be
object;
assume u
in (Px
\ Py);
then
A3: u
in Px & not u
in Py by
XBOOLE_0:def 5;
then
consider ux be
Element of x such that
A4: u
=
<*ux*>;
not ux
in y by
A3,
A4;
then ux
in (x
\ y) by
A1,
XBOOLE_0:def 5;
hence u
in Pxy by
A4;
end;
let u be
object;
assume u
in Pxy;
then
consider uxy be
Element of (x
\ y) such that
A5: u
=
<*uxy*>;
A6: uxy is
Element of x & not uxy is
Element of y by
A1,
XBOOLE_0:def 5;
now
assume u
in Py;
then
consider a be
Element of y such that
A7:
<*uxy*>
=
<*a*> by
A5;
thus contradiction by
A7,
A6,
FINSEQ_1: 76;
end;
then u
in Px & not u
in Py by
A5,
A6;
hence u
in (Px
\ Py) by
XBOOLE_0:def 5;
end;
then (Px
\ Py)
c= Pxy & Pxy
c= (Px
\ Py);
hence thesis by
A2;
end;
suppose
A8: not x is
empty & not y is
empty & (x
\ y) is
empty;
then
A9: (
product
<*x*>)
= the set of all
<*t*> where t be
Element of x & (
product
<*y*>)
= the set of all
<*t*> where t be
Element of y by
Thm23;
set Px = the set of all
<*t*> where t be
Element of x;
set Py = the set of all
<*t*> where t be
Element of y;
(Px
\ Py)
c=
{}
proof
let t be
object;
assume t
in (Px
\ Py);
then
A10: t
in Px & not t
in Py by
XBOOLE_0:def 5;
then
consider t1 be
Element of x such that
A11: t
=
<*t1*>;
not t1
in y by
A10,
A11;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
hence thesis by
A8,
A9;
end;
suppose x is
empty or y is
empty;
hence thesis by
Thm22;
end;
end;
theorem ::
SRINGS_4:28
Thm27: for X be
non-empty1
-element
FinSequence, S be
SemiringFamily of X holds the set of all (
product
<*s*>) where s be
Element of (S
. 1) is
semiring_of_sets of the set of all
<*x*> where x be
Element of (X
. 1)
proof
let X be
non-empty1
-element
FinSequence, S be
SemiringFamily of X;
S is
SemiringFamily of X & 1
in (
Seg 1) by
FINSEQ_1: 3;
then
A1: (S
. 1) is
semiring_of_sets of (X
. 1) by
Def2;
set S1 = the set of all (
product
<*s*>) where s be
Element of (S
. 1);
set X1 = the set of all
<*x*> where x be
Element of (X
. 1);
now
S1
c= (
bool X1)
proof
let x be
object;
assume
A2: x
in S1;
then
consider s0 be
Element of (S
. 1) such that
A3: x
= (
product
<*s0*>);
per cases ;
suppose
A4: s0 is non
empty;
reconsider x1 = x as
set by
A2;
x1
c= X1
proof
let y be
object;
assume y
in x1;
then y
in the set of all
<*a*> where a be
Element of s0 by
A3,
A4,
Thm23;
then
consider a be
Element of s0 such that
A6: y
=
<*a*>;
A7: a
in (
union (S
. 1)) by
A4,
A1,
TARSKI:def 4;
(
union (S
. 1))
c= (
union (
bool (X
. 1))) by
A1,
ZFMISC_1: 77;
then (
union (S
. 1))
c= (X
. 1) by
ZFMISC_1: 81;
hence y
in X1 by
A6,
A7;
end;
hence x
in (
bool X1);
end;
suppose
A8: s0 is
empty;
(
product
<*
{} *>)
c= X1;
hence x
in (
bool X1) by
A8,
A3;
end;
end;
then
reconsider S2 = S1 as
Subset-Family of X1;
now
Z:
{} is
Element of (S
. 1) by
A1,
SETFAM_1:def 8;
then
A9:
{}
in S1 by
Thm22;
thus S2 is
with_empty_element by
Z,
Thm22;
now
let s1,s2 be
Element of S2;
assume
A10: (s1
/\ s2) is non
empty;
A11: s1
in S1 & s2
in S2 by
A9;
then
consider sa1 be
Element of (S
. 1) such that
A12: s1
= (
product
<*sa1*>);
consider sa2 be
Element of (S
. 1) such that
A13: s2
= (
product
<*sa2*>) by
A11;
A14: (sa1
/\ sa2) is non
empty by
A12,
A13,
A10,
Thm25,
Thm22;
then
consider ax be
finite
Subset of (S
. 1) such that
A15: ax is
a_partition of (sa1
/\ sa2) by
A1,
SRINGS_1:def 1;
A16: ax is non
empty by
A14,
A15;
set x = the set of all (
product
<*t*>) where t be
Element of ax;
now
deffunc
F(
object) = (
product
<*$1*>);
consider f be
Function such that
A17: (
dom f)
= ax and
A18: for x be
object st x
in ax holds (f
. x)
=
F(x) from
FUNCT_1:sch 3;
(
rng f)
= x
proof
now
hereby
let t be
object;
assume t
in (
rng f);
then
consider q be
object such that
A19: q
in (
dom f) and
A20: t
= (f
. q) by
FUNCT_1:def 3;
t
=
F(q) by
A17,
A19,
A20,
A18;
hence t
in x by
A17,
A19;
end;
let t be
object;
assume t
in x;
then
consider u be
Element of ax such that
A21: t
= (
product
<*u*>);
(f
. u)
=
F(u) by
A18,
A14,
A15;
hence t
in (
rng f) by
A21,
A17,
A14,
A15,
FUNCT_1:def 3;
end;
then x
c= (
rng f) & (
rng f)
c= x;
hence thesis;
end;
hence x is
finite by
A17,
FINSET_1: 8;
x
c= S2
proof
let t be
object;
assume t
in x;
then
consider u be
Element of ax such that
A22: t
= (
product
<*u*>);
u
in ax & ax
c= (S
. 1) by
A16;
hence t
in S2 by
A22;
end;
hence x is
Subset of S2;
now
A23: x
c= (
bool (s1
/\ s2))
proof
let t be
object;
assume t
in x;
then
consider u0 be
Element of ax such that
A24: t
= (
product
<*u0*>);
reconsider t1 = t as
set by
A24;
per cases ;
suppose
A25: t1 is
empty;
{}
c= (s1
/\ s2);
hence thesis by
A25;
end;
suppose
A26: t1 is non
empty;
then
A28: t
= the set of all
<*y*> where y be
Element of u0 by
A24,
Thm22,
Thm23;
t1
c= (s1
/\ s2)
proof
let y be
object;
assume y
in t1;
then
consider z be
Element of u0 such that
A29: y
=
<*z*> by
A28;
A30: (
product
<*(sa1
/\ sa2)*>)
= the set of all
<*a*> where a be
Element of (sa1
/\ sa2) by
A14,
Thm23;
u0
in ax & (
union ax)
= (sa1
/\ sa2) by
A16,
A15,
EQREL_1:def 4;
then z
in (sa1
/\ sa2) by
A24,
A26,
Thm22,
TARSKI:def 4;
then y
in (
product
<*(sa1
/\ sa2)*>) by
A29,
A30;
hence y
in (s1
/\ s2) by
A12,
A13,
Thm25;
end;
hence thesis;
end;
end;
hence x is
Subset-Family of (s1
/\ s2);
now
hereby
let a be
object;
assume a
in (
union x);
then
consider b be
set such that
A31: a
in b and
A32: b
in x by
TARSKI:def 4;
thus a
in (s1
/\ s2) by
A31,
A32,
A23;
end;
let a be
object;
assume a
in (s1
/\ s2);
then
A33: a
in (
product
<*(sa1
/\ sa2)*>) by
A12,
A13,
Thm25;
(
product
<*(sa1
/\ sa2)*>)
= the set of all
<*u*> where u be
Element of (sa1
/\ sa2) by
A14,
Thm23;
then
consider b be
Element of (sa1
/\ sa2) such that
A34: a
=
<*b*> by
A33;
b
in (sa1
/\ sa2) & (
union ax)
= (sa1
/\ sa2) by
A14,
A15,
EQREL_1:def 4;
then
consider d be
set such that
A35: b
in d & d
in ax by
TARSKI:def 4;
A36: (
product
<*d*>)
= the set of all
<*u*> where u be
Element of d by
A35,
Thm23;
<*b*>
in (
product
<*d*>) & (
product
<*d*>)
in x by
A35,
A36;
hence a
in (
union x) by
A34,
TARSKI:def 4;
end;
then (
union x)
c= (s1
/\ s2) & (s1
/\ s2)
c= (
union x);
hence (
union x)
= (s1
/\ s2);
hereby
let A be
Subset of (s1
/\ s2);
assume A
in x;
then
consider a be
Element of ax such that
A37: A
= (
product
<*a*>);
A38: a
in ax by
A16;
A39: A
= the set of all
<*u*> where u be
Element of a by
A14,
A15,
A37,
Thm23;
consider b be
object such that
A40: b
in a by
A14,
A15,
XBOOLE_0:def 1;
<*b*>
in A by
A39,
A40;
hence A
<>
{} ;
let B be
Subset of (s1
/\ s2);
assume B
in x;
then
consider b be
Element of ax such that
A41: B
= (
product
<*b*>);
A42: b
in ax by
A16;
a
misses b implies A
misses B by
A37,
A41,
Thm25,
Thm22;
hence A
= B or A
misses B by
A42,
A38,
A15,
EQREL_1:def 4,
A37,
A41;
end;
end;
hence x is
a_partition of (s1
/\ s2) by
EQREL_1:def 4;
end;
hence ex x be
finite
Subset of S2 st x is
a_partition of (s1
/\ s2);
end;
hence S2 is
cap-finite-partition-closed;
now
let s1,s2 be
Element of S2;
assume
A44: s2
c= s1;
per cases ;
suppose
A45: (s1
\ s2) is
empty;
now
{}
c= S2;
hence
{} is
finite
Subset of S2;
thus
{} is
a_partition of
{} by
EQREL_1: 45;
end;
hence ex x be
finite
Subset of S2 st x is
a_partition of (s1
\ s2) by
A45;
end;
suppose
A46: (s1
\ s2) is non
empty & s2 is
empty;
now
{s1}
c= S2
proof
let t be
object;
assume t
in
{s1};
then t
= s1 by
TARSKI:def 1;
hence thesis by
A9;
end;
hence
{s1} is
finite
Subset of S2;
thus
{s1} is
a_partition of s1 by
A46,
EQREL_1: 39;
end;
hence ex x be
finite
Subset of S2 st x is
a_partition of (s1
\ s2) by
A46;
end;
suppose
A47: (s1
\ s2) is non
empty & s2 is non
empty;
A48: s1
in S1 & s2
in S2 by
A9;
then
consider sa1 be
Element of (S
. 1) such that
A49: s1
= (
product
<*sa1*>);
consider sa2 be
Element of (S
. 1) such that
A50: s2
= (
product
<*sa2*>) by
A48;
A51: sa1 is non
empty by
A47,
A49;
A52: (
product
<*sa1*>)
= the set of all
<*u*> where u be
Element of sa1 by
A47,
A49,
Thm22,
Thm23;
A53: (
product
<*sa2*>)
= the set of all
<*u*> where u be
Element of sa2 by
A47,
A50,
Thm22,
Thm23;
sa2
c= sa1
proof
assume not sa2
c= sa1;
then
consider a be
object such that
A54: a
in sa2 and
A55: not a
in sa1;
<*a*>
in s2 by
A50,
A54,
A53;
then
<*a*>
in (
product
<*sa1*>) by
A44,
A49;
then
consider a0 be
Element of sa1 such that
A56:
<*a*>
=
<*a0*> by
A52;
a
= a0 by
A56,
FINSEQ_1: 76;
hence contradiction by
A51,
A55;
end;
then
consider ax be
finite
Subset of (S
. 1) such that
A57: ax is
a_partition of (sa1
\ sa2) by
A1,
SRINGS_1:def 3;
A58: ax is non
empty
proof
assume ax is
empty;
then (sa1
\ sa2)
=
{} by
A57;
hence contradiction by
A47,
A49,
A50,
Thm26,
Thm22;
end;
A59: (sa1
\ sa2)
<>
{} by
A49,
A50,
A47,
Thm26,
Thm22;
set x = the set of all (
product
<*t*>) where t be
Element of ax;
now
deffunc
F(
object) = (
product
<*$1*>);
consider f be
Function such that
A60: (
dom f)
= ax and
A61: for x be
object st x
in ax holds (f
. x)
=
F(x) from
FUNCT_1:sch 3;
(
rng f)
= x
proof
now
hereby
let t be
object;
assume t
in (
rng f);
then
consider q be
object such that
A62: q
in (
dom f) and
A63: t
= (f
. q) by
FUNCT_1:def 3;
t
= (
product
<*q*>) & q
in ax by
A60,
A61,
A62,
A63;
hence t
in x;
end;
let t be
object;
assume t
in x;
then
consider u be
Element of ax such that
A64: t
= (
product
<*u*>);
(f
. u)
=
F(u) by
A61,
A58;
hence t
in (
rng f) by
A64,
A60,
A58,
FUNCT_1:def 3;
end;
then x
c= (
rng f) & (
rng f)
c= x;
hence thesis;
end;
hence x is
finite by
A60,
FINSET_1: 8;
x
c= S2
proof
let t be
object;
assume t
in x;
then
consider u be
Element of ax such that
A65: t
= (
product
<*u*>);
u
in ax & ax
c= (S
. 1) by
A58;
hence t
in S2 by
A65;
end;
hence x is
Subset of S2;
now
A66: x
c= (
bool (s1
\ s2))
proof
let t be
object;
assume t
in x;
then
consider u0 be
Element of ax such that
A67: t
= (
product
<*u0*>);
reconsider t1 = t as
set by
A67;
per cases ;
suppose
A68: t1 is
empty;
{}
c= (s1
\ s2);
hence thesis by
A68;
end;
suppose
A69: t1 is non
empty;
then
A71: t
= the set of all
<*y*> where y be
Element of u0 by
A67,
Thm22,
Thm23;
t1
c= (s1
\ s2)
proof
let y be
object;
assume y
in t1;
then
consider z be
Element of u0 such that
A72: y
=
<*z*> by
A71;
A73: (
product
<*(sa1
\ sa2)*>)
= the set of all
<*a*> where a be
Element of (sa1
\ sa2) by
A59,
Thm23;
u0
in ax & (
union ax)
= (sa1
\ sa2) by
A57,
A58,
EQREL_1:def 4;
then z
in (sa1
\ sa2) by
A67,
A69,
Thm22,
TARSKI:def 4;
then y
in (
product
<*(sa1
\ sa2)*>) by
A72,
A73;
hence y
in (s1
\ s2) by
A49,
A50,
Thm26;
end;
hence thesis;
end;
end;
hence x is
Subset-Family of (s1
\ s2);
now
hereby
let a be
object;
assume a
in (
union x);
then
consider b be
set such that
A74: a
in b and
A75: b
in x by
TARSKI:def 4;
thus a
in (s1
\ s2) by
A66,
A74,
A75;
end;
let a be
object;
assume
A76: a
in (s1
\ s2);
A77: a
in (
product
<*(sa1
\ sa2)*>) by
Thm26,
A76,
A49,
A50;
(
product
<*(sa1
\ sa2)*>)
= the set of all
<*u*> where u be
Element of (sa1
\ sa2) by
A59,
Thm23;
then
consider b be
Element of (sa1
\ sa2) such that
A78: a
=
<*b*> by
A77;
b
in (sa1
\ sa2) & (
union ax)
= (sa1
\ sa2) by
A59,
A57,
EQREL_1:def 4;
then
consider d be
set such that
A79: b
in d & d
in ax by
TARSKI:def 4;
A80: (
product
<*d*>)
= the set of all
<*u*> where u be
Element of d by
Thm23,
A79;
<*b*>
in (
product
<*d*>) & (
product
<*d*>)
in x by
A79,
A80;
hence a
in (
union x) by
A78,
TARSKI:def 4;
end;
then (
union x)
c= (s1
\ s2) & (s1
\ s2)
c= (
union x);
hence (
union x)
= (s1
\ s2);
hereby
let A be
Subset of (s1
\ s2);
assume A
in x;
then
consider a be
Element of ax such that
A81: A
= (
product
<*a*>);
A82: a
in ax by
A58;
A83: A
= the set of all
<*u*> where u be
Element of a by
A57,
A58,
A81,
Thm23;
consider b be
object such that
A84: b
in a by
A57,
A58,
XBOOLE_0:def 1;
<*b*>
in A by
A83,
A84;
hence A
<>
{} ;
let B be
Subset of (s1
\ s2);
assume B
in x;
then
consider b be
Element of ax such that
A85: B
= (
product
<*b*>);
A86: b
in ax by
A58;
a
misses b implies A
misses B by
A81,
A85,
Thm25,
Thm22;
hence A
= B or A
misses B by
A86,
A81,
A85,
A82,
A57,
EQREL_1:def 4;
end;
end;
hence x is
a_partition of (s1
\ s2) by
EQREL_1:def 4;
end;
hence ex x be
finite
Subset of S2 st x is
a_partition of (s1
\ s2);
end;
end;
hence S2 is
diff-c=-finite-partition-closed;
end;
hence S1 is
semiring_of_sets of X1;
end;
hence thesis;
end;
theorem ::
SRINGS_4:29
Thm28: for X be
non-empty1
-element
FinSequence, S be
SemiringFamily of X holds (
SemiringProduct S) is
semiring_of_sets of (
product X)
proof
let X be
non-empty1
-element
FinSequence, S be
SemiringFamily of X;
set S1 = the set of all (
product
<*s*>) where s be
Element of (S
. 1);
set X1 = the set of all
<*x*> where x be
Element of (X
. 1);
S1
= (
SemiringProduct S) & X1
= (
product X) by
Thm21,
Thm24;
hence thesis by
Thm27;
end;
theorem ::
SRINGS_4:30
Thm29: for X1,X2 be
set, S1 be
semiring_of_sets of X1, S2 be
semiring_of_sets of X2 holds the set of all
[:s1, s2:] where s1 be
Element of S1, s2 be
Element of S2 is
semiring_of_sets of
[:X1, X2:]
proof
let X1,X2 be
set, S1 be
semiring_of_sets of X1, S2 be
semiring_of_sets of X2;
set S = { s where s be
Subset of
[:X1, X2:] : ex x1,x2 be
set st x1
in S1 & x2
in S2 & s
=
[:x1, x2:] };
S is
semiring_of_sets of
[:X1, X2:] by
SRINGS_2: 7;
hence thesis by
SRINGS_2: 2;
end;
theorem ::
SRINGS_4:31
Thm30: for Xn be
non-emptyn
-element
FinSequence, X1 be
non-empty1
-element
FinSequence, Sn be
SemiringFamily of Xn, S1 be
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 be
Subset-Family of
[:(
product Xn), (
product X1):] st S12
= the set of all
[:s1, s2:] where s1 be
Element of (
SemiringProduct Sn), s2 be
Element of (
SemiringProduct S1) holds ex I be
Function of
[:(
product Xn), (
product X1):], (
product (Xn
^ X1)) st I is
one-to-one & I is
onto & (for x,y be
FinSequence st x
in (
product Xn) & y
in (
product X1) holds (I
. (x,y))
= (x
^ y)) & (I
.: S12)
= (
SemiringProduct (Sn
^ S1))
proof
let Xn be
non-emptyn
-element
FinSequence, X1 be
non-empty1
-element
FinSequence, Sn be
SemiringFamily of Xn, S1 be
SemiringFamily of X1;
assume that
A1: (
SemiringProduct Sn) is
semiring_of_sets of (
product Xn) and
A2: (
SemiringProduct S1) is
semiring_of_sets of (
product X1);
let S12 be
Subset-Family of
[:(
product Xn), (
product X1):] such that
A2b: S12
= the set of all
[:s1, s2:] where s1 be
Element of (
SemiringProduct Sn), s2 be
Element of (
SemiringProduct S1);
reconsider S12 as
semiring_of_sets of
[:(
product Xn), (
product X1):] by
A1,
A2,
A2b,
Thm29;
A3: 1
in (
Seg 1) & S1 is
SemiringFamily of X1 by
FINSEQ_1: 3;
then
A4: (S1
. 1) is
semiring_of_sets of (X1
. 1) by
Def2;
A5: (S1
. 1) is non
empty by
A3,
Def2;
A6: 1
in (
Seg 1) by
FINSEQ_1: 3;
then
A7: (
union (S1
. 1))
c= (X1
. 1) by
Thm17;
consider I be
Function of
[:(
product Xn), (
product X1):], (
product (Xn
^ X1)) such that
A8: I is
one-to-one and
A9: I is
onto and
A10: for x,y be
FinSequence st x
in (
product Xn) & y
in (
product X1) holds (I
. (x,y))
= (x
^ y) by
PRVECT_3: 6;
take I;
(I
.: S12)
= (
SemiringProduct (Sn
^ S1))
proof
hereby
let t be
object;
assume t
in (I
.: S12);
then
consider s12 be
Subset of
[:(
product Xn), (
product X1):] such that
A12: s12
in S12 and
A13: t
= (I
.: s12) by
FUNCT_2:def 10;
consider s1 be
Element of (
SemiringProduct Sn), s2 be
Element of (
SemiringProduct S1) such that
A14: s12
=
[:s1, s2:] by
A2b,
A12;
consider g1 be
Function such that
A15: s1
= (
product g1) and
A16: g1
in (
product Sn) by
A1,
Def3;
A17: s2
in (
SemiringProduct S1) by
A2;
s2
in the set of all (
product
<*s*>) where s be
Element of (S1
. 1) by
A17,
Thm24;
then
consider s11 be
Element of (S1
. 1) such that
A18: s2
= (
product
<*s11*>);
reconsider g1 as n
-element
FinSequence by
A16,
Thm18;
A19: (
dom Xn)
= (
Seg n) & (
dom Sn)
= (
Seg n) & (
dom X1)
= (
Seg 1) & (
dom S1)
= (
Seg 1) by
FINSEQ_1: 89;
A20: (
dom g1)
= (
Seg n) by
FINSEQ_1: 89;
A21: (
len g1)
= n by
FINSEQ_3: 153;
A22: (
dom (g1
^
<*s11*>))
= (
Seg (n
+ 1)) by
FINSEQ_1: 89;
A23: (
dom I)
=
[:(
product Xn), (
product X1):] by
FUNCT_2:def 1;
now
(
product (g1
^
<*s11*>))
= (I
.:
[:(
product g1), (
product
<*s11*>):])
proof
hereby
let u be
object;
assume u
in (
product (g1
^
<*s11*>));
then
consider v be
Function such that
A24: u
= v and
A25: (
dom v)
= (
dom (g1
^
<*s11*>)) and
A26: for y be
object st y
in (
dom (g1
^
<*s11*>)) holds (v
. y)
in ((g1
^
<*s11*>)
. y) by
CARD_3:def 5;
A27: (
dom v)
= (
Seg (n
+ 1)) by
A25,
FINSEQ_1: 89;
then
reconsider v as
FinSequence by
FINSEQ_1:def 2;
(
card (
dom v))
= (
card (
Seg (n
+ 1))) by
A25,
FINSEQ_1: 89;
then (
card (
dom v))
= (n
+ 1) by
FINSEQ_1: 57;
then (
card v)
= (n
+ 1) by
CARD_1: 62;
then
reconsider v as (n
+ 1)
-element
FinSequence by
CARD_1:def 7;
reconsider v1 = (v
| (
Seg n)) as
FinSequence by
FINSEQ_1: 15;
(
len v)
= (n
+ 1) by
FINSEQ_3: 153;
then
A28: n
<= (
len v) by
NAT_1: 11;
then
A29: (
dom v1)
= (
Seg n) by
FINSEQ_1: 17;
set w =
[(v
| (
Seg n)),
<*(v
. (n
+ 1))*>];
A30:
now
now
A31: (
dom (v
| (
Seg n)))
= (
Seg n) & (
dom Xn)
= (
Seg n) by
A29,
FINSEQ_1: 89;
thus (
dom (v
| (
Seg n)))
= (
dom Xn) by
A29,
FINSEQ_1: 89;
let y be
object;
assume
A32: y
in (
dom Xn);
then
A33: y
in (
Seg n) & (
Seg n)
c= (
Seg (n
+ 1)) by
FINSEQ_1: 89,
FINSEQ_3: 18;
y
in (
dom (v
| (
Seg n))) by
A32,
FINSEQ_1: 89,
A29;
then
A34: ((v
| (
Seg n))
. y)
= (v
. y) by
FUNCT_1: 47;
A35: (v
. y)
in ((g1
^
<*s11*>)
. y) by
A33,
A22,
A26;
A36: ((v
| (
Seg n))
. y)
in (g1
. y) by
A34,
A35,
A32,
A20,
A31,
FINSEQ_1:def 7;
A37: g1
in (
product Sn) & y
in (
dom Sn) by
A16,
A32,
Thm16;
consider gg be
Function such that
A38: gg
= g1 and (
dom gg)
= (
dom Sn) and
A39: for y be
object st y
in (
dom Sn) holds (gg
. y)
in (Sn
. y) by
A16,
CARD_3:def 5;
(g1
. y)
in (Sn
. y) by
A37,
A38,
A39;
then
A40: ((v
| (
Seg n))
. y)
in (
union (Sn
. y)) & y
in (
Seg n) by
A32,
FINSEQ_1: 89,
A36,
TARSKI:def 4;
(
union (Sn
. y))
c= (Xn
. y) by
A33,
Thm17;
hence ((v
| (
Seg n))
. y)
in (Xn
. y) by
A40;
end;
hence (v
| (
Seg n))
in (
product Xn) by
CARD_3:def 5;
A41: (v
. (n
+ 1))
in ((g1
^
<*s11*>)
. (n
+ 1)) by
A22,
FINSEQ_1: 4,
A26;
((g1
^
<*s11*>)
. (n
+ 1))
= s11 by
A21,
FINSEQ_1: 42;
then (v
. (n
+ 1))
in (
union (S1
. 1)) & (
union (S1
. 1))
c= (X1
. 1) by
A41,
A5,
A6,
Thm17,
TARSKI:def 4;
then
<*(v
. (n
+ 1))*>
in the set of all
<*a*> where a be
Element of (X1
. 1);
hence
<*(v
. (n
+ 1))*>
in (
product X1) by
Thm21;
end;
now
thus w
in (
dom I) by
ZFMISC_1:def 2,
A30,
A23;
now
now
thus (
dom v1)
= (
dom g1) by
A28,
FINSEQ_1: 17,
A20;
now
let y be
object;
assume
A42: y
in (
dom g1);
then
A43: y
in (
Seg n) & (
Seg n)
c= (
Seg (n
+ 1)) by
FINSEQ_1: 89,
FINSEQ_3: 18;
A44: ((v
| (
Seg n))
. y)
= (v
. y) by
A42,
A20,
A29,
FUNCT_1: 47;
(v
. y)
in ((g1
^
<*s11*>)
. y) by
A43,
A22,
A26;
hence (v1
. y)
in (g1
. y) by
A44,
A42,
FINSEQ_1:def 7;
end;
hence for y be
object st y
in (
dom g1) holds (v1
. y)
in (g1
. y);
end;
hence (v
| (
Seg n))
in (
product g1) by
CARD_3:def 5;
A46: (v
. (n
+ 1))
in ((g1
^
<*s11*>)
. (n
+ 1)) by
A22,
A26,
FINSEQ_1: 4;
now
(
dom
<*(v
. (n
+ 1))*>)
= (
Seg 1) & (
dom
<*s11*>)
= (
Seg 1) by
FINSEQ_1:def 8;
hence (
dom
<*(v
. (n
+ 1))*>)
= (
dom
<*s11*>);
let y be
object;
assume y
in (
dom
<*s11*>);
then y
in (
Seg 1) & (
Seg 1)
=
{1} by
FINSEQ_1:def 8,
FINSEQ_1: 2;
then
A47: y
= 1 by
TARSKI:def 1;
(
<*(v
. (n
+ 1))*>
. 1)
= (v
. (n
+ 1)) & (
<*s11*>
. 1)
= s11 by
FINSEQ_1:def 8;
hence (
<*(v
. (n
+ 1))*>
. y)
in (
<*s11*>
. y) by
A21,
A46,
FINSEQ_1: 42,
A47;
end;
hence
<*(v
. (n
+ 1))*>
in (
product
<*s11*>) by
CARD_3:def 5;
end;
hence w
in
[:(
product g1), (
product
<*s11*>):] by
ZFMISC_1:def 2;
A48: (I
. w)
= (I
. (v1,
<*(v
. (n
+ 1))*>)) by
BINOP_1:def 1;
(v1
^
<*(v
. (n
+ 1))*>)
= (v
| (
Seg (n
+ 1))) by
A27,
FINSEQ_1: 4,
FINSEQ_5: 10;
hence u
= (I
. w) by
A48,
A30,
A10,
A24,
A27;
end;
hence u
in (I
.:
[:(
product g1), (
product
<*s11*>):]) by
FUNCT_1:def 6;
end;
let u be
object;
assume u
in (I
.:
[:(
product g1), (
product
<*s11*>):]);
then
consider v be
object such that v
in (
dom I) and
A50: v
in
[:(
product g1), (
product
<*s11*>):] and
A51: u
= (I
. v) by
FUNCT_1:def 6;
consider va,vb be
object such that
A52: va
in (
product g1) and
A53: vb
in (
product
<*s11*>) and
A54: v
=
[va, vb] by
A50,
ZFMISC_1:def 2;
consider wa be
Function such that
A55: wa
= va and
A56: (
dom wa)
= (
dom g1) and
A57: for y be
object st y
in (
dom g1) holds (wa
. y)
in (g1
. y) by
A52,
CARD_3:def 5;
consider wb be
Function such that
A58: wb
= vb and
A59: (
dom wb)
= (
dom
<*s11*>) and
A60: for y be
object st y
in (
dom
<*s11*>) holds (wb
. y)
in (
<*s11*>
. y) by
A53,
CARD_3:def 5;
A61: (
dom g1)
= (
Seg n) by
FINSEQ_1: 89;
then
reconsider wa as
FinSequence by
A56,
FINSEQ_1:def 2;
reconsider wa as n
-element
FinSequence by
A55,
A52,
Thm18;
reconsider wb as
FinSequence by
A59,
FINSEQ_1:def 8,
FINSEQ_1:def 2;
(
card (
dom wb))
= 1 by
A59,
CARD_1:def 7;
then (
card wb)
= 1 by
CARD_1: 62;
then
reconsider wb as 1
-element
FinSequence by
CARD_1:def 7;
reconsider w = (wa
^ wb) as (n
+ 1)
-element
FinSequence;
now
A62:
now
now
thus (
dom wa)
= (
dom Xn) by
FINSEQ_1: 89,
A19;
let y be
object;
assume
A63: y
in (
dom Xn);
then y
in (
dom g1) by
FINSEQ_1: 89,
A19;
then
A64: (wa
. y)
in (g1
. y) by
A57;
consider gg1 be
Function such that
A65: gg1
= g1 and (
dom gg1)
= (
dom Sn) and
A66: for y be
object st y
in (
dom Sn) holds (gg1
. y)
in (Sn
. y) by
A16,
CARD_3:def 5;
(g1
. y)
in (Sn
. y) by
A63,
A19,
A65,
A66;
then
A67: (wa
. y)
in (
union (Sn
. y)) by
A64,
TARSKI:def 4;
(
union (Sn
. y))
c= (Xn
. y) by
A63,
A19,
Thm17;
hence (wa
. y)
in (Xn
. y) by
A67;
end;
hence wa
in (
product Xn) by
CARD_3:def 5;
now
thus (
dom wb)
= (
dom X1) by
FINSEQ_1: 89,
A19;
let y be
object;
assume
A68: y
in (
dom X1);
y
in (
dom
<*s11*>) by
A68,
A19,
FINSEQ_1:def 8;
then
A69: (wb
. y)
in (
<*s11*>
. y) by
A60;
A70: y
= 1 by
A68,
A19,
FINSEQ_1: 2,
TARSKI:def 1;
then
A71: (wb
. y)
in s11 by
A69,
FINSEQ_1:def 8;
(wb
. y)
in (
union (S1
. 1)) by
A71,
A5,
TARSKI:def 4;
hence (wb
. y)
in (X1
. y) by
A70,
A7;
end;
hence wb
in (
product X1) by
CARD_3:def 5;
end;
(I
.
[va, vb])
= (I
. (wa,wb)) by
A55,
A58,
BINOP_1:def 1;
hence u
= w by
A54,
A51,
A10,
A62;
A73: (
dom (g1
^
<*s11*>))
= (
Seg (n
+ 1)) & (
dom w)
= (
Seg (n
+ 1)) by
FINSEQ_1: 89;
hence (
dom w)
= (
dom (g1
^
<*s11*>));
hereby
let y be
object;
assume y
in (
dom (g1
^
<*s11*>));
then y
in ((
Seg n)
\/
{(n
+ 1)}) by
A73,
FINSEQ_1: 9;
then y
in (
Seg n) or y
in
{(n
+ 1)} by
XBOOLE_0:def 3;
per cases by
TARSKI:def 1;
suppose
A74: y
in (
Seg n);
then
A75: y
in (
dom g1) by
FINSEQ_1: 89;
((g1
^
<*s11*>)
. y)
= (g1
. y) & (wa
. y)
in (g1
. y) by
A74,
A61,
A57,
FINSEQ_1:def 7;
hence (w
. y)
in ((g1
^
<*s11*>)
. y) by
A56,
FINSEQ_1:def 7,
A75;
end;
suppose
A77: y
= (n
+ 1);
then
A78: ((g1
^
<*s11*>)
. y)
= s11 by
A21,
FINSEQ_1: 42;
(
dom wb)
= (
dom X1) by
FINSEQ_1: 89,
A19;
then 1
in (
dom wb) by
A19,
FINSEQ_1: 2,
TARSKI:def 1;
then
A79: (wb
. 1)
= (w
. ((
len wa)
+ 1)) by
FINSEQ_1:def 7;
A80: ((
len wa)
+ 1)
= (n
+ 1) by
FINSEQ_3: 153;
1
in (
Seg 1) by
FINSEQ_1: 3;
then 1
in (
dom
<*s11*>) by
FINSEQ_1:def 8;
then (w
. y)
in (
<*s11*>
. 1) by
A60,
A80,
A77,
A79;
hence (w
. y)
in ((g1
^
<*s11*>)
. y) by
A78,
FINSEQ_1:def 8;
end;
end;
end;
hence u
in (
product (g1
^
<*s11*>)) by
CARD_3:def 5;
end;
hence t
= (
product (g1
^
<*s11*>)) by
A13,
A14,
A15,
A18;
now
A81: (
len (Sn
^ S1))
= (n
+ 1) by
FINSEQ_3: 153;
then
A82: (
dom (Sn
^ S1))
= (
Seg (n
+ 1)) by
FINSEQ_1:def 3;
thus (
dom (g1
^
<*s11*>))
= (
dom (Sn
^ S1)) by
A81,
A22,
FINSEQ_1:def 3;
let u be
object;
assume u
in (
dom (Sn
^ S1));
then u
in ((
Seg n)
\/
{(n
+ 1)}) by
A82,
FINSEQ_1: 9;
then u
in (
Seg n) or u
in
{(n
+ 1)} by
XBOOLE_0:def 3;
per cases by
TARSKI:def 1;
suppose
A83: u
in (
Seg n);
then
A84: u
in (
dom Sn) by
FINSEQ_1: 89;
A85: ((Sn
^ S1)
. u)
= (Sn
. u) by
A19,
A83,
FINSEQ_1:def 7;
(
dom g1)
= (
Seg n) by
FINSEQ_1: 89;
then
A86: ((g1
^
<*s11*>)
. u)
= (g1
. u) by
A83,
FINSEQ_1:def 7;
consider gg1 be
Function such that
A87: g1
= gg1 and (
dom gg1)
= (
dom Sn) and
A88: for y be
object st y
in (
dom Sn) holds (gg1
. y)
in (Sn
. y) by
A16,
CARD_3:def 5;
thus ((g1
^
<*s11*>)
. u)
in ((Sn
^ S1)
. u) by
A87,
A88,
A84,
A86,
A85;
end;
suppose
A89: u
= (n
+ 1);
then
A90: ((g1
^
<*s11*>)
. u)
= s11 by
A21,
FINSEQ_1: 42;
A91: s11
in (S1
. 1) by
A5;
1
in (
dom S1) & (
len Sn)
= n by
A19,
FINSEQ_1: 3,
FINSEQ_3: 153;
hence ((g1
^
<*s11*>)
. u)
in ((Sn
^ S1)
. u) by
A89,
A90,
A91,
FINSEQ_1:def 7;
end;
end;
hence (g1
^
<*s11*>)
in (
product (Sn
^ S1)) by
CARD_3:def 5;
end;
hence t
in (
SemiringProduct (Sn
^ S1)) by
Def3;
end;
let t be
object;
assume t
in (
SemiringProduct (Sn
^ S1));
then
consider f be
Function such that
A92: t
= (
product f) and
A93: f
in (
product (Sn
^ S1)) by
Def3;
consider g be
Function such that
A94: f
= g and
A95: (
dom g)
= (
dom (Sn
^ S1)) and
A96: for y be
object st y
in (
dom (Sn
^ S1)) holds (g
. y)
in ((Sn
^ S1)
. y) by
A93,
CARD_3:def 5;
A97: (
dom Xn)
= (
Seg n) & (
dom Sn)
= (
Seg n) & (
dom X1)
= (
Seg 1) & (
dom S1)
= (
Seg 1) by
FINSEQ_1: 89;
(
dom X1)
=
{1} & (
dom S1)
=
{1} by
FINSEQ_1: 2,
FINSEQ_1: 89;
then
A98: 1
in (
dom X1) & 1
in (
dom S1) by
TARSKI:def 1;
A99: (
len Xn)
= n & (
len Sn)
= n & (
len X1)
= 1 & (
len S1)
= 1 by
FINSEQ_3: 153;
A100: (
len (Sn
^ S1))
= (n
+ 1) by
FINSEQ_3: 153;
then
A101: (
dom (Sn
^ S1))
= (
Seg (n
+ 1)) by
FINSEQ_1:def 3;
(
dom g)
= (
Seg (n
+ 1)) by
A95,
A100,
FINSEQ_1:def 3;
then
reconsider g as
FinSequence by
FINSEQ_1:def 2;
(
card (
dom g))
= (n
+ 1) by
A95,
CARD_1:def 7;
then (
card g)
= (n
+ 1) by
CARD_1: 62;
then
reconsider g as (n
+ 1)
-element
FinSequence by
CARD_1:def 7;
reconsider t0 = t as
set by
TARSKI: 1;
now
let a be
object;
assume a
in (
product f);
then
consider b be
Function such that
A102: a
= b and
A103: (
dom b)
= (
dom f) and
A104: for y be
object st y
in (
dom f) holds (b
. y)
in (f
. y) by
CARD_3:def 5;
now
take b;
thus a
= b by
A102;
(
len (Sn
^ S1))
= (n
+ 1) by
FINSEQ_3: 153;
then
A105: (
dom (Sn
^ S1))
= (
Seg (n
+ 1)) by
FINSEQ_1:def 3;
A106: (
dom f)
= (
Seg (n
+ 1)) by
A105,
A93,
CARD_3: 9;
A107: (
dom b)
= (
Seg (n
+ 1)) by
A103,
A105,
A93,
CARD_3: 9;
A108: (
len (Xn
^ X1))
= (n
+ 1) by
FINSEQ_3: 153;
then
A109: (
dom (Xn
^ X1))
= (
Seg (n
+ 1)) by
FINSEQ_1:def 3;
thus (
dom b)
= (
dom (Xn
^ X1)) by
A108,
A107,
FINSEQ_1:def 3;
let y be
object;
assume
A110: y
in (
dom (Xn
^ X1));
then
A111: (b
. y)
in (f
. y) by
A104,
A106,
A109;
(g
. y)
in ((Sn
^ S1)
. y) by
A96,
A105,
A109,
A110;
then
A112: (b
. y)
in (
union ((Sn
^ S1)
. y)) by
A111,
A94,
TARSKI:def 4;
y
in ((
Seg n)
\/
{(n
+ 1)}) by
A110,
A109,
FINSEQ_1: 9;
then y
in (
Seg n) or y
in
{(n
+ 1)} by
XBOOLE_0:def 3;
per cases by
TARSKI:def 1;
suppose
A113: y
in (
Seg n);
then
A114: ((Xn
^ X1)
. y)
= (Xn
. y) by
A97,
FINSEQ_1:def 7;
(Sn
. y) is
semiring_of_sets of (Xn
. y) by
A113,
Def2;
then (
union (Sn
. y))
c= (
union (
bool (Xn
. y))) by
ZFMISC_1: 77;
then (
union (Sn
. y))
c= (Xn
. y) & (
union ((Sn
^ S1)
. y))
= (
union (Sn
. y)) by
ZFMISC_1: 81,
A97,
A113,
FINSEQ_1:def 7;
hence (b
. y)
in ((Xn
^ X1)
. y) by
A112,
A114;
end;
suppose
A116: y
= (n
+ 1);
then
A117: ((Xn
^ X1)
. y)
= (X1
. 1) by
A99,
A98,
FINSEQ_1:def 7;
(
union (S1
. 1))
c= (
union (
bool (X1
. 1))) by
A4,
ZFMISC_1: 77;
then (
union (S1
. 1))
c= (X1
. 1) & (
union ((Sn
^ S1)
. y))
= (
union (S1
. 1)) by
A116,
A99,
A98,
FINSEQ_1:def 7,
ZFMISC_1: 81;
hence (b
. y)
in ((Xn
^ X1)
. y) by
A112,
A117;
end;
end;
hence a
in (
product (Xn
^ X1)) by
CARD_3:def 5;
end;
then t0
c= (
product (Xn
^ X1)) by
A92;
then
reconsider t1 = t0 as
Subset of (
product (Xn
^ X1));
reconsider hn = (
product (g
| n)) as
set;
n
<= (n
+ 1) & (
len g)
= (n
+ 1) by
NAT_1: 11,
FINSEQ_3: 153;
then
A118b: (
len (g
| n))
= n by
FINSEQ_1: 59;
then
A119: (
dom (g
| n))
= (
Seg n) by
FINSEQ_1:def 3;
A120:
now
let a be
object;
assume a
in hn;
then
consider b be
Function such that
A121: a
= b and
A122: (
dom b)
= (
dom (g
| n)) and
A123: for y be
object st y
in (
dom (g
| n)) holds (b
. y)
in ((g
| n)
. y) by
CARD_3:def 5;
now
thus (
dom b)
= (
dom Xn) by
A122,
A118b,
FINSEQ_1:def 3,
A97;
let y be
object;
assume
A124: y
in (
dom Xn);
then
A125: y
in (
Seg n) by
FINSEQ_1: 89;
(b
. y)
in ((g
| n)
. y) by
A124,
A97,
A119,
A123;
then (b
. y)
in ((g
| (
Seg n))
. y) by
FINSEQ_1:def 15;
then
A126: (b
. y)
in (g
. y) by
A125,
FUNCT_1: 49;
(
Seg n)
c= (
Seg (n
+ 1)) by
NAT_1: 11,
FINSEQ_1: 5;
then
A127: (g
. y)
in ((Sn
^ S1)
. y) by
A101,
A96,
A125;
(g
. y)
in (Sn
. y) by
A124,
A127,
A97,
FINSEQ_1:def 7;
then
A128: (b
. y)
in (
union (Sn
. y)) by
A126,
TARSKI:def 4;
(Sn
. y) is
semiring_of_sets of (Xn
. y) by
A125,
Def2;
then (
union (Sn
. y))
c= (
union (
bool (Xn
. y))) by
ZFMISC_1: 77;
then (
union (Sn
. y))
c= (Xn
. y) by
ZFMISC_1: 81;
hence (b
. y)
in (Xn
. y) by
A128;
end;
hence a
in (
product Xn) by
A121,
CARD_3:def 5;
end;
then
A129: hn
c= (
product Xn);
reconsider h1 = (
product
<*(g
. (n
+ 1))*>) as
set;
A130:
now
let a be
object;
assume a
in h1;
then
consider b be
Function such that
A131: a
= b and
A132: (
dom b)
= (
dom
<*(g
. (n
+ 1))*>) and
A133: for y be
object st y
in (
dom
<*(g
. (n
+ 1))*>) holds (b
. y)
in (
<*(g
. (n
+ 1))*>
. y) by
CARD_3:def 5;
A134: (
dom
<*(g
. (n
+ 1))*>)
= (
Seg 1) by
FINSEQ_1:def 8;
now
thus (
dom b)
= (
dom X1) by
A132,
FINSEQ_1:def 8,
A97;
let y be
object;
assume
A135: y
in (
dom X1);
then
A136: y
in (
Seg 1) by
FINSEQ_1: 89;
A137: (b
. y)
in (
<*(g
. (n
+ 1))*>
. y) by
A135,
A133,
A134,
A97;
A138: y
= 1 by
A136,
FINSEQ_1: 2,
TARSKI:def 1;
1
in (
dom S1) & (
len Sn)
= n by
A97,
FINSEQ_1: 3,
FINSEQ_3: 153;
then ((Sn
^ S1)
. ((
len Sn)
+ 1))
= (S1
. 1) & (
dom (Sn
^ S1))
= (
Seg (n
+ 1)) by
A99,
FINSEQ_1:def 7;
then (b
. y)
in (g
. (n
+ 1)) & (g
. (n
+ 1))
in (S1
. 1) by
A138,
A137,
FINSEQ_1:def 8,
A96,
A99,
FINSEQ_1: 3;
then
A139: (b
. y)
in (
union (S1
. 1)) by
TARSKI:def 4;
(
union (S1
. 1))
c= (
union (
bool (X1
. 1))) by
A4,
ZFMISC_1: 77;
then (
union (S1
. 1))
c= (X1
. 1) by
ZFMISC_1: 81;
hence (b
. y)
in (X1
. y) by
A139,
A138;
end;
hence a
in (
product X1) by
A131,
CARD_3:def 5;
end;
then h1
c= (
product X1);
then
reconsider s12 =
[:hn, h1:] as
Subset of
[:(
product Xn), (
product X1):] by
A129,
ZFMISC_1: 96;
now
now
now
thus hn
= (
product (g
| n));
now
thus (
dom (g
| n))
= (
dom Sn) by
A119,
FINSEQ_1: 89;
let y be
object;
assume
A140: y
in (
dom Sn);
then
A141: y
in (
Seg n) by
FINSEQ_1: 89;
(
Seg n)
c= (
Seg (n
+ 1)) by
NAT_1: 11,
FINSEQ_1: 5;
then
A142: (g
. y)
in ((Sn
^ S1)
. y) by
A96,
A101,
A141;
A143: (g
. y)
in (Sn
. y) by
A142,
A140,
FINSEQ_1:def 7;
y
in (
dom (g
| (
Seg n))) by
A141,
A119,
FINSEQ_1:def 15;
then (g
. y)
= ((g
| (
Seg n))
. y) by
FUNCT_1: 47;
hence ((g
| n)
. y)
in (Sn
. y) by
A143,
FINSEQ_1:def 15;
end;
hence (g
| n)
in (
product Sn) by
CARD_3:def 5;
end;
hence hn is
Element of (
SemiringProduct Sn) by
Def3;
now
thus h1
= (
product
<*(g
. (n
+ 1))*>);
now
thus (
dom
<*(g
. (n
+ 1))*>)
= (
dom S1) by
FINSEQ_1:def 8,
A97;
let b be
object;
assume b
in (
dom S1);
then
A144: b
= 1 by
A97,
FINSEQ_1: 2,
TARSKI:def 1;
A145: (
<*(g
. (n
+ 1))*>
. 1)
= (g
. (n
+ 1)) by
FINSEQ_1:def 8;
(
<*(g
. (n
+ 1))*>
. 1)
in ((Sn
^ S1)
. (n
+ 1)) & 1
in (
dom S1) by
A96,
FINSEQ_1: 4,
A101,
A145,
A97,
FINSEQ_1: 2,
TARSKI:def 1;
hence (
<*(g
. (n
+ 1))*>
. b)
in (S1
. b) by
A144,
A99,
FINSEQ_1:def 7;
end;
hence
<*(g
. (n
+ 1))*>
in (
product S1) by
CARD_3:def 5;
end;
hence h1 is
Element of (
SemiringProduct S1) by
Def3;
end;
hence s12
in S12 by
A2b;
now
hereby
let u be
object;
assume u
in (I
.:
[:hn, h1:]);
then
consider v be
object such that v
in (
dom I) and
A146: v
in
[:hn, h1:] and
A147: u
= (I
. v) by
FUNCT_1:def 6;
consider va,vb be
object such that
A148: va
in hn and
A149: vb
in h1 and
A150: v
=
[va, vb] by
A146,
ZFMISC_1:def 2;
A151: va
in (
product Xn) & vb
in (
product X1) by
A120,
A130,
A148,
A149;
reconsider va as n
-element
FinSequence by
A120,
A148,
Thm18;
reconsider vb as 1
-element
FinSequence by
A149,
Thm18;
A152: u
= (I
. (va,vb)) by
A147,
A150,
BINOP_1:def 1
.= (va
^ vb) by
A10,
A151;
set vab = (va
^ vb);
(
len (Sn
^ S1))
= (n
+ 1) by
FINSEQ_3: 153;
then
A153: (
dom (Sn
^ S1))
= (
Seg (n
+ 1)) by
FINSEQ_1:def 3;
then
A154: (
dom f)
= (
Seg (n
+ 1)) by
A93,
CARD_3: 9;
A155: (
dom (va
^ vb))
= (
Seg (n
+ 1)) by
FINSEQ_1: 89;
now
thus (
dom vab)
= (
dom f) by
A153,
A93,
CARD_3: 9,
A155;
let y be
object;
assume y
in (
dom f);
then y
in ((
Seg n)
\/
{(n
+ 1)}) by
A154,
FINSEQ_1: 9;
then y
in (
Seg n) or y
in
{(n
+ 1)} by
XBOOLE_0:def 3;
per cases by
TARSKI:def 1;
suppose
A156: y
in (
Seg n);
then
A157: y
in (
dom va) by
FINSEQ_1: 89;
then
A158: (vab
. y)
= (va
. y) by
FINSEQ_1:def 7;
consider va1 be
Function such that
A159: va1
= va and
A160: (
dom va1)
= (
dom (g
| n)) and
A161: for y be
object st y
in (
dom (g
| n)) holds (va1
. y)
in ((g
| n)
. y) by
A148,
CARD_3:def 5;
(va1
. y)
in ((g
| n)
. y) by
A157,
A159,
A160,
A161;
then (va1
. y)
in ((g
| (
Seg n))
. y) by
FINSEQ_1:def 15;
hence (vab
. y)
in (f
. y) by
A94,
A156,
A158,
A159,
FUNCT_1: 49;
end;
suppose
A162: y
= (n
+ 1);
now
(
dom vb)
= (
Seg 1) by
FINSEQ_1: 89;
hence 1
in (
dom vb) by
FINSEQ_1: 2,
TARSKI:def 1;
thus y
= ((
len va)
+ 1) by
A162,
FINSEQ_3: 153;
end;
then
A163: ((va
^ vb)
. y)
= (vb
. 1) by
FINSEQ_1:def 7;
consider vb1 be
Function such that
A164: vb
= vb1 and (
dom vb1)
= (
dom
<*(g
. (n
+ 1))*>) and
A165: for y be
object st y
in (
dom
<*(g
. (n
+ 1))*>) holds (vb1
. y)
in (
<*(g
. (n
+ 1))*>
. y) by
A149,
CARD_3:def 5;
(
dom
<*(g
. (n
+ 1))*>)
= (
Seg 1) by
FINSEQ_1:def 8;
then 1
in (
dom
<*(g
. (n
+ 1))*>) by
FINSEQ_1: 2,
TARSKI:def 1;
then (vb1
. 1)
in (
<*(g
. (n
+ 1))*>
. 1) by
A165;
hence (vab
. y)
in (f
. y) by
A164,
A163,
A162,
A94,
FINSEQ_1:def 8;
end;
end;
hence u
in (
product f) by
A152,
CARD_3:def 5;
end;
let u be
object;
assume u
in (
product f);
then
consider v be
Function such that
A166: u
= v and
A167: (
dom v)
= (
dom f) and
A168: for y be
object st y
in (
dom f) holds (v
. y)
in (f
. y) by
CARD_3:def 5;
(
len (Sn
^ S1))
= (n
+ 1) by
FINSEQ_3: 153;
then
A169: (
dom (Sn
^ S1))
= (
Seg (n
+ 1)) by
FINSEQ_1:def 3;
A170: (
dom f)
= (
Seg (n
+ 1)) by
A93,
A169,
CARD_3: 9;
A171: (
dom v)
= (
Seg (n
+ 1)) by
A93,
A167,
A169,
CARD_3: 9;
reconsider v as
FinSequence by
A93,
A167,
A169,
CARD_3: 9,
FINSEQ_1:def 2;
(
card (
dom v))
= (n
+ 1) by
A171,
FINSEQ_1: 57;
then (
card v)
= (n
+ 1) by
CARD_1: 62;
then
reconsider v as (n
+ 1)
-element
FinSequence by
CARD_1:def 7;
reconsider xn = (v
| (
Seg n)) as
FinSequence by
FINSEQ_1: 15;
reconsider x1 =
<*(v
. (n
+ 1))*> as 1
-element
FinSequence;
A172: xn
in (
product Xn) & x1
in (
product X1)
proof
now
(
len v)
= (n
+ 1) by
FINSEQ_3: 153;
then
A173: n
<= (
len v) by
NAT_1: 11;
then
A174: (
dom xn)
= (
Seg n) by
FINSEQ_1: 17;
thus (
dom xn)
= (
dom Xn) by
A173,
FINSEQ_1: 17,
A97;
let y be
object;
assume
A175: y
in (
dom Xn);
A176: y
in (
Seg n) & (
Seg n)
c= (
Seg (n
+ 1)) by
NAT_1: 11,
A175,
FINSEQ_1: 89,
FINSEQ_1: 5;
A177: (v
. y)
in (f
. y) by
A176,
A170,
A168;
A178: (f
. y)
in ((Sn
^ S1)
. y) by
A176,
A101,
A94,
A96;
A179: (f
. y)
in (Sn
. y) by
A175,
A97,
A178,
FINSEQ_1:def 7;
(Sn
. y) is
semiring_of_sets of (Xn
. y) by
A175,
A97,
Def2;
then (
union (Sn
. y))
c= (
union (
bool (Xn
. y))) by
ZFMISC_1: 77;
then
A180: (
union (Sn
. y))
c= (Xn
. y) by
ZFMISC_1: 81;
(v
. y)
in (
union (Sn
. y)) by
A179,
A177,
TARSKI:def 4;
then (v
. y)
in (Xn
. y) by
A180;
hence (xn
. y)
in (Xn
. y) by
A174,
A175,
A97,
FUNCT_1: 47;
end;
hence xn
in (
product Xn) by
CARD_3:def 5;
now
thus (
dom x1)
= (
dom X1) by
A97,
FINSEQ_1:def 8;
let y be
object;
assume y
in (
dom X1);
then
A181: y
= 1 by
A97,
FINSEQ_1: 2,
TARSKI:def 1;
then
A182: (x1
. y)
= (v
. (n
+ 1)) by
FINSEQ_1:def 8;
1
in (
dom S1) & (
len Sn)
= n by
A97,
FINSEQ_1: 3,
FINSEQ_3: 153;
then ((Sn
^ S1)
. ((
len Sn)
+ 1))
= (S1
. 1) & (
dom (Sn
^ S1))
= (
Seg (n
+ 1)) by
A99,
FINSEQ_1:def 7;
then (v
. (n
+ 1))
in (f
. (n
+ 1)) & (f
. (n
+ 1))
in (S1
. 1) by
A99,
A94,
A96,
A170,
A168,
FINSEQ_1: 4;
then (v
. (n
+ 1))
in (
union (S1
. 1)) & (
union (S1
. 1))
c= (X1
. 1) by
A6,
Thm17,
TARSKI:def 4;
hence (x1
. y)
in (X1
. y) by
A181,
A182;
end;
hence x1
in (
product X1) by
CARD_3:def 5;
end;
set x =
[xn, x1];
now
(
dom I)
=
[:(
product Xn), (
product X1):] by
FUNCT_2:def 1;
hence
[xn, x1]
in (
dom I) by
A172,
ZFMISC_1:def 2;
now
now
(
len v)
= (n
+ 1) by
FINSEQ_3: 153;
then n
<= (
len v) by
NAT_1: 11;
then
A183: (
dom xn)
= (
Seg n) by
FINSEQ_1: 17;
then
A184: (
dom (v
| (
Seg n)))
= (
Seg n) & (
Seg n)
= (
dom (g
| n)) by
A118b,
FINSEQ_1:def 3;
thus
A185: (
dom (v
| (
Seg n)))
= (
dom (g
| n)) by
A183,
A118b,
FINSEQ_1:def 3;
let y be
object;
assume
A186: y
in (
dom (g
| n));
then
A187: ((v
| (
Seg n))
. y)
= (v
. y) by
A185,
FUNCT_1: 47;
(
Seg n)
c= (
Seg (n
+ 1)) & (
dom (g
| n))
= (
Seg n) & (
dom f)
= (
Seg (n
+ 1)) by
NAT_1: 11,
A118b,
FINSEQ_1:def 3,
A93,
A169,
CARD_3: 9,
FINSEQ_1: 5;
then
A188: (v
. y)
in (g
. y) by
A94,
A168,
A186;
((g
| (
Seg n))
. y)
= (g
. y) by
A186,
A184,
FUNCT_1: 49;
hence ((v
| (
Seg n))
. y)
in ((g
| n)
. y) by
A187,
A188,
FINSEQ_1:def 15;
end;
hence xn
in hn by
CARD_3:def 5;
now
(
dom x1)
= (
dom X1) by
A97,
FINSEQ_1:def 8;
hence (
dom x1)
= (
dom
<*(g
. (n
+ 1))*>) by
A97,
FINSEQ_1:def 8;
let y be
object;
assume y
in (
dom
<*(g
. (n
+ 1))*>);
then y
in (
Seg 1) by
FINSEQ_1:def 8;
then
A189: y
= 1 by
FINSEQ_1: 2,
TARSKI:def 1;
then
A190: (
<*(g
. (n
+ 1))*>
. y)
= (g
. (n
+ 1)) by
FINSEQ_1:def 8;
(x1
. y)
= (v
. (n
+ 1)) by
A189,
FINSEQ_1:def 8;
hence (x1
. y)
in (
<*(g
. (n
+ 1))*>
. y) by
A168,
A170,
FINSEQ_1: 4,
A94,
A190;
end;
hence x1
in h1 by
CARD_3:def 5;
thus x
=
[xn, x1];
end;
hence x
in
[:hn, h1:] by
ZFMISC_1:def 2;
now
A191: (I
. x)
= (I
. (xn,x1)) by
BINOP_1:def 1
.= (xn
^ x1) by
A10,
A172;
(xn
^
<*(v
. (n
+ 1))*>)
= (v
| (
Seg (n
+ 1))) by
A171,
FINSEQ_1: 4,
FINSEQ_5: 10;
hence (I
. x)
= v by
A171,
A191;
end;
hence u
= (I
. x) by
A166;
end;
hence u
in (I
.:
[:hn, h1:]) by
FUNCT_1:def 6;
end;
then (I
.:
[:hn, h1:])
c= (
product f) & (
product f)
c= (I
.:
[:hn, h1:]);
hence t1
= (I
.: s12) by
A92;
end;
hence thesis by
FUNCT_2:def 10;
end;
hence thesis by
A8,
A9,
A10;
end;
theorem ::
SRINGS_4:32
Thm31: for Xn be
non-emptyn
-element
FinSequence, X1 be
non-empty1
-element
FinSequence, Sn be
SemiringFamily of Xn, S1 be
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
let Xn be
non-emptyn
-element
FinSequence, X1 be
non-empty1
-element
FinSequence, Sn be
SemiringFamily of Xn, S1 be
SemiringFamily of X1;
assume that
A1: (
SemiringProduct Sn) is
semiring_of_sets of (
product Xn) and
A2: (
SemiringProduct S1) is
semiring_of_sets of (
product X1);
reconsider S12 = the set of all
[:s1, s2:] where s1 be
Element of (
SemiringProduct Sn), s2 be
Element of (
SemiringProduct S1) as
semiring_of_sets of
[:(
product Xn), (
product X1):] by
A1,
A2,
Thm29;
consider I be
Function of
[:(
product Xn), (
product X1):], (
product (Xn
^ X1)) such that
A3: I is
one-to-one and I is
onto and for x,y be
FinSequence st x
in (
product Xn) & y
in (
product X1) holds (I
. (x,y))
= (x
^ y) and
A4: (I
.: S12)
= (
SemiringProduct (Sn
^ S1)) by
A1,
A2,
Thm30;
thus thesis by
A3,
A4,
Thm11,
Thm12;
end;
theorem ::
SRINGS_4:33
Thm32: for S be
SemiringFamily of X holds (
SemiringProduct S) is
semiring_of_sets of (
product X)
proof
let S be
SemiringFamily of X;
reconsider SP = (
SemiringProduct S) as
Subset-Family of (
product X) by
Thm20;
defpred
P[ non
zero
Nat] means for X be
non-empty$1
-element
FinSequence, S be
SemiringFamily of X holds (
SemiringProduct S) is
semiring_of_sets of (
product X);
A1:
P[1] by
Thm28;
A2:
now
let n be non
zero
Nat;
assume
A3:
P[n];
now
let X be
non-empty(n
+ 1)
-element
FinSequence, S be
SemiringFamily of X;
reconsider SPS = (
SemiringProduct S) as
Subset-Family of (
product X) by
Thm20;
consider Xq be
FinSequence, xq be
object such that
A4: X
= (Xq
^
<*xq*>) by
FINSEQ_1: 46;
(
len X)
= ((
len Xq)
+ (
len
<*xq*>)) by
A4,
FINSEQ_1: 22
.= ((
len Xq)
+ 1) by
FINSEQ_1: 39;
then
A5: (
len Xq)
= n by
XCMPLX_1: 2,
FINSEQ_3: 153;
reconsider Xn = Xq as n
-element
FinSequence by
A5,
CARD_1:def 7;
(
rng Xn)
c= (
rng X) by
A4,
FINSEQ_1: 29;
then
A7: not
{}
in (
rng Xn);
reconsider Xn as
non-emptyn
-element
FinSequence by
A7,
RELAT_1:def 9;
reconsider X1 =
<*xq*> as 1
-element
FinSequence;
(
rng X1)
c= (
rng X) by
A4,
FINSEQ_1: 30;
then
A9: not
{}
in (
rng X1);
reconsider X1 as
non-empty1
-element
FinSequence by
A9,
RELAT_1:def 9;
consider Sq be
FinSequence, sq be
object such that
A10: S
= (Sq
^
<*sq*>) by
FINSEQ_1: 46;
(
len S)
= ((
len Sq)
+ (
len
<*sq*>)) by
A10,
FINSEQ_1: 22
.= ((
len Sq)
+ 1) by
FINSEQ_1: 39;
then (
len Sq)
= n by
FINSEQ_3: 153,
XCMPLX_1: 2;
then
reconsider Sn = Sq as n
-element
FinSequence by
CARD_1:def 7;
reconsider S1 =
<*sq*> as 1
-element
FinSequence;
(
Seg (n
+ 1))
= ((
Seg n)
\/
{(n
+ 1)}) by
FINSEQ_1: 9;
then
A11: (
Seg n)
c= (
Seg (n
+ 1)) by
XBOOLE_1: 7;
A12: (
len Xn)
= n & (
len Sn)
= n by
FINSEQ_3: 153;
now
now
let i be
Nat;
assume
A14: i
in (
Seg n);
then i
in (
Seg (
len Xn)) & i
in (
Seg (
len Sn)) by
FINSEQ_3: 153;
then (X
. i)
= ((Xn
^ X1)
. i) & (S
. i)
= ((Sn
^ S1)
. i) & 1
<= i & i
<= (
len Xn) & i
<= (
len Sn) by
A4,
A10,
FINSEQ_1: 1;
then (X
. i)
= (Xn
. i) & (S
. i)
= (Sn
. i) by
FINSEQ_1: 64;
hence (Sn
. i) is
semiring_of_sets of (Xn
. i) by
A14,
A11,
Def2;
end;
hence Sn is
SemiringFamily of Xn by
Def2;
end;
then
A16: Xn is
non-empty & Sn is
SemiringFamily of Xn & (
SemiringProduct Sn) is
semiring_of_sets of (
product Xn) by
A3;
A17: (
len X1)
= 1 by
FINSEQ_1: 39;
then
A18: (X1
. 1)
= (X
. (n
+ 1)) by
FINSEQ_1: 65,
A4,
A12;
(
len S1)
= 1 by
FINSEQ_1: 39;
then
A20: (S1
. 1)
= (S
. (n
+ 1)) by
FINSEQ_1: 65,
A12,
A10;
now
thus X1 is
non-empty;
A23: (n
+ 1)
in (
Seg (n
+ 1)) by
FINSEQ_1: 3;
now
let i be
Nat;
assume i
in (
Seg 1);
then i
= 1 by
TARSKI:def 1,
FINSEQ_1: 2;
hence (S1
. i) is
semiring_of_sets of (X1
. i) by
A23,
A20,
A18,
Def2;
end;
hence (X1
. 1)
= (X
. (n
+ 1)) & S1 is
SemiringFamily of X1 by
A4,
A12,
A17,
FINSEQ_1: 65,
Def2;
end;
then S1 is
SemiringFamily of X1 & (
SemiringProduct S1) is
semiring_of_sets of (
product X1) by
Thm28;
hence (
SemiringProduct S) is
semiring_of_sets of (
product X) by
A16,
Thm31,
A4,
A10;
end;
hence
P[(n
+ 1)];
end;
for n be non
zero
Nat holds
P[n] from
NAT_1:sch 10(
A1,
A2);
hence thesis;
end;
definition
let n be non
zero
Nat, X be
non-emptyn
-element
FinSequence, S be
SemiringFamily of X;
::
SRINGS_4:def5
attr S is
cap-closed-yielding means
:
Def4: for i be
Nat st i
in (
Seg n) holds (S
. i) is
cap-closed;
end
registration
let n be non
zero
Nat, X be
non-emptyn
-element
FinSequence;
cluster
cap-closed-yielding for
SemiringFamily of X;
existence
proof
deffunc
F(
set) = (
bool (X
. $1));
consider p be
FinSequence such that
A1: (
len p)
= n and
A2: for i be
Nat st i
in (
dom p) holds (p
. i)
=
F(i) from
FINSEQ_1:sch 2;
reconsider p as n
-element
FinSequence by
A1,
CARD_1:def 7;
take p;
now
let i be
Nat;
assume
A3: i
in (
Seg n);
reconsider Xi = (X
. i) as
set;
A4: (
bool Xi) is
semiring_of_sets of Xi by
SRINGS_2: 5;
i
in (
dom p) by
A3,
A1,
FINSEQ_1:def 3;
hence (p
. i) is
semiring_of_sets of (X
. i) by
A2,
A4;
end;
then
reconsider p as
SemiringFamily of X by
Def2;
now
let i be
Nat;
assume i
in (
Seg n);
then i
in (
dom p) by
A1,
FINSEQ_1:def 3;
then (p
. i)
= (
bool (X
. i)) by
A2;
hence (p
. i) is
cap-closed;
end;
then p is
cap-closed-yielding;
hence thesis;
end;
end
begin
registration
let X be
set;
cluster
cap-closed for
semiring_of_sets of X;
existence
proof
reconsider S = (
bool X) as
semiring_of_sets of X by
SRINGS_2: 5;
S is
cap-closed;
hence thesis;
end;
end
theorem ::
SRINGS_4:34
Thm33: for X be
non-empty1
-element
FinSequence, S be
cap-closed-yielding
SemiringFamily of X holds the set of all (
product
<*s*>) where s be
Element of (S
. 1) is
cap-closed
semiring_of_sets of the set of all
<*x*> where x be
Element of (X
. 1)
proof
let X be
non-empty1
-element
FinSequence, S be
cap-closed-yielding
SemiringFamily of X;
S is
cap-closed-yielding
SemiringFamily of X & 1
in (
Seg 1) by
FINSEQ_1: 3;
then
A1: (S
. 1) is
semiring_of_sets of (X
. 1) & (S
. 1) is
cap-closed by
Def2,
Def4;
set S1 = the set of all (
product
<*s*>) where s be
Element of (S
. 1);
set X1 = the set of all
<*x*> where x be
Element of (X
. 1);
now
let s1,s2 be
set;
assume that
A2: s1
in S1 and
A3: s2
in S1;
consider t1 be
Element of (S
. 1) such that
A4: s1
= (
product
<*t1*>) by
A2;
consider t2 be
Element of (S
. 1) such that
A5: s2
= (
product
<*t2*>) by
A3;
A6: (s1
/\ s2)
= (
product
<*(t1
/\ t2)*>) by
A4,
A5,
Thm25;
(t1
/\ t2) is
Element of (S
. 1) by
A1;
hence (s1
/\ s2)
in S1 by
A6;
end;
then S1 is
cap-closed;
hence thesis by
Thm27;
end;
theorem ::
SRINGS_4:35
Thm34: for X be
non-empty1
-element
FinSequence, S be
cap-closed-yielding
SemiringFamily of X holds (
SemiringProduct S) is
cap-closed
semiring_of_sets of (
product X)
proof
let X be
non-empty1
-element
FinSequence, S be
cap-closed-yielding
SemiringFamily of X;
set S1 = the set of all (
product
<*s*>) where s be
Element of (S
. 1);
set X1 = the set of all
<*x*> where x be
Element of (X
. 1);
S1
= (
SemiringProduct S) & X1
= (
product X) by
Thm21,
Thm24;
hence thesis by
Thm33;
end;
theorem ::
SRINGS_4:36
Thm35: for X1,X2 be
set, S1 be
cap-closed
semiring_of_sets of X1, S2 be
cap-closed
semiring_of_sets of X2 holds the set of all
[:s1, s2:] where s1 be
Element of S1, s2 be
Element of S2 is
cap-closed
semiring_of_sets of
[:X1, X2:]
proof
let X1,X2 be
set, S1 be
cap-closed
semiring_of_sets of X1, S2 be
cap-closed
semiring_of_sets of X2;
set S = { s where s be
Subset of
[:X1, X2:] : ex x1,x2 be
set st x1
in S1 & x2
in S2 & s
=
[:x1, x2:] };
S is
semiring_of_sets of
[:X1, X2:] & S is
cap-closed by
SRINGS_2: 7,
SRINGS_2: 3;
hence thesis by
SRINGS_2: 2;
end;
theorem ::
SRINGS_4:37
Thm36: for Xn be
non-emptyn
-element
FinSequence, X1 be
non-empty1
-element
FinSequence, Sn be
cap-closed-yielding
SemiringFamily of Xn, S1 be
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
let Xn be
non-emptyn
-element
FinSequence, X1 be
non-empty1
-element
FinSequence, Sn be
cap-closed-yielding
SemiringFamily of Xn, S1 be
cap-closed-yielding
SemiringFamily of X1;
assume that
A1: (
SemiringProduct Sn) is
cap-closed
semiring_of_sets of (
product Xn) and
A2: (
SemiringProduct S1) is
cap-closed
semiring_of_sets of (
product X1);
reconsider S12 = the set of all
[:s1, s2:] where s1 be
Element of (
SemiringProduct Sn), s2 be
Element of (
SemiringProduct S1) as
semiring_of_sets of
[:(
product Xn), (
product X1):] by
A1,
A2,
Thm29;
consider I be
Function of
[:(
product Xn), (
product X1):], (
product (Xn
^ X1)) such that
A3: I is
one-to-one and I is
onto and for x,y be
FinSequence st x
in (
product Xn) & y
in (
product X1) holds (I
. (x,y))
= (x
^ y) and
A4: (I
.: S12)
= (
SemiringProduct (Sn
^ S1)) by
A1,
A2,
Thm30;
S12 is
cap-closed by
A1,
A2,
Thm35;
hence thesis by
A3,
Thm10,
A4,
Thm12;
end;
Thm37: for S be
cap-closed-yielding
SemiringFamily of X holds (
SemiringProduct S) is
cap-closed
proof
let S be
cap-closed-yielding
SemiringFamily of X;
reconsider SP = (
SemiringProduct S) as
Subset-Family of (
product X) by
Thm20;
defpred
P[ non
zero
Nat] means for X be
non-empty$1
-element
FinSequence, S be
cap-closed-yielding
SemiringFamily of X holds (
SemiringProduct S) is
cap-closed
semiring_of_sets of (
product X);
A1:
P[1] by
Thm34;
A2:
now
let n be non
zero
Nat;
assume
A3:
P[n];
now
let X be
non-empty(n
+ 1)
-element
FinSequence, S be
cap-closed-yielding
SemiringFamily of X;
reconsider SPS = (
SemiringProduct S) as
Subset-Family of (
product X) by
Thm20;
consider Xq be
FinSequence, xq be
object such that
A4: X
= (Xq
^
<*xq*>) by
FINSEQ_1: 46;
(
len X)
= ((
len Xq)
+ (
len
<*xq*>)) by
A4,
FINSEQ_1: 22
.= ((
len Xq)
+ 1) by
FINSEQ_1: 39;
then
A5: (
len Xq)
= n by
XCMPLX_1: 2,
FINSEQ_3: 153;
reconsider Xn = Xq as n
-element
FinSequence by
A5,
CARD_1:def 7;
(
rng Xn)
c= (
rng X) by
A4,
FINSEQ_1: 29;
then
A7: not
{}
in (
rng Xn);
reconsider Xn as
non-emptyn
-element
FinSequence by
A7,
RELAT_1:def 9;
reconsider X1 =
<*xq*> as 1
-element
FinSequence;
(
rng X1)
c= (
rng X) by
A4,
FINSEQ_1: 30;
then
A9: not
{}
in (
rng X1);
reconsider X1 as
non-empty1
-element
FinSequence by
A9,
RELAT_1:def 9;
consider Sq be
FinSequence, sq be
object such that
A10: S
= (Sq
^
<*sq*>) by
FINSEQ_1: 46;
(
len S)
= ((
len Sq)
+ (
len
<*sq*>)) by
A10,
FINSEQ_1: 22
.= ((
len Sq)
+ 1) by
FINSEQ_1: 39;
then (
len Sq)
= n by
FINSEQ_3: 153,
XCMPLX_1: 2;
then
reconsider Sn = Sq as n
-element
FinSequence by
CARD_1:def 7;
reconsider S1 =
<*sq*> as 1
-element
FinSequence;
(
Seg (n
+ 1))
= ((
Seg n)
\/
{(n
+ 1)}) by
FINSEQ_1: 9;
then
A11: (
Seg n)
c= (
Seg (n
+ 1)) by
XBOOLE_1: 7;
A12: (
len Xn)
= n & (
len Sn)
= n by
FINSEQ_3: 153;
now
A13: for i be
Nat st i
in (
Seg n) holds (Sn
. i) is
cap-closed
semiring_of_sets of (Xn
. i)
proof
let i be
Nat;
assume
A14: i
in (
Seg n);
then i
in (
Seg (
len Xn)) & i
in (
Seg (
len Sn)) by
FINSEQ_3: 153;
then (X
. i)
= ((Xn
^ X1)
. i) & (S
. i)
= ((Sn
^ S1)
. i) & 1
<= i & i
<= (
len Xn) & i
<= (
len Sn) by
A4,
A10,
FINSEQ_1: 1;
then (X
. i)
= (Xn
. i) & (S
. i)
= (Sn
. i) by
FINSEQ_1: 64;
hence thesis by
A14,
A11,
Def2,
Def4;
end;
for i be
Nat st i
in (
Seg n) holds (Sn
. i) is
semiring_of_sets of (Xn
. i) by
A13;
then
reconsider P = Sn as
SemiringFamily of Xn by
Def2;
P is
cap-closed-yielding by
A13;
hence Sn is
cap-closed-yielding
SemiringFamily of Xn;
end;
then
A16: Xn is
non-empty & Sn is
cap-closed-yielding
SemiringFamily of Xn & (
SemiringProduct Sn) is
cap-closed
semiring_of_sets of (
product Xn) by
A3;
A17: (
len X1)
= 1 by
FINSEQ_1: 39;
then
A18: (X1
. 1)
= (X
. (n
+ 1)) by
FINSEQ_1: 65,
A4,
A12;
(
len S1)
= 1 by
FINSEQ_1: 39;
then
A20: (S1
. 1)
= (S
. (n
+ 1)) by
FINSEQ_1: 65,
A12,
A10;
now
thus X1 is
non-empty;
A23: (n
+ 1)
in (
Seg (n
+ 1)) by
FINSEQ_1: 3;
A23a:
now
let i be
Nat;
assume i
in (
Seg 1);
then i
= 1 by
TARSKI:def 1,
FINSEQ_1: 2;
hence (S1
. i) is
cap-closed
semiring_of_sets of (X1
. i) by
A23,
A20,
A18,
Def2,
Def4;
end;
A23b: for i be
Nat st i
in (
Seg 1) holds (S1
. i) is
semiring_of_sets of (X1
. i) by
A23a;
reconsider P = S1 as
SemiringFamily of X1 by
A23b,
Def2;
for i be
Nat st i
in (
Seg 1) holds (P
. i) is
cap-closed by
A23a;
hence (X1
. 1)
= (X
. (n
+ 1)) & S1 is
cap-closed-yielding
SemiringFamily of X1 by
A17,
FINSEQ_1: 65,
A4,
A12,
Def4;
end;
then
A24: S1 is
cap-closed-yielding
SemiringFamily of X1 & (
SemiringProduct S1) is
cap-closed
semiring_of_sets of (
product X1) by
Thm34;
thus (
SemiringProduct S) is
cap-closed
semiring_of_sets of (
product X) by
A16,
A24,
Thm36,
A10,
A4;
end;
hence
P[(n
+ 1)];
end;
for n be non
zero
Nat holds
P[n] from
NAT_1:sch 10(
A1,
A2);
hence thesis;
end;
registration
let n, X;
let S be
cap-closed-yielding
SemiringFamily of X;
cluster (
SemiringProduct S) ->
cap-closed;
coherence by
Thm37;
end
theorem ::
SRINGS_4:38
for S be
cap-closed-yielding
SemiringFamily of X holds (
SemiringProduct S) is
cap-closed
semiring_of_sets of (
product X) by
Thm32;
begin
definition
let n be non
zero
Nat, X be
non-emptyn
-element
FinSequence;
::
SRINGS_4:def6
mode
ClassicalSemiringFamily of X -> n
-element
FinSequence means
:
Def5: for i be
Nat st i
in (
Seg n) holds (it
. i) is
with_empty_element
semi-diff-closed
cap-closed
Subset-Family of (X
. i);
existence
proof
deffunc
F(
set) = (
bool (X
. $1));
consider p be
FinSequence such that
A1: (
len p)
= n and
A2: for i be
Nat st i
in (
dom p) holds (p
. i)
=
F(i) from
FINSEQ_1:sch 2;
reconsider p as n
-element
FinSequence by
A1,
CARD_1:def 7;
take p;
now
let i be
Nat;
assume
A3: i
in (
Seg n);
reconsider Xi = (X
. i) as
set;
(
bool Xi)
c= (
bool Xi);
then
reconsider BXi = (
bool Xi) as
Subset-Family of Xi;
A4: BXi is
cap-finite-partition-closed
diff-c=-finite-partition-closed
with_countable_Cover
with_empty_element
Subset-Family of Xi;
i
in (
dom p) by
A3,
A1,
FINSEQ_1:def 3;
hence (p
. i) is
with_empty_element
semi-diff-closed
cap-closed
Subset-Family of (X
. i) by
A2,
A4;
end;
hence thesis;
end;
end
notation
let n be non
zero
Nat, X be n
-element
FinSequence;
synonym
MeasurableRectangle (X) for
SemiringProduct (X);
end
theorem ::
SRINGS_4:39
Thm38: for S be
ClassicalSemiringFamily of X holds S is
cap-closed-yielding
SemiringFamily of X
proof
let S be
ClassicalSemiringFamily of X;
now
let i be
Nat;
assume
A1: i
in (
Seg n);
(S
. i) is
with_empty_element
semi-diff-closed
cap-closed
Subset-Family of (X
. i) by
A1,
Def5;
hence (S
. i) is
semiring_of_sets of (X
. i) by
SRINGS_3: 9;
end;
then
reconsider SC = S as
SemiringFamily of X by
Def2;
for i be
Nat st i
in (
Seg n) holds (SC
. i) is
cap-closed by
Def5;
hence thesis by
Def4;
end;
theorem ::
SRINGS_4:40
for S be
ClassicalSemiringFamily of X holds (
MeasurableRectangle S) is
with_empty_element
semi-diff-closed
cap-closed
Subset-Family of (
product X)
proof
let S be
ClassicalSemiringFamily of X;
reconsider S1 = S as
cap-closed-yielding
SemiringFamily of X by
Thm38;
(
SemiringProduct S1) is
cap-closed
with_empty_element
cap-finite-partition-closed
diff-finite-partition-closed
Subset-Family of (
product X) by
Thm32;
hence thesis by
SRINGS_3: 10;
end;