[mizar] New mizar articles - FM12(3)

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

Dear All,

We attach the second part of 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 were accepted for inclusion in the MML.

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

1. Noboru Endou,
   Complex Valued Functions Space,
   pp. 231--235,
   MML Id: CFUNCDOM

2. Noboru Endou,
   Banach Algebra of Bounded Complex Linear Operators,
   pp. 237--242,
   MML Id: CLOPBAN2

3. Yuzhong Ding and Xiquan Liang,
   Formulas and Identities of Trigonometric Functions,
   pp. 243--246,
   MML Id: SIN_COS5

4. Yuzhong Ding and Xiquan Liang,
   Solving Roots of the Special Polynomial Equation with Real Coefficients,
   pp. 247--250,
   MML Id: POLYEQ_4

5. Adam Grabowski and Artur Korni{\l}owicz,
   Algebraic Properties of Homotopies,
   pp. 251--260,
   MML Id: BORSUK_6

6. Artur Korni{\l}owicz, Yasunari Shidama, and Adam Grabowski,
   The Fundamental Group,
   pp. 261--268,
   MML Id: TOPALG_1

7. Takaya Nishiyama, Keiji Ohkubo, and Yasunari Shidama,
   The Continuous Functions on Normed Linear Spaces,
   pp. 269--275,
   MML Id: NFCONT_1

8. Takaya Nishiyama, Artur Korni{\l}owicz, and Yasunari Shidama,
   The Uniform Continuity of Functions on Normed Linear Spaces,
   pp. 277--279,
   MML Id: NFCONT_2

9. Noboru Endou,
   Series on Complex Banach Algebra,
   pp. 281--288,
   MML Id: CLOPBAN3

10.Noboru Endou,
   Exponential Function on Complex Banach Algebra,
   pp. 289--293,
   MML Id: CLOPBAN4

11.Artur Korni{\l}owicz,
   The Fundamental Group of Convex Subspaces of ${\cal E}^n_{\rm T}$,
   pp. 295--299,
   MML Id: TOPALG_2

12.Artur Korni{\l}owicz and Yasunari Shidama,
   Intersections of Intervals and Balls in ${\cal E}^n_{\rm T}$,
   pp. 301--306,
   MML Id: TOPREAL9

13.Magdalena Jastrz\c{e}bska and Adam Grabowski,
   Some Properties of Fibonacci Numbers,
   pp. 307--313,
   MML Id: FIB_NUM2

14.Ewa Romanowicz and Adam Grabowski,
   The Hall Marriage Theorem,
   pp. 315--320,
   MML Id: HALLMAR1

15.Hiroshi Imura, Morishige Kimura, and Yasunari Shidama,
   The Differentiable Functions on Normed Linear Spaces,
   pp. 321--327,
   MML Id: NDIFF_1

16.Piotr Wojtecki and Adam Grabowski,
   Lucas Numbers and Generalized Fibonacci Numbers,
   pp. 329--333,
   MML Id: FIB_NUM3

17.Katarzyna Romanowicz and Adam Grabowski,
   The Operation of Addition of Relational Structures,
   pp. 335--339,
   MML Id: LATSUM_1

18.Karol P\c{a}k,
   The Nagata-Smirnov Theorem. Part I,
   pp. 341--346,
   MML Id: NAGATA_1

19.Gijs Geleijnse and Grzegorz Bancerek,
   Properties of Groups,
   pp. 347--350,
   MML Id: GROUP_8

20.Dorota Cz\c{e}stochowska and Adam Grabowski,
   Catalan Numbers,
   pp. 351--353,
   MML Id: CATALAN1

21.Violetta Kozarkiewicz and Adam Grabowski,
   Axiomatization of Boolean Algebras Based on Sheffer Stroke,
   pp. 355--361,
   MML Id: SHEFFER1

22.Aneta {\L}ukaszuk and Adam Grabowski,
   Short Sheffer Stroke-Based Single Axiom for Boolean Algebras,
   pp. 363--370,
   MML Id: SHEFFER2

23.Hiroshi Imura, Yuji Sakai, and Yasunari Shidama,
   Differentiable Functions on Normed Linear Spaces. Part II,
   pp. 371--374,
   MML Id: NDIFF_2

24.Takaya Nishiyama, Hirofumi Fukura, and Yatsuka Nakamura,
   Logical Correctness of Vector Calculation Programs,
   pp. 375--380,
   MML Id: PRGCOR_2

25.Hiroshi Imura, Masami Tanaka, and Yatsuka Nakamura,
   Continuous Mappings between Finite and One-Dimensional Finite
     Topological Spaces,
   pp. 381--384,
   MML Id: FINTOPO4

26.Karol P\c{a}k,
   The Nagata-Smirnov Theorem. Part II,
   pp. 385--389,
   MML Id: NAGATA_2

27.Artur Korni{\l}owicz,
   On the Isomorphism of Fundamental Groups,
   pp. 391--396,
   MML Id: TOPALG_3

28.Noboru Endou,
   Algebra of Complex Vector Valued Functions,
   pp. 397--401,
   MML Id: VFUNCT_2

29.Noboru Endou,
   Continuous Functions on Real and Complex Normed Linear Spaces,
   pp. 403--419,
   MML Id: NCFCONT1,

30.Artur Korni{\l}owicz,
   On the Fundamental Groups of Products of Topological Spaces,
   pp. 421--425,
   MML Id: TOPALG_4

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

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