let X be set ; for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for P being pre-Measure of S ex M being zeroed nonnegative additive Function of (Ring_generated_by S),ExtREAL st
for A being set st A in Ring_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 with_empty_element cap-closed semi-diff-closed Subset-Family of X; for P being pre-Measure of S ex M being zeroed nonnegative additive Function of (Ring_generated_by S),ExtREAL st
for A being set st A in Ring_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; ex M being zeroed nonnegative additive Function of (Ring_generated_by S),ExtREAL st
for A being set st A in Ring_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
M . A = Sum (P * F)
defpred S1[ 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 Ring_generated_by S holds
ex p being object st
( p in ExtREAL & S1[A,p] )
consider M being Function of (Ring_generated_by S),ExtREAL such that
A5:
for A being object st A in Ring_generated_by S holds
S1[A,M . A]
from FUNCT_2:sch 1(A1);
A18:
for A being Element of Ring_generated_by S holds 0 <= M . A
for A, B being Element of Ring_generated_by S st A misses B & A \/ B in Ring_generated_by S holds
M . (A \/ B) = (M . A) + (M . B)
proof
let A,
B be
Element of
Ring_generated_by S;
( A misses B & A \/ B in Ring_generated_by S implies M . (A \/ B) = (M . A) + (M . B) )
assume A19:
(
A misses B &
A \/ B in Ring_generated_by S )
;
M . (A \/ B) = (M . A) + (M . B)
A in Ring_generated_by S
;
then
A in DisUnion S
by SRINGS_3:18;
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 Ring_generated_by S
;
then
B in DisUnion S
by SRINGS_3:18;
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 9, SUPINF_2:def 12;
P * G is
nonnegative
by Th45;
then A28:
not
-infty in rng (P * G)
by SUPINF_2:def 9, SUPINF_2:def 12;
P * H = (P * F) ^ (P * G)
by FINSEQOP:9;
hence
M . (A \/ B) = (M . A) + (M . B)
by A25, A26, A27, A28, EXTREAL1:10;
verum
end;
then A29:
M is additive
by MEASURE1:def 3;
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 (Ring_generated_by S),ExtREAL by A18, A29, VALUED_0:def 19, MEASURE1:def 2;
take
M
; for A being set st A in Ring_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 Ring_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
M . A = Sum (P * F)
by A5; verum