let X be non empty set ; :: thesis:
let Y be ComplexNormSpace; :: thesis:
let f, g be Point of (C_NormSpace_of_BoundedFunctions X,Y); :: thesis:
let c be Complex; :: thesis:

A1: now

assume A2: ||.f.|| = 0 ; :: thesis:
reconsider g = f as bounded Function of X,the carrier of Y by Def5;
set z = X --> (0. Y);
reconsider z = X --> (0. Y) as Function of X,the carrier of Y ;

now

let t be Element of X; :: thesis:
||.(g . t).|| <= ||.f.|| by Th20;
then ||.(g . t).|| = 0 by A2, CLVECT_1:106;
hence g . t = 0. Y by CLVECT_1:def 11
.= z . t by FUNCOP_1:13 ;
:: thesis:

end;

then g = z by FUNCT_2:113;
hence f = 0. (C_NormSpace_of_BoundedFunctions X,Y) by Th19; :: thesis:

end;

A3: now

assume A4: f = 0. (C_NormSpace_of_BoundedFunctions X,Y) ; :: thesis:
thus ||.f.|| = 0 :: thesis:

proof

set z = X --> (0. Y);
reconsider z = X --> (0. Y) as Function of X,the carrier of Y ;
reconsider g = f as bounded Function of X,the carrier of Y by Def5;
A5: z = g by A4, Th19;

A6: now

let r be Real; :: thesis:
assume A7: r in PreNorms g ; :: thesis:
consider t being Element of X such that
A8: r = ||.(g . t).|| by A7;
||.(g . t).|| = ||.(0. Y).|| by A5, FUNCOP_1:13
.= 0 by CLVECT_1:def 11 ;
hence ( 0 <= r & r <= 0 ) by A8; :: thesis:

end;

A9: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th14;
consider r0 being set such that
A10: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 = r0 as Real by A10;
A11: 0 <= r0 by A6, A10;
( ( for s being real number st s in PreNorms g holds
s <= 0 ) implies sup (PreNorms g) <= 0 ) by SEQ_4:62;
then sup (PreNorms g) = 0 by A6, A9, A10, A11, SEQ_4:def 4;
then (ComplexBoundedFunctionsNorm X,Y) . f = 0 by Th18;
hence ||.f.|| = 0 by CLVECT_1:def 10; :: thesis:

end;

A12: ||.(c * f).|| = |.c.| * ||.f.||

proof

reconsider f1 = f, h1 = c * f as bounded Function of X,the carrier of Y by Def5;

A13: now

let t be Element of X; :: thesis:
A14: ||.(h1 . t).|| = ||.(c * (f1 . t)).|| by Th24;
A15: ||.(c * (f1 . t)).|| = |.c.| * ||.(f1 . t).|| by CLVECT_1:def 11;
0 <= |.c.| by COMPLEX1:132;
hence ||.(h1 . t).|| <= |.c.| * ||.f.|| by A14, A15, Th20, XREAL_1:66; :: thesis:

end;

A16: now

let r be Real; :: thesis:
assume A17: r in PreNorms h1 ; :: thesis:
consider t being Element of X such that
A18: r = ||.(h1 . t).|| by A17;
thus r <= |.c.| * ||.f.|| by A13, A18; :: thesis:

end;

A19: ( ( for s being real number st s in PreNorms h1 holds
s <= |.c.| * ||.f.|| ) implies sup (PreNorms h1) <= |.c.| * ||.f.|| ) by SEQ_4:62;
(ComplexBoundedFunctionsNorm X,Y) . (c * f) = sup (PreNorms h1) by Th18;
then A20: ||.(c * f).|| <= |.c.| * ||.f.|| by A16, A19, CLVECT_1:def 10;

now

per cases ;

case A21: c <> 0c ; :: thesis:

A22: now

