let X1, X2 be non empty set ; 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 E being Element of sigma (measurable_rectangles (S1,S2)) st E in Field_generated_by (measurable_rectangles (S1,S2)) & M1 is sigma_finite holds
for V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st V = [:A,B:] holds
E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
let S1 be SigmaField of X1; for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2)) st E in Field_generated_by (measurable_rectangles (S1,S2)) & M1 is sigma_finite holds
for V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st V = [:A,B:] holds
E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
let S2 be SigmaField of X2; for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2)) st E in Field_generated_by (measurable_rectangles (S1,S2)) & M1 is sigma_finite holds
for V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st V = [:A,B:] holds
E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
let M1 be sigma_Measure of S1; for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2)) st E in Field_generated_by (measurable_rectangles (S1,S2)) & M1 is sigma_finite holds
for V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st V = [:A,B:] holds
E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
let M2 be sigma_Measure of S2; for E being Element of sigma (measurable_rectangles (S1,S2)) st E in Field_generated_by (measurable_rectangles (S1,S2)) & M1 is sigma_finite holds
for V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st V = [:A,B:] holds
E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
let E be Element of sigma (measurable_rectangles (S1,S2)); ( E in Field_generated_by (measurable_rectangles (S1,S2)) & M1 is sigma_finite implies for V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st V = [:A,B:] holds
E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } )
assume that
A1:
E in Field_generated_by (measurable_rectangles (S1,S2))
and
A2:
M1 is sigma_finite
; for V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st V = [:A,B:] holds
E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
let V be Element of sigma (measurable_rectangles (S1,S2)); for A being Element of S1
for B being Element of S2 st V = [:A,B:] holds
E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
let A be Element of S1; for B being Element of S2 st V = [:A,B:] holds
E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
let B be Element of S2; ( V = [:A,B:] implies E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } )
assume
V = [:A,B:]
; E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
then
V in { [:A,B:] where A is Element of S1, B is Element of S2 : verum }
;
then A5:
V in measurable_rectangles (S1,S2)
by MEASUR10:def 5;
measurable_rectangles (S1,S2) c= Field_generated_by (measurable_rectangles (S1,S2))
by SRINGS_3:21;
then A6:
E /\ V in Field_generated_by (measurable_rectangles (S1,S2))
by A1, A5, FINSUB_1:def 2;
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
E /\ V in DisUnion (measurable_rectangles (S1,S2))
by A6, SRINGS_3:22;
then
E /\ V in { W where W is Subset of [:X1,X2:] : ex G being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st W = Union G }
by SRINGS_3:def 3;
then consider W being Subset of [:X1,X2:] such that
A11:
( E /\ V = W & ex G being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st W = Union G )
;
consider G being disjoint_valued FinSequence of measurable_rectangles (S1,S2) such that
A12:
E /\ V = Union G
by A11;
A13:
G in (measurable_rectangles (S1,S2)) *
by FINSEQ_1:def 11;
measurable_rectangles (S1,S2) c= sigma (measurable_rectangles (S1,S2))
by PROB_1:def 9;
then
(measurable_rectangles (S1,S2)) * c= (sigma (measurable_rectangles (S1,S2))) *
by FINSEQ_1:62;
then reconsider G = G as disjoint_valued FinSequence of sigma (measurable_rectangles (S1,S2)) by A13, FINSEQ_1:def 11;
Integral (M2,(X-vol ((Union G),M1))) = (product_sigma_Measure (M1,M2)) . (Union G)
by A2, Th103;
hence
E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
by A12; verum