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:30 ; :: 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:30 ; :: 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:30 ; :: thesis: verum

end;

then A5: (a + b) rto_power p = abs (a + b) by SEQ_1:16;
A6: a rto_power p = abs a by A4, SEQ_1:16;
A7: b rto_power p = abs b by A4, SEQ_1:16;
A8: (Sum (a rto_power p)) to_power (1 / p) = Sum (abs a) by A1, A6, POWER:30;
A9: (Sum (b rto_power p)) to_power (1 / p) = Sum (abs b) by A1, A7, POWER:30;
A10: abs b is summable by A3, A4, SEQ_1:16;
A11: a is absolutely_summable by A2, A6, SERIES_1:def 5;
A12: b is absolutely_summable by A3, A7, SERIES_1:def 5;
A13: ( a = seq_id a & b = seq_id b ) by RSSPACE:3;
then reconsider a1 = a as VECTOR of l1_Space by A11, RSSPACE3:8;
reconsider b1 = b as VECTOR of l1_Space by A12, A13, RSSPACE3:8;
A14: ||.(a1 + b1).|| <= ||.a1.|| + ||.b1.|| by RSSPACE3:9;
A15: ||.(a1 + b1).|| = the norm of l1_Space . (a1 + b1) by NORMSP_1:def 1
.= 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:8
.= Sum (abs ((seq_id a1) + (seq_id b1))) by RSSPACE:3 ;
A16: ||.a1.|| = the norm of l1_Space . a1 by NORMSP_1:def 1
.= Sum (abs (seq_id a1)) by RSSPACE3:def 2, RSSPACE3:def 3 ;
A17: ||.b1.|| = the norm of l1_Space . b1 by NORMSP_1:def 1
.= Sum (abs (seq_id b1)) by RSSPACE3:def 2, RSSPACE3:def 3 ;
A18: seq_id a1 = a by RSSPACE:3;
A19: seq_id b1 = b by RSSPACE:3;
A20: ( (abs a) + (abs b) is summable & Sum ((abs a) + (abs b)) = (Sum (abs a)) + (Sum (abs b)) ) by A2, A6, A10, SERIES_1:10;
deffunc H₁( Element of NAT ) -> Element of REAL = (abs (a . $1)) + (abs (b . $1));
consider c being Real_Sequence such that
A21: for n being Element of NAT holds c . n = H₁(n) from SEQ_1:sch 1();

A22: 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 )
A23: (abs (a + b)) . n = abs ((a + b) . n) by SEQ_1:16;
hence (abs (a + b)) . n >= 0 by COMPLEX1:132; :: thesis: ( c . n = (abs (a . n)) + (abs (b . n)) & c . n = ((abs a) . n) + ((abs b) . n) & (abs (a + b)) . n <= c . n )
abs ((a + b) . n) = abs ((a . n) + (b . n)) by SEQ_1:11;
then A24: (abs (a + b)) . n <= (abs (a . n)) + (abs (b . n)) by A23, COMPLEX1:142;
thus c . n = (abs (a . n)) + (abs (b . n)) by A21; :: 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:16
.= ((abs a) . n) + ((abs b) . n) by SEQ_1:16 ;
hence c . n = ((abs a) . n) + ((abs b) . n) by A21; :: thesis: (abs (a + b)) . n <= c . n
thus (abs (a + b)) . n <= c . n by A21, A24; :: thesis: verum

end;

then c = (abs a) + (abs b) by SEQ_1:11;
hence (a + b) rto_power p is summable by A5, A20, A22, SERIES_1:24; :: 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))
thus (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, A8, A9, A14, A15, A16, A17, A18, A19, POWER:30; :: thesis: verum