let p be Real; :: thesis: ( 1 <= p implies for a, b being Real_Sequence
for n being Element of NAT holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) )
assume A1: 1 <= p ; :: thesis: for a, b being Real_Sequence
for n being Element of NAT holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
let a, b be Real_Sequence; :: thesis: for n being Element of NAT holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
set ap = a rto_power p;
set bp = b rto_power p;
set ab = (a + b) rto_power p;
let n be Element of NAT ; :: thesis: ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))

now

per cases ( p > 1 or p = 1 ) by A1, XXREAL_0:1;

case A2: p > 1 ; :: thesis: ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))

now

let n be Element of NAT ; :: thesis: ( (a rto_power p) . n = (abs (a . n)) to_power p & (b rto_power p) . n = (abs (b . n)) to_power p & ((a + b) rto_power p) . n = (abs ((a . n) + (b . n))) to_power p )
thus (a rto_power p) . n = (abs (a . n)) to_power p by Def1; :: thesis: ( (b rto_power p) . n = (abs (b . n)) to_power p & ((a + b) rto_power p) . n = (abs ((a . n) + (b . n))) to_power p )
thus (b rto_power p) . n = (abs (b . n)) to_power p by Def1; :: thesis: ((a + b) rto_power p) . n = (abs ((a . n) + (b . n))) to_power p
((a + b) rto_power p) . n = (abs ((a + b) . n)) to_power p by Def1
.= (abs ((a . n) + (b . n))) to_power p by SEQ_1:11 ;
hence ((a + b) rto_power p) . n = (abs ((a . n) + (b . n))) to_power p ; :: thesis: verum

end;

hence ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) by A2, HOLDER_1:7; :: thesis: verum

end;

case p = 1 ; :: thesis: ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))

hence ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) by Lm3; :: thesis: verum

end;

end;

end;

hence ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) ; :: thesis: verum