reconsider e = One_ ((ComplexBoundedFunctions X),(CAlgebra X)) as Element of (C_Normed_Algebra_of_BoundedFunctions X) ;

take e ; :: according to GROUP_1:def 1 :: thesis: for b_{1} being Element of the carrier of (C_Normed_Algebra_of_BoundedFunctions X) holds

( b_{1} * e = b_{1} & e * b_{1} = b_{1} )

thus for b_{1} being Element of the carrier of (C_Normed_Algebra_of_BoundedFunctions X) holds

( b_{1} * e = b_{1} & e * b_{1} = b_{1} )
by Lm3; :: thesis: verum

take e ; :: according to GROUP_1:def 1 :: thesis: for b

( b

thus for b

( b