let k be natural number ; :: thesis:
let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let f be PartFunc of X,ExtREAL ; :: thesis:
let E be Element of S; :: thesis:
reconsider k1 = k as Element of NAT by ORDINAL1:def 13;
assume that
A1: E c= dom f and
A2: f is_measurable_on E ; :: thesis:
A3: dom (|.f.| |^ k) = dom |.f.| by Def5;
then A4: dom (|.f.| |^ k) = dom f by MESFUNC1:def 10;

per cases ;

suppose A5: k = 0 ; :: thesis:

A6: for r being real number st 1 < r holds
E /\ (less_dom (|.f.| |^ k),(R_EAL r)) in S

proof

let r be real number ; :: thesis:
assume A7: 1 < r ; :: thesis:
E c= less_dom (|.f.| |^ k),(R_EAL r)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A8: x in E ; :: thesis:
then (|.f.| |^ k) . x = (|.f.| . x) |^ k by A1, A4, Def5;
then (|.f.| |^ k) . x < r by A5, A7, Th6, FINSEQ_2:72;
hence x in less_dom (|.f.| |^ k),(R_EAL r) by A1, A4, A8, MESFUNC1:def 12; :: thesis:

end;

then E /\ (less_dom (|.f.| |^ k),(R_EAL r)) = E by XBOOLE_1:28;
hence E /\ (less_dom (|.f.| |^ k),(R_EAL r)) in S ; :: thesis:

end;

A9: E c= dom (|.f.| |^ k) by A1, A3, MESFUNC1:def 10;
for r being real number holds E /\ (less_dom (|.f.| |^ k),(R_EAL r)) in S

proof

let r be real number ; :: thesis:

now

assume A10: r <= 1 ; :: thesis:
E c= great_eq_dom (|.f.| |^ k),(R_EAL r)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A11: x in E ; :: thesis:
then (|.f.| |^ k) . x = (|.f.| . x) |^ k by A1, A4, Def5;
then r <= (|.f.| |^ k) . x by A5, A10, Th6, FINSEQ_2:72;
hence x in great_eq_dom (|.f.| |^ k),(R_EAL r) by A1, A4, A11, MESFUNC1:def 15; :: thesis:

end;

then E /\ (great_eq_dom (|.f.| |^ k),(R_EAL r)) = E by XBOOLE_1:28;
then E /\ (less_dom (|.f.| |^ k),(R_EAL r)) = E \ E by A9, MESFUNC1:21;
hence E /\ (less_dom (|.f.| |^ k),(R_EAL r)) in S ; :: thesis:

end;

hence E /\ (less_dom (|.f.| |^ k),(R_EAL r)) in S by A6; :: thesis:

end;

hence |.f.| |^ k is_measurable_on E by MESFUNC1:def 17; :: thesis:

end;

suppose A12: k <> 0 ; :: thesis:

then A13: (1 / k) * k = 1 by XCMPLX_1:88;
A14: for r being real number st 0 < r holds
great_eq_dom (|.f.| |^ k),(R_EAL r) = great_eq_dom |.f.|,(R_EAL (r to_power (1 / k)))

proof

let r be real number ; :: thesis:
assume A15: 0 < r ; :: thesis:
A16: great_eq_dom (|.f.| |^ k),(R_EAL r) c= great_eq_dom |.f.|,(R_EAL (r to_power (1 / k)))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A17: x in great_eq_dom (|.f.| |^ k),(R_EAL r) ; :: thesis:
then A18: x in dom (|.f.| |^ k) by MESFUNC1:def 15;
then A19: |.f.| . x = |.(f . x).| by A3, MESFUNC1:def 10;
then A20: 0 <= |.f.| . x by EXTREAL2:51;

per cases . x = +infty or |.f.| . x <> +infty ) ;

suppose |.f.| . x = +infty ; :: thesis:

then R_EAL (r to_power (1 / k)) <= |.f.| . x by XXREAL_0:3;
hence x in great_eq_dom |.f.|,(R_EAL (r to_power (1 / k))) by A3, A18, MESFUNC1:def 15; :: thesis:

end;

suppose |.f.| . x <> +infty ; :: thesis:

