set p = the Element of Omega;

consider P being Function of Sigma,REAL such that

A1: for D being Subset of Omega st D in Sigma holds

( ( the Element of Omega in D implies P . D = 1 ) & ( not the Element of Omega in D implies P . D = 0 ) ) by Th28;

take P ; :: thesis: ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds

P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds

( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ) )

thus for A being Event of Sigma holds 0 <= P . A by A1; :: thesis: ( P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds

P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds

( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ) )

[#] Sigma in Sigma ;

hence P . Omega = 1 by A1; :: thesis: ( ( for A, B being Event of Sigma st A misses B holds

P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds

( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ) )

thus for A, B being Event of Sigma st A misses B holds

P . (A \/ B) = (P . A) + (P . B) :: thesis: for ASeq being SetSequence of Sigma st ASeq is non-ascending holds

( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )

A8: for n being Nat holds (P * ASeq) . n = P . (ASeq . n)

A13: ( not for n being Nat holds the Element of Omega in ASeq . n implies ex m being Nat st

for n being Nat st m <= n holds

(P * ASeq) . n = 0 )

for n being Nat st m <= n holds

(P * ASeq) . n = 0 implies ( P * ASeq is convergent & lim (P * ASeq) = 0 ) ) by Th1;

rng ASeq c= Sigma by RELAT_1:def 19;

then A17: Intersection ASeq in Sigma by Def6;

reconsider r = 1 as Real ;

A18: ( ( for n being Nat holds (P * ASeq) . n = 1 ) implies ( P * ASeq is convergent & lim (P * ASeq) = 1 ) )

consider P being Function of Sigma,REAL such that

A1: for D being Subset of Omega st D in Sigma holds

( ( the Element of Omega in D implies P . D = 1 ) & ( not the Element of Omega in D implies P . D = 0 ) ) by Th28;

take P ; :: thesis: ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds

P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds

( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ) )

thus for A being Event of Sigma holds 0 <= P . A by A1; :: thesis: ( P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds

P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds

( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ) )

