let X be non empty set ; :: thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) holds
lim_inf f is E -measurable
let S be SigmaField of X; :: thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) holds
lim_inf f is E -measurable
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; :: thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) holds
lim_inf f is E -measurable
let E be Element of S; :: thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) implies lim_inf f is E -measurable )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is E -measurable ; :: thesis: lim_inf f is E -measurable

A3: now :: thesis: for r being Real holds E /\ (great_dom ((lim_inf f),r)) in S

let r be Real; :: thesis: E /\ (great_dom ((lim_inf f),r)) in S
deffunc H₁( Element of NAT ) -> Element of bool X = E /\ (great_dom (((inferior_realsequence f) . $1),r));
consider F being sequence of (bool X) such that
A4: for x being Element of NAT holds F . x = H₁(x) from FUNCT_2:sch 4();

now :: thesis: for i being Nat holds F . i in S

let i be Nat; :: thesis: F . i in S
i in NAT by ORDINAL1:def 12;
then A5: F . i = E /\ (great_dom (((inferior_realsequence f) . i),r)) by A4;
A6: dom ((inferior_realsequence f) . i) = E by A1, Def5;
(inferior_realsequence f) . i is E -measurable by A1, A2, Th20;
hence F . i in S by A5, A6, MESFUNC1:29; :: thesis: verum

end;

then A7: rng F c= S by NAT_1:52;
A8: for x being Nat holds F . x = E /\ (great_dom (((inferior_realsequence f) . x),r))

proof

let x be Nat; :: thesis: F . x = E /\ (great_dom (((inferior_realsequence f) . x),r))
reconsider x9 = x as Element of NAT by ORDINAL1:def 12;
F . x9 = E /\ (great_dom (((inferior_realsequence f) . x9),r)) by A4;
hence F . x = E /\ (great_dom (((inferior_realsequence f) . x),r)) ; :: thesis: verum

end;

reconsider F = F as SetSequence of S by A7, RELAT_1:def 19;
rng F c= S ;
then F is sequence of S by FUNCT_2:6;
then A9: rng F is N_Sub_set_fam of X by MEASURE1:23;
A10: rng F is N_Measure_fam of S by A9, MEASURE2:def 1;
union (rng F) = E /\ (great_dom ((lim_inf f),r)) by A1, A8, Th22;
hence E /\ (great_dom ((lim_inf f),r)) in S by A10, MEASURE2:2; :: thesis: verum

end;

dom (lim_inf f) = E by A1, Def7;
hence lim_inf f is E -measurable by A3, MESFUNC1:29; :: thesis: verum