:: deftheorem defines seq POLYDIFF:def 3 :
for L being non empty ZeroStr
for x being Element of L
for n being Nat holds seq (n,x) = (0_. L) +* (n,x);