then reconsider fx = |.f.| . x as Element of REAL by A20, XXREAL_0:14;
A21: r <= (|.f.| |^ k) . x by A17, MESFUNC1:def 15;
(|.f.| |^ k) . x = (|.f.| . x) |^ k by A18, Def5;
then A22: r <= fx to_power k1 by A21, Th11;
(fx to_power k) to_power (1 / k) = fx to_power ((k * 1) / k) by A12, A19, EXTREAL2:51, HOLDER_1:2;
then A23: (fx to_power k) to_power (1 / k) = fx by A13, POWER:30;
r is Real by XREAL_0:def 1;
then r to_power (1 / k) <= (fx to_power k) to_power (1 / k) by A12, A15, A22, HOLDER_1:3;
hence x in great_eq_dom |.f.|,(R_EAL (r to_power (1 / k))) by A3, A18, A23, MESFUNC1:def 15; :: thesis:

end;

end;

end;

great_eq_dom |.f.|,(R_EAL (r to_power (1 / k))) c= great_eq_dom (|.f.| |^ k),(R_EAL r)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A24: x in great_eq_dom |.f.|,(R_EAL (r to_power (1 / k))) ; :: thesis:
then A25: x in dom |.f.| by MESFUNC1:def 15;
then A26: (|.f.| |^ k) . x = (|.f.| . x) |^ k by A3, Def5;
|.f.| . x = |.(f . x).| by A25, MESFUNC1:def 10;
then A27: 0 <= |.f.| . x by EXTREAL2:51;

A28: now

assume |.f.| . x <> +infty ; :: thesis:
then reconsider fx = |.f.| . x as Element of REAL by A27, XXREAL_0:14;
reconsider R = r to_power (1 / k) as Real by XREAL_0:def 1;
A29: 0 < r to_power (1 / k) by A15, POWER:39;
A30: R to_power k1 = r to_power ((1 / k) * k) by A15, POWER:38;
A31: (|.f.| |^ k) . x = fx |^ k by A26, Th11;
R_EAL (r to_power (1 / k)) <= |.f.| . x by A24, MESFUNC1:def 15;
then r to_power 1 <= fx to_power k by A12, A13, A29, A30, HOLDER_1:3;
hence r <= (|.f.| |^ k) . x by A31, POWER:30; :: thesis:

end;

now

assume |.f.| . x = +infty ; :: thesis:
then (|.f.| . x) |^ k = +infty by A12, Th13, NAT_1:14;
hence r <= (|.f.| |^ k) . x by A26, XXREAL_0:3; :: thesis:

end;

hence x in great_eq_dom (|.f.| |^ k),(R_EAL r) by A3, A25, A28, MESFUNC1:def 15; :: thesis:

end;

hence great_eq_dom (|.f.| |^ k),(R_EAL r) = great_eq_dom |.f.|,(R_EAL (r to_power (1 / k))) by A16, XBOOLE_0:def 10; :: thesis:

end;

A32: |.f.| is_measurable_on E by A1, A2, MESFUNC2:29;
for r being real number holds E /\ (great_eq_dom (|.f.| |^ k),(R_EAL r)) in S

proof

let r be real number ; :: thesis:

per cases ;

suppose A33: r <= 0 ; :: thesis:

E c= great_eq_dom (|.f.| |^ k),(R_EAL r)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A34: x in E ; :: thesis:
then A35: |.f.| . x = |.(f . x).| by A1, A3, A4, MESFUNC1:def 10;
(|.f.| |^ k) . x = (|.f.| . x) |^ k by A1, A4, A34, Def5;
then r <= (|.f.| |^ k) . x by A33, A35, Th12, EXTREAL2:51;
hence x in great_eq_dom (|.f.| |^ k),(R_EAL r) by A1, A4, A34, MESFUNC1:def 15; :: thesis:

end;

then E /\ (great_eq_dom (|.f.| |^ k),(R_EAL r)) = E by XBOOLE_1:28;
hence E /\ (great_eq_dom (|.f.| |^ k),(R_EAL r)) in S ; :: thesis:

end;

suppose 0 < r ; :: thesis:

then E /\ (great_eq_dom (|.f.| |^ k),(R_EAL r)) = E /\ (great_eq_dom |.f.|,(R_EAL (r to_power (1 / k)))) by A14;
hence E /\ (great_eq_dom (|.f.| |^ k),(R_EAL r)) in S by A1, A3, A4, A32, MESFUNC1:31; :: thesis:

end;

end;

end;

hence |.f.| |^ k is_measurable_on E by A1, A4, MESFUNC1:31; :: thesis:

end;

end;