let X be non empty set ; :: thesis: 1_ (C_Algebra_of_BoundedFunctions X) = X --> 1r
A1: C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;
1_ (CAlgebra X) = X --> 1r ;
hence 1_ (C_Algebra_of_BoundedFunctions X) = X --> 1r by A1, Th3; :: thesis: verum