let x, y be Point of Complex_l1_Space; for p being Complex holds
( ( ||.x.|| = 0 implies x = 0. Complex_l1_Space ) & ( x = 0. Complex_l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(p * x).|| = |.p.| * ||.x.|| )
let p be Complex; ( ( ||.x.|| = 0 implies x = 0. Complex_l1_Space ) & ( x = 0. Complex_l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(p * x).|| = |.p.| * ||.x.|| )
A1:
for n being Nat holds 0 <= |.(seq_id x).| . n
A3:
for n being Nat holds |.(seq_id (x + y)).| . n = |.(((seq_id x) . n) + ((seq_id y) . n)).|
A5:
for n being Nat holds |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + (|.(seq_id y).| . n)
A6:
for n being Nat holds |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n
seq_id y is absolutely_summable
by Def1;
then A7:
|.(seq_id y).| is summable
by COMSEQ_3:def 9;
seq_id x is absolutely_summable
by Def1;
then
|.(seq_id x).| is summable
by COMSEQ_3:def 9;
then
|.(seq_id x).| + |.(seq_id y).| is summable
by A7, SERIES_1:7;
then A8:
Sum |.(seq_id (x + y)).| <= Sum (|.(seq_id x).| + |.(seq_id y).|)
by A6, A2, SERIES_1:20;
A11:
Sum |.(seq_id (x + y)).| = ||.(x + y).||
by Th5;
A15:
( ||.x.|| = Sum |.(seq_id x).| & ||.y.|| = Sum |.(seq_id y).| )
by Th5;
A16:
for n being Nat holds |.(p (#) (seq_id x)).| . n = |.p.| * (|.(seq_id x).| . n)
seq_id x is absolutely_summable
by Def1;
then A17:
|.(seq_id x).| is summable
by COMSEQ_3:def 9;
seq_id x is absolutely_summable
by Def1;
then A18:
|.(seq_id x).| is summable
by COMSEQ_3:def 9;
||.(p * x).|| =
Sum |.(seq_id (p * x)).|
by Th5
.=
Sum |.(seq_id (p (#) (seq_id x))).|
by Th5
.=
Sum (|.p.| (#) |.(seq_id x).|)
by A16, SEQ_1:9
.=
|.p.| * (Sum |.(seq_id x).|)
by A17, SERIES_1:10
.=
|.p.| * ||.x.||
by Th5
;
hence
( ( ||.x.|| = 0 implies x = 0. Complex_l1_Space ) & ( x = 0. Complex_l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(p * x).|| = |.p.| * ||.x.|| )
by A12, A9, A1, A18, A15, A11, A7, A8, SERIES_1:7, SERIES_1:18; verum