theorem Th24: :: ALGGEO_1:24

for R being domRing
for n being non empty Ordinal
for m being non zero Nat
for F being Subset of (Alg_Sets (n,R)) st card F = m holds
union F is Algebraic_Set of n,R