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