let X be non empty set ; :: thesis: for S being SigmaField of X
for E being sequence of S
for f being PartFunc of X,ExtREAL st ( for n being Nat holds f is E . n -measurable ) holds
f is Union E -measurable
let S be SigmaField of X; :: thesis: for E being sequence of S
for f being PartFunc of X,ExtREAL st ( for n being Nat holds f is E . n -measurable ) holds
f is Union E -measurable
let E be sequence of S; :: thesis: for f being PartFunc of X,ExtREAL st ( for n being Nat holds f is E . n -measurable ) holds
f is Union E -measurable
let f be PartFunc of X,ExtREAL; :: thesis: ( ( for n being Nat holds f is E . n -measurable ) implies f is Union E -measurable )
assume A1: for n being Nat holds f is E . n -measurable ; :: thesis: f is Union E -measurable
for r being Real holds (Union E) /\ (less_dom (f,r)) in S

proof

let r be Real; :: thesis: (Union E) /\ (less_dom (f,r)) in S
deffunc H₁( Element of NAT ) -> Element of bool X = (E . $1) /\ (less_dom (f,r));
consider E1 being sequence of (bool X) such that
A2: for n being Element of NAT holds E1 . n = H₁(n) from FUNCT_2:sch 4();
for n being Element of NAT holds E1 . n = (less_dom (f,r)) /\ (E . n) by A2;
then union (rng E1) = (less_dom (f,r)) /\ (union (rng E)) by Th20;
then A3: Union E1 = (less_dom (f,r)) /\ (union (rng E)) by CARD_3:def 4;
reconsider E1 = E1 as SetSequence of X ;
for n being Element of NAT holds E1 . n in S

proof

let n be Element of NAT ; :: thesis: E1 . n in S
A4: f is E . n -measurable by A1;
E1 . n = (E . n) /\ (less_dom (f,r)) by A2;
hence E1 . n in S by A4, MESFUNC1:def 16; :: thesis: verum

end;

then rng E1 c= S by FUNCT_2:114;
then reconsider E1 = E1 as SetSequence of S by RELAT_1:def 19;
Union E1 = (Union E) /\ (less_dom (f,r)) by A3, CARD_3:def 4;
hence (Union E) /\ (less_dom (f,r)) in S by PROB_1:17; :: thesis: verum

end;

hence f is Union E -measurable by MESFUNC1:def 16; :: thesis: verum