let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being Finite_Sep_Sequence of S holds dom F = dom (M * F)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for F being Finite_Sep_Sequence of S holds dom F = dom (M * F)
let M be sigma_Measure of S; :: thesis: for F being Finite_Sep_Sequence of S holds dom F = dom (M * F)
let F be Finite_Sep_Sequence of S; :: thesis: dom F = dom (M * F)
dom M = S by FUNCT_2:def 1;
then rng F c= dom M ;
hence dom F = dom (M * F) by RELAT_1:27; :: thesis: verum