let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for K being disjoint_valued Function of NAT,(measurable_rectangles (S1,S2)) st Union K in measurable_rectangles (S1,S2) holds
(product-pre-Measure (M1,M2)) . (Union K) = SUM ((product-pre-Measure (M1,M2)) * K)
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for K being disjoint_valued Function of NAT,(measurable_rectangles (S1,S2)) st Union K in measurable_rectangles (S1,S2) holds
(product-pre-Measure (M1,M2)) . (Union K) = SUM ((product-pre-Measure (M1,M2)) * K)
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for K being disjoint_valued Function of NAT,(measurable_rectangles (S1,S2)) st Union K in measurable_rectangles (S1,S2) holds
(product-pre-Measure (M1,M2)) . (Union K) = SUM ((product-pre-Measure (M1,M2)) * K)
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for K being disjoint_valued Function of NAT,(measurable_rectangles (S1,S2)) st Union K in measurable_rectangles (S1,S2) holds
(product-pre-Measure (M1,M2)) . (Union K) = SUM ((product-pre-Measure (M1,M2)) * K)
let M2 be sigma_Measure of S2; :: thesis: for K being disjoint_valued Function of NAT,(measurable_rectangles (S1,S2)) st Union K in measurable_rectangles (S1,S2) holds
(product-pre-Measure (M1,M2)) . (Union K) = SUM ((product-pre-Measure (M1,M2)) * K)
let K be disjoint_valued Function of NAT,(measurable_rectangles (S1,S2)); :: thesis: ( Union K in measurable_rectangles (S1,S2) implies (product-pre-Measure (M1,M2)) . (Union K) = SUM ((product-pre-Measure (M1,M2)) * K) )
assume A1: Union K in measurable_rectangles (S1,S2) ; :: thesis: (product-pre-Measure (M1,M2)) . (Union K) = SUM ((product-pre-Measure (M1,M2)) * K)
then consider A being Element of S1, B being Element of S2 such that
A2: Union K = [:A,B:] ;
consider P being Element of S1, Q being Element of S2 such that
Q1: ( Union K = [:P,Q:] & (product-pre-Measure (M1,M2)) . (Union K) = (M1 . P) * (M2 . Q) ) by A1, Def6;
A10: ( A c= X1 & B c= X2 ) ;
deffunc H₁( object ) -> Element of bool [:[:X1,X2:],ExtREAL:] = chi ((K . $1),[:X1,X2:]);
consider XK being Functional_Sequence of [:X1,X2:],ExtREAL such that
A3: for n being Nat holds XK . n = H₁(n) from SEQFUNC:sch 1();
K1: dom XK = NAT by FUNCT_2:def 1;

now :: thesis: for n being object st n in NAT holds
XK . n in Funcs ([:X1,X2:],ExtREAL)

let n be object ; :: thesis: ( n in NAT implies XK . n in Funcs ([:X1,X2:],ExtREAL) )
assume n in NAT ; :: thesis: XK . n in Funcs ([:X1,X2:],ExtREAL)
then reconsider n1 = n as Nat ;
K2: XK . n = chi ((K . n1),[:X1,X2:]) by A3;
K3: dom (chi ((K . n1),[:X1,X2:])) = [:X1,X2:] by FUNCT_3:def 3;
rng (chi ((K . n1),[:X1,X2:])) c= ExtREAL ;
hence XK . n in Funcs ([:X1,X2:],ExtREAL) by K2, K3, FUNCT_2:def 2; :: thesis: verum

end;

then reconsider XXK = XK as sequence of (Funcs ([:X1,X2:],ExtREAL)) by K1, FUNCT_2:3;
defpred S₁[ Nat, object ] means $2 = proj1 (K . $1);
B0: for i being Element of NAT ex A being Element of S1 st S₁[i,A]

proof

let i be Element of NAT ; :: thesis: ex A being Element of S1 st S₁[i,A]
K . i in measurable_rectangles (S1,S2) ;
then consider Ai being Element of S1, Bi being Element of S2 such that
B1: K . i = [:Ai,Bi:] ;

per cases ( Bi <> {} or Bi = {} ) ;

suppose B2: Bi <> {} ; :: thesis: ex A being Element of S1 st S₁[i,A]

take Ai ; :: thesis: S₁[i,Ai]
thus proj1 (K . i) = Ai by B1, B2, FUNCT_5:9; :: thesis: verum

end;

suppose B3: Bi = {} ; :: thesis: ex A being Element of S1 st S₁[i,A]

reconsider Ai = {} as Element of S1 by MEASURE1:7;
take Ai ; :: thesis: S₁[i,Ai]
thus proj1 (K . i) = Ai by B3, B1; :: thesis: verum

end;

end;

end;

consider D being Function of NAT,S1 such that
B4: for i being Element of NAT holds S₁[i,D . i] from FUNCT_2:sch 3(B0);
defpred S₂[ Nat, object ] means $2 = proj2 (K . $1);
C0: for i being Element of NAT ex B being Element of S2 st S₂[i,B]

proof

let i be Element of NAT ; :: thesis: ex B being Element of S2 st S₂[i,B]
K . i in measurable_rectangles (S1,S2) ;
then consider Ai being Element of S1, Bi being Element of S2 such that
C1: K . i = [:Ai,Bi:] ;

per cases ( Ai <> {} or Ai = {} ) ;

suppose C2: Ai <> {} ; :: thesis: ex B being Element of S2 st S₂[i,B]

take Bi ; :: thesis: S₂[i,Bi]
thus proj2 (K . i) = Bi by C1, C2, FUNCT_5:9; :: thesis: verum

end;

suppose C3: Ai = {} ; :: thesis: ex B being Element of S2 st S₂[i,B]

reconsider Bi = {} as Element of S2 by MEASURE1:7;
take Bi ; :: thesis: S₂[i,Bi]
thus proj2 (K . i) = Bi by C1, C3; :: thesis: verum

end;

end;

end;

consider E being Function of NAT,S2 such that
C4: for i being Element of NAT holds S₂[i,E . i] from FUNCT_2:sch 3(C0);
deffunc H₂( object ) -> Element of bool [:X1,ExtREAL:] = chi ((D . $1),X1);
consider XD being Functional_Sequence of X1,ExtREAL such that
B5: for n being Nat holds XD . n = H₂(n) from SEQFUNC:sch 1();
deffunc H₃( object ) -> Element of bool [:X2,ExtREAL:] = chi ((E . $1),X2);
consider XE being Functional_Sequence of X2,ExtREAL such that
C5: for n being Nat holds XE . n = H₃(n) from SEQFUNC:sch 1();
E0: for n being Nat
for x, y being object st x in X1 & y in X2 holds
(XK . n) . (x,y) = ((XD . n) . x) * ((XE . n) . y)

proof

let n be Nat; :: thesis: for x, y being object st x in X1 & y in X2 holds
(XK . n) . (x,y) = ((XD . n) . x) * ((XE . n) . y)
let x, y be object ; :: thesis: ( x in X1 & y in X2 implies (XK . n) . (x,y) = ((XD . n) . x) * ((XE . n) . y) )
assume E1: ( x in X1 & y in X2 ) ; :: thesis: (XK . n) . (x,y) = ((XD . n) . x) * ((XE . n) . y)
then E7: [x,y] in [:X1,X2:] by ZFMISC_1:87;
E5: ( XK . n = chi ((K . n),[:X1,X2:]) & XD . n = chi ((D . n),X1) & XE . n = chi ((E . n),X2) ) by A3, B5, C5;
E2: n in NAT by ORDINAL1:def 12;
K . n in measurable_rectangles (S1,S2) ;
then consider An being Element of S1, Bn being Element of S2 such that
E3: K . n = [:An,Bn:] ;
E4: ( D . n = proj1 (K . n) & E . n = proj2 (K . n) ) by B4, C4, E2;

per cases ( ( x in An & y in Bn ) or not x in An or not y in Bn ) ;

suppose ( x in An & y in Bn ) ; :: thesis: (XK . n) . (x,y) = ((XD . n) . x) * ((XE . n) . y)

then ( D . n = An & E . n = Bn ) by E4, E3, FUNCT_5:9;
hence (XK . n) . (x,y) = ((XD . n) . x) * ((XE . n) . y) by E5, E3, E1, Th26; :: thesis: verum

