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)) )
assume A1: for n being Element of NAT holds F . n c= F . (n + 1) ; :: thesis: M . (union (rng F)) = sup (rng (M * F))
consider G being Function of NAT ,S such that
A2: ( G . 0 = F . 0 & ( for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \ (F . n) ) ) by Th4;
A3: G is Sep_Sequence of S by A1, A2, Th25;
A4: rng (Ser (M * G)) = rng (M * F)

proof

A5: ( dom (Ser (M * G)) = NAT & dom (M * F) = NAT ) by FUNCT_2:def 1;
for m being set st m in NAT holds
(Ser (M * G)) . m = (M * F) . m

proof

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
defpred S₁[ Element of NAT ] means (Ser (M * G)) . $1 = (M * F) . $1;
A7: S₁[ 0 ]

proof

thus (Ser (M * G)) . 0 = (M * G) . 0 by SUPINF_2:63
.= M . (F . 0 ) by A2, FUNCT_2:21
.= (M * F) . 0 by FUNCT_2:21 ; :: thesis: verum

end;

A8: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A9: (Ser (M * G)) . m = (M * F) . m ; :: thesis: S₁[m + 1]
A10: ( (M * G) . (m + 1) = M . (G . (m + 1)) & (M * F) . (m + 1) = M . (F . (m + 1)) ) by FUNCT_2:21;
A11: ( G . (m + 1) = (F . (m + 1)) \ (F . m) & F . m c= F . (m + 1) ) by A1, A2;
(Ser (M * G)) . (m + 1) = ((M * F) . m) + ((M * G) . (m + 1)) by A9, SUPINF_2:63
.= (M . (F . m)) + (M . (G . (m + 1))) by A10, FUNCT_2:21
.= M . ((F . m) \/ (G . (m + 1))) by A11, MEASURE1:61, XBOOLE_1:79
.= (M * F) . (m + 1) by A10, A11, XBOOLE_1:45 ;
hence S₁[m + 1] ; :: thesis: verum

end;

for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A7, A8);
hence (Ser (M * G)) . m = (M * F) . m by A6; :: thesis: verum

end;

hence rng (Ser (M * G)) = rng (M * F) by A5, FUNCT_1:9; :: thesis: verum

end;

M . (union (rng F)) = M . (union (rng G)) by A1, A2, Th24
.= SUM (M * G) by A3, MEASURE1:def 11
.= sup (rng (M * F)) by A4 ;
hence M . (union (rng F)) = sup (rng (M * F)) ; :: thesis: verum