:: by Noboru Endou

::

:: Received August 14, 2015

:: Copyright (c) 2015-2018 Association of Mizar Users

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;

end;
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;

definition

let D be set ;

let Y be FinSequenceSet of D;

let F be FinSequence of Y;

ex b_{1} being FinSequence of NAT st

( dom b_{1} = dom F & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = len (F . n) ) )

for b_{1}, b_{2} being FinSequence of NAT st dom b_{1} = dom F & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = len (F . n) ) & dom b_{2} = dom F & ( for n being Nat st n in dom b_{2} holds

b_{2} . n = len (F . n) ) holds

b_{1} = b_{2}

end;
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 ( dom it = dom F & ( for n being Nat st n in dom it holds

it . n = len (F . n) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{4} being FinSequence of NAT holds

( b_{4} = Length F iff ( dom b_{4} = dom F & ( for n being Nat st n in dom b_{4} holds

b_{4} . n = len (F . n) ) ) );

for D being set

for Y being FinSequenceSet of D

for F being FinSequence of Y

for b

( b

b

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 (Length F) = 0

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 (Length F) = 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)))*>

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 (Length F) 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))) )

for Y being FinSequenceSet of D

for F being FinSequence of Y

for n being Nat st 1 <= n & n <= Sum (Length F) 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)

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))

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 )

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;

ex b_{1} being FinSequence of D st

( len b_{1} = Sum (Length F) & ( for n being Nat st n in dom b_{1} 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))) & b_{1} . n = (F . (k + 1)) . m ) ) )

for b_{1}, b_{2} being FinSequence of D st len b_{1} = Sum (Length F) & ( for n being Nat st n in dom b_{1} 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))) & b_{1} . n = (F . (k + 1)) . m ) ) & len b_{2} = Sum (Length F) & ( for n being Nat st n in dom b_{2} 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))) & b_{2} . n = (F . (k + 1)) . m ) ) holds

b_{1} = b_{2}

end;
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 (Length F) & ( 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 ( len it = Sum (Length F) & ( 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 ) ) );

ex b

( len b

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))) & b

proof end;

uniqueness for b

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))) & b

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))) & b

b

proof 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 b_{4} being FinSequence of D holds

( b_{4} = joined_FinSeq F iff ( len b_{4} = Sum (Length F) & ( for n being Nat st n in dom b_{4} 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))) & b_{4} . n = (F . (k + 1)) . m ) ) ) );

for D being non empty set

for Y being FinSequenceSet of D

for F being FinSequence of Y

for b

( b

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))) & b

definition

let D be set ;

let Y be FinSequenceSet of D;

let s be sequence of Y;

ex b_{1} being sequence of NAT st

for n being Nat holds b_{1} . n = len (s . n)

