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

A1: C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;

0. (CAlgebra X) = X --> 0 ;

hence 0. (C_Algebra_of_BoundedFunctions X) = X --> 0 by A1, Th3; :: thesis: verum

A1: C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;

0. (CAlgebra X) = X --> 0 ;

hence 0. (C_Algebra_of_BoundedFunctions X) = X --> 0 by A1, Th3; :: thesis: verum