let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B being non empty Subset of Sigma
for b being Element of B
for f being SetSequence of Sigma st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is disjoint_valued holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for B being non empty Subset of Sigma
for b being Element of B
for f being SetSequence of Sigma st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is disjoint_valued holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
let P be Probability of Sigma; :: thesis: for B being non empty Subset of Sigma
for b being Element of B
for f being SetSequence of Sigma st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is disjoint_valued holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
let B be non empty Subset of Sigma; :: thesis: for b being Element of B
for f being SetSequence of Sigma st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is disjoint_valued holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
let b be Element of B; :: thesis: for f being SetSequence of Sigma st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is disjoint_valued holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
let f be SetSequence of Sigma; :: thesis: ( ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is disjoint_valued implies P . (b /\ (Union f)) = (P . b) * (P . (Union f)) )
reconsider b = b as Element of Sigma ;
reconsider r = P . b as Real ;
for n being Nat holds (seqIntersection (b,f)) . n is Event of Sigma

proof

let n be Nat; :: thesis: (seqIntersection (b,f)) . n is Event of Sigma
A1: n in NAT by ORDINAL1:def 12;
b /\ (f . n) is Event of Sigma ;
hence (seqIntersection (b,f)) . n is Event of Sigma by DYNKIN:def 1, A1; :: thesis: verum

end;

then reconsider seqIntf = seqIntersection (b,f) as SetSequence of Sigma by PROB_1:25;
for n being Nat holds (seqIntersection (b,(Partial_Union f))) . n is Event of Sigma

proof

let n be Nat; :: thesis: (seqIntersection (b,(Partial_Union f))) . n is Event of Sigma
A2: n in NAT by ORDINAL1:def 12;
b /\ ((Partial_Union f) . n) is Event of Sigma ;
hence (seqIntersection (b,(Partial_Union f))) . n is Event of Sigma by DYNKIN:def 1, A2; :: thesis: verum

end;

then reconsider seqIntPf = seqIntersection (b,(Partial_Union f)) as SetSequence of Sigma by PROB_1:25;
A3: b /\ (Union f) = b /\ (Union (Partial_Union f)) by PROB_3:15
.= Union seqIntPf by DYNKIN:10 ;
assume A4: for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ; :: thesis: ( not f is disjoint_valued or P . (b /\ (Union f)) = (P . b) * (P . (Union f)) )

now :: thesis: for n being Element of NAT holds (P * seqIntf) . n = (r (#) (P * f)) . n

let n be Element of NAT ; :: thesis: (P * seqIntf) . n = (r (#) (P * f)) . n
thus (P * seqIntf) . n = P . (seqIntf . n) by FUNCT_2:15
.= P . ((f . n) /\ b) by DYNKIN:def 1
.= (P . (f . n)) * (P . b) by A4
.= ((P * f) . n) * r by FUNCT_2:15
.= (r (#) (P * f)) . n by SEQ_1:9 ; :: thesis: verum

end;

then A5: P * seqIntf = r (#) (P * f) by FUNCT_2:def 7;
A6: for x being set
for n, m being Element of NAT st n <= m & x in (Partial_Union f) . n holds
x in (Partial_Union f) . m

proof

let x be set ; :: thesis: for n, m being Element of NAT st n <= m & x in (Partial_Union f) . n holds
x in (Partial_Union f) . m
reconsider Pf = Partial_Union f as SetSequence of Sigma ;
let n, m be Element of NAT ; :: thesis: ( n <= m & x in (Partial_Union f) . n implies x in (Partial_Union f) . m )
assume A7: n <= m ; :: thesis: ( not x in (Partial_Union f) . n or x in (Partial_Union f) . m )
assume A8: x in (Partial_Union f) . n ; :: thesis: x in (Partial_Union f) . m
Pf is non-descending by PROB_3:11;
then Pf . n c= Pf . m by A7;
hence x in (Partial_Union f) . m by A8; :: thesis: verum

end;

for n, m being Nat st n <= m holds
(seqIntersection (b,(Partial_Union f))) . n c= (seqIntersection (b,(Partial_Union f))) . m

proof

let n, m be Nat; :: thesis: ( n <= m implies (seqIntersection (b,(Partial_Union f))) . n c= (seqIntersection (b,(Partial_Union f))) . m )
assume A9: n <= m ; :: thesis: (seqIntersection (b,(Partial_Union f))) . n c= (seqIntersection (b,(Partial_Union f))) . m
A10: m in NAT by ORDINAL1:def 12;
A11: n in NAT by ORDINAL1:def 12;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (seqIntersection (b,(Partial_Union f))) . n or x in (seqIntersection (b,(Partial_Union f))) . m )
assume x in (seqIntersection (b,(Partial_Union f))) . n ; :: thesis: x in (seqIntersection (b,(Partial_Union f))) . m
then A12: x in b /\ ((Partial_Union f) . n) by DYNKIN:def 1, A11;
then x in (Partial_Union f) . n by XBOOLE_0:def 4;
then A13: x in (Partial_Union f) . m by A6, A9, A11, A10;
x in b by A12, XBOOLE_0:def 4;
then x in b /\ ((Partial_Union f) . m) by A13, XBOOLE_0:def 4;
hence x in (seqIntersection (b,(Partial_Union f))) . m by DYNKIN:def 1, A10; :: thesis: verum

end;

then A14: seqIntersection (b,(Partial_Union f)) is non-descending ;
assume A15: f is disjoint_valued ; :: thesis: P . (b /\ (Union f)) = (P . b) * (P . (Union f))
then A16: seqIntersection (b,f) is disjoint_valued by DYNKIN:9;
for n being Element of NAT holds (Partial_Union seqIntf) . n = (seqIntersection (b,(Partial_Union f))) . n

proof

defpred S₁[ Nat] means (Partial_Union seqIntf) . $1 = (seqIntersection (b,(Partial_Union f))) . $1;
let n be Element of NAT ; :: thesis: (Partial_Union seqIntf) . n = (seqIntersection (b,(Partial_Union f))) . n
A17: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A18: (Partial_Union seqIntf) . k = (seqIntersection (b,(Partial_Union f))) . k ; :: thesis: S₁[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def 12;
(Partial_Union seqIntf) . (k + 1) = ((Partial_Union seqIntf) . k) \/ (seqIntf . (k + 1)) by PROB_3:def 2
.= (b /\ ((Partial_Union f) . k)) \/ (seqIntf . (k + 1)) by A18, DYNKIN:def 1
.= (b /\ ((Partial_Union f) . k)) \/ (b /\ (f . (k + 1))) by DYNKIN:def 1
.= b /\ (((Partial_Union f) . k) \/ (f . (k + 1))) by XBOOLE_1:23
.= b /\ ((Partial_Union f) . (k + 1)) by PROB_3:def 2
.= (seqIntersection (b,(Partial_Union f))) . (k + 1) by DYNKIN:def 1 ;
hence S₁[k + 1] ; :: thesis: verum

end;

(Partial_Union seqIntf) . 0 = seqIntf . 0 by PROB_3:def 2
.= b /\ (f . 0) by DYNKIN:def 1
.= b /\ ((Partial_Union f) . 0) by PROB_3:def 2
.= (seqIntersection (b,(Partial_Union f))) . 0 by DYNKIN:def 1 ;
then A19: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A19, A17);
hence (Partial_Union seqIntf) . n = (seqIntersection (b,(Partial_Union f))) . n ; :: thesis: verum

end;

then P * (seqIntersection (b,(Partial_Union f))) = P * (Partial_Union seqIntf) by FUNCT_2:63
.= Partial_Sums (P * seqIntf) by A16, PROB_3:44
.= r (#) (Partial_Sums (P * f)) by A5, SERIES_1:9
.= r (#) (P * (Partial_Union f)) by A15, PROB_3:44 ;
then r * (lim (P * (Partial_Union f))) = lim (P * seqIntPf) by PROB_3:41, SEQ_2:8
.= P . (b /\ (Union f)) by A14, A3, PROB_2:10 ;
hence P . (b /\ (Union f)) = (P . b) * (P . (Union f)) by PROB_3:41; :: thesis: verum