Journal of Formalized Mathematics, Volume 2, 1990

Table of contents

1. Function Domains and Fr\aenkel Operator
   by Andrzej Trybulec
   
2. Integers
   by Michal J. Trybulec
   
3. The Complex Numbers
   by Czeslaw Bylinski
   
4. Ordinal Arithmetics
   by Grzegorz Bancerek
   
5. The Modification of a Function by a Function and the Iteration of the Composition of a Function
   by Czeslaw Bylinski
   
6. Finite Sequences and Tuples of Elements of a Non-empty Sets
   by Czeslaw Bylinski
   
7. Curried and Uncurried Functions
   by Grzegorz Bancerek
   
8. Cardinal Arithmetics
   by Grzegorz Bancerek
   
9. Fano-Desargues Parallelity Spaces
   by Eugeniusz Kusak and Wojciech Leonczuk
   
10. Real Functions Spaces
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
    
11. Tarski's Classes and Ranks
    by Grzegorz Bancerek
    
12. Non-contiguous Substrings and One-to-one Finite Sequences
    by Wojciech A. Trybulec
    
13. Pigeon Hole Principle
    by Wojciech A. Trybulec
    
14. Linear Combinations in Real Linear Space
    by Wojciech A. Trybulec
    
15. K\"onig's Theorem
    by Grzegorz Bancerek
    
16. Universal Classes
    by Bogdan Nowak and Grzegorz Bancerek
    
17. Analytical Ordered Affine Spaces
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
    
18. Metric Spaces
    by Stanislawa Kanas, Adam Lecko, and Mariusz Startek
    
19. Ordered Affine Spaces Defined in Terms of Directed Parallelity - Part I
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
    
20. Parallelity and Lines in Affine Spaces
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
    
21. Classical Configurations in Affine Planes
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
    
22. Affine Localizations of Desargues Axiom
    by Eugeniusz Kusak, Henryk Oryszczyszyn, and Krzysztof Prazmowski
    
23. Binary Operations Applied to Finite Sequences
    by Czeslaw Bylinski
    
24. Semigroup Operations on Finite Subsets
    by Czeslaw Bylinski
    
25. The Collinearity Structure
    by Wojciech Skaba
    
26. The Sum and Product of Finite Sequences of Real Numbers
    by Czeslaw Bylinski
    
27. A Classical First Order Language
    by Czeslaw Bylinski
    
28. Classical and Non-classical Pasch Configurations in Ordered Affine Planes
    by Henryk Oryszczyszyn, Krzysztof Prazmowski, and Malgorzata Prazmowska
    
29. The Lattice of Real Numbers. The Lattice of Real Functions
    by Marek Chmur
    
30. A Construction of an Abstract Space of Congruence of Vectors
    by Grzegorz Lewandowski and Krzysztof Prazmowski
    
31. A First-Order Predicate Calculus
    by Agata Darmochwal
    
32. Partial Functions from a Domain to a Domain
    by Jaroslaw Kotowicz
    
33. Partial Functions from a Domain to the Set of Real Numbers
    by Jaroslaw Kotowicz
    
34. Increasing and Continuous Ordinal Sequences
    by Grzegorz Bancerek
    
35. Transformations in Affine Spaces
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
    
36. Subcategories and Products of Categories
    by Czeslaw Bylinski
    
37. Many-Argument Relations
    by Edmund Woronowicz
    
38. Interpretation and Satisfiability in the First Order Logic
    by Edmund Woronowicz
    
39. Probability
    by Andrzej Nedzusiak
    
40. Translations in Affine Planes
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
    
41. Introduction to Probability
    by Jan Popiolek
    
42. A Construction of Analytical Projective Space
    by Wojciech Leonczuk and Krzysztof Prazmowski
    
43. Projective Spaces
    by Wojciech Leonczuk and Krzysztof Prazmowski
    
44. Topological Properties of Subsets in Real Numbers
    by Konrad Raczkowski and Pawel Sadowski
    
45. Properties of Real Functions
    by Jaroslaw Kotowicz
    
46. Real Function Continuity
    by Konrad Raczkowski and Pawel Sadowski
    
47. Real Function Uniform Continuity
    by Jaroslaw Kotowicz and Konrad Raczkowski
    
48. Real Function Differentiability
    by Konrad Raczkowski and Pawel Sadowski
    
49. Average Value Theorems for Real Functions of One Variable
    by Jaroslaw Kotowicz, Konrad Raczkowski, and Pawel Sadowski
    
