for R being non empty ZeroStr
for p, q being AlgSequence of R st len p = len q & ( for k being Nat st k < len p holds
p . k = q . k ) holds
p = q