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*>;

hence rpoly (1,a) is Ppoly of R by A, dpp1; :: thesis: verum

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)

Product <*p*> = p
by GROUP_4:9;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) by FINSEQ_1:40; :: thesis: verum

end;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) by FINSEQ_1:40; :: thesis: verum

hence rpoly (1,a) is Ppoly of R by A, dpp1; :: thesis: verum