:: deftheorem Def9 defines zero RATFUNC1:def 9 :
for L being non trivial multLoopStr_0
for z being rational_function of L holds
( z is zero iff z `1 = 0_. L );