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:
assume E in Field_generated_by (measurable_rectangles (S1,S2)) ; :: thesis:
then E in DisUnion (measurable_rectangles (S1,S2)) by SRINGS_3:22;
then E in { E1 where E1 is Subset of [:X1,X2:] : ex f being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E1 = Union f } by SRINGS_3:def 3;
then consider E1 being Subset of [:X1,X2:] such that
A1: ( E = E1 & ex f being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E1 = Union f ) ;
consider f being disjoint_valued FinSequence of measurable_rectangles (S1,S2) such that
A2: E1 = Union f by A1;
defpred S₁[ Nat, object ] means $2 = proj1 (f . $1);
A3: for i being Nat st i in Seg (len f) holds
ex Ai being Element of S1 st S₁[i,Ai]

let i be Nat; :: thesis:
assume i in Seg (len f) ; :: thesis:
then i in dom f by FINSEQ_1:def 3;
then f . i in measurable_rectangles (S1,S2) by PARTFUN1:4;
then f . i in { [:A,B:] where A is Element of S1, B is Element of S2 : verum } by MEASUR10:def 5;
then consider Ai being Element of S1, Bi being Element of S2 such that
A4: f . i = [:Ai,Bi:] ;

end;

reconsider Ai = {} as Element of S1 by MEASURE1:7;
take Ai ; :: thesis:
thus proj1 (f . i) = Ai by A4, A6; :: thesis:

end;

consider A being FinSequence of S1 such that
A7: ( dom A = Seg (len f) & ( for i being Nat st i in Seg (len f) holds
S₁[i,A . i] ) ) from FINSEQ_1:sch 5(A3);
defpred S₂[ Nat, object ] means $2 = proj2 (f . $1);
A8: for i being Nat st i in Seg (len f) holds
ex Bi being Element of S2 st S₂[i,Bi]

end;

reconsider Bi = {} as Element of S2 by MEASURE1:7;
take Bi ; :: thesis:
thus proj2 (f . i) = Bi by A9, A11; :: thesis:

end;

consider B being FinSequence of S2 such that
A12: ( dom B = Seg (len f) & ( for i being Nat st i in Seg (len f) holds
S₂[i,B . i] ) ) from FINSEQ_1:sch 5(A8);
take f ; :: thesis:
take A ; :: thesis:
take B ; :: thesis:
thus len f = len A by A7, FINSEQ_1:def 3; :: thesis:
thus len f = len B by A12, FINSEQ_1:def 3; :: thesis:
thus E = Union f by A1, A2; :: thesis:
thus A13: for n being Nat st n in dom f holds
( proj1 (f . n) = A . n & proj2 (f . n) = B . n ) :: thesis:

end;

let n be Nat; :: thesis:
let x, y be set ; :: thesis:
assume A14: ( n in dom f & x in X1 & y in X2 ) ; :: thesis:
then A15: ( A . n = proj1 (f . n) & B . n = proj2 (f . n) ) by A13;
f . n in measurable_rectangles (S1,S2) by A14, 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 An being Element of S1, Bn being Element of S2 such that
A16: f . n = [:An,Bn:] ;
A17: [x,y] in [:X1,X2:] by A14, ZFMISC_1:87;

then ( (chi ((f . n),[:X1,X2:])) . (x,y) = 0 & (chi ((A . n),X1)) . x = 0 & (chi ((B . n),X2)) . y = 0 ) by A14, A15, A17, FUNCT_3:def 3;
hence (chi ((f . n),[:X1,X2:])) . (x,y) = ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) ; :: thesis:

end;

then ( (chi ((A . n),X1)) . x = 1 & (chi ((B . n),X2)) . y = 1 ) by FUNCT_3:def 3;
then A20: ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) = 1 by XXREAL_3:81;
( proj1 (f . n) c= An & proj2 (f . n) c= Bn ) by A16, FUNCT_5:10;
then ( [x,y] in f . n & [x,y] in [:X1,X2:] ) by A19, A15, A16, ZFMISC_1:def 2;
hence (chi ((f . n),[:X1,X2:])) . (x,y) = ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) by A20, FUNCT_3:def 3; :: thesis:

end;

then ( (chi ((A . n),X1)) . x = 0 or (chi ((B . n),X2)) . y = 0 ) by A14, FUNCT_3:def 3;
then A22: ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) = 0 ;
not [x,y] in f . n by A18, A21, A16, ZFMISC_1:87;
hence (chi ((f . n),[:X1,X2:])) . (x,y) = ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) by A17, A22, FUNCT_3:def 3; :: thesis:

end;