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: now

assume A2: ||.x.|| = 0 ; :: thesis: x = 0. linfty_Space
A3: ||.x.|| = sup (rng (abs (seq_id x))) by Th3;
seq_id x is bounded by Th3;
then A4: for n being Element of NAT holds 0 = (seq_id x) . n by A2, A3, Lm7;
x in the_set_of_RealSequences by Def1;
hence x = 0. linfty_Space by A4, Th3, RSSPACE:def 6; :: thesis: verum

end;

A5: now

assume Z: x = 0. linfty_Space ; :: thesis: ||.x.|| = 0
A6: 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 13;
hence (seq_id x) . n = 0 by Th3, Z, RSSPACE:def 6; :: thesis: verum

end;

thus ||.x.|| = sup (rng (abs (seq_id x))) by Th3
.= 0 by A6, Lm6 ; :: thesis: verum

end;

A7: seq_id x is bounded by Def1;
A8: 0 <= sup (rng (abs (seq_id x)))

proof

A9: abs (seq_id x) is bounded by A7;
(abs (seq_id x)) . 1 = abs ((seq_id x) . 1) by SEQ_1:16;
then 0 <= (abs (seq_id x)) . 1 by COMPLEX1:132;
hence 0 <= sup (rng (abs (seq_id x))) by A9, Lm2; :: thesis: verum

end;

A10: ||.y.|| = sup (rng (abs (seq_id y))) by Th3;
A11: sup (rng (abs (seq_id (x + y)))) = ||.(x + y).|| by Th3;
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 Th3
.= (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 bounded by Def1;
then A15: abs (seq_id x) is bounded ;
seq_id y is bounded by Def1;
then A16: abs (seq_id y) is bounded ;
A17: upper_bound (rng (abs (seq_id (x + y)))) <= (upper_bound (rng (abs (seq_id x)))) + (upper_bound (rng (abs (seq_id y))))

proof

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))))
A18: (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) + (abs (seq_id y))) . n by A14;
A19: ((abs (seq_id x)) + (abs (seq_id y))) . n = ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n) by SEQ_1:11;
A20: (abs (seq_id x)) . n <= sup (rng (abs (seq_id x))) by A15, Lm2;
(abs (seq_id y)) . n <= sup (rng (abs (seq_id y))) by A16, Lm2;
then ((abs (seq_id x)) + (abs (seq_id y))) . n <= (upper_bound (rng (abs (seq_id x)))) + (upper_bound (rng (abs (seq_id y)))) by A19, A20, XREAL_1:9;
hence (abs (seq_id (x + y))) . n <= (upper_bound (rng (abs (seq_id x)))) + (upper_bound (rng (abs (seq_id y)))) by A18, XXREAL_0:2; :: thesis: verum

end;

hence upper_bound (rng (abs (seq_id (x + y)))) <= (upper_bound (rng (abs (seq_id x)))) + (upper_bound (rng (abs (seq_id y)))) by Lm1; :: thesis: verum

end;

A21: 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 bounded by Def1;
then abs (seq_id x) is bounded ;
then rng (abs (seq_id x)) is bounded by PSCOMP_1:7;
then A22: rng (abs (seq_id x)) is bounded_above by XXREAL_2:def 11;
||.(a * x).|| = sup (rng (abs (seq_id (a * x)))) by Th3
.= sup (rng (abs (seq_id (a (#) (seq_id x))))) by Th3
.= sup (rng (abs (a (#) (seq_id x)))) by RSSPACE:3
.= sup (rng ((abs a) (#) (abs (seq_id x)))) by A21, SEQ_1:13
.= sup ((abs a) ** (rng (abs (seq_id x)))) by INTEGRA2:17
.= (abs a) * (sup (rng (abs (seq_id x)))) by A22, COMPLEX1:132, 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 A1, A5, A8, A10, A11, A17, Th3; :: thesis: verum