let X be set ; :: thesis: for S being semialgebra_of_sets of X
for P being pre-Measure of S ex M being Measure of (Field_generated_by S) st
for A being set st A in Field_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
M . A = Sum (P * F)
let S be semialgebra_of_sets of X; :: thesis: for P being pre-Measure of S ex M being Measure of (Field_generated_by S) st
for A being set st A in Field_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
M . A = Sum (P * F)
let P be pre-Measure of S; :: thesis: ex M being Measure of (Field_generated_by S) st
for A being set st A in Field_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
M . A = Sum (P * F)
defpred S₁[ object , object ] means for F being disjoint_valued FinSequence of S st $1 = Union F holds
$2 = Sum (P * F);
A1: for A being object st A in Field_generated_by S holds
ex p being object st
( p in ExtREAL & S₁[A,p] )

proof

let A be object ; :: thesis: ( A in Field_generated_by S implies ex p being object st
( p in ExtREAL & S₁[A,p] ) )
assume A in Field_generated_by S ; :: thesis: ex p being object st
( p in ExtREAL & S₁[A,p] )
then A in DisUnion S by SRINGS_3:22;
then consider V being Subset of X such that
A3: ( A = V & ex F being disjoint_valued FinSequence of S st V = Union F ) ;
consider F being disjoint_valued FinSequence of S such that
A4: V = Union F by A3;
set p = Sum (P * F);
take Sum (P * F) ; :: thesis: ( Sum (P * F) in ExtREAL & S₁[A, Sum (P * F)] )
thus ( Sum (P * F) in ExtREAL & S₁[A, Sum (P * F)] ) by A3, A4, Th54; :: thesis: verum

end;

consider M being Function of (Field_generated_by S),ExtREAL such that
A5: for A being object st A in Field_generated_by S holds
S₁[A,M . A] from FUNCT_2:sch 1(A1);
A18: for A being Element of Field_generated_by S holds 0 <= M . A

proof

let A be Element of Field_generated_by S; :: thesis: 0 <= M . A
A in Field_generated_by S ;
then A in DisUnion S by SRINGS_3:22;
then consider V being Subset of X such that
A7: ( A = V & ex F being disjoint_valued FinSequence of S st V = Union F ) ;
consider F being disjoint_valued FinSequence of S such that
A8: V = Union F by A7;
consider PF being sequence of ExtREAL such that
A10: ( Sum (P * F) = PF . (len (P * F)) & PF . 0 = 0. & ( for i being Nat st i < len (P * F) holds
PF . (i + 1) = (PF . i) + ((P * F) . (i + 1)) ) ) by EXTREAL1:def 2;
defpred S₂[ Nat] means ( $1 <= len (P * F) implies PF . $1 >= 0 );
A11: S₂[ 0 ] by A10;
A12: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume A13: S₂[i] ; :: thesis: S₂[i + 1]
assume A14: i + 1 <= len (P * F) ; :: thesis: PF . (i + 1) >= 0
then i + 1 in dom (P * F) by NAT_1:11, FINSEQ_3:25;
then (P * F) . (i + 1) = P . (F . (i + 1)) by FUNCT_1:12;
then A17: (P * F) . (i + 1) >= 0 by SUPINF_2:51;
PF . (i + 1) = (PF . i) + ((P * F) . (i + 1)) by A14, A10, NAT_1:13;
hence PF . (i + 1) >= 0 by A13, A14, NAT_1:13, A17; :: thesis: verum

end;

for i being Nat holds S₂[i] from NAT_1:sch 2(A11, A12);
then Sum (P * F) >= 0 by A10;
hence 0 <= M . A by A7, A8, A5; :: thesis: verum

end;

A29: for A, B being Element of Field_generated_by S st A misses B holds
M . (A \/ B) = (M . A) + (M . B)

proof

let A, B be Element of Field_generated_by S; :: thesis: ( A misses B implies M . (A \/ B) = (M . A) + (M . B) )
assume A19: A misses B ; :: thesis: M . (A \/ B) = (M . A) + (M . B)
A in Field_generated_by S ;
then A in DisUnion S by SRINGS_3:22;
then consider V being Subset of X such that
A20: ( A = V & ex F being disjoint_valued FinSequence of S st V = Union F ) ;
consider F being disjoint_valued FinSequence of S such that
A21: V = Union F by A20;
B in Field_generated_by S ;
then B in DisUnion S by SRINGS_3:22;
then consider W being Subset of X such that
A22: ( B = W & ex G being disjoint_valued FinSequence of S st W = Union G ) ;
consider G being disjoint_valued FinSequence of S such that
A23: W = Union G by A22;
set H = F ^ G;
A24: ( A = union (rng F) & B = union (rng G) ) by A20, A21, A22, A23, CARD_3:def 4;
then reconsider H = F ^ G as disjoint_valued FinSequence of S by A19, Th43;
rng H = (rng F) \/ (rng G) by FINSEQ_1:31;
then union (rng H) = (union (rng F)) \/ (union (rng G)) by ZFMISC_1:78;
then A \/ B = Union H by A24, CARD_3:def 4;
then A25: M . (A \/ B) = Sum (P * H) by A5;
A26: ( M . A = Sum (P * F) & M . B = Sum (P * G) ) by A20, A21, A22, A23, A5;
P * F is nonnegative by Th45;
then A27: not -infty in rng (P * F) by SUPINF_2:def 12, SUPINF_2:def 9;
P * G is nonnegative by Th45;
then A28: not -infty in rng (P * G) by SUPINF_2:def 12, SUPINF_2:def 9;
P * H = (P * F) ^ (P * G) by FINSEQOP:9;
hence M . (A \/ B) = (M . A) + (M . B) by A25, A26, A27, A28, EXTREAL1:10; :: thesis: verum

end;

reconsider E = {} as Element of S by SETFAM_1:def 8;
reconsider F = <*E*> as disjoint_valued FinSequence of S ;
rng F = {{}} by FINSEQ_1:38;
then union (rng F) = {} by ZFMISC_1:25;
then Union F = {} by CARD_3:def 4;
then M . {} = Sum (P * F) by A5, FINSUB_1:7;
then M . {} = Sum <*(P . {})*> by FINSEQ_2:35;
then M . {} = P . {} by EXTREAL1:8;
then M . {} = 0 by VALUED_0:def 19;
then reconsider M = M as zeroed nonnegative additive Function of (Field_generated_by S),ExtREAL by A18, A29, VALUED_0:def 19, MEASURE1:def 2, MEASURE1:def 8;
take M ; :: thesis: for A being set st A in Field_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
M . A = Sum (P * F)
thus for A being set st A in Field_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
M . A = Sum (P * F) by A5; :: thesis: verum