let X1, X2 be non empty set ; :: thesis:
let S1 be SigmaField of X1; :: thesis:
let S2 be SigmaField of X2; :: thesis:
let E be Element of sigma (measurable_rectangles (S1,S2)); :: thesis:
let K be set ; :: thesis:
assume AS: K = { C where C is Subset of [:X1,X2:] : for x being set holds X-section (C,x) in S2 } ; :: thesis:

let C1, C2 be set ; :: thesis:
assume A2: ( C1 in K & C2 in K ) ; :: thesis:
then consider SC1 being Subset of [:X1,X2:] such that
A3: ( C1 = SC1 & ( for x being set holds X-section (SC1,x) in S2 ) ) by AS;
consider SC2 being Subset of [:X1,X2:] such that
A4: ( C2 = SC2 & ( for x being set holds X-section (SC2,x) in S2 ) ) by AS, A2;

let x be set ; :: thesis:
A5: ( X-section (SC1,x) in S2 & X-section (SC2,x) in S2 ) by A3, A4;
X-section ((SC1 \/ SC2),x) = (X-section (SC1,x)) \/ (X-section (SC2,x)) by Th20;
hence X-section ((SC1 \/ SC2),x) in S2 by A5, PROB_1:3; :: thesis:

end;

hence C1 \/ C2 in K by AS, A3, A4; :: thesis:

end;

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 :: thesis:

let C be set ; :: thesis:
assume C in DisUnion (measurable_rectangles (S1,S2)) ; :: thesis:
then 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

proof

let n be Nat; :: thesis:
assume n in dom F ; :: thesis:
then F . n in measurable_rectangles (S1,S2) by PARTFUN1:4;
then F . n in { [:A,B:] where A is Element of S1, B is Element of S2 : verum } by MEASUR10:def 5;
then consider A being Element of S1, B being Element of S2 such that
A10: F . n = [:A,B:] ;

now :: thesis:

let x be set ; :: thesis:
( X-section ([:A,B:],x) = B or X-section ([:A,B:],x) = {} ) by Th16;
hence X-section ([:A,B:],x) in S2 by MEASURE1:7; :: thesis:

end;

hence F . n in K by AS, A10; :: thesis:

end;

hence C in K by A1, A7, A8, A9, Th41, FINSUB_1:def 1; :: thesis:

end;

then DisUnion (measurable_rectangles (S1,S2)) c= K ;
hence Field_generated_by (measurable_rectangles (S1,S2)) c= K by SRINGS_3:22; :: thesis:

now :: thesis:

let A be set ; :: thesis:
assume A in K ; :: thesis:
then ex A1 being Subset of [:X1,X2:] st
( A = A1 & ( for x being set holds X-section (A1,x) in S2 ) ) by AS;
hence A in bool [:X1,X2:] ; :: thesis:

end;

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

proof

let C be Subset of [:X1,X2:]; :: thesis:
assume C in K ; :: thesis:
then consider C1 being Subset of [:X1,X2:] such that
A11: ( C = C1 & ( for x being set holds X-section (C1,x) in S2 ) ) by AS;

now :: thesis:

let x be set ; :: thesis:

per cases ;

suppose A12: x in X1 ; :: thesis:

A13: X-section (C1,x) in S2 by A11;
X2 in S2 by PROB_1:5;
then X2 \ (X-section (C1,x)) in S2 by A13, PROB_1:6;
hence X-section (([:X1,X2:] \ C1),x) in S2 by A12, Th19; :: thesis:

end;

suppose not x in X1 ; :: thesis:

then X-section (([:X1,X2:] \ C1),x) = {} by Th17;
hence X-section (([:X1,X2:] \ C1),x) in S2 by MEASURE1:7; :: thesis:

end;

then [:X1,X2:] \ C in K by AS, A11;
hence C ` in K by SUBSET_1:def 4; :: thesis:

end;

then K is compl-closed by PROB_1:def 1;
then reconsider K = K as Field_Subset of [:X1,X2:] by A7, A6;

now :: thesis:

let M be N_Sub_set_fam of [:X1,X2:]; :: thesis:
assume A15: M c= K ; :: thesis:
consider E being SetSequence of [:X1,X2:] such that
A16: rng E = M by SUPINF_2:def 8;

now :: thesis:

let x be set ; :: thesis:
defpred S₁[ 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 S₁[n,d]

proof

let n be Element of NAT ; :: thesis:
set d = { y where y is Element of X2 : [x,y] in E . n } ;

now :: thesis:

let y be set ; :: thesis:
assume y in { y where y is Element of X2 : [x,y] in E . n } ; :: thesis:
then ex y1 being Element of X2 st
( y = y1 & [x,y1] in E . n ) ;
hence y in X2 ; :: thesis:

end;

then { y where y is Element of X2 : [x,y] in E . n } c= X2 ;
then reconsider d = { y where y is Element of X2 : [x,y] in E . n } as Element of bool X2 ;
take d ; :: thesis:
thus S₁[n,d] ; :: thesis:

end;

consider D being Function of NAT,(bool X2) such that
A19: for n being Element of NAT holds S₁[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)

proof

let n be Nat; :: thesis:
n is Element of NAT by ORDINAL1:def 12;
hence D . n = X-section ((E . n),x) by A19; :: thesis:

end;

A21: dom D = NAT by FUNCT_2:def 1;

now :: thesis:

let D0 be set ; :: thesis:
assume D0 in rng D ; :: thesis:
then consider n0 being Element of NAT such that
A22: D0 = D . n0 by FUNCT_2:113;
A23: D0 = X-section ((E . n0),x) by A20, A22;
E . n0 in K by A15, A16, FUNCT_2:112;
then ex C0 being Subset of [:X1,X2:] st
( E . n0 = C0 & ( for x being set holds X-section (C0,x) in S2 ) ) by AS;
hence D0 in S2 by A23; :: thesis:

end;

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; :: thesis:

end;

hence union M in K by AS, A16; :: thesis:

end;

then K is sigma-additive by MEASURE1:def 5;
hence K is SigmaField of [:X1,X2:] ; :: thesis: