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

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

assume p is quadratic ; :: thesis: ex b, c being Element of R st p = <%c,b,(1. R)%>
then consider a being non zero Element of R, b, c being Element of R such that
A: p = <%c,b,a%> by qua5;
H: ( 3 -' 1 = 3 - 1 & a <> 0. R ) by XREAL_0:def 2;
1. R = LC p by RATFUNC1:def 7
.= p . ((len p) -' 1) by RATFUNC1:def 6
.= p . 2 by H, A, qua3
.= a by A, qua1 ;
hence ex b, c being Element of R st p = <%c,b,(1. R)%> by A; :: thesis: verum

end;

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