let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being sequence of S
for n being Nat holds { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } is Element of S
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for F being sequence of S
for n being Nat holds { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } is Element of S
let M be sigma_Measure of S; :: thesis: for F being sequence of S
for n being Nat holds { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } is Element of S
let F be sequence of S; :: thesis: for n being Nat holds { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } is Element of S
let n be Nat; :: thesis: { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } is Element of S
set G = { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } ;
deffunc H₁( Element of NAT ) -> Element of S = F . (n + $1);
consider E being sequence of S such that
A1: for k being Element of NAT holds E . k = H₁(k) from FUNCT_2:sch 4();

now :: thesis: for z being object st z in { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } holds
z in meet (rng E)

let z be object ; :: thesis: ( z in { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } implies z in meet (rng E) )
assume z in { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } ; :: thesis: z in meet (rng E)
then A2: ex x being Element of X st
( z = x & ( for k being Nat st n <= k holds
x in F . k ) ) ;
for Y being set st Y in rng E holds
z in Y

proof

let Y be set ; :: thesis: ( Y in rng E implies z in Y )
assume Y in rng E ; :: thesis: z in Y
then consider l being object such that
A3: l in NAT and
A4: Y = E . l by FUNCT_2:11;
reconsider l = l as Element of NAT by A3;
z in F . (n + l) by A2, NAT_1:12;
hence z in Y by A1, A4; :: thesis: verum

end;

hence z in meet (rng E) by SETFAM_1:def 1; :: thesis: verum

end;

then A5: { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } c= meet (rng E) ;
rng E is N_Sub_set_fam of X by MEASURE1:23;
then rng E is N_Measure_fam of S by MEASURE2:def 1;
then A6: meet (rng E) is Element of S by MEASURE2:2;

now :: thesis: for z being object st z in meet (rng E) holds
z in { x where x is Element of X : for k being Nat st n <= k holds
x in F . k }

let z be object ; :: thesis: ( z in meet (rng E) implies z in { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } )
assume A7: z in meet (rng E) ; :: thesis: z in { x where x is Element of X : for k being Nat st n <= k holds
x in F . k }

now :: thesis: for k being Nat st n <= k holds
z in F . k

let k be Nat; :: thesis: ( n <= k implies z in F . k )
assume n <= k ; :: thesis: z in F . k
then reconsider l = k - n as Element of NAT by NAT_1:21;
E . l in rng E by FUNCT_2:4;
then z in E . l by A7, SETFAM_1:def 1;
then z in F . (n + l) by A1;
hence z in F . k ; :: thesis: verum

end;

hence z in { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } by A6, A7; :: thesis: verum

end;

then meet (rng E) c= { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } ;
hence { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } is Element of S by A6, A5, XBOOLE_0:def 10; :: thesis: verum