let X be non empty set ; :: thesis: 0. (R_Algebra_of_BoundedFunctions X) = X --> 0
A1: R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th03;
0. (RAlgebra X) = X --> 0 ;
hence 0. (R_Algebra_of_BoundedFunctions X) = X --> 0 by A1, RLSUB121; :: thesis: verum