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 V71() holds
P . (b /\ ()) = (P . b) * (P . ())

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 V71() holds
P . (b /\ ()) = (P . b) * (P . ())

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 V71() holds
P . (b /\ ()) = (P . b) * (P . ())

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 V71() holds
P . (b /\ ()) = (P . b) * (P . ())

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 V71() holds
P . (b /\ ()) = (P . b) * (P . ())

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 V71() implies P . (b /\ ()) = (P . b) * (P . ()) )

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 ; :: thesis: verum
end;
then reconsider seqIntf = seqIntersection (b,f) as SetSequence of Sigma by PROB_1:25;
for n being Nat holds (seqIntersection (b,())) . n is Event of Sigma
proof
let n be Nat; :: thesis: (seqIntersection (b,())) . n is Event of Sigma
A2: n in NAT by ORDINAL1:def 12;
b /\ (() . n) is Event of Sigma ;
hence (seqIntersection (b,())) . n is Event of Sigma by ; :: thesis: verum
end;
then reconsider seqIntPf = seqIntersection (b,()) as SetSequence of Sigma by PROB_1:25;
A3: b /\ () = b /\ () 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 V71() or P . (b /\ ()) = (P . b) * (P . ()) )
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 () . n holds
x in () . m
proof
let x be set ; :: thesis: for n, m being Element of NAT st n <= m & x in () . n holds
x in () . m

reconsider Pf = Partial_Union f as SetSequence of Sigma ;
let n, m be Element of NAT ; :: thesis: ( n <= m & x in () . n implies x in () . m )
assume A7: n <= m ; :: thesis: ( not x in () . n or x in () . m )
assume A8: x in () . n ; :: thesis: x in () . m
Pf is non-descending by PROB_3:11;
then Pf . n c= Pf . m by A7;
hence x in () . m by A8; :: thesis: verum
end;
for n, m being Nat st n <= m holds
(seqIntersection (b,())) . n c= (seqIntersection (b,())) . m
proof
let n, m be Nat; :: thesis: ( n <= m implies (seqIntersection (b,())) . n c= (seqIntersection (b,())) . m )
assume A9: n <= m ; :: thesis: (seqIntersection (b,())) . n c= (seqIntersection (b,())) . 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,())) . n or x in (seqIntersection (b,())) . m )
assume x in (seqIntersection (b,())) . n ; :: thesis: x in (seqIntersection (b,())) . m
then A12: x in b /\ (() . n) by ;
then x in () . n by XBOOLE_0:def 4;
then A13: x in () . m by A6, A9, A11, A10;
x in b by ;
then x in b /\ (() . m) by ;
hence x in (seqIntersection (b,())) . m by ; :: thesis: verum
end;
then A14: seqIntersection (b,()) is non-descending ;
assume A15: f is V71() ; :: thesis: P . (b /\ ()) = (P . b) * (P . ())
then A16: seqIntersection (b,f) is V71() by DYNKIN:9;
for n being Element of NAT holds (Partial_Union seqIntf) . n = (seqIntersection (b,())) . n
proof
defpred S1[ Nat] means (Partial_Union seqIntf) . \$1 = (seqIntersection (b,())) . \$1;
let n be Element of NAT ; :: thesis: (Partial_Union seqIntf) . n = (seqIntersection (b,())) . n
A17: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A18: (Partial_Union seqIntf) . k = (seqIntersection (b,())) . k ; :: thesis: S1[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 /\ (() . k)) \/ (seqIntf . (k + 1)) by
.= (b /\ (() . k)) \/ (b /\ (f . (k + 1))) by DYNKIN:def 1
.= b /\ ((() . k) \/ (f . (k + 1))) by XBOOLE_1:23
.= b /\ (() . (k + 1)) by PROB_3:def 2
.= (seqIntersection (b,())) . (k + 1) by DYNKIN:def 1 ;
hence S1[k + 1] ; :: thesis: verum
end;
(Partial_Union seqIntf) . 0 = seqIntf . 0 by PROB_3:def 2
.= b /\ (f . 0) by DYNKIN:def 1
.= b /\ (() . 0) by PROB_3:def 2
.= (seqIntersection (b,())) . 0 by DYNKIN:def 1 ;
then A19: S1[ 0 ] ;
for k being Nat holds S1[k] from hence (Partial_Union seqIntf) . n = (seqIntersection (b,())) . n ; :: thesis: verum
end;
then P * (seqIntersection (b,())) = P * (Partial_Union seqIntf) by FUNCT_2:63
.= Partial_Sums (P * seqIntf) by
.= r (#) (Partial_Sums (P * f)) by
.= r (#) (P * ()) by ;
then r * (lim (P * ())) = lim (P * seqIntPf) by
.= P . (b /\ ()) by ;
hence P . (b /\ ()) = (P . b) * (P . ()) by PROB_3:41; :: thesis: verum