let R be comRing; :: 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 eval (p,a) = y + (a * 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 eval (p,a) = y + (a * z) )
assume A: deg p < 2 ; :: thesis: for a being Element of R ex y, z being Element of R st eval (p,a) = y + (a * z)
let a be Element of R; :: thesis: ex y, z being Element of R st eval (p,a) = y + (a * z)
consider y, z being Element of R such that
B: p = <%y,z%> by A, deg2;
take y ; :: thesis: ex z being Element of R st eval (p,a) = y + (a * z)
take z ; :: thesis: eval (p,a) = y + (a * z)
thus eval (p,a) = y + (z * a) by B, POLYNOM5:44
.= y + (a * z) by GROUP_1:def 12 ; :: thesis: verum