let L be non trivial ZeroStr ; :: thesis: for p being Polynomial of L st len p = 1 holds
ex a being non zero Element of L st p = <%a%>
let p be Polynomial of L; :: thesis: ( len p = 1 implies ex a being non zero Element of L st p = <%a%> )
assume A1: len p = 1 ; :: thesis: ex a being non zero Element of L st p = <%a%>
1 = 1 + 0 ;
then p . 0 <> 0. L by A1, ALGSEQ_1:10;
then reconsider a = p . 0 as non zero Element of L by STRUCT_0:def 12;
take a ; :: thesis: p = <%a%>
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: p . n = <%a%> . n

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: p . n = <%a%> . n

hence p . n = <%a%> . n by POLYNOM5:32; :: thesis: verum

end;

suppose n > 0 ; :: thesis: p . n = <%a%> . n

then A2: 0 + 1 <= n by NAT_1:13;
hence p . n = 0. L by A1, ALGSEQ_1:8
.= <%a%> . n by A2, POLYNOM5:32 ;
:: thesis: verum

end;

end;