end;

suppose ( not x in An or not y in Bn ) ; :: thesis: (XK . n) . (x,y) = ((XD . n) . x) * ((XE . n) . y)

then not [x,y] in [:An,Bn:] by ZFMISC_1:87;
then E8: (XK . n) . (x,y) = 0 by E7, E5, E3, FUNCT_3:def 3;

per cases ( [:An,Bn:] = {} or [:An,Bn:] <> {} ) ;

suppose [:An,Bn:] = {} ; :: thesis: (XK . n) . (x,y) = ((XD . n) . x) * ((XE . n) . y)

then ( (XD . n) . x = 0 & (XE . n) . y = 0 ) by E4, E3, E5, E1, FUNCT_3:def 3;
hence (XK . n) . (x,y) = ((XD . n) . x) * ((XE . n) . y) by E8; :: thesis: verum

end;

suppose [:An,Bn:] <> {} ; :: thesis: (XK . n) . (x,y) = ((XD . n) . x) * ((XE . n) . y)

then ( D . n = An & E . n = Bn ) by E4, E3, FUNCT_5:9;
hence (XK . n) . (x,y) = ((XD . n) . x) * ((XE . n) . y) by E3, E5, E1, Th26; :: thesis: verum

end;

end;

end;

end;

end;

HH2: (product-pre-Measure (M1,M2)) . (Union K) = (M1 . A) * (M2 . B)

proof

per cases ( ( A <> {} & B <> {} ) or A = {} or B = {} ) ;

suppose ( A <> {} & B <> {} ) ; :: thesis: (product-pre-Measure (M1,M2)) . (Union K) = (M1 . A) * (M2 . B)

then ( A = P & B = Q ) by A2, Q1, ZFMISC_1:110;
hence (product-pre-Measure (M1,M2)) . (Union K) = (M1 . A) * (M2 . B) by Q1; :: thesis: verum

end;

suppose HA: ( A = {} or B = {} ) ; :: thesis: (product-pre-Measure (M1,M2)) . (Union K) = (M1 . A) * (M2 . B)

then ( P = {} or Q = {} ) by A2, Q1;
then ( ( M1 . A = 0 or M2 . B = 0 ) & ( M1 . P = 0 or M2 . Q = 0 ) ) by HA, VALUED_0:def 19;
hence (product-pre-Measure (M1,M2)) . (Union K) = (M1 . A) * (M2 . B) by Q1; :: thesis: verum

end;

end;

end;

T1: rng (chi ([:A,B:],[:X1,X2:])) c= ExtREAL ;
dom (chi ([:A,B:],[:X1,X2:])) = [:X1,X2:] by FUNCT_3:def 3;
then reconsider CAB = chi ([:A,B:],[:X1,X2:]) as Function of [:X1,X2:],ExtREAL by T1, FUNCT_2:2;
QQ: for x being Element of X1 holds (M2 . B) * ((chi (A,X1)) . x) = Integral (M2,(ProjMap1 (CAB,x)))

proof

let x be Element of X1; :: thesis: (M2 . B) * ((chi (A,X1)) . x) = Integral (M2,(ProjMap1 (CAB,x)))
QQ1: for y being Element of X2 holds (ProjMap1 (CAB,x)) . y = ((chi (A,X1)) . x) * ((chi (B,X2)) . y)

proof

let y be Element of X2; :: thesis: (ProjMap1 (CAB,x)) . y = ((chi (A,X1)) . x) * ((chi (B,X2)) . y)
(ProjMap1 (CAB,x)) . y = (chi ((Union K),[:X1,X2:])) . (x,y) by A2, MESFUNC9:def 6;
hence (ProjMap1 (CAB,x)) . y = ((chi (A,X1)) . x) * ((chi (B,X2)) . y) by A2, Th26; :: thesis: verum

end;

per cases ( x in A or not x in A ) ;

suppose x in A ; :: thesis: (M2 . B) * ((chi (A,X1)) . x) = Integral (M2,(ProjMap1 (CAB,x)))

then QQ2: (chi (A,X1)) . x = 1 by FUNCT_3:def 3;
then QQ4: (M2 . B) * ((chi (A,X1)) . x) = M2 . B by XXREAL_3:81;
QQ3: dom (ProjMap1 (CAB,x)) = X2 by FUNCT_2:def 1
.= dom (chi (B,X2)) by FUNCT_3:def 3 ;
for y being Element of X2 st y in dom (ProjMap1 (CAB,x)) holds
(ProjMap1 (CAB,x)) . y = (chi (B,X2)) . y

proof

let y be Element of X2; :: thesis: ( y in dom (ProjMap1 (CAB,x)) implies (ProjMap1 (CAB,x)) . y = (chi (B,X2)) . y )
assume y in dom (ProjMap1 (CAB,x)) ; :: thesis: (ProjMap1 (CAB,x)) . y = (chi (B,X2)) . y
(ProjMap1 (CAB,x)) . y = ((chi (A,X1)) . x) * ((chi (B,X2)) . y) by QQ1;
hence (ProjMap1 (CAB,x)) . y = (chi (B,X2)) . y by QQ2, XXREAL_3:81; :: thesis: verum

end;

then ProjMap1 (CAB,x) = chi (B,X2) by QQ3, PARTFUN1:5;
hence (M2 . B) * ((chi (A,X1)) . x) = Integral (M2,(ProjMap1 (CAB,x))) by QQ4, MESFUNC9:14; :: thesis: verum

end;

suppose not x in A ; :: thesis: (M2 . B) * ((chi (A,X1)) . x) = Integral (M2,(ProjMap1 (CAB,x)))

then QQ5: (chi (A,X1)) . x = 0 by FUNCT_3:def 3;
then QQ9: (M2 . B) * ((chi (A,X1)) . x) = 0 ;
QQ8: {} is Element of S2 by PROB_1:4;
QQ6: dom (ProjMap1 (CAB,x)) = X2 by FUNCT_2:def 1
.= dom (chi ({},X2)) by FUNCT_3:def 3 ;
for y being Element of X2 st y in dom (ProjMap1 (CAB,x)) holds
(ProjMap1 (CAB,x)) . y = (chi ({},X2)) . y

proof

let y be Element of X2; :: thesis: ( y in dom (ProjMap1 (CAB,x)) implies (ProjMap1 (CAB,x)) . y = (chi ({},X2)) . y )
assume y in dom (ProjMap1 (CAB,x)) ; :: thesis: (ProjMap1 (CAB,x)) . y = (chi ({},X2)) . y
(ProjMap1 (CAB,x)) . y = ((chi (A,X1)) . x) * ((chi (B,X2)) . y) by QQ1;
then (ProjMap1 (CAB,x)) . y = 0 by QQ5;
hence (ProjMap1 (CAB,x)) . y = (chi ({},X2)) . y by FUNCT_3:def 3; :: thesis: verum

end;

then ProjMap1 (CAB,x) = chi ({},X2) by QQ6, PARTFUN1:5;
then Integral (M2,(ProjMap1 (CAB,x))) = M2 . {} by QQ8, MESFUNC9:14;
hence (M2 . B) * ((chi (A,X1)) . x) = Integral (M2,(ProjMap1 (CAB,x))) by QQ9, VALUED_0:def 19; :: thesis: verum

end;

end;

end;

RB1: dom XD = NAT by FUNCT_2:def 1;
for n being object st n in NAT holds
XD . n in Funcs (X1,REAL)

proof

let n be object ; :: thesis: ( n in NAT implies XD . n in Funcs (X1,REAL) )
assume n in NAT ; :: thesis: XD . n in Funcs (X1,REAL)
then reconsider n1 = n as Element of NAT ;
RB2: XD . n = chi ((D . n1),X1) by B5;
then RB3: dom (XD . n) = X1 by FUNCT_3:def 3;
( rng (XD . n) c= {0,1} & {0,1} c= REAL ) by RB2, FUNCT_3:39, XREAL_0:def 1;
then rng (XD . n) c= REAL ;
hence XD . n in Funcs (X1,REAL) by RB3, FUNCT_2:def 2; :: thesis: verum

end;

then reconsider RXD = XD as sequence of (Funcs (X1,REAL)) by RB1, FUNCT_2:3;
Y3: for n being Nat holds
( D . n c= A & E . n c= B )