for b_{1}, b_{2} being sequence of NAT st ( for n being Nat holds b_{1} . n = len (s . n) ) & ( for n being Nat holds b_{2} . n = len (s . n) ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = len (s . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being sequence of NAT holds

( b_{4} = Length s iff for n being Nat holds b_{4} . n = len (s . n) );

for D being set

for Y being FinSequenceSet of D

for s being sequence of Y

for b

( b

definition

let s be sequence of NAT;

:: original: Partial_Sums

redefine func Partial_Sums s -> sequence of NAT;

correctness

coherence

Partial_Sums s is sequence of NAT;

end;
:: original: Partial_Sums

redefine func Partial_Sums s -> sequence of NAT;

correctness

coherence

Partial_Sums s is sequence of NAT;

proof end;

registration

let D be non empty set ;

existence

ex b_{1} being FinSequenceSet of D st

( not b_{1} is empty & b_{1} is with_non-empty_element )

end;
existence

ex b

( not b

proof 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 < (Partial_Sums (Length s)) . n & (Partial_Sums (Length s)) . n < (Partial_Sums (Length s)) . (n + 1) )

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 < (Partial_Sums (Length s)) . n & (Partial_Sums (Length s)) . n < (Partial_Sums (Length s)) . (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) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n )

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) & ((((Partial_Sums (Length s)) . 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 (Length s) is increasing

for Y being non empty with_non-empty_element FinSequenceSet of D

for s being non-empty sequence of Y holds Partial_Sums (Length s) 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) & (((Partial_Sums (Length s)) . k1) - (len (s . k1))) + m1 = (((Partial_Sums (Length s)) . k2) - (len (s . k2))) + m2 holds

( m1 = m2 & k1 = k2 )

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) & (((Partial_Sums (Length s)) . k1) - (len (s . k1))) + m1 = (((Partial_Sums (Length s)) . 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 = ((Partial_Sums (Length s)) . k) - 1

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 = ((Partial_Sums (Length s)) . 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;

ex b_{1} being sequence of D st

for n being Nat ex k, m being Nat st

( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & b_{1} . n = (s . k) . m )

for b_{1}, b_{2} being sequence of D st ( for n being Nat ex k, m being Nat st

( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & b_{1} . n = (s . k) . m ) ) & ( for n being Nat ex k, m being Nat st

( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & b_{2} . n = (s . k) . m ) ) holds

b_{1} = b_{2}

end;
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) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & it . n = (s . k) . m );

existence for n being Nat ex k, m being Nat st

( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & it . n = (s . k) . m );

ex b

for n being Nat ex k, m being Nat st

( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & b

proof end;

uniqueness for b

( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & b

( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & b

b

proof 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 b_{4} being sequence of D holds

( b_{4} = joined_seq s iff for n being Nat ex k, m being Nat st

( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & b_{4} . n = (s . k) . m ) );

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 b

( b

( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & b

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 = (joined_seq s) . (((Partial_Sums (Length s)) . n) - 1) ) holds

s1 is subsequence of joined_seq s

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 = (joined_seq s) . (((Partial_Sums (Length s)) . 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 = ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 & (joined_seq s) . n = (s . k) . m )

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 = ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 & (joined_seq s) . 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

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 (joined_FinSeq F) = union { (rng (F . n)) where n is Nat : n in dom F }

for Y being FinSequenceSet of D

for F being FinSequence of Y holds rng (joined_FinSeq F) = 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

<*x*> is FinSequence of ExtREAL

end;
:: original: <*

redefine func <*x*> -> FinSequence of ExtREAL ;

coherence

<*x*> is FinSequence of ExtREAL

proof end;

definition

let e be FinSequence of ExtREAL * ;

ex b_{1} being FinSequence of ExtREAL st

( len b_{1} = len e & ( for k being Nat st k in dom b_{1} holds

b_{1} . k = Sum (e . k) ) )

for b_{1}, b_{2} being FinSequence of ExtREAL st len b_{1} = len e & ( for k being Nat st k in dom b_{1} holds

b_{1} . k = Sum (e . k) ) & len b_{2} = len e & ( for k being Nat st k in dom b_{2} holds

b_{2} . k = Sum (e . k) ) holds

b_{1} = b_{2}

end;
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 ( len it = len e & ( for k being Nat st k in dom it holds

it . k = Sum (e . k) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines Sum MEASURE9:def 5 :

for e being FinSequence of ExtREAL *

for b_{2} being FinSequence of ExtREAL holds

( b_{2} = Sum e iff ( len b_{2} = len e & ( for k being Nat st k in dom b_{2} holds

b_{2} . k = Sum (e . k) ) ) );

for e being FinSequence of ExtREAL *

for b

( b

b

:: deftheorem defines SumAll MEASURE9:def 6 :

for M being Matrix of ExtREAL holds SumAll M = Sum (Sum M);

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)) ) )

( 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

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)

Sum H = (Sum F) + (Sum G)

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)

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)

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)

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 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)

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 @)

not -infty in rng (M . i) ) holds

SumAll M = SumAll (M @)

proof 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 F) = Union H

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 F) = Union H

proof end;

registration

let X be set ;

let P be with_empty_element cap-closed semi-diff-closed Subset-Family of X;

ex b_{1} being sequence of P st b_{1} is disjoint_valued

end;
let P be with_empty_element cap-closed semi-diff-closed Subset-Family of X;

