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
proof
defpred S1[ 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 S1[m] holds
S1[m + 1]
proof
let m be 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;
A11: m in NAT by ORDINAL1:def 12;
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:def 11
.= (M . (F . m)) + (M . (G . (m + 1))) by
.= M . ((F . m) \/ (G . (m + 1))) by
.= (M * F) . (m + 1) by ;
hence S1[m + 1] ; :: thesis: verum
end;
(Ser (M * G)) . 0 = (M * G) . 0 by SUPINF_2:def 11
.= M . (F . 0) by
.= (M * F) . 0 by FUNCT_2:15 ;
then A12: S1[ 0 ] ;
for m being Nat holds S1[m] from NAT_1:sch 2(A12, A7);
hence (Ser (M * G)) . m = (M * F) . m by A6; :: thesis: verum
end;
A13: ( 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
.= sup (rng (M * F)) by ;
hence M . (union (rng F)) = sup (rng (M * F)) ; :: thesis: verum