:: deftheorem defines 1._ RATFUNC1:def 14 :
for L being non degenerated multLoopStr_0 holds 1._ L = [(1_. L),(1_. L)];