let R be non degenerated Ring; :: thesis: for p being Polynomial of R holds
( p is quadratic iff ex a being non zero Element of R ex b, c being Element of R st p = <%c,b,a%> )
let p be Polynomial of R; :: thesis: ( p is quadratic iff ex a being non zero Element of R ex b, c being Element of R st p = <%c,b,a%> )

now :: thesis: ( p is quadratic implies ex a being non zero Element of R ex b, c being Element of R st p = <%c,b,a%> )

assume A: p is quadratic ; :: thesis: ex a being non zero Element of R ex b, c being Element of R st p = <%c,b,a%>
B: deg p = (len p) - 1 by HURWITZ:def 2;
reconsider a = p . 2, b = p . 1, c = p . 0 as Element of R ;

now :: thesis: for i being Element of NAT holds p . i = <%c,b,a%> . i

let i be Element of NAT ; :: thesis: p . b₁ = <%c,b,a%> . b₁
( i <= 2 implies not not i = 0 & ... & not i = 2 ) ;

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

suppose i = 0 ; :: thesis: p . b₁ = <%c,b,a%> . b₁

hence p . i = <%c,b,a%> . i by qua1; :: thesis: verum

end;

suppose i = 1 ; :: thesis: p . b₁ = <%c,b,a%> . b₁

hence p . i = <%c,b,a%> . i by qua1; :: thesis: verum

end;

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

hence p . i = <%c,b,a%> . i by qua1; :: thesis: verum

end;

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

then i + 1 > 2 + 1 by XREAL_1:6;
then C: i >= 3 by NAT_1:13;
hence <%c,b,a%> . i = 0. R by qua1
.= p . i by A, B, C, ALGSEQ_1:8 ;
:: thesis: verum

end;

end;

end;

then D: p = <%c,b,a%> ;
len p = 2 + 1 by B, A;
then not a is zero by ALGSEQ_1:10;
hence ex a being non zero Element of R ex b, c being Element of R st p = <%c,b,a%> by D; :: thesis: verum

end;

hence ( p is quadratic iff ex a being non zero Element of R ex b, c being Element of R st p = <%c,b,a%> ) ; :: thesis: verum