reconsider e = FuncUnit X as Element of (R_Algebra_of_BoundedLinearOperators X) ;

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

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

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

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

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

( b

thus for b

( b