reconsider ND = {} as Element of S by MEASURE1:7;
set g = X --> 0c;
set I = { f where f is PartFunc of X,COMPLEX : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) } ;
A1: { f where f is PartFunc of X,COMPLEX : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) } c= PFuncs (X,COMPLEX)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is PartFunc of X,COMPLEX : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) } or x in PFuncs (X,COMPLEX) )
assume x in { f where f is PartFunc of X,COMPLEX : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) } ; :: thesis: x in PFuncs (X,COMPLEX)
then ex f being PartFunc of X,COMPLEX st
( x = f & ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) ) ;
hence x in PFuncs (X,COMPLEX) by PARTFUN1:45; :: thesis: verum

end;

A2: dom (X --> 0c) = ND ` by FUNCOP_1:13;
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 A2, Lm2, VALUED_0:def 19;
then X --> 0c in { f where f is PartFunc of X,COMPLEX : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) } by A2;
hence { f where f is PartFunc of X,COMPLEX : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) } is non empty Subset of (CLSp_PFunct X) by A1; :: thesis: verum