reconsider p = rpoly (1,(1. R)) as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;

set F = <*p*>;

reconsider q = Product <*p*> as Polynomial of R by POLYNOM3:def 10;

( q = Product F & ( for i being Nat st i in dom F holds

ex a being Element of R st F . i = rpoly (1,a) ) )

take <*p*> ; :: thesis: ( q = Product <*p*> & ( for i being Nat st i in dom <*p*> holds

ex a being Element of R st <*p*> . i = rpoly (1,a) ) )

thus ( q = Product <*p*> & ( for i being Nat st i in dom <*p*> holds

ex a being Element of R st <*p*> . i = rpoly (1,a) ) ) by A; :: thesis: verum

set F = <*p*>;

reconsider q = Product <*p*> as Polynomial of R by POLYNOM3:def 10;

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)

take
q
; :: thesis: ex F being non empty FinSequence of (Polynom-Ring R) st 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

( q = Product F & ( for i being Nat st i in dom F holds

ex a being Element of R st F . i = rpoly (1,a) ) )

take <*p*> ; :: thesis: ( q = Product <*p*> & ( for i being Nat st i in dom <*p*> holds

ex a being Element of R st <*p*> . i = rpoly (1,a) ) )

thus ( q = Product <*p*> & ( for i being Nat st i in dom <*p*> holds

ex a being Element of R st <*p*> . i = rpoly (1,a) ) ) by A; :: thesis: verum