theorem Th13: :: ALGGEO_1:13

for R being domRing
for n being non empty Ordinal holds Zero_ (0_ (n,R)) = Funcs (n,([#] R))