set I = { f where f is PartFunc of X,REAL : 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,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) } c= PFuncs X,REAL

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) } or x in PFuncs X,REAL )
assume x in { f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) } ; :: thesis: x in PFuncs X,REAL
then ex f being PartFunc of X,REAL 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,REAL by PARTFUN1:119; :: thesis: verum

end;

set g = X --> 0 ;
reconsider ND = {} as Element of S by MEASURE1:66;
A3: M . ND = 0 by VALUED_0:def 19;
A4: dom (X --> 0 ) = ND ` by FUNCOP_1:19;
for x being Element of X st x in dom (X --> 0 ) holds
(X --> 0 ) . x = 0 by FUNCOP_1:13;
then X --> 0 is_integrable_on M by A4, Lm2;
then X --> 0 in { f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) } by A3, A4;
hence { f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) } is non empty Subset of (RLSp_PFunct X) by A1; :: thesis: verum