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 Th56;
reconsider XSeq = ASeq as SetSequence of Omega ;
A3: ( ( for k being Nat st k in dom FSeq holds
XSeq . k = FSeq . k ) & ( for k being Nat st not k in dom FSeq holds
XSeq . k = {} ) ) by A1, A2;
then P . (Union ASeq) = P . (Union FSeq) by Th55;
then P . (Union FSeq) <= Sum (P * ASeq) by A1, A2, Th64;
hence P . (Union FSeq) <= Sum (P * FSeq) by A1, A2, Th64; :: thesis: ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) )
assume A4: FSeq is disjoint_valued ; :: thesis: P . (Union FSeq) = Sum (P * FSeq)
A5: ( FSeq is disjoint_valued implies ASeq is disjoint_valued )

proof

assume A6: FSeq is disjoint_valued ; :: thesis: ASeq is disjoint_valued
for m, n being Nat st m <> n holds
ASeq . m misses ASeq . n

proof

let m, n be Nat; :: thesis: ( m <> n implies ASeq . m misses ASeq . n )
assume A7: 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 A8: ( m in dom FSeq & n in dom FSeq ) ; :: thesis: ASeq . m misses ASeq . n

FSeq . m misses FSeq . n by A6, A7, PROB_2:def 2;
then ASeq . m misses FSeq . n by A1, A8;
hence ASeq . m misses ASeq . n by A1, A8; :: 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 ; :: thesis: verum

end;

end;

end;

hence ASeq is disjoint_valued ; :: thesis: verum

end;

thus P . (Union FSeq) = P . (Union ASeq) by Th55, A3
.= Sum (P * ASeq) by A5, A4, Th46
.= Sum (P * FSeq) by A1, A2, Th64 ; :: thesis: verum