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;

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;

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;

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

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

then A5:
|.(Im f).| to_power 2 is nonnegative
by Th26, MESFUNC6:52;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;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

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

then A12:
|.(Re f).| to_power 2 is nonnegative
by Th26, MESFUNC6:52;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;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

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

then A21:
|.f.| = ((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)
by A17, FUNCT_1:2;|.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;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

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