let p be Real; :: thesis: ( 1 = p implies for a, b being Real_Sequence
for n being Element of NAT holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) )
assume A1: p = 1 ; :: thesis: for a, b being Real_Sequence
for n being Element of NAT holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
let a, b be Real_Sequence; :: thesis: for n being Element of NAT holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
let n be Element of NAT ; :: thesis: ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))

A2: 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 (a + b) rto_power p = abs (a + b) by SEQ_1:12;
then A3: ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) = (Partial_Sums (abs (a + b))) . n by A1, POWER:25;
a rto_power p = abs a by A2, SEQ_1:12;
then A4: ((Partial_Sums (a rto_power p)) . n) to_power (1 / p) = (Partial_Sums (abs a)) . n by A1, POWER:25;
deffunc H₁( Element of NAT ) -> Element of REAL = (abs (a . $1)) + (abs (b . $1));
consider c being Real_Sequence such that
A5: for n being Element of NAT holds c . n = H₁(n) from SEQ_1:sch 1();
A6: for n being Element of NAT holds abs ((a + b) . n) <= (abs (b . n)) + (abs (a . n))

proof

let n be Element of NAT ; :: thesis: abs ((a + b) . n) <= (abs (b . n)) + (abs (a . n))
abs ((a + b) . n) = abs ((a . n) + (b . n)) by SEQ_1:7;
hence abs ((a + b) . n) <= (abs (b . n)) + (abs (a . n)) by COMPLEX1:56; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: (abs (a + b)) . n <= c . n
A7: abs ((a + b) . n) = (abs (a + b)) . n by SEQ_1:12;
abs ((a + b) . n) <= (abs (b . n)) + (abs (a . n)) by A6;
hence (abs (a + b)) . n <= c . n by A5, A7; :: thesis: verum

end;

then A8: (Partial_Sums (abs (a + b))) . n <= (Partial_Sums c) . n by SERIES_1:14;

now

let n be Element of NAT ; :: thesis: c . n = ((abs a) + (abs b)) . n
A9: abs (a . n) = (abs a) . n by SEQ_1:12;
abs (b . n) = (abs b) . n by SEQ_1:12;
hence c . n = ((abs a) . n) + ((abs b) . n) by A5, A9
.= ((abs a) + (abs b)) . n by SEQ_1:7 ;
:: thesis: verum

end;

then for n being set st n in NAT holds
c . n = ((abs a) + (abs b)) . n ;
then A10: c = (abs a) + (abs b) by FUNCT_2:12;
b rto_power p = abs b by A2, SEQ_1:12;
then A11: ((Partial_Sums (b rto_power p)) . n) to_power (1 / p) = (Partial_Sums (abs b)) . n by A1, POWER:25;
Partial_Sums ((abs a) + (abs b)) = (Partial_Sums (abs a)) + (Partial_Sums (abs b)) by SERIES_1:5;
hence ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) by A3, A4, A11, A10, A8, SEQ_1:7; :: thesis: verum