let X be set ; :: thesis: for x being Element of X
for L being non empty 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 empty 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 empty 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:34
.= 0. L by POLYNOM1:81 ;
hence contradiction by A1, POLYNOM1:def 9; :: 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 9; :: thesis: verum

end;

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