let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for k being positive Real st f in Lp_Functions M,k & g in Lp_Functions M,k holds
f + g in Lp_Functions M,k
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for k being positive Real st f in Lp_Functions M,k & g in Lp_Functions M,k holds
f + g in Lp_Functions M,k
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL
for k being positive Real st f in Lp_Functions M,k & g in Lp_Functions M,k holds
f + g in Lp_Functions M,k
let f, g be PartFunc of X,REAL ; :: thesis: for k being positive Real st f in Lp_Functions M,k & g in Lp_Functions M,k holds
f + g in Lp_Functions M,k
let k be positive Real; :: thesis: ( f in Lp_Functions M,k & g in Lp_Functions M,k implies f + g in Lp_Functions M,k )
set W = Lp_Functions M,k;
assume A1: ( f in Lp_Functions M,k & g in Lp_Functions M,k ) ; :: thesis: f + g in Lp_Functions M,k
then consider f1 being PartFunc of X,REAL such that
A1a: ( f1 = f & ex Ef1 being Element of S st
( M . (Ef1 ` ) = 0 & dom f1 = Ef1 & f1 is_measurable_on Ef1 & (abs f1) to_power k is_integrable_on M ) ) ;
consider Ef being Element of S such that
A2: ( M . (Ef ` ) = 0 & dom f1 = Ef & f1 is_measurable_on Ef & (abs f1) to_power k is_integrable_on M ) by A1a;
consider g1 being PartFunc of X,REAL such that
A2a: ( g1 = g & ex Eg1 being Element of S st
( M . (Eg1 ` ) = 0 & dom g1 = Eg1 & g1 is_measurable_on Eg1 & (abs g1) to_power k is_integrable_on M ) ) by A1;
consider Eg being Element of S such that
A3: ( M . (Eg ` ) = 0 & dom g1 = Eg & g1 is_measurable_on Eg & (abs g1) to_power k is_integrable_on M ) by A2a;
A4: dom (f1 + g1) = Ef /\ Eg by A2, A3, VALUED_1:def 1;
set Efg = Ef /\ Eg;
set s = (abs (f1 + g1)) to_power k;
set t = (2 to_power k) (#) (((abs f1) to_power k) + ((abs g1) to_power k));
A6: (Ef /\ Eg) ` = (X \ Ef) \/ (X \ Eg) by XBOOLE_1:54;
( Ef ` is Element of S & Eg ` is Element of S ) by MEASURE1:66;
then ( Ef ` is measure_zero of M & Eg ` is measure_zero of M ) by A2, A3, MEASURE1:def 13;
then (Ef ` ) \/ (Eg ` ) is measure_zero of M by MEASURE1:70;
then A8: M . ((Ef /\ Eg) ` ) = 0 by A6, MEASURE1:def 13;
( f1 is_measurable_on Ef /\ Eg & g1 is_measurable_on Ef /\ Eg ) by A2, A3, MESFUNC6:16, XBOOLE_1:17;
then A11: f1 + g1 is_measurable_on Ef /\ Eg by MESFUNC6:26;
then A13: abs (f1 + g1) is_measurable_on Ef /\ Eg by A4, MESFUNC6:48;
((abs f1) to_power k) + ((abs g1) to_power k) is_integrable_on M by A1, A1a, A2a, Lm007;
then A17: (2 to_power k) (#) (((abs f1) to_power k) + ((abs g1) to_power k)) is_integrable_on M by MESFUNC6:102;
C1: ( dom (abs f1) = dom f1 & dom (abs g1) = dom g1 & dom (abs (f1 + g1)) = dom (f1 + g1) ) by VALUED_1:def 11;
then A21: (abs (f1 + g1)) to_power k is_measurable_on Ef /\ Eg by A4, A13, MESFUN6C:29;
A22: abs ((abs (f1 + g1)) to_power k) = (abs (f1 + g1)) to_power k by Lm002b;
A25: dom ((abs (f1 + g1)) to_power k) = Ef /\ Eg by A4, C1, MESFUN6C:def 6;
A28: dom ((2 to_power k) (#) (((abs f1) to_power k) + ((abs g1) to_power k))) = dom (((abs f1) to_power k) + ((abs g1) to_power k)) by VALUED_1:def 5
.= (dom ((abs f1) to_power k)) /\ (dom ((abs g1) to_power k)) by VALUED_1:def 1
.= (dom (abs f1)) /\ (dom ((abs g1) to_power k)) by MESFUN6C:def 6
.= (dom (abs f1)) /\ (dom (abs g1)) by MESFUN6C:def 6
.= dom (f1 + g1) by C1, VALUED_1:def 1
.= dom ((abs (f1 + g1)) to_power k) by C1, MESFUN6C:def 6 ;

now

let x be Element of X; :: thesis: ( x in dom ((abs (f1 + g1)) to_power k) implies abs (((abs (f1 + g1)) to_power k) . x) <= ((2 to_power k) (#) (((abs f1) to_power k) + ((abs g1) to_power k))) . x )
assume x in dom ((abs (f1 + g1)) to_power k) ; :: thesis: abs (((abs (f1 + g1)) to_power k) . x) <= ((2 to_power k) (#) (((abs f1) to_power k) + ((abs g1) to_power k))) . x
then (abs ((abs (f1 + g1)) to_power k)) . x <= ((2 to_power k) (#) (((abs f1) to_power k) + ((abs g1) to_power k))) . x by A22, Lm008, A2, A3, A25;
hence abs (((abs (f1 + g1)) to_power k) . x) <= ((2 to_power k) (#) (((abs f1) to_power k) + ((abs g1) to_power k))) . x by VALUED_1:18; :: thesis: verum

end;

then (abs (f1 + g1)) to_power k is_integrable_on M by A21, A25, A28, A17, MESFUNC6:96;
hence f + g in Lp_Functions M,k by A1a, A2a, A8, A4, A11; :: thesis: verum