:: MEASURE2 semantic presentation

begin

theorem :: MEASURE2:1
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Function of NAT,S holds M * F is V86() by MEASURE1:25;

definition
let X be set ;
let S be SigmaField of X;
mode N_Measure_fam of S ->  N_Sub_set_fam of X means :Def1: :: MEASURE2:def 1
it c= S;
existence
 ex b1 being N_Sub_set_fam of X st b1 c= S
proof
 ( {} is Subset of X & {{},{}} = {{}} ) by ENUMSET1:29, XBOOLE_1:2;
then reconsider C = {{}} as N_Sub_set_fam of X by MEASURE1:20;
take  C ; ::_thesis: C c= S
 {} in S by PROB_1:4;
hence  C c= S by ZFMISC_1:31; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines N_Measure_fam MEASURE2:def_1_:_
 for X being set
for S being SigmaField of X
for b3 being N_Sub_set_fam of X holds
( b3 is N_Measure_fam of S iff b3 c= S );

theorem Th2: :: MEASURE2:2
for X being set
for S being SigmaField of X
for T being N_Measure_fam of S holds
( meet T in S & union T in S )
proof
let X be set ; ::_thesis: for S being SigmaField of X
for T being N_Measure_fam of S holds
( meet T in S & union T in S )
let S be SigmaField of X; ::_thesis: for T being N_Measure_fam of S holds
( meet T in S & union T in S )
let T be N_Measure_fam of S; ::_thesis: ( meet T in S & union T in S )
 T c= S by Def1;
hence  ( meet T in S & union T in S ) by MEASURE1:22, MEASURE1:def_5; ::_thesis: verum
end;

definition
let X be set ;
let S be SigmaField of X;
let T be N_Measure_fam of S;
:: original: meet
redefine func meet T ->  Element of S;
coherence
 meet T is Element of S by Th2;
:: original: union
redefine func union T ->  Element of S;
coherence
 union T is Element of S by Th2;
end;

theorem Th3: :: MEASURE2:3
for X being set
for S being SigmaField of X
for N being Function of NAT,S ex F being Function of NAT,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) )
proof
let X be set ; ::_thesis: for S being SigmaField of X
for N being Function of NAT,S ex F being Function of NAT,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) )
let S be SigmaField of X; ::_thesis: for N being Function of NAT,S ex F being Function of NAT,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) )
let N be Function of NAT,S; ::_thesis: ex F being Function of NAT,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) )
reconsider S = S as non empty set ;
defpred S1[ set , set , set ] means  for A, B being Element of S
for c being Element of NAT st c = $1 & A = $2 & B = $3 holds
B = (N . (c + 1)) \ (N . c);
reconsider A = N . 0 as Element of S ;
A1: for c being Element of NAT
for A being Element of S ex B being Element of S st S1[c,A,B]
proof
let c be Element of NAT ; ::_thesis: for A being Element of S ex B being Element of S st S1[c,A,B]
let A be Element of S; ::_thesis: ex B being Element of S st S1[c,A,B]
reconsider B = (N . (c + 1)) \ (N . c) as Element of S ;
take  B ; ::_thesis: S1[c,A,B]
thus  S1[c,A,B] ; ::_thesis: verum
end;
consider F being Function of NAT,S such that
A2: ( F . 0 = A & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A1);
 for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (N . n)
proof
let n be Element of NAT ; ::_thesis: F . (n + 1) = (N . (n + 1)) \ (N . n)
 for a, b being Element of S
for s being Element of NAT st s = n & a = F . n & b = F . (n + 1) holds
b = (N . (s + 1)) \ (N . s) by A2;
hence  F . (n + 1) = (N . (n + 1)) \ (N . n) ; ::_thesis: verum
end;
hence  ex F being Function of NAT,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) ) by A2; ::_thesis: verum
end;

theorem Th4: :: MEASURE2:4
for X being set
for S being SigmaField of X
for N being Function of NAT,S ex F being Function of NAT,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) )
proof
let X be set ; ::_thesis: for S being SigmaField of X
for N being Function of NAT,S ex F being Function of NAT,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) )
let S be SigmaField of X; ::_thesis: for N being Function of NAT,S ex F being Function of NAT,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) )
let N be Function of NAT,S; ::_thesis: ex F being Function of NAT,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) )
defpred S1[ set , set , set ] means  for A, B being Element of S
for c being Element of NAT st c = $1 & A = $2 & B = $3 holds
B = (N . (c + 1)) \/ A;
A1: for c being Element of NAT
for A being Element of S ex B being Element of S st S1[c,A,B]
proof
let c be Element of NAT ; ::_thesis: for A being Element of S ex B being Element of S st S1[c,A,B]
let A be Element of S; ::_thesis: ex B being Element of S st S1[c,A,B]
reconsider B = (N . (c + 1)) \/ A as Element of S ;
take  B ; ::_thesis: S1[c,A,B]
thus  S1[c,A,B] ; ::_thesis: verum
end;
consider F being Function of NAT,S such that
A2: ( F . 0 = N . 0 & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A1);
 for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) by A2;
hence  ex F being Function of NAT,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) ) by A2; ::_thesis: verum
end;

theorem Th5: :: MEASURE2:5
for X being set
for S being non empty Subset-Family of X
for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds
for r being set
for n being Element of NAT holds
( r in F . n iff ex k being Element of NAT st
( k <= n & r in N . k ) )
proof
let X be set ; ::_thesis: for S being non empty Subset-Family of X
for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds
for r being set
for n being Element of NAT holds
( r in F . n iff ex k being Element of NAT st
( k <= n & r in N . k ) )
let S be non empty Subset-Family of X; ::_thesis: for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds
for r being set
for n being Element of NAT holds
( r in F . n iff ex k being Element of NAT st
( k <= n & r in N . k ) )
let N, F be Function of NAT,S; ::_thesis: ( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) implies for r being set
for n being Element of NAT holds
( r in F . n iff ex k being Element of NAT st
( k <= n & r in N . k ) ) )
assume that
A1: F . 0 = N . 0 and
A2: for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ; ::_thesis: for r being set
for n being Element of NAT holds
( r in F . n iff ex k being Element of NAT st
( k <= n & r in N . k ) )
let r be set ; ::_thesis: for n being Element of NAT holds
( r in F . n iff ex k being Element of NAT st
( k <= n & r in N . k ) )
let n be Element of NAT ; ::_thesis: ( r in F . n iff ex k being Element of NAT st
( k <= n & r in N . k ) )
defpred S1[ Element of NAT ] means ( ex k being Element of NAT st
( k <= $1 & r in N . k ) implies r in F . $1 );
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: ( ex k being Element of NAT st
( k <= n & r in N . k ) implies r in F . n ) ; ::_thesis: S1[n + 1]
A5: F . (n + 1) = (N . (n + 1)) \/ (F . n) by A2;
given k being Element of NAT  such that A6: k <= n + 1 and
A7: r in N . k ; ::_thesis: r in F . (n + 1)
 ( k <= n or k = n + 1 ) by A6, NAT_1:8;
