let L be non empty right_complementable left-distributive well-unital add-associative right_zeroed doubleLoopStr ; :: thesis: for x being Element of L holds Roots <%(- x),(1. L)%> = {x}
let x be Element of L; :: thesis: Roots <%(- x),(1. L)%> = {x}
now :: thesis: for a being object holds
( ( a in Roots <%(- x),(1. L)%> implies x = a ) & ( a = x implies a in Roots <%(- x),(1. L)%> ) )
let a be object ; :: thesis: ( ( a in Roots <%(- x),(1. L)%> implies x = a ) & ( a = x implies a in Roots <%(- x),(1. L)%> ) )
hereby :: thesis: ( a = x implies a in Roots <%(- x),(1. L)%> )
assume A1: a in Roots <%(- x),(1. L)%> ; :: thesis: x = a
then reconsider b = a as Element of L ;
b is_a_root_of <%(- x),(1. L)%> by A1, POLYNOM5:def 10;
then 0. L = eval (<%(- x),(1. L)%>,b)
.= (- x) + b by POLYNOM5:47 ;
then - x = - b by RLVECT_1:6;
hence x = a by RLVECT_1:18; :: thesis: verum
end;
eval (<%(- x),(1. L)%>,x) = (- x) + x by POLYNOM5:47
.= 0. L by RLVECT_1:5 ;
then A2: x is_a_root_of <%(- x),(1. L)%> ;
assume a = x ; :: thesis: a in Roots <%(- x),(1. L)%>
hence a in Roots <%(- x),(1. L)%> by A2, POLYNOM5:def 10; :: thesis: verum
end;
hence Roots <%(- x),(1. L)%> = {x} by TARSKI:def 1; :: thesis: verum