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)

now :: thesis: for y being object st y in rng F holds
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;

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