let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being sequence of S
for A being Element of S st meet (rng F) c= A & ( for n being Element of NAT holds A c= F . n ) holds
M . A = M . (meet (rng F))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for F being sequence of S
for A being Element of S st meet (rng F) c= A & ( for n being Element of NAT holds A c= F . n ) holds
M . A = M . (meet (rng F))

let M be sigma_Measure of S; :: thesis: for F being sequence of S
for A being Element of S st meet (rng F) c= A & ( for n being Element of NAT holds A c= F . n ) holds
M . A = M . (meet (rng F))

let F be sequence of S; :: thesis: for A being Element of S st meet (rng F) c= A & ( for n being Element of NAT holds A c= F . n ) holds
M . A = M . (meet (rng F))

let A be Element of S; :: thesis: ( meet (rng F) c= A & ( for n being Element of NAT holds A c= F . n ) implies M . A = M . (meet (rng F)) )
assume that
A1: meet (rng F) c= A and
A2: for n being Element of NAT holds A c= F . n ; :: thesis: M . A = M . (meet (rng F))
A c= meet (rng F)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in meet (rng F) )
assume A3: x in A ; :: thesis: x in meet (rng F)
for Y being set st Y in rng F holds
x in Y
proof
let Y be set ; :: thesis: ( Y in rng F implies x in Y )
A4: dom F = NAT by FUNCT_2:def 1;
assume Y in rng F ; :: thesis: x in Y
then ex n being object st
( n in NAT & Y = F . n ) by ;
then A c= Y by A2;
hence x in Y by A3; :: thesis: verum
end;
hence x in meet (rng F) by SETFAM_1:def 1; :: thesis: verum
end;
then A5: M . A <= M . (meet (rng F)) by MEASURE1:31;
M . (meet (rng F)) <= M . A by ;
hence M . A = M . (meet (rng F)) by ; :: thesis: verum