let L be non trivial ZeroStr ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ex b being Element of L ex c being non zero Element of L st p = <%a,b,c%>
take b = p . 1; :: thesis: ex c being non zero Element of L st p = <%a,b,c%>
take c ; :: thesis: p = <%a,b,c%>
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: p . n = <%a,b,c%> . n
( not not n = 0 & ... & not n = 2 or n > 2 ) ;

per cases then ( n = 0 or n = 1 or n = 2 or n > 2 ) ;

suppose ( n = 0 or n = 1 or n = 2 ) ; :: thesis: p . n = <%a,b,c%> . n

hence p . n = <%a,b,c%> . n by NIVEN:23, NIVEN:24, NIVEN:25; :: thesis: verum

end;

suppose n > 2 ; :: thesis: p . n = <%a,b,c%> . n

then A2: 2 + 1 <= n by NAT_1:13;
hence p . n = 0. L by A1, ALGSEQ_1:8
.= <%a,b,c%> . n by A2, NIVEN:26 ;
:: thesis: verum

end;

end;