Volume 5, Number 3 (1996): pdf, ps, dvi.

- Yatsuka Nakamura, Piotr Rudnicki.
Vertex Sequences Induced by Chains,
Formalized Mathematics 5(3), pages 297-304, 1996. MML Identifier: GRAPH_2

**Summary**: In the three preliminary sections to the article we define two operations on finite sequences which seem to be of general interest. The first is the $cut$ operation that extracts a contiguous chunk of a finite sequence from a position to a position. The second operation is a glueing catenation that given two finite sequences catenates them with removal of the first element of the second sequence. The main topic of the article is to define an operation which for a given chain in a graph returns the sequence of vertices through which the chain passes. We define the exact conditions when such an operation is uniquely definable. This is done with the help of the so called two-valued alternating finite sequences. We also prove theorems about the existence of simple chains which are subchains of a given chain. In order to do this we define the notion of a finite subsequence of a typed finite sequence.

- Andrzej Iwaniuk.
On the Lattice of Subspaces of a Vector Space,
Formalized Mathematics 5(3), pages 305-308, 1996. MML Identifier: VECTSP_8

**Summary**:

- Janusz Ganczarski.
On the Lattice of Subgroups of a Group,
Formalized Mathematics 5(3), pages 309-312, 1996. MML Identifier: LATSUBGR

**Summary**:

- Miroslaw Jan Paszek.
On the Lattice of Subalgebras of a Universal Algebra,
Formalized Mathematics 5(3), pages 313-316, 1996. MML Identifier: UNIALG_3

**Summary**:

- Andrzej Trybulec.
On the Decomposition of Finite Sequences,
Formalized Mathematics 5(3), pages 317-322, 1996. MML Identifier: FINSEQ_6

**Summary**:

- Yatsuka Nakamura, Andrzej Trybulec.
Decomposing a Go-Board into Cells,
Formalized Mathematics 5(3), pages 323-328, 1996. MML Identifier: GOBOARD5

**Summary**:

- Grzegorz Bancerek.
Indexed Category,
Formalized Mathematics 5(3), pages 329-337, 1996. MML Identifier: INDEX_1

**Summary**: The concept of indexing of a category (a part of indexed category, see \cite{TarleckiBurstallGoguen}) is introduced as a pair formed by a many sorted category and a many sorted functor. The indexing of a category $C$ against to \cite{TarleckiBurstallGoguen} is not a functor but it can be treated as a functor from $C$ into some categorial category (see \cite{CAT_5.ABS}). The goal of the article is to work out the notation necessary to define institutions (see \cite{GoguenBurstall}).

- Robert Milewski.
Associated Matrix of Linear Map,
Formalized Mathematics 5(3), pages 339-345, 1996. MML Identifier: MATRLIN

**Summary**:

- Andrzej Trybulec.
On the Geometry of a Go-Board,
Formalized Mathematics 5(3), pages 347-352, 1996. MML Identifier: GOBOARD6

**Summary**:

- Jozef Bialas, Yatsuka Nakamura.
The Theorem of Weierstrass,
Formalized Mathematics 5(3), pages 353-359, 1996. MML Identifier: WEIERSTR

**Summary**:

- Jozef Bialas, Yatsuka Nakamura.
Dyadic Numbers and T$_4$ Topological Spaces,
Formalized Mathematics 5(3), pages 361-366, 1996. MML Identifier: URYSOHN1

**Summary**:

- Grzegorz Bancerek, Yatsuka Nakamura.
Full Adder Circuit. Part I,
Formalized Mathematics 5(3), pages 367-380, 1996. MML Identifier: FACIRC_1

**Summary**: We continue the formalisation of circuits started by Piotr Rudnicki, Andrzej Trybulec, Pauline Kawamoto, and the second author in \cite{PRE_CIRC.ABS}, \cite{MSAFREE2.ABS}, \cite{CIRCUIT1.ABS}, \cite{CIRCUIT2.ABS}. The first step in proving properties of full $n$-bit adder circuit, i.e. 1-bit adder, is presented. We employ the notation of combining circuits introduced in \cite{CIRCCOMB.ABS}.

