let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A, B being Element of S st f is A -measurable & f is B -measurable holds
f is A \/ B -measurable
let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL
for A, B being Element of S st f is A -measurable & f is B -measurable holds
f is A \/ B -measurable
let f be PartFunc of X,ExtREAL; :: thesis: for A, B being Element of S st f is A -measurable & f is B -measurable holds
f is A \/ B -measurable
let A, B be Element of S; :: thesis: ( f is A -measurable & f is B -measurable implies f is A \/ B -measurable )
assume A1: ( f is A -measurable & f is B -measurable ) ; :: thesis: f is A \/ B -measurable
for r being Real holds (A \/ B) /\ (less_dom (f,r)) in S

proof

let r be Real; :: thesis: (A \/ B) /\ (less_dom (f,r)) in S
( A /\ (less_dom (f,r)) in S & B /\ (less_dom (f,r)) in S ) by A1;
then (A /\ (less_dom (f,r))) \/ (B /\ (less_dom (f,r))) in S by FINSUB_1:def 1;
hence (A \/ B) /\ (less_dom (f,r)) in S by XBOOLE_1:23; :: thesis: verum

end;

hence f is A \/ B -measurable ; :: thesis: verum