:: deftheorem defines || POLYDIFF:def 4 :
for L being non empty ZeroStr
for p being sequence of L
for n being Nat holds p || n = p +* (n,(0. L));