let p be Real; :: thesis: ( 1 = p implies for a, b being Real_Sequence
for n being 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 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 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 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 :: 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 (a + b) rto_power p = |.(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 = |.a.| by A2, SEQ_1:12;
then A4: ((Partial_Sums (a rto_power p)) . n) to_power (1 / p) = (Partial_Sums |.a.|) . n by A1, POWER:25;
deffunc H₁( Nat) -> set = |.(a . $1).| + |.(b . $1).|;
consider c being Real_Sequence such that
A5: for n being Nat holds c . n = H₁(n) from SEQ_1:sch 1();
A6: for n being Nat holds |.((a + b) . n).| <= |.(b . n).| + |.(a . n).|

proof

let n be Nat; :: thesis: |.((a + b) . n).| <= |.(b . n).| + |.(a . n).|
|.((a + b) . n).| = |.((a . n) + (b . n)).| by SEQ_1:7;
hence |.((a + b) . n).| <= |.(b . n).| + |.(a . n).| by COMPLEX1:56; :: thesis: verum

end;

now :: thesis: for n being Nat holds (abs (a + b)) . n <= c . n

let n be Nat; :: thesis: (abs (a + b)) . n <= c . n
A7: |.((a + b) . n).| = (abs (a + b)) . n by SEQ_1:12;
|.((a + b) . n).| <= |.(b . n).| + |.(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 :: thesis: for n being Nat holds c . n = ((abs a) + (abs b)) . n

let n be Nat; :: thesis: c . n = ((abs a) + (abs b)) . n
A9: |.(a . n).| = (abs a) . n by SEQ_1:12;
|.(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 object 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 = |.b.| by A2, SEQ_1:12;
then A11: ((Partial_Sums (b rto_power p)) . n) to_power (1 / p) = (Partial_Sums |.b.|) . n by A1, POWER:25;
Partial_Sums ((abs a) + (abs b)) = (Partial_Sums (abs a)) + (Partial_Sums |.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