let k be Real; :: thesis: for X being non empty set

for S being SigmaField of X

for E being Element of S

for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is E -measurable holds

f to_power k is E -measurable

let X be non empty set ; :: thesis: for S being SigmaField of X

for E being Element of S

for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is E -measurable holds

f to_power k is E -measurable

let S be SigmaField of X; :: thesis: for E being Element of S

for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is E -measurable holds

f to_power k is E -measurable

let E be Element of S; :: thesis: for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is E -measurable holds

f to_power k is E -measurable

let f be PartFunc of X,REAL; :: thesis: ( f is nonnegative & 0 <= k & E c= dom f & f is E -measurable implies f to_power k is E -measurable )

reconsider k1 = k as Real ;

assume that

A1: f is nonnegative and

A2: 0 <= k and

A3: E c= dom f and

A4: f is E -measurable ; :: thesis: f to_power k is E -measurable

A5: dom (f to_power k) = dom f by Def4;

for S being SigmaField of X

for E being Element of S

for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is E -measurable holds

f to_power k is E -measurable

let X be non empty set ; :: thesis: for S being SigmaField of X

for E being Element of S

for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is E -measurable holds

f to_power k is E -measurable

let S be SigmaField of X; :: thesis: for E being Element of S

for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is E -measurable holds

f to_power k is E -measurable

let E be Element of S; :: thesis: for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is E -measurable holds

f to_power k is E -measurable

let f be PartFunc of X,REAL; :: thesis: ( f is nonnegative & 0 <= k & E c= dom f & f is E -measurable implies f to_power k is E -measurable )

reconsider k1 = k as Real ;

assume that

A1: f is nonnegative and

A2: 0 <= k and

A3: E c= dom f and

A4: f is E -measurable ; :: thesis: f to_power k is E -measurable

A5: dom (f to_power k) = dom f by Def4;

per cases
( k = 0 or k > 0 )
by A2;

end;

suppose A6:
k = 0
; :: thesis: f to_power k is E -measurable

A7:
E c= dom (f to_power k)
by A3, Def4;

end;now :: thesis: for r being Real holds E /\ (less_dom ((f to_power k),r)) in S

hence
f to_power k is E -measurable
by MESFUNC6:12; :: thesis: verumlet r be Real; :: thesis: E /\ (less_dom ((f to_power k),b_{1})) in S

reconsider r1 = r as Real ;

end;reconsider r1 = r as Real ;

per cases
( r <= 1 or 1 < r )
;

end;

suppose A8:
r <= 1
; :: thesis: E /\ (less_dom ((f to_power k),b_{1})) in S

then E /\ (great_eq_dom ((f to_power k),r)) = E by XBOOLE_1:28;

then E /\ (less_dom ((f to_power k),r1)) = E \ E by A7, Th28;

hence E /\ (less_dom ((f to_power k),r)) in S ; :: thesis: verum

end;

now :: thesis: for x being object st x in E holds

x in great_eq_dom ((f to_power k),r1)

then
E c= great_eq_dom ((f to_power k),r)
by TARSKI:def 3;x in great_eq_dom ((f to_power k),r1)

let x be object ; :: thesis: ( x in E implies x in great_eq_dom ((f to_power k),r1) )

assume A9: x in E ; :: thesis: x in great_eq_dom ((f to_power k),r1)

then (f to_power k) . x = (f . x) to_power k by A3, A5, Def4;

then r <= (f to_power k) . x by A6, A8, POWER:24;

hence x in great_eq_dom ((f to_power k),r1) by A3, A5, A9, MESFUNC6:6; :: thesis: verum

end;assume A9: x in E ; :: thesis: x in great_eq_dom ((f to_power k),r1)

then (f to_power k) . x = (f . x) to_power k by A3, A5, Def4;

then r <= (f to_power k) . x by A6, A8, POWER:24;

hence x in great_eq_dom ((f to_power k),r1) by A3, A5, A9, MESFUNC6:6; :: thesis: verum

then E /\ (great_eq_dom ((f to_power k),r)) = E by XBOOLE_1:28;

then E /\ (less_dom ((f to_power k),r1)) = E \ E by A7, Th28;

hence E /\ (less_dom ((f to_power k),r)) in S ; :: thesis: verum

suppose A10:
1 < r
; :: thesis: E /\ (less_dom ((f to_power k),b_{1})) in S

then E /\ (less_dom ((f to_power k),r)) = E by XBOOLE_1:28;

hence E /\ (less_dom ((f to_power k),r)) in S ; :: thesis: verum

end;

now :: thesis: for x being object st x in E holds

