Fin-set: A syntactical definition of finite sets

We state Fin-set, by which one founds the notion of finite sets in a syntactical way. Any finite set {a1, a2,..., an} is defined as a well formed term of the form S(a1 + (a2 + (··· + (an−1 + an)···))), where + is a binary and S a unary operational symbol. Related to the operational symbol the term-substitutions (1) are introduced. Definition of finite sets is called syntactical because by two algorithms Set-alg and Calc one can effectively establish whether any given set-terms are equal or not equal. All other notions related to finite sets, like ∈, ordered pair, Cartesian product, relation, function, cardinal number are defined as terms as well. Each of these definitions is recursive. For instance, ∈ is defined by x ∈ S(a1) iff x = a1 x ∈ S(a1 + ···+ an) iff x = a1 or x ∈ S(a2 + ···+ an) x/∈ O (O denotes the empty set).