let X be set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for F being Finite_Sep_Sequence of S holds F is Finite_Sep_Sequence of COM (S,M)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for F being Finite_Sep_Sequence of S holds F is Finite_Sep_Sequence of COM (S,M)

let M be sigma_Measure of S; :: thesis: for F being Finite_Sep_Sequence of S holds F is Finite_Sep_Sequence of COM (S,M)

let F be Finite_Sep_Sequence of S; :: thesis: F is Finite_Sep_Sequence of COM (S,M)

hence F is Finite_Sep_Sequence of COM (S,M) by FINSEQ_1:def 4; :: thesis: verum

for M being sigma_Measure of S

for F being Finite_Sep_Sequence of S holds F is Finite_Sep_Sequence of COM (S,M)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for F being Finite_Sep_Sequence of S holds F is Finite_Sep_Sequence of COM (S,M)

let M be sigma_Measure of S; :: thesis: for F being Finite_Sep_Sequence of S holds F is Finite_Sep_Sequence of COM (S,M)

let F be Finite_Sep_Sequence of S; :: thesis: F is Finite_Sep_Sequence of COM (S,M)

now :: thesis: for y being object st y in rng F holds

y in COM (S,M)

then
rng F c= COM (S,M)
;y in COM (S,M)

let y be object ; :: thesis: ( y in rng F implies y in COM (S,M) )

assume y in rng F ; :: thesis: y in COM (S,M)

then y is Element of COM (S,M) by Th27;

hence y in COM (S,M) ; :: thesis: verum

end;assume y in rng F ; :: thesis: y in COM (S,M)

then y is Element of COM (S,M) by Th27;

hence y in COM (S,M) ; :: thesis: verum

hence F is Finite_Sep_Sequence of COM (S,M) by FINSEQ_1:def 4; :: thesis: verum