let R be domRing; :: thesis: 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)}
let n be non empty Ordinal; :: thesis: 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)}
let a be Element of R; :: thesis: for i being Element of n holds Support ((1_1 (i,R)) + (a | (n,R))) c= {(UnitBag i)} \/ {(EmptyBag n)}
let i be Element of n; :: thesis: Support ((1_1 (i,R)) + (a | (n,R))) c= {(UnitBag i)} \/ {(EmptyBag n)}
set p = 1_1 (i,R);
set q = a | (n,R);
set UBi = UnitBag i;
A1: Support (1_1 (i,R)) = {(UnitBag i)} by HILBASIS:13;
A2: ( Support (a | (n,R)) = {} or Support (a | (n,R)) = {(EmptyBag n)} ) by POLYNOM7:22;
A5: Support ((1_1 (i,R)) + (a | (n,R))) c= (Support (1_1 (i,R))) \/ (Support (a | (n,R))) by POLYNOM1:20;
Support (a | (n,R)) c= {(EmptyBag n)} by A2, XBOOLE_0:def 1;
then (Support (1_1 (i,R))) \/ (Support (a | (n,R))) c= (Support (1_1 (i,R))) \/ {(EmptyBag n)} by XBOOLE_1:9;
hence Support ((1_1 (i,R)) + (a | (n,R))) c= {(UnitBag i)} \/ {(EmptyBag n)} by A1, A5; :: thesis: verum