let X be non empty set ; :: thesis: 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 ) )
let S be SigmaField of X; :: thesis: 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 ) )
let M be sigma_Measure of S; :: thesis: 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 ) )
let f be PartFunc of X,COMPLEX; :: thesis: 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 ) )
let u be VECTOR of (CLSp_L1Funct M); :: thesis: ( f = u implies ( 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 ) ) )
reconsider u2 = u as VECTOR of (CLSp_PFunct X) by TARSKI:def 3;
reconsider h = u2 + ((- 1r) * u2) as Element of PFuncs (X,COMPLEX) ;
set g = X --> 0c;
u + ((- 1r) * u) in L1_CFunctions M ;
then consider v being PartFunc of X,COMPLEX such that
A1: v = u + ((- 1r) * u) and
ex ND being Element of S st
( M . ND = 0 & dom v = ND ` & v is_integrable_on M ) ;
assume A2: f = u ; :: thesis: ( 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 ) )
reconsider u9 = u2 as Element of PFuncs (X,COMPLEX) ;
A3: h = (addcpfunc X) . (u2,((multcomplexcpfunc X) . ((- 1r),u2)))
.= (CPFuncZero X) | (dom f) by A2, Th10 ;
u in L1_CFunctions M ;
then ex uu1 being PartFunc of X,COMPLEX st
( uu1 = u & ex ND being Element of S st
( M . ND = 0 & dom uu1 = ND ` & uu1 is_integrable_on M ) ) ;
then consider ND being Element of S such that
A4: M . ND = 0 and
A5: dom f = ND ` and
f is_integrable_on M by A2;
[R,u] in [:COMPLEX,(L1_CFunctions M):] ;
then A6: (- 1r) * u2 = (- 1r) * u by FUNCT_1:49;
hence u + ((- 1r) * u) = (X --> 0) | (dom f) by A3, ZFMISC_1:87, FUNCT_1:49; :: thesis: 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 )
v | (ND `) = ((X --> 0c) | (ND `)) | (ND `) by A3, A6, A1, A5, ZFMISC_1:87, FUNCT_1:49;
then A7: v | (ND `) = (X --> 0c) | (ND `) by FUNCT_1:51;
X --> 0c in L1_CFunctions M by Lm3;
hence 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 ) by A1, A4, A7, Def11; :: thesis: verum