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

let n be Element of NAT ; :: thesis: ( ((a + b) rto_power p) . n = abs ((a + b) . n) & (a rto_power p) . n = abs (a . n) & (b rto_power p) . n = abs (b . n) )
thus ((a + b) rto_power p) . n = (abs ((a + b) . n)) to_power p by Def1
.= abs ((a + b) . n) by A1, POWER:25 ; :: thesis: ( (a rto_power p) . n = abs (a . n) & (b rto_power p) . n = abs (b . n) )
thus (a rto_power p) . n = (abs (a . n)) to_power p by Def1
.= abs (a . n) by A1, POWER:25 ; :: thesis: (b rto_power p) . n = abs (b . n)
thus (b rto_power p) . n = (abs (b . n)) to_power p by Def1
.= abs (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 by RSSPACE:1;
A7: a rto_power p = abs 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;
abs b is summable by A3, A4, SEQ_1:12;
then A8: (abs a) + (abs b) is summable by A2, A7, SERIES_1:7;
A9: b rto_power p = abs b by A4, SEQ_1:12;
then A10: (Sum (b rto_power p)) to_power (1 / p) = Sum (abs b) by A1, POWER:25;
A11: b = seq_id b by RSSPACE:1;
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.|| = the normF of l1_Space . b1
.= Sum (abs (seq_id b1)) by RSSPACE3:def 2, RSSPACE3:def 3 ;
A13: seq_id b1 = b by RSSPACE:1;
deffunc H₁( Element of NAT ) -> Element of REAL = (abs (a . $1)) + (abs (b . $1));
consider c being Real_Sequence such that
A14: for n being Element of NAT holds c . n = H₁(n) from SEQ_1:sch 1();

A15: now

let n be Element of NAT ; :: thesis: ( (abs (a + b)) . n >= 0 & c . n = (abs (a . n)) + (abs (b . n)) & c . n = ((abs a) . n) + ((abs b) . n) & (abs (a + b)) . n <= c . n )
A16: (abs (a + b)) . n = abs ((a + b) . n) by SEQ_1:12;
hence (abs (a + b)) . n >= 0 by COMPLEX1:46; :: thesis: ( c . n = (abs (a . n)) + (abs (b . n)) & c . n = ((abs a) . n) + ((abs b) . n) & (abs (a + b)) . n <= c . n )
thus c . n = (abs (a . n)) + (abs (b . n)) by A14; :: thesis: ( c . n = ((abs a) . n) + ((abs b) . n) & (abs (a + b)) . n <= c . n )
(abs (a . n)) + (abs (b . n)) = ((abs a) . n) + (abs (b . n)) by SEQ_1:12
.= ((abs a) . n) + ((abs b) . n) by SEQ_1:12 ;
hence c . n = ((abs a) . n) + ((abs b) . n) by A14; :: thesis: (abs (a + b)) . n <= c . n
abs ((a + b) . n) = abs ((a . n) + (b . n)) by SEQ_1:7;
then (abs (a + b)) . n <= (abs (a . n)) + (abs (b . n)) by A16, COMPLEX1:56;
hence (abs (a + b)) . n <= c . n by A14; :: thesis: verum

end;

then c = (abs a) + (abs 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.|| = the normF of l1_Space . a1
.= Sum (abs (seq_id a1)) by RSSPACE3:def 2, RSSPACE3:def 3 ;
A18: seq_id a1 = a by RSSPACE:1;
A19: ||.(a1 + b1).|| = the normF of l1_Space . (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))) by RSSPACE:1 ;
A20: ||.(a1 + b1).|| <= ||.a1.|| + ||.b1.|| by RSSPACE3:7;
(Sum (a rto_power p)) to_power (1 / p) = Sum (abs 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, A18, A13, POWER:25; :: thesis: verum