Banach Algebra of Continuous Functionals and the Space of Real-Valued Continuous Functionals with Bounded Support. - Katuhiko Kanazashi; Noboru Endou; Yasunari Shidama (Formaliz. Math., 2010)

Banach Algebra of Bounded Complex-Valued Functionals. - Katuhiko Kanazashi; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2011)

Functional Space C(ω), C0(ω). - Katuhiko Kanazashi; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2012)

The Ck Space. - Katuhiko Kanazashi; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2013)