let x, y be Point of l1_Space; :: thesis: for a being Real holds
( ( ||.x.|| = 0 implies x = 0. l1_Space ) & ( x = 0. l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
let a be Real; :: thesis: ( ( ||.x.|| = 0 implies x = 0. l1_Space ) & ( x = 0. l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
A1: for n being Nat holds 0 <= (abs (seq_id x)) . n

proof

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

end;

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

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

end;

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

proof

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

end;

A4: for n being Nat holds (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n)

proof

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

end;

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

proof

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

end;

seq_id y is absolutely_summable by Def1;
then A6: abs (seq_id y) is summable by SERIES_1:def 4;
seq_id x is absolutely_summable by Def1;
then abs (seq_id x) is summable by SERIES_1:def 4;
then (abs (seq_id x)) + (abs (seq_id y)) is summable by A6, SERIES_1:7;
then A7: Sum (abs (seq_id (x + y))) <= Sum ((abs (seq_id x)) + (abs (seq_id y))) by A5, A2, SERIES_1:20;

A8: now :: thesis: ( x = 0. l1_Space implies ||.x.|| = 0 )

assume x = 0. l1_Space ; :: thesis: ||.x.|| = 0
then A9: for n being Nat holds (seq_id x) . n = 0 by Th6;
thus ||.x.|| = Sum (abs (seq_id x)) by Def2
.= 0 by A9, Th3 ; :: thesis: verum

end;

A10: Sum (abs (seq_id (x + y))) = ||.(x + y).|| by Th6;

A11: now :: thesis: ( ||.x.|| = 0 implies x = 0. l1_Space )

A12: x in the_set_of_RealSequences by Def1;
assume A13: ||.x.|| = 0 ; :: thesis: x = 0. l1_Space
( ||.x.|| = Sum (abs (seq_id x)) & seq_id x is absolutely_summable ) by Th6;
then for n being Nat holds 0 = (seq_id x) . n by A13, Th4;
hence x = 0. l1_Space by A12, Th6, RSSPACE:5; :: thesis: verum

end;

A14: ( ||.x.|| = Sum (abs (seq_id x)) & ||.y.|| = Sum (abs (seq_id y)) ) by Th6;
A15: for n being Nat holds (abs (a (#) (seq_id x))) . n = |.a.| * ((abs (seq_id x)) . n)

proof

let n be Nat; :: thesis: (abs (a (#) (seq_id x))) . n = |.a.| * ((abs (seq_id x)) . n)
(abs (a (#) (seq_id x))) . n = |.((a (#) (seq_id x)) . n).| by SEQ_1:12
.= |.(a * ((seq_id x) . n)).| by SEQ_1:9
.= |.a.| * |.((seq_id x) . n).| by COMPLEX1:65
.= |.a.| * ((abs (seq_id x)) . n) by SEQ_1:12 ;
hence (abs (a (#) (seq_id x))) . n = |.a.| * ((abs (seq_id x)) . n) ; :: thesis: verum

end;

seq_id x is absolutely_summable by Def1;
then A16: abs (seq_id x) is summable by SERIES_1:def 4;
seq_id x is absolutely_summable by Def1;
then A17: abs (seq_id x) is summable by SERIES_1:def 4;
||.(a * x).|| = Sum (abs (seq_id (a * x))) by Th6
.= Sum |.(seq_id (a (#) (seq_id x))).| by Th6
.= Sum (|.a.| (#) (abs (seq_id x))) by A15, SEQ_1:9
.= |.a.| * (Sum (abs (seq_id x))) by A16, SERIES_1:10
.= |.a.| * ||.x.|| by Th6 ;
hence ( ( ||.x.|| = 0 implies x = 0. l1_Space ) & ( x = 0. l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| ) by A11, A8, A1, A17, A14, A10, A6, A7, SERIES_1:7, SERIES_1:18; :: thesis: verum