let ASeq be SetSequence of Borel_Sets ; :: thesis: ( ASeq is non-ascending implies ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) )

A1: now

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

end;

assume A2: ASeq is non-ascending ; :: thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )

now

per cases ( for n being Element of NAT holds 0 in ASeq . n or ex n being Element of NAT st not 0 in ASeq . n ) ;

suppose A3: for n being Element of NAT holds 0 in ASeq . n ; :: thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )

reconsider r = 1 as Real ;
rng ASeq c= Borel_Sets by RELAT_1:def 19;
then A4: Intersection ASeq in Borel_Sets by PROB_1:def 6;
A5: 0 in Intersection ASeq by A3, PROB_1:13;

A6: now

let n be Element of NAT ; :: thesis: (P * ASeq) . n = 1
A7: ( rng ASeq c= Borel_Sets & ASeq . n in rng ASeq ) by NAT_1:51, RELAT_1:def 19;
0 in ASeq . n by A3;
then P . (ASeq . n) = 1 by A7, Lm1;
hence (P * ASeq) . n = 1 by A1; :: thesis: verum

end;

A8: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
(P * ASeq) . n = r

proof

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

end;

then lim (P * ASeq) = 1 by PROB_1:1;
hence ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) by A8, A5, A4, Lm1, PROB_1:1; :: thesis: verum

end;

suppose A9: not for n being Element of NAT holds 0 in ASeq . n ; :: thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )

rng ASeq c= Borel_Sets by RELAT_1:def 19;
then A10: Intersection ASeq in Borel_Sets by PROB_1:def 6;
A11: not 0 in Intersection ASeq by A9, PROB_1:13;
A12: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
(P * ASeq) . n = 0

proof

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

proof

let n be Element of NAT ; :: thesis: ( m <= n implies (P * ASeq) . n = 0 )
assume m <= n ; :: thesis: (P * ASeq) . n = 0
then ASeq . n c= ASeq . m by A2, PROB_1:def 4;
then A14: not 0 in ASeq . n by A13;
( rng ASeq c= Borel_Sets & ASeq . n in rng ASeq ) by NAT_1:51, RELAT_1:def 19;
then P . (ASeq . n) = 0 by A14, Lm1;
hence (P * ASeq) . n = 0 by A1; :: thesis: verum

end;

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

end;

then lim (P * ASeq) = 0 by PROB_1:1;
hence ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) by A12, A11, A10, Lm1, PROB_1:1; :: thesis: verum

end;

end;

end;

hence ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ; :: thesis: verum