In section 4.2 we will see that this theorem is also the key to prove that stability checking can be reduced to synthesizing LC-one-ports, in **other words** to prove theorem 1 from above.

## 3 The Mizar System

The logical basis of Mizar [RT01,Miz10] is classical first order logic extended, however, with so-called schemes. Schemes introduce free second **order variables,**
in this way enabling among others the definition of induction schemes. **In addition Mizar objects are typed, the types forming a hierarchy with the fundamental**
type set. The user can introduce new (sub)types describing mathematical **objects such as groups, fields, vector spaces or polynomials over rings or fields. To**
this end the Mizar language provides a powerful typing mechanism based on adjective subtypes [Ban03].

The current development of Mizar relies on Tarski-Grothendieck set theory
- a variant of Zermelo Fraenkel set theory using Tarski's axiom on arbitrarily large, strongly inaccessible cardinals [Tar39] which can be used to prove the axiom of choice —, though in principle the Mizar language can be used with other axiom systems also. Mizar proofs are written in natural deduction style as presented in the calculus of [Ja´s34]. The rules of the calculus are connected with corresponding (English) natural language phrases so that the Mizar language is close to the one used in mathematical textbooks. The Mizar proof **checker** verifies the individual proof steps using the notion of obvious inferences [Dav81] to shorten the rather long proofs of pure natural deduction.

Mizar objects are typed, the types forming a hierarchy with the fundamental type set **[Ban03]. New types are constructed using type constructors called**
modes. Modes can be decorated with adjectives - given by so-called **attribute** definitions - in this way extending the type hierarchy: For example, given the mode Ring **and an attribute** commutative **a new mode** commutative Ring can be constructed, which obeys all the properties given by the mode Ring **plus** the ones stated by the attribute commutative**. Furthermore, a variable of type** commutative Ring **then is also of type** Ring**, which implies that all notions** defined for Ring **are available for** commutative Ring**. In addition all theorems**
proved for type Ring **are applicable for objects of type** commutative Ring**; indeed the Mizar checker itself infers subtype relations in order to check whether**
notions and theorems are applicable for a given type.

## 4 Mizar Formalization Of The Theorem 4.1 Some Preliminaries About Rational Functions

Although the theory of polynomials in Mizar is rather well developed, rational functions have not been defined yet. Rational functions can - analogously to polynomials - be defined over arbitrary fields: Rational functions are simply