hence  r in F . (n + 1) by A4, A7, A5, XBOOLE_0:def_3; ::_thesis: verum
end;
thus  ( r in F . n implies ex k being Element of NAT st
( k <= n & r in N . k ) ) ::_thesis: ( ex k being Element of NAT st
( k <= n & r in N . k ) implies r in F . n )
proof
defpred S2[ Nat] means r in F . $1;
assume A8: r in F . n ; ::_thesis: ex k being Element of NAT st
( k <= n & r in N . k )
then A9: ex n being Nat st S2[n] ;
 ex s being Nat st
( S2[s] & ( for k being Nat st S2[k] holds
s <= k ) ) from NAT_1:sch_5(A9);
then consider s being Nat such that
A10: r in F . s and
A11: for k being Nat st r in F . k holds
s <= k ;
A12: ( ex k being Nat st s = k + 1 implies ex k being Element of NAT st
( k <= n & r in N . k ) )
proof
given k being Nat such that A13: s = k + 1 ; ::_thesis: ex k being Element of NAT st
( k <= n & r in N . k )
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A14: not r in F . k
proof
assume  r in F . k ; ::_thesis: contradiction
then  s <= k by A11;
hence  contradiction by A13, NAT_1:13; ::_thesis: verum
end;
take  s ; ::_thesis: ( s is Element of REAL & s is Element of NAT & s <= n & r in N . s )
A15: s in NAT by ORDINAL1:def_12;
 F . s = (N . s) \/ (F . k) by A2, A13;
hence  ( s is Element of REAL & s is Element of NAT & s <= n & r in N . s ) by A8, A10, A11, A14, A15, XBOOLE_0:def_3; ::_thesis: verum
end;
 ( s = 0 implies ex k being Element of NAT st
( k <= n & r in N . k ) ) by A1, A10, NAT_1:2;
hence  ex k being Element of NAT st
( k <= n & r in N . k ) by A12, NAT_1:6; ::_thesis: verum
end;
A16: S1[ 0 ] by A1, NAT_1:3;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A16, A3);
hence  ( ex k being Element of NAT st
( k <= n & r in N . k ) implies r in F . n ) ; ::_thesis: verum
end;

theorem Th6: :: MEASURE2:6
for X being set
for S being non empty Subset-Family of X
for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds
for n, m being Element of NAT st n < m holds
F . n c= F . m
proof
let X be set ; ::_thesis: for S being non empty Subset-Family of X
for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds
for n, m being Element of NAT st n < m holds
F . n c= F . m
let S be non empty Subset-Family of X; ::_thesis: for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds
for n, m being Element of NAT st n < m holds
F . n c= F . m
let N, F be Function of NAT,S; ::_thesis: ( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) implies for n, m being Element of NAT st n < m holds
F . n c= F . m )
assume that
A1: F . 0 = N . 0 and
A2: for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ; ::_thesis: for n, m being Element of NAT st n < m holds
F . n c= F . m
defpred S1[ Element of NAT ] means  for m being Element of NAT st $1 < m holds
F . $1 c= F . m;
A3: S1[ 0 ]
proof
A4: for k being Element of NAT st 0 < k + 1 holds
F . 0 c= F . (k + 1)
proof
defpred S2[ Element of NAT ] means ( 0 < $1 + 1 implies F . 0 c= F . ($1 + 1) );
A5: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
A6: 0 <= k by NAT_1:2;
 F . ((k + 1) + 1) = (N . ((k + 1) + 1)) \/ (F . (k + 1)) by A2;
then A7: F . (k + 1) c= F . ((k + 1) + 1) by XBOOLE_1:7;
assume  ( 0 < k + 1 implies F . 0 c= F . (k + 1) ) ; ::_thesis: S2[k + 1]
hence  S2[k + 1] by A7, A6, NAT_1:13, XBOOLE_1:1; ::_thesis: verum
end;
 F . (0 + 1) = (N . (0 + 1)) \/ (F . 0) by A2;
then A8: S2[ 0 ] by XBOOLE_1:7;
thus  for k being Element of NAT holds S2[k] from NAT_1:sch_1(A8, A5); ::_thesis: verum
end;
let m be Element of NAT ; ::_thesis: ( 0 < m implies F . 0 c= F . m )
assume A9: 0 < m ; ::_thesis: F . 0 c= F . m
then consider k being Nat such that
A10: m = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 m = k + 1 by A10;
hence  F . 0 c= F . m by A9, A4; ::_thesis: verum
end;
A11: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A12: for m being Element of NAT st n < m holds
F . n c= F . m ; ::_thesis: S1[n + 1]
let m be Element of NAT ; ::_thesis: ( n + 1 < m implies F . (n + 1) c= F . m )
assume A13: n + 1 < m ; ::_thesis: F . (n + 1) c= F . m
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in F . (n + 1) or r in F . m )
A14: ( r in F . n implies r in F . m )
proof
assume A15: r in F . n ; ::_thesis: r in F . m
 ( n < m implies r in F . m )
proof
assume  n < m ; ::_thesis: r in F . m
then  F . n c= F . m by A12;
hence  r in F . m by A15; ::_thesis: verum
end;
hence  r in F . m by A13, NAT_1:13; ::_thesis: verum
end;
assume A16: r in F . (n + 1) ; ::_thesis: r in F . m
A17: F . (n + 1) = (N . (n + 1)) \/ (F . n) by A2;
 ( r in N . (n + 1) implies r in F . m ) by A1, A2, A13, Th5;
hence  r in F . m by A16, A17, A14, XBOOLE_0:def_3; ::_thesis: verum
end;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A11); ::_thesis: verum
end;

