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 :: thesis: for u being object st u in Support p holds
u in Support (- p)
let u be object ; :: 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 4;
now :: thesis: not (- p) . u9 = 0. L
assume (- p) . u9 = 0. L ; :: thesis: contradiction
then (- p) . u9 = - (- (0. L)) by RLVECT_1:17;
then - (p . u9) = - (- (0. L)) by POLYNOM1:17
.= 0. L by RLVECT_1:17 ;
then p . u9 = - (0. L) by RLVECT_1:17;
hence contradiction by A3, RLVECT_1:12; :: thesis: verum
end;
hence u in Support (- p) by POLYNOM1:def 4; :: thesis: verum
end;
now :: thesis: for u being object st u in Support (- p) holds
u in Support p
let u be object ; :: 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 4;
now :: thesis: not p . u9 = 0. L
A6: (- p) . u9 = - (p . u9) by POLYNOM1:17;
assume p . u9 = 0. L ; :: thesis: contradiction
hence contradiction by A5, A6, RLVECT_1:12; :: thesis: verum
end;
hence u in Support p by POLYNOM1:def 4; :: thesis: verum
end;
hence Support (- p) = Support p by A1, TARSKI:2; :: thesis: verum