theorem Th49: :: NUMBER19:49

for L being non degenerated domRing-like Ring
for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence holds deg (~ (Product (rpoly (f,z)))) = Sum f