let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for k being positive Real
for f, g being PartFunc of X,REAL st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) holds
( (abs f) to_power k is_integrable_on M & (abs g) to_power k is_integrable_on M & ((abs f) to_power k) + ((abs g) to_power k) is_integrable_on M )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for k being positive Real
for f, g being PartFunc of X,REAL st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) holds
( (abs f) to_power k is_integrable_on M & (abs g) to_power k is_integrable_on M & ((abs f) to_power k) + ((abs g) to_power k) is_integrable_on M )
let M be sigma_Measure of S; :: thesis: for k being positive Real
for f, g being PartFunc of X,REAL st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) holds
( (abs f) to_power k is_integrable_on M & (abs g) to_power k is_integrable_on M & ((abs f) to_power k) + ((abs g) to_power k) is_integrable_on M )
let k be positive Real; :: thesis: for f, g being PartFunc of X,REAL st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) holds
( (abs f) to_power k is_integrable_on M & (abs g) to_power k is_integrable_on M & ((abs f) to_power k) + ((abs g) to_power k) is_integrable_on M )
let f, g be PartFunc of X,REAL; :: thesis: ( f in Lp_Functions (M,k) & g in Lp_Functions (M,k) implies ( (abs f) to_power k is_integrable_on M & (abs g) to_power k is_integrable_on M & ((abs f) to_power k) + ((abs g) to_power k) is_integrable_on M ) )
assume A1: ( f in Lp_Functions (M,k) & g in Lp_Functions (M,k) ) ; :: thesis: ( (abs f) to_power k is_integrable_on M & (abs g) to_power k is_integrable_on M & ((abs f) to_power k) + ((abs g) to_power k) is_integrable_on M )
then A2: ex f1 being PartFunc of X,REAL st
( f = f1 & ex Ev being Element of S st
( M . (Ev `) = 0 & dom f1 = Ev & f1 is Ev -measurable & (abs f1) to_power k is_integrable_on M ) ) ;
ex g1 being PartFunc of X,REAL st
( g = g1 & ex Eu being Element of S st
( M . (Eu `) = 0 & dom g1 = Eu & g1 is Eu -measurable & (abs g1) to_power k is_integrable_on M ) ) by A1;
hence ( (abs f) to_power k is_integrable_on M & (abs g) to_power k is_integrable_on M & ((abs f) to_power k) + ((abs g) to_power k) is_integrable_on M ) by A2, MESFUNC6:100; :: thesis: verum