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 3;
A2: now :: thesis: for x being object st x in dom p holds
p . x = 0. L
let x be object ; :: 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:12;
i >= 0 ;
hence p . x = 0. L by A1; :: thesis: verum
end;
dom p = NAT by NORMSP_1:12;
hence p = 0_. L by A2, FUNCOP_1:11; :: thesis: verum