theorem Th14: :: ALGGEO_1:14
for R being domRing
for n being non empty Ordinal holds Zero_ (1_ (n,R)) = {} (Funcs (n,([#] R)))