theorem Th7: :: MEASURE2:7
for X being set
for S being non empty Subset-Family of X
for N, G, F being Function of NAT,S st G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds
for n, m being Element of NAT st n <= m holds
F . n c= G . m
proof
let X be set ; ::_thesis: for S being non empty Subset-Family of X
for N, G, F being Function of NAT,S st G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds
for n, m being Element of NAT st n <= m holds
F . n c= G . m
let S be non empty Subset-Family of X; ::_thesis: for N, G, F being Function of NAT,S st G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds
for n, m being Element of NAT st n <= m holds
F . n c= G . m
let N, G, F be Function of NAT,S; ::_thesis: ( G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) implies for n, m being Element of NAT st n <= m holds
F . n c= G . m )
assume that
A1: G . 0 = N . 0 and
A2: for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) and
A3: F . 0 = N . 0 and
A4: for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ; ::_thesis: for n, m being Element of NAT st n <= m holds
F . n c= G . m
let n, m be Element of NAT ; ::_thesis: ( n <= m implies F . n c= G . m )
A5: for n being Element of NAT holds F . n c= G . n
proof
defpred S1[ Element of NAT ] means F . $1 c= G . $1;
A6: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  F . n c= G . n ; ::_thesis: S1[n + 1]
 G . (n + 1) = (N . (n + 1)) \/ (G . n) by A2;
then A7: N . (n + 1) c= G . (n + 1) by XBOOLE_1:7;
 F . (n + 1) = (N . (n + 1)) \ (G . n) by A4;
hence  S1[n + 1] by A7, XBOOLE_1:1; ::_thesis: verum
end;
A8: S1[ 0 ] by A1, A3;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A6); ::_thesis: verum
end;
A9: ( n < m implies F . n c= G . m )
proof
assume  n < m ; ::_thesis: F . n c= G . m
then A10: G . n c= G . m by A1, A2, Th6;
 F . n c= G . n by A5;
hence  F . n c= G . m by A10, XBOOLE_1:1; ::_thesis: verum
end;
assume  n <= m ; ::_thesis: F . n c= G . m
then  ( n = m or n < m ) by XXREAL_0:1;
hence  F . n c= G . m by A5, A9; ::_thesis: verum
end;

theorem Th8: :: MEASURE2:8
for X being set
for S being SigmaField of X
for N, G being Function of NAT,S ex F being Function of NAT,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) )
proof
let X be set ; ::_thesis: for S being SigmaField of X
for N, G being Function of NAT,S ex F being Function of NAT,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) )
let S be SigmaField of X; ::_thesis: for N, G being Function of NAT,S ex F being Function of NAT,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) )
let N, G be Function of NAT,S; ::_thesis: ex F being Function of NAT,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) )
defpred S1[ set , set , set ] means  for A, B being Element of S
for c being Element of NAT st c = $1 & A = $2 & B = $3 holds
B = (N . (c + 1)) \ (G . c);
A1: for c being Element of NAT
for A being Element of S ex B being Element of S st S1[c,A,B]
proof
let c be Element of NAT ; ::_thesis: for A being Element of S ex B being Element of S st S1[c,A,B]
let A be Element of S; ::_thesis: ex B being Element of S st S1[c,A,B]
consider B being set  such that
A2: B = (N . (c + 1)) \ (G . c) ;
reconsider B = B as Element of S by A2;
take  B ; ::_thesis: S1[c,A,B]
thus  S1[c,A,B] by A2; ::_thesis: verum
end;
consider F being Function of NAT,S such that
A3: ( F . 0 = N . 0 & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A1);
 for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n)
proof
let n be Element of NAT ; ::_thesis: F . (n + 1) = (N . (n + 1)) \ (G . n)
 for a, b being Element of S
for s being Element of NAT st s = n & a = F . n & b = F . (n + 1) holds
b = (N . (s + 1)) \ (G . s) by A3;
hence  F . (n + 1) = (N . (n + 1)) \ (G . n) ; ::_thesis: verum
end;
hence  ex F being Function of NAT,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) ) by A3; ::_thesis: verum
end;

theorem :: MEASURE2:9
for X being set
for S being SigmaField of X
for N being Function of NAT,S ex F being Function of NAT,S st
( F . 0 = {} & ( for n being Element of NAT holds F . (n + 1) = (N . 0) \ (N . n) ) )
proof
let X be set ; ::_thesis: for S being SigmaField of X
for N being Function of NAT,S ex F being Function of NAT,S st
( F . 0 = {} & ( for n being Element of NAT holds F . (n + 1) = (N . 0) \ (N . n) ) )
let S be SigmaField of X; ::_thesis: for N being Function of NAT,S ex F being Function of NAT,S st
( F . 0 = {} & ( for n being Element of NAT holds F . (n + 1) = (N . 0) \ (N . n) ) )
let N be Function of NAT,S; ::_thesis: ex F being Function of NAT,S st
( F . 0 = {} & ( for n being Element of NAT holds F . (n + 1) = (N . 0) \ (N . n) ) )
defpred S1[ set , set , set ] means  for A, B being Element of S
for c being Element of NAT st c = $1 & A = $2 & B = $3 holds
B = (N . 0) \ (N . c);
reconsider A = {} as Element of S by PROB_1:4;
A1: for c being Element of NAT
for A being Element of S ex B being Element of S st S1[c,A,B]
proof
let c be Element of NAT ; ::_thesis: for A being Element of S ex B being Element of S st S1[c,A,B]
let A be Element of S; ::_thesis: ex B being Element of S st S1[c,A,B]
reconsider B = (N . 0) \ (N . c) as Element of S ;
take  B ; ::_thesis: S1[c,A,B]
thus  S1[c,A,B] ; ::_thesis: verum
end;
consider F being Function of NAT,S such that
A2: ( F . 0 = A & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A1);
 for n being Element of NAT holds F . (n + 1) = (N . 0) \ (N . n)
proof
let n be Element of NAT ; ::_thesis: F . (n + 1) = (N . 0) \ (N . n)
 for a, b being Element of S
for s being Element of NAT st s = n & a = F . n & b = F . (n + 1) holds
b = (N . 0) \ (N . s) by A2;
hence  F . (n + 1) = (N . 0) \ (N . n) ; ::_thesis: verum
end;
hence  ex F being Function of NAT,S st
( F . 0 = {} & ( for n being Element of NAT holds F . (n + 1) = (N . 0) \ (N . n) ) ) by A2; ::_thesis: verum
end;

