let F be Field; :: thesis: for c1, c2 being Element of F holds (rpoly (1,c1)) *' (rpoly (1,c2)) = <%(c1 * c2),(- (c1 + c2)),(1. F)%>
let c1, c2 be Element of F; :: thesis: (rpoly (1,c1)) *' (rpoly (1,c2)) = <%(c1 * c2),(- (c1 + c2)),(1. F)%>
thus (rpoly (1,c1)) *' (rpoly (1,c2)) = <%(- c1),(1. F)%> *' (rpoly (1,c2)) by RING_5:10
.= <%(- c1),(1. F)%> *' <%(- c2),(1. F)%> by RING_5:10
.= <%(c1 * c2),(- (c1 + c2)),(1. F)%> by lemred3 ; :: thesis: verum