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
for n being Nat holds (inferior_realsequence f) . n 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
for n being Nat holds (inferior_realsequence f) . n 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
for n being Nat holds (inferior_realsequence f) . n 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 for n being Nat holds (inferior_realsequence f) . n is E -measurable )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is E -measurable ; :: thesis: for n being Nat holds (inferior_realsequence f) . n is E -measurable
let n be Nat; :: thesis: (inferior_realsequence f) . n is E -measurable
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

A3: now :: thesis: for r being Real holds E /\ (great_eq_dom (((inferior_realsequence f) . n),r)) in S

let r be Real; :: thesis: E /\ (great_eq_dom (((inferior_realsequence f) . n),r)) in S
deffunc H₁( Element of NAT ) -> Element of bool X = E /\ (great_eq_dom ((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
A5: f . i is E -measurable by A2;
i in NAT by ORDINAL1:def 12;
then A6: F . i = E /\ (great_eq_dom ((f . i),r)) by A4;
dom (f . i) = E by A1, Def2;
hence F . i in S by A6, A5, MESFUNC1:27; :: thesis: verum

end;

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

proof

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

end;

reconsider F = F as SetSequence of S by A7, RELAT_1:def 19;
(inferior_setsequence F) . n9 in rng (inferior_setsequence F) by NAT_1:51;
then (inferior_setsequence F) . n9 in S ;
hence E /\ (great_eq_dom (((inferior_realsequence f) . n),r)) in S by A1, A8, Th18; :: thesis: verum

end;

dom ((inferior_realsequence f) . n9) = E by A1, Def5;
hence (inferior_realsequence f) . n is E -measurable by A3, MESFUNC1:27; :: thesis: verum