let R be domRing; :: thesis: for a being Element of R holds a | R = <%a%>
let a be Element of R; :: thesis: a | R = <%a%>
for j being Nat holds (a | R) . j = <%a%> . j

proof

let j be Nat; :: thesis: (a | R) . j = <%a%> . j
(a | R) . j = (a * (1_. R)) . j by RING_4:16
.= <%a%> . j by POLYNOM5:29 ;
hence (a | R) . j = <%a%> . j ; :: thesis: verum

end;

hence a | R = <%a%> ; :: thesis: verum