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

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)

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;

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

hence
u in Support (- p)
by POLYNOM1:def 4; :: thesis: verumassume
(- 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;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

now :: thesis: for u being object st u in Support (- p) holds

u in Support p

hence
Support (- p) = Support p
by A1, TARSKI:2; :: thesis: verumu 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;

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

hence
u in Support p
by POLYNOM1:def 4; :: thesis: verumA6:
(- 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;assume p . u9 = 0. L ; :: thesis: contradiction

hence contradiction by A5, A6, RLVECT_1:12; :: thesis: verum