x in less_dom ((f to_power k),r)

then
E c= less_dom ((f to_power k),r)
by TARSKI:def 3;x in less_dom ((f to_power k),r)

let x be object ; :: thesis: ( x in E implies x in less_dom ((f to_power k),r) )

assume A11: x in E ; :: thesis: x in less_dom ((f to_power k),r)

then (f to_power k) . x = (f . x) to_power k by A3, A5, Def4;

then (f to_power k) . x < r by A6, A10, POWER:24;

hence x in less_dom ((f to_power k),r) by A3, A5, A11, MESFUNC6:3; :: thesis: verum

end;assume A11: x in E ; :: thesis: x in less_dom ((f to_power k),r)

then (f to_power k) . x = (f . x) to_power k by A3, A5, Def4;

then (f to_power k) . x < r by A6, A10, POWER:24;

hence x in less_dom ((f to_power k),r) by A3, A5, A11, MESFUNC6:3; :: thesis: verum

then E /\ (less_dom ((f to_power k),r)) = E by XBOOLE_1:28;

hence E /\ (less_dom ((f to_power k),r)) in S ; :: thesis: verum

suppose A12:
k > 0
; :: thesis: f to_power k is E -measurable

for r being Real holds E /\ (great_eq_dom ((f to_power k),r)) in S

end;proof

hence
f to_power k is E -measurable
by A3, A5, MESFUNC6:13; :: thesis: verum
let r be Real; :: thesis: E /\ (great_eq_dom ((f to_power k),r)) in S

reconsider r1 = r as Real ;

end;reconsider r1 = r as Real ;

per cases
( r1 <= 0 or 0 < r1 )
;

end;

suppose A13:
r1 <= 0
; :: thesis: E /\ (great_eq_dom ((f to_power k),r)) in S

then E /\ (great_eq_dom ((f to_power k),r)) = E by XBOOLE_1:28;

hence E /\ (great_eq_dom ((f to_power k),r)) in S ; :: thesis: verum

end;

now :: thesis: for x being object st x in E holds

x in great_eq_dom ((f to_power k),r1)

then
E c= great_eq_dom ((f to_power k),r)
by TARSKI:def 3;x in great_eq_dom ((f to_power k),r1)

let x be object ; :: thesis: ( x in E implies x in great_eq_dom ((f to_power k),r1) )

assume x in E ; :: thesis: x in great_eq_dom ((f to_power k),r1)

then x in dom f by A3;

then A14: x in dom (f to_power k) by Def4;

0 <= (f to_power k) . x by A1, A12, MESFUNC6:51;

hence x in great_eq_dom ((f to_power k),r1) by A13, A14, MESFUNC6:6; :: thesis: verum

end;assume x in E ; :: thesis: x in great_eq_dom ((f to_power k),r1)

then x in dom f by A3;

then A14: x in dom (f to_power k) by Def4;

0 <= (f to_power k) . x by A1, A12, MESFUNC6:51;

hence x in great_eq_dom ((f to_power k),r1) by A13, A14, MESFUNC6:6; :: thesis: verum

then E /\ (great_eq_dom ((f to_power k),r)) = E by XBOOLE_1:28;

hence E /\ (great_eq_dom ((f to_power k),r)) in S ; :: thesis: verum

suppose A15:
0 < r1
; :: thesis: E /\ (great_eq_dom ((f to_power k),r)) in S

hence E /\ (great_eq_dom ((f to_power k),r)) in S by A3, A4, MESFUNC6:13; :: thesis: verum

end;

A16: now :: thesis: for x being object st x in great_eq_dom (f,(r1 to_power (1 / k))) holds

x in great_eq_dom ((f to_power k),r1)

x in great_eq_dom ((f to_power k),r1)

set R = r to_power (jj / k);

let x be object ; :: thesis: ( x in great_eq_dom (f,(r1 to_power (1 / k))) implies x in great_eq_dom ((f to_power k),r1) )

reconsider xx = x as set by TARSKI:1;

A17: 0 < r to_power (jj / k) by A15, POWER:34;

assume A18: x in great_eq_dom (f,(r1 to_power (1 / k))) ; :: thesis: x in great_eq_dom ((f to_power k),r1)

then A19: x in dom (f to_power k) by A5, MESFUNC6:6;

(r to_power (jj / k)) to_power k = r to_power ((1 / k) * k) by A15, POWER:33;

then A20: (r to_power (jj / k)) to_power k = r to_power 1 by A12, XCMPLX_1:87;

ex y being Real st

( y = f . x & r1 to_power (1 / k) <= y ) by A18, MESFUNC6:6;

