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 m being positive Real
for r1, r2, r3 being Element of REAL st 1 <= m & f in Lp_Functions M,m & g in Lp_Functions M,m & r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) holds
r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for m being positive Real
for r1, r2, r3 being Element of REAL st 1 <= m & f in Lp_Functions M,m & g in Lp_Functions M,m & r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) holds
r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m))
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL
for m being positive Real
for r1, r2, r3 being Element of REAL st 1 <= m & f in Lp_Functions M,m & g in Lp_Functions M,m & r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) holds
r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m))
let f, g be PartFunc of X,REAL ; :: thesis: for m being positive Real
for r1, r2, r3 being Element of REAL st 1 <= m & f in Lp_Functions M,m & g in Lp_Functions M,m & r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) holds
r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m))
let m be positive Real; :: thesis: for r1, r2, r3 being Element of REAL st 1 <= m & f in Lp_Functions M,m & g in Lp_Functions M,m & r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) holds
r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m))
let r1, r2, r3 be Element of REAL ; :: thesis: ( 1 <= m & f in Lp_Functions M,m & g in Lp_Functions M,m & r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) implies r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) )
assume AS: ( 1 <= m & f in Lp_Functions M,m & g in Lp_Functions M,m & r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) ) ; :: thesis: r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m))

per cases ( m = 1 or m <> 1 ) ;

suppose S1: m = 1 ; :: thesis: r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m))

then K1: ( r1 = Integral M,(abs f) & r2 = Integral M,(abs g) & r3 = Integral M,(abs (f + g)) ) by AS, LmPW006;
L01: ex f1 being PartFunc of X,REAL st
( f = f1 & ex ND being Element of S st
( M . (ND ` ) = 0 & dom f1 = ND & f1 is_measurable_on ND & (abs f1) to_power m is_integrable_on M ) ) by AS;
R01: ex g1 being PartFunc of X,REAL st
( g = g1 & ex ND being Element of S st
( M . (ND ` ) = 0 & dom g1 = ND & g1 is_measurable_on ND & (abs g1) to_power m is_integrable_on M ) ) by AS;
then ( abs f is_integrable_on M & abs g is_integrable_on M ) by S1, L01, LmPW006;
then ( f is_integrable_on M & g is_integrable_on M ) by L01, R01, MESFUNC6:94;
then Integral M,(abs (f + g)) <= (Integral M,(abs f)) + (Integral M,(abs g)) by LPSPACE1:56;
then L: r3 <= r1 + r2 by K1, XXREAL_3:def 2;
( r1 to_power (1 / m) = r1 & r2 to_power (1 / m) = r2 ) by S1, POWER:30;
hence r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) by L, S1, POWER:30; :: thesis: verum

end;

suppose S2: m <> 1 ; :: thesis: r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m))

set n1 = 1 - (1 / m);
1 < m by AS, S2, XXREAL_0:1;
then 1 / m < 1 by XREAL_1:191;
then 0 < 1 - (1 / m) by XREAL_1:52;
then reconsider n = 1 / (1 - (1 / m)) as positive Real ;
(1 / m) + (1 / n) = 1 ;
then ex rr1, rr2, rr3 being Real st
( rr1 = Integral M,((abs f) to_power m) & rr2 = Integral M,((abs g) to_power m) & rr3 = Integral M,((abs (f + g)) to_power m) & rr3 to_power (1 / m) <= (rr1 to_power (1 / m)) + (rr2 to_power (1 / m)) ) by AS, Th002;
hence r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) by AS; :: thesis: verum

end;

end;