@MISC{ORDINAL7.MIZ,
  AUTHOR = {Koch, Sebastian},
  NOTE1 = {The author is enrolled in the Johannes Gutenberg University in Mayence, Germany},
  TITLE = {Natural Addition of Ordinals},
  SECTION1 = {Preliminaries},
  SECTION2 = {About the Cantor Normal Form},
  SECTION3 = {Natural Addition of Ordinals},
  DAY = {27},
  MONTH = {May},
  YEAR = {2019},
  ADDRESS1 = {Germany\\\href{mailto:skoch02@students.uni-mainz.de}{skoch02@students.uni-mainz.de}},
  SUMMARY = {In \cite{ORDINAL5.ABS} the existence of the Cantor normal form of ordinals was proven 
  in Mizar \cite{FourDecades}. In this article, its uniqueness is proven. The basic proof idea 
  is well known (cf. \cite{Cantor,Abian,Bachmann,Sierpinski,Deiser}). In this variant the additional 
  closure of ordinals is used, which is also proven in this article using lemmas from 
  \cite{ORDINAL5.ABS}. The absorption law of ordinal addition is proven here, too.\par
  The natural sum or Heisenberg sum (cf. \cite{Bachmann,Deiser}) of two ordinals 
  $\alpha$, $\beta$, denoted by $\alpha\oplus\beta$, is formalized using the Cantor normal 
  form. The concept of bags, as used to formalize polynomials in Mizar 
  (cf. \cite{PRE_POLY.ABS, POLYNOM1.ABS}), couldn't easily be applied in this case 
  since there is no set of all ordinals, so it wasn't used here. The chosen definition 
  of the natural sum turned out to be slightly sophisticated, leading to a rather 
  long proof of its monotonicity property, while the proofs of the other shown 
  properties are straightforward.}}

@book{Sierpinski,
  title = {Cardinal and ordinal numbers},
  series = {Polska Akademia Nauk. Monografie matematyczne ; 34},
  author = {Sierpi´nski, Waclaw},
  address = {Warszawa},
  publisher = {[PWN]},
  year = {1965},
  edition = {2. ed., rev},
  pages = {491 S.}
}
@book{Bachmann,
  title = {Transfinite Zahlen},
  series = {Ergebnisse der Mathematik und ihrer Grenzgebiete ; 1},
  author = {Bachmann, Heinz},
  address = {Berlin [u.a.]},
  publisher = {Springer},
  year = {1967},
  edition = {2., neubearb. Aufl.},
  pages = {VIII, 228 S.}
}
@article{Cantor,
  title={Beitr{\"a}ge zur Begr{\"u}ndung der transfiniten Mengenlehre},
  author={Cantor, Georg},
  journal={Mathematische Annalen},
  volume={49},
  number={2},
  pages={207--246},
  year={1897},
  publisher={Springer}
}
@book{Abian,
  title = {The theory of sets and transfinite arithmetic},
  series = {Saunders mathematics books},
  author = {Abian, Alexander},
  address = {Philadelphia [u.a.]},
  publisher = {Saunders},
  year = {1965},
  pages = {406 S.}
}
@book{Deiser,
  title = {Einführung in die Mengenlehre : die Mengenlehre Georg Cantors und ihre Axiomatisierung durch Ernst Zermelo},
  author = {Deiser, Oliver},
  address = {Berlin [u.a.]},
  publisher = {Springer},
  year = {2004},
  edition = {2., verb. und erw. Aufl.},
  ISBN = {3-540-20401-6},
  pages = {551 S.}
}
@Article{FourDecades,
  author={Grabowski, Adam and Korni{\l}owicz, Artur and Naumowicz, Adam},
  title={Four Decades of {M}izar},
  journal={Journal of Automated Reasoning},
  year={2015},
  volume={55},
  number={3},
  pages={191--198},
  issn={1573-0670},
  doi={10.1007/s10817-015-9345-1}
}