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