theorem Th25: :: ALGGEO_1:25

for R being domRing
for n being non empty Ordinal
for a being Function of n,R holds Zero_ (polyset a) = {a}