Banach Algebra of Bounded Complex-Valued Functionals Katuhiko Kanazashi, Hiroyuki Okazaki, Yasunari Shidama (2011) Formalized Mathematics In this article, we describe some basic properties of the Banach algebra which is constructed from all bounded complex-valued functionals.