let L be non empty ZeroStr ; :: thesis: <%(0. L)%> = 0_. L
len <%(0. L)%> = 0 by ALGSEQ_1:31;
hence <%(0. L)%> = 0_. L by POLYNOM4:8; :: thesis: verum