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)) = {()}

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)) = {()}
let L be non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr ; :: thesis: Support (1_1 (x,L)) = {()}
now :: thesis: for a being object holds
( ( a in Support (1_1 (x,L)) implies a in {()} ) & ( a in {()} implies a in Support (1_1 (x,L)) ) )
let a be object ; :: thesis: ( ( a in Support (1_1 (x,L)) implies a in {()} ) & ( a in {()} implies a in Support (1_1 (x,L)) ) )
hereby :: thesis: ( a in {()} implies a in Support (1_1 (x,L)) )
assume A1: a in Support (1_1 (x,L)) ; :: thesis: a in {()}
then reconsider b = a as Element of Bags X ;
now :: thesis: not a <> UnitBag x
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 4; :: thesis: verum
end;
hence a in {()} by TARSKI:def 1; :: thesis: verum
end;
assume A2: a in {()} ; :: 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 ; :: thesis: verum
end;
hence Support (1_1 (x,L)) = {()} by TARSKI:2; :: thesis: verum