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 F1 being Set_Sequence of S1
for F2 being Set_Sequence of S2
for n being Nat holds (product_sigma_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n))
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 F1 being Set_Sequence of S1
for F2 being Set_Sequence of S2
for n being Nat holds (product_sigma_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n))
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for F1 being Set_Sequence of S1
for F2 being Set_Sequence of S2
for n being Nat holds (product_sigma_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n))
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for F1 being Set_Sequence of S1
for F2 being Set_Sequence of S2
for n being Nat holds (product_sigma_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n))
let M2 be sigma_Measure of S2; :: thesis: for F1 being Set_Sequence of S1
for F2 being Set_Sequence of S2
for n being Nat holds (product_sigma_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n))
let F1 be Set_Sequence of S1; :: thesis: for F2 being Set_Sequence of S2
for n being Nat holds (product_sigma_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n))
let F2 be Set_Sequence of S2; :: thesis: for n being Nat holds (product_sigma_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n))
let n be Nat; :: thesis: (product_sigma_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n))
A1: [:(F1 . n),(F2 . n):] is Element of sigma (measurable_rectangles (S1,S2)) by Th3;
then A2: (product_sigma_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (sigma_Meas (C_Meas (product_Measure (M1,M2)))) . [:(F1 . n),(F2 . n):] by FUNCT_1:49;
A3: measurable_rectangles (S1,S2) c= Field_generated_by (measurable_rectangles (S1,S2)) by SRINGS_3:21;
( F1 . n in S1 & F2 . n in S2 ) by MEASURE8:def 2;
then [:(F1 . n),(F2 . n):] in { [:A,B:] where A is Element of S1, B is Element of S2 : verum } ;
then A4: [:(F1 . n),(F2 . n):] in measurable_rectangles (S1,S2) by MEASUR10:def 5;
product_Measure (M1,M2) is completely-additive by MEASURE9:60;
then A5: (product_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (C_Meas (product_Measure (M1,M2))) . [:(F1 . n),(F2 . n):] by A3, A4, MEASURE8:18;
sigma (measurable_rectangles (S1,S2)) c= sigma_Field (C_Meas (product_Measure (M1,M2))) by Th9;
then (product_sigma_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (product_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] by A1, A2, A5, MEASURE4:def 3;
hence (product_sigma_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n)) by Th6; :: thesis: verum