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 S₁[ 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₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[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₁[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₁[m + 1] ; :: thesis: verum

end;

(Ser (M * G)) . 0 = (M * G) . 0 by SUPINF_2:def 11
.= M . (F . 0) by A1, FUNCT_2:15
.= (M * F) . 0 by FUNCT_2:15 ;
then A12: S₁[ 0 ] ;
for m being Nat holds S₁[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 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