let X1, X2 be non empty set ; :: thesis:
let S1 be SigmaField of X1; :: thesis:
let S2 be SigmaField of X2; :: thesis:
let M2 be sigma_Measure of S2; :: thesis:
let D be Function of NAT,S1; :: thesis:
let E be Function of NAT,S2; :: thesis:
let A be Element of S1; :: thesis:
let B be Element of S2; :: thesis:
let F be Functional_Sequence of X2,ExtREAL; :: thesis:
let RD be sequence of (Funcs (X1,REAL)); :: thesis:
let x be Element of X1; :: thesis:
assume that
A7: for n being Nat holds RD . n = chi ((D . n),X1) and
A8: for n being Nat holds F . n = ((RD . n) . x) (#) (chi ((E . n),X2)) and
A9: for n being Nat holds E . n c= B ; :: thesis:
B1: for n being Nat holds dom (F . n) = X2

proof

let n be Nat; :: thesis:
dom (F . n) = dom (((RD . n) . x) (#) (chi ((E . n),X2))) by A8;
then dom (F . n) = dom (chi ((E . n),X2)) by MESFUNC1:def 6;
hence dom (F . n) = X2 by FUNCT_3:def 3; :: thesis:

end;

reconsider SX2 = X2 as Element of S2 by PROB_1:5;
P1: dom (F . 0) = X2 by B1;
B2: for n being Nat
for y being set holds
( not y in E . n or (F . n) . y = 0 or (F . n) . y = 1 )

proof

let n be Nat; :: thesis:
let y be set ; :: thesis:
assume B3: y in E . n ; :: thesis:
B4: E . n in S2 ;
then y in X2 by B3;
then B5: y in dom (F . n) by B1;
then B6: (F . n) . y in rng (F . n) by FUNCT_1:3;
reconsider y1 = y as Element of X2 by B3, B4;

B7: now :: thesis:

assume x in D . n ; :: thesis:
then (chi ((D . n),X1)) . x = 1 by FUNCT_3:def 3;
then (RD . n) . x = 1 by A7;
then F . n = 1 (#) (chi ((E . n),X2)) by A8;
then F . n = chi ((E . n),X2) by MESFUNC2:1;
then rng (F . n) c= {0,1} by FUNCT_3:39;
hence ( (F . n) . y = 0 or (F . n) . y = 1 ) by B6, TARSKI:def 2; :: thesis:

end;

now :: thesis:

assume not x in D . n ; :: thesis:
then (chi ((D . n),X1)) . x = 0 by FUNCT_3:def 3;
then (RD . n) . x = 0 by A7;
then F . n = 0 (#) (chi ((E . n),X2)) by A8;
then (F . n) . y = 0 * ((chi ((E . n),X2)) . y1) by B5, MESFUNC1:def 6;
hence (F . n) . y = 0 ; :: thesis:

end;

hence ( (F . n) . y = 0 or (F . n) . y = 1 ) by B7; :: thesis:

end;

B8: for n being Nat
for y being set st not y in E . n holds
(F . n) . y = 0

proof

let n be Nat; :: thesis:
let y be set ; :: thesis:
assume B9: not y in E . n ; :: thesis:

B10: now :: thesis:

assume B11: y in X2 ; :: thesis:
then reconsider y1 = y as Element of X2 ;
B12: (chi ((E . n),X2)) . y1 = 0 by B9, FUNCT_3:def 3;
B13: y in dom (F . n) by B1, B11;
F . n = ((RD . n) . x) (#) (chi ((E . n),X2)) by A8;
then (F . n) . y = ((RD . n) . x) * ((chi ((E . n),X2)) . y1) by B13, MESFUNC1:def 6;
hence (F . n) . y = 0 by B12; :: thesis:

end;

now :: thesis:

assume not y in X2 ; :: thesis:
then not y in dom (F . n) ;
hence (F . n) . y = 0 by FUNCT_1:def 2; :: thesis:

end;

hence (F . n) . y = 0 by B10; :: thesis:

end;

P2: now :: thesis:

let n, m be Nat; :: thesis:
assume n <> m ; :: thesis:
thus for y being set holds
( not y in (dom (F . n)) /\ (dom (F . m)) or (F . n) . y <> +infty or (F . m) . y <> -infty ) :: thesis:

proof

let y be set ; :: thesis:
assume y in (dom (F . n)) /\ (dom (F . m)) ; :: thesis:
( not y in E . n or (F . n) . y <> +infty or (F . m) . y <> -infty ) by B2;
hence ( (F . n) . y <> +infty or (F . m) . y <> -infty ) by B8; :: thesis:

end;

then S2: F is additive by MESFUNC9:def 5;

now :: thesis:

let n, m be Nat; :: thesis:
( dom (F . n) = X2 & dom (F . m) = X2 ) by B1;
hence dom (F . n) = dom (F . m) ; :: thesis:

end;

then P3: F is with_the_same_dom by MESFUNC8:def 2;
P4: for n being Nat holds
( F . n is nonnegative & F . n is B -measurable )

proof

let n be Nat; :: thesis:

now :: thesis:

let y be object ; :: thesis:

per cases ;

suppose not y in dom (F . n) ; :: thesis:

hence (F . n) . y >= 0 by FUNCT_1:def 2; :: thesis:

end;

suppose ( y in dom (F . n) & y in E . n ) ; :: thesis:

hence (F . n) . y >= 0 by B2; :: thesis:

end;

suppose ( y in dom (F . n) & not y in E . n ) ; :: thesis:

hence (F . n) . y >= 0 by B8; :: thesis:

end;

hence F . n is nonnegative by SUPINF_2:51; :: thesis:
thus F . n is B -measurable :: thesis:

proof

B14: dom (chi ((E . n),X2)) = X2 by FUNCT_3:def 3;

per cases ;

suppose x in D . n ; :: thesis:

then (chi ((D . n),X1)) . x = 1 by FUNCT_3:def 3;
then (RD . n) . x = 1 by A7;
then F . n = 1 (#) (chi ((E . n),X2)) by A8;
hence F . n is B -measurable by B14, MESFUNC1:37, MESFUNC2:29; :: thesis:

end;

suppose not x in D . n ; :: thesis:

then (chi ((D . n),X1)) . x = 0 by FUNCT_3:def 3;
then (RD . n) . x = 0 by A7;
then F . n = 0 (#) (chi ((E . n),X2)) by A8;
hence F . n is B -measurable by B14, MESFUNC1:37, MESFUNC2:29; :: thesis:

end;

for y being Element of X2 st y in B holds
F # y is summable

proof

let y be Element of X2; :: thesis:
assume y in B ; :: thesis:
for n being Element of NAT holds 0 <= (F # y) . n

proof

let n be Element of NAT ; :: thesis:
(F # y) . n = (F . n) . y by MESFUNC5:def 13;
hence 0 <= (F # y) . n by P4, SUPINF_2:51; :: thesis:

end;

then F # y is nonnegative by SUPINF_2:39;
then Partial_Sums (F # y) is non-decreasing by MESFUNC9:16;
hence F # y is summable by RINFSUP2:37, MESFUNC9:def 2; :: thesis:

end;

then consider I being ExtREAL_sequence such that
Q1: ( ( for n being Nat holds I . n = Integral (M2,((F . n) | B)) ) & I is summable & Integral (M2,((lim (Partial_Sums F)) | B)) = Sum I ) by P1, P2, P3, P4, MESFUNC9:def 5, MESFUNC9:51;
take I ; :: thesis:
R1: for n being Nat holds chi ((E . n),X2) is SX2 -measurable by MESFUNC2:29;
Q2: for n being Nat holds I . n = (M2 . (E . n)) * ((chi ((D . n),X1)) . x)

proof

let n be Nat; :: thesis:
B16: I . n = Integral (M2,((F . n) | B)) by Q1;
B17: dom ((F . n) | B) = (dom (F . n)) /\ B by RELAT_1:61;
then B18: dom ((F . n) | B) = X2 /\ B by B1;
B19: dom (((RD . n) . x) (#) ((chi ((E . n),X2)) | B)) = dom ((chi ((E . n),X2)) | B) by MESFUNC1:def 6
.= (dom (chi ((E . n),X2))) /\ B by RELAT_1:61
.= X2 /\ B by FUNCT_3:def 3 ;

now :: thesis:

let y be object ; :: thesis:
assume B20: y in dom ((F . n) | B) ; :: thesis:
then reconsider y1 = y as Element of X2 ;
B22: ( y in X2 & y in B ) by B17, B20, XBOOLE_0:def 4;
dom (chi ((E . n),X2)) = X2 by FUNCT_3:def 3;
then B23: y in dom (((RD . n) . x) (#) (chi ((E . n),X2))) by B22, MESFUNC1:def 6;
B21: ((F . n) | B) . y = (F . n) . y1 by B20, FUNCT_1:47
.= (((RD . n) . x) (#) (chi ((E . n),X2))) . y1 by A8
.= ((RD . n) . x) * ((chi ((E . n),X2)) . y) by B23, MESFUNC1:def 6 ;
(((RD . n) . x) (#) ((chi ((E . n),X2)) | B)) . y = ((RD . n) . x) * (((chi ((E . n),X2)) | B) . y) by B20, B18, B19, MESFUNC1:def 6
.= ((RD . n) . x) * ((chi ((E . n),X2)) . y) by B22, FUNCT_1:49 ;
hence ((F . n) | B) . y = (((RD . n) . x) (#) ((chi ((E . n),X2)) | B)) . y by B21; :: thesis:

end;

then B24: I . n = Integral (M2,(((RD . n) . x) (#) ((chi ((E . n),X2)) | B))) by B16, B18, B19, FUNCT_1:def 11;
C0: B = dom (((RD . n) . x) (#) ((chi ((E . n),X2)) | B)) by B19, XBOOLE_1:28;
C4: dom ((chi ((E . n),X2)) | B) = (dom (chi ((E . n),X2))) /\ B by RELAT_1:61;
(dom (chi ((E . n),X2))) /\ B = X2 /\ B by FUNCT_3:def 3;
then C3: (dom (chi ((E . n),X2))) /\ B = B by XBOOLE_1:28;
then C8: (chi ((E . n),X2)) | B is B -measurable by MESFUNC2:29, MESFUNC5:42;
C5a: (chi ((E . n),X2)) | B is nonnegative by MESFUNC5:15;

C6: now :: thesis:

assume x in D . n ; :: thesis:
then (chi ((D . n),X1)) . x = 1 by FUNCT_3:def 3;
hence (RD . n) . x = 1 by A7; :: thesis:

end;

C7: now :: thesis:

assume not x in D . n ; :: thesis:
then (chi ((D . n),X1)) . x = 0 by FUNCT_3:def 3;
hence (RD . n) . x = 0 by A7; :: thesis:

end;

then ((RD . n) . x) (#) ((chi ((E . n),X2)) | B) is nonnegative by C5a, C6, MESFUNC5:20;
then I . n = integral+ (M2,(((RD . n) . x) (#) ((chi ((E . n),X2)) | B))) by B24, C0, C8, C3, C4, MESFUNC1:37, MESFUNC5:88;
then I . n = ((RD . n) . x) * (integral+ (M2,((chi ((E . n),X2)) | B))) by C3, C4, C6, C7, C8, MESFUNC5:15, MESFUNC5:86;
then D2: I . n = ((RD . n) . x) * (Integral (M2,((chi ((E . n),X2)) | B))) by C3, C4, C8, MESFUNC5:15, MESFUNC5:88;
E1: dom (chi ((E . n),X2)) = X2 by FUNCT_3:def 3;
for y being object st y in (dom (chi ((E . n),X2))) \ B holds
(chi ((E . n),X2)) . y = 0

proof

let y be object ; :: thesis:
assume E4: y in (dom (chi ((E . n),X2))) \ B ; :: thesis:
then reconsider y1 = y as Element of X2 ;
E . n c= B by A9;
then not y1 in E . n by E4, XBOOLE_0:def 5;
hence (chi ((E . n),X2)) . y = 0 by FUNCT_3:def 3; :: thesis:

end;

then Integral (M2,(chi ((E . n),X2))) = Integral (M2,((chi ((E . n),X2)) | B)) by E1, R1, Th28;
then I . n = (M2 . (E . n)) * ((RD . n) . x) by D2, MESFUNC9:14;
hence I . n = (M2 . (E . n)) * ((chi ((D . n),X1)) . x) by A7; :: thesis:

end;

F1: dom (lim (Partial_Sums F)) = dom ((Partial_Sums F) . 0) by MESFUNC8:def 9
.= dom (F . 0) by MESFUNC9:def 4 ;
then F4: dom (lim (Partial_Sums F)) = SX2 by B1;
G0: Partial_Sums F is with_the_same_dom Functional_Sequence of X2,ExtREAL by P2, P3, MESFUNC9:def 5, MESFUNC9:43;
G1: dom ((Partial_Sums F) . 0) = dom (F . 0) by MESFUNC9:def 4
.= SX2 by B1 ;
R2: for n being Nat holds F . n is SX2 -measurable

proof

let n be Nat; :: thesis:
( chi ((E . n),X2) is SX2 -measurable & dom (chi ((E . n),X2)) = SX2 ) by MESFUNC2:29, FUNCT_3:def 3;
then ((RD . n) . x) (#) (chi ((E . n),X2)) is SX2 -measurable by MESFUNC1:37;
hence F . n is SX2 -measurable by A8; :: thesis:

end;

for n being Nat holds F . n is without-infty

proof

let n be Nat; :: thesis:
F . n is nonnegative by P4;
hence F . n is without-infty ; :: thesis:

end;

then G2: for n being Nat holds (Partial_Sums F) . n is SX2 -measurable by R2, MESFUNC9:41;
for y being Element of X2 st y in SX2 holds
(Partial_Sums F) # y is convergent

proof

let y be Element of X2; :: thesis:
assume y in SX2 ; :: thesis:
then y in dom (F . 0) by B1;
hence (Partial_Sums F) # y is convergent by P3, P4, MESFUNC9:38; :: thesis:

end;

then F2: lim (Partial_Sums F) is SX2 -measurable by G0, G1, G2, MESFUNC8:25;
F3: for y being object st y in (dom (lim (Partial_Sums F))) \ B holds
(lim (Partial_Sums F)) . y = 0

proof

let y be object ; :: thesis:
assume K0: y in (dom (lim (Partial_Sums F))) \ B ; :: thesis:
then K1: ( y in dom (lim (Partial_Sums F)) & not y in B ) by XBOOLE_0:def 5;
then y in dom ((Partial_Sums F) . 0) by MESFUNC8:def 9;
then J1: y in dom (F . 0) by MESFUNC9:def 4;
reconsider y1 = y as Element of X2 by K0;
K2: (lim (Partial_Sums F)) . y = lim ((Partial_Sums F) # y1) by K1, MESFUNC8:def 9;
for n being Nat holds ((Partial_Sums F) # y1) . n = 0

proof

let n be Nat; :: thesis:
K6: ((Partial_Sums F) # y1) . n = ((Partial_Sums F) . n) . y1 by MESFUNC5:def 13;
defpred S₁[ Nat] means ((Partial_Sums F) . $1) . y1 = 0 ;
K3: ((Partial_Sums F) . 0) . y1 = (F . 0) . y1 by MESFUNC9:def 4;
E . 0 c= B by A9;
then K4: S₁[ 0 ] by K1, K3, B8;
K5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume J2: S₁[k] ; :: thesis:
J3: dom ((Partial_Sums F) . (k + 1)) = dom ((Partial_Sums F) . 0) by S2, P3, MESFUNC9:43, MESFUNC8:def 2
.= dom (F . 0) by MESFUNC9:def 4 ;
J4: E . (k + 1) c= B by A9;
(Partial_Sums F) . (k + 1) = ((Partial_Sums F) . k) + (F . (k + 1)) by MESFUNC9:def 4;
then ((Partial_Sums F) . (k + 1)) . y1 = (((Partial_Sums F) . k) . y1) + ((F . (k + 1)) . y1) by J1, J3, MESFUNC1:def 3
.= (F . (k + 1)) . y1 by J2, XXREAL_3:4 ;
hence S₁[k + 1] by J4, B8, K1; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(K4, K5);
hence ((Partial_Sums F) # y1) . n = 0 by K6; :: thesis:

end;

hence (lim (Partial_Sums F)) . y = 0 by K2, MESFUNC5:52; :: thesis:

end;

for y being object st y in dom (lim (Partial_Sums F)) holds
(lim (Partial_Sums F)) . y >= 0

proof

let y be object ; :: thesis:
assume L1: y in dom (lim (Partial_Sums F)) ; :: thesis:
then reconsider y1 = y as Element of X2 ;
L2: for n being Nat holds ((Partial_Sums F) # y1) . n >= 0

proof

let n be Nat; :: thesis:
((Partial_Sums F) . n) . y1 >= 0 by P4, MESFUNC9:36, SUPINF_2:51;
hence ((Partial_Sums F) # y1) . n >= 0 by MESFUNC5:def 13; :: thesis:

end;

lim ((Partial_Sums F) # y1) >= 0 by L1, F1, L2, P3, P4, MESFUNC9:10, MESFUNC9:38;
hence (lim (Partial_Sums F)) . y >= 0 by L1, MESFUNC8:def 9; :: thesis:

end;

hence ( ( for n being Nat holds I . n = (M2 . (E . n)) * ((chi ((D . n),X1)) . x) ) & I is summable & Integral (M2,(lim (Partial_Sums F))) = Sum I ) by Q1, Q2, F4, F2, F3, Th28, SUPINF_2:52; :: thesis: