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 Th60;
take P ; :: thesis:
thus for A being Event of Sigma holds 0 <= P . A by A1; :: thesis:
[#] Sigma in Sigma ;
hence P . Omega = 1 by A1; :: thesis:
thus for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) :: thesis:

let A, B be Event of Sigma; :: thesis:
assume A20: A misses B ; :: thesis:
A21: ( 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;
A22: ( not the Element of Omega in A & the Element of Omega in B implies ( P . A = 0 & P . B = 1 ) ) by A1;
A23: ( 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;
A24: ( not the Element of Omega in A & not the Element of Omega in B implies ( P . A = 0 & P . B = 0 ) ) by A1;
A25: ( 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, A20, A21, A22, A23, A24, A25, XBOOLE_0:3; :: thesis:

end;

let ASeq be SetSequence of Sigma; :: thesis:
A3: for n being Element of NAT holds (P * ASeq) . n = P . (ASeq . n)

let n be Element of NAT ; :: thesis:
dom (P * ASeq) = NAT by FUNCT_2:def 1;
hence (P * ASeq) . n = P . (ASeq . n) by FUNCT_1:12; :: thesis:

end;

A4: ( ( for n being Element of NAT holds the Element of Omega in ASeq . n ) implies for n being Element of NAT holds (P * ASeq) . n = 1 )

assume A5: for n being Element of NAT holds the Element of Omega in ASeq . n ; :: thesis:
for n being Element of NAT holds (P * ASeq) . n = 1

let n be Element of NAT ; :: thesis:
A6: ( 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 A5;
then P . (ASeq . n) = 1 by A1, A6;
hence (P * ASeq) . n = 1 by A3; :: thesis:

end;

hence for n being Element of NAT holds (P * ASeq) . n = 1 ; :: thesis:

end;

assume A7: ASeq is non-ascending ; :: thesis:
A8: ( not for n being Element of NAT holds the Element of Omega in ASeq . n implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
(P * ASeq) . n = 0 )

assume not for n being Element of NAT holds the Element of Omega in ASeq . n ; :: thesis:
then consider m being Element of NAT such that
A9: not the Element of Omega in ASeq . m ;
take m ; :: thesis:
for n being Element of NAT st m <= n holds
(P * ASeq) . n = 0

let n be Element of NAT ; :: thesis:
assume m <= n ; :: thesis:
then ASeq . n c= ASeq . m by A7, Def6;
then A10: not the Element of Omega in ASeq . n by A9;
( rng ASeq c= Sigma & ASeq . n in rng ASeq ) by NAT_1:51, RELAT_1:def 19;
then P . (ASeq . n) = 0 by A1, A10;
hence (P * ASeq) . n = 0 by A3; :: thesis:

end;

hence for n being Element of NAT st m <= n holds
(P * ASeq) . n = 0 ; :: thesis:

end;

A11: ( ex m being Element of NAT st
for n being Element of NAT st m <= n holds
(P * ASeq) . n = 0 implies ( P * ASeq is convergent & lim (P * ASeq) = 0 ) ) by Th3;
rng ASeq c= Sigma by RELAT_1:def 19;
then A13: Intersection ASeq in Sigma by Def8;
reconsider r = 1 as Real ;
A15: ( ( for n being Element of NAT holds (P * ASeq) . n = 1 ) implies ( P * ASeq is convergent & lim (P * ASeq) = 1 ) )

assume A16: for n being Element of NAT holds (P * ASeq) . n = 1 ; :: thesis:
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
(P * ASeq) . n = r

take 0 ; :: thesis:
thus for n being Element of NAT st 0 <= n holds
(P * ASeq) . n = r by A16; :: thesis:

end;

hence ( P * ASeq is convergent & lim (P * ASeq) = 1 ) by Th3; :: thesis:

end;

end;

end;