then r1 to_power jj <= (f . xx) to_power k1 by A12, A17, A20, HOLDER_1:3;

then r <= (f . xx) to_power k by POWER:25;

then r <= (f to_power k) . xx by A19, Def4;

hence x in great_eq_dom ((f to_power k),r1) by A19, MESFUNC6:6; :: thesis: verum

end;let x be object ; :: thesis: ( x in great_eq_dom (f,(r1 to_power (1 / k))) implies x in great_eq_dom ((f to_power k),r1) )

reconsider xx = x as set by TARSKI:1;

A17: 0 < r to_power (jj / k) by A15, POWER:34;

assume A18: x in great_eq_dom (f,(r1 to_power (1 / k))) ; :: thesis: x in great_eq_dom ((f to_power k),r1)

then A19: x in dom (f to_power k) by A5, MESFUNC6:6;

(r to_power (jj / k)) to_power k = r to_power ((1 / k) * k) by A15, POWER:33;

then A20: (r to_power (jj / k)) to_power k = r to_power 1 by A12, XCMPLX_1:87;

ex y being Real st

( y = f . x & r1 to_power (1 / k) <= y ) by A18, MESFUNC6:6;

then r1 to_power jj <= (f . xx) to_power k1 by A12, A17, A20, HOLDER_1:3;

then r <= (f . xx) to_power k by POWER:25;

then r <= (f to_power k) . xx by A19, Def4;

hence x in great_eq_dom ((f to_power k),r1) by A19, MESFUNC6:6; :: thesis: verum

now :: thesis: for x being object st x in great_eq_dom ((f to_power k),r1) holds

x in great_eq_dom (f,(r1 to_power (1 / k)))

then
E /\ (great_eq_dom ((f to_power k),r1)) = E /\ (great_eq_dom (f,(r1 to_power (1 / k))))
by A16, TARSKI:2;x in great_eq_dom (f,(r1 to_power (1 / k)))

let x be object ; :: thesis: ( x in great_eq_dom ((f to_power k),r1) implies x in great_eq_dom (f,(r1 to_power (1 / k))) )

reconsider xx = x as set by TARSKI:1;

assume A21: x in great_eq_dom ((f to_power k),r1) ; :: thesis: x in great_eq_dom (f,(r1 to_power (1 / k)))

then A22: x in dom (f to_power k) by MESFUNC6:6;

0 <= f . xx by A1, MESFUNC6:51;

then ((f . xx) to_power k1) to_power (1 / k1) = (f . xx) to_power ((k1 * 1) / k1) by A12, HOLDER_1:2;

then ((f . xx) to_power k1) to_power (1 / k1) = (f . xx) to_power 1 by A12, XCMPLX_1:87;

then A23: ((f . xx) to_power k) to_power (1 / k) = f . x by POWER:25;

ex y2 being Real st

( y2 = (f to_power k) . x & r1 <= y2 ) by A21, MESFUNC6:6;

then r <= (f . xx) to_power k by A22, Def4;

then r to_power (1 / k1) <= ((f . xx) to_power k1) to_power (1 / k1) by A12, A15, HOLDER_1:3;

hence x in great_eq_dom (f,(r1 to_power (1 / k))) by A5, A22, A23, MESFUNC6:6; :: thesis: verum

end;reconsider xx = x as set by TARSKI:1;

assume A21: x in great_eq_dom ((f to_power k),r1) ; :: thesis: x in great_eq_dom (f,(r1 to_power (1 / k)))

then A22: x in dom (f to_power k) by MESFUNC6:6;

0 <= f . xx by A1, MESFUNC6:51;

then ((f . xx) to_power k1) to_power (1 / k1) = (f . xx) to_power ((k1 * 1) / k1) by A12, HOLDER_1:2;

then ((f . xx) to_power k1) to_power (1 / k1) = (f . xx) to_power 1 by A12, XCMPLX_1:87;

then A23: ((f . xx) to_power k) to_power (1 / k) = f . x by POWER:25;

ex y2 being Real st

( y2 = (f to_power k) . x & r1 <= y2 ) by A21, MESFUNC6:6;

then r <= (f . xx) to_power k by A22, Def4;

then r to_power (1 / k1) <= ((f . xx) to_power k1) to_power (1 / k1) by A12, A15, HOLDER_1:3;

hence x in great_eq_dom (f,(r1 to_power (1 / k))) by A5, A22, A23, MESFUNC6:6; :: thesis: verum

hence E /\ (great_eq_dom ((f to_power k),r)) in S by A3, A4, MESFUNC6:13; :: thesis: verum