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 A1: ( E in Field_generated_by (measurable_rectangles (S1,S2)) & E <> {} ) ; :: thesis:
consider f being disjoint_valued FinSequence of measurable_rectangles (S1,S2), A being FinSequence of S1, B being FinSequence of S2 such that
A2: ( len f = len A & len f = len B & E = Union f & ( for n being Nat st n in dom f holds
( proj1 (f . n) = A . n & proj2 (f . n) = B . n ) ) & ( for n being Nat
for x, y being set st n in dom f & x in X1 & y in X2 holds
(chi ((f . n),[:X1,X2:])) . (x,y) = ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) ) ) by A1, Th66;
deffunc H₁( set ) -> Function of [:X1,X2:],ExtREAL = chi ((f . $1),[:X1,X2:]);
consider Xf being FinSequence such that
A3: ( len Xf = len f & ( for n being Nat st n in dom Xf holds
Xf . n = H₁(n) ) ) from FINSEQ_1:sch 2();

now :: thesis:

let z be set ; :: thesis:
assume z in rng Xf ; :: thesis:
then consider i being object such that
A4: ( i in dom Xf & z = Xf . i ) by FUNCT_1:def 3;
reconsider i = i as Nat by A4;
z = chi ((f . i),[:X1,X2:]) by A3, A4;
hence z in Funcs ([:X1,X2:],ExtREAL) by FUNCT_2:8; :: thesis:

end;

then rng Xf c= Funcs ([:X1,X2:],ExtREAL) ;
then reconsider Xf = Xf as FinSequence of Funcs ([:X1,X2:],ExtREAL) by FINSEQ_1:def 4;

now :: thesis:

let n be Nat; :: thesis:
assume n in dom Xf ; :: thesis:
then Xf . n = chi ((f . n),[:X1,X2:]) by A3;
then rng (Xf . n) c= {0,1} by FUNCT_3:39;
then not -infty in rng (Xf . n) ;
hence Xf . n is without-infty by MESFUNC5:def 3; :: thesis:

end;

then Xf is without_-infty-valued ;
then reconsider Xf = Xf as summable FinSequence of Funcs ([:X1,X2:],ExtREAL) ;
take f ; :: thesis:
take A ; :: thesis:
take B ; :: thesis:
take Xf ; :: thesis:
defpred S₁[ Nat] means ( $1 in dom f implies (Partial_Sums Xf) . $1 = chi ((Union (f | $1)),[:X1,X2:]) );
A9: dom Xf = dom f by A3, FINSEQ_3:29;
A5: S₁[ 0 ] by FINSEQ_3:24;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A7: S₁[k] ; :: thesis:
assume A8: k + 1 in dom f ; :: thesis:

per cases ;

suppose A10: k = 0 ; :: thesis:

then A11: (Partial_Sums Xf) . (k + 1) = Xf . (k + 1) by DEF13
.= chi ((f . (k + 1)),[:X1,X2:]) by A3, A8, A9 ;
not f is empty by A8;
then f | (k + 1) = <*(f . (k + 1))*> by A10, FINSEQ_5:20;
then rng (f | (k + 1)) = {(f . (k + 1))} by FINSEQ_1:39;
then union (rng (f | (k + 1))) = f . (k + 1) by ZFMISC_1:25;
hence (Partial_Sums Xf) . (k + 1) = chi ((Union (f | (k + 1))),[:X1,X2:]) by A11, CARD_3:def 4; :: thesis:

end;

suppose k <> 0 ; :: thesis:

then A12: k >= 1 by NAT_1:14;
A13: ( 1 <= k + 1 & k + 1 <= len Xf ) by A8, A3, FINSEQ_3:25;
then A14: k < len Xf by NAT_1:13;
then k < len (Partial_Sums Xf) by DEF13;
then k in dom (Partial_Sums Xf) by A12, FINSEQ_3:25;
then A16: (Partial_Sums Xf) /. k = chi ((Union (f | k)),[:X1,X2:]) by A3, A14, A7, A12, FINSEQ_3:25, PARTFUN1:def 6;
A17: Xf /. (k + 1) = Xf . (k + 1) by A8, A9, PARTFUN1:def 6
.= chi ((f . (k + 1)),[:X1,X2:]) by A8, A9, A3 ;

A24: now :: thesis:

assume (Union (f | k)) /\ (f . (k + 1)) <> {} ; :: thesis:
then consider z being object such that
A18: z in (Union (f | k)) /\ (f . (k + 1)) by XBOOLE_0:def 1;
A19: ( z in Union (f | k) & z in f . (k + 1) ) by A18, XBOOLE_0:def 4;
then z in union (rng (f | k)) by CARD_3:def 4;
then consider Z being set such that
A20: ( z in Z & Z in rng (f | k) ) by TARSKI:def 4;
consider j being Element of NAT such that
A21: ( j in dom (f | k) & Z = (f | k) . j ) by A20, PARTFUN1:3;
( 1 <= j & j <= len (f | k) ) by A21, FINSEQ_3:25;
then A22: ( 1 <= j & j <= k ) by A14, A3, FINSEQ_1:59;
then A23: Z = f . j by A21, FINSEQ_3:112;
j <> k + 1 by A22, NAT_1:13;
then f . j misses f . (k + 1) by PROB_2:def 2;
hence contradiction by A23, A19, A20, XBOOLE_0:def 4; :: thesis:

