theorem :: ALGGEO_1:27

for R being domRing
for n being non empty Ordinal
for m being non zero Nat
for P being Subset of (singletons (Funcs (n,([#] R)))) st card P = m holds
union P is Algebraic_Set of n,R