Volume 13, Number 3 (2005): pdf, ps, dvi.

- Krzysztof Retel.
Properties of First and Second Order Cutting of Binary Relations,
Formalized Mathematics 13(3), pages 361-365, 2005. MML Identifier: RELSET_2

**Summary**: This paper introduces some notions concerning binary relations according to \cite{Riguet}. It is also an attempt to complement the knowledge contained in Mizar Mathematical Library regarding binary relations. We define here an image and inverse image of element of set A under binary relation of two sets A,B as image and inverse image of singleton of the element under this relation, respectively. Next, we define "The First Order Cutting Relation of two sets A,B under a subset of the set A" as the union of images of elements of this subset under the relation. We also define "The Second Order Cutting Subset of the Cartesian Product of two sets A,B under a subset of the set A" as an intersection of images of elements of this subset under the subset of the cartesian product. The paper also defines first and second projection of binary relations. The main goal of the article is to prove properties and collocations of introduced definitions in this paper. The numbers written in parenthesis after the label of theorems correspond to the numbers of expressions contained in the original article.

- Wenpai Chang, Hiroshi Yamazaki, Yatsuka Nakamura.
The Inner Product and Conjugate of Finite Sequences of Complex Numbers,
Formalized Mathematics 13(3), pages 367-373, 2005. MML Identifier: COMPLSP2

**Summary**: A concept of "the inner product and conjugate of finite sequences of complex numbers" is defined here. Addition, subtraction, Scalar multiplication and inner product are introduced using correspondent definitions of "conjugate of finite sequences of Field". Many equations for such operations consist like a case of "conjugate of finite sequences of Field". Some operations on the set of $n$-tuples of complex numbers are introduced as well. Addition, difference of such $n$-tuples, complement of a $n$-tuple and multiplication of these are defined in terms of complex numbers.

- Bo Zhang, Hiroshi Yamazaki, Yatsuka Nakamura.
Inferior Limit and Superior Limit of Sequences of Real Numbers,
Formalized Mathematics 13(3), pages 375-381, 2005. MML Identifier: RINFSUP1

**Summary**: A concept of inferior limit and superior limit of sequences of real numbers is defined here. This article contains the following items: definition of the superior sequence and the inferior sequence of real numbers, definition of the superior limit and the inferior limit of real number, and definition of the relation between the limit value and the superior limit, the inferior limit of sequences of real numbers.

- Fuguo Ge, Xiquan Liang, Yuzhong Ding.
Formulas and Identities of Inverse Hyperbolic Functions,
Formalized Mathematics 13(3), pages 383-387, 2005. MML Identifier: SIN_COS7

**Summary**: This article describes definitions of inverse hyperbolic functions and their main properties, as well as some addition formulas with hyperbolic functions.

- Akihiro Kubo.
Lines on Planes in $n$-Dimensional Euclidean Spaces,
Formalized Mathematics 13(3), pages 389-397, 2005. MML Identifier: EUCLIDLP

**Summary**: In this paper, we introduce basic properties of lines in the plane on this space. Lines and planes are expressed by the vector equation and are the image of $R$ and $R^2.$ By this, we can say that the properties of the classic Euclid geometry are satisfied also in $R^n$ as we know them intuitively. Next, we define the metric between the point and the line of this space.

- Karol Pcak.
Cardinal Numbers and Finite Sets,
Formalized Mathematics 13(3), pages 399-406, 2005. MML Identifier: CARD_FIN

**Summary**: In this paper we define class of functions and operators needed for proof of the principle of inclusions and the disconnections. We given also certain cardinal numbers concerning elementary class of functions (of course this function mapping finite set in finite set).

- Bo Zhang, Hiroshi Yamazaki, Yatsuka Nakamura.
Some Equations Related to the Limit of Sequence of Subsets,
Formalized Mathematics 13(3), pages 407-412, 2005. MML Identifier: SETLIM_2

**Summary**: Set operations for sequences of subsets are introduced here. Some relations for these operations with the limit of sequences of subsets, also with the inferior sequence and the superior sequence of sets, and with the inferior limit and the superior limit of sets are shown.

- Fuguo Ge, Xiquan Liang.
On the Partial Product of Series and Related Basic Inequalities,
Formalized Mathematics 13(3), pages 413-416, 2005. MML Identifier: SERIES_3

**Summary**: This article describes definition of partial product of series, introduced similarly to its related partial sum, as well as several important inequalities true for chosen special series.

- Masami Tanaka, Hiroshi Imura, Yatsuka Nakamura.
Homeomorphism between Finite Topological Spaces, Two-Dimensional Lattice Spaces and a Fixed Point Theorem,
Formalized Mathematics 13(3), pages 417-419, 2005. MML Identifier: FINTOPO5

**Summary**: In this paper, we first introduced the notion of homeomorphism between finite topological spaces. We also gave a fixed point theorem in finite topological space. Next, we showed two 2-dimensional concrete models of lattice spaces. One was 2-dimensional linear finite topological space. Another was 2-dimensional small finite topological space.

- Akira Nishino, Yasunari Shidama.
The Maclaurin Expansions,
Formalized Mathematics 13(3), pages 421-425, 2005. MML Identifier: TAYLOR_2

**Summary**: A concept of the Maclaurin expansions is defined here. This article contains the definition of the Maclaurin expansion and expansions of exp, sin and cos functions.

- Yan Zhang, Xiquan Liang.
Several Differentiable Formulas of Special Functions,
Formalized Mathematics 13(3), pages 427-434, 2005. MML Identifier: FDIFF_4

**Summary**: In this article, we give several differentiable formulas of special functions.