pairs of polynomials whose second component is not the zero polynomial.8 **These**
can be easily introduced as a Mizar type Rational_function of L**, where** L is the underlying coefficient domain.

definition let L be non trivial multLoopStr_0; mode rational_function of L means ex p1 being Polynomial of L st ex p2 being non zero Polynomial of L st it = [p1,p2];
end; In Mizar the result types of the pair constructor [ , ] **and the projections**
'1 and '2**, that in the original definition are simply** set**, then can be modified** into Rational_function and (non zero) Polynomial **respectively. In addition**
one can introduce the usual functions num and denom **as synonyms for the corresponding projections.**
definition let L be non trivial multLoopStr_0; let p1 be Polynomial of L;
let p2 be non zero Polynomial of L;
redefine func [p1,p2] -> rational_function of L;
end; definition let L be non trivial multLoopStr_0; let z be rational_function of L; redefine func z'1 -> Polynomial of L;
redefine func z'2 -> non zero Polynomial of L;
end; notation let L be non trivial multLoopStr_0; let z be rational_function of L; synonym num(z) for z'1; synonym denom(z) for z'2; end; Now that num and denom **— applied to rational functions - have result type**
Polynomial**, operations for rational functions can straightforwardly be defined** by employing the corresponding functions for polynomials. So, for example, the evaluation of rational functions can be defined using evaluation of polynomials and the division operator / **defined for arbitrary fields** L.

8 **Of course rational functions can be introduced "more algebraically" as the quotient**
field of a polynomial ring. Here we decided to use pairs to concentrate on application issues; see the discussion in section 5.