let X be non empty set ; :: thesis: for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st F = 0. (R_Normed_Algebra_of_BoundedFunctions X) holds
0 = ||.F.||
let F be Point of (R_Normed_Algebra_of_BoundedFunctions X); :: thesis: ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies 0 = ||.F.|| )
assume A1: F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ; :: thesis: 0 = ||.F.||
set z = X --> 0 ;
reconsider z = X --> 0 as Function of X,REAL by FUNCOP_1:58;
F in BoundedFunctions X ;
then consider g being Function of X,REAL such that
A0: ( g = F & g | X is bounded ) ;

A3: now

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
A5: r = abs (g . t) ;
z = g by A1, A0, ThB18;
then abs (g . t) = abs 0 by FUNCOP_1:13;
hence ( 0 <= r & r <= 0 ) by A5, ABSVALUE:7; :: thesis: verum

end;

A6: ( not PreNorms g is empty & PreNorms g is bounded_above ) by A0, ThB13;
consider r0 being set such that
A7: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 = r0 as Real by A7;
A8: ( 0 <= r0 & r0 <= 0 ) by A3, A7;
( ( 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 A3, A6, A7, A8, SEQ_4:def 4;
hence 0 = ||.F.|| by A0, ThB17; :: thesis: verum