Many-argument relations

Summary. Definitions of relations based on finite sequences. The arity of relation, the set of logical values Boolean consisting of false and true and the operations of negation and conjunction on them are defined. MML Identifier:MARGREL1. WWW:http://mizar.org/JFM/Vol2/margrel1.html The articles [4], [2], [6], [1], [7], [3], and [5] provide the notation and terminology for this paper. In this paper k is a natural number and D is a non empty set. Let B, A be non empty sets and let b be an element of B. Then A ↦− → b is an element of B A. Let I1 be a set. We say that I1 is relation-like if and only if the conditions (Def. 1) are satisfied. (Def. 1)(i) For every set x such that x ∈ I1 holds x is a finite sequence, and (ii) for all finite sequences a, b such that a ∈ I1 and b ∈ I1 holds lena = lenb. Let us mention that there exists a set which is relation-like. A relation is a relation-like set. We follow the rules: X denotes a set, p, r denote relations, and a, b denote finite sequences. The following two propositions are true