Support (1_1 (x,L)) = {(UnitBag x)} by Th13;
hence 1_1 (x,L) is finite-Support by POLYNOM1:def 5; :: thesis: verum