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 x9 = x as Polynomial of L by POLYNOM3:def 10;

A4: p - p = 0_. L by A2;

x + mx = x9 + (- x9) by POLYNOM3:def 10

.= 0. (Polynom-Ring L) by A1, A4, POLYNOM3:def 10 ;

then x = - mx by RLVECT_1:6;

hence - x = - p by A1, RLVECT_1:17; :: thesis: verum

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

reconsider mx = - x9 as Element of (Polynom-Ring L) by POLYNOM3:def 10;(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 A3, FUNCOP_1:7 ; :: thesis: verum

end;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 A3, FUNCOP_1:7 ; :: thesis: verum

A4: p - p = 0_. L by A2;

x + mx = x9 + (- x9) by POLYNOM3:def 10

.= 0. (Polynom-Ring L) by A1, A4, POLYNOM3:def 10 ;

then x = - mx by RLVECT_1:6;

hence - x = - p by A1, RLVECT_1:17; :: thesis: verum