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;

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

A3: ( v = u + ((- 1) * u) & ex ND being Element of S st

( M . (ND `) = 0 & dom v = ND & v is ND -measurable & (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 ND -measurable & (abs uu1) to_power k is_integrable_on M ) ) ;

then consider ND being Element of S such that

A4: ( M . (ND `) = 0 & dom f = ND & f is ND -measurable & (abs f) to_power k is_integrable_on M ) by A1;

set g = X --> 0;

A5: ( ND ` is Element of S & (ND `) ` = ND ) by MEASURE1:34;

A6: X --> 0 in Lp_Functions (M,k) by Th23;

v | ND = ((X --> 0) | ND) | ND by A2, A3, A4, A1, LPSPACE1:16;

then v | ND = (X --> 0) | ND by FUNCT_1:51;

then v a.e.= X --> 0,M by A4, A5;

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 A3, A6; :: thesis: verum

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;

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

A3: ( v = u + ((- 1) * u) & ex ND being Element of S st

( M . (ND `) = 0 & dom v = ND & v is ND -measurable & (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 ND -measurable & (abs uu1) to_power k is_integrable_on M ) ) ;

then consider ND being Element of S such that

A4: ( M . (ND `) = 0 & dom f = ND & f is ND -measurable & (abs f) to_power k is_integrable_on M ) by A1;

set g = X --> 0;

A5: ( ND ` is Element of S & (ND `) ` = ND ) by MEASURE1:34;

A6: X --> 0 in Lp_Functions (M,k) by Th23;

v | ND = ((X --> 0) | ND) | ND by A2, A3, A4, A1, LPSPACE1:16;

then v | ND = (X --> 0) | ND by FUNCT_1:51;

then v a.e.= X --> 0,M by A4, A5;

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 A3, A6; :: thesis: verum