for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for u being VECTOR of (CLSp_L1Funct M) st f = u holds
( u + ((- 1r) * u) = (X --> 0c) | (dom f) & ex v, g being PartFunc of X,COMPLEX st
( v in L1_CFunctions M & g in L1_CFunctions M & v = u + ((- 1r) * u) & g = X --> 0c & v a.e.cpfunc= g,M ) )