let X1, X2 be non empty set ; :: thesis:
let S1 be SigmaField of X1; :: thesis:
let S2 be SigmaField of X2; :: thesis:
let M1 be sigma_Measure of S1; :: thesis:
let M2 be sigma_Measure of S2; :: 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, C being summable FinSequence of Funcs ([:X1,X2:],ExtREAL) such that
A2: ( E = Union F & len F in dom F & len F = len A & len F = len B & len F = len C & ( for n being Nat st n in dom F holds
F . n = [:(A . n),(B . n):] ) & ( for n being Nat st n in dom C holds
C . n = chi ((F . n),[:X1,X2:]) ) & (Partial_Sums C) . (len C) = chi (E,[:X1,X2:]) & ( for n being Nat
for x, y being set st n in dom C & x in X1 & y in X2 holds
(C . n) . (x,y) = ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) ) & ( for x being Element of X1 holds ProjMap1 ((chi (E,[:X1,X2:])),x) = ProjMap1 (((Partial_Sums C) /. (len C)),x) ) & ( for y being Element of X2 holds ProjMap2 ((chi (E,[:X1,X2:])),y) = ProjMap2 (((Partial_Sums C) /. (len C)),y) ) ) by A1, Th70;
A3: measurable_rectangles (S1,S2) c= sigma (measurable_rectangles (S1,S2)) by PROB_1:def 9;
defpred S₁[ Nat, object ] means ex f being Function of X1,ExtREAL st
( f = $2 & ( for x being Element of X1 holds f . x = Integral (M2,(ProjMap1 ((C /. $1),x))) ) );
I1: for n being Nat st n in Seg (len F) holds
ex z being object st S₁[n,z]

proof

let n be Nat; :: thesis:
assume n in Seg (len F) ; :: thesis:
deffunc H₁( Element of X1) -> Element of ExtREAL = Integral (M2,(ProjMap1 ((C /. n),$1)));
consider f being Function of X1,ExtREAL such that
I2: for x being Element of X1 holds f . x = H₁(x) from FUNCT_2:sch 4();
take z = f; :: thesis:
thus ex f being Function of X1,ExtREAL st
( f = z & ( for x being Element of X1 holds f . x = Integral (M2,(ProjMap1 ((C /. n),x))) ) ) by I2; :: thesis:

end;

consider I being FinSequence such that
I3: ( dom I = Seg (len F) & ( for n being Nat st n in Seg (len F) holds
S₁[n,I . n] ) ) from FINSEQ_1:sch 1(I1);

now :: thesis:

let z be set ; :: thesis:
assume z in rng I ; :: thesis:
then consider n being object such that
I4: ( n in dom I & z = I . n ) by FUNCT_1:def 3;
reconsider n = n as Element of NAT by I4;
consider f being Function of X1,ExtREAL such that
I5: ( f = I . n & ( for x being Element of X1 holds f . x = Integral (M2,(ProjMap1 ((C /. n),x))) ) ) by I3, I4;
( dom f = X1 & rng f c= ExtREAL ) by FUNCT_2:def 1;
hence z in Funcs (X1,ExtREAL) by I4, I5, FUNCT_2:def 2; :: thesis:

end;

then rng I c= Funcs (X1,ExtREAL) ;
then reconsider I = I as FinSequence of Funcs (X1,ExtREAL) by FINSEQ_1:def 4;
I6: for x being Element of X1
for n being Nat st n in dom I holds
(I . n) . x = Integral (M2,(ProjMap1 ((C /. n),x)))

proof

let x be Element of X1; :: thesis:
let n be Nat; :: thesis:
assume I7: n in dom I ; :: thesis:
then n in dom F by I3, FINSEQ_1:def 3;
then reconsider Fn = F . n as Element of sigma (measurable_rectangles (S1,S2)) by A3, PARTFUN1:4;
ex f being Function of X1,ExtREAL st
( f = I . n & ( for x being Element of X1 holds f . x = Integral (M2,(ProjMap1 ((C /. n),x))) ) ) by I3, I7;
hence (I . n) . x = Integral (M2,(ProjMap1 ((C /. n),x))) ; :: thesis:

end;

I7: now :: thesis:

