let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being Function of NAT,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 Function of NAT,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 Function of NAT,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 Function of NAT,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 set ; :: 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 set st
( n in NAT & Y = F . n ) by A4, FUNCT_1:def 3;
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 A1, MEASURE1:31;
hence M . A = M . (meet (rng F)) by A5, XXREAL_0:1; :: thesis: verum