let X be non empty set ; :: thesis: X --> 0 = 0. (C_Normed_Algebra_of_BoundedFunctions X)

X --> 0 = 0. (C_Algebra_of_BoundedFunctions X) by Th8;

hence X --> 0 = 0. (C_Normed_Algebra_of_BoundedFunctions X) ; :: thesis: verum

X --> 0 = 0. (C_Algebra_of_BoundedFunctions X) by Th8;

hence X --> 0 = 0. (C_Normed_Algebra_of_BoundedFunctions X) ; :: thesis: verum