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 sequence of S st T = rng F holds
M . () <= 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 sequence of S st T = rng F holds
M . () <= SUM (M * F)

let M be sigma_Measure of S; :: thesis: for T being N_Measure_fam of S
for F being sequence of S st T = rng F holds
M . () <= SUM (M * F)

let T be N_Measure_fam of S; :: thesis: for F being sequence of S st T = rng F holds
M . () <= SUM (M * F)

let F be sequence of S; :: thesis: ( T = rng F implies M . () <= SUM (M * F) )
consider G being sequence of S such that
A1: ( G . 0 = F . 0 & ( for n being Nat holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ) ) by Th4;
consider H being sequence of S such that
A2: H . 0 = F . 0 and
A3: for n being Nat holds H . (n + 1) = (F . (n + 1)) \ (G . n) by Th8;
for n, m being object st n <> m holds
H . n misses H . m
proof
let n, m be object ; :: thesis: ( n <> m implies H . n misses H . m )
assume A4: n <> m ; :: thesis: H . n misses H . m
per cases ( ( 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 ; :: 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 ; :: 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 ; :: 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 object ; :: 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 object such that
A15: s in dom H and
A16: E = H . s by ;
reconsider s = s as Element of NAT by A15;
A17: F . s in rng F by FUNCT_2:4;
E c= F . s by ;
hence r in union (rng F) by ; :: thesis: verum
end;
let r be object ; :: 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 object st
( s in dom F & E = F . s ) by ;
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 ;
ex k being Nat st
( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from 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 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 Nat such that
A27: i <= l and
A28: r in F . i by ;
k <= i by ;
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 NAT & r in H . k ) by ; :: thesis: verum
end;
( k = 0 implies ex s1 being Element of NAT st r in H . s1 ) by ;
hence ex s1 being Element of NAT st r in H . s1 by ; :: 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 ; :: thesis: verum
end;
assume T = rng F ; :: thesis: M . () <= SUM (M * F)
hence M . () <= SUM (M * F) by ; :: thesis: verum