:: deftheorem defines L1_Functions LPSPACE1:def 8 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds L1_Functions M = { 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 ) } ;