proof

let n be Nat; :: thesis: ( D . n c= A & E . n c= B )
n is Element of NAT by ORDINAL1:def 12;
then YY1: ( D . n = proj1 (K . n) & E . n = proj2 (K . n) ) by B4, C4;
( proj1 (K . n) c= proj1 (Union K) & proj1 (Union K) c= A & proj2 (K . n) c= proj2 (Union K) & proj2 (Union K) c= B ) by A2, XTUPLE_0:8, XTUPLE_0:9, FUNCT_5:10, ABCMIZ_1:1;
hence ( D . n c= A & E . n c= B ) by YY1; :: thesis: verum

end;

Z1: for x being Element of X1 ex XF being Functional_Sequence of X2,ExtREAL ex I being ExtREAL_sequence st
( ( for n being Nat holds XF . n = ((RXD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds I . n = (M2 . (E . n)) * ((chi ((D . n),X1)) . x) ) & I is summable & Integral (M2,(lim (Partial_Sums XF))) = Sum I )

proof

let x be Element of X1; :: thesis: ex XF being Functional_Sequence of X2,ExtREAL ex I being ExtREAL_sequence st
( ( for n being Nat holds XF . n = ((RXD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds I . n = (M2 . (E . n)) * ((chi ((D . n),X1)) . x) ) & I is summable & Integral (M2,(lim (Partial_Sums XF))) = Sum I )
deffunc H₄( Nat) -> Element of bool [:X2,ExtREAL:] = ((RXD . $1) . x) (#) (chi ((E . $1),X2));
defpred S₃[ Nat, object ] means $2 = H₄($1);
W1: for n being Element of NAT ex y being Element of PFuncs (X2,ExtREAL) st S₃[n,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of PFuncs (X2,ExtREAL) st S₃[n,y]
reconsider r = (RXD . n) . x as Real ;
reconsider y = H₄(n) as Element of PFuncs (X2,ExtREAL) by PARTFUN1:45;
take y ; :: thesis: S₃[n,y]
thus S₃[n,y] ; :: thesis: verum

end;

consider XF being Function of NAT,(PFuncs (X2,ExtREAL)) such that
W2: for n being Element of NAT holds S₃[n,XF . n] from FUNCT_2:sch 3(W1);
reconsider XF = XF as Functional_Sequence of X2,ExtREAL ;
Y2: for n being Nat holds XF . n = ((RXD . n) . x) (#) (chi ((E . n),X2))

proof

let n be Nat; :: thesis: XF . n = ((RXD . n) . x) (#) (chi ((E . n),X2))
n is Element of NAT by ORDINAL1:def 12;
hence XF . n = ((RXD . n) . x) (#) (chi ((E . n),X2)) by W2; :: thesis: verum

end;

consider I being ExtREAL_sequence such that
Y4: ( ( for n being Nat holds I . n = (M2 . (E . n)) * ((chi ((D . n),X1)) . x) ) & I is summable & Integral (M2,(lim (Partial_Sums XF))) = Sum I ) by B5, Y2, Y3, Th30;
thus ex XF being Functional_Sequence of X2,ExtREAL ex I being ExtREAL_sequence st
( ( for n being Nat holds XF . n = ((RXD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds I . n = (M2 . (E . n)) * ((chi ((D . n),X1)) . x) ) & I is summable & Integral (M2,(lim (Partial_Sums XF))) = Sum I ) by Y2, Y4; :: thesis: verum

end;

dom (lim (Partial_Sums XK)) = dom ((Partial_Sums XK) . 0) by MESFUNC8:def 9;
then dom (lim (Partial_Sums XK)) = dom (XK . 0) by MESFUNC9:def 4;
then dom (lim (Partial_Sums XK)) = dom (chi ((K . 0),[:X1,X2:])) by A3;
then QR0: dom (lim (Partial_Sums XK)) = [:X1,X2:] by FUNCT_3:def 3;
then reconsider LPSXK = lim (Partial_Sums XK) as Function of [:X1,X2:],ExtREAL by FUNCT_2:67;
QR: for x being Element of X1
for y being Element of X2 holds (ProjMap1 (CAB,x)) . y = (ProjMap1 (LPSXK,x)) . y

proof

let x be Element of X1; :: thesis: for y being Element of X2 holds (ProjMap1 (CAB,x)) . y = (ProjMap1 (LPSXK,x)) . y
let y be Element of X2; :: thesis: (ProjMap1 (CAB,x)) . y = (ProjMap1 (LPSXK,x)) . y
QR1: [x,y] in [:X1,X2:] by ZFMISC_1:def 2;
(ProjMap1 (CAB,x)) . y = (chi ([:A,B:],[:X1,X2:])) . (x,y) by MESFUNC9:def 6
.= LPSXK . (x,y) by A3, Th25, QR1, A2 ;
hence (ProjMap1 (CAB,x)) . y = (ProjMap1 (LPSXK,x)) . y by MESFUNC9:def 6; :: thesis: verum

end;

QS: for x being Element of X1 holds ProjMap1 (CAB,x) = ProjMap1 (LPSXK,x)

proof

let x be Element of X1; :: thesis: ProjMap1 (CAB,x) = ProjMap1 (LPSXK,x)
for y being Element of X2 holds (ProjMap1 (CAB,x)) . y = (ProjMap1 (LPSXK,x)) . y by QR;
hence ProjMap1 (CAB,x) = ProjMap1 (LPSXK,x) by FUNCT_2:def 8; :: thesis: verum

end;

QT: for x being Element of X1 holds (M2 . B) * ((chi (A,X1)) . x) = Integral (M2,(ProjMap1 (LPSXK,x)))

proof

let x be Element of X1; :: thesis: (M2 . B) * ((chi (A,X1)) . x) = Integral (M2,(ProjMap1 (LPSXK,x)))
ProjMap1 (CAB,x) = ProjMap1 (LPSXK,x) by QS;
hence (M2 . B) * ((chi (A,X1)) . x) = Integral (M2,(ProjMap1 (LPSXK,x))) by QQ; :: thesis: verum

end;

ZZ: for x being Element of X1 ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = (M2 . (E . n)) * ((chi ((D . n),X1)) . x) ) & (M2 . B) * ((chi (A,X1)) . x) = Sum I )

proof

let x be Element of X1; :: thesis: ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = (M2 . (E . n)) * ((chi ((D . n),X1)) . x) ) & (M2 . B) * ((chi (A,X1)) . x) = Sum I )
consider XF being Functional_Sequence of X2,ExtREAL, I being ExtREAL_sequence such that
Z3: ( ( for n being Nat holds XF . n = ((RXD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds I . n = (M2 . (E . n)) * ((chi ((D . n),X1)) . x) ) & I is summable & Integral (M2,(lim (Partial_Sums XF))) = Sum I ) by Z1;
dom (lim (Partial_Sums XF)) = dom ((Partial_Sums XF) . 0) by MESFUNC8:def 9;
then Z31: dom (lim (Partial_Sums XF)) = dom (XF . 0) by MESFUNC9:def 4;
then dom (lim (Partial_Sums XF)) = dom (((RXD . 0) . x) (#) (chi ((E . 0),X2))) by Z3;
then dom (lim (Partial_Sums XF)) = dom (chi ((E . 0),X2)) by MESFUNC1:def 6;
then Z4A: dom (lim (Partial_Sums XF)) = X2 by FUNCT_3:def 3;
then Z4: dom (ProjMap1 (LPSXK,x)) = dom (lim (Partial_Sums XF)) by FUNCT_2:def 1;

now :: thesis: for y being Element of X2 st y in dom (ProjMap1 (LPSXK,x)) holds
(ProjMap1 (LPSXK,x)) . y = (lim (Partial_Sums XF)) . y

let y be Element of X2; :: thesis: ( y in dom (ProjMap1 (LPSXK,x)) implies (ProjMap1 (LPSXK,x)) . y = (lim (Partial_Sums XF)) . y )
assume Z41: y in dom (ProjMap1 (LPSXK,x)) ; :: thesis: (ProjMap1 (LPSXK,x)) . y = (lim (Partial_Sums XF)) . y
Z42: (ProjMap1 (LPSXK,x)) . y = LPSXK . (x,y) by MESFUNC9:def 6;
reconsider z = [x,y] as Element of [:X1,X2:] by ZFMISC_1:def 2;
Z46: for n being Nat holds dom (XK . n) = [:X1,X2:]

proof

let n be Nat; :: thesis: dom (XK . n) = [:X1,X2:]
XK . n = chi ((K . n),[:X1,X2:]) by A3;
hence dom (XK . n) = [:X1,X2:] by FUNCT_3:def 3; :: thesis: verum

end;

Z49: for n being Nat holds XK . n is nonnegative

proof

let n be Nat; :: thesis: XK . n is nonnegative
for z being object holds 0 <= (XK . n) . z

proof

let z be object ; :: thesis: 0 <= (XK . n) . z
Z45: XK . n = chi ((K . n),[:X1,X2:]) by A3;
Z44: dom (XK . n) = [:X1,X2:] by Z46;

per cases ( not z in [:X1,X2:] or ( z in [:X1,X2:] & z in K . n ) or ( z in [:X1,X2:] & not z in K . n ) ) ;

suppose not z in [:X1,X2:] ; :: thesis: 0 <= (XK . n) . z

hence (XK . n) . z >= 0 by Z44, FUNCT_1:def 2; :: thesis: verum

end;

suppose ( z in [:X1,X2:] & z in K . n ) ; :: thesis: 0 <= (XK . n) . z

hence (XK . n) . z >= 0 by Z45, FUNCT_3:def 3; :: thesis: verum

end;

suppose ( z in [:X1,X2:] & not z in K . n ) ; :: thesis: 0 <= (XK . n) . z

hence (XK . n) . z >= 0 by Z45, FUNCT_3:def 3; :: thesis: verum

end;

end;

end;

hence XK . n is nonnegative by SUPINF_2:51; :: thesis: verum

end;

for n, m being Nat holds dom (XK . n) = dom (XK . m)

proof

let n, m be Nat; :: thesis: dom (XK . n) = dom (XK . m)
dom (XK . n) = [:X1,X2:] by Z46;
hence dom (XK . n) = dom (XK . m) by Z46; :: thesis: verum

end;

then Z48: XK is with_the_same_dom by MESFUNC8:def 2;
ZZ1: dom (XK . 0) = [:X1,X2:] by Z46;
then ZP1: (Partial_Sums XK) # z is convergent by Z49, Z48, MESFUNC9:38;
Z50: for n being Nat holds dom (XF . n) = X2

proof

let n be Nat; :: thesis: dom (XF . n) = X2
XF . n = ((RXD . n) . x) (#) (chi ((E . n),X2)) by Z3;
then dom (XF . n) = dom (chi ((E . n),X2)) by MESFUNC1:def 6;
hence dom (XF . n) = X2 by FUNCT_3:def 3; :: thesis: verum

end;

ZZ5: for n, m being Nat holds dom (XF . n) = dom (XF . m)

proof

let n, m be Nat; :: thesis: dom (XF . n) = dom (XF . m)
dom (XF . n) = X2 by Z50;
hence dom (XF . n) = dom (XF . m) by Z50; :: thesis: verum

end;

then Z51: XF is with_the_same_dom by MESFUNC8:def 2;
ZX1: for n being Nat holds XF . n is nonnegative

proof

let n be Nat; :: thesis: XF . n is nonnegative
for y being object holds 0 <= (XF . n) . y

proof

let y be object ; :: thesis: 0 <= (XF . n) . y
Z53: XF . n = ((RXD . n) . x) (#) (chi ((E . n),X2)) by Z3;
Z54: dom (XF . n) = X2 by Z50;

per cases ( not y in X2 or ( y in X2 & y in E . n ) or ( y in X2 & not y in E . n ) ) ;

suppose not y in X2 ; :: thesis: 0 <= (XF . n) . y

hence (XF . n) . y >= 0 by Z54, FUNCT_1:def 2; :: thesis: verum

end;

suppose Z55: ( y in X2 & y in E . n ) ; :: thesis: 0 <= (XF . n) . y

then reconsider y1 = y as Element of X2 ;
Z56: (XF . n) . y = ((RXD . n) . x) * ((chi ((E . n),X2)) . y1) by Z53, Z54, MESFUNC1:def 6;
(chi ((E . n),X2)) . y1 = 1 by Z55, FUNCT_3:def 3;
then (XF . n) . y = (RXD . n) . x by Z56, XXREAL_3:81;
then (XF . n) . y = (chi ((D . n),X1)) . x by B5;
hence (XF . n) . y >= 0 by SUPINF_2:51; :: thesis: verum

end;

suppose Z57: ( y in X2 & not y in E . n ) ; :: thesis: 0 <= (XF . n) . y

then reconsider y1 = y as Element of X2 ;
Z58: (XF . n) . y = ((RXD . n) . x) * ((chi ((E . n),X2)) . y1) by Z53, Z54, MESFUNC1:def 6;
(chi ((E . n),X2)) . y1 = 0 by Z57, FUNCT_3:def 3;
hence (XF . n) . y >= 0 by Z58; :: thesis: verum

end;

end;

end;

hence XF . n is nonnegative by SUPINF_2:51; :: thesis: verum

end;

then ZP2: (Partial_Sums XF) # y is convergent by Z51, Z31, Z4A, MESFUNC9:38;
X20: for n being Nat holds ((Partial_Sums XK) # z) . n = ((Partial_Sums XF) # y) . n

proof

let n be Nat; :: thesis: ((Partial_Sums XK) # z) . n = ((Partial_Sums XF) # y) . n
X17: ( ((Partial_Sums XK) # z) . n = ((Partial_Sums XK) . n) . z & ((Partial_Sums XF) # y) . n = ((Partial_Sums XF) . n) . y ) by MESFUNC5:def 13;
defpred S₃[ Nat] means ((Partial_Sums XK) . $1) . z = ((Partial_Sums XF) . $1) . y;
((Partial_Sums XK) . 0) . z = (XK . 0) . (x,y) by MESFUNC9:def 4;
then X14: ((Partial_Sums XK) . 0) . z = ((XD . 0) . x) * ((XE . 0) . y) by E0;
X13: y in dom (((RXD . 0) . x) (#) (chi ((E . 0),X2))) by Z3, Z31, Z4, Z41;
(Partial_Sums XF) . 0 = XF . 0 by MESFUNC9:def 4;
then ((Partial_Sums XF) . 0) . y = (((RXD . 0) . x) (#) (chi ((E . 0),X2))) . y by Z3;
then ((Partial_Sums XF) . 0) . y = ((XD . 0) . x) * ((chi ((E . 0),X2)) . y) by X13, MESFUNC1:def 6;
then X15: S₃[ 0 ] by C5, X14;
X16: for n being Nat st S₃[n] holds
S₃[n + 1]

proof

let n be Nat; :: thesis: ( S₃[n] implies S₃[n + 1] )
assume X18: S₃[n] ; :: thesis: S₃[n + 1]
X30: dom ((Partial_Sums XK) . (n + 1)) = dom (XK . 0) by Z49, Z48, MESFUNC9:29, MESFUNC9:30;
(Partial_Sums XK) . (n + 1) = ((Partial_Sums XK) . n) + (XK . (n + 1)) by MESFUNC9:def 4;
then X31: ((Partial_Sums XK) . (n + 1)) . z = (((Partial_Sums XK) . n) . z) + ((XK . (n + 1)) . z) by ZZ1, X30, MESFUNC1:def 3;
X32: dom ((Partial_Sums XF) . (n + 1)) = dom (XF . 0) by Z51, ZX1, MESFUNC9:30, MESFUNC9:29;
(Partial_Sums XF) . (n + 1) = ((Partial_Sums XF) . n) + (XF . (n + 1)) by MESFUNC9:def 4;
then X33: ((Partial_Sums XF) . (n + 1)) . y = (((Partial_Sums XF) . n) . y) + ((XF . (n + 1)) . y) by Z31, Z4A, X32, MESFUNC1:def 3;
(XK . (n + 1)) . z = (XK . (n + 1)) . (x,y) ;
then X35: (XK . (n + 1)) . z = ((XD . (n + 1)) . x) * ((XE . (n + 1)) . y) by E0;
dom (XF . (n + 1)) = dom (XF . 0) by ZZ5;
then X34: y in dom (((RXD . (n + 1)) . x) (#) (chi ((E . (n + 1)),X2))) by Z3, Z31, Z4, Z41;
(XF . (n + 1)) . y = (((RXD . (n + 1)) . x) (#) (chi ((E . (n + 1)),X2))) . y by Z3;
then (XF . (n + 1)) . y = ((RXD . (n + 1)) . x) * ((chi ((E . (n + 1)),X2)) . y) by X34, MESFUNC1:def 6;
hence S₃[n + 1] by C5, X35, X33, X31, X18; :: thesis: verum

end;

for n being Nat holds S₃[n] from NAT_1:sch 2(X15, X16);
hence ((Partial_Sums XK) # z) . n = ((Partial_Sums XF) # y) . n by X17; :: thesis: verum

end;

for n being Nat holds ((Partial_Sums XK) # z) . n <= ((Partial_Sums XF) # y) . n by X20;
then ZP3: lim ((Partial_Sums XK) # z) <= lim ((Partial_Sums XF) # y) by ZP1, ZP2, RINFSUP2:38;
for n being Nat holds ((Partial_Sums XF) # y) . n <= ((Partial_Sums XK) # z) . n by X20;
then lim ((Partial_Sums XF) # y) <= lim ((Partial_Sums XK) # z) by ZP1, ZP2, RINFSUP2:38;
then lim ((Partial_Sums XK) # z) = lim ((Partial_Sums XF) # y) by ZP3, XXREAL_0:1;
then (lim (Partial_Sums XK)) . z = lim ((Partial_Sums XF) # y) by QR0, MESFUNC8:def 9;
hence (ProjMap1 (LPSXK,x)) . y = (lim (Partial_Sums XF)) . y by Z42, Z4A, MESFUNC8:def 9; :: thesis: verum

end;

then ProjMap1 (LPSXK,x) = lim (Partial_Sums XF) by Z4, PARTFUN1:5;
hence ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = (M2 . (E . n)) * ((chi ((D . n),X1)) . x) ) & (M2 . B) * ((chi (A,X1)) . x) = Sum I ) by Z3, QT; :: thesis: verum

end;

defpred S₃[ Nat, object ] means ( ( M2 . (E . $1) = +infty implies $2 = Xchi ((D . $1),X1) ) & ( M2 . (E . $1) <> +infty implies ex m2 being Real st
( m2 = M2 . (E . $1) & $2 = m2 (#) (chi ((D . $1),X1)) ) ) );
H1: for n being Element of NAT ex y being Element of PFuncs (X1,ExtREAL) st S₃[n,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of PFuncs (X1,ExtREAL) st S₃[n,y]

per cases ( M2 . (E . n) = +infty or M2 . (E . n) <> +infty ) ;

suppose HA1: M2 . (E . n) = +infty ; :: thesis: ex y being Element of PFuncs (X1,ExtREAL) st S₃[n,y]

set y = Xchi ((D . n),X1);
reconsider y = Xchi ((D . n),X1) as Element of PFuncs (X1,ExtREAL) by PARTFUN1:45;
S₃[n,y] by HA1;
hence ex y being Element of PFuncs (X1,ExtREAL) st S₃[n,y] ; :: thesis: verum

end;

suppose HA2: M2 . (E . n) <> +infty ; :: thesis: ex y being Element of PFuncs (X1,ExtREAL) st S₃[n,y]

M2 . (E . n) >= 0 by SUPINF_2:51;
then M2 . (E . n) in REAL by HA2, XXREAL_0:14;
then reconsider m2 = M2 . (E . n) as Real ;
set y = m2 (#) (chi ((D . n),X1));
reconsider y = m2 (#) (chi ((D . n),X1)) as Element of PFuncs (X1,ExtREAL) by PARTFUN1:45;
S₃[n,y] ;
hence ex y being Element of PFuncs (X1,ExtREAL) st S₃[n,y] ; :: thesis: verum

end;

end;

end;

consider FI being Function of NAT,(PFuncs (X1,ExtREAL)) such that
H2: for n being Element of NAT holds S₃[n,FI . n] from FUNCT_2:sch 3(H1);
H3: for n being Nat holds dom (FI . n) = X1

proof

let n be Nat; :: thesis: dom (FI . n) = X1
HA3: n is Element of NAT by ORDINAL1:def 12;

per cases ( M2 . (E . n) = +infty or M2 . (E . n) <> +infty ) ;

suppose M2 . (E . n) = +infty ; :: thesis: dom (FI . n) = X1

then FI . n = Xchi ((D . n),X1) by H2, HA3;
hence dom (FI . n) = X1 by FUNCT_2:def 1; :: thesis: verum

end;

suppose M2 . (E . n) <> +infty ; :: thesis: dom (FI . n) = X1

then consider m2 being Real such that
HA4: ( m2 = M2 . (E . n) & FI . n = m2 (#) (chi ((D . n),X1)) ) by H2, HA3;
dom (FI . n) = dom (chi ((D . n),X1)) by HA4, MESFUNC1:def 6;
hence dom (FI . n) = X1 by FUNCT_3:def 3; :: thesis: verum

end;

end;

end;

F1: A c= dom (FI . 0) by H3, A10;
F2A: for n being Nat holds FI . n is nonnegative

proof

let n be Nat; :: thesis: FI . n is nonnegative
HA5: n is Element of NAT by ORDINAL1:def 12;

per cases ( M2 . (E . n) = +infty or M2 . (E . n) <> +infty ) ;

suppose M2 . (E . n) = +infty ; :: thesis: FI . n is nonnegative

then FI . n = Xchi ((D . n),X1) by H2, HA5;
hence FI . n is nonnegative ; :: thesis: verum

end;

suppose M2 . (E . n) <> +infty ; :: thesis: FI . n is nonnegative

then consider m2 being Real such that
HA6: ( m2 = M2 . (E . n) & FI . n = m2 (#) (chi ((D . n),X1)) ) by H2, HA5;
for x being object holds (FI . n) . x >= 0

proof

let x be object ; :: thesis: (FI . n) . x >= 0

per cases ( x in X1 or not x in X1 ) ;

suppose HA7: x in X1 ; :: thesis: (FI . n) . x >= 0

then reconsider x1 = x as Element of X1 ;
x1 in dom (chi ((D . n),X1)) by HA7, FUNCT_3:def 3;
then x1 in dom (FI . n) by HA6, MESFUNC1:def 6;
then HA8: (FI . n) . x = m2 * ((chi ((D . n),X1)) . x1) by HA6, MESFUNC1:def 6;
( m2 >= 0 & (chi ((D . n),X1)) . x1 >= 0 ) by HA6, SUPINF_2:51;
hence (FI . n) . x >= 0 by HA8; :: thesis: verum

end;

suppose not x in X1 ; :: thesis: (FI . n) . x >= 0

then not x in dom (FI . n) ;
hence (FI . n) . x >= 0 by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence FI . n is nonnegative by SUPINF_2:51; :: thesis: verum

end;

end;

end;

for n, m being Nat holds dom (FI . n) = dom (FI . m)

proof

let n, m be Nat; :: thesis: dom (FI . n) = dom (FI . m)
( dom (FI . n) = X1 & dom (FI . m) = X1 ) by H3;
hence dom (FI . n) = dom (FI . m) ; :: thesis: verum

end;

then F3: FI is with_the_same_dom by MESFUNC8:def 2;
reconsider XX = X1 as Element of S1 by MEASURE1:7;
F4: for n being Nat holds
( FI . n is nonnegative & FI . n is A -measurable & FI . n is XX -measurable )

proof

let n be Nat; :: thesis: ( FI . n is nonnegative & FI . n is A -measurable & FI . n is XX -measurable )
F4A: n is Element of NAT by ORDINAL1:def 12;
thus FI . n is nonnegative by F2A; :: thesis: ( FI . n is A -measurable & FI . n is XX -measurable )

per cases ( M2 . (E . n) = +infty or M2 . (E . n) <> +infty ) ;

suppose M2 . (E . n) = +infty ; :: thesis: ( FI . n is A -measurable & FI . n is XX -measurable )

then FI . n = Xchi ((D . n),X1) by H2, F4A;
hence ( FI . n is A -measurable & FI . n is XX -measurable ) by Th32; :: thesis: verum

end;

suppose M2 . (E . n) <> +infty ; :: thesis: ( FI . n is A -measurable & FI . n is XX -measurable )

then consider m2 being Real such that
F4B: ( m2 = M2 . (E . n) & FI . n = m2 (#) (chi ((D . n),X1)) ) by H2, F4A;
dom (chi ((D . n),X1)) = X1 by FUNCT_3:def 3;
hence ( FI . n is A -measurable & FI . n is XX -measurable ) by F4B, MESFUNC2:29, MESFUNC1:37; :: thesis: verum

end;

end;

end;

F5: for x being Element of X1 st x in A holds
FI # x is summable

proof

let x be Element of X1; :: thesis: ( x in A implies FI # x is summable )
assume x in A ; :: thesis: FI # x is summable
for n being Element of NAT holds (FI # x) . n >= 0

proof

let n be Element of NAT ; :: thesis: (FI # x) . n >= 0
(FI # x) . n = (FI . n) . x by MESFUNC5:def 13;
hence (FI # x) . n >= 0 by F4, SUPINF_2:51; :: thesis: verum

end;

then FI # x is nonnegative by SUPINF_2:39;
hence FI # x is summable by MEASURE8:2; :: thesis: verum

end;

consider J being ExtREAL_sequence such that
F6: ( ( for n being Nat holds J . n = Integral (M1,((FI . n) | A)) ) & J is summable & Integral (M1,((lim (Partial_Sums FI)) | A)) = Sum J ) by F1, F3, F4, F5, MESFUNC9:30, MESFUNC9:51;
G1: for n being Nat holds J . n = Integral (M1,(FI . n))

proof

let n be Nat; :: thesis: J . n = Integral (M1,(FI . n))
F4A: n is Element of NAT by ORDINAL1:def 12;
FF: XX = dom (FI . n) by H3;
T1: ex E being Element of S1 st
( E = dom (FI . n) & FI . n is E -measurable )

proof

take XX ; :: thesis: ( XX = dom (FI . n) & FI . n is XX -measurable )
thus ( XX = dom (FI . n) & FI . n is XX -measurable ) by FF, F4; :: thesis: verum

end;

for x being object st x in (dom (FI . n)) \ A holds
(FI . n) . x = 0

proof

let x be object ; :: thesis: ( x in (dom (FI . n)) \ A implies (FI . n) . x = 0 )
assume T3: x in (dom (FI . n)) \ A ; :: thesis: (FI . n) . x = 0
then T3A: ( x in dom (FI . n) & not x in A ) by XBOOLE_0:def 5;
D . n c= A by Y3;
then T6: not x in D . n by T3, XBOOLE_0:def 5;

per cases ( M2 . (E . n) = +infty or M2 . (E . n) <> +infty ) ;

suppose M2 . (E . n) = +infty ; :: thesis: (FI . n) . x = 0

then FI . n = Xchi ((D . n),X1) by H2, F4A;
hence (FI . n) . x = 0 by T6, T3, DefXchi; :: thesis: verum

end;

suppose M2 . (E . n) <> +infty ; :: thesis: (FI . n) . x = 0

then consider m2 being Real such that
F4B: ( m2 = M2 . (E . n) & FI . n = m2 (#) (chi ((D . n),X1)) ) by H2, F4A;
T5: (FI . n) . x = m2 * ((chi ((D . n),X1)) . x) by F4B, T3A, MESFUNC1:def 6;
(chi ((D . n),X1)) . x = 0 by T3, T6, FUNCT_3:def 3;
hence (FI . n) . x = 0 by T5; :: thesis: verum

end;

end;

end;

then Integral (M1,(FI . n)) = Integral (M1,((FI . n) | A)) by F4, T1, Th28;
hence J . n = Integral (M1,(FI . n)) by F6; :: thesis: verum

end;

reconsider XX = X1 as Element of S1 by MEASURE1:7;
for n being Element of NAT holds J . n = ((product-pre-Measure (M1,M2)) * K) . n

proof

let n be Element of NAT ; :: thesis: J . n = ((product-pre-Measure (M1,M2)) * K) . n
Integral (M1,(FI . n)) = (M2 . (E . n)) * (M1 . (D . n))

proof

M2: XX = dom (FI . n) by H3;
M3b: FI . n is nonnegative by F4;

per cases ( M2 . (E . n) = +infty or M2 . (E . n) <> +infty ) ;

suppose M0: M2 . (E . n) = +infty ; :: thesis: Integral (M1,(FI . n)) = (M2 . (E . n)) * (M1 . (D . n))

then M1: FI . n = Xchi ((D . n),X1) by H2;

per cases ( M1 . (D . n) = 0 or M1 . (D . n) <> 0 ) ;

suppose M5: M1 . (D . n) = 0 ; :: thesis: Integral (M1,(FI . n)) = (M2 . (E . n)) * (M1 . (D . n))

then Integral (M1,(FI . n)) = 0 by M1, Th34;
hence Integral (M1,(FI . n)) = (M2 . (E . n)) * (M1 . (D . n)) by M5; :: thesis: verum

end;

suppose Q1: M1 . (D . n) <> 0 ; :: thesis: Integral (M1,(FI . n)) = (M2 . (E . n)) * (M1 . (D . n))

then M1 . (D . n) > 0 by SUPINF_2:51;
then (M2 . (E . n)) * (M1 . (D . n)) = +infty by M0, XXREAL_3:def 5;
hence Integral (M1,(FI . n)) = (M2 . (E . n)) * (M1 . (D . n)) by M1, Q1, Th34; :: thesis: verum

end;

end;

end;

suppose M2 . (E . n) <> +infty ; :: thesis: Integral (M1,(FI . n)) = (M2 . (E . n)) * (M1 . (D . n))

then consider m2 being Real such that
R2: ( m2 = M2 . (E . n) & FI . n = m2 (#) (chi ((D . n),X1)) ) by H2;
R3: m2 >= 0 by R2, SUPINF_2:51;
R4: XX = dom (chi ((D . n),X1)) by FUNCT_3:def 3;
R5: chi ((D . n),X1) is XX -measurable by MESFUNC2:29;
integral+ (M1,(m2 (#) (chi ((D . n),X1)))) = m2 * (integral+ (M1,(chi ((D . n),X1)))) by R4, MESFUNC2:29, R3, MESFUNC5:86;
then integral+ (M1,(m2 (#) (chi ((D . n),X1)))) = m2 * (Integral (M1,(chi ((D . n),X1)))) by R4, MESFUNC2:29, MESFUNC5:88;
then integral+ (M1,(m2 (#) (chi ((D . n),X1)))) = m2 * (M1 . (D . n)) by MESFUNC9:14;
hence Integral (M1,(FI . n)) = (M2 . (E . n)) * (M1 . (D . n)) by R2, M2, R4, R5, MESFUNC1:37, M3b, MESFUNC5:88; :: thesis: verum

end;

end;

end;

then Q9: J . n = (M2 . (E . n)) * (M1 . (D . n)) by G1;
Q17: dom K = NAT by FUNCT_2:def 1;
consider Dn being Element of S1, En being Element of S2 such that
Q10: ( K . n = [:Dn,En:] & (product-pre-Measure (M1,M2)) . (K . n) = (M1 . Dn) * (M2 . En) ) by Def6;
Q13: ( D . n = proj1 (K . n) & E . n = proj2 (K . n) ) by B4, C4;
(M1 . Dn) * (M2 . En) = (M1 . (D . n)) * (M2 . (E . n))

proof

per cases ( Dn = {} or En = {} or ( Dn <> {} & En <> {} ) ) ;

suppose Q14: ( Dn = {} or En = {} ) ; :: thesis: (M1 . Dn) * (M2 . En) = (M1 . (D . n)) * (M2 . (E . n))

then ( M1 . Dn = 0 or M2 . En = 0 ) by VALUED_0:def 19;
then Q15: (M1 . Dn) * (M2 . En) = 0 ;
( D . n = {} & E . n = {} ) by Q13, Q10, Q14;
then ( M1 . (D . n) = 0 & M2 . (E . n) = 0 ) by VALUED_0:def 19;
hence (M1 . Dn) * (M2 . En) = (M1 . (D . n)) * (M2 . (E . n)) by Q15; :: thesis: verum

end;

suppose ( Dn <> {} & En <> {} ) ; :: thesis: (M1 . Dn) * (M2 . En) = (M1 . (D . n)) * (M2 . (E . n))

then ( Dn = D . n & En = E . n ) by Q10, Q13, FUNCT_5:9;
hence (M1 . Dn) * (M2 . En) = (M1 . (D . n)) * (M2 . (E . n)) ; :: thesis: verum

end;

end;

end;

hence J . n = ((product-pre-Measure (M1,M2)) * K) . n by Q9, Q17, Q10, FUNCT_1:13; :: thesis: verum

end;

then F7: J = (product-pre-Measure (M1,M2)) * K by FUNCT_2:def 8;
V5: dom (lim (Partial_Sums FI)) = dom ((Partial_Sums FI) . 0) by MESFUNC8:def 9;
then V0: dom (lim (Partial_Sums FI)) = dom (FI . 0) by MESFUNC9:def 4;
then V1: XX = dom (lim (Partial_Sums FI)) by H3;
for x being Element of X1 holds (lim (Partial_Sums FI)) . x >= 0

proof

let x be Element of X1; :: thesis: (lim (Partial_Sums FI)) . x >= 0
(Partial_Sums FI) # x is non-decreasing by V0, V1, F3, F2A, MESFUNC9:38;
then lim ((Partial_Sums FI) # x) = sup ((Partial_Sums FI) # x) by RINFSUP2:37;
then ((Partial_Sums FI) # x) . 0 <= lim ((Partial_Sums FI) # x) by RINFSUP2:23;
then ((Partial_Sums FI) . 0) . x <= lim ((Partial_Sums FI) # x) by MESFUNC5:def 13;
then (FI . 0) . x <= lim ((Partial_Sums FI) # x) by MESFUNC9:def 4;
then 0 <= lim ((Partial_Sums FI) # x) by F2A, SUPINF_2:51;
hence 0 <= (lim (Partial_Sums FI)) . x by V1, MESFUNC8:def 9; :: thesis: verum

end;

then V4: lim (Partial_Sums FI) is nonnegative by SUPINF_2:39;
W4: Partial_Sums FI is with_the_same_dom by F2A, F3, MESFUNC9:30, MESFUNC9:43;
for n being Nat holds
( FI . n is XX -measurable & FI . n is without-infty )

proof

let n be Nat; :: thesis: ( FI . n is XX -measurable & FI . n is without-infty )
thus FI . n is XX -measurable by F4; :: thesis: FI . n is without-infty
FI . n is nonnegative by F4;
hence FI . n is without-infty ; :: thesis: verum

end;

then W1: for n being Nat holds (Partial_Sums FI) . n is XX -measurable by MESFUNC9:41;
V2: for x being Element of X1 st x in XX holds
(Partial_Sums FI) # x is convergent by V0, V1, F3, F2A, MESFUNC9:38;
V3: for x being object st x in (dom (lim (Partial_Sums FI))) \ A holds
(lim (Partial_Sums FI)) . x = 0

proof

let x be object ; :: thesis: ( x in (dom (lim (Partial_Sums FI))) \ A implies (lim (Partial_Sums FI)) . x = 0 )
assume VV1: x in (dom (lim (Partial_Sums FI))) \ A ; :: thesis: (lim (Partial_Sums FI)) . x = 0
then reconsider x1 = x as Element of X1 ;
for n being Nat holds ((Partial_Sums FI) # x1) . n = 0

proof

let n be Nat; :: thesis: ((Partial_Sums FI) # x1) . n = 0
VV4: x1 in X1 ;
then x1 in dom (FI . 0) by H3;
then VV7: ((Partial_Sums FI) # x1) . n = (Partial_Sums (FI # x1)) . n by F2A, F3, MESFUNC9:30, MESFUNC9:32;
VV8: for k being Nat holds (FI # x1) . k = 0

proof

let k be Nat; :: thesis: (FI # x1) . k = 0
F4A: k is Element of NAT by ORDINAL1:def 12;
D . k c= A by Y3;
then VV2: not x1 in D . k by VV1, XBOOLE_0:def 5;

per cases ( M2 . (E . k) = +infty or M2 . (E . k) <> +infty ) ;

suppose M2 . (E . k) = +infty ; :: thesis: (FI # x1) . k = 0

then FI . k = Xchi ((D . k),X1) by H2, F4A;
then (FI . k) . x1 = 0 by VV2, DefXchi;
hence (FI # x1) . k = 0 by MESFUNC5:def 13; :: thesis: verum

end;

suppose M2 . (E . k) <> +infty ; :: thesis: (FI # x1) . k = 0

then consider m2 being Real such that
VV3: ( m2 = M2 . (E . k) & FI . k = m2 (#) (chi ((D . k),X1)) ) by H2, F4A;
VV5: (chi ((D . k),X1)) . x1 = 0 by VV2, FUNCT_3:def 3;
x1 in dom (FI . k) by VV4, H3;
then (FI . k) . x1 = m2 * ((chi ((D . k),X1)) . x1) by VV3, MESFUNC1:def 6;
hence (FI # x1) . k = 0 by VV5, MESFUNC5:def 13; :: thesis: verum

end;

end;

end;

defpred S₄[ Nat] means (Partial_Sums (FI # x1)) . $1 = 0 ;
(Partial_Sums (FI # x1)) . 0 = (FI # x1) . 0 by MESFUNC9:def 1;
then VV9: S₄[ 0 ] by VV8;
VV10: for k being Nat st S₄[k] holds
S₄[k + 1]

proof

let k be Nat; :: thesis: ( S₄[k] implies S₄[k + 1] )
assume VV11: S₄[k] ; :: thesis: S₄[k + 1]
(Partial_Sums (FI # x1)) . (k + 1) = ((Partial_Sums (FI # x1)) . k) + ((FI # x1) . (k + 1)) by MESFUNC9:def 1
.= ((Partial_Sums (FI # x1)) . k) + 0 by VV8
.= (Partial_Sums (FI # x1)) . k by XXREAL_3:4 ;
hence S₄[k + 1] by VV11; :: thesis: verum

end;

for k being Nat holds S₄[k] from NAT_1:sch 2(VV9, VV10);
hence ((Partial_Sums FI) # x1) . n = 0 by VV7; :: thesis: verum

end;

then lim ((Partial_Sums FI) # x1) = 0 by MESFUNC5:52;
hence (lim (Partial_Sums FI)) . x = 0 by V1, MESFUNC8:def 9; :: thesis: verum

end;

F9: Integral (M1,(lim (Partial_Sums FI))) = Integral (M1,((lim (Partial_Sums FI)) | A)) by V1, V2, V3, V4, Th28, V5, W1, W4, MESFUNC8:25;
Integral (M1,(lim (Partial_Sums FI))) = (M1 . A) * (M2 . B)

proof

J1: lim (Partial_Sums FI) is Function of X1,ExtREAL by V1, FUNCT_2:def 1;

per cases ( M2 . B = +infty or M2 . B <> +infty ) ;

suppose I0: M2 . B = +infty ; :: thesis: Integral (M1,(lim (Partial_Sums FI))) = (M1 . A) * (M2 . B)

for x being Element of X1 holds (lim (Partial_Sums FI)) . x = (Xchi (A,X1)) . x

proof

let x be Element of X1; :: thesis: (lim (Partial_Sums FI)) . x = (Xchi (A,X1)) . x
JJ: x in X1 ;
J2: dom (FI . 0) = X1 by H3;
J4: (lim (Partial_Sums FI)) . x = lim ((Partial_Sums FI) # x) by V1, MESFUNC8:def 9;
consider I being ExtREAL_sequence such that
J5: for n being Nat holds
( I . n = (M2 . (E . n)) * ((chi ((D . n),X1)) . x) & (M2 . B) * ((chi (A,X1)) . x) = Sum I ) by ZZ;
J6: lim (Partial_Sums I) = (M2 . B) * ((chi (A,X1)) . x) by J5, MESFUNC9:def 3;
for n being Element of NAT holds (FI # x) . n = I . n

proof

let n be Element of NAT ; :: thesis: (FI # x) . n = I . n

per cases ( M2 . (E . n) = +infty or M2 . (E . n) <> +infty ) ;

suppose J8: M2 . (E . n) = +infty ; :: thesis: (FI # x) . n = I . n

then FI . n = Xchi ((D . n),X1) by H2;
then J9: (FI # x) . n = (Xchi ((D . n),X1)) . x by MESFUNC5:def 13;

per cases ( x in D . n or not x in D . n ) ;

suppose J10: x in D . n ; :: thesis: (FI # x) . n = I . n

then J11: (FI # x) . n = +infty by J9, DefXchi;
(chi ((D . n),X1)) . x = 1 by J10, FUNCT_3:def 3;
then (M2 . (E . n)) * ((chi ((D . n),X1)) . x) = +infty by J8, XXREAL_3:81;
hence (FI # x) . n = I . n by J5, J11; :: thesis: verum

end;

suppose J12: not x in D . n ; :: thesis: (FI # x) . n = I . n

then J13: (FI # x) . n = 0 by J9, DefXchi;
(chi ((D . n),X1)) . x = 0 by J12, FUNCT_3:def 3;
then (M2 . (E . n)) * ((chi ((D . n),X1)) . x) = 0 ;
hence (FI # x) . n = I . n by J5, J13; :: thesis: verum

end;

end;

end;

suppose M2 . (E . n) <> +infty ; :: thesis: (FI # x) . n = I . n

then consider m2 being Real such that
J15: ( m2 = M2 . (E . n) & FI . n = m2 (#) (chi ((D . n),X1)) ) by H2;
x in dom (FI . n) by JJ, H3;
then (FI . n) . x = m2 * ((chi ((D . n),X1)) . x) by J15, MESFUNC1:def 6;
then (FI # x) . n = m2 * ((chi ((D . n),X1)) . x) by MESFUNC5:def 13;
hence (FI # x) . n = I . n by J15, J5; :: thesis: verum

end;

end;

end;

then FI # x = I by FUNCT_2:63;
then J17: for n being Element of NAT holds ((Partial_Sums FI) # x) . n = (Partial_Sums I) . n by F2A, F3, J2, MESFUNC9:30, MESFUNC9:32;
(Xchi (A,X1)) . x = (M2 . B) * ((chi (A,X1)) . x)

proof

per cases ( x in A or not x in A ) ;

suppose J18: x in A ; :: thesis: (Xchi (A,X1)) . x = (M2 . B) * ((chi (A,X1)) . x)

then J19: (Xchi (A,X1)) . x = +infty by DefXchi;
(chi (A,X1)) . x = 1 by J18, FUNCT_3:def 3;
hence (Xchi (A,X1)) . x = (M2 . B) * ((chi (A,X1)) . x) by J19, I0, XXREAL_3:81; :: thesis: verum

end;

suppose J20: not x in A ; :: thesis: (Xchi (A,X1)) . x = (M2 . B) * ((chi (A,X1)) . x)

then J21: (Xchi (A,X1)) . x = 0 by DefXchi;
(chi (A,X1)) . x = 0 by J20, FUNCT_3:def 3;
hence (Xchi (A,X1)) . x = (M2 . B) * ((chi (A,X1)) . x) by J21; :: thesis: verum

end;

end;

end;

hence (lim (Partial_Sums FI)) . x = (Xchi (A,X1)) . x by J17, J4, J6, FUNCT_2:63; :: thesis: verum

end;

then I1: lim (Partial_Sums FI) = Xchi (A,X1) by J1, FUNCT_2:63;

per cases ( M1 . A <> 0 or M1 . A = 0 ) ;

suppose I2: M1 . A <> 0 ; :: thesis: Integral (M1,(lim (Partial_Sums FI))) = (M1 . A) * (M2 . B)

then M1 . A > 0 by SUPINF_2:51;
then (M1 . A) * (M2 . B) = +infty by I0, XXREAL_3:def 5;
hence Integral (M1,(lim (Partial_Sums FI))) = (M1 . A) * (M2 . B) by I1, I2, Th34; :: thesis: verum

end;

suppose I3: M1 . A = 0 ; :: thesis: Integral (M1,(lim (Partial_Sums FI))) = (M1 . A) * (M2 . B)

then (M1 . A) * (M2 . B) = 0 ;
hence Integral (M1,(lim (Partial_Sums FI))) = (M1 . A) * (M2 . B) by I1, I3, Th34; :: thesis: verum

end;

end;

end;

suppose J22: M2 . B <> +infty ; :: thesis: Integral (M1,(lim (Partial_Sums FI))) = (M1 . A) * (M2 . B)

M2 . B >= 0 by SUPINF_2:51;
then M2 . B in REAL by J22, XXREAL_0:14;
then reconsider M2B = M2 . B as Real ;
G3: X1 = dom (chi (A,X1)) by FUNCT_3:def 3;
dom (M2B (#) (chi (A,X1))) = dom (chi (A,X1)) by MESFUNC1:def 6;
then G0: dom (M2B (#) (chi (A,X1))) = X1 by FUNCT_3:def 3;
then G1: M2B (#) (chi (A,X1)) is Function of X1,ExtREAL by FUNCT_2:def 1;
R5: chi (A,X1) is XX -measurable by MESFUNC2:29;
for x being Element of X1 holds (lim (Partial_Sums FI)) . x = (M2B (#) (chi (A,X1))) . x

proof

let x be Element of X1; :: thesis: (lim (Partial_Sums FI)) . x = (M2B (#) (chi (A,X1))) . x
JJ: x in X1 ;
J2: dom (FI . 0) = X1 by H3;
J4: (lim (Partial_Sums FI)) . x = lim ((Partial_Sums FI) # x) by V1, MESFUNC8:def 9;
consider I being ExtREAL_sequence such that
J5: for n being Nat holds
( I . n = (M2 . (E . n)) * ((chi ((D . n),X1)) . x) & (M2 . B) * ((chi (A,X1)) . x) = Sum I ) by ZZ;
J6: lim (Partial_Sums I) = (M2 . B) * ((chi (A,X1)) . x) by J5, MESFUNC9:def 3;
for n being Element of NAT holds (FI # x) . n = I . n

proof

let n be Element of NAT ; :: thesis: (FI # x) . n = I . n
( M2 . (E . n) <= M2 . B & M2 . B < +infty ) by Y3, MEASURE1:8, J22, XXREAL_0:4;
then consider m2 being Real such that
J15: ( m2 = M2 . (E . n) & FI . n = m2 (#) (chi ((D . n),X1)) ) by H2;
x in dom (FI . n) by JJ, H3;
then (FI . n) . x = m2 * ((chi ((D . n),X1)) . x) by J15, MESFUNC1:def 6;
then (FI # x) . n = m2 * ((chi ((D . n),X1)) . x) by MESFUNC5:def 13;
hence (FI # x) . n = I . n by J15, J5; :: thesis: verum

end;

then FI # x = I by FUNCT_2:63;
then for n being Element of NAT holds ((Partial_Sums FI) # x) . n = (Partial_Sums I) . n by F2A, F3, J2, MESFUNC9:30, MESFUNC9:32;
then lim ((Partial_Sums FI) # x) = lim (Partial_Sums I) by FUNCT_2:63;
hence (lim (Partial_Sums FI)) . x = (M2B (#) (chi (A,X1))) . x by J4, J6, G0, MESFUNC1:def 6; :: thesis: verum

end;

then lim (Partial_Sums FI) = M2B (#) (chi (A,X1)) by J1, G1, FUNCT_2:63;
then integral+ (M1,(lim (Partial_Sums FI))) = M2B * (integral+ (M1,(chi (A,X1)))) by SUPINF_2:51, G3, R5, MESFUNC5:86;
then Integral (M1,(lim (Partial_Sums FI))) = M2B * (integral+ (M1,(chi (A,X1)))) by V1, V2, V4, V5, W1, W4, MESFUNC8:25, MESFUNC5:88;
then Integral (M1,(lim (Partial_Sums FI))) = M2B * (Integral (M1,(chi (A,X1)))) by G3, R5, MESFUNC5:88;
hence Integral (M1,(lim (Partial_Sums FI))) = (M1 . A) * (M2 . B) by MESFUNC9:14; :: thesis: verum

end;

end;

end;

hence (product-pre-Measure (M1,M2)) . (Union K) = SUM ((product-pre-Measure (M1,M2)) * K) by F9, HH2, F6, F7, MEASURE8:2; :: thesis: verum