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

M . (union T) <= SUM (M * F)

let T be N_Measure_fam of S; :: thesis: for F being sequence of S st T = rng F holds

M . (union T) <= SUM (M * F)

let F be sequence of S; :: thesis: ( T = rng F implies M . (union T) <= 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

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

hence M . (union T) <= SUM (M * F) by A10, A6, A12, SUPINF_2:43; :: thesis: verum

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

M . (union T) <= SUM (M * F)

let T be N_Measure_fam of S; :: thesis: for F being sequence of S st T = rng F holds

M . (union T) <= SUM (M * F)

let F be sequence of S; :: thesis: ( T = rng F implies M . (union T) <= 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

then
H is Sep_Sequence of S
by PROB_2:def 2;
let n, m be object ; :: thesis: ( n <> m implies H . n misses H . m )

assume A4: n <> m ; :: thesis: H . n misses H . m

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

end;

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

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

A10:
for n being Element of NAT holds (M * H) . n <= (M * F) . n
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 )

hence H . n c= F . n by A2, A8; :: thesis: verum

end;A8: ( ex k being Nat st n = k + 1 implies H . n c= F . n )

proof

( n = 0 or ex k being Nat st n = k + 1 )
by NAT_1:6;
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;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

hence H . n c= F . n by A2, A8; :: thesis: verum

proof

A12:
union (rng H) = union (rng F)
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;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

proof

assume
T = rng F
; :: thesis: M . (union T) <= SUM (M * F)
thus
union (rng H) c= union (rng F)
:: according to XBOOLE_0:def 10 :: thesis: union (rng F) c= 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 A19, FUNCT_1:def 3;

ex s1 being Element of NAT st r in H . s1

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

let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in union (rng F) or r in union (rng H) )
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 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;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 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

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 A19, FUNCT_1:def 3;

ex s1 being Element of NAT st r in H . s1

proof

then consider s1 being Element of NAT such that
defpred S_{1}[ Nat] means r in F . $1;

A21: ex k being Nat st S_{1}[k]
by A18, A20;

ex k being Nat st

( S_{1}[k] & ( for n being Nat st S_{1}[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 )

hence ex s1 being Element of NAT st r in H . s1 by A24, NAT_1:6; :: thesis: verum

end;A21: ex k being Nat st S

ex k being Nat st

( S

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

( k = 0 implies ex s1 being Element of NAT st r in H . s1 )
by A2, A22;
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

hence ( k is Element of NAT & r in H . k ) by A22, A25, A26, XBOOLE_0:def 5; :: thesis: verum

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

H . (l + 1) = (F . (l + 1)) \ (G . l)
by A3;
assume
r in G . l
; :: thesis: contradiction

then consider i being 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;then consider i being 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

hence ( k is Element of NAT & r in H . k ) by A22, A25, A26, XBOOLE_0:def 5; :: thesis: verum

hence ex s1 being Element of NAT st r in H . s1 by A24, NAT_1:6; :: thesis: verum

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

hence M . (union T) <= SUM (M * F) by A10, A6, A12, SUPINF_2:43; :: thesis: verum