theorem Th50: :: NUMBER19:50

for L being non degenerated comRing
for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence
for x being Element of the carrier of L ex e being FinSequence of the carrier of L st
( eval ((~ (Product (rpoly (f,z)))),x) = Product e & len e = len f & ( for i being Nat st 1 <= i & i <= len e holds
e . i = eval ((rpoly ((f /. i),(z /. i))),x) ) )