reconsider e = One_ ((ContinuousFunctions X),(RAlgebra the carrier of X)) as Element of (R_Normed_Algebra_of_ContinuousFunctions X) ;
take e ; :: according to GROUP_1:def 1 :: thesis: for b₁ being Element of the carrier of (R_Normed_Algebra_of_ContinuousFunctions X) holds
( b₁ * e = b₁ & e * b₁ = b₁ )
thus for b₁ being Element of the carrier of (R_Normed_Algebra_of_ContinuousFunctions X) holds
( b₁ * e = b₁ & e * b₁ = b₁ ) by Lm2; :: thesis: verum