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 sequence of ExtREAL such that
A1: Sum F1 = f . (len F1) and
A2: f . 0 = 0. and
A3: for i being Nat st i < len F1 holds
f . (i + 1) = (f . i) + (F1 . (i + 1)) by EXTREAL1:def 2;
consider G being Sep_Sequence of S such that
A4: union (rng F) = union (rng G) and
A5: for n being Nat st n in dom F holds
F . n = G . n and
A6: for m being Nat st not m in dom F holds
G . m = {} by MESFUNC2:30;
defpred S1[ Nat] means ( $1 <= len F1 implies (Ser (M * G)) . $1 = f . $1 );
set G1 = M * G;
A7: dom G = NAT by FUNCT_2:def 1;
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:25;
then A10: i + 1 in dom F by Th8;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A11: i + 1 in NAT by ORDINAL1:def 12;
(Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + ((M * G) . (i + 1)) by SUPINF_2:def 11
.= ((Ser (M * G)) . i) + (M . (G . (i + 1))) by A7, FUNCT_1:13, A11
.= ((Ser (M * G)) . i) + (M . (F . (i + 1))) by A5, A10 ;
hence (Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + (F1 . (i + 1)) by A10, FUNCT_1:13; :: thesis: verum
end;
A12: for k being Nat st S1[k] holds
S1[k + 1]
proof
A13: for i being Nat st i < len F1 holds
f . (i + 1) = (f . i) + (F1 . (i + 1)) by A3;
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A14: S1[k] ; :: thesis: S1[k + 1]
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, A14;
hence (Ser (M * G)) . (k + 1) = f . (k + 1) by A13, A15; :: thesis: verum
end;
defpred S2[ Nat] means ( $1 >= len F1 implies (Ser (M * G)) . $1 = (Ser (M * G)) . (len F1) );
A16: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A17: S2[k] ; :: thesis: S2[k + 1]
assume A18: 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 12;
now :: thesis: ( ( k >= len F1 & (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1) ) or ( k < len F1 & (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1) ) )
per cases ( k >= len F1 or k < len F1 ) ;
case A19: k >= len F1 ; :: thesis: (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1)
then k + 1 > len F1 by NAT_1:13;
then not k + 1 in Seg (len F1) by FINSEQ_1:1;
then not k + 1 in dom F1 by FINSEQ_1:def 3;
then A20: not k + 1 in dom F by Th8;
k + 1 in NAT by ORDINAL1:def 12;
then A21: (M * G) . (k + 1) = M . (G . (k + 1)) by A7, FUNCT_1:13
.= M . {} by A6, A20
.= 0. by VALUED_0:def 19 ;
(Ser (M * G)) . (k + 1) = ((Ser (M * G)) . (len F1)) + ((M * G) . (k + 1)) by A17, A19, SUPINF_2:def 11;
hence (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1) by A21, 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 A18, XXREAL_0:1; :: thesis: verum
end;
end;
end;
hence (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1) ; :: thesis: verum
end;
defpred S3[ Nat] means ( $1 < len F1 implies (Ser (M * G)) . ((len F1) - $1) <= (Ser (M * G)) . (len F1) );
A22: M * G is nonnegative by MEASURE2:1;
A23: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume A24: S3[k] ; :: thesis: S3[k + 1]
assume A25: k + 1 < len F1 ; :: thesis: (Ser (M * G)) . ((len F1) - (k + 1)) <= (Ser (M * G)) . (len F1)
then consider k9 being Nat such that
A26: len F1 = (k + 1) + k9 by NAT_1:10;
reconsider k9 = k9 as Element of NAT by ORDINAL1:def 12;
( k <= k + 1 & (Ser (M * G)) . k9 <= (Ser (M * G)) . (k9 + 1) ) by A22, NAT_1:11, SUPINF_2:40;
hence (Ser (M * G)) . ((len F1) - (k + 1)) <= (Ser (M * G)) . (len F1) by A24, A25, A26, XXREAL_0:2; :: thesis: verum
end;
not 0 in Seg (len F) by FINSEQ_1:1;
then not 0 in dom F by FINSEQ_1:def 3;
then A27: G . 0 = {} by A6;
(Ser (M * G)) . 0 = (M * G) . 0 by SUPINF_2:def 11;
then A28: (Ser (M * G)) . 0 = M . (G . 0) by A7, FUNCT_1:13
.= 0. by A27, VALUED_0:def 19 ;
then A29: S1[ 0 ] by A2;
A30: for k being Nat holds S1[k] from NAT_1:sch 2(A29, A12);
 A31: S3[ 0 ] ;
A32: for i being Nat holds S3[i] from NAT_1:sch 2(A31, A23);
 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) )
A34: len F1 <= (len F1) + i by NAT_1:11;
assume i < len F1 ; :: thesis: (Ser (M * G)) . i <= (Ser (M * G)) . (len F1)
then consider k being Nat such that
A35: len F1 = i + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
k = (len F1) - i by A35;
then A36: k <= len F1 by A34, XREAL_1:20;
(Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1)
proof
now :: thesis: ( ( k = len F1 & (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1) ) or ( k < len F1 & (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1) ) )
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 A28, A22, SUPINF_2:40; :: 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 A35; :: thesis: verum
end;
A37: S2[ 0 ] ;
A38: for k being Nat holds S2[k] from NAT_1:sch 2(A37, A16);
 for z being ExtReal st z in rng (Ser (M * G)) holds
z <= (Ser (M * G)) . (len F1)
proof
let z be ExtReal; :: 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 object such that
A39: n in dom (Ser (M * G)) and
A40: z = (Ser (M * G)) . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A39;
now :: thesis: ( ( n < len F1 & z <= (Ser (M * G)) . (len F1) ) or ( n >= len F1 & z <= (Ser (M * G)) . (len F1) ) )
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, A40; :: thesis: verum
end;
case n >= len F1 ; :: thesis: z <= (Ser (M * G)) . (len F1)
hence z <= (Ser (M * G)) . (len F1) by A38, A40; :: thesis: verum
end;
end;
end;
hence z <= (Ser (M * G)) . (len F1) ; :: thesis: verum
end;
then A41: (Ser (M * G)) . (len F1) is UpperBound of rng (Ser (M * G)) by XXREAL_2:def 1;
dom (Ser (M * G)) = NAT by FUNCT_2:def 1;
then A42: (Ser (M * G)) . (len F1) = sup (rng (Ser (M * G))) by A41, FUNCT_1:3, XXREAL_2:55;
M . (union (rng F)) = SUM (M * G) by A4, MEASURE1:def 6
.= sup (rng (Ser (M * G))) ;
hence M . (union (rng F)) = Sum (M * F) by A1, A30, A42; :: thesis: verum