:: Construction of Measure from Semialgebra of Sets
:: by Noboru Endou
::
:: Copyright (c) 2015-2019 Association of Mizar Users

theorem Th52: :: MEASURE9:1
for K being Relation st rng K is empty-membered holds
union (rng K) = {}
proof end;

theorem :: MEASURE9:2
for K being Function holds
( rng K is empty-membered iff for x being object holds K . x = {} )
proof end;

definition
let D be set ;
let F be FinSequenceSet of D;
let f be FinSequence of F;
let n be Nat;
:: original: .
redefine func f . n -> FinSequence of D;
correctness
coherence
f . n is FinSequence of D
;
proof end;
end;

definition
let D be set ;
let Y be FinSequenceSet of D;
let F be FinSequence of Y;
func Length F -> FinSequence of NAT means :Def1: :: MEASURE9:def 1
( dom it = dom F & ( for n being Nat st n in dom it holds
it . n = len (F . n) ) );
existence
ex b1 being FinSequence of NAT st
( dom b1 = dom F & ( for n being Nat st n in dom b1 holds
b1 . n = len (F . n) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of NAT st dom b1 = dom F & ( for n being Nat st n in dom b1 holds
b1 . n = len (F . n) ) & dom b2 = dom F & ( for n being Nat st n in dom b2 holds
b2 . n = len (F . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Length MEASURE9:def 1 :
for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for b4 being FinSequence of NAT holds
( b4 = Length F iff ( dom b4 = dom F & ( for n being Nat st n in dom b4 holds
b4 . n = len (F . n) ) ) );

theorem :: MEASURE9:3
for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y st ( for n being Nat st n in dom F holds
F . n = <*> D ) holds
Sum () = 0
proof end;

theorem Th2: :: MEASURE9:4
for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for k being Nat st k < len F holds
Length (F | (k + 1)) = (Length (F | k)) ^ <*(len (F . (k + 1)))*>
proof end;

theorem Th3: :: MEASURE9:5
for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for n being Nat st 1 <= n & n <= Sum () holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) )
proof end;

RFINSEQlm3: for n being Nat
for D being set
for f being FinSequence of D st len f <= n holds
f | n = f

proof end;

RFINSEQ6: for D being set
for f being FinSequence of D
for n, m being Nat st n in dom f & m in Seg n holds
( (f | n) . m = f . m & m in dom f )

proof end;

RFINSEQ8: for D being set
for f being FinSequence of D
for n being Nat holds (f | n) ^ (f /^ n) = f

proof end;

theorem Th4: :: MEASURE9:6
for D being set
for Y being FinSequenceSet of D
for F1, F2 being FinSequence of Y holds Length (F1 ^ F2) = (Length F1) ^ (Length F2)
proof end;

theorem Th5: :: MEASURE9:7
for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for k1, k2 being Nat st k1 <= k2 holds
Sum (Length (F | k1)) <= Sum (Length (F | k2))
proof end;

theorem Th6: :: MEASURE9:8
for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for m1, m2, k1, k2 being Nat st 1 <= m1 & 1 <= m2 & m1 + (Sum (Length (F | k1))) = m2 + (Sum (Length (F | k2))) & m1 + (Sum (Length (F | k1))) <= Sum (Length (F | (k1 + 1))) & m2 + (Sum (Length (F | k2))) <= Sum (Length (F | (k2 + 1))) holds
( m1 = m2 & k1 = k2 )
proof end;

definition
let D be non empty set ;
let Y be FinSequenceSet of D;
let F be FinSequence of Y;
func joined_FinSeq F -> FinSequence of D means :Def2: :: MEASURE9:def 2
( len it = Sum () & ( for n being Nat st n in dom it holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & it . n = (F . (k + 1)) . m ) ) );
existence
ex b1 being FinSequence of D st
( len b1 = Sum () & ( for n being Nat st n in dom b1 holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & b1 . n = (F . (k + 1)) . m ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of D st len b1 = Sum () & ( for n being Nat st n in dom b1 holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & b1 . n = (F . (k + 1)) . m ) ) & len b2 = Sum () & ( for n being Nat st n in dom b2 holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & b2 . n = (F . (k + 1)) . m ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines joined_FinSeq MEASURE9:def 2 :
for D being non empty set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for b4 being FinSequence of D holds
( b4 = joined_FinSeq F iff ( len b4 = Sum () & ( for n being Nat st n in dom b4 holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & b4 . n = (F . (k + 1)) . m ) ) ) );

definition
let D be set ;
let Y be FinSequenceSet of D;
let s be sequence of Y;
func Length s -> sequence of NAT means :Def3: :: MEASURE9:def 3
for n being Nat holds it . n = len (s . n);
existence
ex b1 being sequence of NAT st
for n being Nat holds b1 . n = len (s . n)
proof end;
uniqueness
for b1, b2 being sequence of NAT st ( for n being Nat holds b1 . n = len (s . n) ) & ( for n being Nat holds b2 . n = len (s . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Length MEASURE9:def 3 :
for D being set
for Y being FinSequenceSet of D
for s being sequence of Y
for b4 being sequence of NAT holds
( b4 = Length s iff for n being Nat holds b4 . n = len (s . n) );

definition
let s be sequence of NAT;
:: original: Partial_Sums
redefine func Partial_Sums s -> sequence of NAT;
correctness
coherence ;
proof end;
end;

registration
let D be non empty set ;
existence
ex b1 being FinSequenceSet of D st
( not b1 is empty & b1 is with_non-empty_element )
proof end;
end;

theorem Th7: :: MEASURE9:9
for D being non empty set
for Y being non empty with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y
for n being Nat holds
( len (s . n) >= 1 & n < () . n & () . n < () . (n + 1) )
proof end;

theorem Th8: :: MEASURE9:10
for D being non empty set
for Y being non empty with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y
for n being Nat ex k, m being Nat st
( m in dom (s . k) & (((() . k) - (len (s . k))) + m) - 1 = n )
proof end;

theorem Th9: :: MEASURE9:11
for D being non empty set
for Y being non empty with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y holds Partial_Sums () is increasing
proof end;

theorem Th10: :: MEASURE9:12
for D being non empty set
for Y being non empty with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y
for m1, m2, k1, k2 being Nat st m1 in dom (s . k1) & m2 in dom (s . k2) & ((() . k1) - (len (s . k1))) + m1 = ((() . k2) - (len (s . k2))) + m2 holds
( m1 = m2 & k1 = k2 )
proof end;

theorem Th11: :: MEASURE9:13
for D being non empty set
for Y being with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y ex N being increasing sequence of NAT st
for k being Nat holds N . k = (() . k) - 1
proof end;

definition
let D be non empty set ;
let Y be with_non-empty_element FinSequenceSet of D;
let s be non-empty sequence of Y;
func joined_seq s -> sequence of D means :Def4: :: MEASURE9:def 4
for n being Nat ex k, m being Nat st
( m in dom (s . k) & (((() . k) - (len (s . k))) + m) - 1 = n & it . n = (s . k) . m );
existence
ex b1 being sequence of D st
for n being Nat ex k, m being Nat st
( m in dom (s . k) & (((() . k) - (len (s . k))) + m) - 1 = n & b1 . n = (s . k) . m )
proof end;
uniqueness
for b1, b2 being sequence of D st ( for n being Nat ex k, m being Nat st
( m in dom (s . k) & (((() . k) - (len (s . k))) + m) - 1 = n & b1 . n = (s . k) . m ) ) & ( for n being Nat ex k, m being Nat st
( m in dom (s . k) & (((() . k) - (len (s . k))) + m) - 1 = n & b2 . n = (s . k) . m ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines joined_seq MEASURE9:def 4 :
for D being non empty set
for Y being with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y
for b4 being sequence of D holds
( b4 = joined_seq s iff for n being Nat ex k, m being Nat st
( m in dom (s . k) & (((() . k) - (len (s . k))) + m) - 1 = n & b4 . n = (s . k) . m ) );

theorem :: MEASURE9:14
for D being non empty set
for Y being with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y
for s1 being sequence of D st ( for n being Nat holds s1 . n = () . ((() . n) - 1) ) holds
s1 is subsequence of joined_seq s
proof end;

theorem Th13: :: MEASURE9:15
for D being non empty set
for Y being with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y
for k, m being Nat st m in dom (s . k) holds
ex n being Nat st
( n = (((() . k) - (len (s . k))) + m) - 1 & () . n = (s . k) . m )
proof end;

theorem Th14: :: MEASURE9:16
for D being non empty set
for Y being FinSequenceSet of D
for F being FinSequence of Y st ( for n, m being Nat st n <> m holds
union (rng (F . n)) misses union (rng (F . m)) ) & ( for n being Nat holds F . n is disjoint_valued ) holds
joined_FinSeq F is disjoint_valued
proof end;

theorem Th15: :: MEASURE9:17
for D being non empty set
for Y being FinSequenceSet of D
for F being FinSequence of Y holds rng () = union { (rng (F . n)) where n is Nat : n in dom F }
proof end;

definition
let x be ext-real number ;
:: original: <*
redefine func <*x*> -> FinSequence of ExtREAL ;
coherence
proof end;
end;

definition
let e be FinSequence of ExtREAL * ;
func Sum e -> FinSequence of ExtREAL means :Def5: :: MEASURE9:def 5
( len it = len e & ( for k being Nat st k in dom it holds
it . k = Sum (e . k) ) );
existence
ex b1 being FinSequence of ExtREAL st
( len b1 = len e & ( for k being Nat st k in dom b1 holds
b1 . k = Sum (e . k) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of ExtREAL st len b1 = len e & ( for k being Nat st k in dom b1 holds
b1 . k = Sum (e . k) ) & len b2 = len e & ( for k being Nat st k in dom b2 holds
b2 . k = Sum (e . k) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Sum MEASURE9:def 5 :
for e being FinSequence of ExtREAL *
for b2 being FinSequence of ExtREAL holds
( b2 = Sum e iff ( len b2 = len e & ( for k being Nat st k in dom b2 holds
b2 . k = Sum (e . k) ) ) );

definition
let M be Matrix of ExtREAL;
func SumAll M -> Element of ExtREAL equals :: MEASURE9:def 6
Sum (Sum M);
coherence
Sum (Sum M) is Element of ExtREAL
;
end;

:: deftheorem defines SumAll MEASURE9:def 6 :
for M being Matrix of ExtREAL holds SumAll M = Sum (Sum M);

theorem Th16: :: MEASURE9:18
for M being Matrix of ExtREAL holds
( len (Sum M) = len M & ( for i being Nat st i in Seg (len M) holds
(Sum M) . i = Sum (Line (M,i)) ) )
proof end;

theorem Th17: :: MEASURE9:19
for F being FinSequence of ExtREAL st ( for i being Nat st i in dom F holds
F . i <> -infty ) holds
Sum F <> -infty
proof end;

theorem Th18: :: MEASURE9:20
for F, G, H being FinSequence of ExtREAL st not -infty in rng F & not -infty in rng G & dom F = dom G & H = F + G holds
Sum H = (Sum F) + (Sum G)
proof end;

theorem Th19: :: MEASURE9:21
for r being R_eal
for F being FinSequence of ExtREAL holds Sum (F ^ <*r*>) = (Sum F) + r
proof end;

theorem Th20: :: MEASURE9:22
for r being R_eal
for i being Nat st r is real holds
Sum (i |-> r) = i * r
proof end;

theorem Th21: :: MEASURE9:23
for M being Matrix of ExtREAL st len M = 0 holds
SumAll M = 0
proof end;

theorem Th22: :: MEASURE9:24
for m being Nat
for M being Matrix of m, 0 ,ExtREAL holds SumAll M = 0
proof end;

theorem Th23: :: MEASURE9:25
for n, m, k being Nat
for M1 being Matrix of n,k,ExtREAL
for M2 being Matrix of m,k,ExtREAL holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
proof end;

theorem Th24: :: MEASURE9:26
for M1, M2 being Matrix of ExtREAL st ( for i being Nat st i in dom M1 holds
not -infty in rng (M1 . i) ) & ( for i being Nat st i in dom M2 holds
not -infty in rng (M2 . i) ) holds
(Sum M1) + (Sum M2) = Sum (M1 ^^ M2)
proof end;

theorem Th25: :: MEASURE9:27
for M1, M2 being Matrix of ExtREAL st len M1 = len M2 & ( for i being Nat st i in dom M1 holds
not -infty in rng (M1 . i) ) & ( for i being Nat st i in dom M2 holds
not -infty in rng (M2 . i) ) holds
(SumAll M1) + (SumAll M2) = SumAll (M1 ^^ M2)
proof end;

theorem Th26: :: MEASURE9:28
for p being FinSequence of ExtREAL st not -infty in rng p holds
SumAll <*p*> = SumAll ()
proof end;

theorem Th27: :: MEASURE9:29
for p being ext-real number
for M being Matrix of ExtREAL st ( for i being Nat st i in dom M holds
not p in rng (M . i) ) holds
for j being Nat st j in dom (M @) holds
not p in rng ((M @) . j)
proof end;

theorem Th28: :: MEASURE9:30
for M being Matrix of ExtREAL st ( for i being Nat st i in dom M holds
not -infty in rng (M . i) ) holds
SumAll M = SumAll (M @)
proof end;

registration
let x be object ;
correctness
coherence ;
proof end;
end;

theorem :: MEASURE9:31
for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for F being FinSequence of S
for G being Element of S ex H being disjoint_valued FinSequence of S st G \ () = Union H
proof end;

registration
let X be set ;
let P be with_empty_element cap-closed semi-diff-closed Subset-Family of X;
existence
ex b1 being sequence of P st b1 is disjoint_valued
proof end;
end;

LM: for X being set
for P being non empty Subset-Family of X holds
( P --> 0. is V224() & P --> 0. is additive & P --> 0. is zeroed )

proof end;

registration
let X be set ;
let P be non empty Subset-Family of X;
existence
ex b1 being Function of P,ExtREAL st
( b1 is V224() & b1 is additive & b1 is zeroed )
proof end;
end;

registration
let X be set ;
let P be with_empty_element Subset-Family of X;
existence
ex b1 being Function of NAT,P st b1 is disjoint_valued
proof end;
end;

definition
let X be set ;
let P be with_empty_element Subset-Family of X;
mode pre-Measure of P -> zeroed V224() Function of P,ExtREAL means :Def8: :: MEASURE9:def 7
( ( for F being disjoint_valued FinSequence of P st Union F in P holds
it . () = Sum (it * F) ) & ( for K being disjoint_valued Function of NAT,P st Union K in P holds
it . () <= SUM (it * K) ) );
existence
ex b1 being zeroed V224() Function of P,ExtREAL st
( ( for F being disjoint_valued FinSequence of P st Union F in P holds
b1 . () = Sum (b1 * F) ) & ( for K being disjoint_valued Function of NAT,P st Union K in P holds
b1 . () <= SUM (b1 * K) ) )
proof end;
end;

:: deftheorem Def8 defines pre-Measure MEASURE9:def 7 :
for X being set
for P being with_empty_element Subset-Family of X
for b3 being zeroed V224() Function of P,ExtREAL holds
( b3 is pre-Measure of P iff ( ( for F being disjoint_valued FinSequence of P st Union F in P holds
b3 . () = Sum (b3 * F) ) & ( for K being disjoint_valued Function of NAT,P st Union K in P holds
b3 . () <= SUM (b3 * K) ) ) );

theorem :: MEASURE9:32
for X being with_empty_element set
for F being FinSequence of X ex G being Function of NAT,X st
( ( for i being Nat holds F . i = G . i ) & Union F = Union G )
proof end;

theorem :: MEASURE9:33
for X being non empty set
for F being FinSequence of X
for G being Function of NAT,X st ( for i being Nat holds F . i = G . i ) holds
( F is disjoint_valued iff G is disjoint_valued )
proof end;

theorem :: MEASURE9:34
for F being FinSequence of ExtREAL
for G being ExtREAL_sequence st ( for i being Nat holds F . i = G . i ) holds
( F is nonnegative iff G is V224() )
proof end;

LL1: ( is nonnegative & is V251() )
proof end;

LL2: ( is nonpositive & is V252() )
proof end;

registration
existence
ex b1 being FinSequence of ExtREAL st b1 is nonnegative
by LL1;
existence
not for b1 being FinSequence of ExtREAL holds b1 is V251()
by LL1;
existence
ex b1 being FinSequence of ExtREAL st b1 is nonpositive
by LL2;
existence
not for b1 being FinSequence of ExtREAL holds b1 is V252()
by LL2;
cluster nonnegative -> V251() for FinSequence of ExtREAL ;
correctness
coherence
for b1 being FinSequence of ExtREAL st b1 is nonnegative holds
b1 is V251()
;
;
cluster nonpositive -> V252() for FinSequence of ExtREAL ;
correctness
coherence
for b1 being FinSequence of ExtREAL st b1 is nonpositive holds
b1 is V252()
;
;
end;

registration
let X, Y be non empty set ;
let F be V251() Function of Y,ExtREAL;
let G be Function of X,Y;
cluster G * F -> V251() for Function of X,ExtREAL;
correctness
coherence
for b1 being Function of X,ExtREAL st b1 = F * G holds
b1 is without-infty
;
proof end;
end;

registration
let X, Y be non empty set ;
let F be V224() Function of Y,ExtREAL;
let G be Function of X,Y;
cluster G * F -> V224() for Function of X,ExtREAL;
correctness
coherence
for b1 being Function of X,ExtREAL st b1 = F * G holds
b1 is nonnegative
;
by MEASURE1:25;
end;

theorem Th33: :: MEASURE9:35
for a being R_eal holds Sum <*a*> = a
proof end;

theorem Th34: :: MEASURE9:36
for F being FinSequence of ExtREAL
for k being Nat holds
( ( F is V251() implies F | k is V251() ) & ( F is V252() implies F | k is V252() ) )
proof end;

theorem Th35: :: MEASURE9:37
for F being V251() FinSequence of ExtREAL
for G being ExtREAL_sequence st ( for i being Nat holds F . i = G . i ) holds
for i being Nat holds Sum (F | i) = () . i
proof end;

theorem :: MEASURE9:38
for F being V251() FinSequence of ExtREAL
for G being ExtREAL_sequence st ( for i being Nat holds F . i = G . i ) holds
( G is summable & Sum F = Sum G )
proof end;

theorem :: MEASURE9:39
for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for F being disjoint_valued FinSequence of S
for R being non empty preBoolean Subset-Family of X st S c= R & Union F in R holds
for i being Nat holds Union (F | i) in R
proof end;

theorem :: MEASURE9:40
for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for P being pre-Measure of S
for F1, F2 being disjoint_valued FinSequence of S st Union F1 in S & Union F1 = Union F2 holds
P . (Union F1) = P . (Union F2) ;

theorem FStoMAT1: :: MEASURE9:41
for S being non empty cap-closed set
for F1, F2 being FinSequence of S ex Mx being Matrix of len F1, len F2,S st
for i, j being Nat st [i,j] in Indices Mx holds
Mx * (i,j) = (F1 . i) /\ (F2 . j)
proof end;

theorem Th40: :: MEASURE9:42
for X being set
for S being with_empty_element cap-closed Subset-Family of X
for F1, F2 being non empty disjoint_valued FinSequence of S
for P being zeroed V224() Function of S,ExtREAL
for Mx being Matrix of len F1, len F2,ExtREAL st Union F1 = Union F2 & ( for i, j being Nat st [i,j] in Indices Mx holds
Mx * (i,j) = P . ((F1 . i) /\ (F2 . j)) ) & ( for F being disjoint_valued FinSequence of S st Union F in S holds
P . () = Sum (P * F) ) holds
( ( for i being Nat st i <= len (P * F1) holds
(P * F1) . i = (Sum Mx) . i ) & Sum (P * F1) = SumAll Mx )
proof end;

theorem Th41: :: MEASURE9:43
for X being set
for S being with_empty_element cap-closed Subset-Family of X
for F1, F2 being non empty disjoint_valued FinSequence of S
for P being zeroed V224() Function of S,ExtREAL
for Mx being Matrix of len F1, len F2,ExtREAL st Union F1 = Union F2 & ( for i, j being Nat st [i,j] in Indices Mx holds
Mx * (i,j) = P . ((F1 . i) /\ (F2 . j)) ) & ( for F being disjoint_valued FinSequence of S st Union F in S holds
P . () = Sum (P * F) ) holds
( ( for i being Nat st i <= len (P * F2) holds
(P * F2) . i = (Sum (Mx @)) . i ) & Sum (P * F2) = SumAll (Mx @) )
proof end;

theorem Th42: :: MEASURE9:44
for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for P being pre-Measure of S
for A being set st A in Ring_generated_by S holds
for F1, F2 being disjoint_valued FinSequence of S st A = Union F1 & A = Union F2 holds
Sum (P * F1) = Sum (P * F2)
proof end;

theorem Th43: :: MEASURE9:45
for f1, f2 being FinSequence st f1 is disjoint_valued & f2 is disjoint_valued & union (rng f1) misses union (rng f2) holds
f1 ^ f2 is disjoint_valued
proof end;

theorem :: MEASURE9:46
for X being set
for P being with_empty_element semi-diff-closed Subset-Family of X
for M being pre-Measure of P
for A, B being set st A in P & B in P & A \ B in P & B c= A holds
M . A >= M . B
proof end;

theorem Th45: :: MEASURE9:47
for Y, S being non empty set
for F being PartFunc of Y,S
for M being Function of S,ExtREAL st M is V224() holds
M * F is nonnegative
proof end;

theorem Th46: :: MEASURE9:48
for X being 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 V224() additive Function of ,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)
proof end;

theorem :: MEASURE9:49
for X, Y being set
for F, G being Function of NAT,(bool X) st ( for i being Nat holds G . i = (F . i) /\ Y ) & Union F = Y holds
Union G = Union F
proof end;

theorem :: MEASURE9:50
for X being 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 Function of ,ExtREAL st
( M . {} = 0 & ( for K being disjoint_valued FinSequence of S st Union K in Ring_generated_by S holds
M . () = Sum (P * K) ) )
proof end;

theorem :: MEASURE9:51
for X, Z being set
for P being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for K being disjoint_valued Function of NAT, st Z = { [n,F] where n is Nat, F is disjoint_valued FinSequence of P : ( Union F = K . n & ( K . n = {} implies F = ) ) } holds
( proj2 Z is FinSequenceSet of P & ( for x being object holds
( x in rng K iff ex F being FinSequence of P st
( F in proj2 Z & Union F = x ) ) ) & proj2 Z is with_non-empty_elements )
proof end;

theorem :: MEASURE9:52
for X being set
for P being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for K being disjoint_valued Function of NAT, st rng K is with_non-empty_element holds
ex Y being non empty FinSequenceSet of P st
( Y = { F where F is disjoint_valued FinSequence of P : ( Union F in rng K & F <> {} ) } & Y is with_non-empty_elements )
proof end;

theorem Th51: :: MEASURE9:53
for X, Z being set
for P being semialgebra_of_sets of X
for K being disjoint_valued Function of NAT, st Z = { [n,F] where n is Nat, F is disjoint_valued FinSequence of P : ( Union F = K . n & ( K . n = {} implies F = ) ) } holds
( proj2 Z is FinSequenceSet of P & ( for x being object holds
( x in rng K iff ex F being FinSequence of P st
( F in proj2 Z & Union F = x ) ) ) & proj2 Z is with_non-empty_elements )
proof end;

theorem Th54: :: MEASURE9:54
for X being set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for A being set
for F1, F2 being disjoint_valued FinSequence of S st A = Union F1 & A = Union F2 holds
Sum (P * F1) = Sum (P * F2)
proof end;

theorem Th55: :: MEASURE9:55
for X being set
for S being semialgebra_of_sets of X
for P being pre-Measure of S ex M being Measure of 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)
proof end;

theorem :: MEASURE9:56
for F being ExtREAL_sequence
for n being Nat
for a being R_eal st ( for k being Nat holds F . k = a ) holds
() . n = a * (n + 1)
proof end;

theorem Th57: :: MEASURE9:57
for X being non empty set
for F being sequence of X
for n being Nat holds rng (F | (Segm (n + 1))) = (rng (F | (Segm n))) \/ {(F . n)}
proof end;

theorem Th58: :: MEASURE9:58
for X being set
for S being Field_Subset of X
for M being Measure of S
for F being Sep_Sequence of S
for n being Nat holds
( union (rng (F | (Segm (n + 1)))) in S & (Partial_Sums (M * F)) . n = M . (union (rng (F | (Segm (n + 1))))) )
proof end;

theorem Th59: :: MEASURE9:59
for X being set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for M being Measure of 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) ) holds
proof end;

definition
let X be set ;
let S be semialgebra_of_sets of X;
let P be pre-Measure of S;
mode induced_Measure of S,P -> Measure of means :Def9: :: MEASURE9:def 8
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
it . A = Sum (P * F);
existence
ex b1 being Measure of 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
b1 . A = Sum (P * F)
by Th55;
end;

:: deftheorem Def9 defines induced_Measure MEASURE9:def 8 :
for X being set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for b4 being Measure of holds
( b4 is induced_Measure of S,P iff 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
b4 . A = Sum (P * F) );

theorem Th60: :: MEASURE9:60
for X being set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for M being induced_Measure of S,P holds M is completely-additive
proof end;

theorem Th61: :: MEASURE9:61
for X being non empty set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for M being induced_Measure of S,P holds (sigma_Meas ()) | () is sigma_Measure of ()
proof end;

definition
let X be non empty set ;
let S be semialgebra_of_sets of X;
let P be pre-Measure of S;
let M be induced_Measure of S,P;
mode induced_sigma_Measure of S,M -> sigma_Measure of () means :Def10: :: MEASURE9:def 9
it = (sigma_Meas ()) | ();
existence
ex b1 being sigma_Measure of () st b1 = (sigma_Meas ()) | ()
proof end;
end;

:: deftheorem Def10 defines induced_sigma_Measure MEASURE9:def 9 :
for X being non empty set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for M being induced_Measure of S,P
for b5 being sigma_Measure of () holds
( b5 is induced_sigma_Measure of S,M iff b5 = (sigma_Meas ()) | () );

theorem :: MEASURE9:62
for X being non empty set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for m being induced_Measure of S,P
for M being induced_sigma_Measure of S,m holds M is_extension_of m
proof end;