theorem Th10: :: MEASURE2:10
for X being set
for S being SigmaField of X
for N, G, F being Function of NAT,S st G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds
for n, m being Element of NAT st n < m holds
F . n misses F . m
proof
let X be set ; ::_thesis: for S being SigmaField of X
for N, G, F being Function of NAT,S st G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds
for n, m being Element of NAT st n < m holds
F . n misses F . m
let S be SigmaField of X; ::_thesis: for N, G, F being Function of NAT,S st G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds
for n, m being Element of NAT st n < m holds
F . n misses F . m
let N, G, F be Function of NAT,S; ::_thesis: ( G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) implies for n, m being Element of NAT st n < m holds
F . n misses F . m )
assume that
A1: ( G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 ) and
A2: for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ; ::_thesis: for n, m being Element of NAT st n < m holds
F . n misses F . m
let n, m be Element of NAT ; ::_thesis: ( n < m implies F . n misses F . m )
assume A3: n < m ; ::_thesis: F . n misses F . m
then  0 <> m by NAT_1:2;
then consider k being Nat such that
A4: m = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 F . (k + 1) = (N . (k + 1)) \ (G . k) by A2;
then A5: G . k misses F . (k + 1) by XBOOLE_1:79;
 n <= k by A3, A4, NAT_1:13;
hence (F . n) /\ (F . m) = ((F . n) /\ (G . k)) /\ (F . (k + 1)) by A1, A2, A4, Th7, XBOOLE_1:28
.= (F . n) /\ ((G . k) /\ (F . (k + 1))) by XBOOLE_1:16
.= (F . n) /\ {} by A5, XBOOLE_0:def_7
.= {} ;
:: according to XBOOLE_0:def_7 ::_thesis: verum
end;

theorem Th11: :: MEASURE2:11
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for T being N_Measure_fam of S
for F being Function of NAT,S st T = rng F holds
M . (union T) <= SUM (M * F)
proof
let X be set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for T being N_Measure_fam of S
for F being Function of NAT,S st T = rng F holds
M . (union T) <= SUM (M * F)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for T being N_Measure_fam of S
for F being Function of NAT,S st T = rng F holds
M . (union T) <= SUM (M * F)
let M be sigma_Measure of S; ::_thesis: for T being N_Measure_fam of S
for F being Function of NAT,S st T = rng F holds
M . (union T) <= SUM (M * F)
let T be N_Measure_fam of S; ::_thesis: for F being Function of NAT,S st T = rng F holds
M . (union T) <= SUM (M * F)
let F be Function of NAT,S; ::_thesis: ( T = rng F implies M . (union T) <= SUM (M * F) )
consider G being Function of NAT,S such that
A1: ( G . 0 = F . 0 & ( for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ) ) by Th4;
consider H being Function of NAT,S such that
A2: H . 0 = F . 0 and
A3: for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) by Th8;
 for n, m being set st n <> m holds
H . n misses H . m
proof
let n, m be set ; ::_thesis: ( n <> m implies H . n misses H . m )
assume A4: n <> m ; ::_thesis: H . n misses H . m
percases ( ( n in dom H & m in dom H ) or not n in dom H or not m in dom H ) ;
suppose ( n in dom H & m in dom H ) ; ::_thesis: H . n misses H . m
then reconsider n9 = n, m9 = m as Element of NAT ;
A5: ( m9 < n9 implies H . m misses H . n ) by A1, A2, A3, Th10;
 ( n9 < m9 implies H . n misses H . m ) by A1, A2, A3, Th10;
hence  H . n misses H . m by A4, A5, XXREAL_0:1; ::_thesis: verum
end;
suppose ( not n in dom H or not m in dom H ) ; ::_thesis: H . n misses H . m
then  ( H . n = {} or H . m = {} ) by FUNCT_1:def_2;
hence  H . n misses H . m by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
then  H is Sep_Sequence of S by PROB_2:def_2;
then A6: SUM (M * H) = M . (union (rng H)) by MEASURE1:def_6;
A7: for n being Element of NAT holds H . n c= F . n
proof
let n be Element of NAT ; ::_thesis: H . n c= F . n
A8: ( ex k being Nat st n = k + 1 implies H . n c= F . n )
proof
given k being Nat such that A9: n = k + 1 ; ::_thesis: H . n c= F . n
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 H . n = (F . n) \ (G . k) by A3, A9;
hence  H . n c= F . n by XBOOLE_1:36; ::_thesis: verum
end;
 ( n = 0 or ex k being Nat st n = k + 1 ) by NAT_1:6;
hence  H . n c= F . n by A2, A8; ::_thesis: verum
end;
A10: for n being Element of NAT holds (M * H) . n <= (M * F) . n
proof
let n be Element of NAT ; ::_thesis: (M * H) . n <= (M * F) . n
 NAT = dom (M * F) by FUNCT_2:def_1;
then A11: (M * F) . n = M . (F . n) by FUNCT_1:12;
 NAT = dom (M * H) by FUNCT_2:def_1;
then  (M * H) . n = M . (H . n) by FUNCT_1:12;
hence  (M * H) . n <= (M * F) . n by A7, A11, MEASURE1:31; ::_thesis: verum
end;
A12: union (rng H) = union (rng F)
proof
thus  union (rng H) c= union (rng F) :: according to XBOOLE_0:def_10 ::_thesis: union (rng F) c= union (rng H)
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in union (rng H) or r in union (rng F) )
assume  r in union (rng H) ; ::_thesis: r in union (rng F)
then consider E being set  such that
A13: r in E and
A14: E in rng H by TARSKI:def_4;
consider s being set  such that
A15: s in dom H and
A16: E = H . s by A14, FUNCT_1:def_3;
reconsider s = s as Element of NAT by A15;
A17: F . s in rng F by FUNCT_2:4;
 E c= F . s by A7, A16;
hence  r in union (rng F) by A13, A17, TARSKI:def_4; ::_thesis: verum
end;
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in union (rng F) or r in union (rng H) )
assume  r in union (rng F) ; ::_thesis: r in union (rng H)
then consider E being set  such that
A18: r in E and
A19: E in rng F by TARSKI:def_4;
A20: ex s being set st
( s in dom F & E = F . s ) by A19, FUNCT_1:def_3;
 ex s1 being Element of NAT st r in H . s1
proof
defpred S1[ Nat] means r in F . $1;
A21: ex k being Nat st S1[k] by A18, A20;
 ex k being Nat st
( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch_5(A21);
then consider k being Nat such that
A22: r in F . k and
A23: for n being Nat st r in F . n holds
k <= n ;
A24: ( ex l being Nat st k = l + 1 implies ex s1 being Element of NAT st r in H . s1 )
proof
given l being Nat such that A25: k = l + 1 ; ::_thesis: ex s1 being Element of NAT st r in H . s1
take  k ; ::_thesis: ( k is Element of REAL & k is Element of NAT & r in H . k )
reconsider l = l as Element of NAT by ORDINAL1:def_12;
A26: not r in G . l
proof
assume  r in G . l ; ::_thesis: contradiction
then consider i being Element of NAT  such that
A27: i <= l and
A28: r in F . i by A1, Th5;
 k <= i by A23, A28;
hence  contradiction by A25, A27, NAT_1:13; ::_thesis: verum
end;
 H . (l + 1) = (F . (l + 1)) \ (G . l) by A3;
hence  ( k is Element of REAL & k is Element of NAT & r in H . k ) by A22, A25, A26, XBOOLE_0:def_5; ::_thesis: verum
end;
 ( k = 0 implies ex s1 being Element of NAT st r in H . s1 ) by A2, A22;
hence  ex s1 being Element of NAT st r in H . s1 by A24, NAT_1:6; ::_thesis: verum
end;
then consider s1 being Element of NAT  such that
A29: r in H . s1 ;
 H . s1 in rng H by FUNCT_2:4;
hence  r in union (rng H) by A29, TARSKI:def_4; ::_thesis: verum
end;
assume  T = rng F ; ::_thesis: M . (union T) <= SUM (M * F)
hence  M . (union T) <= SUM (M * F) by A10, A6, A12, SUPINF_2:43; ::_thesis: verum
end;

theorem Th12: :: MEASURE2:12
for X being set
for S being SigmaField of X
for T being N_Measure_fam of S ex F being Function of NAT,S st T = rng F
proof
let X be set ; ::_thesis: for S being SigmaField of X
for T being N_Measure_fam of S ex F being Function of NAT,S st T = rng F
let S be SigmaField of X; ::_thesis: for T being N_Measure_fam of S ex F being Function of NAT,S st T = rng F
let T be N_Measure_fam of S; ::_thesis: ex F being Function of NAT,S st T = rng F
consider F being Function of NAT,(bool X) such that
A1: T = rng F by SUPINF_2:def_8;
 rng F c= S by A1, Def1;
then  F is Function of NAT,S by FUNCT_2:6;
then consider F being Function of NAT,S such that
A2: T = rng F by A1;
take  F ; ::_thesis: T = rng F
thus  T = rng F by A2; ::_thesis: verum
end;

theorem Th13: :: MEASURE2:13
for N, F being Function st F . 0 = {} & ( for n being Element of NAT holds
( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) holds
for n being Element of NAT holds F . n c= F . (n + 1)
proof
let N, F be Function; ::_thesis: ( F . 0 = {} & ( for n being Element of NAT holds
( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) implies for n being Element of NAT holds F . n c= F . (n + 1) )
assume that
A1: F . 0 = {} and
A2: for n being Element of NAT holds
( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ; ::_thesis: for n being Element of NAT holds F . n c= F . (n + 1)
defpred S1[ Element of NAT ] means F . $1 c= F . ($1 + 1);
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  F . n c= F . (n + 1) ; ::_thesis: S1[n + 1]
 F . ((n + 1) + 1) = (N . 0) \ (N . (n + 1)) by A2;
then  (N . 0) \ (N . n) c= F . ((n + 1) + 1) by A2, XBOOLE_1:34;
hence  S1[n + 1] by A2; ::_thesis: verum
end;
let n be Element of NAT ; ::_thesis: F . n c= F . (n + 1)
 F . (0 + 1) = (N . 0) \ (N . 0) by A2;
then A4: S1[ 0 ] by A1, XBOOLE_1:37;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3);
hence  F . n c= F . (n + 1) ; ::_thesis: verum
end;

theorem :: MEASURE2:14
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
union T is measure_zero of M
proof
let X be set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
union T is measure_zero of M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
union T is measure_zero of M
let M be sigma_Measure of S; ::_thesis: for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
union T is measure_zero of M
let T be N_Measure_fam of S; ::_thesis: ( ( for A being set st A in T holds
A is measure_zero of M ) implies union T is measure_zero of M )
consider F being Function of NAT,S such that
A1: T = rng F by Th12;
set G = M * F;
assume A2: for A being set st A in T holds
A is measure_zero of M ; ::_thesis: union T is measure_zero of M
A3: for r being Element of NAT st 0 <= r holds
(M * F) . r = 0.
proof
let r be Element of NAT ; ::_thesis: ( 0 <= r implies (M * F) . r = 0. )
 F . r is measure_zero of M by A2, A1, FUNCT_2:4;
then  M . (F . r) = 0. by MEASURE1:def_7;
hence  ( 0 <= r implies (M * F) . r = 0. ) by FUNCT_2:15; ::_thesis: verum
end;
 M * F is V86() by MEASURE1:25;
then  SUM (M * F) = (Ser (M * F)) . 0 by A3, SUPINF_2:48;
then  SUM (M * F) = (M * F) . 0 by SUPINF_2:44;
then  SUM (M * F) = 0. by A3;
then A4: M . (union T) <= 0. by A1, Th11;
 0. <= M . (union T) by MEASURE1:def_2;
then  M . (union T) = 0. by A4, XXREAL_0:1;
hence  union T is measure_zero of M by MEASURE1:def_7; ::_thesis: verum
end;

theorem :: MEASURE2:15
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for T being N_Measure_fam of S st ex A being set st
( A in T & A is measure_zero of M ) holds
meet T is measure_zero of M by MEASURE1:36, SETFAM_1:3;

theorem :: MEASURE2:16
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
meet T is measure_zero of M
proof
let X be set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
meet T is measure_zero of M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
meet T is measure_zero of M
let M be sigma_Measure of S; ::_thesis: for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
meet T is measure_zero of M
let T be N_Measure_fam of S; ::_thesis: ( ( for A being set st A in T holds
A is measure_zero of M ) implies meet T is measure_zero of M )
assume A1: for A being set st A in T holds
A is measure_zero of M ; ::_thesis: meet T is measure_zero of M
 ex A being set st
( A in T & A is measure_zero of M )
proof
consider F being Function of NAT,(bool X) such that
A2: T = rng F by SUPINF_2:def_8;
take  F . 0 ; ::_thesis: ( F . 0 in T & F . 0 is measure_zero of M )
thus  ( F . 0 in T & F . 0 is measure_zero of M ) by A1, A2, FUNCT_2:4; ::_thesis: verum
end;
hence  meet T is measure_zero of M by MEASURE1:36, SETFAM_1:3; ::_thesis: verum
end;

definition
let X be set ;
let S be SigmaField of X;
let IT be N_Measure_fam of S;
attrIT is non-decreasing  means :Def2: :: MEASURE2:def 2
 ex F being Function of NAT,S st
( IT = rng F & ( for n being Element of NAT holds F . n c= F . (n + 1) ) );
end;

:: deftheorem Def2 defines non-decreasing MEASURE2:def_2_:_
 for X being set
for S being SigmaField of X
for IT being N_Measure_fam of S holds
( IT is non-decreasing iff ex F being Function of NAT,S st
( IT = rng F & ( for n being Element of NAT holds F . n c= F . (n + 1) ) ) );

registration
let X be set ;
let S be SigmaField of X;
cluster non empty V46() non-decreasing for N_Measure_fam of S;
existence
 ex b1 being N_Measure_fam of S st b1 is non-decreasing
proof
consider A being set  such that
A1: A in S by PROB_1:4;
reconsider A = A as Subset of X by A1;
consider B, C being Subset of X such that
A2: ( B = A & C = A ) ;
A3: {A} c= S by A1, ZFMISC_1:31;
consider F being Function of NAT,(bool X) such that
A4: rng F = {B,C} and
A5: ( F . 0 = B & ( for n being Element of NAT st 0 < n holds
F . n = C ) ) by MEASURE1:19;
A6: rng F = {A} by A2, A4, ENUMSET1:29;
then A7: rng F c= S by A1, ZFMISC_1:31;
 {A} is N_Sub_set_fam of X by A6, SUPINF_2:def_8;
then reconsider T = {A} as N_Measure_fam of S by A3, Def1;
reconsider F = F as Function of NAT,S by A7, FUNCT_2:6;
take  T ; ::_thesis: T is non-decreasing
take  F ; :: according to MEASURE2:def_2 ::_thesis: ( T = rng F & ( for n being Element of NAT holds F . n c= F . (n + 1) ) )
 for n being Element of NAT holds F . n c= F . (n + 1)
proof
let n be Element of NAT ; ::_thesis: F . n c= F . (n + 1)
 F . n = A by A2, A5, NAT_1:3;
hence  F . n c= F . (n + 1) by A2, A5, NAT_1:3; ::_thesis: verum
end;
hence  ( T = rng F & ( for n being Element of NAT holds F . n c= F . (n + 1) ) ) by A2, A4, ENUMSET1:29; ::_thesis: verum
end;
end;

definition
let X be set ;
let S be SigmaField of X;
let IT be N_Measure_fam of S;
attrIT is non-increasing  means :: MEASURE2:def 3
 ex F being Function of NAT,S st
( IT = rng F & ( for n being Element of NAT holds F . (n + 1) c= F . n ) );
end;

:: deftheorem  defines non-increasing MEASURE2:def_3_:_
 for X being set
for S being SigmaField of X
for IT being N_Measure_fam of S holds
( IT is non-increasing iff ex F being Function of NAT,S st
( IT = rng F & ( for n being Element of NAT holds F . (n + 1) c= F . n ) ) );

registration
let X be set ;
let S be SigmaField of X;
cluster non empty V46() non-increasing for N_Measure_fam of S;
existence
 ex b1 being N_Measure_fam of S st b1 is non-increasing
proof
consider A being set  such that
A1: A in S by PROB_1:4;
reconsider A = A as Subset of X by A1;
A2: {A} c= S by A1, ZFMISC_1:31;
set B = A;
set C = A;
consider F being Function of NAT,(bool X) such that
A3: rng F = {A,A} and
A4: ( F . 0 = A & ( for n being Element of NAT st 0 < n holds
F . n = A ) ) by MEASURE1:19;
A5: rng F = {A} by A3, ENUMSET1:29;
then A6: rng F c= S by A1, ZFMISC_1:31;
 {A} is N_Sub_set_fam of X by A5, SUPINF_2:def_8;
then reconsider T = {A} as N_Measure_fam of S by A2, Def1;
reconsider F = F as Function of NAT,S by A6, FUNCT_2:6;
take  T ; ::_thesis: T is non-increasing
take  F ; :: according to MEASURE2:def_3 ::_thesis: ( T = rng F & ( for n being Element of NAT holds F . (n + 1) c= F . n ) )
 for n being Element of NAT holds F . (n + 1) c= F . n
proof
let n be Element of NAT ; ::_thesis: F . (n + 1) c= F . n
 F . n = A by A4, NAT_1:3;
hence  F . (n + 1) c= F . n by A4, NAT_1:3; ::_thesis: verum
end;
hence  ( T = rng F & ( for n being Element of NAT holds F . (n + 1) c= F . n ) ) by A3, ENUMSET1:29; ::_thesis: verum
end;
end;

theorem :: MEASURE2:17
for X being set
for S being SigmaField of X
for N, F being Function of NAT,S st F . 0 = {} & ( for n being Element of NAT holds
( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) holds
rng F is non-decreasing N_Measure_fam of S
proof
let X be set ; ::_thesis: for S being SigmaField of X
for N, F being Function of NAT,S st F . 0 = {} & ( for n being Element of NAT holds
( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) holds
rng F is non-decreasing N_Measure_fam of S
let S be SigmaField of X; ::_thesis: for N, F being Function of NAT,S st F . 0 = {} & ( for n being Element of NAT holds
( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) holds
rng F is non-decreasing N_Measure_fam of S
let N, F be Function of NAT,S; ::_thesis: ( F . 0 = {} & ( for n being Element of NAT holds
( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) implies rng F is non-decreasing N_Measure_fam of S )
assume  ( F . 0 = {} & ( for n being Element of NAT holds
( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) ) ; ::_thesis: rng F is non-decreasing N_Measure_fam of S
then A1: for n being Element of NAT holds F . n c= F . (n + 1) by Th13;
 ( rng F c= S & rng F is N_Sub_set_fam of X ) by MEASURE1:23, RELAT_1:def_19;
hence  rng F is non-decreasing N_Measure_fam of S by A1, Def1, Def2; ::_thesis: verum
end;

theorem Th18: :: MEASURE2:18
for N being Function st ( for n being Element of NAT holds N . n c= N . (n + 1) ) holds
for m, n being Element of NAT st n <= m holds
N . n c= N . m
proof
let N be Function; ::_thesis: ( ( for n being Element of NAT holds N . n c= N . (n + 1) ) implies for m, n being Element of NAT st n <= m holds
N . n c= N . m )
defpred S1[ Element of NAT ] means  for n being Element of NAT st n <= $1 holds
N . n c= N . $1;
assume A1: for n being Element of NAT holds N . n c= N . (n + 1) ; ::_thesis: for m, n being Element of NAT st n <= m holds
N . n c= N . m
A2: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A3: for n being Element of NAT st n <= m holds
N . n c= N . m ; ::_thesis: S1[m + 1]
let n be Element of NAT ; ::_thesis: ( n <= m + 1 implies N . n c= N . (m + 1) )
A4: ( n <= m implies N . n c= N . (m + 1) )
proof
assume  n <= m ; ::_thesis: N . n c= N . (m + 1)
then A5: N . n c= N . m by A3;
 N . m c= N . (m + 1) by A1;
hence  N . n c= N . (m + 1) by A5, XBOOLE_1:1; ::_thesis: verum
end;
assume  n <= m + 1 ; ::_thesis: N . n c= N . (m + 1)
hence  N . n c= N . (m + 1) by A4, NAT_1:8; ::_thesis: verum
end;
A6: S1[ 0 ] by NAT_1:3;
thus  for m being Element of NAT holds S1[m] from NAT_1:sch_1(A6, A2); ::_thesis: verum
end;

theorem Th19: :: MEASURE2:19
for N, F being Function st F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
for n, m being Element of NAT st n < m holds
F . n misses F . m
proof
let N, F be Function; ::_thesis: ( F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) implies for n, m being Element of NAT st n < m holds
F . n misses F . m )
assume that
A1: F . 0 = N . 0 and
A2: for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ; ::_thesis: for n, m being Element of NAT st n < m holds
F . n misses F . m
let n, m be Element of NAT ; ::_thesis: ( n < m implies F . n misses F . m )
assume A3: n < m ; ::_thesis: F . n misses F . m
then  0 <> m by NAT_1:2;
then consider k being Nat such that
A4: m = k + 1 by NAT_1:6;
A5: for n being Element of NAT holds F . n c= N . n
proof
defpred S1[ Element of NAT ] means F . $1 c= N . $1;
A6: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  F . n c= N . n ; ::_thesis: S1[n + 1]
 F . (n + 1) = (N . (n + 1)) \ (N . n) by A2;
hence  S1[n + 1] ; ::_thesis: verum
end;
A7: S1[ 0 ] by A1;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A6); ::_thesis: verum
end;
A8: for n, m being Element of NAT st n <= m holds
F . n c= N . m
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies F . n c= N . m )
A9: ( n < m implies F . n c= N . m )
proof
assume  n < m ; ::_thesis: F . n c= N . m
then A10: N . n c= N . m by A2, Th18;
 F . n c= N . n by A5;
hence  F . n c= N . m by A10, XBOOLE_1:1; ::_thesis: verum
end;
assume  n <= m ; ::_thesis: F . n c= N . m
then  ( n = m or n < m ) by XXREAL_0:1;
hence  F . n c= N . m by A5, A9; ::_thesis: verum
end;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 F . (k + 1) = (N . (k + 1)) \ (N . k) by A2;
then A11: N . k misses F . (k + 1) by XBOOLE_1:79;
 n <= k by A3, A4, NAT_1:13;
then (F . n) /\ (F . (k + 1)) = ((F . n) /\ (N . k)) /\ (F . (k + 1)) by A8, XBOOLE_1:28
.= (F . n) /\ ((N . k) /\ (F . (k + 1))) by XBOOLE_1:16
.= (F . n) /\ {} by A11, XBOOLE_0:def_7
.= {} ;
hence  F . n misses F . m by A4, XBOOLE_0:def_7; ::_thesis: verum
end;

theorem Th20: :: MEASURE2:20
for X being set
for S being SigmaField of X
for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
union (rng F) = union (rng N)
proof
let X be set ; ::_thesis: for S being SigmaField of X
for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
union (rng F) = union (rng N)
let S be SigmaField of X; ::_thesis: for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
union (rng F) = union (rng N)
let N, F be Function of NAT,S; ::_thesis: ( F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) implies union (rng F) = union (rng N) )
assume that
A1: F . 0 = N . 0 and
A2: for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ; ::_thesis: union (rng F) = union (rng N)
thus  union (rng F) c= union (rng N) :: according to XBOOLE_0:def_10 ::_thesis: union (rng N) c= union (rng F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng F) or x in union (rng N) )
assume  x in union (rng F) ; ::_thesis: x in union (rng N)
then consider Y being set  such that
A3: x in Y and
A4: Y in rng F by TARSKI:def_4;
consider n being set  such that
A5: n in dom F and
A6: Y = F . n by A4, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A5;
A7: ( ex k being Nat st n = k + 1 implies ex Z being set st
( x in Z & Z in rng N ) )
proof
given k being Nat such that A8: n = k + 1 ; ::_thesis: ex Z being set st
( x in Z & Z in rng N )
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 Y = (N . (k + 1)) \ (N . k) by A2, A6, A8;
then  x in N . (k + 1) by A3, XBOOLE_0:def_5;
hence  ex Z being set st
( x in Z & Z in rng N ) by FUNCT_2:4; ::_thesis: verum
end;
 ( n = 0 implies ex Z being set st
( x in Z & Z in rng N ) ) by A1, A3, A6, FUNCT_2:4;
hence  x in union (rng N) by A7, NAT_1:6, TARSKI:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng N) or x in union (rng F) )
assume  x in union (rng N) ; ::_thesis: x in union (rng F)
then consider Y being set  such that
A9: x in Y and
A10: Y in rng N by TARSKI:def_4;
A11: ex n being set st
( n in dom N & Y = N . n ) by A10, FUNCT_1:def_3;
 ex Z being set st
( x in Z & Z in rng F )
proof
 ex s being Element of NAT st x in F . s
proof
defpred S1[ Nat] means x in N . $1;
A12: ex k being Nat st S1[k] by A9, A11;
 ex k being Nat st
( S1[k] & ( for r being Nat st S1[r] holds
k <= r ) ) from NAT_1:sch_5(A12);
then consider k being Nat such that
A13: x in N . k and
A14: for r being Nat st x in N . r holds
k <= r ;
A15: ( ex l being Nat st k = l + 1 implies ex s being Element of NAT st x in F . s )
proof
given l being Nat such that A16: k = l + 1 ; ::_thesis: ex s being Element of NAT st x in F . s
take  k ; ::_thesis: ( k is Element of REAL & k is Element of NAT & x in F . k )
reconsider l = l as Element of NAT by ORDINAL1:def_12;
A17: not x in N . l
proof
assume  x in N . l ; ::_thesis: contradiction
then  l + 1 <= l by A14, A16;
hence  contradiction by NAT_1:13; ::_thesis: verum
end;
 F . (l + 1) = (N . (l + 1)) \ (N . l) by A2;
hence  ( k is Element of REAL & k is Element of NAT & x in F . k ) by A13, A16, A17, XBOOLE_0:def_5; ::_thesis: verum
end;
 ( k = 0 implies ex s being Element of NAT st x in F . s ) by A1, A13;
hence  ex s being Element of NAT st x in F . s by A15, NAT_1:6; ::_thesis: verum
end;
hence  ex Z being set st
( x in Z & Z in rng F ) by FUNCT_2:4; ::_thesis: verum
end;
hence  x in union (rng F) by TARSKI:def_4; ::_thesis: verum
end;

theorem Th21: :: MEASURE2:21
for X being set
for S being SigmaField of X
for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
F is Sep_Sequence of S
proof
let X be set ; ::_thesis: for S being SigmaField of X
for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
F is Sep_Sequence of S
let S be SigmaField of X; ::_thesis: for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
F is Sep_Sequence of S
let N, F be Function of NAT,S; ::_thesis: ( F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) implies F is Sep_Sequence of S )
assume A1: ( F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) ) ; ::_thesis: F is Sep_Sequence of S
 for n, m being set st n <> m holds
