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

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

let i be Nat; :: thesis: ( i in Seg n implies ex M being object st S₁[i,M] )
assume i in Seg n ; :: thesis: ex M being object st S₁[i,M]
then reconsider F = S . i as Field_Subset of (X . i) by Def3;
reconsider M = F --> 0. as Function of F,ExtREAL ;
A1: for A, B being Element of F st A misses B holds
M . (A \/ B) = (M . A) + (M . B)

proof

let A, B be Element of F; :: thesis: ( A misses B implies M . (A \/ B) = (M . A) + (M . B) )
assume A misses B ; :: thesis: M . (A \/ B) = (M . A) + (M . B)
A2: ( M . A = 0. & M . B = 0. ) by FUNCOP_1:7;
reconsider A = A, B = B as Element of S . i ;
0. = (M . A) + (M . B) by A2;
hence M . (A \/ B) = (M . A) + (M . B) by FUNCOP_1:7; :: thesis: verum

end;

( ( for x being Element of S . i holds 0. <= M . x ) & M . {} = 0. ) by FUNCOP_1:7, PROB_1:4;
then M is zeroed nonnegative additive Function of F,ExtREAL by A1, VALUED_0:def 19, MEASURE1:def 8, SUPINF_2:39;
hence ex M being object st S₁[i,M] ; :: thesis: verum

end;

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