theorem :: POLYNOM3:27

for L being non empty addLoopStr
for p, q being sequence of L
for n being Element of NAT holds (p - q) . n = (p . n) - (q . n) by NORMSP_1:def 3;