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