:: deftheorem Def8 defines rational_function RATFUNC1:def 8 :
for L being non trivial multLoopStr_0
for b₂ being set holds
( b₂ is rational_function of L iff ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st b₂ = [p1,p2] );