@MISC{DUALSP04.MIZ,
  AUTHOR = {Narita, Keiko and Endou, Noboru and Shidama, Yasunari},
  TITLE = {The Orthogonal Projection and {R}iesz Representation Theorem},
  ACKNOWLEDGEMENT = {This work was supported by JSPS KAKENHI 22300285 and 23500029.},
  SECTION1 = {Preliminaries},
  SECTION2 = {The Orthogonal Projection},
  SECTION3 = {Riesz Representation Theorem},
  DAY = {1},
  MONTH = {July},
  YEAR = {2015},
  ADDRESS1 = {Hirosaki-city\\ Aomori, Japan},
  ADDRESS2 = {Gifu National College of Technology\\ Gifu, Japan},
  ADDRESS3 = {Shinshu University\\ Nagano, Japan},
  SUMMARY = {In this article, the orthogonal projection and Riesz representation theorem are mainly formalized.
  In the first section, we defined the norm of elements on real Hilbert spaces, and defined
  Mizar functor \verb!RUSp2RNSp!, real normed spaces as real Hilbert spaces. By this definition,
  we regarded sequences of real
  Hilbert spaces as sequences of real normed spaces, and proved some properties about real Hilbert spaces.
  Furthermore, we defined continuity and Lipschitz continuity of functionals on real Hilbert spaces.
  Referring the article \cite{DUALSP01.ABS}, we also defined some definitions on real Hilbert spaces
  and proved some theorems for defining dual spaces of real Hilbert spaces. About properties of all
  definitions, we proved that they are equivalent properties of functionals on real normed spaces.
  In Sec. 2, by the definitions \cite{RUSUB_5.ABS}, we showed properties of orthogonal complement.
  And using theorems of Sec. 1, we proved some lemmas. Then we proved theorems, orthogonal decomposition
  about elements of real Hilbert spaces. They are the last two theorems, existence and uniqueness.
  In the third and final section, we defined the kernel of linear functionals on real Hilbert spaces.
  We used this definition and theorems of the former sections for the proof.
  By the last three theorems, we showed Riesz representation theorem, existence, uniqueness,
  and about the norm of bounded linear functionals on real Hilbert spaces.}}
