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