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 :: thesis: for x being Element of X st x in dom (abs (X --> 0)) holds
(abs (X --> 0)) . x = 0
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:7;
then A2: |.((X --> 0) . x).| = 0 by ABSVALUE:2;
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:13;
then dom (abs (X --> 0)) = X by VALUED_1:def 11;
hence Integral (M,(abs (X --> 0))) = 0 by A1, Lm2; :: thesis: verum