[mizar] New Mizar articles - FM12(2)

[Adam Grabowski <adam@math.uwb.edu.pl>]

Dear All,

due to the long delay in the regeneration process
of the Journal of Formalized Mathematics we attach
the list of Mizar articles which were submitted to
the Mizar Mathematical Library since our last posting
to the Mizar Forum mailing list.

All files were verified by the Mizar system
and accepted for inclusion in the MML.

The following articles form
the contents of Formalized Mathematics, 12(2), 2004:

1. Yasumasa Suzuki,
   Banach Space of Bounded Real Sequences,
   pp. 77--83,
   MML Id: RSSPACE4

2. Yuzhong Ding and Xiquan Liang,
   Solving Roots of Polynomial Equation of Degree 2
     and 3 with Complex Coefficients,
   pp. 85--92,
   MML Id: POLYEQ_3

3. Noboru Endou,
   Complex Linear Space and Complex Normed Space,
   pp. 93--102,
   MML Id: CLVECT_1

4. Yasunari Shidama,
   The Banach Algebra of Bounded Linear Operators,
   pp. 103--108,
   MML Id: LOPBAN_2

5. Noboru Endou,
   Complex Linear Space of Complex Sequences,
   pp. 109--117,
   MML Id: CSSPACE

6. Yatsuka Nakamura,
   Behaviour of an Arc Crossing a Line,
   pp. 119--124,
   MML Id: JORDAN20

7. Masami Tanaka and Yatsuka Nakamura,
   Some Set Series in Finite Topological Spaces.
     Fundamental Concepts for Image Processing,
   pp. 125--129,
   MML Id: FINTOPO3

8. Yasunari Shidama,
   The Series on Banach Algebra,
   pp. 131--138,
   MML Id: LOPBAN_3

9. Pacharapokin Chanapat, Kanchun, and Hiroshi Yamazaki,
   Formulas and Identities of Trigonometric Functions,
   pp. 139--141,
   MML Id: SIN_COS4

10.Krzysztof Retel,
   The Class of Series-Parallel Graphs. Part III,
   pp. 143--149,
   MML Id: NECKLA_3

11.Artur Korni{\l}owicz and Yasunari Shidama,
   Relocability for SCM over Ring,
   pp. 151--157,
   MML Id: SCMRING4

12.Noboru Endou,
   Convergent Sequences in Complex Unitary Space,
   pp. 159--165,
   MML Id: CLVECT_2

13.Artur Korni{\l}owicz,
   Recursive Definitions. Part II,
   pp. 167--172,
   MML Id: RECDEF_2

14.Yasunari Shidama,
   The Exponential Function on Banach Algebra,
   pp. 173--177,
   MML Id: LOPBAN_4

15.Artur Korni{\l}owicz and Piotr Rudnicki,
   Fundamental Theorem of Arithmetic,
   pp. 179--186,
   MML Id: NAT_3

16.Noboru Endou,
   Hilbert Space of Complex Sequences,
   pp. 187--190,
   MML Id: CSSPACE2

17.Noboru Endou,
   Banach Space of Absolute Summable Complex Sequences,
   pp. 191--194,
   MML Id: CSSPACE3

18.Yasunari Shidama,
   The Taylor Expansions,
   pp. 195--200,
   MML Id: TAYLOR_1

19.Noboru Endou,
   Complex Banach Space of Bounded Linear Operators,
   pp. 201--209,
   MML Id: CLOPBAN1

20.Noboru Endou,
   Complex Banach Space of Bounded Complex Sequences,
   pp. 211--218,
   MML Id: CSSPACE4

21.Hirofumi Fukura and Yatsuka Nakamura,
   Concatenation of Finite Sequences Reducing Overlapping Part and
     an Argument of Separators of Sequential Files,
   pp. 219--224,
   MML Id: FINSEQ_8

22.Yasumasa Suzuki and Noboru Endou,
   Cauchy Sequence of Complex Unitary Space,
   pp. 225--229,
   MML Id: CLVECT_3

All articles are available also on the home page of
Formalized Mathematics:
http://mizar.org/fm/

  Regards,
  Adam Grabowski
  Library Committee of the Association of Mizar Users