theorem :: ALGSEQ_1:17

for R being non empty ZeroStr
for p being AlgSequence of R holds
( p = <%(0. R)%> iff rng p = {(0. R)} )