let n be Nat; :: thesis:
assume I8: n in dom I ; :: thesis:
then consider f being Function of X1,ExtREAL such that
I9: ( f = I . n & ( for x being Element of X1 holds f . x = Integral (M2,(ProjMap1 ((C /. n),x))) ) ) by I3;
I10: n in dom F by I3, I8, FINSEQ_1:def 3;
then reconsider Fn = F . n as Element of sigma (measurable_rectangles (S1,S2)) by A3, PARTFUN1:4;
F . n in measurable_rectangles (S1,S2) by I10, 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
I11: F . n = [:An,Bn:] ;
for x being Element of X1 holds 0 <= f . x

proof

let x be Element of X1; :: thesis:
I12: n in dom C by I3, I8, A2, FINSEQ_1:def 3;
then C /. n = C . n by PARTFUN1:def 6;
then I13: C /. n = chi ((F . n),[:X1,X2:]) by A2, I12;
f . x = Integral (M2,(ProjMap1 ((C /. n),x))) by I9;
then I14: f . x = (M2 . (Measurable-X-section (Fn,x))) * ((chi (An,X1)) . x) by I11, I13, Th65;
( M2 . (Measurable-X-section (Fn,x)) >= 0 & (chi (An,X1)) . x >= 0 ) by SUPINF_2:51;
hence 0 <= f . x by I14; :: thesis:

end;

then I . n is nonnegative Function of X1,ExtREAL by I9, SUPINF_2:39;
hence I . n is without-infty ; :: thesis:

end;

then I15: I is without_-infty-valued ;
then reconsider I = I as summable FinSequence of Funcs (X1,ExtREAL) ;
defpred S₂[ Nat, object ] means ex f being Function of X2,ExtREAL st
( f = $2 & ( for x being Element of X2 holds f . x = Integral (M1,(ProjMap2 ((C /. $1),x))) ) );
J1: for n being Nat st n in Seg (len F) holds
ex z being object st S₂[n,z]

proof

let n be Nat; :: thesis:
assume n in Seg (len F) ; :: thesis:
deffunc H₁( Element of X2) -> Element of ExtREAL = Integral (M1,(ProjMap2 ((C /. n),$1)));
consider f being Function of X2,ExtREAL such that
J2: for x being Element of X2 holds f . x = H₁(x) from FUNCT_2:sch 4();
take z = f; :: thesis:
thus ex f being Function of X2,ExtREAL st
( f = z & ( for x being Element of X2 holds f . x = Integral (M1,(ProjMap2 ((C /. n),x))) ) ) by J2; :: thesis:

end;

consider J being FinSequence such that
J3: ( dom J = Seg (len F) & ( for n being Nat st n in Seg (len F) holds
S₂[n,J . n] ) ) from FINSEQ_1:sch 1(J1);

now :: thesis:

let z be set ; :: thesis:
assume z in rng J ; :: thesis:
then consider n being object such that
J4: ( n in dom J & z = J . n ) by FUNCT_1:def 3;
reconsider n = n as Element of NAT by J4;
consider f being Function of X2,ExtREAL such that
J5: ( f = J . n & ( for x being Element of X2 holds f . x = Integral (M1,(ProjMap2 ((C /. n),x))) ) ) by J3, J4;
( dom f = X2 & rng f c= ExtREAL ) by FUNCT_2:def 1;
hence z in Funcs (X2,ExtREAL) by J4, J5, FUNCT_2:def 2; :: thesis:

end;

then rng J c= Funcs (X2,ExtREAL) ;
then reconsider J = J as FinSequence of Funcs (X2,ExtREAL) by FINSEQ_1:def 4;
J6: for x being Element of X2
for n being Nat st n in dom J holds
(J . n) . x = Integral (M1,(ProjMap2 ((C /. n),x)))

proof

let x be Element of X2; :: thesis:
let n be Nat; :: thesis:
assume J7: n in dom J ; :: thesis:
then n in dom F by J3, FINSEQ_1:def 3;
then reconsider Fn = F . n as Element of sigma (measurable_rectangles (S1,S2)) by A3, PARTFUN1:4;
ex f being Function of X2,ExtREAL st
( f = J . n & ( for x being Element of X2 holds f . x = Integral (M1,(ProjMap2 ((C /. n),x))) ) ) by J3, J7;
hence (J . n) . x = Integral (M1,(ProjMap2 ((C /. n),x))) ; :: thesis:

end;

J7: now :: thesis:

