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,REAL
for k being positive Real
for u being VECTOR of (RLSp_LpFunct M,k) st f = u holds
( u + ((- 1) * u) = (X --> 0 ) | (dom f) & ex v, g being PartFunc of X,REAL st
( v in Lp_Functions M,k & g in Lp_Functions M,k & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for k being positive Real
for u being VECTOR of (RLSp_LpFunct M,k) st f = u holds
( u + ((- 1) * u) = (X --> 0 ) | (dom f) & ex v, g being PartFunc of X,REAL st
( v in Lp_Functions M,k & g in Lp_Functions M,k & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL
for k being positive Real
for u being VECTOR of (RLSp_LpFunct M,k) st f = u holds
( u + ((- 1) * u) = (X --> 0 ) | (dom f) & ex v, g being PartFunc of X,REAL st
( v in Lp_Functions M,k & g in Lp_Functions M,k & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) )
let f be PartFunc of X,REAL ; :: thesis: for k being positive Real
for u being VECTOR of (RLSp_LpFunct M,k) st f = u holds
( u + ((- 1) * u) = (X --> 0 ) | (dom f) & ex v, g being PartFunc of X,REAL st
( v in Lp_Functions M,k & g in Lp_Functions M,k & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) )
let k be positive Real; :: thesis: for u being VECTOR of (RLSp_LpFunct M,k) st f = u holds
( u + ((- 1) * u) = (X --> 0 ) | (dom f) & ex v, g being PartFunc of X,REAL st
( v in Lp_Functions M,k & g in Lp_Functions M,k & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) )
let u be VECTOR of (RLSp_LpFunct M,k); :: thesis: ( f = u implies ( u + ((- 1) * u) = (X --> 0 ) | (dom f) & ex v, g being PartFunc of X,REAL st
( v in Lp_Functions M,k & g in Lp_Functions M,k & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) ) )
reconsider u2 = u as VECTOR of (RLSp_PFunct X) by TARSKI:def 3;
reconsider h = u2 + ((- 1) * u2) as Element of PFuncs X,REAL ;
assume A1: f = u ; :: thesis: ( u + ((- 1) * u) = (X --> 0 ) | (dom f) & ex v, g being PartFunc of X,REAL st
( v in Lp_Functions M,k & g in Lp_Functions M,k & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) )
(- 1) * u = (- 1) * u2 by LPSPACE1:5;
then A2: u + ((- 1) * u) = u2 + ((- 1) * u2) by LPSPACE1:4;
hence u + ((- 1) * u) = (X --> 0 ) | (dom f) by A1, LPSPACE1:16; :: thesis: ex v, g being PartFunc of X,REAL st
( v in Lp_Functions M,k & g in Lp_Functions M,k & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M )
u + ((- 1) * u) in Lp_Functions M,k ;
then consider v being PartFunc of X,REAL such that
A4: ( v = u + ((- 1) * u) & ex ND being Element of S st
( M . (ND ` ) = 0 & dom v = ND & v is_measurable_on ND & (abs v) to_power k is_integrable_on M ) ) ;
u in Lp_Functions M,k ;
then ex uu1 being PartFunc of X,REAL st
( uu1 = u & ex ND being Element of S st
( M . (ND ` ) = 0 & dom uu1 = ND & uu1 is_measurable_on ND & (abs uu1) to_power k is_integrable_on M ) ) ;
then consider ND being Element of S such that
A6: ( M . (ND ` ) = 0 & dom f = ND & f is_measurable_on ND & (abs f) to_power k is_integrable_on M ) by A1;
set g = X --> 0 ;
A7: ( ND ` is Element of S & (ND ` ) ` = ND ) by MEASURE1:66;
A8: X --> 0 in Lp_Functions M,k by LmDef1Lp;
v | ND = ((X --> 0 ) | ND) | ND by A2, A4, A6, A1, LPSPACE1:16;
then v | ND = (X --> 0 ) | ND by FUNCT_1:82;
then v a.e.= X --> 0 ,M by A6, A7, LPSPACE1:def 10;
hence ex v, g being PartFunc of X,REAL st
( v in Lp_Functions M,k & g in Lp_Functions M,k & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) by A4, A8; :: thesis: verum