theorem :: POLYNOM5:50

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr
for p being Polynomial of L holds Subst (p,(0_. L)) = <%(p . 0)%>