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

for M being sigma_Measure of S

for k being positive Real holds Integral (M,((abs (X --> 0)) to_power k)) = 0

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for k being positive Real holds Integral (M,((abs (X --> 0)) to_power k)) = 0

let M be sigma_Measure of S; :: thesis: for k being positive Real holds Integral (M,((abs (X --> 0)) to_power k)) = 0

let k be positive Real; :: thesis: Integral (M,((abs (X --> 0)) to_power k)) = 0

A1: for x being object st x in dom (X --> 0) holds

0 <= (X --> 0) . x ;

then Integral (M,((abs (X --> 0)) to_power k)) = Integral (M,((X --> 0) to_power k)) by Th14, MESFUNC6:52

.= Integral (M,(X --> 0)) by Th12

.= Integral (M,(abs (X --> 0))) by A1, Th14, MESFUNC6:52 ;

hence Integral (M,((abs (X --> 0)) to_power k)) = 0 by LPSPACE1:54; :: thesis: verum

for M being sigma_Measure of S

for k being positive Real holds Integral (M,((abs (X --> 0)) to_power k)) = 0

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for k being positive Real holds Integral (M,((abs (X --> 0)) to_power k)) = 0

let M be sigma_Measure of S; :: thesis: for k being positive Real holds Integral (M,((abs (X --> 0)) to_power k)) = 0

let k be positive Real; :: thesis: Integral (M,((abs (X --> 0)) to_power k)) = 0

A1: for x being object st x in dom (X --> 0) holds

0 <= (X --> 0) . x ;

then Integral (M,((abs (X --> 0)) to_power k)) = Integral (M,((X --> 0) to_power k)) by Th14, MESFUNC6:52

.= Integral (M,(X --> 0)) by Th12

.= Integral (M,(abs (X --> 0))) by A1, Th14, MESFUNC6:52 ;

hence Integral (M,((abs (X --> 0)) to_power k)) = 0 by LPSPACE1:54; :: thesis: verum