let X be set ; :: thesis: for S being semialgebra_of_sets of X
for P being pre-Measure of S
for A being set
for F1, F2 being disjoint_valued FinSequence of S st A = Union F1 & A = Union F2 holds
Sum (P * F1) = Sum (P * F2)
let S be semialgebra_of_sets of X; :: thesis: for P being pre-Measure of S
for A being set
for F1, F2 being disjoint_valued FinSequence of S st A = Union F1 & A = Union F2 holds
Sum (P * F1) = Sum (P * F2)
let P be pre-Measure of S; :: thesis: for A being set
for F1, F2 being disjoint_valued FinSequence of S st A = Union F1 & A = Union F2 holds
Sum (P * F1) = Sum (P * F2)
let A be set ; :: thesis: for F1, F2 being disjoint_valued FinSequence of S st A = Union F1 & A = Union F2 holds
Sum (P * F1) = Sum (P * F2)

hereby :: thesis: verum

let F1, F2 be disjoint_valued FinSequence of S; :: thesis: ( A = Union F1 & A = Union F2 implies Sum (P * b₁) = Sum (P * b₂) )
assume A1: ( A = Union F1 & A = Union F2 ) ; :: thesis: Sum (P * b₁) = Sum (P * b₂)
consider SMF1 being Function of NAT,ExtREAL such that
A2: ( Sum (P * F1) = SMF1 . (len (P * F1)) & SMF1 . 0 = 0 & ( for i being Nat st i < len (P * F1) holds
SMF1 . (i + 1) = (SMF1 . i) + ((P * F1) . (i + 1)) ) ) by EXTREAL1:def 2;
consider SMF2 being Function of NAT,ExtREAL such that
A3: ( Sum (P * F2) = SMF2 . (len (P * F2)) & SMF2 . 0 = 0 & ( for i being Nat st i < len (P * F2) holds
SMF2 . (i + 1) = (SMF2 . i) + ((P * F2) . (i + 1)) ) ) by EXTREAL1:def 2;
dom P = S by FUNCT_2:def 1;
then ( rng F1 c= dom P & rng F2 c= dom P ) ;
then A4: ( dom (P * F1) = dom F1 & dom (P * F2) = dom F2 ) by RELAT_1:27;
then A5: ( dom (P * F1) = Seg (len F1) & dom (P * F2) = Seg (len F2) & len (P * F1) = len F1 & len (P * F2) = len F2 ) by FINSEQ_1:def 3, FINSEQ_3:29;

per cases ( len (P * F1) = 0 or len (P * F2) = 0 or ( len (P * F1) <> 0 & len (P * F2) <> 0 ) ) ;

suppose A6: len (P * F1) = 0 ; :: thesis: Sum (P * b₁) = Sum (P * b₂)

then P * F1 = {} ;
then F1 = {} by A4;
then rng F1 = {} ;
then Union F2 = {} by A1, CARD_3:def 4, ZFMISC_1:2;
then A7: union (rng F2) = {} by CARD_3:def 4;
defpred S₁[ Nat] means ( $1 <= len (P * F2) implies SMF2 . $1 = 0 );
A8: S₁[ 0 ] by A3;
A9: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A10: S₁[i] ; :: thesis: S₁[i + 1]
assume A11: i + 1 <= len (P * F2) ; :: thesis: SMF2 . (i + 1) = 0
then A13: ( SMF2 . (i + 1) = (SMF2 . i) + ((P * F2) . (i + 1)) & SMF2 . i = 0 ) by A3, A10, NAT_1:13;
A14: i + 1 in dom (P * F2) by A11, NAT_1:11, FINSEQ_3:25;
then F2 . (i + 1) = {} by A4, A7, ORDERS_1:6, FUNCT_1:3;
then P . (F2 . (i + 1)) = 0 by VALUED_0:def 19;
then (P * F2) . (i + 1) = 0 by A14, FUNCT_1:12;
hence SMF2 . (i + 1) = 0 by A13; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A8, A9);
hence Sum (P * F1) = Sum (P * F2) by A2, A3, A6; :: thesis: verum

