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)

M . (meet (rng F)) <= M . A by A1, MEASURE1:31;

hence M . A = M . (meet (rng F)) by A5, XXREAL_0:1; :: thesis: verum

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

then A5:
M . A <= M . (meet (rng F))
by MEASURE1:31;
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

end;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

hence
x in meet (rng F)
by SETFAM_1:def 1; :: thesis: verum
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 A4, FUNCT_1:def 3;

then A c= Y by A2;

hence x in Y by A3; :: thesis: verum

end;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 A4, FUNCT_1:def 3;

then A c= Y by A2;

hence x in Y by A3; :: thesis: verum

M . (meet (rng F)) <= M . A by A1, MEASURE1:31;

hence M . A = M . (meet (rng F)) by A5, XXREAL_0:1; :: thesis: verum