defpred S₁[ Nat, object ] means $2 is Measure of (S . $1);

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]
reconsider M = (S . i) --> 0. as Function of (S . i),ExtREAL ;
A1: for A, B being Element of S . i st A misses B holds
M . (A \/ B) = (M . A) + (M . B)

proof

let A, B be Element of S . i; :: 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 set ;
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 V161() additive Function of (S . i),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
M . i is Measure of (S . i)
thus for i being Nat st i in Seg n holds
M . i is Measure of (S . i) by A4; :: thesis: verum