let n be Nat; :: thesis:
assume J8: n in dom J ; :: thesis:
then consider f being Function of X2,ExtREAL such that
J9: ( f = J . n & ( for x being Element of X2 holds f . x = Integral (M1,(ProjMap2 ((C /. n),x))) ) ) by J3;
J10: n in dom F by J3, J8, FINSEQ_1:def 3;
then reconsider Fn = F . n as Element of sigma (measurable_rectangles (S1,S2)) by A3, PARTFUN1:4;
F . n in measurable_rectangles (S1,S2) by J10, 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
J11: F . n = [:An,Bn:] ;
for x being Element of X2 holds 0 <= f . x

proof

let x be Element of X2; :: thesis:
J12: n in dom C by J3, J8, A2, FINSEQ_1:def 3;
then C /. n = C . n by PARTFUN1:def 6;
then J13: C /. n = chi ((F . n),[:X1,X2:]) by A2, J12;
f . x = Integral (M1,(ProjMap2 ((C /. n),x))) by J9;
then J14: f . x = (M1 . (Measurable-Y-section (Fn,x))) * ((chi (Bn,X2)) . x) by J11, J13, Th65;
( M1 . (Measurable-Y-section (Fn,x)) >= 0 & (chi (Bn,X2)) . x >= 0 ) by SUPINF_2:51;
hence 0 <= f . x by J14; :: thesis:

end;

then J . n is nonnegative Function of X2,ExtREAL by J9, SUPINF_2:39;
hence J . n is without-infty ; :: thesis:

end;

then J15: J is without_-infty-valued ;
then reconsider J = J as summable FinSequence of Funcs (X2,ExtREAL) ;
take F ; :: thesis:
take A ; :: thesis:
take B ; :: thesis:
take C ; :: thesis:
take I ; :: thesis:
take J ; :: thesis:
thus ( E = Union F & len F in dom F & len F = len A & len F = len B & len F = len C ) by A2; :: thesis:
thus K1: ( len F = len I & len F = len J ) by I3, J3, FINSEQ_1:def 3; :: thesis:
thus for n being Nat st n in dom C holds
C . n = chi ((F . n),[:X1,X2:]) by A2; :: thesis:
len C = len (Partial_Sums C) by DEF13;
then dom F = dom (Partial_Sums C) by A2, FINSEQ_3:29;
hence (Partial_Sums C) /. (len C) = chi (E,[:X1,X2:]) by A2, PARTFUN1:def 6; :: thesis:
thus for x being Element of X1
for n being Nat st n in dom I holds
(I . n) . x = Integral (M2,(ProjMap1 ((C /. n),x))) by I6; :: thesis:
thus for n being Nat
for P being Element of S1 st n in dom I holds
I /. n is P -measurable :: thesis:

proof

let n be Nat; :: thesis:
let P be Element of S1; :: thesis:
assume I16: n in dom I ; :: thesis:
then consider f being Function of X1,ExtREAL such that
I17: ( f = I . n & ( for x being Element of X1 holds f . x = Integral (M2,(ProjMap1 ((C /. n),x))) ) ) by I3;
I18: I /. n = f by I16, I17, PARTFUN1:def 6;
I19: n in dom F by I3, I16, FINSEQ_1:def 3;
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
I20: F . n = [:An,Bn:] ;
reconsider Fn = F . n as Element of sigma (measurable_rectangles (S1,S2)) by A3, I19, PARTFUN1:4;

per cases ;

suppose I21: M2 . Bn = +infty ; :: thesis:

for x being Element of X1 holds f . x = (Xchi (An,X1)) . x

proof

let x be Element of X1; :: thesis:
I22: f . x = Integral (M2,(ProjMap1 ((C /. n),x))) by I17;
I23: n in dom C by I3, I16, A2, FINSEQ_1:def 3;
then C /. n = C . n by PARTFUN1:def 6;
then C /. n = chi ((F . n),[:X1,X2:]) by A2, I23;
then I24: f . x = (M2 . (Measurable-X-section (Fn,x))) * ((chi (An,X1)) . x) by I20, I22, Th65;

per cases ;

suppose I25: x in An ; :: thesis:

then ( M2 . (Measurable-X-section (Fn,x)) = +infty & (chi (An,X1)) . x = 1 ) by I20, I21, Th16, FUNCT_3:def 3;
then f . x = +infty by I24, XXREAL_3:81;
hence f . x = (Xchi (An,X1)) . x by I25, MEASUR10:def 7; :: thesis:

