let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds
( P . (Union FSeq) <= Sum (P * FSeq) & ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) )
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds
( P . (Union FSeq) <= Sum (P * FSeq) & ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) )
let P be Probability of Sigma; :: thesis: for FSeq being FinSequence of Sigma holds
( P . (Union FSeq) <= Sum (P * FSeq) & ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) )
let FSeq be FinSequence of Sigma; :: thesis: ( P . (Union FSeq) <= Sum (P * FSeq) & ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) )
consider ASeq being SetSequence of Sigma such that
A1: for k being Nat st k in dom FSeq holds
ASeq . k = FSeq . k and
A2: for k being Nat st not k in dom FSeq holds
ASeq . k = {} by Th61;
P . (Union ASeq) = P . (Union FSeq) by A1, A2, Th60;
then P . (Union FSeq) <= Sum (P * ASeq) by A1, A2, Th69;
hence P . (Union FSeq) <= Sum (P * FSeq) by A1, A2, Th69; :: thesis: ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) )
assume A3: FSeq is disjoint_valued ; :: thesis: P . (Union FSeq) = Sum (P * FSeq)
A4: ( FSeq is disjoint_valued implies ASeq is disjoint_valued )

proof

assume A5: FSeq is disjoint_valued ; :: thesis: ASeq is disjoint_valued
for m, n being Element of NAT st m <> n holds
ASeq . m misses ASeq . n

proof

let m, n be Element of NAT ; :: thesis: ( m <> n implies ASeq . m misses ASeq . n )
assume A6: m <> n ; :: thesis: ASeq . m misses ASeq . n

per cases ( ( m in dom FSeq & n in dom FSeq ) or not m in dom FSeq or not n in dom FSeq ) ;

suppose A7: ( m in dom FSeq & n in dom FSeq ) ; :: thesis: ASeq . m misses ASeq . n

FSeq . m misses FSeq . n by A5, A6, PROB_2:def 2;
then ASeq . m misses FSeq . n by A1, A7;
hence ASeq . m misses ASeq . n by A1, A7; :: thesis: verum

end;

suppose ( not m in dom FSeq or not n in dom FSeq ) ; :: thesis: ASeq . m misses ASeq . n

then ( ASeq . m = {} or ASeq . n = {} ) by A2;
hence ASeq . m misses ASeq . n by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

hence ASeq is disjoint_valued by PROB_2:def 3; :: thesis: verum

end;

thus P . (Union FSeq) = P . (Union ASeq) by A1, A2, Th60
.= Sum (P * ASeq) by A4, A3, Th51
.= Sum (P * FSeq) by A1, A2, Th69 ; :: thesis: verum