defpred S₁[ Nat, object ] means ex F being SigmaField of (X . $1) st
( F = S . $1 & $2 is sigma_Measure of F );

A1: now :: thesis: for i being Nat st i in Seg m holds
ex M being object st S₁[i,M]

let i be Nat; :: thesis: ( i in Seg m implies ex M being object st S₁[i,M] )
assume i in Seg m ; :: thesis: ex M being object st S₁[i,M]
then reconsider F = S . i as SigmaField of (X . i) by Def2;
set M = the sigma_Measure of F;
the sigma_Measure of F is sigma_Measure of F ;
hence ex M being object st S₁[i,M] ; :: thesis: verum

end;

consider M being FinSequence such that
A2: ( dom M = Seg m & ( for i being Nat st i in Seg m holds
S₁[i,M . i] ) ) from FINSEQ_1:sch 1(A1);
Seg (len M) = Seg m by A2, FINSEQ_1:def 3;
then reconsider M = M as m -element FinSequence by CARD_1:def 7, FINSEQ_1:6;
take M ; :: thesis: for i being Nat st i in Seg m holds
ex Si being SigmaField of (X . i) st
( Si = S . i & M . i is sigma_Measure of Si )
thus for i being Nat st i in Seg m holds
ex Si being SigmaField of (X . i) st
( Si = S . i & M . i is sigma_Measure of Si ) by A2; :: thesis: verum