let X1, X2 be non empty set ; for S1 being SigmaField of X1
for S2 being SigmaField of X2
for E being Element of sigma (measurable_rectangles (S1,S2))
for K being set st K = { C where C is Subset of [:X1,X2:] : for p being set holds X-section (C,p) in S2 } holds
( Field_generated_by (measurable_rectangles (S1,S2)) c= K & K is SigmaField of [:X1,X2:] )
let S1 be SigmaField of X1; for S2 being SigmaField of X2
for E being Element of sigma (measurable_rectangles (S1,S2))
for K being set st K = { C where C is Subset of [:X1,X2:] : for p being set holds X-section (C,p) in S2 } holds
( Field_generated_by (measurable_rectangles (S1,S2)) c= K & K is SigmaField of [:X1,X2:] )
let S2 be SigmaField of X2; for E being Element of sigma (measurable_rectangles (S1,S2))
for K being set st K = { C where C is Subset of [:X1,X2:] : for p being set holds X-section (C,p) in S2 } holds
( Field_generated_by (measurable_rectangles (S1,S2)) c= K & K is SigmaField of [:X1,X2:] )
let E be Element of sigma (measurable_rectangles (S1,S2)); for K being set st K = { C where C is Subset of [:X1,X2:] : for p being set holds X-section (C,p) in S2 } holds
( Field_generated_by (measurable_rectangles (S1,S2)) c= K & K is SigmaField of [:X1,X2:] )
let K be set ; ( K = { C where C is Subset of [:X1,X2:] : for p being set holds X-section (C,p) in S2 } implies ( Field_generated_by (measurable_rectangles (S1,S2)) c= K & K is SigmaField of [:X1,X2:] ) )
assume AS:
K = { C where C is Subset of [:X1,X2:] : for x being set holds X-section (C,x) in S2 }
; ( Field_generated_by (measurable_rectangles (S1,S2)) c= K & K is SigmaField of [:X1,X2:] )
A1:
now for C1, C2 being set st C1 in K & C2 in K holds
C1 \/ C2 in Kend;
then A6:
K is cup-closed
by FINSUB_1:def 1;
for x being set holds X-section (({} [:X1,X2:]),x) in S2
by MEASURE1:7;
then A7:
{} in K
by AS;
now for C being set st C in DisUnion (measurable_rectangles (S1,S2)) holds
C in Klet C be
set ;
( C in DisUnion (measurable_rectangles (S1,S2)) implies C in K )assume
C in DisUnion (measurable_rectangles (S1,S2))
;
C in Kthen
C in { A where A is Subset of [:X1,X2:] : ex F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st A = Union F }
by SRINGS_3:def 3;
then consider C1 being
Subset of
[:X1,X2:] such that A8:
(
C = C1 & ex
F being
disjoint_valued FinSequence of
measurable_rectangles (
S1,
S2) st
C1 = Union F )
;
consider F being
disjoint_valued FinSequence of
measurable_rectangles (
S1,
S2)
such that A9:
C1 = Union F
by A8;
for
n being
Nat st
n in dom F holds
F . n in K
hence
C in K
by A1, A7, A8, A9, Th41, FINSUB_1:def 1;
verum end;
then
DisUnion (measurable_rectangles (S1,S2)) c= K
;
hence
Field_generated_by (measurable_rectangles (S1,S2)) c= K
by SRINGS_3:22; K is SigmaField of [:X1,X2:]
then
K c= bool [:X1,X2:]
;
then reconsider K = K as Subset-Family of [:X1,X2:] ;
for C being Subset of [:X1,X2:] st C in K holds
C ` in K
then
K is compl-closed
by PROB_1:def 1;
then reconsider K = K as Field_Subset of [:X1,X2:] by A7, A6;
now for M being N_Sub_set_fam of [:X1,X2:] st M c= K holds
union M in Klet M be
N_Sub_set_fam of
[:X1,X2:];
( M c= K implies union M in K )assume A15:
M c= K
;
union M in Kconsider E being
SetSequence of
[:X1,X2:] such that A16:
rng E = M
by SUPINF_2:def 8;
now for x being set holds X-section ((union (rng E)),x) in S2let x be
set ;
X-section ((union (rng E)),x) in S2defpred S1[
Nat,
object ]
means $2
= { y where y is Element of X2 : [x,y] in E . $1 } ;
A18:
for
n being
Element of
NAT ex
d being
Element of
bool X2 st
S1[
n,
d]
consider D being
Function of
NAT,
(bool X2) such that A19:
for
n being
Element of
NAT holds
S1[
n,
D . n]
from FUNCT_2:sch 3(A18);
reconsider D =
D as
SetSequence of
X2 ;
A20:
for
n being
Nat holds
D . n = X-section (
(E . n),
x)
A21:
dom D = NAT
by FUNCT_2:def 1;
then
rng D c= S2
;
then
D is
sequence of
S2
by A21, FUNCT_2:2;
then A24:
union (rng D) is
Element of
S2
by MEASURE1:24;
X-section (
(union (rng E)),
x)
= union (rng D)
by A20, Th24;
hence
X-section (
(union (rng E)),
x)
in S2
by A24;
verum end; hence
union M in K
by AS, A16;
verum end;
then
K is sigma-additive
by MEASURE1:def 5;
hence
K is SigmaField of [:X1,X2:]
; verum