let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L st len p = 0 holds
p = 0_. L
let p be Polynomial of L; :: thesis: ( len p = 0 implies p = 0_. L )
assume len p = 0 ; :: thesis: p = 0_. L
then A1: 0 is_at_least_length_of p by ALGSEQ_1:def 4;

A2: now

let x be set ; :: thesis: ( x in dom p implies p . x = 0. L )
assume x in dom p ; :: thesis: p . x = 0. L
then reconsider i = x as Element of NAT by NORMSP_1:17;
i >= 0 ;
hence p . x = 0. L by A1, ALGSEQ_1:def 3; :: thesis: verum

end;

dom p = NAT by NORMSP_1:17;
hence p = 0_. L by A2, FUNCOP_1:17; :: thesis: verum