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 set 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 Lm002b, MESFUNC6:52
.= Integral M,(X --> 0 ) by Lm001
.= Integral M,(abs (X --> 0 )) by A1, Lm002b, MESFUNC6:52 ;
hence Integral M,((abs (X --> 0 )) to_power k) = 0 by LPSPACE1:55; :: thesis: verum