let R be Ring; :: thesis: for p being Polynomial of R st deg p < 2 holds
for a being Element of R ex y, z being Element of R st p = <%y,z%>
let p be Polynomial of R; :: thesis: ( deg p < 2 implies for a being Element of R ex y, z being Element of R st p = <%y,z%> )
assume A: deg p < 2 ; :: thesis: for a being Element of R ex y, z being Element of R st p = <%y,z%>
let a be Element of R; :: thesis: ex y, z being Element of R st p = <%y,z%>
take y = p . 0; :: thesis: ex z being Element of R st p = <%y,z%>
take z = p . 1; :: thesis: p = <%y,z%>
set q = <%y,z%>;

now :: thesis: for i being Element of NAT holds p . i = <%y,z%> . i

let i be Element of NAT ; :: thesis: p . b₁ = <%y,z%> . b₁

per cases ( i = 0 or i = 1 or ( i <> 0 & i <> 1 ) ) ;

suppose i = 0 ; :: thesis: p . b₁ = <%y,z%> . b₁

hence p . i = <%y,z%> . i by POLYNOM5:38; :: thesis: verum

end;

suppose i = 1 ; :: thesis: p . b₁ = <%y,z%> . b₁

hence p . i = <%y,z%> . i by POLYNOM5:38; :: thesis: verum

end;

suppose ( i <> 0 & i <> 1 ) ; :: thesis: p . b₁ = <%y,z%> . b₁

then B: not i is trivial by NAT_2:def 1;
then i >= 2 by NAT_2:29;
then i > deg p by A, XXREAL_0:2;
then i > (len p) - 1 by HURWITZ:def 2;
then i >= ((len p) - 1) + 1 by INT_1:7;
hence p . i = 0. R by ALGSEQ_1:8
.= <%y,z%> . i by B, NAT_2:29, POLYNOM5:38 ;
:: thesis: verum

end;

end;

end;

hence p = <%y,z%> ; :: thesis: verum