let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being SetSequence of st M . (Union F) < +infty holds
ex G being Function of NAT ,S st
( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for F being SetSequence of st M . (Union F) < +infty holds
ex G being Function of NAT ,S st
( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) )
let M be sigma_Measure of S; :: thesis: for F being SetSequence of st M . (Union F) < +infty holds
ex G being Function of NAT ,S st
( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) )
let F be SetSequence of ; :: thesis: ( M . (Union F) < +infty implies ex G being Function of NAT ,S st
( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) ) )
assume A1: M . (Union F) < +infty ; :: thesis: ex G being Function of NAT ,S st
( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) )
rng (superior_setsequence F) c= S by RELAT_1:def 19;
then reconsider G = superior_setsequence F as Function of NAT ,S by FUNCT_2:8;
A3: for n being Element of NAT holds G . (n + 1) c= G . n

proof

let n be Element of NAT ; :: thesis: G . (n + 1) c= G . n
n <= n + 1 by NAT_1:12;
hence G . (n + 1) c= G . n by PROB_1:def 6; :: thesis: verum

end;

G . 0 = union { (F . k) where k is Element of NAT : 0 <= k } by SETLIM_1:def 3;
then G . 0 = union (rng F) by SETLIM_1:5;
then A5: M . (meet (rng G)) = inf (rng (M * G)) by A1, A3, MEASURE3:14;
reconsider F1 = F, G1 = G as SetSequence of X ;
consider f being SetSequence of X such that
A6: ( lim_sup F1 = meet f & ( for n being Element of NAT holds f . n = Union (F1 ^\ n) ) ) by KURATO_2:def 4;

now

let n be Element of NAT ; :: thesis: f . n = G1 . n
f . n = Union (F1 ^\ n) by A6;
hence f . n = G1 . n by Th2; :: thesis: verum

end;

then f = G1 by FUNCT_2:113;
hence ex G being Function of NAT ,S st
( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) ) by A5, A6; :: thesis: verum