let X1, X2 be non empty set ; for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for D being Function of NAT,S1
for E being Function of NAT,S2
for A being Element of S1
for B being Element of S2
for F being Functional_Sequence of X2,ExtREAL
for RD being sequence of (Funcs (X1,REAL))
for x being Element of X1 st ( for n being Nat holds RD . n = chi ((D . n),X1) ) & ( for n being Nat holds F . n = ((RD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds E . n c= B ) holds
ex I being ExtREAL_sequence st
( ( 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 )
let S1 be SigmaField of X1; for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for D being Function of NAT,S1
for E being Function of NAT,S2
for A being Element of S1
for B being Element of S2
for F being Functional_Sequence of X2,ExtREAL
for RD being sequence of (Funcs (X1,REAL))
for x being Element of X1 st ( for n being Nat holds RD . n = chi ((D . n),X1) ) & ( for n being Nat holds F . n = ((RD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds E . n c= B ) holds
ex I being ExtREAL_sequence st
( ( 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 )
let S2 be SigmaField of X2; for M2 being sigma_Measure of S2
for D being Function of NAT,S1
for E being Function of NAT,S2
for A being Element of S1
for B being Element of S2
for F being Functional_Sequence of X2,ExtREAL
for RD being sequence of (Funcs (X1,REAL))
for x being Element of X1 st ( for n being Nat holds RD . n = chi ((D . n),X1) ) & ( for n being Nat holds F . n = ((RD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds E . n c= B ) holds
ex I being ExtREAL_sequence st
( ( 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 )
let M2 be sigma_Measure of S2; for D being Function of NAT,S1
for E being Function of NAT,S2
for A being Element of S1
for B being Element of S2
for F being Functional_Sequence of X2,ExtREAL
for RD being sequence of (Funcs (X1,REAL))
for x being Element of X1 st ( for n being Nat holds RD . n = chi ((D . n),X1) ) & ( for n being Nat holds F . n = ((RD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds E . n c= B ) holds
ex I being ExtREAL_sequence st
( ( 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 )
let D be Function of NAT,S1; for E being Function of NAT,S2
for A being Element of S1
for B being Element of S2
for F being Functional_Sequence of X2,ExtREAL
for RD being sequence of (Funcs (X1,REAL))
for x being Element of X1 st ( for n being Nat holds RD . n = chi ((D . n),X1) ) & ( for n being Nat holds F . n = ((RD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds E . n c= B ) holds
ex I being ExtREAL_sequence st
( ( 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 )
let E be Function of NAT,S2; for A being Element of S1
for B being Element of S2
for F being Functional_Sequence of X2,ExtREAL
for RD being sequence of (Funcs (X1,REAL))
for x being Element of X1 st ( for n being Nat holds RD . n = chi ((D . n),X1) ) & ( for n being Nat holds F . n = ((RD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds E . n c= B ) holds
ex I being ExtREAL_sequence st
( ( 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 )
let A be Element of S1; for B being Element of S2
for F being Functional_Sequence of X2,ExtREAL
for RD being sequence of (Funcs (X1,REAL))
for x being Element of X1 st ( for n being Nat holds RD . n = chi ((D . n),X1) ) & ( for n being Nat holds F . n = ((RD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds E . n c= B ) holds
ex I being ExtREAL_sequence st
( ( 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 )
let B be Element of S2; for F being Functional_Sequence of X2,ExtREAL
for RD being sequence of (Funcs (X1,REAL))
for x being Element of X1 st ( for n being Nat holds RD . n = chi ((D . n),X1) ) & ( for n being Nat holds F . n = ((RD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds E . n c= B ) holds
ex I being ExtREAL_sequence st
( ( 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 )
let F be Functional_Sequence of X2,ExtREAL; for RD being sequence of (Funcs (X1,REAL))
for x being Element of X1 st ( for n being Nat holds RD . n = chi ((D . n),X1) ) & ( for n being Nat holds F . n = ((RD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds E . n c= B ) holds
ex I being ExtREAL_sequence st
( ( 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 )
let RD be sequence of (Funcs (X1,REAL)); for x being Element of X1 st ( for n being Nat holds RD . n = chi ((D . n),X1) ) & ( for n being Nat holds F . n = ((RD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds E . n c= B ) holds
ex I being ExtREAL_sequence st
( ( 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 )
let x be Element of X1; ( ( for n being Nat holds RD . n = chi ((D . n),X1) ) & ( for n being Nat holds F . n = ((RD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds E . n c= B ) implies ex I being ExtREAL_sequence st
( ( 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 ) )
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
; ex I being ExtREAL_sequence st
( ( 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 )
B1:
for n being Nat holds dom (F . n) = X2
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 )
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;
for y being set st not y in E . n holds
(F . n) . y = 0 let y be
set ;
( not y in E . n implies (F . n) . y = 0 )
assume B9:
not
y in E . n
;
(F . n) . y = 0
B10:
now ( y in X2 implies (F . n) . y = 0 )end;
now ( not y in X2 implies (F . n) . y = 0 )end;
hence
(F . n) . y = 0
by B10;
verum
end;
then S2:
F is additive
by MESFUNC9:def 5;
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 )
for y being Element of X2 st y in B holds
F # y is summable
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
; ( ( 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 )
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;
I . n = (M2 . (E . n)) * ((chi ((D . n),X1)) . x)
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 for y being object st y in dom ((F . n) | B) holds
((F . n) | B) . y = (((RD . n) . x) (#) ((chi ((E . n),X2)) | B)) . ylet y be
object ;
( y in dom ((F . n) | B) implies ((F . n) | B) . y = (((RD . n) . x) (#) ((chi ((E . n),X2)) | B)) . y )assume B20:
y in dom ((F . n) | B)
;
((F . n) | B) . y = (((RD . n) . x) (#) ((chi ((E . n),X2)) | B)) . ythen 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;
verum 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 ( x in D . n implies (RD . n) . x = 1 )end;
C7:
now ( not x in D . n implies (RD . n) . x = 0 )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
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;
verum
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
for n being Nat holds F . n is V169()
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
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
for y being object st y in dom (lim (Partial_Sums F)) holds
(lim (Partial_Sums F)) . y >= 0
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; verum