:: deftheorem defines - POLYNOM1:def 7 :
for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, q being Series of n,L holds p - q = p + (- q);