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