end;

suppose B6: len (P * F2) = 0 ; :: thesis: Sum (P * b₁) = Sum (P * b₂)

then P * F2 = {} ;
then F2 = {} by A4;
then rng F2 = {} ;
then Union F1 = {} by A1, CARD_3:def 4, ZFMISC_1:2;
then B7: union (rng F1) = {} by CARD_3:def 4;
defpred S₁[ Nat] means ( $1 <= len (P * F1) implies SMF1 . $1 = 0 );
B8: S₁[ 0 ] by A2;
B9: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume B10: S₁[i] ; :: thesis: S₁[i + 1]
assume B11: i + 1 <= len (P * F1) ; :: thesis: SMF1 . (i + 1) = 0
then B13: ( SMF1 . (i + 1) = (SMF1 . i) + ((P * F1) . (i + 1)) & SMF1 . i = 0 ) by A2, B10, NAT_1:13;
B14: i + 1 in dom (P * F1) by B11, NAT_1:11, FINSEQ_3:25;
then F1 . (i + 1) = {} by A4, B7, ORDERS_1:6, FUNCT_1:3;
then P . (F1 . (i + 1)) = 0 by VALUED_0:def 19;
then (P * F1) . (i + 1) = 0 by B14, FUNCT_1:12;
hence SMF1 . (i + 1) = 0 by B13; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(B8, B9);
hence Sum (P * F1) = Sum (P * F2) by A2, A3, B6; :: thesis: verum

end;

suppose A15: ( len (P * F1) <> 0 & len (P * F2) <> 0 ) ; :: thesis: Sum (P * b₁) = Sum (P * b₂)

defpred S₁[ Nat, Nat, set ] means $3 = P . ((F1 . $1) /\ (F2 . $2));
MX0: for i, j being Nat st [i,j] in [:(Seg (len F1)),(Seg (len F2)):] holds
ex A being Element of ExtREAL st S₁[i,j,A] ;
consider Mx being Matrix of len F1, len F2,ExtREAL such that
MX1: for i, j being Nat st [i,j] in Indices Mx holds
S₁[i,j,Mx * (i,j)] from MATRIX_0:sch 2(MX0);
C3: len Mx = len F1 by MATRIX_0:def 2;
then C4: width Mx = len F2 by A15, A5, MATRIX_0:20;
CC0: for F being disjoint_valued FinSequence of S st Union F in S holds
P . (Union F) = Sum (P * F) by Def8;
( not F1 is empty & not F2 is empty ) by A15;
then C10: ( Sum (P * F1) = SumAll Mx & Sum (P * F2) = SumAll (Mx @) ) by A1, MX1, CC0, Th40, Th41;
for i being Nat st i in dom Mx holds
not -infty in rng (Mx . i)

proof

let i be Nat; :: thesis: ( i in dom Mx implies not -infty in rng (Mx . i) )
assume F1: i in dom Mx ; :: thesis: not -infty in rng (Mx . i)
assume -infty in rng (Mx . i) ; :: thesis: contradiction
then consider j being object such that
F2: ( j in dom (Mx . i) & (Mx . i) . j = -infty ) by FUNCT_1:def 3;
reconsider j = j as Nat by F2;
F3: [i,j] in Indices Mx by F1, F2, MATRPROB:13;
then (Mx . i) . j = Mx * (i,j) by MATRPROB:14;
then F5: (Mx . i) . j = P . ((F1 . i) /\ (F2 . j)) by F3, MX1;
( i in Seg (len Mx) & j in Seg (width Mx) ) by F3, MATRPROB:12;
then ( i in dom F1 & j in dom F2 ) by C3, C4, FINSEQ_1:def 3;
then ( F1 . i in rng F1 & F2 . j in rng F2 ) by FUNCT_1:3;
then (F1 . i) /\ (F2 . j) in S by FINSUB_1:def 2;
hence contradiction by F2, F5, MEASURE1:def 2; :: thesis: verum

end;

hence Sum (P * F1) = Sum (P * F2) by C10, Th28; :: thesis: verum

end;

end;

end;