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 ()) to_power (1 / p)) + ((Sum ()) 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 ()) to_power (1 / p)) + ((Sum ()) to_power (1 / p)) ) )
assume that
A1: p = 1 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 ()) to_power (1 / p)) + ((Sum ()) to_power (1 / p)) )
A4: now :: thesis: for n being Nat holds
( ((a + b) rto_power p) . n = |.((a + b) . n).| & () . n = |.(a . n).| & () . n = |.(b . n).| )
let n be Nat; :: thesis: ( ((a + b) rto_power p) . n = |.((a + b) . n).| & () . n = |.(a . n).| & () . n = |.(b . n).| )
thus ((a + b) rto_power p) . n = |.((a + b) . n).| to_power p by Def1
.= |.((a + b) . n).| by ; :: thesis: ( () . n = |.(a . n).| & () . n = |.(b . n).| )
thus () . n = |.(a . n).| to_power p by Def1
.= |.(a . n).| by ; :: thesis: () . n = |.(b . n).|
thus () . n = |.(b . n).| to_power p by Def1
.= |.(b . n).| by ; :: thesis: verum
end;
then A5: (a + b) rto_power p = abs (a + b) by SEQ_1:12;
A6: a = seq_id a ;
A7: a rto_power p = |.a.| by ;
then a is absolutely_summable by ;
then reconsider a1 = a as VECTOR of l1_Space by ;
|.b.| is summable by ;
then A8: |.a.| + |.b.| is summable by ;
A9: b rto_power p = |.b.| by ;
then A10: (Sum ()) to_power (1 / p) = Sum |.b.| by ;
A11: b = seq_id b ;
b is absolutely_summable by ;
then reconsider b1 = b as VECTOR of l1_Space by ;
A12: ||.b1.|| = Sum (abs (seq_id b1)) by ;
deffunc H1( Nat) -> set = |.(a . \$1).| + |.(b . \$1).|;
consider c being Real_Sequence such that
A14: for n being Nat holds c . n = H1(n) from SEQ_1:sch 1();
A15: now :: thesis: for n being Nat holds
( (abs (a + b)) . n >= 0 & c . n = |.(a . n).| + |.(b . n).| & c . n = (|.a.| . n) + (|.b.| . n) & (abs (a + b)) . n <= c . n )
let n be Nat; :: thesis: ( (abs (a + b)) . n >= 0 & c . n = |.(a . n).| + |.(b . n).| & c . n = (|.a.| . n) + (|.b.| . n) & (abs (a + b)) . n <= c . n )
A16: (abs (a + b)) . n = |.((a + b) . n).| by SEQ_1:12;
hence (abs (a + b)) . n >= 0 by COMPLEX1:46; :: thesis: ( c . n = |.(a . n).| + |.(b . n).| & c . n = (|.a.| . n) + (|.b.| . n) & (abs (a + b)) . n <= c . n )
thus c . n = |.(a . n).| + |.(b . n).| by A14; :: thesis: ( c . n = (|.a.| . n) + (|.b.| . n) & (abs (a + b)) . n <= c . n )
|.(a . n).| + |.(b . n).| = (|.a.| . n) + |.(b . n).| by SEQ_1:12
.= (|.a.| . n) + (|.b.| . n) by SEQ_1:12 ;
hence c . n = (|.a.| . n) + (|.b.| . n) by A14; :: thesis: (abs (a + b)) . n <= c . n
|.((a + b) . n).| = |.((a . n) + (b . n)).| by SEQ_1:7;
then |.(a + b).| . n <= |.(a . n).| + |.(b . n).| by ;
hence (abs (a + b)) . n <= c . n by A14; :: thesis: verum
end;
then c = |.a.| + |.b.| by SEQ_1:7;
hence (a + b) rto_power p is summable by ; :: thesis: (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum ()) to_power (1 / p)) + ((Sum ()) to_power (1 / p))
A17: ||.a1.|| = Sum (abs (seq_id a1)) by ;
A19: ||.(a1 + b1).|| = Sum (abs (seq_id (a1 + b1))) by
.= Sum (abs (seq_id ((seq_id a1) + (seq_id b1)))) by RSSPACE3:6
.= Sum (abs ((seq_id a1) + (seq_id b1))) ;
A20: ||.(a1 + b1).|| <= ||.a1.|| + ||.b1.|| by RSSPACE3:7;
(Sum ()) to_power (1 / p) = Sum |.a.| by ;
hence (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum ()) to_power (1 / p)) + ((Sum ()) to_power (1 / p)) by A1, A5, A10, A20, A19, A17, A12, POWER:25; :: thesis: verum