[#] Sigma in Sigma ;

hence P . Omega = 1 by A1; :: thesis: ( ( for A, B being Event of Sigma st A misses B holds

P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds

( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ) )

thus for A, B being Event of Sigma st A misses B holds

P . (A \/ B) = (P . A) + (P . B) :: thesis: for ASeq being SetSequence of Sigma st ASeq is non-ascending holds

( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )

proof

let ASeq be SetSequence of Sigma; :: thesis: ( ASeq is non-ascending implies ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) )
let A, B be Event of Sigma; :: thesis: ( A misses B implies P . (A \/ B) = (P . A) + (P . B) )

assume A2: A misses B ; :: thesis: P . (A \/ B) = (P . A) + (P . B)

A3: ( the Element of Omega in A & not the Element of Omega in B implies the Element of Omega in A \/ B ) by XBOOLE_0:def 3;

A4: ( not the Element of Omega in A & the Element of Omega in B implies ( P . A = 0 & P . B = 1 ) ) by A1;

A5: ( not the Element of Omega in A & the Element of Omega in B implies the Element of Omega in A \/ B ) by XBOOLE_0:def 3;

A6: ( not the Element of Omega in A & not the Element of Omega in B implies ( P . A = 0 & P . B = 0 ) ) by A1;

A7: ( not the Element of Omega in A & not the Element of Omega in B implies not the Element of Omega in A \/ B ) by XBOOLE_0:def 3;

( the Element of Omega in A & not the Element of Omega in B implies ( P . A = 1 & P . B = 0 ) ) by A1;

hence P . (A \/ B) = (P . A) + (P . B) by A1, A2, A3, A4, A5, A6, A7, XBOOLE_0:3; :: thesis: verum

end;assume A2: A misses B ; :: thesis: P . (A \/ B) = (P . A) + (P . B)

A3: ( the Element of Omega in A & not the Element of Omega in B implies the Element of Omega in A \/ B ) by XBOOLE_0:def 3;

A4: ( not the Element of Omega in A & the Element of Omega in B implies ( P . A = 0 & P . B = 1 ) ) by A1;

A5: ( not the Element of Omega in A & the Element of Omega in B implies the Element of Omega in A \/ B ) by XBOOLE_0:def 3;

A6: ( not the Element of Omega in A & not the Element of Omega in B implies ( P . A = 0 & P . B = 0 ) ) by A1;

A7: ( not the Element of Omega in A & not the Element of Omega in B implies not the Element of Omega in A \/ B ) by XBOOLE_0:def 3;

( the Element of Omega in A & not the Element of Omega in B implies ( P . A = 1 & P . B = 0 ) ) by A1;

hence P . (A \/ B) = (P . A) + (P . B) by A1, A2, A3, A4, A5, A6, A7, XBOOLE_0:3; :: thesis: verum

A8: for n being Nat holds (P * ASeq) . n = P . (ASeq . n)

proof

A9:
( ( for n being Nat holds the Element of Omega in ASeq . n ) implies for n being Nat holds (P * ASeq) . n = 1 )
let n be Nat; :: thesis: (P * ASeq) . n = P . (ASeq . n)

reconsider n = n as Element of NAT by ORDINAL1:def 12;

dom (P * ASeq) = NAT by FUNCT_2:def 1;

then (P * ASeq) . n = P . (ASeq . n) by FUNCT_1:12;

hence (P * ASeq) . n = P . (ASeq . n) ; :: thesis: verum

end;reconsider n = n as Element of NAT by ORDINAL1:def 12;

dom (P * ASeq) = NAT by FUNCT_2:def 1;

then (P * ASeq) . n = P . (ASeq . n) by FUNCT_1:12;

hence (P * ASeq) . n = P . (ASeq . n) ; :: thesis: verum

proof

assume A12:
ASeq is non-ascending
; :: thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
assume A10:
for n being Nat holds the Element of Omega in ASeq . n
; :: thesis: for n being Nat holds (P * ASeq) . n = 1

for n being Nat holds (P * ASeq) . n = 1

end;for n being Nat holds (P * ASeq) . n = 1

proof

hence
for n being Nat holds (P * ASeq) . n = 1
; :: thesis: verum
let n be Nat; :: thesis: (P * ASeq) . n = 1

A11: ( rng ASeq c= Sigma & ASeq . n in rng ASeq ) by NAT_1:51, RELAT_1:def 19;

the Element of Omega in ASeq . n by A10;

then P . (ASeq . n) = 1 by A1, A11;

hence (P * ASeq) . n = 1 by A8; :: thesis: verum

end;A11: ( rng ASeq c= Sigma & ASeq . n in rng ASeq ) by NAT_1:51, RELAT_1:def 19;

the Element of Omega in ASeq . n by A10;

then P . (ASeq . n) = 1 by A1, A11;

hence (P * ASeq) . n = 1 by A8; :: thesis: verum

A13: ( not for n being Nat holds the Element of Omega in ASeq . n implies ex m being Nat st

for n being Nat st m <= n holds

(P * ASeq) . n = 0 )

proof

A16:
( ex m being Nat st
assume
not for n being Nat holds the Element of Omega in ASeq . n
; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

(P * ASeq) . n = 0

then consider m being Nat such that

A14: not the Element of Omega in ASeq . m ;

take m ; :: thesis: for n being Nat st m <= n holds

(P * ASeq) . n = 0

for n being Nat st m <= n holds

(P * ASeq) . n = 0

(P * ASeq) . n = 0 ; :: thesis: verum

end;for n being Nat st m <= n holds

(P * ASeq) . n = 0

then consider m being Nat such that

A14: not the Element of Omega in ASeq . m ;

take m ; :: thesis: for n being Nat st m <= n holds

(P * ASeq) . n = 0

for n being Nat st m <= n holds

(P * ASeq) . n = 0

proof

hence
for n being Nat st m <= n holds
let n be Nat; :: thesis: ( m <= n implies (P * ASeq) . n = 0 )

assume m <= n ; :: thesis: (P * ASeq) . n = 0

then ASeq . n c= ASeq . m by A12;

then A15: not the Element of Omega in ASeq . n by A14;

( rng ASeq c= Sigma & ASeq . n in rng ASeq ) by NAT_1:51, RELAT_1:def 19;

then P . (ASeq . n) = 0 by A1, A15;

hence (P * ASeq) . n = 0 by A8; :: thesis: verum

end;assume m <= n ; :: thesis: (P * ASeq) . n = 0

then ASeq . n c= ASeq . m by A12;

then A15: not the Element of Omega in ASeq . n by A14;

( rng ASeq c= Sigma & ASeq . n in rng ASeq ) by NAT_1:51, RELAT_1:def 19;

then P . (ASeq . n) = 0 by A1, A15;

hence (P * ASeq) . n = 0 by A8; :: thesis: verum

(P * ASeq) . n = 0 ; :: thesis: verum

for n being Nat st m <= n holds

(P * ASeq) . n = 0 implies ( P * ASeq is convergent & lim (P * ASeq) = 0 ) ) by Th1;

rng ASeq c= Sigma by RELAT_1:def 19;

then A17: Intersection ASeq in Sigma by Def6;

reconsider r = 1 as Real ;

A18: ( ( for n being Nat holds (P * ASeq) . n = 1 ) implies ( P * ASeq is convergent & lim (P * ASeq) = 1 ) )

proof

assume A19:
for n being Nat holds (P * ASeq) . n = 1
; :: thesis: ( P * ASeq is convergent & lim (P * ASeq) = 1 )

ex m being Nat st

for n being Nat st m <= n holds

(P * ASeq) . n = r

end;ex m being Nat st

for n being Nat st m <= n holds

(P * ASeq) . n = r

proof

hence
( P * ASeq is convergent & lim (P * ASeq) = 1 )
by Th1; :: thesis: verum
take
0
; :: thesis: for n being Nat st 0 <= n holds

(P * ASeq) . n = r

thus for n being Nat st 0 <= n holds

(P * ASeq) . n = r by A19; :: thesis: verum

end;(P * ASeq) . n = r

thus for n being Nat st 0 <= n holds

(P * ASeq) . n = r by A19; :: thesis: verum

per cases
( ex n being Nat st not the Element of Omega in ASeq . n or for n being Nat holds the Element of Omega in ASeq . n )
;

end;

suppose A20:
not for n being Nat holds the Element of Omega in ASeq . n
; :: thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )

then
not the Element of Omega in Intersection ASeq
by Th13;

hence ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) by A1, A13, A16, A20, A17; :: thesis: verum

end;hence ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) by A1, A13, A16, A20, A17; :: thesis: verum

suppose A21:
for n being Nat holds the Element of Omega in ASeq . n
; :: thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )

then
the Element of Omega in Intersection ASeq
by Th13;

hence ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) by A1, A9, A18, A21, A17; :: thesis: verum

end;hence ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) by A1, A9, A18, A21, A17; :: thesis: verum