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 V77() )

.= Sum (P * ASeq) by A5, A4, Th46

.= Sum (P * FSeq) by A1, A2, Th64 ; :: thesis: verum

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 V77() )

proof

thus P . (Union FSeq) =
P . (Union ASeq)
by Th55, A3
assume A6:
FSeq is disjoint_valued
; :: thesis: ASeq is V77()

for m, n being Nat st m <> n holds

ASeq . m misses ASeq . n

end;for m, n being Nat st m <> n holds

ASeq . m misses ASeq . n

proof

hence
ASeq is V77()
; :: thesis: verum
let m, n be Nat; :: thesis: ( m <> n implies ASeq . m misses ASeq . n )

assume A7: m <> n ; :: thesis: ASeq . m misses ASeq . n

end;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 )
;

end;

.= Sum (P * ASeq) by A5, A4, Th46

.= Sum (P * FSeq) by A1, A2, Th64 ; :: thesis: verum