theorem :: RING_EMB:16

for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for f being Polynomial of 0,R holds
( dom f = Bags 0 & Bags 0 = {{}} & rng f = {(f . (EmptyBag 0))} )