let a, b be Real_Sequence; :: thesis: for p being Real st 1 <= p & a rto_power p is summable & b rto_power p is summable holds
( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) )
let p be Real; :: thesis: ( 1 <= p & a rto_power p is summable & b rto_power p is summable implies ( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) ) )
assume that
A1: 1 <= p and
A2: a rto_power p is summable and
A3: b rto_power p is summable ; :: thesis: ( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) )
set ab = (a + b) rto_power p;
set bp = b rto_power p;
set ap = a rto_power p;

A4: now :: thesis: for n being Nat holds
( (a rto_power p) . n = |.(a . n).| to_power p & (b rto_power p) . n = |.(b . n).| to_power p & ((a + b) rto_power p) . n = |.((a . n) + (b . n)).| to_power p )

let n be Nat; :: thesis: ( (a rto_power p) . n = |.(a . n).| to_power p & (b rto_power p) . n = |.(b . n).| to_power p & ((a + b) rto_power p) . n = |.((a . n) + (b . n)).| to_power p )
thus (a rto_power p) . n = |.(a . n).| to_power p by Def1; :: thesis: ( (b rto_power p) . n = |.(b . n).| to_power p & ((a + b) rto_power p) . n = |.((a . n) + (b . n)).| to_power p )
thus (b rto_power p) . n = |.(b . n).| to_power p by Def1; :: thesis: ((a + b) rto_power p) . n = |.((a . n) + (b . n)).| to_power p
((a + b) rto_power p) . n = |.((a + b) . n).| to_power p by Def1
.= |.((a . n) + (b . n)).| to_power p by SEQ_1:7 ;
hence ((a + b) rto_power p) . n = |.((a . n) + (b . n)).| to_power p ; :: thesis: verum

end;

reconsider p = p as Real ;

now :: thesis: ( ( p > 1 & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) & (a + b) rto_power p is summable ) or ( p = 1 & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) & (a + b) rto_power p is summable ) )

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

case p > 1 ; :: thesis: ( (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) & (a + b) rto_power p is summable )

hence ( (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) & (a + b) rto_power p is summable ) by A2, A3, A4, HOLDER_1:13; :: thesis: verum

end;

case p = 1 ; :: thesis: ( (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) & (a + b) rto_power p is summable )

hence ( (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) & (a + b) rto_power p is summable ) by A2, A3, Lm4; :: thesis: verum

end;

end;

end;

hence ( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) ) ; :: thesis: verum