let X be set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for F being sequence of S st ( for n being 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 sequence of S st ( for n being 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 sequence of S st ( for n being Nat holds F . n c= F . (n + 1) ) holds

M . (union (rng F)) = sup (rng (M * F))

let F be sequence of S; :: thesis: ( ( for n being Nat holds F . n c= F . (n + 1) ) implies M . (union (rng F)) = sup (rng (M * F)) )

consider G being sequence of S such that

A1: G . 0 = F . 0 and

A2: for n being Nat holds G . (n + 1) = (F . (n + 1)) \ (F . n) by Th3;

assume A3: for n being 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 object st m in NAT holds

(Ser (M * G)) . m = (M * F) . m

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 A13, A5, FUNCT_1:2 ;

hence M . (union (rng F)) = sup (rng (M * F)) ; :: thesis: verum

for M being sigma_Measure of S

for F being sequence of S st ( for n being 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 sequence of S st ( for n being 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 sequence of S st ( for n being Nat holds F . n c= F . (n + 1) ) holds

M . (union (rng F)) = sup (rng (M * F))

let F be sequence of S; :: thesis: ( ( for n being Nat holds F . n c= F . (n + 1) ) implies M . (union (rng F)) = sup (rng (M * F)) )

consider G being sequence of S such that

A1: G . 0 = F . 0 and

A2: for n being Nat holds G . (n + 1) = (F . (n + 1)) \ (F . n) by Th3;

assume A3: for n being 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 object st m in NAT holds

(Ser (M * G)) . m = (M * F) . m

proof

A13:
( dom (Ser (M * G)) = NAT & dom (M * F) = NAT )
by FUNCT_2:def 1;
defpred S_{1}[ Nat] means (Ser (M * G)) . $1 = (M * F) . $1;

let m be object ; :: 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 Nat st S_{1}[m] holds

S_{1}[m + 1]

.= M . (F . 0) by A1, FUNCT_2:15

.= (M * F) . 0 by FUNCT_2:15 ;

then A12: S_{1}[ 0 ]
;

for m being Nat holds S_{1}[m]
from NAT_1:sch 2(A12, A7);

hence (Ser (M * G)) . m = (M * F) . m by A6; :: thesis: verum

end;let m be object ; :: 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 Nat st S

S

proof

(Ser (M * G)) . 0 =
(M * G) . 0
by SUPINF_2:def 11
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[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;

A11: m in NAT by ORDINAL1:def 12;

assume (Ser (M * G)) . m = (M * F) . m ; :: thesis: S_{1}[m + 1]

then (Ser (M * G)) . (m + 1) = ((M * F) . m) + ((M * G) . (m + 1)) by SUPINF_2:def 11

.= (M . (F . m)) + (M . (G . (m + 1))) by A8, FUNCT_2:15, A11

.= 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 S_{1}[m + 1]
; :: thesis: verum

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

A11: m in NAT by ORDINAL1:def 12;

assume (Ser (M * G)) . m = (M * F) . m ; :: thesis: S

then (Ser (M * G)) . (m + 1) = ((M * F) . m) + ((M * G) . (m + 1)) by SUPINF_2:def 11

.= (M . (F . m)) + (M . (G . (m + 1))) by A8, FUNCT_2:15, A11

.= 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 S

.= M . (F . 0) by A1, FUNCT_2:15

.= (M * F) . 0 by FUNCT_2:15 ;

then A12: S

for m being Nat holds S

hence (Ser (M * G)) . m = (M * F) . m by A6; :: thesis: verum

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 A13, A5, FUNCT_1:2 ;

hence M . (union (rng F)) = sup (rng (M * F)) ; :: thesis: verum