theorem Th9: :: ALGGEO_1:9

for R being domRing
for n being non empty Ordinal
for a being Element of R
for i being Element of n holds Support ((1_1 (i,R)) + (a | (n,R))) c= {(UnitBag i)} \/ {(EmptyBag n)}