let X be non empty set ; :: thesis: for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S st f is A -measurable & g is A -measurable holds
f + g is A -measurable
let S be SigmaField of X; :: thesis: for f, g being PartFunc of X,REAL
for A being Element of S st f is A -measurable & g is A -measurable holds
f + g is A -measurable
let f, g be PartFunc of X,REAL; :: thesis: for A being Element of S st f is A -measurable & g is A -measurable holds
f + g is A -measurable
let A be Element of S; :: thesis: ( f is A -measurable & g is A -measurable implies f + g is A -measurable )
assume ( f is A -measurable & g is A -measurable ) ; :: thesis: f + g is A -measurable
then ( R_EAL f is A -measurable & R_EAL g is A -measurable ) ;
then (R_EAL f) + (R_EAL g) is A -measurable by MESFUNC2:7;
then R_EAL (f + g) is A -measurable by Th23;
hence f + g is A -measurable ; :: thesis: verum