Volume 18 (2010): Issue 1 (January 2010)

In this article, we first extend several basic theorems of the operation of vector in 3-dimensional Euclidean spaces. Then three unit vectors: e1, e2, e3 and the definition of vector function in the same spaces are introduced. By dint of unit vector the main operation properties as well as the differentiation formulas of vector function are shown [12].

In this article, we give a definition of a functional space which is constructed from all continuous functions defined on a compact topological space. We prove that this functional space is a Banach algebra. Next, we give a definition of a function space which is constructed from all real-valued continuous functions with bounded support. We prove that this function space is a real normed space.

This article introduces the free magma M(X) constructed on a set X [6]. Then, we formalize some theorems about M(X): if f is a function from the set X to a magma N, the free magma M(X) has a unique extension of f to a morphism of M(X) into N and every magma is isomorphic to a magma generated by a set X under a set of relators on M(X). In doing it, the article defines the stable subset under the law of composition of a magma, the submagma, the equivalence relation compatible with the law of composition and the equivalence kernel of a function. We also introduce some schemes on the recursive function.

In this article, we give several differentiation and integrability formulas of special and composite functions including the trigonometric function, and the polynomial function.

In this article, we shall extend the result of [19] to discuss partial differentiation of real ternary functions (refer to [8] and [16] for partial differentiation).

This text includes the definition of chain-complete poset, fix-point theorem on it, and the definition of the function space of continuous functions on chain-complete posets [10].

This article describes the concept of the nilpotent group and some properties of the nilpotent groups.

In this article, we give some important theorems of forward difference, backward difference, central difference and difference quotient and forward difference, backward difference, central difference and difference quotient formulas of some special functions.

The aim of this paper is to develop a formal theory of Mizar linguistic concepts following the ideas from [6] and [7]. The theory presented is an abstraction from the existing implementation of the Mizar system and is devoted to the formalization of Mizar expressions. The concepts formalized here are: standarized constructor signature, arity-rich signatures, and the unification of Mizar expressions.

In the paper we show how to express the Fibonacci numbers and Lucas numbers using the floor and ceiling operations.

In the article we prove that a family of open n-hypercubes is a basis of n-dimensional Euclidean space. The equality of the space and the product of n real lines has been proven.

In this article we describe the notion of affinely independent subset of a real linear space. First we prove selected theorems concerning operations on linear combinations. Then we introduce affine independence and prove the equivalence of various definitions of this notion. We also introduce the notion of the affine hull, i.e. a subset generated by a set of vectors which is an intersection of all affine sets including the given set. Finally, we introduce and prove selected properties of the barycentric coordinates.

In this article we define the notion of abstract simplicial complexes and operations on them. We introduce the following basic notions: simplex, face, vertex, degree, skeleton, subdivision and substructure, and prove some of their properties.