let X be set ; :: thesis: for x being Element of X
for L being non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr holds Support (1_1 (x,L)) = {(UnitBag x)}
let x be Element of X; :: thesis: for L being non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr holds Support (1_1 (x,L)) = {(UnitBag x)}
let L be non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr ; :: thesis: Support (1_1 (x,L)) = {(UnitBag x)}

now

let a be set ; :: thesis: ( ( a in Support (1_1 (x,L)) implies a in {(UnitBag x)} ) & ( a in {(UnitBag x)} implies a in Support (1_1 (x,L)) ) )

hereby :: thesis: ( a in {(UnitBag x)} implies a in Support (1_1 (x,L)) )

assume A1: a in Support (1_1 (x,L)) ; :: thesis: a in {(UnitBag x)}
then reconsider b = a as Element of Bags X ;

now

assume a <> UnitBag x ; :: thesis: contradiction
then (1_1 (x,L)) . b = (0_ (X,L)) . b by FUNCT_7:32
.= 0. L by POLYNOM1:22 ;
hence contradiction by A1, POLYNOM1:def 3; :: thesis: verum

end;

hence a in {(UnitBag x)} by TARSKI:def 1; :: thesis: verum

end;

assume A2: a in {(UnitBag x)} ; :: thesis: a in Support (1_1 (x,L))
then a = UnitBag x by TARSKI:def 1;
then (1_1 (x,L)) . a <> 0. L by Th12;
hence a in Support (1_1 (x,L)) by A2, POLYNOM1:def 3; :: thesis: verum

end;

hence Support (1_1 (x,L)) = {(UnitBag x)} by TARSKI:1; :: thesis: verum