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: 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 (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) )

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

let n be Nat; :: thesis: ( ((a + b) rto_power p) . n = |.((a + b) . n).| & (a rto_power p) . n = |.(a . n).| & (b rto_power p) . n = |.(b . n).| )
thus ((a + b) rto_power p) . n = |.((a + b) . n).| to_power p by Def1
.= |.((a + b) . n).| by A1, POWER:25 ; :: thesis: ( (a rto_power p) . n = |.(a . n).| & (b rto_power p) . n = |.(b . n).| )
thus (a rto_power p) . n = |.(a . n).| to_power p by Def1
.= |.(a . n).| by A1, POWER:25 ; :: thesis: (b rto_power p) . n = |.(b . n).|
thus (b rto_power p) . n = |.(b . n).| to_power p by Def1
.= |.(b . n).| by A1, POWER:25 ; :: 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 A4, SEQ_1:12;
then a is absolutely_summable by A2, SERIES_1:def 4;
then reconsider a1 = a as VECTOR of l1_Space by A6, RSSPACE3:6;
|.b.| is summable by A3, A4, SEQ_1:12;
then A8: |.a.| + |.b.| is summable by A2, A7, SERIES_1:7;
A9: b rto_power p = |.b.| by A4, SEQ_1:12;
then A10: (Sum (b rto_power p)) to_power (1 / p) = Sum |.b.| by A1, POWER:25;
A11: b = seq_id b ;
b is absolutely_summable by A3, A9, SERIES_1:def 4;
then reconsider b1 = b as VECTOR of l1_Space by A11, RSSPACE3:6;
A12: ||.b1.|| = Sum (abs (seq_id b1)) by RSSPACE3:def 2, RSSPACE3:def 3;
deffunc H₁( Nat) -> set = |.(a . $1).| + |.(b . $1).|;
consider c being Real_Sequence such that
A14: for n being Nat holds c . n = H₁(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 A16, COMPLEX1:56;
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 A5, A8, A15, SERIES_1:20; :: 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))
A17: ||.a1.|| = Sum (abs (seq_id a1)) by RSSPACE3:def 2, RSSPACE3:def 3;
A19: ||.(a1 + b1).|| = Sum (abs (seq_id (a1 + b1))) by RSSPACE3:def 2, RSSPACE3:def 3
.= 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 (a rto_power p)) to_power (1 / p) = Sum |.a.| by A1, A7, POWER:25;
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)) by A1, A5, A10, A20, A19, A17, A12, POWER:25; :: thesis: verum