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 A -measurable & A c= dom f holds
|.f.| is A -measurable
let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX
for A being Element of S st f is A -measurable & A c= dom f holds
|.f.| is A -measurable
let f be PartFunc of X,COMPLEX; :: thesis: for A being Element of S st f is A -measurable & A c= dom f holds
|.f.| is A -measurable
let A be Element of S; :: thesis: ( f is A -measurable & A c= dom f implies |.f.| is A -measurable )
assume that
A1: f is A -measurable and
A2: A c= dom f ; :: thesis: |.f.| is A -measurable
A3: dom (Im f) = dom f by COMSEQ_3:def 4;

A4: now :: thesis: for x being object st x in dom |.(Im f).| holds
0 <= |.(Im f).| . x

let x be object ; :: 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:46; :: thesis: verum

end;

then A5: |.(Im f).| to_power 2 is nonnegative by Th26, MESFUNC6:52;
A6: dom |.(Im f).| = dom (Im f) by VALUED_1:def 11;
then A7: dom (|.(Im f).| to_power 2) = dom f by A3, Def4;
Im f is A -measurable by A1;
then |.(Im f).| is A -measurable by A2, A3, MESFUNC6:48;
then A8: |.(Im f).| to_power 2 is A -measurable by A2, A6, A3, A4, Th29, MESFUNC6:52;
A9: dom (Re f) = dom f by COMSEQ_3:def 3;

A10: now :: thesis: for x being object st x in dom |.(Re f).| holds
0 <= |.(Re f).| . x

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

end;

then A12: |.(Re f).| to_power 2 is nonnegative by Th26, MESFUNC6:52;
set F = (|.(Re f).| to_power 2) + (|.(Im f).| to_power 2);
A13: dom |.f.| = dom f by VALUED_1:def 11;
A14: dom |.(Re f).| = dom (Re f) by VALUED_1:def 11;
then A15: dom (|.(Re f).| to_power 2) = dom f by A9, Def4;
A16: 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;
then A17: dom |.f.| = dom (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) by A13, A15, A7, Def4;

now :: thesis: for x being object st x in dom |.f.| holds
|.f.| . x = (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x

let x be object ; :: thesis: ( x in dom |.f.| implies |.f.| . x = (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x )
assume A18: 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 A13, A15, Def4;
then (|.(Re f).| to_power 2) . x = |.((Re f) . x).| to_power 2 by A14, A13, A9, A18, VALUED_1:def 11;
then (|.(Re f).| to_power 2) . x = |.(Re (f . x)).| to_power 2 by A13, A9, A18, COMSEQ_3:def 3;
then (|.(Re f).| to_power 2) . x = |.(Re (f . x)).| ^2 by POWER:46;
then A19: (|.(Re f).| to_power 2) . x = (Re (f . x)) ^2 by COMPLEX1:75;
(|.(Im f).| to_power 2) . x = (|.(Im f).| . x) to_power 2 by A13, A7, A18, Def4;
then (|.(Im f).| to_power 2) . x = |.((Im f) . x).| to_power 2 by A6, A13, A3, A18, VALUED_1:def 11;
then (|.(Im f).| to_power 2) . x = |.(Im (f . x)).| to_power 2 by A13, A3, A18, COMSEQ_3:def 4;
then (|.(Im f).| to_power 2) . x = |.(Im (f . x)).| ^2 by POWER:46;
then A20: (|.(Im f).| to_power 2) . x = (Im (f . x)) ^2 by COMPLEX1:75;
(((|.(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 A12, A5, Th27, MESFUNC6:56
.= sqrt (((Re (f . x)) ^2) + ((Im (f . x)) ^2)) by A13, A16, A15, A7, A18, A19, A20, VALUED_1:def 1 ;
then (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x = |.(f . x).| by A17, A18, Def4;
hence |.f.| . x = (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x by A18, VALUED_1:def 11; :: thesis: verum

end;

then A21: |.f.| = ((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2) by A17, FUNCT_1:2;
Re f is A -measurable by A1;
then |.(Re f).| is A -measurable by A2, A9, MESFUNC6:48;
then |.(Re f).| to_power 2 is A -measurable by A2, A14, A9, A10, Th29, MESFUNC6:52;
then (|.(Re f).| to_power 2) + (|.(Im f).| to_power 2) is A -measurable by A8, MESFUNC6:26;
hence |.f.| is A -measurable by A2, A12, A5, A16, A15, A7, A21, Th29, MESFUNC6:56; :: thesis: verum