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