50. Construction of Rings and Left-, Right-, and Bi-Modules over a Ring
    by Michal Muzalewski
    
51. Properties of Fields
    by Jozef Bialas
    
52. Filters - Part I. Implicative Lattices
    by Grzegorz Bancerek
    
53. Groups
    by Wojciech A. Trybulec
    
54. The Divisibility of Integers and Integer Relatively Primes
    by Rafal Kwiatek and Grzegorz Zwara
    
55. From Loops to Abelian Multiplicative Groups with Zero
    by Michal Muzalewski and Wojciech Skaba
    
56. Basic Properties of Rational Numbers
    by Andrzej Kondracki
    
57. Basis of Real Linear Space
    by Wojciech A. Trybulec
    
58. Finite Sums of Vectors in Vector Space
    by Wojciech A. Trybulec
    
59. Subgroup and Cosets of Subgroups
    by Wojciech A. Trybulec
    
60. Subspaces and Cosets of Subspaces in Vector Space
    by Wojciech A. Trybulec
    
61. Operations on Subspaces in Vector Space
    by Wojciech A. Trybulec
    
62. Linear Combinations in Vector Space
    by Wojciech A. Trybulec
    
63. Basis of Vector Space
    by Wojciech A. Trybulec
    
64. Factorial and Newton Coeffitients
    by Rafal Kwiatek
    
65. Analytical Metric Affine Spaces and Planes
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
    
66. Some Elementary Notions of the Theory of Petri Nets
    by Waldemar Korczynski
    
67. Classes of Conjugation. Normal Subgroups
    by Wojciech A. Trybulec
    
68. Replacing of Variables in Formulas of ZF Theory
    by Grzegorz Bancerek
    
69. The Reflection Theorem
    by Grzegorz Bancerek
    
70. Binary Operations on Finite Sequences
    by Wojciech A. Trybulec
    
71. Finite Join and Finite Meet, and Dual Lattices
    by Andrzej Trybulec
    
72. Consequences of the Reflection Theorem
    by Grzegorz Bancerek
    
73. Desargues Theorem In Projective 3-Space
    by Eugeniusz Kusak
    
74. The Limit of a Real Function at Infinity
    by Jaroslaw Kotowicz
    
75. The One-Side Limits of a Real Function at a Point
    by Jaroslaw Kotowicz
    
76. Lattice of Subgroups of a Group. Frattini Subgroup
    by Wojciech A. Trybulec
    
77. Equalities and Inequalities in Real Numbers
    by Andrzej Kondracki
    
78. Countable Sets and Hessenberg's Theorem
    by Grzegorz Bancerek
    
79. The Limit of a Real Function at a Point
    by Jaroslaw Kotowicz
    
80. The Limit of a Composition of Real Functions
    by Jaroslaw Kotowicz
    
81. Locally Connected Spaces
    by Beata Padlewska
    
82. Construction of Finite Sequence over Ring and Left-, Right-, and Bi-Modules over a Ring
    by Michal Muzalewski and Leslaw W. Szczerba
    
83. Relations of Tolerance
    by Krzysztof Hryniewiecki
    
84. Real Normed Space
    by Jan Popiolek
    
85. Schemes of Existence of Some Types of Functions
    by Jaroslaw Kotowicz
    
86. Integer and Rational Exponents
    by Konrad Raczkowski
    
87. Homotheties and Shears in Affine Planes
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
    
88. Directed Geometrical Bundles and Their Analytical Representation
    by Grzegorz Lewandowski, Krzysztof Prazmowski, and Bozena Lewandowska
    
89. Definable Functions
    by Grzegorz Bancerek
    
90. Propositional Calculus
    by Grzegorz Bancerek, Agata Darmochwal, and Andrzej Trybulec
    
91. Complex Spaces
    by Czeslaw Bylinski and Andrzej Trybulec
    
92. Several Pepoerties of Fields. Field Theory
    by Jozef Bialas
    
93. Infimum and Supremum of the Set of Real Numbers. Measure Theory
    by Jozef Bialas
    
94. Series of Positive Real Numbers. Measure Theory
    by Jozef Bialas
    
95. From Double Loops to Fields
    by Wojciech Skaba and Michal Muzalewski
    
96. Metrics in Cartesian Product
    by Stanislawa Kanas and Jan Stankiewicz
    