F . n misses F . m
proof
let n, m be set ; ::_thesis: ( n <> m implies F . n misses F . m )
assume A2: n <> m ; ::_thesis: F . n misses F . m
percases ( ( n in dom F & m in dom F ) or not n in dom F or not m in dom F ) ;
suppose ( n in dom F & m in dom F ) ; ::_thesis: F . n misses F . m
then reconsider n9 = n, m9 = m as Element of NAT ;
A3: ( m9 < n9 implies F . m misses F . n ) by A1, Th19;
 ( n9 < m9 implies F . n misses F . m ) by A1, Th19;
hence  F . n misses F . m by A2, A3, XXREAL_0:1; ::_thesis: verum
end;
suppose ( not n in dom F or not m in dom F ) ; ::_thesis: F . n misses F . m
then  ( F . n = {} or F . m = {} ) by FUNCT_1:def_2;
hence  F . n misses F . m by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence  F is Sep_Sequence of S by PROB_2:def_2; ::_thesis: verum
end;

theorem :: MEASURE2:22
for X being set
for S being SigmaField of X
for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) )
proof
let X be set ; ::_thesis: for S being SigmaField of X
for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) )
let S be SigmaField of X; ::_thesis: for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) )
let N, F be Function of NAT,S; ::_thesis: ( F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) implies ( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) ) )
assume that
A1: F . 0 = N . 0 and
A2: for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ; ::_thesis: ( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) )
 for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n)