let t be Element of X; :: thesis:
h1 . t = c * (f1 . t) by Th24;
then A23: (c " ) * (h1 . t) = ((c " ) * c) * (f1 . t) by CLVECT_1:def 2
.= 1r * (f1 . t) by A21, COMPLEX1:def 7, XCMPLX_0:def 7
.= f1 . t by CLVECT_1:def 2 ;
A24: ||.((c " ) * (h1 . t)).|| = |.(c " ).| * ||.(h1 . t).|| by CLVECT_1:def 11;
A25: 0 <= |.(c " ).| by COMPLEX1:132;
|.(c " ).| = |.(1r / c).| by COMPLEX1:def 7, XCMPLX_1:217
.= 1 / |.c.| by COMPLEX1:134, COMPLEX1:153
.= 1 * (|.c.| " ) by XCMPLX_0:def 9
.= |.c.| " ;
hence ||.(f1 . t).|| <= (|.c.| " ) * ||.(c * f).|| by A23, A24, A25, Th20, XREAL_1:66; :: thesis:

end;

A26: now

let r be Real; :: thesis:
assume A27: r in PreNorms f1 ; :: thesis:
consider t being Element of X such that
A28: r = ||.(f1 . t).|| by A27;
thus r <= (|.c.| " ) * ||.(c * f).|| by A22, A28; :: thesis:

end;

A29: |.c.| <> 0 by A21, COMPLEX1:133;
A30: ( ( for s being real number st s in PreNorms f1 holds
s <= (|.c.| " ) * ||.(c * f).|| ) implies sup (PreNorms f1) <= (|.c.| " ) * ||.(c * f).|| ) by SEQ_4:62;
(ComplexBoundedFunctionsNorm X,Y) . f = sup (PreNorms f1) by Th18;
then A31: ||.f.|| <= (|.c.| " ) * ||.(c * f).|| by A26, A30, CLVECT_1:def 10;
0 <= |.c.| by COMPLEX1:132;
then |.c.| * ||.f.|| <= |.c.| * ((|.c.| " ) * ||.(c * f).||) by A31, XREAL_1:66;
then |.c.| * ||.f.|| <= (|.c.| * (|.c.| " )) * ||.(c * f).|| ;
then |.c.| * ||.f.|| <= 1 * ||.(c * f).|| by A29, XCMPLX_0:def 7;
hence |.c.| * ||.f.|| <= ||.(c * f).|| ; :: thesis:

end;

case A32: c = 0c ; :: thesis:

reconsider fz = f as VECTOR of (C_VectorSpace_of_BoundedFunctions X,Y) ;
c * f = (Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) . [c,f] by CLVECT_1:def 1
.= c * fz by CLVECT_1:def 1
.= 0. (C_VectorSpace_of_BoundedFunctions X,Y) by A32, CLVECT_1:2
.= 0. (C_NormSpace_of_BoundedFunctions X,Y) ;
hence ||.(c * f).|| = |.c.| * ||.f.|| by A32, Th22, COMPLEX1:130; :: thesis:

end;

hence ||.(c * f).|| = |.c.| * ||.f.|| by A20, XXREAL_0:1; :: thesis:

end;

||.(f + g).|| <= ||.f.|| + ||.g.||

proof

reconsider f1 = f, g1 = g, h1 = f + g as bounded Function of X,the carrier of Y by Def5;

A33: now

let t be Element of X; :: thesis:
A34: ||.(h1 . t).|| = ||.((f1 . t) + (g1 . t)).|| by Th23;
A35: ||.((f1 . t) + (g1 . t)).|| <= ||.(f1 . t).|| + ||.(g1 . t).|| by CLVECT_1:def 11;
A36: ||.(f1 . t).|| <= ||.f.|| by Th20;
||.(g1 . t).|| <= ||.g.|| by Th20;
then ||.(f1 . t).|| + ||.(g1 . t).|| <= ||.f.|| + ||.g.|| by A36, XREAL_1:9;
hence ||.(h1 . t).|| <= ||.f.|| + ||.g.|| by A34, A35, XXREAL_0:2; :: thesis:

end;

A37: now

let r be Real; :: thesis:
assume A38: r in PreNorms h1 ; :: thesis:
consider t being Element of X such that
A39: r = ||.(h1 . t).|| by A38;
thus r <= ||.f.|| + ||.g.|| by A33, A39; :: thesis:

end;

A40: ( ( for s being real number st s in PreNorms h1 holds
s <= ||.f.|| + ||.g.|| ) implies sup (PreNorms h1) <= ||.f.|| + ||.g.|| ) by SEQ_4:62;
(ComplexBoundedFunctionsNorm X,Y) . (f + g) = sup (PreNorms h1) by Th18;
hence ||.(f + g).|| <= ||.f.|| + ||.g.|| by A37, A40, CLVECT_1:def 10; :: thesis:

end;

hence ( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions X,Y) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions X,Y) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| ) by A1, A3, A12; :: thesis: