let x, y be Point of Complex_linfty_Space ; :: thesis: for c being Complex holds
( ( ||.x.|| = 0 implies x = 0. Complex_linfty_Space ) & ( x = 0. Complex_linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(c * x).|| = |.c.| * ||.x.|| )
let c be Complex; :: thesis: ( ( ||.x.|| = 0 implies x = 0. Complex_linfty_Space ) & ( x = 0. Complex_linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(c * x).|| = |.c.| * ||.x.|| )

A1: now

assume A2: ||.x.|| = 0 ; :: thesis: x = 0. Complex_linfty_Space
A3: ||.x.|| = sup (rng |.(seq_id x).|) by Th3;
seq_id x is bounded by Th3;
then A4: for n being Element of NAT holds 0c = (seq_id x) . n by A2, A3, Lm11;
x in the_set_of_ComplexSequences by Def1;
hence x = 0. Complex_linfty_Space by A4, Th3, CSSPACE:def 6; :: thesis: verum

end;

A5: now

assume x = 0. Complex_linfty_Space ; :: thesis: ||.x.|| = 0
then A6: for n being Element of NAT holds (seq_id x) . n = 0c by Th3, CSSPACE:def 6;
thus ||.x.|| = sup (rng |.(seq_id x).|) by Th3
.= 0 by A6, Lm8 ; :: thesis: verum

end;

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

proof

A9: |.(seq_id x).| is bounded by A7, Lm9;
|.(seq_id x).| . 1 = |.((seq_id x) . 1).| by VALUED_1:18;
then 0 <= |.(seq_id x).| . 1 by COMPLEX1:132;
hence 0 <= sup (rng |.(seq_id x).|) by A9, Lm2; :: thesis: verum

end;

A10: ||.y.|| = sup (rng |.(seq_id y).|) by Th3;
A11: sup (rng |.(seq_id (x + y)).|) = ||.(x + y).|| by Th3;
A12: for n being Element of NAT holds |.(seq_id (x + y)).| . n = |.(((seq_id x) . n) + ((seq_id y) . n)).|

proof

let n be Element of NAT ; :: thesis: |.(seq_id (x + y)).| . n = |.(((seq_id x) . n) + ((seq_id y) . n)).|
|.(seq_id (x + y)).| . n = |.(seq_id ((seq_id x) + (seq_id y))).| . n by Th3
.= |.((seq_id x) + (seq_id y)).| . n by CSSPACE:3
.= |.(((seq_id x) + (seq_id y)) . n).| by VALUED_1:18
.= |.(((seq_id x) . n) + ((seq_id y) . n)).| by VALUED_1:1 ;
hence |.(seq_id (x + y)).| . n = |.(((seq_id x) . n) + ((seq_id y) . n)).| ; :: thesis: verum

end;

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

proof

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

end;

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

proof

let n be Element of NAT ; :: thesis: |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n
(|.(seq_id x).| . n) + (|.(seq_id y).| . n) = (|.(seq_id x).| + |.(seq_id y).|) . n by SEQ_1:11;
hence |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n by A13; :: thesis: verum

end;

seq_id x is bounded by Def1;
then A15: |.(seq_id x).| is bounded by Lm9;
seq_id y is bounded by Def1;
then A16: |.(seq_id y).| is bounded by Lm9;
A17: upper_bound (rng |.(seq_id (x + y)).|) <= (upper_bound (rng |.(seq_id x).|)) + (upper_bound (rng |.(seq_id y).|))

proof

now

let n be Element of NAT ; :: thesis: |.(seq_id (x + y)).| . n <= (upper_bound (rng |.(seq_id x).|)) + (upper_bound (rng |.(seq_id y).|))
A18: |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n by A14;
A19: (|.(seq_id x).| + |.(seq_id y).|) . n = (|.(seq_id x).| . n) + (|.(seq_id y).| . n) by SEQ_1:11;
A20: |.(seq_id x).| . n <= sup (rng |.(seq_id x).|) by A15, Lm2;
|.(seq_id y).| . n <= sup (rng |.(seq_id y).|) by A16, Lm2;
then (|.(seq_id x).| + |.(seq_id y).|) . n <= (upper_bound (rng |.(seq_id x).|)) + (upper_bound (rng |.(seq_id y).|)) by A19, A20, XREAL_1:9;
hence |.(seq_id (x + y)).| . n <= (upper_bound (rng |.(seq_id x).|)) + (upper_bound (rng |.(seq_id y).|)) by A18, XXREAL_0:2; :: thesis: verum

end;

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

end;

A21: for n being Element of NAT holds |.(c (#) (seq_id x)).| . n = |.c.| * (|.(seq_id x).| . n)

proof

let n be Element of NAT ; :: thesis: |.(c (#) (seq_id x)).| . n = |.c.| * (|.(seq_id x).| . n)
|.(c (#) (seq_id x)).| . n = |.((c (#) (seq_id x)) . n).| by VALUED_1:18
.= |.(c * ((seq_id x) . n)).| by VALUED_1:6
.= |.c.| * |.((seq_id x) . n).| by COMPLEX1:151
.= |.c.| * (|.(seq_id x).| . n) by VALUED_1:18 ;
hence |.(c (#) (seq_id x)).| . n = |.c.| * (|.(seq_id x).| . n) ; :: thesis: verum

end;

seq_id x is bounded by Def1;
then |.(seq_id x).| is bounded by Lm9;
then rng |.(seq_id x).| is bounded by PSCOMP_1:7;
then A22: rng |.(seq_id x).| is bounded_above by XXREAL_2:def 11;
||.(c * x).|| = sup (rng |.(seq_id (c * x)).|) by Th3
.= sup (rng |.(seq_id (c (#) (seq_id x))).|) by Th3
.= sup (rng |.(c (#) (seq_id x)).|) by CSSPACE:3
.= sup (rng (|.c.| (#) |.(seq_id x).|)) by A21, SEQ_1:13
.= sup (|.c.| ** (rng |.(seq_id x).|)) by INTEGRA2:17
.= |.c.| * (sup (rng |.(seq_id x).|)) by A22, COMPLEX1:132, INTEGRA2:13
.= |.c.| * ||.x.|| by Th3 ;
hence ( ( ||.x.|| = 0 implies x = 0. Complex_linfty_Space ) & ( x = 0. Complex_linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(c * x).|| = |.c.| * ||.x.|| ) by A1, A5, A8, A10, A11, A17, Th3; :: thesis: verum