let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for x being Element of (Polynom-Ring L)
for p being sequence of L st x = p holds
- x = - p
let x be Element of (Polynom-Ring L); :: 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 x' = x as Polynomial of L by POLYNOM3:def 12;
A2: dom (0_. L) = NAT by FUNCT_2:def 1;
A3: dom (p - p) = NAT by FUNCT_2:def 1;

now

let i be set ; :: thesis: ( i in NAT implies (p - p) . i = (0_. L) . i )
assume A4: i in NAT ; :: thesis: (p - p) . i = (0_. L) . i
then reconsider i' = i as Element of NAT ;
thus (p - p) . i = (p . i') - (p . i') by POLYNOM3:27
.= 0. L by RLVECT_1:28
.= (0_. L) . i by A4, FUNCOP_1:13 ; :: thesis: verum

end;

then A5: p - p = 0_. L by A2, A3, FUNCT_1:9;
reconsider mx = - x' as Element of (Polynom-Ring L) by POLYNOM3:def 12;
x + mx = x' + (- x') by POLYNOM3:def 12
.= 0. (Polynom-Ring L) by A1, A5, POLYNOM3:def 12 ;
then x = - mx by RLVECT_1:19;
hence - x = - p by A1, RLVECT_1:30; :: thesis: verum