let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S holds X --> 0 in L1_CFunctions M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds X --> 0 in L1_CFunctions M
let M be sigma_Measure of S; :: thesis: X --> 0 in L1_CFunctions M
set g = X --> 0c;
reconsider ND = {} as Element of S by MEASURE1:7;
A1: dom (X --> 0c) = ND ` by FUNCT_2:def 1;
for x being Element of X st x in dom (X --> 0c) holds
(X --> 0c) . x = 0 by FUNCOP_1:7;
then ( M . ND = 0 & X --> 0c is_integrable_on M ) by A1, Lm2, VALUED_0:def 19;
hence X --> 0 in L1_CFunctions M by A1; :: thesis: verum