- Grzegorz Bancerek.
Continuous, Stable, and Linear Maps of Coherence Spaces,
Formalized Mathematics 5(3), pages 381-393, 1996. MML Identifier: COHSP_1

**Summary**:

- Artur Kornilowicz.
Some Basic Properties of Many Sorted Sets,
Formalized Mathematics 5(3), pages 395-399, 1996. MML Identifier: PZFMISC1

**Summary**:

- Oleg Okhotnikov.
Replacement of Subtrees in a Tree,
Formalized Mathematics 5(3), pages 401-403, 1996. MML Identifier: TREES_A

**Summary**: This paper is based on previous works \cite{TREES_1.ABS}, \cite{TREES_2.ABS} in which the operation replacement of subtree in a tree has been defined. We extend this notion for arbitrary non empty antichain.

- Grzegorz Bancerek.
Minimal Signature for Partial Algebra,
Formalized Mathematics 5(3), pages 405-414, 1996. MML Identifier: PUA2MSS1

**Summary**: The concept of characterizing of partial algebras by many sorted signature is introduced, i.e. we say that a signature $S$ characterizes a partial algebra $A$ if there is an $S$-algebra whose sorts form a partition of the carrier of algebra $A$ and operations are formed from operations of $A$ by the partition. The main result is that for any partial algebra there is the minimal many sorted signature which characterizes the algebra. The minimality means that there are signature endomorphisms from any signature which characterizes the algebra $A$ onto the minimal one.

- Oleg Okhotnikov.
The Subformula Tree of a Formula of the First Order Language,
Formalized Mathematics 5(3), pages 415-422, 1996. MML Identifier: QC_LANG4

**Summary**: A continuation of \cite{QC_LANG3.ABS}. The notions of list of immediate constituents of a formula and subformula tree of a formula are introduced. The some propositions related to these notions are proved.

- Mariusz Zynel.
The Steinitz Theorem and the Dimension of a Vector Space,
Formalized Mathematics 5(3), pages 423-428, 1996. MML Identifier: VECTSP_9

**Summary**: The main purpose of the paper is to define the dimension of an abstract vector space. The dimension of a finite-dimensional vector space is, by the most common definition, the number of vectors in a basis. Obviously, each basis contains the same number of vectors. We prove the Steinitz Theorem together with Exchange Lemma in the second section. The Steinitz Theorem says that each linearly-independent subset of a vector space has cardinality less than any subset that generates the space, moreover it can be extended to a basis. Further we review some of the standard facts involving the dimension of a vector space. Additionally, in the last section, we introduce two notions: the family of subspaces of a fixed dimension and the pencil of subspaces. Both of them can be applied in the algebraic representation of several geometries.

- Andrzej Trybulec.
On the Go-Board of a Standard Special Circular Sequence,
Formalized Mathematics 5(3), pages 429-438, 1996. MML Identifier: GOBOARD7

**Summary**:

- Jaroslaw Gryko.
On the Monoid of Endomorphisms of Universal Algebra and Many Sorted Algebra,
Formalized Mathematics 5(3), pages 439-442, 1996. MML Identifier: ENDALG

**Summary**:

- Andrzej Trybulec.
More on Segments on a Go-Board,
Formalized Mathematics 5(3), pages 443-450, 1996. MML Identifier: GOBOARD8

**Summary**: We continue the preparatory work for the Jordan Curve Theorem.

- Artur Kornilowicz.
Certain Facts about Families of Subsets of Many Sorted Sets,
Formalized Mathematics 5(3), pages 451-456, 1996. MML Identifier: MSSUBFAM

**Summary**:

- Beata Madras.
On the Concept of the Triangulation,
Formalized Mathematics 5(3), pages 457-462, 1996. MML Identifier: TRIANG_1

**Summary**: