:: deftheorem defines *' RATFUNC1:def 16 :
for L being non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being rational_function of L holds p *' q = [((p `1) *' (q `1)),((p `2) *' (q `2))];