theorem :: ALGSEQ_1:13

for R being non empty ZeroStr st the carrier of R <> {(0. R)} holds
for k being Nat ex p being AlgSequence of R st len p = k