let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for x being Element of ()
for p being sequence of L st x = p holds
- x = - p

let x be Element of (); :: thesis: for p being sequence of L st x = p holds
- x = - p

let p be sequence of L; :: thesis: ( x = p implies - x = - p )
assume A1: x = p ; :: thesis: - x = - p
reconsider x9 = x as Polynomial of L by POLYNOM3:def 10;
A2: now :: thesis: for i being object st i in NAT holds
(p - p) . i = (0_. L) . i
let i be object ; :: thesis: ( i in NAT implies (p - p) . i = (0_. L) . i )
assume A3: i in NAT ; :: thesis: (p - p) . i = (0_. L) . i
then reconsider i9 = i as Element of NAT ;
thus (p - p) . i = (p . i9) - (p . i9) by POLYNOM3:27
.= 0. L by RLVECT_1:15
.= (0_. L) . i by ; :: thesis: verum
end;
reconsider mx = - x9 as Element of () by POLYNOM3:def 10;
A4: p - p = 0_. L by A2;
x + mx = x9 + (- x9) by POLYNOM3:def 10
.= 0. () by ;
then x = - mx by RLVECT_1:6;
hence - x = - p by ; :: thesis: verum