end;

A25: (Partial_Sums Xf) . (k + 1) = (chi ((Union (f | k)),[:X1,X2:])) + (chi ((f . (k + 1)),[:X1,X2:])) by A16, A17, A12, A13, DEF13, NAT_1:13;
( 1 <= k + 1 & k + 1 <= len (Partial_Sums Xf) ) by A13, DEF13;
then k + 1 in dom (Partial_Sums Xf) by FINSEQ_3:25;
then A26: (Partial_Sums Xf) /. (k + 1) = (Partial_Sums Xf) . (k + 1) by PARTFUN1:def 6;

now :: thesis:

let z be Element of [:X1,X2:]; :: thesis:
dom ((chi ((Union (f | k)),[:X1,X2:])) + (chi ((f . (k + 1)),[:X1,X2:]))) = [:X1,X2:] by A25, A26, FUNCT_2:def 1;
then A28: ((Partial_Sums Xf) . (k + 1)) . z = ((chi ((Union (f | k)),[:X1,X2:])) . z) + ((chi ((f . (k + 1)),[:X1,X2:])) . z) by A25, MESFUNC1:def 3;

per cases ;

suppose A31: z in Union (f | (k + 1)) ; :: thesis:

then z in union (rng (f | (k + 1))) by CARD_3:def 4;
then consider Z being set such that
A29: ( z in Z & Z in rng (f | (k + 1)) ) by TARSKI:def 4;
consider j being Element of NAT such that
A30: ( j in dom (f | (k + 1)) & Z = (f | (k + 1)) . j ) by A29, PARTFUN1:3;
A36: ( 1 <= j & j <= len (f | (k + 1)) ) by A30, FINSEQ_3:25;
then A32: ( 1 <= j & j <= k + 1 ) by A13, A3, FINSEQ_1:59;
then A33: Z = f . j by A30, FINSEQ_3:112;

now :: thesis:

per cases ;

suppose j = k + 1 ; :: thesis:

then A34: z in f . (k + 1) by A29, A30, FINSEQ_3:112;
then A35: (chi ((f . (k + 1)),[:X1,X2:])) . z = 1 by FUNCT_3:def 3;
not z in Union (f | k) by A24, A34, XBOOLE_0:def 4;
then (chi ((Union (f | k)),[:X1,X2:])) . z = 0 by FUNCT_3:def 3;
hence ((Partial_Sums Xf) . (k + 1)) . z = 1 by A28, A35, XXREAL_3:4; :: thesis:

end;

suppose j <> k + 1 ; :: thesis:

then j < k + 1 by A32, XXREAL_0:1;
then A37: j <= k by NAT_1:13;
then j <= len (f | k) by A3, A14, FINSEQ_1:59;
then ( j in dom (f | k) & Z = (f | k) . j ) by A33, A36, A37, FINSEQ_3:25, FINSEQ_3:112;
then Z in rng (f | k) by FUNCT_1:3;
then z in union (rng (f | k)) by A29, TARSKI:def 4;
then A38: z in Union (f | k) by CARD_3:def 4;
then A39: (chi ((Union (f | k)),[:X1,X2:])) . z = 1 by FUNCT_3:def 3;
not z in f . (k + 1) by A24, A38, XBOOLE_0:def 4;
then (chi ((f . (k + 1)),[:X1,X2:])) . z = 0 by FUNCT_3:def 3;
hence ((Partial_Sums Xf) . (k + 1)) . z = 1 by A28, A39, XXREAL_3:4; :: thesis:

end;

hence ((Partial_Sums Xf) . (k + 1)) . z = (chi ((Union (f | (k + 1))),[:X1,X2:])) . z by A31, FUNCT_3:def 3; :: thesis:

end;

suppose A40: not z in Union (f | (k + 1)) ; :: thesis:

then A41: (chi ((Union (f | (k + 1))),[:X1,X2:])) . z = 0 by FUNCT_3:def 3;
A42: not z in union (rng (f | (k + 1))) by A40, CARD_3:def 4;
A43: for j being Nat st 1 <= j & j <= k + 1 holds
not z in f . j

proof

let j be Nat; :: thesis:
assume B1: ( 1 <= j & j <= k + 1 ) ; :: thesis:
then ( 1 <= j & j <= len (f | (k + 1)) ) by A3, A13, FINSEQ_1:59;
then j in dom (f | (k + 1)) by FINSEQ_3:25;
then (f | (k + 1)) . j in rng (f | (k + 1)) by FUNCT_1:3;
then f . j in rng (f | (k + 1)) by B1, FINSEQ_3:112;
hence not z in f . j by A42, TARSKI:def 4; :: thesis:

