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 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 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 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 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 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 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 A1: ( 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 A2: m = 1 ; :: thesis: r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m))

then A3: ( r1 = Integral (M,(abs f)) & r2 = Integral (M,(abs g)) & r3 = Integral (M,(abs (f + g))) ) by A1, Th8;
A4: 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 ND -measurable & (abs f1) to_power m is_integrable_on M ) ) by A1;
A5: 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 ND -measurable & (abs g1) to_power m is_integrable_on M ) ) by A1;
then ( abs f is_integrable_on M & abs g is_integrable_on M ) by A2, A4, Th8;
then ( f is_integrable_on M & g is_integrable_on M ) by A4, A5, MESFUNC6:94;
then Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g))) by LPSPACE1:55;
then A6: r3 <= r1 + r2 by A3, XXREAL_3:def 2;
( r1 to_power (1 / m) = r1 & r2 to_power (1 / m) = r2 ) by A2, POWER:25;
hence r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) by A6, A2, POWER:25; :: thesis: verum

end;

suppose A7: 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 A1, A7, XXREAL_0:1;
then 1 / m < 1 by XREAL_1:189;
then 0 < 1 - (1 / m) by XREAL_1:50;
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 A1, Lm5;
hence r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) by A1; :: thesis: verum

end;

end;