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_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_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_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_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_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_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_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n))
let n be Nat; :: thesis: (product_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n))
( F1 . n in S1 & F2 . n in S2 ) by MEASURE8:def 2;
hence (product_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n)) by Th5; :: thesis: verum