end;

now :: thesis:

assume z in Union (f | k) ; :: thesis:
then z in union (rng (f | k)) by CARD_3:def 4;
then consider Z being set such that
A46: ( z in Z & Z in rng (f | k) ) by TARSKI:def 4;
consider j being Element of NAT such that
A47: ( j in dom (f | k) & Z = (f | k) . j ) by A46, PARTFUN1:3;
( 1 <= j & j <= len (f | k) ) by A47, FINSEQ_3:25;
then A48: ( 1 <= j & j <= k ) by A3, A14, FINSEQ_1:59;
then ( 1 <= j & j <= k + 1 ) by NAT_1:13;
then not z in f . j by A43;
hence contradiction by A46, A47, A48, FINSEQ_3:112; :: thesis:

end;

then A50: (chi ((Union (f | k)),[:X1,X2:])) . z = 0 by FUNCT_3:def 3;
1 <= k + 1 by NAT_1:11;
then not z in f . (k + 1) by A43;
then (chi ((f . (k + 1)),[:X1,X2:])) . z = 0 by FUNCT_3:def 3;
hence ((Partial_Sums Xf) . (k + 1)) . z = (chi ((Union (f | (k + 1))),[:X1,X2:])) . z by A41, A28, A50; :: thesis:

end;

hence (Partial_Sums Xf) . (k + 1) = chi ((Union (f | (k + 1))),[:X1,X2:]) by A26, FUNCT_2:def 8; :: thesis:

end;

A51: for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A6);
thus E = Union f by A2; :: thesis:
union (rng f) <> {} by A1, A2, CARD_3:def 4;
then dom f <> {} by ZFMISC_1:2, RELAT_1:42;
then Seg (len f) <> {} by FINSEQ_1:def 3;
then A52: len f in Seg (len f) by FINSEQ_3:7;
hence A53: len f in dom f by FINSEQ_1:def 3; :: thesis:
thus ( len f = len A & len f = len B ) by A2; :: thesis:
thus len f = len Xf by A3; :: thesis:
thus for n being Nat st n in dom f holds
f . n = [:(A . n),(B . n):] :: thesis:

proof

let n be Nat; :: thesis:
assume A54: 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 An being Element of S1, Bn being Element of S2 such that
A55: f . n = [:An,Bn:] ;

per cases ;

suppose A57: f . n = {} ; :: thesis:

then ( A . n = proj1 {} & B . n = proj2 {} ) by A2, A54;
hence f . n = [:(A . n),(B . n):] by A57, ZFMISC_1:90; :: thesis:

end;

suppose f . n <> {} ; :: thesis:

then A59: ( proj1 (f . n) = An & proj2 (f . n) = Bn ) by A55, FUNCT_5:9;
( proj1 (f . n) = A . n & proj2 (f . n) = B . n ) by A2, A54;
hence f . n = [:(A . n),(B . n):] by A55, A59; :: thesis:

end;

thus for n being Nat st n in dom Xf holds
Xf . n = chi ((f . n),[:X1,X2:]) by A3; :: thesis:
A60: (Partial_Sums Xf) . (len Xf) = chi ((Union (f | (len f))),[:X1,X2:]) by A51, A3, A53
.= chi ((Union f),[:X1,X2:]) by FINSEQ_1:58 ;
hence (Partial_Sums Xf) . (len Xf) = chi (E,[:X1,X2:]) by A2; :: thesis:
thus for n being Nat
for x, y being set st n in dom Xf & x in X1 & y in X2 holds
(Xf . n) . (x,y) = ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) :: thesis:

proof

let n be Nat; :: thesis:
let x, y be set ; :: thesis:
assume Q1: ( n in dom Xf & x in X1 & y in X2 ) ; :: thesis:
then (chi ((f . n),[:X1,X2:])) . (x,y) = ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) by A2, A9;
hence (Xf . n) . (x,y) = ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) by Q1, A3; :: thesis:

end;

thus for x being Element of X1 holds ProjMap1 ((chi (E,[:X1,X2:])),x) = ProjMap1 (((Partial_Sums Xf) /. (len Xf)),x) :: thesis:

proof

let x be Element of X1; :: thesis:
len f = len (Partial_Sums Xf) by A3, DEF13;
then len Xf in dom (Partial_Sums Xf) by A52, A3, FINSEQ_1:def 3;
hence ProjMap1 ((chi (E,[:X1,X2:])),x) = ProjMap1 (((Partial_Sums Xf) /. (len Xf)),x) by A60, A2, PARTFUN1:def 6; :: thesis:

end;

let y be Element of X2; :: thesis:
len f = len (Partial_Sums Xf) by A3, DEF13;
then len Xf in dom (Partial_Sums Xf) by A52, A3, FINSEQ_1:def 3;
hence ProjMap2 ((chi (E,[:X1,X2:])),y) = ProjMap2 (((Partial_Sums Xf) /. (len Xf)),y) by A60, A2, PARTFUN1:def 6; :: thesis: