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)}

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 :: thesis: for a being object holds

( ( a in Support (1_1 (x,L)) implies a in {(UnitBag x)} ) & ( a in {(UnitBag x)} implies a in Support (1_1 (x,L)) ) )

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

let a be object ; :: 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)) ) )

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 4; :: thesis: verum

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

assume A2:
a in {(UnitBag x)}
; :: thesis: 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 ;

end;then reconsider b = a as Element of Bags X ;

now :: thesis: not a <> UnitBag x

hence
a in {(UnitBag x)}
by TARSKI:def 1; :: thesis: verumassume
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;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

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 4; :: thesis: verum