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).|| = (abs 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).|| = (abs a) * ||.x.|| )

A1: now

assume A2: ||.x.|| = 0 ; :: thesis: x = 0. l1_Space
A3: ||.x.|| = Sum (abs (seq_id x)) by Th8;
seq_id x is absolutely_summable by Th8;
then A4: for n being Element of NAT holds 0 = (seq_id x) . n by A2, A3, Th6;
x in the_set_of_RealSequences by Def1;
hence x = 0. l1_Space by A4, Th8, RSSPACE:def 6; :: thesis: verum

end;

A5: now

assume x = 0. l1_Space ; :: thesis: ||.x.|| = 0
then A6: for n being Element of NAT holds (seq_id x) . n = 0 by Th8, RSSPACE:def 6;
thus ||.x.|| = the norm of l1_Space . x by NORMSP_1:def 1
.= Sum (abs (seq_id x)) by Def2
.= 0 by A6, Th5 ; :: thesis: verum

end;

A7: for n being Element of NAT holds 0 <= (abs (seq_id x)) . n

proof

let n be Element of NAT ; :: thesis: 0 <= (abs (seq_id x)) . n
0 <= abs ((seq_id x) . n) by COMPLEX1:132;
hence 0 <= (abs (seq_id x)) . n by SEQ_1:16; :: thesis: verum

end;

seq_id x is absolutely_summable by Def1;
then A8: abs (seq_id x) is summable by SERIES_1:def 5;
A9: ||.x.|| = Sum (abs (seq_id x)) by Th8;
A10: ||.y.|| = Sum (abs (seq_id y)) by Th8;
A11: Sum (abs (seq_id (x + y))) = ||.(x + y).|| by Th8;
A12: for n being Element of NAT holds (abs (seq_id (x + y))) . n = abs (((seq_id x) . n) + ((seq_id y) . n))

proof

let n be Element of NAT ; :: thesis: (abs (seq_id (x + y))) . n = abs (((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 Th8
.= (abs ((seq_id x) + (seq_id y))) . n by RSSPACE:3
.= abs (((seq_id x) + (seq_id y)) . n) by SEQ_1:16
.= abs (((seq_id x) . n) + ((seq_id y) . n)) by SEQ_1:11 ;
hence (abs (seq_id (x + y))) . n = abs (((seq_id x) . n) + ((seq_id y) . n)) ; :: thesis: verum

end;

A13: for n being Element of NAT holds (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n)

proof

let n be Element of NAT ; :: thesis: (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n)
abs (((seq_id x) . n) + ((seq_id y) . n)) <= (abs ((seq_id x) . n)) + (abs ((seq_id y) . n)) by COMPLEX1:142;
then (abs (seq_id (x + y))) . n <= (abs ((seq_id x) . n)) + (abs ((seq_id y) . n)) by A12;
then (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + (abs ((seq_id y) . n)) by SEQ_1:16;
hence (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n) by SEQ_1:16; :: thesis: verum

end;

A14: for n being Element of NAT holds (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) + (abs (seq_id y))) . n

proof

let n be Element of 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:11;
hence (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) + (abs (seq_id y))) . n by A13; :: thesis: verum

end;

seq_id x is absolutely_summable by Def1;
then A15: abs (seq_id x) is summable by SERIES_1:def 5;
seq_id y is absolutely_summable by Def1;
then A16: abs (seq_id y) is summable by SERIES_1:def 5;
then A17: (abs (seq_id x)) + (abs (seq_id y)) is summable by A15, SERIES_1:10;

now

let n be Element of NAT ; :: thesis: 0 <= (abs (seq_id (x + y))) . n
(abs (seq_id (x + y))) . n = abs ((seq_id (x + y)) . n) by SEQ_1:16;
hence 0 <= (abs (seq_id (x + y))) . n by COMPLEX1:132; :: thesis: verum

end;

then A18: Sum (abs (seq_id (x + y))) <= Sum ((abs (seq_id x)) + (abs (seq_id y))) by A14, A17, SERIES_1:24;
A19: for n being Element of NAT holds (abs (a (#) (seq_id x))) . n = (abs a) * ((abs (seq_id x)) . n)

proof

let n be Element of NAT ; :: thesis: (abs (a (#) (seq_id x))) . n = (abs a) * ((abs (seq_id x)) . n)
(abs (a (#) (seq_id x))) . n = abs ((a (#) (seq_id x)) . n) by SEQ_1:16
.= abs (a * ((seq_id x) . n)) by SEQ_1:13
.= (abs a) * (abs ((seq_id x) . n)) by COMPLEX1:151
.= (abs a) * ((abs (seq_id x)) . n) by SEQ_1:16 ;
hence (abs (a (#) (seq_id x))) . n = (abs a) * ((abs (seq_id x)) . n) ; :: thesis: verum

end;

seq_id x is absolutely_summable by Def1;
then A20: abs (seq_id x) is summable by SERIES_1:def 5;
||.(a * x).|| = Sum (abs (seq_id (a * x))) by Th8
.= Sum (abs (seq_id (a (#) (seq_id x)))) by Th8
.= Sum (abs (a (#) (seq_id x))) by RSSPACE:3
.= Sum ((abs a) (#) (abs (seq_id x))) by A19, SEQ_1:13
.= (abs a) * (Sum (abs (seq_id x))) by A20, SERIES_1:13
.= (abs a) * ||.x.|| by Th8 ;
hence ( ( ||.x.|| = 0 implies x = 0. l1_Space ) & ( x = 0. l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| ) by A1, A5, A7, A8, A9, A10, A11, A16, A18, SERIES_1:10, SERIES_1:21; :: thesis: verum