let x, y be Point of Complex_l1_Space; :: thesis: 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; :: thesis: ( ( ||.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

proof

let n be Nat; :: thesis: 0 <= |.(seq_id x).| . n
0 <= |.((seq_id x) . n).| by COMPLEX1:46;
hence 0 <= |.(seq_id x).| . n by VALUED_1:18; :: thesis: verum

end;

A2: now :: thesis: for n being Nat holds 0 <= |.(seq_id (x + y)).| . n

let n be Nat; :: thesis: 0 <= |.(seq_id (x + y)).| . n
|.(seq_id (x + y)).| . n = |.((seq_id (x + y)) . n).| by VALUED_1:18;
hence 0 <= |.(seq_id (x + y)).| . n by COMPLEX1:46; :: thesis: verum

end;

A3: for n being Nat holds |.(seq_id (x + y)).| . n = |.(((seq_id x) . n) + ((seq_id y) . n)).|

proof

let n be Nat; :: thesis: |.(seq_id (x + y)).| . n = |.(((seq_id x) . n) + ((seq_id y) . n)).|
A4: n in NAT by ORDINAL1:def 12;
|.(seq_id (x + y)).| . n = |.(seq_id ((seq_id x) + (seq_id y))).| . n by Th5
.= |.(((seq_id x) + (seq_id y)) . n).| by VALUED_1:18
.= |.(((seq_id x) . n) + ((seq_id y) . n)).| by VALUED_1:1, A4 ;
hence |.(seq_id (x + y)).| . n = |.(((seq_id x) . n) + ((seq_id y) . n)).| ; :: thesis: verum

end;

A5: for n being Nat holds |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + (|.(seq_id y).| . n)

proof

let n be Nat; :: thesis: |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + (|.(seq_id y).| . n)
|.(((seq_id x) . n) + ((seq_id y) . n)).| <= |.((seq_id x) . n).| + |.((seq_id y) . n).| by COMPLEX1:56;
then |.(seq_id (x + y)).| . n <= |.((seq_id x) . n).| + |.((seq_id y) . n).| by A3;
then |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + |.((seq_id y) . n).| by VALUED_1:18;
hence |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + (|.(seq_id y).| . n) by VALUED_1:18; :: thesis: verum

end;

A6: for n being Nat holds |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n

proof

let n be Nat; :: thesis: |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n
(|.(seq_id x).| . n) + (|.(seq_id y).| . n) = (|.(seq_id x).| + |.(seq_id y).|) . n by SEQ_1:7;
hence |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n by A5; :: thesis: verum

end;

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;

A9: now :: thesis: ( x = 0. Complex_l1_Space implies ||.x.|| = 0 )

assume x = 0. Complex_l1_Space ; :: thesis: ||.x.|| = 0
then A10: for n being Nat holds (seq_id x) . n = 0 by Th5, CSSPACE:4;
thus ||.x.|| = Sum |.(seq_id x).| by Def2
.= 0 by A10, Th3 ; :: thesis: verum

end;

A11: Sum |.(seq_id (x + y)).| = ||.(x + y).|| by Th5;

A12: now :: thesis: ( ||.x.|| = 0 implies x = 0. Complex_l1_Space )

A13: x in the_set_of_ComplexSequences by Def1;
assume A14: ||.x.|| = 0 ; :: thesis: x = 0. Complex_l1_Space
( ||.x.|| = Sum |.(seq_id x).| & seq_id x is absolutely_summable ) by Th5;
then for n being Nat holds 0 = (seq_id x) . n by A14, CSSPACE2:13;
hence x = 0. Complex_l1_Space by A13, Th5, CSSPACE:5; :: thesis: verum

end;

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)

proof

let n be Nat; :: thesis: |.(p (#) (seq_id x)).| . n = |.p.| * (|.(seq_id x).| . n)
reconsider p = p as Element of COMPLEX by XCMPLX_0:def 2;
|.(p (#) (seq_id x)).| . n = |.((p (#) (seq_id x)) . n).| by VALUED_1:18
.= |.(p * ((seq_id x) . n)).| by VALUED_1:6
.= |.p.| * |.((seq_id x) . n).| by COMPLEX1:65
.= |.p.| * (|.(seq_id x).| . n) by VALUED_1:18 ;
hence |.(p (#) (seq_id x)).| . n = |.p.| * (|.(seq_id x).| . n) ; :: thesis: verum

end;

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