proof
let n be Element of NAT ; ::_thesis: N . (n + 1) = (F . (n + 1)) \/ (N . n)
 F . (n + 1) = (N . (n + 1)) \ (N . n) by A2;
hence  N . (n + 1) = (F . (n + 1)) \/ (N . n) by A2, XBOOLE_1:45; ::_thesis: verum
end;
hence  ( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) ) by A1; ::_thesis: verum
end;

theorem :: MEASURE2:23
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Function of NAT,S st ( for n being Element of NAT holds F . n c= F . (n + 1) ) holds
M . (union (rng F)) = sup (rng (M * F))
proof
let X be set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being Function of NAT,S st ( for n being Element of NAT holds F . n c= F . (n + 1) ) holds
M . (union (rng F)) = sup (rng (M * F))
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for F being Function of NAT,S st ( for n being Element of NAT holds F . n c= F . (n + 1) ) holds
M . (union (rng F)) = sup (rng (M * F))
let M be sigma_Measure of S; ::_thesis: for F being Function of NAT,S st ( for n being Element of NAT holds F . n c= F . (n + 1) ) holds
M . (union (rng F)) = sup (rng (M * F))
let F be Function of NAT,S; ::_thesis: ( ( for n being Element of NAT holds F . n c= F . (n + 1) ) implies M . (union (rng F)) = sup (rng (M * F)) )
consider G being Function of NAT,S such that
A1: G . 0 = F . 0 and
A2: for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \ (F . n) by Th3;
assume A3: for n being Element of NAT holds F . n c= F . (n + 1) ; ::_thesis: M . (union (rng F)) = sup (rng (M * F))
then A4: G is Sep_Sequence of S by A1, A2, Th21;
A5: for m being set st m in NAT holds
(Ser (M * G)) . m = (M * F) . m
proof
defpred S1[ Element of NAT ] means (Ser (M * G)) . $1 = (M * F) . $1;
let m be set ; ::_thesis: ( m in NAT implies (Ser (M * G)) . m = (M * F) . m )
assume A6: m in NAT ; ::_thesis: (Ser (M * G)) . m = (M * F) . m
A7: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
A8: (M * G) . (m + 1) = M . (G . (m + 1)) by FUNCT_2:15;
A9: (M * F) . (m + 1) = M . (F . (m + 1)) by FUNCT_2:15;
A10: G . (m + 1) = (F . (m + 1)) \ (F . m) by A2;
assume  (Ser (M * G)) . m = (M * F) . m ; ::_thesis: S1[m + 1]
then (Ser (M * G)) . (m + 1) = ((M * F) . m) + ((M * G) . (m + 1)) by SUPINF_2:44
.= (M . (F . m)) + (M . (G . (m + 1))) by A8, FUNCT_2:15
.= M . ((F . m) \/ (G . (m + 1))) by A10, MEASURE1:30, XBOOLE_1:79
.= (M * F) . (m + 1) by A3, A9, A10, XBOOLE_1:45 ;
hence  S1[m + 1] ; ::_thesis: verum
end;
(Ser (M * G)) . 0 = (M * G) . 0 by SUPINF_2:44
.= M . (F . 0) by A1, FUNCT_2:15
.= (M * F) . 0 by FUNCT_2:15 ;
then A11: S1[ 0 ] ;
 for m being Element of NAT holds S1[m] from NAT_1:sch_1(A11, A7);
hence  (Ser (M * G)) . m = (M * F) . m by A6; ::_thesis: verum
end;
A12: ( dom (Ser (M * G)) = NAT & dom (M * F) = NAT ) by FUNCT_2:def_1;
M . (union (rng F)) = M . (union (rng G)) by A3, A1, A2, Th20
.= SUM (M * G) by A4, MEASURE1:def_6
.= sup (rng (M * F)) by A12, A5, FUNCT_1:2 ;
hence  M . (union (rng F)) = sup (rng (M * F)) ; ::_thesis: verum
end;