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 ()) . n) to_power (1 / p)) + (((Partial_Sums ()) . 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 ()) . n) to_power (1 / p)) + (((Partial_Sums ()) . 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 ()) . n) to_power (1 / p)) + (((Partial_Sums ()) . n) to_power (1 / p))
let n be Nat; :: thesis: ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums ()) . n) to_power (1 / p)) + (((Partial_Sums ()) . n) to_power (1 / p))
A2: now :: thesis: for n being Nat holds
( ((a + b) rto_power p) . n = |.((a + b) . n).| & () . n = |.(a . n).| & () . n = |.(b . n).| )
let n be Nat; :: thesis: ( ((a + b) rto_power p) . n = |.((a + b) . n).| & () . n = |.(a . n).| & () . n = |.(b . n).| )
thus ((a + b) rto_power p) . n = |.((a + b) . n).| to_power p by Def1
.= |.((a + b) . n).| by ; :: thesis: ( () . n = |.(a . n).| & () . n = |.(b . n).| )
thus () . n = |.(a . n).| to_power p by Def1
.= |.(a . n).| by ; :: thesis: () . n = |.(b . n).|
thus () . n = |.(b . n).| to_power p by Def1
.= |.(b . n).| by ; :: 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 ;
a rto_power p = |.a.| by ;
then A4: ((Partial_Sums ()) . n) to_power (1 / p) = () . n by ;
deffunc H1( Nat) -> set = |.(a . \$1).| + |.(b . \$1).|;
consider c being Real_Sequence such that
A5: for n being Nat holds c . n = H1(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 <= () . 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 ;
then A11: ((Partial_Sums ()) . n) to_power (1 / p) = () . n by ;
Partial_Sums ((abs a) + (abs b)) = (Partial_Sums (abs a)) + () by SERIES_1:5;
hence ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums ()) . n) to_power (1 / p)) + (((Partial_Sums ()) . n) to_power (1 / p)) by A3, A4, A11, A10, A8, SEQ_1:7; :: thesis: verum