let R be domRing; :: thesis: for a being Element of R holds rpoly (1,a) is Ppoly of R
let a be Element of R; :: thesis: rpoly (1,a) is Ppoly of R
reconsider p = rpoly (1,a) as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
set F = <*p*>;

A: now :: thesis: for i being Nat st i in dom <*p*> holds
ex a being Element of R st <*p*> . i = rpoly (1,a)

let i be Nat; :: thesis: ( i in dom <*p*> implies ex a being Element of R st <*p*> . i = rpoly (1,a) )
assume AS: i in dom <*p*> ; :: thesis: ex a being Element of R st <*p*> . i = rpoly (1,a)
dom <*p*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by AS, TARSKI:def 1;
hence ex a being Element of R st <*p*> . i = rpoly (1,a) ; :: thesis: verum

end;

Product <*p*> = p by GROUP_4:9;
hence rpoly (1,a) is Ppoly of R by A, dpp1; :: thesis: verum