97. Submetric Spaces - Part I
    by Adam Lecko and Mariusz Startek
    
98. On Pseudometric Spaces
    by Adam Lecko and Mariusz Startek
    
99. Real Exponents and Logarithms
    by Konrad Raczkowski and Andrzej Nedzusiak
    
100. Hessenberg Theorem
     by Eugeniusz Kusak and Wojciech Leonczuk
     
101. Three-Argument Operations and Four-Argument Operations
     by Michal Muzalewski and Wojciech Skaba
     
102. Incidence Projective Spaces
     by Wojciech Leonczuk and Krzysztof Prazmowski
     
103. One-Dimensional Congruence of Segments, Basic Facts and Midpoint Relation
     by Barbara Konstanta, Urszula Kowieska, Grzegorz Lewandowski, and Krzysztof Prazmowski
     
104. Algebra of Normal Forms
     by Andrzej Trybulec
     
105. Ordered Rings - Part I
     by Michal Muzalewski and Leslaw W. Szczerba
     
106. Ordered Rings - Part II
     by Michal Muzalewski and Leslaw W. Szczerba
     
107. Ordered Rings - Part III
     by Michal Muzalewski and Leslaw W. Szczerba
     
108. $N$-Tuples and Cartesian Products for $n=5$
     by Michal Muzalewski and Wojciech Skaba
     
109. $N$-Tuples and Cartesian Products for $n=6$
     by Michal Muzalewski and Wojciech Skaba
     
110. $N$-Tuples and Cartesian Products for $n=7$
     by Michal Muzalewski and Wojciech Skaba
     
111. $N$-Tuples and Cartesian Products for $n=8$
     by Michal Muzalewski and Wojciech Skaba
     
112. $N$-Tuples and Cartesian Products for $n=9$
     by Michal Muzalewski and Wojciech Skaba
     
113. Ternary Fields
     by Michal Muzalewski and Wojciech Skaba
     
114. The $\sigma$-additive Measure Theory
     by Jozef Bialas
     
115. Incidence Projective Space ( a reduction theorem in a plane)
     by Eugeniusz Kusak and Wojciech Leonczuk
     
116. Groups, Rings, Left- and Right-Modules
     by Michal Muzalewski and Wojciech Skaba
     
117. Linear Independence in Left Module over Domain
     by Michal Muzalewski and Wojciech Skaba
     
118. Submodules and Cosets of Submodules in Right Module over Associative Ring
     by Michal Muzalewski and Wojciech Skaba
     
119. Operations on Submodules in Right Module over Associative Ring
     by Michal Muzalewski and Wojciech Skaba
     
120. Linear Combinations in Right Module over Associative Ring
     by Michal Muzalewski and Wojciech Skaba
     
121. Linear Independence in Right Module over Domain
     by Michal Muzalewski and Wojciech Skaba
     
122. Calculus of Propositions
     by Jan Popiolek and Andrzej Trybulec
     
123. Calculus of Quantifiers. Deduction Theorem
     by Agata Darmochwal
     
124. A Construction of Analytical Ordered Trapezium Spaces
     by Henryk Oryszczyszyn and Krzysztof Prazmowski
     
125. On Projections in Projective Planes - Part II
     by Eugeniusz Kusak, Wojciech Leonczuk, and Krzysztof Prazmowski
     
126. Metric-Affine Configurations in Metric Affine Planes - Part I
     by Jolanta Swierzynska and Bogdan Swierzynski
     
127. Metric-Affine Configurations in Metric Affine Planes - Part II
     by Jolanta Swierzynska and Bogdan Swierzynski
     
128. Fanoian, Pappian and Desarguesian Affine Spaces
     by Krzysztof Prazmowski
     
129. Elementary Variants of Affine Configurational Theorems
     by Krzysztof Prazmowski and Krzysztof Radziszewski
     
130. Semi-Affine Space
     by Eugeniusz Kusak and Krzysztof Radziszewski
     
131. Planes in Affine Spaces
     by Wojciech Leonczuk, Henryk Oryszczyszyn, and Krzysztof Prazmowski
     
132. Graphs
     by Krzysztof Hryniewiecki
     
133. Mostowski's Fundamental Operations - Part I
     by Andrzej Kondracki
     
134. A Projective Closure and Projective Horizon of an Affine Space
     by Henryk Oryszczyszyn and Krzysztof Prazmowski
     
135. Schemes
     by Stanislaw T. Czuba