:: deftheorem defines * BASEL_2:def 2 :
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for a being Polynomial of L
for n being Nat holds n * a = n * (@ a);