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

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