cluster Relation-like omega -defined P -valued non empty Function-like total V31( omega ,P) disjoint_valued for sequence of ;

existence ex b

proof 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;

ex b_{1} being Function of P,ExtREAL st

( b_{1} is V224() & b_{1} is additive & b_{1} is zeroed )

end;
let P be non empty Subset-Family of X;

cluster Relation-like P -defined ExtREAL -valued non empty Function-like total V31(P, ExtREAL ) ext-real-valued zeroed V224() additive for Function of ,;

existence ex b

( b

proof end;

registration

let X be set ;

let P be with_empty_element Subset-Family of X;

ex b_{1} being Function of NAT,P st b_{1} is disjoint_valued

end;
let P be with_empty_element Subset-Family of X;

cluster Relation-like NAT -defined P -valued non empty Function-like total V31( NAT ,P) disjoint_valued for Function of ,;

existence ex b

proof end;

definition

let X be set ;

let P be with_empty_element Subset-Family of X;

ex b_{1} being zeroed V224() Function of P,ExtREAL st

( ( for F being disjoint_valued FinSequence of P st Union F in P holds

b_{1} . (Union F) = Sum (b_{1} * F) ) & ( for K being disjoint_valued Function of NAT,P st Union K in P holds

b_{1} . (Union K) <= SUM (b_{1} * K) ) )

end;
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 . (Union F) = Sum (it * F) ) & ( for K being disjoint_valued Function of NAT,P st Union K in P holds

it . (Union K) <= SUM (it * K) ) );

existence ( ( for F being disjoint_valued FinSequence of P st Union F in P holds

it . (Union F) = Sum (it * F) ) & ( for K being disjoint_valued Function of NAT,P st Union K in P holds

it . (Union K) <= SUM (it * K) ) );

ex b

( ( for F being disjoint_valued FinSequence of P st Union F in P holds

b

b

proof end;

:: deftheorem Def8 defines pre-Measure MEASURE9:def 7 :

for X being set

for P being with_empty_element Subset-Family of X

for b_{3} being zeroed V224() Function of P,ExtREAL holds

( b_{3} is pre-Measure of P iff ( ( for F being disjoint_valued FinSequence of P st Union F in P holds

b_{3} . (Union F) = Sum (b_{3} * F) ) & ( for K being disjoint_valued Function of NAT,P st Union K in P holds

b_{3} . (Union K) <= SUM (b_{3} * K) ) ) );

for X being set

for P being with_empty_element Subset-Family of X

for b

( b

b

b

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 )

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 )

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() )

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: ( <*+infty*> is nonnegative & <*+infty*> is V251() )

proof end;

LL2: ( <*-infty*> is nonpositive & <*-infty*> is V252() )

proof end;

registration

ex b_{1} being FinSequence of ExtREAL st b_{1} is nonnegative
by LL1;

not for b_{1} being FinSequence of ExtREAL holds b_{1} is V251()
by LL1;

ex b_{1} being FinSequence of ExtREAL st b_{1} is nonpositive
by LL2;

not for b_{1} being FinSequence of ExtREAL holds b_{1} is V252()
by LL2;

correctness

coherence

for b_{1} being FinSequence of ExtREAL st b_{1} is nonnegative holds

b_{1} is V251();

;

correctness

coherence

for b_{1} being FinSequence of ExtREAL st b_{1} is nonpositive holds

b_{1} is V252();

;

end;

cluster Relation-like omega -defined ExtREAL -valued Function-like V34() FinSequence-like FinSubsequence-like ext-real-valued nonnegative for of ;

existence ex b

cluster Relation-like omega -defined ExtREAL -valued Function-like V34() FinSequence-like FinSubsequence-like ext-real-valued V251() for of ;

existence not for b

cluster Relation-like omega -defined ExtREAL -valued Function-like V34() FinSequence-like FinSubsequence-like ext-real-valued nonpositive for of ;

existence ex b

cluster Relation-like omega -defined ExtREAL -valued Function-like V34() FinSequence-like FinSubsequence-like ext-real-valued V252() for of ;

existence not for b

correctness

coherence

for b

b

;

