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 A being Element of S1
for B being Element of S2 holds (product_Measure (M1,M2)) . [:A,B:] = (M1 . A) * (M2 . B)
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 A being Element of S1
for B being Element of S2 holds (product_Measure (M1,M2)) . [:A,B:] = (M1 . A) * (M2 . B)
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for A being Element of S1
for B being Element of S2 holds (product_Measure (M1,M2)) . [:A,B:] = (M1 . A) * (M2 . B)
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for A being Element of S1
for B being Element of S2 holds (product_Measure (M1,M2)) . [:A,B:] = (M1 . A) * (M2 . B)
let M2 be sigma_Measure of S2; :: thesis: for A being Element of S1
for B being Element of S2 holds (product_Measure (M1,M2)) . [:A,B:] = (M1 . A) * (M2 . B)
let A be Element of S1; :: thesis: for B being Element of S2 holds (product_Measure (M1,M2)) . [:A,B:] = (M1 . A) * (M2 . B)
let B be Element of S2; :: thesis: (product_Measure (M1,M2)) . [:A,B:] = (M1 . A) * (M2 . B)
set S = measurable_rectangles (S1,S2);
set P = product-pre-Measure (M1,M2);
set m = product_Measure (M1,M2);
A1: DisUnion (measurable_rectangles (S1,S2)) = Field_generated_by (measurable_rectangles (S1,S2)) by SRINGS_3:22;
[:A,B:] in { [:A,B:] where A is Element of S1, B is Element of S2 : verum } ;
then A2: [:A,B:] in measurable_rectangles (S1,S2) by MEASUR10:def 5;
then reconsider F = <*[:A,B:]*> as disjoint_valued FinSequence of measurable_rectangles (S1,S2) by FINSEQ_1:74;
A3: measurable_rectangles (S1,S2) c= DisUnion (measurable_rectangles (S1,S2)) by SRINGS_3:12;
consider SumPF being sequence of ExtREAL such that
A4: ( Sum ((product-pre-Measure (M1,M2)) * F) = SumPF . (len ((product-pre-Measure (M1,M2)) * F)) & SumPF . 0 = 0. & ( for n being Nat st n < len ((product-pre-Measure (M1,M2)) * F) holds
SumPF . (n + 1) = (SumPF . n) + (((product-pre-Measure (M1,M2)) * F) . (n + 1)) ) ) by EXTREAL1:def 2;
A5: len F = 1 by FINSEQ_1:39;
then A6: 1 in dom F by FINSEQ_3:25;
len ((product-pre-Measure (M1,M2)) * F) = 1 by A5, FINSEQ_3:120;
then Sum ((product-pre-Measure (M1,M2)) * F) = (SumPF . 0) + (((product-pre-Measure (M1,M2)) * F) . (0 + 1)) by A4;
then Sum ((product-pre-Measure (M1,M2)) * F) = ((product-pre-Measure (M1,M2)) * F) . 1 by A4, XXREAL_3:4;
then Sum ((product-pre-Measure (M1,M2)) * F) = (product-pre-Measure (M1,M2)) . (F . 1) by A6, FUNCT_1:13;
then Sum ((product-pre-Measure (M1,M2)) * F) = (product-pre-Measure (M1,M2)) . [:A,B:] ;
then A7: Sum ((product-pre-Measure (M1,M2)) * F) = (M1 . A) * (M2 . B) by MEASUR10:22;
rng <*[:A,B:]*> = {[:A,B:]} by FINSEQ_1:39;
then union (rng <*[:A,B:]*>) = [:A,B:] by ZFMISC_1:25;
then [:A,B:] = Union <*[:A,B:]*> by CARD_3:def 4;
hence (product_Measure (M1,M2)) . [:A,B:] = (M1 . A) * (M2 . B) by A1, A2, A3, A7, MEASURE9:def 8; :: thesis: verum