let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being Finite_Sep_Sequence of S holds M . (union (rng F)) = Sum (M * F)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for F being Finite_Sep_Sequence of S holds M . (union (rng F)) = Sum (M * F)
let M be sigma_Measure of S; :: thesis: for F being Finite_Sep_Sequence of S holds M . (union (rng F)) = Sum (M * F)
let F be Finite_Sep_Sequence of S; :: thesis: M . (union (rng F)) = Sum (M * F)
reconsider F1 = M * F as FinSequence of ExtREAL ;
consider f being Function of NAT ,ExtREAL such that
A1: ( Sum F1 = f . (len F1) & f . 0 = 0. & ( for i being Element of NAT st i < len F1 holds
f . (i + 1) = (f . i) + (F1 . (i + 1)) ) ) by CONVFUN1:def 5;
consider G being Sep_Sequence of S such that
A2: ( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds
F . n = G . n ) & ( for m being Nat st not m in dom F holds
G . m = {} ) ) by MESFUNC2:33;
A3: M . (union (rng F)) = SUM (M * G) by A2, MEASURE1:def 11
.= sup (rng (Ser (M * G))) ;
reconsider G1 = M * G as Num of rng (M * G) by SUPINF_2:def 16;
A4: Ser (M * G) = Ser (rng (M * G)),G1 by SUPINF_2:def 21;
then A5: ( (Ser (M * G)) . 0 = G1 . 0 & ( for n being Element of NAT
for y being R_eal st y = (Ser (M * G)) . n holds
(Ser (M * G)) . (n + 1) = y + (G1 . (n + 1)) ) ) by SUPINF_2:def 17;
not 0 in Seg (len F) by FINSEQ_1:3;
then not 0 in dom F by FINSEQ_1:def 3;
then A6: G . 0 = {} by A2;
A7: dom G = NAT by FUNCT_2:def 1;
then A8: (Ser (M * G)) . 0 = M . (G . 0 ) by A5, FUNCT_1:23
.= 0. by A6, VALUED_0:def 19 ;
A9: for i being Nat st i < len F1 holds
(Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + (F1 . (i + 1))
proof
let i be Nat; :: thesis: ( i < len F1 implies (Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + (F1 . (i + 1)) )
assume i < len F1 ; :: thesis: (Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + (F1 . (i + 1))
then ( 1 <= i + 1 & i + 1 <= len F1 ) by NAT_1:11, NAT_1:13;
then i + 1 in dom F1 by FINSEQ_3:27;
then A10: i + 1 in dom F by Th8;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
(Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + (G1 . (i + 1)) by A4, SUPINF_2:def 17
.= ((Ser (M * G)) . i) + (M . (G . (i + 1))) by A7, FUNCT_1:23
.= ((Ser (M * G)) . i) + (M . (F . (i + 1))) by A2, A10 ;
hence (Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + (F1 . (i + 1)) by A10, FUNCT_1:23; :: thesis: verum
end;
defpred S1[ Nat] means ( $1 <= len F1 implies (Ser (M * G)) . $1 = f . $1 );
A11: S1[ 0 ] by A1, A8;
A12: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A13: S1[k] ; :: thesis: S1[k + 1]
A14: for i being Nat st i < len F1 holds
f . (i + 1) = (f . i) + (F1 . (i + 1))
proof
let i be Nat; :: thesis: ( i < len F1 implies f . (i + 1) = (f . i) + (F1 . (i + 1)) )
i in NAT by ORDINAL1:def 13;
hence ( i < len F1 implies f . (i + 1) = (f . i) + (F1 . (i + 1)) ) by A1; :: thesis: verum
end;
assume k + 1 <= len F1 ; :: thesis: (Ser (M * G)) . (k + 1) = f . (k + 1)
then A15: k < len F1 by NAT_1:13;
then (Ser (M * G)) . (k + 1) = (f . k) + (F1 . (k + 1)) by A9, A13;
hence (Ser (M * G)) . (k + 1) = f . (k + 1) by A14, A15; :: thesis: verum
end;
A16: for k being Nat holds S1[k] from NAT_1:sch 2(A11, A12);
 defpred S2[ Nat] means ( $1 >= len F1 implies (Ser (M * G)) . $1 = (Ser (M * G)) . (len F1) );
A17: S2[ 0 ] ;
A18: M * G is nonnegative by MEASURE2:1;
A19: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A20: S2[k] ; :: thesis: S2[k + 1]
assume A21: k + 1 >= len F1 ; :: thesis: (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1)
reconsider k = k as Element of NAT by ORDINAL1:def 13;
now
per cases ( k >= len F1 or k < len F1 ) ;
case A22: k >= len F1 ; :: thesis: (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1)
then A23: (Ser (M * G)) . (k + 1) = ((Ser (M * G)) . (len F1)) + (G1 . (k + 1)) by A4, A20, SUPINF_2:def 17;
k + 1 > len F1 by A22, NAT_1:13;
then not k + 1 in Seg (len F1) by FINSEQ_1:3;
then not k + 1 in dom F1 by FINSEQ_1:def 3;
then A24: not k + 1 in dom F by Th8;
G1 . (k + 1) = M . (G . (k + 1)) by A7, FUNCT_1:23
.= M . {} by A2, A24
.= 0. by VALUED_0:def 19 ;
hence (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1) by A23, XXREAL_3:4; :: thesis: verum
end;
case k < len F1 ; :: thesis: (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1)
then k + 1 <= len F1 by NAT_1:13;
hence (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1) by A21, XXREAL_0:1; :: thesis: verum
end;
end;
end;
hence (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1) ; :: thesis: verum
end;
A25: for k being Nat holds S2[k] from NAT_1:sch 2(A17, A19);
 defpred S3[ Nat] means ( $1 < len F1 implies (Ser (M * G)) . ((len F1) - $1) <= (Ser (M * G)) . (len F1) );
A26: S3[ 0 ] ;
A27: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume A28: S3[k] ; :: thesis: S3[k + 1]
assume A29: k + 1 < len F1 ; :: thesis: (Ser (M * G)) . ((len F1) - (k + 1)) <= (Ser (M * G)) . (len F1)
then consider k' being Nat such that
A30: len F1 = (k + 1) + k' by NAT_1:10;
reconsider k' = k' as Element of NAT by ORDINAL1:def 13;
A31: k <= k + 1 by NAT_1:11;
(Ser (M * G)) . k' <= (Ser (M * G)) . (k' + 1) by A18, SUPINF_2:59;
hence (Ser (M * G)) . ((len F1) - (k + 1)) <= (Ser (M * G)) . (len F1) by A28, A29, A30, A31, XXREAL_0:2; :: thesis: verum
end;
A32: for i being Nat holds S3[i] from NAT_1:sch 2(A26, A27);
 A33: for i being Nat st i < len F1 holds
(Ser (M * G)) . i <= (Ser (M * G)) . (len F1)
proof
let i be Nat; :: thesis: ( i < len F1 implies (Ser (M * G)) . i <= (Ser (M * G)) . (len F1) )
assume i < len F1 ; :: thesis: (Ser (M * G)) . i <= (Ser (M * G)) . (len F1)
then consider k being Nat such that
A34: len F1 = i + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A35: ( k = (len F1) - i & i = (len F1) - k ) by A34;
len F1 <= (len F1) + i by NAT_1:11;
then A36: k <= len F1 by A35, XREAL_1:22;
(Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1)
proof
now
per cases ( k = len F1 or k < len F1 ) by A36, XXREAL_0:1;
case k = len F1 ; :: thesis: (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1)
hence (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1) by A8, A18, SUPINF_2:59; :: thesis: verum
end;
case k < len F1 ; :: thesis: (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1)
hence (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1) by A32; :: thesis: verum
end;
end;
end;
hence (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1) ; :: thesis: verum
end;
hence (Ser (M * G)) . i <= (Ser (M * G)) . (len F1) by A34; :: thesis: verum
end;
for z being ext-real number st z in rng (Ser (M * G)) holds
z <= (Ser (M * G)) . (len F1)
proof
let z be ext-real number ; :: thesis: ( z in rng (Ser (M * G)) implies z <= (Ser (M * G)) . (len F1) )
assume z in rng (Ser (M * G)) ; :: thesis: z <= (Ser (M * G)) . (len F1)
then consider n being set such that
A37: ( n in dom (Ser (M * G)) & z = (Ser (M * G)) . n ) by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A37;
now
per cases ( n < len F1 or n >= len F1 ) ;
case n < len F1 ; :: thesis: z <= (Ser (M * G)) . (len F1)
hence z <= (Ser (M * G)) . (len F1) by A33, A37; :: thesis: verum
end;
case n >= len F1 ; :: thesis: z <= (Ser (M * G)) . (len F1)
hence z <= (Ser (M * G)) . (len F1) by A25, A37; :: thesis: verum
end;
end;
end;
hence z <= (Ser (M * G)) . (len F1) ; :: thesis: verum
end;
then A38: (Ser (M * G)) . (len F1) is UpperBound of rng (Ser (M * G)) by XXREAL_2:def 1;
(Ser (M * G)) . (len F1) in rng (Ser (M * G))
proof
dom (Ser (M * G)) = NAT by FUNCT_2:def 1;
hence (Ser (M * G)) . (len F1) in rng (Ser (M * G)) by FUNCT_1:12; :: thesis: verum
end;
then (Ser (M * G)) . (len F1) = sup (rng (Ser (M * G))) by A38, XXREAL_2:55;
hence M . (union (rng F)) = Sum (M * F) by A1, A3, A16; :: thesis: verum