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).|| = (abs 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).|| = (abs a) * ||.x.|| )
A1: 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:12
.= abs (a * ((seq_id x) . n)) by SEQ_1:9
.= (abs a) * (abs ((seq_id x) . n)) by COMPLEX1:65
.= (abs a) * ((abs (seq_id x)) . n) by SEQ_1:12 ;
hence (abs (a (#) (seq_id x))) . n = (abs a) * ((abs (seq_id x)) . n) ; :: thesis: verum

end;

(abs (seq_id x)) . 1 = abs ((seq_id x) . 1) by SEQ_1:12;
then A2: 0 <= (abs (seq_id x)) . 1 by COMPLEX1:46;
A3: 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 Th3
.= (abs ((seq_id x) + (seq_id y))) . n by RSSPACE:1
.= abs (((seq_id x) + (seq_id y)) . n) by SEQ_1:12
.= abs (((seq_id x) . n) + ((seq_id y) . n)) by SEQ_1:7 ;
hence (abs (seq_id (x + y))) . n = abs (((seq_id x) . n) + ((seq_id y) . n)) ; :: thesis: verum

end;

A4: 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:56;
then (abs (seq_id (x + y))) . n <= (abs ((seq_id x) . n)) + (abs ((seq_id y) . n)) by A3;
then (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + (abs ((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 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:7;
hence (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) + (abs (seq_id y))) . n by A4; :: thesis: verum

end;

A6: now

assume A7: x = 0. linfty_Space ; :: thesis: ||.x.|| = 0
A8: for n being Nat holds (seq_id x) . n = 0

proof

let n be Nat; :: thesis: (seq_id x) . n = 0
n in NAT by ORDINAL1:def 12;
hence (seq_id x) . n = 0 by A7, Th3, RSSPACE:def 6; :: thesis: verum

end;

thus ||.x.|| = upper_bound (rng (abs (seq_id x))) by Th3
.= 0 by A8, Lm6 ; :: 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 bounded by MEASURE6:39;
then A10: rng (abs (seq_id x)) is bounded_above by XXREAL_2:def 11;

A11: now

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 Th3;
then for n being Element of NAT holds 0 = (seq_id x) . n by A13, Lm7;
hence x = 0. linfty_Space by A12, Th3, RSSPACE:def 6; :: thesis: verum

end;

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

now

let n be Element of 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 Th3;
||.(a * x).|| = upper_bound (rng (abs (seq_id (a * x)))) by Th3
.= upper_bound (rng (abs (seq_id (a (#) (seq_id x))))) by Th3
.= upper_bound (rng (abs (a (#) (seq_id x)))) by RSSPACE:1
.= upper_bound (rng ((abs a) (#) (abs (seq_id x)))) by A1, SEQ_1:9
.= upper_bound ((abs a) ** (rng (abs (seq_id x)))) by INTEGRA2:17
.= (abs a) * (upper_bound (rng (abs (seq_id x)))) by A10, COMPLEX1:46, INTEGRA2:13
.= (abs a) * ||.x.|| by Th3 ;
hence ( ( ||.x.|| = 0 implies x = 0. linfty_Space ) & ( x = 0. linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| ) by A11, A6, A9, A19, A18, Th3; :: thesis: verum