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 ;
dom (X --> 0 ) = X by FUNCOP_1:19;
then A2: dom (abs (X --> 0 )) = X by VALUED_1:def 11;

now

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

end;

hence Integral M,(abs (X --> 0 )) = 0 by Lm2, A2; :: thesis: verum