let X be non empty set ; :: thesis: for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX
for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
f - g is_measurable_on A
let S be SigmaField of X; :: thesis: for f, g being PartFunc of X,COMPLEX
for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
f - g is_measurable_on A
let f, g be PartFunc of X,COMPLEX ; :: thesis: for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
f - g is_measurable_on A
let A be Element of S; :: thesis: ( f is_measurable_on A & g is_measurable_on A & A c= dom g implies f - g is_measurable_on A )
assume that
A1: ( f is_measurable_on A & g is_measurable_on A ) and
A2: A c= dom g ; :: thesis: f - g is_measurable_on A
A3: ( Re f is_measurable_on A & Im f is_measurable_on A & Re g is_measurable_on A & Im g is_measurable_on A ) by A1, Def3;
( A c= dom (Re g) & A c= dom (Im g) ) by A2, Def1, Def2;
then ( (Re f) - (Re g) is_measurable_on A & (Im f) - (Im g) is_measurable_on A ) by A3, MESFUNC6:29;
then ( Re (f - g) is_measurable_on A & Im (f - g) is_measurable_on A ) by COM48;
hence f - g is_measurable_on A by Def3; :: thesis: verum