let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A being Element of S st f is_measurable_on A & A c= dom f holds
|.f.| is_measurable_on A
let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX
for A being Element of S st f is_measurable_on A & A c= dom f holds
|.f.| is_measurable_on A
let f be PartFunc of X,COMPLEX ; :: thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds
|.f.| is_measurable_on A
let A be Element of S; :: thesis: ( f is_measurable_on A & A c= dom f implies |.f.| is_measurable_on A )
assume A1: ( f is_measurable_on A & A c= dom f ) ; :: thesis: |.f.| is_measurable_on A
then A2: ( Re f is_measurable_on A & Im f is_measurable_on A ) by Def3;
A0: ( dom |.(Re f).| = dom (Re f) & dom |.(Im f).| = dom (Im f) & dom |.f.| = dom f ) by VALUED_1:def 11;
C0: ( dom (Re f) = dom f & dom (Im f) = dom f ) by Def1, Def2;
then B1: ( |.(Re f).| is_measurable_on A & |.(Im f).| is_measurable_on A ) by A1, A2, MESFUNC6:48;

B3: now

let x be set ; :: thesis: ( x in dom |.(Re f).| implies 0 <= |.(Re f).| . x )
assume P01: x in dom |.(Re f).| ; :: thesis: 0 <= |.(Re f).| . x
0 <= |.((Re f) . x).| by COMPLEX1:132;
hence 0 <= |.(Re f).| . x by P01, VALUED_1:def 11; :: thesis: verum

end;

then C21: |.(Re f).| to_power 2 is nonnegative by Lm648, MESFUNC6:52;

B4: now

let x be set ; :: thesis: ( x in dom |.(Im f).| implies 0 <= |.(Im f).| . x )
assume x in dom |.(Im f).| ; :: thesis: 0 <= |.(Im f).| . x
then |.(Im f).| . x = |.((Im f) . x).| by VALUED_1:def 11;
hence 0 <= |.(Im f).| . x by COMPLEX1:132; :: thesis: verum

end;

then C22: |.(Im f).| to_power 2 is nonnegative by Lm648, MESFUNC6:52;
set F = (|.(Re f).| to_power 2) + (|.(Im f).| to_power 2);
( |.(Re f).| to_power 2 is_measurable_on A & |.(Im f).| to_power 2 is_measurable_on A ) by B1, A0, C0, A1, B3, B4, MES714, MESFUNC6:52;
then C1: (|.(Re f).| to_power 2) + (|.(Im f).| to_power 2) is_measurable_on A by MESFUNC6:26;
C31: dom ((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) = (dom (|.(Re f).| to_power 2)) /\ (dom (|.(Im f).| to_power 2)) by VALUED_1:def 1;
C32: ( dom (|.(Re f).| to_power 2) = dom f & dom (|.(Im f).| to_power 2) = dom f ) by A0, C0, Def7;
then D2: dom |.f.| = dom (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) by A0, Def7, C31;

now

let x be set ; :: thesis: ( x in dom |.f.| implies |.f.| . x = (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x )
assume P01: x in dom |.f.| ; :: thesis: |.f.| . x = (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x
then (|.(Re f).| to_power 2) . x = (|.(Re f).| . x) to_power 2 by A0, C32, Def7;
then (|.(Re f).| to_power 2) . x = |.((Re f) . x).| to_power 2 by P01, A0, C0, VALUED_1:def 11;
then (|.(Re f).| to_power 2) . x = |.(Re (f . x)).| to_power 2 by P01, A0, C0, Def1;
then (|.(Re f).| to_power 2) . x = |.(Re (f . x)).| ^2 by POWER:53;
then Q01: (|.(Re f).| to_power 2) . x = (Re (f . x)) ^2 by COMPLEX1:161;
(|.(Im f).| to_power 2) . x = (|.(Im f).| . x) to_power 2 by P01, A0, C32, Def7;
then (|.(Im f).| to_power 2) . x = |.((Im f) . x).| to_power 2 by P01, A0, C0, VALUED_1:def 11;
then (|.(Im f).| to_power 2) . x = |.(Im (f . x)).| to_power 2 by P01, A0, C0, Def2;
then (|.(Im f).| to_power 2) . x = |.(Im (f . x)).| ^2 by POWER:53;
then Q02: (|.(Im f).| to_power 2) . x = (Im (f . x)) ^2 by COMPLEX1:161;
(((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) . x) to_power (1 / 2) = sqrt (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) . x) by C21, C22, Lm648a, MESFUNC6:56
.= sqrt (((Re (f . x)) ^2 ) + ((Im (f . x)) ^2 )) by Q01, Q02, P01, A0, C31, C32, VALUED_1:def 1 ;
then (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x = |.(f . x).| by P01, D2, Def7;
hence |.f.| . x = (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x by P01, VALUED_1:def 11; :: thesis: verum

end;

then |.f.| = ((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2) by D2, FUNCT_1:9;
hence |.f.| is_measurable_on A by C1, C31, C32, A1, MES714, C21, C22, MESFUNC6:56; :: thesis: verum