let X be non empty set ; :: thesis: 1_ (R_Algebra_of_BoundedFunctions X) = X --> 1
( R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X & 1_ (RAlgebra X) = X --> 1 ) by Th6;
hence 1_ (R_Algebra_of_BoundedFunctions X) = X --> 1 by Th8; :: thesis: verum