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

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

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

hence p . n = <%a,b%> . n by POLYNOM5:38; :: thesis: verum

end;

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

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

end;

end;