end;

suppose I26: not x in An ; :: thesis:

then (chi (An,X1)) . x = 0 by FUNCT_3:def 3;
then f . x = 0 by I24;
hence f . x = (Xchi (An,X1)) . x by I26, MEASUR10:def 7; :: thesis:

end;

then f = Xchi (An,X1) by FUNCT_2:def 8;
hence I /. n is P -measurable by I18, MEASUR10:32; :: thesis:

end;

suppose I27: M2 . Bn <> +infty ; :: thesis:

M2 . Bn >= 0 by SUPINF_2:51;
then M2 . Bn in REAL by I27, XXREAL_0:14;
then reconsider r = M2 . Bn as Real ;
I28: dom (chi (An,X1)) = X1 by FUNCT_2:def 1;
then I29: ( dom f = X1 & dom (r (#) (chi (An,X1))) = X1 ) by MESFUNC1:def 6, FUNCT_2:def 1;
for x being Element of X1 st x in dom f holds
f . x = (r (#) (chi (An,X1))) . x

proof

let x be Element of X1; :: thesis:
assume x in dom f ; :: thesis:
I30: f . x = Integral (M2,(ProjMap1 ((C /. n),x))) by I17;
I31: n in dom C by I3, I16, A2, FINSEQ_1:def 3;
then C /. n = C . n by PARTFUN1:def 6;
then C /. n = chi ((F . n),[:X1,X2:]) by I31, A2;
then I32: f . x = (M2 . (Measurable-X-section (Fn,x))) * ((chi (An,X1)) . x) by I20, I30, Th65;
I33: (r (#) (chi (An,X1))) . x = r * ((chi (An,X1)) . x) by I29, MESFUNC1:def 6;

per cases ;

suppose x in An ; :: thesis:

hence f . x = (r (#) (chi (An,X1))) . x by I33, I32, I20, Th16; :: thesis:

end;

suppose not x in An ; :: thesis:

then I34: (chi (An,X1)) . x = 0 by FUNCT_3:def 3;
(r (#) (chi (An,X1))) . x = r * ((chi (An,X1)) . x) by I29, MESFUNC1:def 6;
hence f . x = (r (#) (chi (An,X1))) . x by I34, I32; :: thesis:

end;

then f = r (#) (chi (An,X1)) by I29, PARTFUN1:5;
hence I /. n is P -measurable by I18, I28, MESFUNC2:29, MESFUNC1:37; :: thesis:

end;

thus for x being Element of X1 holds Integral (M2,(ProjMap1 (((Partial_Sums C) /. (len C)),x))) = ((Partial_Sums I) /. (len I)) . x :: thesis:

proof

let x be Element of X1; :: thesis:
defpred S₃[ Nat] means ( $1 in dom I implies ((Partial_Sums I) . $1) . x = Integral (M2,(ProjMap1 ((chi ((union (rng (F | $1))),[:X1,X2:])),x))) );
I35: S₃[ 0 ] by FINSEQ_3:24;
I36: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis:
assume I37: S₃[k] ; :: thesis:
assume I38: k + 1 in dom I ; :: thesis:
then I39: ( 1 <= k + 1 & k + 1 <= len I ) by FINSEQ_3:25;
then I40: k < len I by NAT_1:13;
then I41: k < len (Partial_Sums I) by DEF13;

per cases ;

suppose I42: k = 0 ; :: thesis:

I43: 1 <= len I by I39, XXREAL_0:2;
then consider f being Function of X1,ExtREAL such that
I44: ( f = I . 1 & ( for x being Element of X1 holds f . x = Integral (M2,(ProjMap1 ((C /. 1),x))) ) ) by I3, FINSEQ_3:25;
1 in Seg (len F) by I43, I3, FINSEQ_3:25;
then I46: 1 in dom C by A2, FINSEQ_1:def 3;
then I47: C /. 1 = C . 1 by PARTFUN1:def 6
.= chi ((F . 1),[:X1,X2:]) by I46, A2 ;
F <> {} by I38, I3;
then F | 1 = <*(F . 1)*> by FINSEQ_5:20;
then rng (F | 1) = {(F . 1)} by FINSEQ_1:39;
then I49: C /. 1 = chi ((union (rng (F | 1))),[:X1,X2:]) by I47, ZFMISC_1:25;
(Partial_Sums I) . (k + 1) = f by I42, I44, DEF13;
hence ((Partial_Sums I) . (k + 1)) . x = Integral (M2,(ProjMap1 ((chi ((union (rng (F | (k + 1)))),[:X1,X2:])),x))) by I44, I49, I42; :: thesis:

end;

suppose k <> 0 ; :: thesis:

then I50: 1 <= k by NAT_1:14;
k <= len (Partial_Sums I) by I40, DEF13;
then I51: k in dom (Partial_Sums I) by I50, FINSEQ_3:25;
then I52: ((Partial_Sums I) /. k) . x = Integral (M2,(ProjMap1 ((chi ((union (rng (F | k))),[:X1,X2:])),x))) by I37, I50, I40, FINSEQ_3:25, PARTFUN1:def 6
.= Integral (M2,(ProjMap1 ((chi ((Union (F | k)),[:X1,X2:])),x))) by CARD_3:def 4 ;
I53: ((Partial_Sums I) . (k + 1)) . x = (((Partial_Sums I) /. k) + (I /. (k + 1))) . x by I39, I50, NAT_1:13, DEF13;
Partial_Sums I is without_-infty-valued by I15, Th57;
then (Partial_Sums I) . k is without-infty by I50, I41, FINSEQ_3:25;
then I54: (Partial_Sums I) /. k is without-infty by I51, PARTFUN1:def 6;
I . (k + 1) is without-infty by I7, I38;
then I /. (k + 1) is without-infty by I38, PARTFUN1:def 6;
then dom (((Partial_Sums I) /. k) + (I /. (k + 1))) = (dom ((Partial_Sums I) /. k)) /\ (dom (I /. (k + 1))) by I54, MESFUNC5:16
.= X1 /\ (dom (I /. (k + 1))) by FUNCT_2:def 1
.= X1 /\ X1 by FUNCT_2:def 1
.= X1 ;
then I55: ((Partial_Sums I) . (k + 1)) . x = (((Partial_Sums I) /. k) . x) + ((I /. (k + 1)) . x) by I53, MESFUNC1:def 3;
reconsider E1 = Union (F | k) as Element of sigma (measurable_rectangles (S1,S2)) by Th71;
I56: ( k + 1 in dom C & k + 1 in dom F ) by A2, I38, I3, FINSEQ_1:def 3;
then reconsider E2 = F . (k + 1) as Element of sigma (measurable_rectangles (S1,S2)) by A3, FINSEQ_2:11;
I57: C /. (k + 1) = C . (k + 1) by I56, PARTFUN1:def 6
.= chi (E2,[:X1,X2:]) by A2, I56 ;
I /. (k + 1) = I . (k + 1) by I38, PARTFUN1:def 6;
then I58: ((Partial_Sums I) . (k + 1)) . x = (Integral (M2,(ProjMap1 ((chi (E1,[:X1,X2:])),x)))) + (Integral (M2,(ProjMap1 ((C /. (k + 1)),x)))) by I6, I38, I52, I55
.= (M2 . (Measurable-X-section (E1,x))) + (Integral (M2,(ProjMap1 ((chi (E2,[:X1,X2:])),x)))) by I57, Th68
.= (M2 . (Measurable-X-section (E1,x))) + (M2 . (Measurable-X-section (E2,x))) by Th68 ;
k < k + 1 by NAT_1:13;
then union (rng (F | k)) misses F . (k + 1) by Th72;
then I59: E1 misses E2 by CARD_3:def 4;
(union (rng (F | k))) \/ (F . (k + 1)) = union (rng (F | (k + 1))) by Th74;
then I60: E1 \/ E2 = union (rng (F | (k + 1))) by CARD_3:def 4;
then reconsider E3 = union (rng (F | (k + 1))) as Element of sigma (measurable_rectangles (S1,S2)) ;
M2 . ((Measurable-X-section (E1,x)) \/ (Measurable-X-section (E2,x))) = M2 . (Measurable-X-section (E3,x)) by I60, Th20
.= Integral (M2,(ProjMap1 ((chi ((union (rng (F | (k + 1)))),[:X1,X2:])),x))) by Th68 ;
hence ((Partial_Sums I) . (k + 1)) . x = Integral (M2,(ProjMap1 ((chi ((union (rng (F | (k + 1)))),[:X1,X2:])),x))) by I59, I58, Th29, MEASURE1:30; :: thesis:

end;

I61: for k being Nat holds S₃[k] from NAT_1:sch 2(I35, I36);
I62: I <> {} by A2, I3, FINSEQ_1:def 3;
then len I in dom I by FINSEQ_5:6;
then len I in Seg (len I) by FINSEQ_1:def 3;
then len I in Seg (len (Partial_Sums I)) by DEF13;
then len I in dom (Partial_Sums I) by FINSEQ_1:def 3;
then I63: ((Partial_Sums I) /. (len I)) . x = ((Partial_Sums I) . (len I)) . x by PARTFUN1:def 6
.= Integral (M2,(ProjMap1 ((chi ((union (rng (F | (len I)))),[:X1,X2:])),x))) by I61, I62, FINSEQ_5:6 ;
E = union (rng F) by A2, CARD_3:def 4
.= union (rng (F | (len I))) by K1, FINSEQ_1:58 ;
hence Integral (M2,(ProjMap1 (((Partial_Sums C) /. (len C)),x))) = ((Partial_Sums I) /. (len I)) . x by A2, I63; :: thesis:

end;

thus for x being Element of X2
for n being Nat st n in dom J holds
(J . n) . x = Integral (M1,(ProjMap2 ((C /. n),x))) by J6; :: thesis:
thus for n being Nat
for P being Element of S2 st n in dom J holds
J /. n is P -measurable :: thesis:

proof

let n be Nat; :: thesis:
let P be Element of S2; :: thesis:
assume I16: n in dom J ; :: thesis:
then consider f being Function of X2,ExtREAL such that
I17: ( f = J . n & ( for x being Element of X2 holds f . x = Integral (M1,(ProjMap2 ((C /. n),x))) ) ) by J3;
I18: J /. n = f by I16, I17, PARTFUN1:def 6;
I19: n in dom F by J3, I16, FINSEQ_1:def 3;
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
I20: F . n = [:An,Bn:] ;
reconsider Fn = F . n as Element of sigma (measurable_rectangles (S1,S2)) by A3, I19, PARTFUN1:4;

per cases ;

suppose I21: M1 . An = +infty ; :: thesis:

for x being Element of X2 holds f . x = (Xchi (Bn,X2)) . x

proof

let x be Element of X2; :: thesis:
I22: f . x = Integral (M1,(ProjMap2 ((C /. n),x))) by I17;
I23: n in dom C by J3, I16, A2, FINSEQ_1:def 3;
then C /. n = C . n by PARTFUN1:def 6;
then C /. n = chi ((F . n),[:X1,X2:]) by A2, I23;
then I24: f . x = (M1 . (Measurable-Y-section (Fn,x))) * ((chi (Bn,X2)) . x) by I20, I22, Th65;

per cases ;

suppose I25: x in Bn ; :: thesis:

then ( M1 . (Measurable-Y-section (Fn,x)) = +infty & (chi (Bn,X2)) . x = 1 ) by I20, I21, Th16, FUNCT_3:def 3;
then f . x = +infty by I24, XXREAL_3:81;
hence f . x = (Xchi (Bn,X2)) . x by I25, MEASUR10:def 7; :: thesis:

end;

suppose I26: not x in Bn ; :: thesis:

then (chi (Bn,X2)) . x = 0 by FUNCT_3:def 3;
then f . x = 0 by I24;
hence f . x = (Xchi (Bn,X2)) . x by I26, MEASUR10:def 7; :: thesis:

end;

then f = Xchi (Bn,X2) by FUNCT_2:def 8;
hence J /. n is P -measurable by I18, MEASUR10:32; :: thesis:

end;

suppose I27: M1 . An <> +infty ; :: thesis:

M1 . An >= 0 by SUPINF_2:51;
then M1 . An in REAL by I27, XXREAL_0:14;
then reconsider r = M1 . An as Real ;
I28: dom (chi (Bn,X2)) = X2 by FUNCT_2:def 1;
then I29: ( dom f = X2 & dom (r (#) (chi (Bn,X2))) = X2 ) by MESFUNC1:def 6, FUNCT_2:def 1;
for x being Element of X2 st x in dom f holds
f . x = (r (#) (chi (Bn,X2))) . x

proof

let x be Element of X2; :: thesis:
assume x in dom f ; :: thesis:
I30: f . x = Integral (M1,(ProjMap2 ((C /. n),x))) by I17;
I31: n in dom C by J3, I16, A2, FINSEQ_1:def 3;
then C /. n = C . n by PARTFUN1:def 6;
then C /. n = chi ((F . n),[:X1,X2:]) by I31, A2;
then I32: f . x = (M1 . (Measurable-Y-section (Fn,x))) * ((chi (Bn,X2)) . x) by I20, I30, Th65;
I33: (r (#) (chi (Bn,X2))) . x = r * ((chi (Bn,X2)) . x) by I29, MESFUNC1:def 6;

per cases ;

suppose x in Bn ; :: thesis:

hence f . x = (r (#) (chi (Bn,X2))) . x by I33, I32, I20, Th16; :: thesis:

end;

suppose not x in Bn ; :: thesis:

then I34: (chi (Bn,X2)) . x = 0 by FUNCT_3:def 3;
(r (#) (chi (Bn,X2))) . x = r * ((chi (Bn,X2)) . x) by I29, MESFUNC1:def 6;
hence f . x = (r (#) (chi (Bn,X2))) . x by I34, I32; :: thesis:

end;

then f = r (#) (chi (Bn,X2)) by I29, PARTFUN1:5;
hence J /. n is P -measurable by I18, I28, MESFUNC2:29, MESFUNC1:37; :: thesis:

end;

thus for x being Element of X2 holds Integral (M1,(ProjMap2 (((Partial_Sums C) /. (len C)),x))) = ((Partial_Sums J) /. (len J)) . x :: thesis:

proof

let x be Element of X2; :: thesis:
defpred S₃[ Nat] means ( $1 in dom J implies ((Partial_Sums J) . $1) . x = Integral (M1,(ProjMap2 ((chi ((union (rng (F | $1))),[:X1,X2:])),x))) );
I35: S₃[ 0 ] by FINSEQ_3:24;
I36: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis:
assume I37: S₃[k] ; :: thesis:
assume I38: k + 1 in dom J ; :: thesis:
then I39: ( 1 <= k + 1 & k + 1 <= len J ) by FINSEQ_3:25;
then I40: k < len J by NAT_1:13;
then I41: k < len (Partial_Sums J) by DEF13;

per cases ;

suppose I42: k = 0 ; :: thesis:

I43: 1 <= len J by I39, XXREAL_0:2;
then consider f being Function of X2,ExtREAL such that
I44: ( f = J . 1 & ( for x being Element of X2 holds f . x = Integral (M1,(ProjMap2 ((C /. 1),x))) ) ) by J3, FINSEQ_3:25;
1 in Seg (len F) by I43, J3, FINSEQ_3:25;
then I46: 1 in dom C by A2, FINSEQ_1:def 3;
then I47: C /. 1 = C . 1 by PARTFUN1:def 6
.= chi ((F . 1),[:X1,X2:]) by I46, A2 ;
F <> {} by I38, J3;
then F | 1 = <*(F . 1)*> by FINSEQ_5:20;
then rng (F | 1) = {(F . 1)} by FINSEQ_1:39;
then I49: C /. 1 = chi ((union (rng (F | 1))),[:X1,X2:]) by I47, ZFMISC_1:25;
(Partial_Sums J) . (k + 1) = f by I42, I44, DEF13;
hence ((Partial_Sums J) . (k + 1)) . x = Integral (M1,(ProjMap2 ((chi ((union (rng (F | (k + 1)))),[:X1,X2:])),x))) by I44, I49, I42; :: thesis:

end;

suppose k <> 0 ; :: thesis:

then I50: 1 <= k by NAT_1:14;
k <= len (Partial_Sums J) by I40, DEF13;
then I51: k in dom (Partial_Sums J) by I50, FINSEQ_3:25;
then I52: ((Partial_Sums J) /. k) . x = Integral (M1,(ProjMap2 ((chi ((union (rng (F | k))),[:X1,X2:])),x))) by I37, I50, I40, FINSEQ_3:25, PARTFUN1:def 6
.= Integral (M1,(ProjMap2 ((chi ((Union (F | k)),[:X1,X2:])),x))) by CARD_3:def 4 ;
I53: ((Partial_Sums J) . (k + 1)) . x = (((Partial_Sums J) /. k) + (J /. (k + 1))) . x by I39, I50, NAT_1:13, DEF13;
Partial_Sums J is without_-infty-valued by J15, Th57;
then (Partial_Sums J) . k is without-infty by I50, I41, FINSEQ_3:25;
then I54: (Partial_Sums J) /. k is without-infty by I51, PARTFUN1:def 6;
J . (k + 1) is without-infty by J7, I38;
then J /. (k + 1) is without-infty by I38, PARTFUN1:def 6;
then dom (((Partial_Sums J) /. k) + (J /. (k + 1))) = (dom ((Partial_Sums J) /. k)) /\ (dom (J /. (k + 1))) by I54, MESFUNC5:16
.= X2 /\ (dom (J /. (k + 1))) by FUNCT_2:def 1
.= X2 /\ X2 by FUNCT_2:def 1
.= X2 ;
then I55: ((Partial_Sums J) . (k + 1)) . x = (((Partial_Sums J) /. k) . x) + ((J /. (k + 1)) . x) by I53, MESFUNC1:def 3;
reconsider E1 = Union (F | k) as Element of sigma (measurable_rectangles (S1,S2)) by Th71;
I56: ( k + 1 in dom C & k + 1 in dom F ) by A2, I38, J3, FINSEQ_1:def 3;
then reconsider E2 = F . (k + 1) as Element of sigma (measurable_rectangles (S1,S2)) by A3, FINSEQ_2:11;
I57: C /. (k + 1) = C . (k + 1) by I56, PARTFUN1:def 6
.= chi (E2,[:X1,X2:]) by A2, I56 ;
J /. (k + 1) = J . (k + 1) by I38, PARTFUN1:def 6;
then I58: ((Partial_Sums J) . (k + 1)) . x = (Integral (M1,(ProjMap2 ((chi (E1,[:X1,X2:])),x)))) + (Integral (M1,(ProjMap2 ((C /. (k + 1)),x)))) by J6, I38, I52, I55
.= (M1 . (Measurable-Y-section (E1,x))) + (Integral (M1,(ProjMap2 ((chi (E2,[:X1,X2:])),x)))) by I57, Th68
.= (M1 . (Measurable-Y-section (E1,x))) + (M1 . (Measurable-Y-section (E2,x))) by Th68 ;
k < k + 1 by NAT_1:13;
then union (rng (F | k)) misses F . (k + 1) by Th72;
then I59: E1 misses E2 by CARD_3:def 4;
(union (rng (F | k))) \/ (F . (k + 1)) = union (rng (F | (k + 1))) by Th74;
then I60: E1 \/ E2 = union (rng (F | (k + 1))) by CARD_3:def 4;
then reconsider E3 = union (rng (F | (k + 1))) as Element of sigma (measurable_rectangles (S1,S2)) ;
M1 . ((Measurable-Y-section (E1,x)) \/ (Measurable-Y-section (E2,x))) = M1 . (Measurable-Y-section (E3,x)) by I60, Th20
.= Integral (M1,(ProjMap2 ((chi ((union (rng (F | (k + 1)))),[:X1,X2:])),x))) by Th68 ;
hence ((Partial_Sums J) . (k + 1)) . x = Integral (M1,(ProjMap2 ((chi ((union (rng (F | (k + 1)))),[:X1,X2:])),x))) by I59, I58, Th29, MEASURE1:30; :: thesis:

end;

I61: for k being Nat holds S₃[k] from NAT_1:sch 2(I35, I36);
I62: J <> {} by A2, J3, FINSEQ_1:def 3;
then len J in dom J by FINSEQ_5:6;
then len J in Seg (len J) by FINSEQ_1:def 3;
then len J in Seg (len (Partial_Sums J)) by DEF13;
then len J in dom (Partial_Sums J) by FINSEQ_1:def 3;
then I63: ((Partial_Sums J) /. (len J)) . x = ((Partial_Sums J) . (len J)) . x by PARTFUN1:def 6
.= Integral (M1,(ProjMap2 ((chi ((union (rng (F | (len J)))),[:X1,X2:])),x))) by I61, I62, FINSEQ_5:6 ;
E = union (rng F) by A2, CARD_3:def 4
.= union (rng (F | (len J))) by K1, FINSEQ_1:58 ;
hence Integral (M1,(ProjMap2 (((Partial_Sums C) /. (len C)),x))) = ((Partial_Sums J) /. (len J)) . x by A2, I63; :: thesis:

end;