Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990
Association of Mizar Users
Construction of Finite Sequence over Ring and Left, Right, and BiModules
over a Ring

Michal Muzalewski

Warsaw University, Bialystok

Leslaw W. Szczerba

Siedlce University
Summary.

This text includes definitions of finite sequences over rings and left,
right, and bimodule over a ring treated as functions defined for {\sl all}
natural numbers, but with almost everywhere equal to zero. Some elementary
theorems are proved, in particular for each category of sequences the scheme
about existence is proved. In all four cases, i.e. for rings, left,
right and bi modules are almost exactly the same, hovewer we do not know how
to do the job in Mizar in a different way. The paper is mostly based on the
paper [2]. In particular the notion of initial segment of natural numbers is
introduced which differs from that of [2] by starting with zero. This
proved to be more convenient for algebraic purposes.
Supported by RPBP.III24.C3.
The terminology and notation used in this paper have been
introduced in the following articles
[6]
[9]
[7]
[1]
[10]
[3]
[8]
[4]
[5]
Contents (PDF format)
Bibliography
 [1]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Czeslaw Bylinski.
Functions from a set to a set.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Jan Popiolek.
Real normed space.
Journal of Formalized Mathematics,
2, 1990.
 [6]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [7]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
 [8]
Wojciech A. Trybulec.
Vectors in real linear space.
Journal of Formalized Mathematics,
1, 1989.
 [9]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [10]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
Received September 13, 1990
[
Download a postscript version,
MML identifier index,
Mizar home page]