Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

## Segments of Natural Numbers and Finite Sequences

Grzegorz Bancerek
Warsaw University, Bialystok
Krzysztof Hryniewiecki
Warsaw University, Warsaw

### Summary.

We define the notion of an initial segment of natural numbers and prove a number of their properties. Using this notion we introduce finite sequences, subsequences, the empty sequence, a sequence of a domain, and the operation of concatenation of two sequences.

Supported by RPBP.III-24.C1.

#### MML Identifier: FINSEQ_1

The terminology and notation used in this paper have been introduced in the following articles [9] [7] [11] [4] [12] [6] [5] [3] [2] [10] [8] [1]

#### Contents (PDF format)

1. Main Part
2. Moved from \cite{FINSET_1.ABS}, 1998
3. Moved from \cite{CARD_1.ABS}, 1999

#### Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[3] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[4] Grzegorz Bancerek. Sequences of ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[5] Grzegorz Bancerek. Zermelo theorem and axiom of choice. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[7] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[8] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[9] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[10] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[11] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[12] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.