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 E being Element of sigma (measurable_rectangles (S1,S2)) st E in Field_generated_by (measurable_rectangles (S1,S2)) & M2 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 (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
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 E being Element of sigma (measurable_rectangles (S1,S2)) st E in Field_generated_by (measurable_rectangles (S1,S2)) & M2 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 (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
let S2 be SigmaField of X2; :: thesis: 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)) & M2 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 (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
let M1 be sigma_Measure of S1; :: thesis: 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)) & M2 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 (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
let M2 be sigma_Measure of S2; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2)) st E in Field_generated_by (measurable_rectangles (S1,S2)) & M2 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 (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
let E be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( E in Field_generated_by (measurable_rectangles (S1,S2)) & M2 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 (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } )
assume that
A1: E in Field_generated_by (measurable_rectangles (S1,S2)) and
A2: M2 is sigma_finite ; :: thesis: 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 (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
let V be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: 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 (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
let A be Element of S1; :: thesis: 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 (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
let B be Element of S2; :: thesis: ( V = [:A,B:] implies E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } )
assume A3: V = [:A,B:] ; :: thesis: E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
V in { [:A,B:] where A is Element of S1, B is Element of S2 : verum } by A3;
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 XX1 = X1 as Element of S1 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 (M1,(Y-vol ((Union G),M2))) = (product_sigma_Measure (M1,M2)) . (Union G) by A2, Th102;
hence E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } by A12; :: thesis: verum