defpred S1[ Nat, object ] means ex F being Field_Subset of (X . $1) st
( F = S . $1 & $2 is Measure of F );
A0:
now for i being Nat st i in Seg n holds
ex M being object st S1[i,M]let i be
Nat;
( i in Seg n implies ex M being object st S1[i,M] )assume
i in Seg n
;
ex M being object st S1[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)
( ( 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
F,
ExtREAL
by A1, VALUED_0:def 19, MEASURE1:def 8, SUPINF_2:39;
hence
ex
M being
object st
S1[
i,
M]
;
verum end;
consider M being FinSequence such that
A4:
( dom M = Seg n & ( for i being Nat st i in Seg n holds
S1[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
; 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; verum