let n be Ordinal; :: thesis: for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds Support (- p) = Support p
let L be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of n,L holds Support (- p) = Support p
let p be Polynomial of n,L; :: thesis: Support (- p) = Support p

A1: now

let u be set ; :: thesis: ( u in Support p implies u in Support (- p) )
assume A2: u in Support p ; :: thesis: u in Support (- p)
then reconsider u9 = u as Element of Bags n ;
A3: p . u9 <> 0. L by A2, POLYNOM1:def 9;

now

assume (- p) . u9 = 0. L ; :: thesis: contradiction
then (- p) . u9 = - (- (0. L)) by RLVECT_1:30;
then - (p . u9) = - (- (0. L)) by POLYNOM1:def 22
.= 0. L by RLVECT_1:30 ;
then p . u9 = - (0. L) by RLVECT_1:30;
hence contradiction by A3, RLVECT_1:25; :: thesis: verum

end;

hence u in Support (- p) by POLYNOM1:def 9; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in Support (- p) implies u in Support p )
assume A4: u in Support (- p) ; :: thesis: u in Support p
then reconsider u9 = u as Element of Bags n ;
A5: (- p) . u9 <> 0. L by A4, POLYNOM1:def 9;

now

A6: (- p) . u9 = - (p . u9) by POLYNOM1:def 22;
assume p . u9 = 0. L ; :: thesis: contradiction
hence contradiction by A5, A6, RLVECT_1:25; :: thesis: verum

end;

hence u in Support p by POLYNOM1:def 9; :: thesis: verum

end;

hence Support (- p) = Support p by A1, TARSKI:2; :: thesis: verum