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 /\ (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 V71() 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 V71() 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 V71() 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 V71() 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 V71() 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

for n being Nat holds (seqIntersection (b,(Partial_Union f))) . n is Event of Sigma

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

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

(seqIntersection (b,(Partial_Union f))) . n c= (seqIntersection (b,(Partial_Union f))) . m

assume A15: f is V71() ; :: thesis: P . (b /\ (Union f)) = (P . b) * (P . (Union f))

then A16: seqIntersection (b,f) is V71() by DYNKIN:9;

for n being Element of NAT holds (Partial_Union seqIntf) . n = (seqIntersection (b,(Partial_Union f))) . n

.= 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

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 /\ (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 V71() 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 V71() 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 V71() 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 V71() 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 V71() 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

then reconsider seqIntf = seqIntersection (b,f) as SetSequence of Sigma by PROB_1:25;
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;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

for n being Nat holds (seqIntersection (b,(Partial_Union f))) . n is Event of Sigma

proof

then reconsider seqIntPf = seqIntersection (b,(Partial_Union f)) as SetSequence of Sigma by PROB_1:25;
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;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

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

then A5:
P * seqIntf = r (#) (P * f)
by FUNCT_2:def 7;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;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

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

for n, m being Nat st n <= m holds
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;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

(seqIntersection (b,(Partial_Union f))) . n c= (seqIntersection (b,(Partial_Union f))) . m

proof

then A14:
seqIntersection (b,(Partial_Union f)) is non-descending
;
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;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

assume A15: f is V71() ; :: thesis: P . (b /\ (Union f)) = (P . b) * (P . (Union f))

then A16: seqIntersection (b,f) is V71() by DYNKIN:9;

for n being Element of NAT holds (Partial_Union seqIntf) . n = (seqIntersection (b,(Partial_Union f))) . n

proof

then P * (seqIntersection (b,(Partial_Union f))) =
P * (Partial_Union seqIntf)
by FUNCT_2:63
defpred S_{1}[ 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_{1}[k] holds

S_{1}[k + 1]

.= 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_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A19, A17);

hence (Partial_Union seqIntf) . n = (seqIntersection (b,(Partial_Union f))) . n ; :: thesis: verum

end;let n be Element of NAT ; :: thesis: (Partial_Union seqIntf) . n = (seqIntersection (b,(Partial_Union f))) . n

A17: for k being Nat st S

S

proof

(Partial_Union seqIntf) . 0 =
seqIntf . 0
by PROB_3:def 2
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A18: (Partial_Union seqIntf) . k = (seqIntersection (b,(Partial_Union f))) . k ; :: thesis: S_{1}[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_{1}[k + 1]
; :: thesis: verum

end;assume A18: (Partial_Union seqIntf) . k = (seqIntersection (b,(Partial_Union f))) . k ; :: thesis: S

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

.= 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

for k being Nat holds S

hence (Partial_Union seqIntf) . n = (seqIntersection (b,(Partial_Union f))) . n ; :: thesis: verum

.= 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