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:
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 A2: A misses B ; :: thesis:
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:

end;

let ASeq be SetSequence of Sigma; :: thesis:
A8: for n being Nat holds (P * ASeq) . n = P . (ASeq . n)

let n be Nat; :: thesis:
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:

end;

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

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

let n be Nat; :: thesis:
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:

end;

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

end;

assume A12: ASeq is non-ascending ; :: thesis:
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 )

assume not for n being Nat holds the Element of Omega in ASeq . n ; :: thesis:
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

let n be Nat; :: thesis:
assume m <= n ; :: thesis:
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:

end;

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

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

assume A19: for n being Nat holds (P * ASeq) . n = 1 ; :: thesis:
ex m being Nat st
for n being Nat st m <= n holds
(P * ASeq) . n = r

take 0 ; :: thesis:
thus for n being Nat st 0 <= n holds
(P * ASeq) . n = r by A19; :: thesis:

end;

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

end;

end;

end;