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) )
proof
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;
let ASeq be SetSequence of Sigma; :: thesis: ( ASeq is non-ascending implies ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) )
A8: for n being Nat holds (P * ASeq) . n = P . (ASeq . n)
proof
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;
A9: ( ( for n being Nat holds the Element of Omega in ASeq . n ) implies for n being Nat holds (P * ASeq) . n = 1 )
proof
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
proof
let n be Nat; :: thesis: (P * ASeq) . n = 1
A11: ( rng ASeq c= Sigma & ASeq . n in rng ASeq ) by ;
the Element of Omega in ASeq . n by A10;
then P . (ASeq . n) = 1 by ;
hence (P * ASeq) . n = 1 by A8; :: thesis: verum
end;
hence for n being Nat holds (P * ASeq) . n = 1 ; :: thesis: verum
end;
assume A12: ASeq is non-ascending ; :: thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
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
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
proof
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 ;
then P . (ASeq . n) = 0 by ;
hence (P * ASeq) . n = 0 by A8; :: thesis: verum
end;
hence for n being Nat st m <= n holds
(P * ASeq) . n = 0 ; :: thesis: verum
end;
A16: ( ex m being Nat st
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
proof
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;
hence ( P * ASeq is convergent & lim (P * ASeq) = 1 ) by Th1; :: thesis: verum
end;
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 ) ;
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;
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;
end;