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