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