correctness

coherence

for b

b

;

registration

let X, Y be non empty set ;

let F be V251() Function of Y,ExtREAL;

let G be Function of X,Y;

correctness

coherence

for b_{1} being Function of X,ExtREAL st b_{1} = F * G holds

b_{1} is without-infty ;

end;
let F be V251() Function of Y,ExtREAL;

let G be Function of X,Y;

correctness

coherence

for b

b

proof end;

registration

let X, Y be non empty set ;

let F be V224() Function of Y,ExtREAL;

let G be Function of X,Y;

correctness

coherence

for b_{1} being Function of X,ExtREAL st b_{1} = F * G holds

b_{1} is nonnegative ;

by MEASURE1:25;

end;
let F be V224() Function of Y,ExtREAL;

let G be Function of X,Y;

correctness

coherence

for b

b

by MEASURE1:25;

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() ) )

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) = (Partial_Sums G) . i

for G being ExtREAL_sequence st ( for i being Nat holds F . i = G . i ) holds

for i being Nat holds Sum (F | i) = (Partial_Sums G) . 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 )

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

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) ;

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)

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 . (Union F) = 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 )

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 . (Union F) = 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 . (Union F) = 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 @) )

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 . (Union F) = 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)

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

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

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

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 (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)

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 (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)

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

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 (Ring_generated_by S),ExtREAL st

( M . {} = 0 & ( for K being disjoint_valued FinSequence of S st Union K in Ring_generated_by S holds

M . (Union K) = Sum (P * K) ) )

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 (Ring_generated_by S),ExtREAL st

( M . {} = 0 & ( for K being disjoint_valued FinSequence of S st Union K in Ring_generated_by S holds

M . (Union K) = 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,(Ring_generated_by P) 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 )

for P being with_empty_element cap-closed semi-diff-closed Subset-Family of X

for K being disjoint_valued Function of NAT,(Ring_generated_by P) 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,(Ring_generated_by P) 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 )

for P being with_empty_element cap-closed semi-diff-closed Subset-Family of X

for K being disjoint_valued Function of NAT,(Ring_generated_by P) 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,(Field_generated_by P) 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 )

for P being semialgebra_of_sets of X

for K being disjoint_valued Function of NAT,(Field_generated_by P) 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)

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 (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)

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)

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

(Partial_Sums F) . n = a * (n + 1)

for n being Nat

for a being R_eal st ( for k being Nat holds F . k = a ) holds

(Partial_Sums F) . 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)}

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))))) )

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 (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) ) holds

M is completely-additive

for S being semialgebra_of_sets of X

for P being pre-Measure of S

for 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) ) holds

M is completely-additive

proof end;

definition

let X be set ;

let S be semialgebra_of_sets of X;

let P be pre-Measure of S;

ex b_{1} 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

b_{1} . A = Sum (P * F)
by Th55;

end;
let S be semialgebra_of_sets of X;

let P be pre-Measure of S;

mode induced_Measure of S,P -> Measure of (Field_generated_by S) 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 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);

ex b

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

b

:: 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 b_{4} being Measure of (Field_generated_by S) holds

( b_{4} 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

b_{4} . A = Sum (P * F) );

for X being set

for S being semialgebra_of_sets of X

for P being pre-Measure of S

for b

( b

for F being disjoint_valued FinSequence of S st A = Union F holds

b

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

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 (C_Meas M)) | (sigma (Field_generated_by S)) is sigma_Measure of (sigma (Field_generated_by S))

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 (C_Meas M)) | (sigma (Field_generated_by S)) is sigma_Measure of (sigma (Field_generated_by S))

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;

ex b_{1} being sigma_Measure of (sigma (Field_generated_by S)) st b_{1} = (sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S))

end;
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 (sigma (Field_generated_by S)) means :Def10: :: MEASURE9:def 9

it = (sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S));

existence it = (sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S));

ex b

proof 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 b_{5} being sigma_Measure of (sigma (Field_generated_by S)) holds

( b_{5} is induced_sigma_Measure of S,M iff b_{5} = (sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S)) );

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 b

( b

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

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;