let X be non empty set ; :: thesis: for a being Complex

for F, G being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds

( ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

let a be Complex; :: thesis: for F, G being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds

( ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

let F, G be Point of (C_Normed_Algebra_of_BoundedFunctions X); :: thesis: ( ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

for F, G being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds

( ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

let a be Complex; :: thesis: for F, G being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds

( ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

let F, G be Point of (C_Normed_Algebra_of_BoundedFunctions X); :: thesis: ( ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

A1: now :: thesis: ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 )

A10:
||.(F + G).|| <= ||.F.|| + ||.G.||
set z = X --> 0c;

reconsider z = X --> 0c as Function of X,COMPLEX ;

F in ComplexBoundedFunctions X ;

then consider g being Function of X,COMPLEX such that

A2: F = g and

A3: g | X is bounded ;

A4: ( not PreNorms g is empty & PreNorms g is bounded_above ) by A3, Th11;

consider r0 being object such that

A5: r0 in PreNorms g by XBOOLE_0:def 1;

reconsider r0 = r0 as Real by A5;

A6: ( ( for s being Real st s in PreNorms g holds

s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:45;

assume F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ; :: thesis: ||.F.|| = 0

then A7: z = g by A2, Th18;

then upper_bound (PreNorms g) = 0 by A8, A4, A6, A5, SEQ_4:def 1;

hence ||.F.|| = 0 by A2, A3, Th13; :: thesis: verum

end;reconsider z = X --> 0c as Function of X,COMPLEX ;

F in ComplexBoundedFunctions X ;

then consider g being Function of X,COMPLEX such that

A2: F = g and

A3: g | X is bounded ;

A4: ( not PreNorms g is empty & PreNorms g is bounded_above ) by A3, Th11;

consider r0 being object such that

A5: r0 in PreNorms g by XBOOLE_0:def 1;

reconsider r0 = r0 as Real by A5;

A6: ( ( for s being Real st s in PreNorms g holds

s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:45;

assume F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ; :: thesis: ||.F.|| = 0

then A7: z = g by A2, Th18;

A8: now :: thesis: for r being Real st r in PreNorms g holds

( 0 <= r & r <= 0 )

then
0 <= r0
by A5;( 0 <= r & r <= 0 )

let r be Real; :: thesis: ( r in PreNorms g implies ( 0 <= r & r <= 0 ) )

assume r in PreNorms g ; :: thesis: ( 0 <= r & r <= 0 )

then consider t being Element of X such that

A9: r = |.(g . t).| ;

|.(g . t).| = |.0.| by A7

.= 0 ;

hence ( 0 <= r & r <= 0 ) by A9; :: thesis: verum

end;assume r in PreNorms g ; :: thesis: ( 0 <= r & r <= 0 )

then consider t being Element of X such that

A9: r = |.(g . t).| ;

|.(g . t).| = |.0.| by A7

.= 0 ;

hence ( 0 <= r & r <= 0 ) by A9; :: thesis: verum

then upper_bound (PreNorms g) = 0 by A8, A4, A6, A5, SEQ_4:def 1;

hence ||.F.|| = 0 by A2, A3, Th13; :: thesis: verum

proof

A20:
||.(a * F).|| = |.a.| * ||.F.||
F + G in ComplexBoundedFunctions X
;

then consider h1 being Function of X,COMPLEX such that

A11: h1 = F + G and

A12: h1 | X is bounded ;

G in ComplexBoundedFunctions X ;

then consider g1 being Function of X,COMPLEX such that

A13: g1 = G and

A14: g1 | X is bounded ;

F in ComplexBoundedFunctions X ;

then consider f1 being Function of X,COMPLEX such that

A15: f1 = F and

A16: f1 | X is bounded ;

s <= ||.F.|| + ||.G.|| ) implies upper_bound (PreNorms h1) <= ||.F.|| + ||.G.|| ) by SEQ_4:45;

hence ||.(F + G).|| <= ||.F.|| + ||.G.|| by A11, A12, A19, Th13; :: thesis: verum

end;then consider h1 being Function of X,COMPLEX such that

A11: h1 = F + G and

A12: h1 | X is bounded ;

G in ComplexBoundedFunctions X ;

then consider g1 being Function of X,COMPLEX such that

A13: g1 = G and

A14: g1 | X is bounded ;

F in ComplexBoundedFunctions X ;

then consider f1 being Function of X,COMPLEX such that

A15: f1 = F and

A16: f1 | X is bounded ;

A17: now :: thesis: for t being Element of X holds |.(h1 . t).| <= ||.F.|| + ||.G.||

let t be Element of X; :: thesis: |.(h1 . t).| <= ||.F.|| + ||.G.||

( |.(f1 . t).| <= ||.F.|| & |.(g1 . t).| <= ||.G.|| ) by A15, A16, A13, A14, Th19;

then A18: |.(f1 . t).| + |.(g1 . t).| <= ||.F.|| + ||.G.|| by XREAL_1:7;

( |.(h1 . t).| = |.((f1 . t) + (g1 . t)).| & |.((f1 . t) + (g1 . t)).| <= |.(f1 . t).| + |.(g1 . t).| ) by A15, A13, A11, Th22, COMPLEX1:56;

hence |.(h1 . t).| <= ||.F.|| + ||.G.|| by A18, XXREAL_0:2; :: thesis: verum

end;( |.(f1 . t).| <= ||.F.|| & |.(g1 . t).| <= ||.G.|| ) by A15, A16, A13, A14, Th19;

then A18: |.(f1 . t).| + |.(g1 . t).| <= ||.F.|| + ||.G.|| by XREAL_1:7;

( |.(h1 . t).| = |.((f1 . t) + (g1 . t)).| & |.((f1 . t) + (g1 . t)).| <= |.(f1 . t).| + |.(g1 . t).| ) by A15, A13, A11, Th22, COMPLEX1:56;

hence |.(h1 . t).| <= ||.F.|| + ||.G.|| by A18, XXREAL_0:2; :: thesis: verum

A19: now :: thesis: for r being Real st r in PreNorms h1 holds

r <= ||.F.|| + ||.G.||

( ( for s being Real st s in PreNorms h1 holds r <= ||.F.|| + ||.G.||

let r be Real; :: thesis: ( r in PreNorms h1 implies r <= ||.F.|| + ||.G.|| )

assume r in PreNorms h1 ; :: thesis: r <= ||.F.|| + ||.G.||

then ex t being Element of X st r = |.(h1 . t).| ;

hence r <= ||.F.|| + ||.G.|| by A17; :: thesis: verum

end;assume r in PreNorms h1 ; :: thesis: r <= ||.F.|| + ||.G.||

then ex t being Element of X st r = |.(h1 . t).| ;

hence r <= ||.F.|| + ||.G.|| by A17; :: thesis: verum

s <= ||.F.|| + ||.G.|| ) implies upper_bound (PreNorms h1) <= ||.F.|| + ||.G.|| ) by SEQ_4:45;

hence ||.(F + G).|| <= ||.F.|| + ||.G.|| by A11, A12, A19, Th13; :: thesis: verum

proof

F in ComplexBoundedFunctions X
;

then consider f1 being Function of X,COMPLEX such that

A21: f1 = F and

A22: f1 | X is bounded ;

a * F in ComplexBoundedFunctions X ;

then consider h1 being Function of X,COMPLEX such that

A23: h1 = a * F and

A24: h1 | X is bounded ;

s <= |.a.| * ||.F.|| ) implies upper_bound (PreNorms h1) <= |.a.| * ||.F.|| ) by SEQ_4:45;

then A27: ||.(a * F).|| <= |.a.| * ||.F.|| by A23, A24, A26, Th13;

end;then consider f1 being Function of X,COMPLEX such that

A21: f1 = F and

A22: f1 | X is bounded ;

a * F in ComplexBoundedFunctions X ;

then consider h1 being Function of X,COMPLEX such that

A23: h1 = a * F and

A24: h1 | X is bounded ;

A25: now :: thesis: for t being Element of X holds |.(h1 . t).| <= |.a.| * ||.F.||

let t be Element of X; :: thesis: |.(h1 . t).| <= |.a.| * ||.F.||

|.(h1 . t).| = |.(a * (f1 . t)).| by A21, A23, Th23;

then |.(h1 . t).| = |.a.| * |.(f1 . t).| by COMPLEX1:65;

hence |.(h1 . t).| <= |.a.| * ||.F.|| by A21, A22, Th19, XREAL_1:64; :: thesis: verum

end;|.(h1 . t).| = |.(a * (f1 . t)).| by A21, A23, Th23;

then |.(h1 . t).| = |.a.| * |.(f1 . t).| by COMPLEX1:65;

hence |.(h1 . t).| <= |.a.| * ||.F.|| by A21, A22, Th19, XREAL_1:64; :: thesis: verum

A26: now :: thesis: for r being Real st r in PreNorms h1 holds

r <= |.a.| * ||.F.||

( ( for s being Real st s in PreNorms h1 holds r <= |.a.| * ||.F.||

let r be Real; :: thesis: ( r in PreNorms h1 implies r <= |.a.| * ||.F.|| )

assume r in PreNorms h1 ; :: thesis: r <= |.a.| * ||.F.||

then ex t being Element of X st r = |.(h1 . t).| ;

hence r <= |.a.| * ||.F.|| by A25; :: thesis: verum

end;assume r in PreNorms h1 ; :: thesis: r <= |.a.| * ||.F.||

then ex t being Element of X st r = |.(h1 . t).| ;

hence r <= |.a.| * ||.F.|| by A25; :: thesis: verum

s <= |.a.| * ||.F.|| ) implies upper_bound (PreNorms h1) <= |.a.| * ||.F.|| ) by SEQ_4:45;

then A27: ||.(a * F).|| <= |.a.| * ||.F.|| by A23, A24, A26, Th13;

per cases
( a <> 0 or a = 0 )
;

end;

suppose A28:
a <> 0
; :: thesis: ||.(a * F).|| = |.a.| * ||.F.||

s <= (|.a.| ") * ||.(a * F).|| ) implies upper_bound (PreNorms f1) <= (|.a.| ") * ||.(a * F).|| ) by SEQ_4:45;

then ||.F.|| <= (|.a.| ") * ||.(a * F).|| by A21, A22, A32, Th13;

then |.a.| * ||.F.|| <= |.a.| * ((|.a.| ") * ||.(a * F).||) by XREAL_1:64;

then |.a.| * ||.F.|| <= (|.a.| * (|.a.| ")) * ||.(a * F).|| ;

then |.a.| * ||.F.|| <= 1 * ||.(a * F).|| by A28, XCMPLX_0:def 7;

hence ||.(a * F).|| = |.a.| * ||.F.|| by A27, XXREAL_0:1; :: thesis: verum

end;

A29: now :: thesis: for t being Element of X holds |.(f1 . t).| <= (|.a.| ") * ||.(a * F).||

let t be Element of X; :: thesis: |.(f1 . t).| <= (|.a.| ") * ||.(a * F).||

|.(a ").| = |.(1 / a).| ;

then A30: |.(a ").| = 1 / |.a.| by COMPLEX1:80;

h1 . t = a * (f1 . t) by A21, A23, Th23;

then (a ") * (h1 . t) = ((a ") * a) * (f1 . t) ;

then A31: (a ") * (h1 . t) = 1 * (f1 . t) by A28, XCMPLX_0:def 7;

( |.((a ") * (h1 . t)).| = |.(a ").| * |.(h1 . t).| & 0 <= |.(a ").| ) by COMPLEX1:65;

hence |.(f1 . t).| <= (|.a.| ") * ||.(a * F).|| by A23, A24, A31, A30, Th19, XREAL_1:64; :: thesis: verum

end;|.(a ").| = |.(1 / a).| ;

then A30: |.(a ").| = 1 / |.a.| by COMPLEX1:80;

h1 . t = a * (f1 . t) by A21, A23, Th23;

then (a ") * (h1 . t) = ((a ") * a) * (f1 . t) ;

then A31: (a ") * (h1 . t) = 1 * (f1 . t) by A28, XCMPLX_0:def 7;

( |.((a ") * (h1 . t)).| = |.(a ").| * |.(h1 . t).| & 0 <= |.(a ").| ) by COMPLEX1:65;

hence |.(f1 . t).| <= (|.a.| ") * ||.(a * F).|| by A23, A24, A31, A30, Th19, XREAL_1:64; :: thesis: verum

A32: now :: thesis: for r being Real st r in PreNorms f1 holds

r <= (|.a.| ") * ||.(a * F).||

( ( for s being Real st s in PreNorms f1 holds r <= (|.a.| ") * ||.(a * F).||

let r be Real; :: thesis: ( r in PreNorms f1 implies r <= (|.a.| ") * ||.(a * F).|| )

assume r in PreNorms f1 ; :: thesis: r <= (|.a.| ") * ||.(a * F).||

then ex t being Element of X st r = |.(f1 . t).| ;

hence r <= (|.a.| ") * ||.(a * F).|| by A29; :: thesis: verum

end;assume r in PreNorms f1 ; :: thesis: r <= (|.a.| ") * ||.(a * F).||

then ex t being Element of X st r = |.(f1 . t).| ;

hence r <= (|.a.| ") * ||.(a * F).|| by A29; :: thesis: verum

s <= (|.a.| ") * ||.(a * F).|| ) implies upper_bound (PreNorms f1) <= (|.a.| ") * ||.(a * F).|| ) by SEQ_4:45;

then ||.F.|| <= (|.a.| ") * ||.(a * F).|| by A21, A22, A32, Th13;

then |.a.| * ||.F.|| <= |.a.| * ((|.a.| ") * ||.(a * F).||) by XREAL_1:64;

then |.a.| * ||.F.|| <= (|.a.| * (|.a.| ")) * ||.(a * F).|| ;

then |.a.| * ||.F.|| <= 1 * ||.(a * F).|| by A28, XCMPLX_0:def 7;

hence ||.(a * F).|| = |.a.| * ||.F.|| by A27, XXREAL_0:1; :: thesis: verum

suppose A33:
a = 0
; :: thesis: ||.(a * F).|| = |.a.| * ||.F.||

reconsider fz = F as VECTOR of (C_Algebra_of_BoundedFunctions X) ;

a * fz = (a + a) * fz by A33

.= (a * fz) + (a * fz) by CLVECT_1:def 3 ;

then 0. (C_Algebra_of_BoundedFunctions X) = (- (a * fz)) + ((a * fz) + (a * fz)) by VECTSP_1:16;

then 0. (C_Algebra_of_BoundedFunctions X) = ((- (a * fz)) + (a * fz)) + (a * fz) by RLVECT_1:def 3;

then 0. (C_Algebra_of_BoundedFunctions X) = (0. (C_Algebra_of_BoundedFunctions X)) + (a * fz) by VECTSP_1:16;

then A34: a * F = 0. (C_Normed_Algebra_of_BoundedFunctions X) by RLVECT_1:4;

|.a.| * ||.F.|| = 0 * ||.F.|| by A33;

hence ||.(a * F).|| = |.a.| * ||.F.|| by A34, Th21; :: thesis: verum

end;a * fz = (a + a) * fz by A33

.= (a * fz) + (a * fz) by CLVECT_1:def 3 ;

then 0. (C_Algebra_of_BoundedFunctions X) = (- (a * fz)) + ((a * fz) + (a * fz)) by VECTSP_1:16;

then 0. (C_Algebra_of_BoundedFunctions X) = ((- (a * fz)) + (a * fz)) + (a * fz) by RLVECT_1:def 3;

then 0. (C_Algebra_of_BoundedFunctions X) = (0. (C_Algebra_of_BoundedFunctions X)) + (a * fz) by VECTSP_1:16;

then A34: a * F = 0. (C_Normed_Algebra_of_BoundedFunctions X) by RLVECT_1:4;

|.a.| * ||.F.|| = 0 * ||.F.|| by A33;

hence ||.(a * F).|| = |.a.| * ||.F.|| by A34, Th21; :: thesis: verum

now :: thesis: ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) )

hence
( ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
by A1, A20, A10; :: thesis: verumset z = X --> 0c;

reconsider z = X --> 0c as Function of X,COMPLEX ;

F in ComplexBoundedFunctions X ;

then consider g being Function of X,COMPLEX such that

A35: F = g and

A36: g | X is bounded ;

assume A37: ||.F.|| = 0 ; :: thesis: F = 0. (C_Normed_Algebra_of_BoundedFunctions X)

hence F = 0. (C_Normed_Algebra_of_BoundedFunctions X) by A35, Th18; :: thesis: verum

end;reconsider z = X --> 0c as Function of X,COMPLEX ;

F in ComplexBoundedFunctions X ;

then consider g being Function of X,COMPLEX such that

A35: F = g and

A36: g | X is bounded ;

assume A37: ||.F.|| = 0 ; :: thesis: F = 0. (C_Normed_Algebra_of_BoundedFunctions X)

now :: thesis: for t being Element of X holds g . t = z . t

then
g = z
by FUNCT_2:63;let t be Element of X; :: thesis: g . t = z . t

|.(g . t).| = 0 by A35, A36, A37, Th19;

hence g . t = 0

.= z . t ;

:: thesis: verum

end;|.(g . t).| = 0 by A35, A36, A37, Th19;

hence g . t = 0

.= z . t ;

:: thesis: verum

hence F = 0. (C_Normed_Algebra_of_BoundedFunctions X) by A35, Th18; :: thesis: verum