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 number ;
for n being Element of NAT holds (seqIntersection b,f) . n is Event of Sigma

proof

let n be Element of NAT ; :: thesis: (seqIntersection b,f) . n is Event of Sigma
b /\ (f . n) is Event of Sigma ;
hence (seqIntersection b,f) . n is Event of Sigma by DYNKIN:def 2; :: thesis: verum

end;

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

proof

let n be Element of NAT ; :: thesis: (seqIntersection b,(@Partial_Union f)) . n is Event of Sigma
b /\ ((@Partial_Union f) . n) is Event of Sigma ;
hence (seqIntersection b,(@Partial_Union f)) . n is Event of Sigma by DYNKIN:def 2; :: thesis: verum

end;

then reconsider seqIntPf = seqIntersection b,(@Partial_Union f) as SetSequence of Sigma by PROB_1:57;
A1: b /\ (Union f) = b /\ (Union (@Partial_Union f)) by PROB_3:17
.= Union seqIntPf by DYNKIN:13 ;
assume A2: 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

let n be Element of NAT ; :: thesis: (P * seqIntf) . n = (r (#) (P * f)) . n
thus (P * seqIntf) . n = P . (seqIntf . n) by FUNCT_2:21
.= P . ((f . n) /\ b) by DYNKIN:def 2
.= (P . (f . n)) * (P . b) by A2
.= ((P * f) . n) * r by FUNCT_2:21
.= (r (#) (P * f)) . n by SEQ_1:13 ; :: thesis: verum

end;

then A3: P * seqIntf = r (#) (P * f) by FUNCT_2:def 8;
A4: 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 A5: n <= m ; :: thesis: ( not x in (@Partial_Union f) . n or x in (@Partial_Union f) . m )
assume A6: x in (@Partial_Union f) . n ; :: thesis: x in (@Partial_Union f) . m
Pf is non-descending by PROB_3:13;
then Pf . n c= Pf . m by A5, PROB_1:def 7;
hence x in (@Partial_Union f) . m by A6; :: thesis: verum

end;

for n, m being Element of NAT st n <= m holds
(seqIntersection b,(@Partial_Union f)) . n c= (seqIntersection b,(@Partial_Union f)) . m

proof

let n, m be Element of NAT ; :: thesis: ( n <= m implies (seqIntersection b,(@Partial_Union f)) . n c= (seqIntersection b,(@Partial_Union f)) . m )
assume A7: n <= m ; :: thesis: (seqIntersection b,(@Partial_Union f)) . n c= (seqIntersection b,(@Partial_Union f)) . m
let x be set ; :: 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 A8: x in b /\ ((@Partial_Union f) . n) by DYNKIN:def 2;
then x in (@Partial_Union f) . n by XBOOLE_0:def 4;
then A9: x in (@Partial_Union f) . m by A4, A7;
x in b by A8, XBOOLE_0:def 4;
then x in b /\ ((@Partial_Union f) . m) by A9, XBOOLE_0:def 4;
hence x in (seqIntersection b,(@Partial_Union f)) . m by DYNKIN:def 2; :: thesis: verum

end;

then A10: seqIntersection b,(@Partial_Union f) is non-descending by PROB_1:def 7;
assume A11: f is disjoint_valued ; :: thesis: P . (b /\ (Union f)) = (P . b) * (P . (Union f))
then A12: seqIntersection b,f is disjoint_valued by DYNKIN:12;
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
A13: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A14: (@Partial_Union seqIntf) . k = (seqIntersection b,(@Partial_Union f)) . k ; :: thesis: S₁[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def 13;
(@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 A14, DYNKIN:def 2
.= (b /\ ((@Partial_Union f) . k)) \/ (b /\ (f . (k + 1))) by DYNKIN:def 2
.= 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 2 ;
hence S₁[k + 1] ; :: thesis: verum

end;

(@Partial_Union seqIntf) . 0 = seqIntf . 0 by PROB_3:def 2
.= b /\ (f . 0 ) by DYNKIN:def 2
.= b /\ ((@Partial_Union f) . 0 ) by PROB_3:def 2
.= (seqIntersection b,(@Partial_Union f)) . 0 by DYNKIN:def 2 ;
then A15: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A15, A13);
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:113
.= Partial_Sums (P * seqIntf) by A12, PROB_3:49
.= r (#) (Partial_Sums (P * f)) by A3, SERIES_1:12
.= r (#) (P * (@Partial_Union f)) by A11, PROB_3:49 ;
then r * (lim (P * (@Partial_Union f))) = lim (P * seqIntPf) by PROB_3:46, SEQ_2:22
.= P . (b /\ (Union f)) by A10, A1, PROB_2:20 ;
hence P . (b /\ (Union f)) = (P . b) * (P . (Union f)) by PROB_3:46; :: thesis: verum