:: deftheorem defines - POLYNOM3:def 6 :
for L being non empty addLoopStr
for p, q being sequence of L holds p - q = p + (- q);