let x, y be Point of linfty_Space; :: thesis: for a being Real holds
( ( ||.x.|| = 0 implies x = 0. linfty_Space ) & ( x = 0. linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
let a be Real; :: thesis: ( ( ||.x.|| = 0 implies x = 0. linfty_Space ) & ( x = 0. linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
A1: 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)
|.(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;

(abs (seq_id x)) . 1 = |.((seq_id x) . 1).| by SEQ_1:12;
then A2: 0 <= (abs (seq_id x)) . 1 by COMPLEX1:46;
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 Th2
.= |.(((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;

A6: now :: thesis: ( x = 0. linfty_Space implies ||.x.|| = 0 )

assume A7: x = 0. linfty_Space ; :: thesis: ||.x.|| = 0
A8: for n being Nat holds (seq_id x) . n = 0 by A7, Th2;
thus ||.x.|| = upper_bound (rng (abs (seq_id x))) by Th2
.= 0 by A8, Lm5 ; :: thesis: verum

end;

seq_id x is bounded by Def1;
then A9: 0 <= upper_bound (rng (abs (seq_id x))) by A2, Lm2;
seq_id x is bounded by Def1;
then rng (abs (seq_id x)) is real-bounded by MEASURE6:39;
then A10: rng (abs (seq_id x)) is bounded_above ;

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

A12: x in the_set_of_RealSequences by Def1;
assume A13: ||.x.|| = 0 ; :: thesis: x = 0. linfty_Space
( ||.x.|| = upper_bound (rng (abs (seq_id x))) & seq_id x is bounded ) by Th2;
then for n being Nat holds 0 = (seq_id x) . n by A13, Lm6;
hence x = 0. linfty_Space by A12, Th2, RSSPACE:5; :: thesis: verum

end;

A14: seq_id y is bounded by Def1;
A15: seq_id x is bounded by Def1;

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

let n be Nat; :: thesis: (abs (seq_id (x + y))) . n <= (upper_bound (rng (abs (seq_id x)))) + (upper_bound (rng (abs (seq_id y))))
A16: (abs (seq_id y)) . n <= upper_bound (rng (abs (seq_id y))) by A14, Lm2;
( ((abs (seq_id x)) + (abs (seq_id y))) . n = ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n) & (abs (seq_id x)) . n <= upper_bound (rng (abs (seq_id x))) ) by A15, Lm2, SEQ_1:7;
then A17: ((abs (seq_id x)) + (abs (seq_id y))) . n <= (upper_bound (rng (abs (seq_id x)))) + (upper_bound (rng (abs (seq_id y)))) by A16, XREAL_1:7;
(abs (seq_id (x + y))) . n <= ((abs (seq_id x)) + (abs (seq_id y))) . n by A5;
hence (abs (seq_id (x + y))) . n <= (upper_bound (rng (abs (seq_id x)))) + (upper_bound (rng (abs (seq_id y)))) by A17, XXREAL_0:2; :: thesis: verum

end;

then A18: upper_bound (rng (abs (seq_id (x + y)))) <= (upper_bound (rng (abs (seq_id x)))) + (upper_bound (rng (abs (seq_id y)))) by Lm1;
A19: ( ||.y.|| = upper_bound (rng (abs (seq_id y))) & upper_bound (rng (abs (seq_id (x + y)))) = ||.(x + y).|| ) by Th2;
||.(a * x).|| = upper_bound (rng (abs (seq_id (a * x)))) by Th2
.= upper_bound (rng |.(seq_id (a (#) (seq_id x))).|) by Th2
.= upper_bound (rng (|.a.| (#) (abs (seq_id x)))) by A1, SEQ_1:9
.= upper_bound (|.a.| ** (rng (abs (seq_id x)))) by INTEGRA2:17
.= |.a.| * (upper_bound (rng (abs (seq_id x)))) by A10, COMPLEX1:46, INTEGRA2:13
.= |.a.| * ||.x.|| by Th2 ;
hence ( ( ||.x.|| = 0 implies x = 0. linfty_Space ) & ( x = 0. linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| ) by A11, A6, A9, A19, A18, Th2; :: thesis: verum