let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S holds Integral M,(abs (X --> 0 )) = 0
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds Integral M,(abs (X --> 0 )) = 0
let M be sigma_Measure of S; :: thesis: Integral M,(abs (X --> 0 )) = 0
set f = X --> 0 ;

A1: now

let x be Element of X; :: thesis: ( x in dom (abs (X --> 0 )) implies (abs (X --> 0 )) . x = 0 )
(X --> 0 ) . x = 0 by FUNCOP_1:13;
then A2: abs ((X --> 0 ) . x) = 0 by ABSVALUE:7;
assume x in dom (abs (X --> 0 )) ; :: thesis: (abs (X --> 0 )) . x = 0
hence (abs (X --> 0 )) . x = 0 by A2, VALUED_1:def 11; :: thesis: verum

end;

dom (X --> 0 ) = X by FUNCOP_1:19;
then dom (abs (X --> 0 )) = X by VALUED_1:def 11;
hence Integral M,(abs (X --> 0 )) = 0 by A1, Lm2; :: thesis: verum