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;
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 A3, FUNCOP_1:7 ; :: thesis: verum
end;
reconsider mx = - x9 as Element of (Polynom-Ring 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