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